%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEV397^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 : n093.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:34:08 EDT 2014 % Result : Theorem 8.59s % Output : Proof 8.59s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEV397^5 : TPTP v6.1.0. Released v4.0.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n093.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 09:06:06 CDT 2014 % % CPUTime : 8.59 % 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 0x1329290>, <kernel.Type object at 0x1347d40>) of role type named a_type % Using role type % Declaring a:Type % FOF formula (<kernel.Constant object at 0x1329908>, <kernel.DependentProduct object at 0x1347b48>) of role type named cZ % Using role type % Declaring cZ:(a->Prop) % FOF formula (<kernel.Constant object at 0x13293b0>, <kernel.DependentProduct object at 0x1347cb0>) of role type named cY % Using role type % Declaring cY:(a->Prop) % FOF formula (<kernel.Constant object at 0x1329290>, <kernel.DependentProduct object at 0x1347ab8>) of role type named cX % Using role type % Declaring cX:(a->Prop) % FOF formula (forall (Xx:a), ((iff ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))) of role conjecture named cTHM59_pme % Conjecture to prove = (forall (Xx:a), ((iff ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))):Prop % Parameter a_DUMMY:a. % We need to prove ['(forall (Xx:a), ((iff ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))))'] % Parameter a:Type. % Parameter cZ:(a->Prop). % Parameter cY:(a->Prop). % Parameter cX:(a->Prop). % Trying to prove (forall (Xx:a), ((iff ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))) % Found or_intror00:=(or_intror0 (cZ Xx)):((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found (or_intror0 (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found or_intror00:=(or_intror0 (cZ Xx)):((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found (or_intror0 (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found or_intror00:=(or_intror0 (cZ Xx)):((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found (or_intror0 (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found or_intror00:=(or_intror0 (cZ Xx)):((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found (or_intror0 (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found or_intror00:=(or_intror0 (cZ Xx)):((cZ Xx)->((or (cY Xx)) (cZ Xx))) % Found (or_intror0 (cZ Xx)) as proof of ((cZ Xx)->((or (cY Xx)) (cZ Xx))) % Found ((or_intror (cY Xx)) (cZ Xx)) as proof of ((cZ Xx)->((or (cY Xx)) (cZ Xx))) % Found ((or_intror (cY Xx)) (cZ Xx)) as proof of ((cZ Xx)->((or (cY Xx)) (cZ Xx))) % Found or_intror00:=(or_intror0 (cZ Xx)):((cZ Xx)->((or (cX Xx)) (cZ Xx))) % Found (or_intror0 (cZ Xx)) as proof of ((cZ Xx)->((or (cX Xx)) (cZ Xx))) % Found ((or_intror (cX Xx)) (cZ Xx)) as proof of ((cZ Xx)->((or (cX Xx)) (cZ Xx))) % Found ((or_intror (cX Xx)) (cZ Xx)) as proof of ((cZ Xx)->((or (cX Xx)) (cZ Xx))) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_intror00:=(or_intror0 (cZ Xx)):((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found (or_intror0 (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_intror00:=(or_intror0 (cZ Xx)):((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found (or_intror0 (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found or_intror00:=(or_intror0 (cZ Xx)):((cZ Xx)->((or (cX Xx)) (cZ Xx))) % Found (or_intror0 (cZ Xx)) as proof of ((cZ Xx)->((or (cX Xx)) (cZ Xx))) % Found ((or_intror (cX Xx)) (cZ Xx)) as proof of ((cZ Xx)->((or (cX Xx)) (cZ Xx))) % Found ((or_intror (cX Xx)) (cZ Xx)) as proof of ((cZ Xx)->((or (cX Xx)) (cZ Xx))) % Found or_intror00:=(or_intror0 (cZ Xx)):((cZ Xx)->((or (cY Xx)) (cZ Xx))) % Found (or_intror0 (cZ Xx)) as proof of ((cZ Xx)->((or (cY Xx)) (cZ Xx))) % Found ((or_intror (cY Xx)) (cZ Xx)) as proof of ((cZ Xx)->((or (cY Xx)) (cZ Xx))) % Found ((or_intror (cY Xx)) (cZ Xx)) as proof of ((cZ Xx)->((or (cY Xx)) (cZ Xx))) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_intror00:=(or_intror0 (cZ Xx)):((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found (or_intror0 (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found or_intror00:=(or_intror0 (cZ Xx)):((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found (or_intror0 (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)) as proof of ((cZ Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found or_introl00:=(or_introl0 (cZ Xx)):((cY Xx)->((or (cY Xx)) (cZ Xx))) % Found (or_introl0 (cZ Xx)) as proof of ((cY Xx)->((or (cY Xx)) (cZ Xx))) % Found ((or_introl (cY Xx)) (cZ Xx)) as proof of ((cY Xx)->((or (cY Xx)) (cZ Xx))) % Found (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx))) as proof of ((cY Xx)->((or (cY Xx)) (cZ Xx))) % Found (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx))) as proof of ((cX Xx)->((cY Xx)->((or (cY Xx)) (cZ Xx)))) % Found (and_rect00 (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))) as proof of ((or (cY Xx)) (cZ Xx)) % Found ((and_rect0 ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))) as proof of ((or (cY Xx)) (cZ Xx)) % Found (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))) as proof of ((or (cY Xx)) (cZ Xx)) % Found (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx))))) as proof of ((or (cY Xx)) (cZ Xx)) % Found (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx))))) as proof of (((and (cX Xx)) (cY Xx))->((or (cY Xx)) (cZ Xx))) % Found ((or_ind00 (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx))) as proof of ((or (cY Xx)) (cZ Xx)) % Found (((or_ind0 ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx))) as proof of ((or (cY Xx)) (cZ Xx)) % Found ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx))) as proof of ((or (cY Xx)) (cZ Xx)) % Found ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx))) as proof of ((or (cY Xx)) (cZ Xx)) % Found or_introl00:=(or_introl0 (cX Xx)):((cZ Xx)->((or (cZ Xx)) (cX Xx))) % Found (or_introl0 (cX Xx)) as proof of ((cZ Xx)->((or (cZ Xx)) (cX Xx))) % Found ((or_introl (cZ Xx)) (cX Xx)) as proof of ((cZ Xx)->((or (cZ Xx)) (cX Xx))) % Found ((or_introl (cZ Xx)) (cX Xx)) as proof of ((cZ Xx)->((or (cZ Xx)) (cX Xx))) % Found x0:(cZ Xx) % Found (fun (x0:(cZ Xx))=> x0) as proof of (cZ Xx) % Found (fun (x0:(cZ Xx))=> x0) as proof of ((cZ Xx)->(cZ Xx)) % Found or_introl000:=(or_introl00 (cZ Xx)):((or (cX Xx)) (cZ Xx)) % Found (or_introl00 (cZ Xx)) as proof of ((or (cX Xx)) (cZ Xx)) % Found ((fun (B:Prop)=> ((or_introl0 B) x1)) (cZ Xx)) as proof of ((or (cX Xx)) (cZ Xx)) % Found ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)) as proof of ((or (cX Xx)) (cZ Xx)) % Found (fun (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx))) as proof of ((or (cX Xx)) (cZ Xx)) % Found (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx))) as proof of ((cY Xx)->((or (cX Xx)) (cZ Xx))) % Found (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx))) as proof of ((cX Xx)->((cY Xx)->((or (cX Xx)) (cZ Xx)))) % Found (and_rect00 (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))) as proof of ((or (cX Xx)) (cZ Xx)) % Found ((and_rect0 ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))) as proof of ((or (cX Xx)) (cZ Xx)) % Found (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))) as proof of ((or (cX Xx)) (cZ Xx)) % Found (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx))))) as proof of ((or (cX Xx)) (cZ Xx)) % Found (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx))))) as proof of (((and (cX Xx)) (cY Xx))->((or (cX Xx)) (cZ Xx))) % Found ((or_ind00 (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx))) as proof of ((or (cX Xx)) (cZ Xx)) % Found (((or_ind0 ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx))) as proof of ((or (cX Xx)) (cZ Xx)) % Found ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx))) as proof of ((or (cX Xx)) (cZ Xx)) % Found ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx))) as proof of ((or (cX Xx)) (cZ Xx)) % Found ((conj10 ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx)))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx)))) as proof of ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) % Found (((conj1 ((or (cY Xx)) (cZ Xx))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx)))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx)))) as proof of ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) % Found ((((conj ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx)))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx)))) as proof of ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) % Found (fun (x:((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))=> ((((conj ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx)))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx))))) as proof of ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) % Found (fun (x:((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))=> ((((conj ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx)))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx))))) as proof of (((or ((and (cX Xx)) (cY Xx))) (cZ Xx))->((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))) % Found x2:(cY Xx) % Found x2 as proof of (cY Xx) % Found x2:(cX Xx) % Found x2 as proof of (cX Xx) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found or_introl00:=(or_introl0 ((and (cX Xx)) (cY Xx))):((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found (or_introl0 ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found ((or_introl (cZ Xx)) ((and (cX Xx)) (cY Xx))) as proof of ((cZ Xx)->((or (cZ Xx)) ((and (cX Xx)) (cY Xx)))) % Found x3:(cZ Xx) % Found (fun (x3:(cZ Xx))=> x3) as proof of (cZ Xx) % Found (fun (x3:(cZ Xx))=> x3) as proof of ((cZ Xx)->(cZ Xx)) % Found x3:(cZ Xx) % Found (fun (x3:(cZ Xx))=> x3) as proof of (cZ Xx) % Found (fun (x3:(cZ Xx))=> x3) as proof of ((cZ Xx)->(cZ Xx)) % Found x3:(cZ Xx) % Found (fun (x3:(cZ Xx))=> x3) as proof of (cZ Xx) % Found (fun (x3:(cZ Xx))=> x3) as proof of ((cZ Xx)->(cZ Xx)) % Found x3:(cZ Xx) % Found (fun (x3:(cZ Xx))=> x3) as proof of (cZ Xx) % Found (fun (x3:(cZ Xx))=> x3) as proof of ((cZ Xx)->(cZ Xx)) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found x2:(cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of (cZ Xx) % Found (fun (x2:(cZ Xx))=> x2) as proof of ((cZ Xx)->(cZ Xx)) % Found x3:(cZ Xx) % Found (fun (x3:(cZ Xx))=> x3) as proof of (cZ Xx) % Found (fun (x3:(cZ Xx))=> x3) as proof of ((cZ Xx)->(cZ Xx)) % Found x3:(cZ Xx) % Found (fun (x3:(cZ Xx))=> x3) as proof of (cZ Xx) % Found (fun (x3:(cZ Xx))=> x3) as proof of ((cZ Xx)->(cZ Xx)) % Found conj1000:=(conj100 x3):((and (cX Xx)) (cY Xx)) % Found (conj100 x3) as proof of ((and (cX Xx)) (cY Xx)) % Found ((conj10 (cY Xx)) x3) as proof of ((and (cX Xx)) (cY Xx)) % Found (((fun (B:Prop)=> ((conj1 B) x2)) (cY Xx)) x3) as proof of ((and (cX Xx)) (cY Xx)) % Found (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3) as proof of ((and (cX Xx)) (cY Xx)) % Found (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3) as proof of ((and (cX Xx)) (cY Xx)) % Found (or_introl00 (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found ((or_introl0 (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3))) as proof of ((cY Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_ind10 (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found (((or_ind1 ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)))) as proof of ((cX Xx)->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((or_ind00 (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found (((or_ind0 ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found (fun (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)))) as proof of (((or (cY Xx)) (cZ Xx))->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)))) as proof of (((or (cX Xx)) (cZ Xx))->(((or (cY Xx)) (cZ Xx))->((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))) % Found (and_rect00 (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found ((and_rect0 ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found (((fun (P:Type) (x0:(((or (cX Xx)) (cZ Xx))->(((or (cY Xx)) (cZ Xx))->P)))=> (((((and_rect ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) P) x0) x)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found (fun (x:((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))=> (((fun (P:Type) (x0:(((or (cX Xx)) (cZ Xx))->(((or (cY Xx)) (cZ Xx))->P)))=> (((((and_rect ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) P) x0) x)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)))))) as proof of ((or ((and (cX Xx)) (cY Xx))) (cZ Xx)) % Found (fun (x:((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))=> (((fun (P:Type) (x0:(((or (cX Xx)) (cZ Xx))->(((or (cY Xx)) (cZ Xx))->P)))=> (((((and_rect ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) P) x0) x)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)))))) as proof of (((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))->((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) % Found ((conj00 (fun (x:((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))=> ((((conj ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx)))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx)))))) (fun (x:((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))=> (((fun (P:Type) (x0:(((or (cX Xx)) (cZ Xx))->(((or (cY Xx)) (cZ Xx))->P)))=> (((((and_rect ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) P) x0) x)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))))) as proof of ((iff ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))) % Found (((conj0 (((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))->((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))) (fun (x:((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))=> ((((conj ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx)))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx)))))) (fun (x:((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))=> (((fun (P:Type) (x0:(((or (cX Xx)) (cZ Xx))->(((or (cY Xx)) (cZ Xx))->P)))=> (((((and_rect ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) P) x0) x)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))))) as proof of ((iff ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))) % Found ((((conj (((or ((and (cX Xx)) (cY Xx))) (cZ Xx))->((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))) (((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))->((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))) (fun (x:((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))=> ((((conj ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx)))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx)))))) (fun (x:((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))=> (((fun (P:Type) (x0:(((or (cX Xx)) (cZ Xx))->(((or (cY Xx)) (cZ Xx))->P)))=> (((((and_rect ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) P) x0) x)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))))) as proof of ((iff ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))) % Found (fun (Xx:a)=> ((((conj (((or ((and (cX Xx)) (cY Xx))) (cZ Xx))->((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))) (((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))->((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))) (fun (x:((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))=> ((((conj ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx)))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx)))))) (fun (x:((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))=> (((fun (P:Type) (x0:(((or (cX Xx)) (cZ Xx))->(((or (cY Xx)) (cZ Xx))->P)))=> (((((and_rect ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) P) x0) x)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)))))))) as proof of ((iff ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))) % Found (fun (Xx:a)=> ((((conj (((or ((and (cX Xx)) (cY Xx))) (cZ Xx))->((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))) (((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))->((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))) (fun (x:((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))=> ((((conj ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx)))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx)))))) (fun (x:((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))=> (((fun (P:Type) (x0:(((or (cX Xx)) (cZ Xx))->(((or (cY Xx)) (cZ Xx))->P)))=> (((((and_rect ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) P) x0) x)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)))))))) as proof of (forall (Xx:a), ((iff ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) ((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))) % Got proof (fun (Xx:a)=> ((((conj (((or ((and (cX Xx)) (cY Xx))) (cZ Xx))->((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))) (((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))->((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))) (fun (x:((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))=> ((((conj ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx)))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx)))))) (fun (x:((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))=> (((fun (P:Type) (x0:(((or (cX Xx)) (cZ Xx))->(((or (cY Xx)) (cZ Xx))->P)))=> (((((and_rect ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) P) x0) x)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)))))))) % Time elapsed = 8.136111s % node=1751 cost=925.000000 depth=30 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (Xx:a)=> ((((conj (((or ((and (cX Xx)) (cY Xx))) (cZ Xx))->((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))) (((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx)))->((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))) (fun (x:((or ((and (cX Xx)) (cY Xx))) (cZ Xx)))=> ((((conj ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cX Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cX Xx)) (cZ Xx))) (fun (x1:(cX Xx)) (x2:(cY Xx))=> ((fun (B:Prop)=> (((or_introl (cX Xx)) B) x1)) (cZ Xx)))))) ((or_intror (cX Xx)) (cZ Xx)))) ((((fun (P:Prop) (x0:(((and (cX Xx)) (cY Xx))->P)) (x1:((cZ Xx)->P))=> ((((((or_ind ((and (cX Xx)) (cY Xx))) (cZ Xx)) P) x0) x1) x)) ((or (cY Xx)) (cZ Xx))) (fun (x0:((and (cX Xx)) (cY Xx)))=> (((fun (P:Type) (x1:((cX Xx)->((cY Xx)->P)))=> (((((and_rect (cX Xx)) (cY Xx)) P) x1) x0)) ((or (cY Xx)) (cZ Xx))) (fun (x1:(cX Xx))=> ((or_introl (cY Xx)) (cZ Xx)))))) ((or_intror (cY Xx)) (cZ Xx)))))) (fun (x:((and ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))))=> (((fun (P:Type) (x0:(((or (cX Xx)) (cZ Xx))->(((or (cY Xx)) (cZ Xx))->P)))=> (((((and_rect ((or (cX Xx)) (cZ Xx))) ((or (cY Xx)) (cZ Xx))) P) x0) x)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x0:((or (cX Xx)) (cZ Xx))) (x1:((or (cY Xx)) (cZ Xx)))=> ((((fun (P:Prop) (x2:((cX Xx)->P)) (x3:((cZ Xx)->P))=> ((((((or_ind (cX Xx)) (cZ Xx)) P) x2) x3) x0)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x2:(cX Xx))=> ((((fun (P:Prop) (x3:((cY Xx)->P)) (x4:((cZ Xx)->P))=> ((((((or_ind (cY Xx)) (cZ Xx)) P) x3) x4) x1)) ((or ((and (cX Xx)) (cY Xx))) (cZ Xx))) (fun (x3:(cY Xx))=> (((or_introl ((and (cX Xx)) (cY Xx))) (cZ Xx)) (((fun (B:Prop)=> (((conj (cX Xx)) B) x2)) (cY Xx)) x3)))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx))))) ((or_intror ((and (cX Xx)) (cY Xx))) (cZ Xx)))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------