%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SYO160^5 : TPTP v7.5.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 0s % DateTime : Tue Mar 29 00:50:48 EDT 2022 % Result : Theorem 2.39s 2.60s % Output : Proof 2.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SYO160^5 : TPTP v7.5.0. Released v4.0.0. % 0.07/0.12 % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.32 % Computer : n009.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % RAMPerCPU : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % DateTime : Fri Mar 11 16:50:22 EST 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.12/0.34 Python 2.7.5 % 1.69/1.94 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 1.69/1.94 FOF formula (<kernel.Constant object at 0xe513b0>, <kernel.Constant object at 0xe51830>) of role type named c % 1.69/1.94 Using role type % 1.69/1.94 Declaring c:fofType % 1.69/1.94 FOF formula (<kernel.Constant object at 0xe56098>, <kernel.DependentProduct object at 0xe51a70>) of role type named cR % 1.69/1.94 Using role type % 1.69/1.94 Declaring cR:(fofType->Prop) % 1.69/1.94 FOF formula (<kernel.Constant object at 0xe513b0>, <kernel.Single object at 0xe51560>) of role type named b % 1.69/1.94 Using role type % 1.69/1.94 Declaring b:fofType % 1.69/1.94 FOF formula (<kernel.Constant object at 0xe51950>, <kernel.Single object at 0xe51290>) of role type named a % 1.69/1.94 Using role type % 1.69/1.94 Declaring a:fofType % 1.69/1.94 FOF formula (<kernel.Constant object at 0xe515f0>, <kernel.DependentProduct object at 0xe51200>) of role type named cQ % 1.69/1.94 Using role type % 1.69/1.94 Declaring cQ:(fofType->Prop) % 1.69/1.94 FOF formula (<kernel.Constant object at 0xe51290>, <kernel.DependentProduct object at 0xe514d0>) of role type named cP % 1.69/1.94 Using role type % 1.69/1.94 Declaring cP:(fofType->Prop) % 1.69/1.94 FOF formula (((and ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx))))->((and ((and (cR a)) (cR b))) (cR c))) of role conjecture named cDISJ_THIRD % 1.69/1.94 Conjecture to prove = (((and ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx))))->((and ((and (cR a)) (cR b))) (cR c))):Prop % 1.69/1.94 We need to prove ['(((and ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx))))->((and ((and (cR a)) (cR b))) (cR c)))'] % 1.69/1.94 Parameter fofType:Type. % 1.69/1.94 Parameter c:fofType. % 1.69/1.94 Parameter cR:(fofType->Prop). % 1.69/1.94 Parameter b:fofType. % 1.69/1.94 Parameter a:fofType. % 1.69/1.94 Parameter cQ:(fofType->Prop). % 1.69/1.94 Parameter cP:(fofType->Prop). % 1.69/1.94 Trying to prove (((and ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx))))->((and ((and (cR a)) (cR b))) (cR c))) % 1.69/1.94 Found x40:=(x4 c):(cP c) % 1.69/1.94 Found (x4 c) as proof of (cP c) % 1.69/1.94 Found (x4 c) as proof of (cP c) % 1.69/1.94 Found (x30 (x4 c)) as proof of (cR c) % 1.69/1.94 Found ((x3 c) (x4 c)) as proof of (cR c) % 1.69/1.94 Found ((x3 c) (x4 c)) as proof of (cR c) % 1.69/1.94 Found x40:=(x4 c):(cQ c) % 1.69/1.94 Found (x4 c) as proof of (cQ c) % 1.69/1.94 Found (x4 c) as proof of (cQ c) % 1.69/1.94 Found (x10 (x4 c)) as proof of (cR c) % 1.69/1.94 Found ((x1 c) (x4 c)) as proof of (cR c) % 1.69/1.94 Found ((x1 c) (x4 c)) as proof of (cR c) % 1.69/1.94 Found x40:=(x4 c):(cP c) % 1.69/1.94 Found (x4 c) as proof of (cP c) % 1.69/1.94 Found (fun (x4:(forall (Xx:fofType), (cP Xx)))=> (x4 c)) as proof of (cP c) % 1.69/1.94 Found (fun (x4:(forall (Xx:fofType), (cP Xx)))=> (x4 c)) as proof of ((forall (Xx:fofType), (cP Xx))->(cP c)) % 1.69/1.94 Found x40:=(x4 c):(cQ c) % 1.69/1.94 Found (x4 c) as proof of (cQ c) % 1.69/1.94 Found (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> (x4 c)) as proof of (cQ c) % 1.69/1.94 Found (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> (x4 c)) as proof of ((forall (Xx:fofType), (cQ Xx))->(cQ c)) % 1.69/1.94 Found x40:=(x4 c):(cP c) % 1.69/1.94 Found (x4 c) as proof of (cP c) % 1.69/1.94 Found (x4 c) as proof of (cP c) % 1.69/1.94 Found (x30 (x4 c)) as proof of (cR c) % 1.69/1.94 Found ((x3 c) (x4 c)) as proof of (cR c) % 1.69/1.94 Found (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c))) as proof of (cR c) % 1.69/1.94 Found (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c))) as proof of ((forall (Xx:fofType), (cP Xx))->(cR c)) % 1.69/1.94 Found x40:=(x4 c):(cQ c) % 1.69/1.94 Found (x4 c) as proof of (cQ c) % 1.69/1.94 Found (x4 c) as proof of (cQ c) % 1.69/1.94 Found (x10 (x4 c)) as proof of (cR c) % 1.69/1.94 Found ((x1 c) (x4 c)) as proof of (cR c) % 1.69/1.94 Found (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c))) as proof of (cR c) % 1.69/1.94 Found (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c))) as proof of ((forall (Xx:fofType), (cQ Xx))->(cR c)) % 1.69/1.94 Found ((or_ind00 (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))) as proof of (cR c) % 1.69/1.94 Found (((or_ind0 (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))) as proof of (cR c) % 2.32/2.56 Found ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))) as proof of (cR c) % 2.32/2.56 Found ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))) as proof of (cR c) % 2.32/2.56 Found x40:=(x4 c):(cQ c) % 2.32/2.56 Found (x4 c) as proof of (cQ c) % 2.32/2.56 Found (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> (x4 c)) as proof of (cQ c) % 2.32/2.56 Found (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> (x4 c)) as proof of ((forall (Xx:fofType), (cQ Xx))->(cQ c)) % 2.32/2.56 Found x40:=(x4 c):(cP c) % 2.32/2.56 Found (x4 c) as proof of (cP c) % 2.32/2.56 Found (fun (x4:(forall (Xx:fofType), (cP Xx)))=> (x4 c)) as proof of (cP c) % 2.32/2.56 Found (fun (x4:(forall (Xx:fofType), (cP Xx)))=> (x4 c)) as proof of ((forall (Xx:fofType), (cP Xx))->(cP c)) % 2.32/2.56 Found x40:=(x4 c):(cQ c) % 2.32/2.56 Found (x4 c) as proof of (cQ c) % 2.32/2.56 Found (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> (x4 c)) as proof of (cQ c) % 2.32/2.56 Found (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> (x4 c)) as proof of ((forall (Xx:fofType), (cQ Xx))->(cQ c)) % 2.32/2.56 Found x40:=(x4 a):(cQ a) % 2.32/2.56 Found (x4 a) as proof of (cQ a) % 2.32/2.56 Found (x4 a) as proof of (cQ a) % 2.32/2.56 Found (x10 (x4 a)) as proof of (cR a) % 2.32/2.56 Found ((x1 a) (x4 a)) as proof of (cR a) % 2.32/2.56 Found ((x1 a) (x4 a)) as proof of (cR a) % 2.32/2.56 Found x40:=(x4 b):(cQ b) % 2.32/2.56 Found (x4 b) as proof of (cQ b) % 2.32/2.56 Found (x4 b) as proof of (cQ b) % 2.32/2.56 Found (x10 (x4 b)) as proof of (cR b) % 2.32/2.56 Found ((x1 b) (x4 b)) as proof of (cR b) % 2.32/2.56 Found ((x1 b) (x4 b)) as proof of (cR b) % 2.32/2.56 Found ((conj10 ((x1 a) (x4 a))) ((x1 b) (x4 b))) as proof of ((and (cR a)) (cR b)) % 2.32/2.56 Found (((conj1 (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b))) as proof of ((and (cR a)) (cR b)) % 2.32/2.56 Found ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b))) as proof of ((and (cR a)) (cR b)) % 2.32/2.56 Found (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))) as proof of ((and (cR a)) (cR b)) % 2.32/2.56 Found (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))) as proof of ((forall (Xx:fofType), (cQ Xx))->((and (cR a)) (cR b))) % 2.32/2.56 Found x40:=(x4 b):(cP b) % 2.32/2.56 Found (x4 b) as proof of (cP b) % 2.32/2.56 Found (x4 b) as proof of (cP b) % 2.32/2.56 Found (x30 (x4 b)) as proof of (cR b) % 2.32/2.56 Found ((x3 b) (x4 b)) as proof of (cR b) % 2.32/2.56 Found ((x3 b) (x4 b)) as proof of (cR b) % 2.32/2.56 Found x40:=(x4 a):(cP a) % 2.32/2.56 Found (x4 a) as proof of (cP a) % 2.32/2.56 Found (x4 a) as proof of (cP a) % 2.32/2.56 Found (x30 (x4 a)) as proof of (cR a) % 2.32/2.56 Found ((x3 a) (x4 a)) as proof of (cR a) % 2.32/2.56 Found ((x3 a) (x4 a)) as proof of (cR a) % 2.32/2.56 Found ((conj10 ((x3 a) (x4 a))) ((x3 b) (x4 b))) as proof of ((and (cR a)) (cR b)) % 2.32/2.56 Found (((conj1 (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))) as proof of ((and (cR a)) (cR b)) % 2.32/2.56 Found ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))) as proof of ((and (cR a)) (cR b)) % 2.32/2.56 Found (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b)))) as proof of ((and (cR a)) (cR b)) % 2.32/2.56 Found (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b)))) as proof of ((forall (Xx:fofType), (cP Xx))->((and (cR a)) (cR b))) % 2.32/2.56 Found ((or_ind00 (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b))))) as proof of ((and (cR a)) (cR b)) % 2.32/2.56 Found (((or_ind0 ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b))))) as proof of ((and (cR a)) (cR b)) % 2.32/2.56 Found ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b))))) as proof of ((and (cR a)) (cR b)) % 2.32/2.56 Found ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b))))) as proof of ((and (cR a)) (cR b)) % 2.32/2.56 Found ((conj00 ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c))))) as proof of ((and ((and (cR a)) (cR b))) (cR c)) % 2.32/2.56 Found (((conj0 (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c))))) as proof of ((and ((and (cR a)) (cR b))) (cR c)) % 2.32/2.56 Found ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c))))) as proof of ((and ((and (cR a)) (cR b))) (cR c)) % 2.32/2.56 Found (fun (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))))) as proof of ((and ((and (cR a)) (cR b))) (cR c)) % 2.32/2.56 Found (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))))) as proof of ((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->((and ((and (cR a)) (cR b))) (cR c))) % 2.32/2.56 Found (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))))) as proof of (((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))->((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->((and ((and (cR a)) (cR b))) (cR c)))) % 2.32/2.56 Found (and_rect10 (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c))))))) as proof of ((and ((and (cR a)) (cR b))) (cR c)) % 2.32/2.56 Found ((and_rect1 ((and ((and (cR a)) (cR b))) (cR c))) (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c))))))) as proof of ((and ((and (cR a)) (cR b))) (cR c)) % 2.39/2.56 Found (((fun (P:Type) (x2:(((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))->((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->P)))=> (((((and_rect ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx)))) P) x2) x0)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c))))))) as proof of ((and ((and (cR a)) (cR b))) (cR c)) % 2.39/2.56 Found (fun (x1:(forall (Xx:fofType), ((cQ Xx)->(cR Xx))))=> (((fun (P:Type) (x2:(((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))->((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->P)))=> (((((and_rect ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx)))) P) x2) x0)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))))))) as proof of ((and ((and (cR a)) (cR b))) (cR c)) % 2.39/2.56 Found (fun (x0:((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (x1:(forall (Xx:fofType), ((cQ Xx)->(cR Xx))))=> (((fun (P:Type) (x2:(((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))->((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->P)))=> (((((and_rect ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx)))) P) x2) x0)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))))))) as proof of ((forall (Xx:fofType), ((cQ Xx)->(cR Xx)))->((and ((and (cR a)) (cR b))) (cR c))) % 2.39/2.57 Found (fun (x0:((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (x1:(forall (Xx:fofType), ((cQ Xx)->(cR Xx))))=> (((fun (P:Type) (x2:(((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))->((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->P)))=> (((((and_rect ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx)))) P) x2) x0)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))))))) as proof of (((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))->((forall (Xx:fofType), ((cQ Xx)->(cR Xx)))->((and ((and (cR a)) (cR b))) (cR c)))) % 2.39/2.57 Found (and_rect00 (fun (x0:((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (x1:(forall (Xx:fofType), ((cQ Xx)->(cR Xx))))=> (((fun (P:Type) (x2:(((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))->((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->P)))=> (((((and_rect ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx)))) P) x2) x0)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c))))))))) as proof of ((and ((and (cR a)) (cR b))) (cR c)) % 2.39/2.57 Found ((and_rect0 ((and ((and (cR a)) (cR b))) (cR c))) (fun (x0:((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (x1:(forall (Xx:fofType), ((cQ Xx)->(cR Xx))))=> (((fun (P:Type) (x2:(((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))->((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->P)))=> (((((and_rect ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx)))) P) x2) x0)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c))))))))) as proof of ((and ((and (cR a)) (cR b))) (cR c)) % 2.39/2.57 Found (((fun (P:Type) (x0:(((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))->((forall (Xx:fofType), ((cQ Xx)->(cR Xx)))->P)))=> (((((and_rect ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx)))) P) x0) x)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x0:((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (x1:(forall (Xx:fofType), ((cQ Xx)->(cR Xx))))=> (((fun (P:Type) (x2:(((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))->((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->P)))=> (((((and_rect ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx)))) P) x2) x0)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c))))))))) as proof of ((and ((and (cR a)) (cR b))) (cR c)) % 2.39/2.57 Found (fun (x:((and ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx)))))=> (((fun (P:Type) (x0:(((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))->((forall (Xx:fofType), ((cQ Xx)->(cR Xx)))->P)))=> (((((and_rect ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx)))) P) x0) x)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x0:((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (x1:(forall (Xx:fofType), ((cQ Xx)->(cR Xx))))=> (((fun (P:Type) (x2:(((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))->((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->P)))=> (((((and_rect ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx)))) P) x2) x0)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))))))))) as proof of ((and ((and (cR a)) (cR b))) (cR c)) % 2.39/2.57 Found (fun (x:((and ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx)))))=> (((fun (P:Type) (x0:(((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))->((forall (Xx:fofType), ((cQ Xx)->(cR Xx)))->P)))=> (((((and_rect ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx)))) P) x0) x)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x0:((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (x1:(forall (Xx:fofType), ((cQ Xx)->(cR Xx))))=> (((fun (P:Type) (x2:(((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))->((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->P)))=> (((((and_rect ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx)))) P) x2) x0)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))))))))) as proof of (((and ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx))))->((and ((and (cR a)) (cR b))) (cR c))) % 2.39/2.57 Got proof (fun (x:((and ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx)))))=> (((fun (P:Type) (x0:(((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))->((forall (Xx:fofType), ((cQ Xx)->(cR Xx)))->P)))=> (((((and_rect ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx)))) P) x0) x)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x0:((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (x1:(forall (Xx:fofType), ((cQ Xx)->(cR Xx))))=> (((fun (P:Type) (x2:(((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))->((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->P)))=> (((((and_rect ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx)))) P) x2) x0)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))))))))) % 2.39/2.60 Time elapsed = 1.960536s % 2.39/2.60 node=554 cost=717.000000 depth=30 % 2.39/2.60 :::::::::::::::::::::: % 2.39/2.60 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.39/2.60 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.39/2.60 (fun (x:((and ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx)))))=> (((fun (P:Type) (x0:(((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))->((forall (Xx:fofType), ((cQ Xx)->(cR Xx)))->P)))=> (((((and_rect ((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (forall (Xx:fofType), ((cQ Xx)->(cR Xx)))) P) x0) x)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x0:((and ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx))))) (x1:(forall (Xx:fofType), ((cQ Xx)->(cR Xx))))=> (((fun (P:Type) (x2:(((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))->((forall (Xx:fofType), ((cP Xx)->(cR Xx)))->P)))=> (((((and_rect ((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (forall (Xx:fofType), ((cP Xx)->(cR Xx)))) P) x2) x0)) ((and ((and (cR a)) (cR b))) (cR c))) (fun (x2:((or (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx)))) (x3:(forall (Xx:fofType), ((cP Xx)->(cR Xx))))=> ((((conj ((and (cR a)) (cR b))) (cR c)) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) ((and (cR a)) (cR b))) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((((conj (cR a)) (cR b)) ((x3 a) (x4 a))) ((x3 b) (x4 b))))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((((conj (cR a)) (cR b)) ((x1 a) (x4 a))) ((x1 b) (x4 b)))))) ((((fun (P:Prop) (x4:((forall (Xx:fofType), (cP Xx))->P)) (x5:((forall (Xx:fofType), (cQ Xx))->P))=> ((((((or_ind (forall (Xx:fofType), (cP Xx))) (forall (Xx:fofType), (cQ Xx))) P) x4) x5) x2)) (cR c)) (fun (x4:(forall (Xx:fofType), (cP Xx)))=> ((x3 c) (x4 c)))) (fun (x4:(forall (Xx:fofType), (cQ Xx)))=> ((x1 c) (x4 c)))))))))) % 2.39/2.60 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------