%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SYO266^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 : n021.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:51:02 EDT 2022 % Result : Theorem 11.94s 12.14s % Output : Proof 12.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.11 % Problem : SYO266^5 : TPTP v7.5.0. Released v4.0.0. % 0.08/0.12 % Command : python CASC.py /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % RAMPerCPU : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % DateTime : Fri Mar 11 23:17:09 EST 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.12/0.34 Python 2.7.5 % 4.62/4.85 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox2/benchmark/', '/export/starexec/sandbox2/benchmark/'] % 4.62/4.85 FOF formula (<kernel.Constant object at 0x10413b0>, <kernel.DependentProduct object at 0x2b36ada3aa28>) of role type named cQ % 4.62/4.85 Using role type % 4.62/4.85 Declaring cQ:(fofType->Prop) % 4.62/4.85 FOF formula (<kernel.Constant object at 0x1041d40>, <kernel.DependentProduct object at 0x2b36ada3a3b0>) of role type named cP % 4.62/4.85 Using role type % 4.62/4.85 Declaring cP:(fofType->Prop) % 4.62/4.85 FOF formula ((iff ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (forall (Y:fofType), ((or (cP Y)) (cQ Y)))) of role conjecture named cTHM44 % 4.62/4.85 Conjecture to prove = ((iff ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (forall (Y:fofType), ((or (cP Y)) (cQ Y)))):Prop % 4.62/4.85 Parameter fofType_DUMMY:fofType. % 4.62/4.85 We need to prove ['((iff ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (forall (Y:fofType), ((or (cP Y)) (cQ Y))))'] % 4.62/4.85 Parameter fofType:Type. % 4.62/4.85 Parameter cQ:(fofType->Prop). % 4.62/4.85 Parameter cP:(fofType->Prop). % 4.62/4.85 Trying to prove ((iff ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (forall (Y:fofType), ((or (cP Y)) (cQ Y)))) % 4.62/4.85 Found classic0:=(classic (cQ X)):((or (cQ X)) (not (cQ X))) % 4.62/4.85 Found (classic (cQ X)) as proof of ((or (cQ X)) ((x0 X)->False)) % 4.62/4.85 Found (classic (cQ X)) as proof of ((or (cQ X)) ((x0 X)->False)) % 4.62/4.85 Found (classic (cQ X)) as proof of ((or (cQ X)) ((x0 X)->False)) % 4.62/4.85 Found (or_comm_i00 (classic (cQ X))) as proof of ((or ((x0 X)->False)) (cQ X)) % 4.62/4.85 Found ((or_comm_i0 ((x0 X)->False)) (classic (cQ X))) as proof of ((or ((x0 X)->False)) (cQ X)) % 4.62/4.85 Found (((or_comm_i (cQ X)) ((x0 X)->False)) (classic (cQ X))) as proof of ((or ((x0 X)->False)) (cQ X)) % 4.62/4.85 Found (((or_comm_i (cQ X)) ((x0 X)->False)) (classic (cQ X))) as proof of ((or ((x0 X)->False)) (cQ X)) % 4.62/4.85 Found x1:=(x X):((or (cP X)) (cQ X)) % 4.62/4.85 Found (x X) as proof of ((or (cP X)) (x0 X)) % 4.62/4.85 Found (x X) as proof of ((or (cP X)) (x0 X)) % 4.62/4.85 Found (or_comm_i00 (x X)) as proof of ((or (x0 X)) (cP X)) % 4.62/4.85 Found ((or_comm_i0 (x0 X)) (x X)) as proof of ((or (x0 X)) (cP X)) % 4.62/4.85 Found (((or_comm_i (cP X)) (x0 X)) (x X)) as proof of ((or (x0 X)) (cP X)) % 4.62/4.85 Found (((or_comm_i (cP X)) (x0 X)) (x X)) as proof of ((or (x0 X)) (cP X)) % 4.62/4.85 Found ((conj10 (((or_comm_i (cP X)) (x0 X)) (x X))) (((or_comm_i (cQ X)) ((x0 X)->False)) (classic (cQ X)))) as proof of ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X))) % 4.62/4.85 Found (((conj1 ((or ((x0 X)->False)) (cQ X))) (((or_comm_i (cP X)) (x0 X)) (x X))) (((or_comm_i (cQ X)) ((x0 X)->False)) (classic (cQ X)))) as proof of ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X))) % 4.62/4.85 Found ((((conj ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X))) (((or_comm_i (cP X)) (x0 X)) (x X))) (((or_comm_i (cQ X)) ((x0 X)->False)) (classic (cQ X)))) as proof of ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X))) % 4.62/4.85 Found (fun (X:fofType)=> ((((conj ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X))) (((or_comm_i (cP X)) (x0 X)) (x X))) (((or_comm_i (cQ X)) ((x0 X)->False)) (classic (cQ X))))) as proof of ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X))) % 4.62/4.85 Found (fun (X:fofType)=> ((((conj ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X))) (((or_comm_i (cP X)) (x0 X)) (x X))) (((or_comm_i (cQ X)) ((x0 X)->False)) (classic (cQ X))))) as proof of (forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))) % 4.62/4.85 Found (ex_intro000 (fun (X:fofType)=> ((((conj ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X))) (((or_comm_i (cP X)) (x0 X)) (x X))) (((or_comm_i (cQ X)) ((x0 X)->False)) (classic (cQ X)))))) as proof of ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) % 4.62/4.85 Found ((ex_intro00 cQ) (fun (X:fofType)=> ((((conj ((or (cQ X)) (cP X))) ((or ((cQ X)->False)) (cQ X))) (((or_comm_i (cP X)) (cQ X)) (x X))) (((or_comm_i (cQ X)) ((cQ X)->False)) (classic (cQ X)))))) as proof of ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) % 6.23/6.46 Found (((ex_intro0 (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) cQ) (fun (X:fofType)=> ((((conj ((or (cQ X)) (cP X))) ((or ((cQ X)->False)) (cQ X))) (((or_comm_i (cP X)) (cQ X)) (x X))) (((or_comm_i (cQ X)) ((cQ X)->False)) (classic (cQ X)))))) as proof of ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) % 6.23/6.46 Found ((((ex_intro (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) cQ) (fun (X:fofType)=> ((((conj ((or (cQ X)) (cP X))) ((or ((cQ X)->False)) (cQ X))) (((or_comm_i (cP X)) (cQ X)) (x X))) (((or_comm_i (cQ X)) ((cQ X)->False)) (classic (cQ X)))))) as proof of ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) % 6.23/6.46 Found (fun (x:(forall (Y:fofType), ((or (cP Y)) (cQ Y))))=> ((((ex_intro (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) cQ) (fun (X:fofType)=> ((((conj ((or (cQ X)) (cP X))) ((or ((cQ X)->False)) (cQ X))) (((or_comm_i (cP X)) (cQ X)) (x X))) (((or_comm_i (cQ X)) ((cQ X)->False)) (classic (cQ X))))))) as proof of ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) % 6.23/6.46 Found (fun (x:(forall (Y:fofType), ((or (cP Y)) (cQ Y))))=> ((((ex_intro (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) cQ) (fun (X:fofType)=> ((((conj ((or (cQ X)) (cP X))) ((or ((cQ X)->False)) (cQ X))) (((or_comm_i (cP X)) (cQ X)) (x X))) (((or_comm_i (cQ X)) ((cQ X)->False)) (classic (cQ X))))))) as proof of ((forall (Y:fofType), ((or (cP Y)) (cQ Y)))->((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) % 6.23/6.46 Found or_intror00:=(or_intror0 (cQ X)):((cQ X)->((or (cP Y)) (cQ X))) % 6.23/6.46 Found (or_intror0 (cQ X)) as proof of ((cQ X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_intror (cP Y)) (cQ X)) as proof of ((cQ X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_intror (cP Y)) (cQ X)) as proof of ((cQ X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_intror (cP Y)) (cQ X)) as proof of ((cQ X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found or_introl00:=(or_introl0 (cQ Y)):((cP X)->((or (cP X)) (cQ Y))) % 6.23/6.46 Found (or_introl0 (cQ Y)) as proof of ((cP X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_introl (cP X)) (cQ Y)) as proof of ((cP X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_introl (cP X)) (cQ Y)) as proof of ((cP X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_introl (cP X)) (cQ Y)) as proof of ((cP X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found or_intror00:=(or_intror0 (cQ X)):((cQ X)->((or (cP Y)) (cQ X))) % 6.23/6.46 Found (or_intror0 (cQ X)) as proof of ((cQ X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_intror (cP Y)) (cQ X)) as proof of ((cQ X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_intror (cP Y)) (cQ X)) as proof of ((cQ X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found or_introl00:=(or_introl0 (cQ Y)):((cP X)->((or (cP X)) (cQ Y))) % 6.23/6.46 Found (or_introl0 (cQ Y)) as proof of ((cP X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_introl (cP X)) (cQ Y)) as proof of ((cP X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_introl (cP X)) (cQ Y)) as proof of ((cP X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found or_intror00:=(or_intror0 (cQ X)):((cQ X)->((or (cP Y)) (cQ X))) % 6.23/6.46 Found (or_intror0 (cQ X)) as proof of ((cQ X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_intror (cP Y)) (cQ X)) as proof of ((cQ X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_intror (cP Y)) (cQ X)) as proof of ((cQ X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_intror (cP Y)) (cQ X)) as proof of ((cQ X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found or_introl00:=(or_introl0 (cQ Y)):((cP X)->((or (cP X)) (cQ Y))) % 6.23/6.46 Found (or_introl0 (cQ Y)) as proof of ((cP X)->((or (cP Y)) (cQ Y))) % 6.23/6.46 Found ((or_introl (cP X)) (cQ Y)) as proof of ((cP X)->((or (cP Y)) (cQ Y))) % 9.82/10.00 Found ((or_introl (cP X)) (cQ Y)) as proof of ((cP X)->((or (cP Y)) (cQ Y))) % 9.82/10.00 Found ((or_introl (cP X)) (cQ Y)) as proof of ((cP X)->((or (cP Y)) (cQ Y))) % 9.82/10.00 Found x4:(cQ X) % 9.82/10.00 Instantiate: X:=Y:fofType % 9.82/10.00 Found (fun (x4:(cQ X))=> x4) as proof of (cQ Y) % 9.82/10.00 Found (fun (x4:(cQ X))=> x4) as proof of ((cQ X)->(cQ Y)) % 9.82/10.00 Found or_introl00:=(or_introl0 (cP Y)):((cQ X)->((or (cQ X)) (cP Y))) % 9.82/10.00 Found (or_introl0 (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found x4:(cQ X) % 9.82/10.00 Instantiate: X:=Y:fofType % 9.82/10.00 Found (fun (x4:(cQ X))=> x4) as proof of (cQ Y) % 9.82/10.00 Found (fun (x4:(cQ X))=> x4) as proof of ((cQ X)->(cQ Y)) % 9.82/10.00 Found or_introl00:=(or_introl0 (cP Y)):((cQ X)->((or (cQ X)) (cP Y))) % 9.82/10.00 Found (or_introl0 (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found x4:(cP X) % 9.82/10.00 Instantiate: X:=Y:fofType % 9.82/10.00 Found (fun (x4:(cP X))=> x4) as proof of (cP Y) % 9.82/10.00 Found (fun (x4:(cP X))=> x4) as proof of ((cP X)->(cP Y)) % 9.82/10.00 Found or_intror00:=(or_intror0 (cP X)):((cP X)->((or (cQ Y)) (cP X))) % 9.82/10.00 Found (or_intror0 (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found x4:(cP X) % 9.82/10.00 Instantiate: X:=Y:fofType % 9.82/10.00 Found (fun (x4:(cP X))=> x4) as proof of (cP Y) % 9.82/10.00 Found (fun (x4:(cP X))=> x4) as proof of ((cP X)->(cP Y)) % 9.82/10.00 Found or_intror00:=(or_intror0 (cP X)):((cP X)->((or (cQ Y)) (cP X))) % 9.82/10.00 Found (or_intror0 (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found x4:(cQ X) % 9.82/10.00 Instantiate: X:=Y:fofType % 9.82/10.00 Found (fun (x4:(cQ X))=> x4) as proof of (cQ Y) % 9.82/10.00 Found (fun (x4:(cQ X))=> x4) as proof of ((cQ X)->(cQ Y)) % 9.82/10.00 Found or_introl00:=(or_introl0 (cP Y)):((cQ X)->((or (cQ X)) (cP Y))) % 9.82/10.00 Found (or_introl0 (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found x4:(cP X) % 9.82/10.00 Instantiate: X:=Y:fofType % 9.82/10.00 Found (fun (x4:(cP X))=> x4) as proof of (cP Y) % 9.82/10.00 Found (fun (x4:(cP X))=> x4) as proof of ((cP X)->(cP Y)) % 9.82/10.00 Found or_intror00:=(or_intror0 (cP X)):((cP X)->((or (cQ Y)) (cP X))) % 9.82/10.00 Found (or_intror0 (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found or_introl00:=(or_introl0 (cP Y)):((cQ X)->((or (cQ X)) (cP Y))) % 9.82/10.00 Found (or_introl0 (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found or_intror00:=(or_intror0 (cP X)):((cP X)->((or (cQ Y)) (cP X))) % 9.82/10.00 Found (or_intror0 (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found or_introl00:=(or_introl0 (cP Y)):((cQ X)->((or (cQ X)) (cP Y))) % 9.82/10.00 Found (or_introl0 (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 9.82/10.00 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found or_intror00:=(or_intror0 (cP X)):((cP X)->((or (cQ Y)) (cP X))) % 11.56/11.80 Found (or_intror0 (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found or_introl00:=(or_introl0 (cP Y)):((cQ X)->((or (cQ X)) (cP Y))) % 11.56/11.80 Found (or_introl0 (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found or_intror00:=(or_intror0 (cP X)):((cP X)->((or (cQ Y)) (cP X))) % 11.56/11.80 Found (or_intror0 (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found or_introl00:=(or_introl0 (cP Y)):((cQ X)->((or (cQ X)) (cP Y))) % 11.56/11.80 Found (or_introl0 (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found or_intror00:=(or_intror0 (cP X)):((cP X)->((or (cQ Y)) (cP X))) % 11.56/11.80 Found (or_intror0 (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found or_introl00:=(or_introl0 (cP Y)):((cQ X)->((or (cQ X)) (cP Y))) % 11.56/11.80 Found (or_introl0 (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found x5:(cQ X) % 11.56/11.80 Instantiate: X:=Y:fofType % 11.56/11.80 Found (fun (x5:(cQ X))=> x5) as proof of (cQ Y) % 11.56/11.80 Found (fun (x5:(cQ X))=> x5) as proof of ((cQ X)->(cQ Y)) % 11.56/11.80 Found x4:(cQ X) % 11.56/11.80 Instantiate: X:=Y:fofType % 11.56/11.80 Found (fun (x4:(cQ X))=> x4) as proof of (cQ Y) % 11.56/11.80 Found (fun (x4:(cQ X))=> x4) as proof of ((cQ X)->(cQ Y)) % 11.56/11.80 Found or_intror00:=(or_intror0 (cP X)):((cP X)->((or (cQ Y)) (cP X))) % 11.56/11.80 Found (or_intror0 (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found x5:(cP X) % 11.56/11.80 Instantiate: X:=Y:fofType % 11.56/11.80 Found (fun (x5:(cP X))=> x5) as proof of (cP Y) % 11.56/11.80 Found (fun (x5:(cP X))=> x5) as proof of ((cP X)->(cP Y)) % 11.56/11.80 Found or_introl00:=(or_introl0 (cP Y)):((cQ X)->((or (cQ X)) (cP Y))) % 11.56/11.80 Found (or_introl0 (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_introl (cQ X)) (cP Y)) as proof of ((cQ X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found x4:(cQ X) % 11.56/11.80 Instantiate: X:=Y:fofType % 11.56/11.80 Found (fun (x4:(cQ X))=> x4) as proof of (cQ Y) % 11.56/11.80 Found (fun (x4:(cQ X))=> x4) as proof of ((cQ X)->(cQ Y)) % 11.56/11.80 Found or_intror00:=(or_intror0 (cP X)):((cP X)->((or (cQ Y)) (cP X))) % 11.56/11.80 Found (or_intror0 (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found ((or_intror (cQ Y)) (cP X)) as proof of ((cP X)->((or (cQ Y)) (cP Y))) % 11.56/11.80 Found x4:(cQ X) % 11.56/11.80 Instantiate: X:=Y:fofType % 11.56/11.80 Found (fun (x4:(cQ X))=> x4) as proof of (cQ Y) % 11.56/11.80 Found (fun (x4:(cQ X))=> x4) as proof of ((cQ X)->(cQ Y)) % 11.56/11.80 Found x4:(cP X) % 11.56/11.80 Instantiate: X:=Y:fofType % 11.56/11.80 Found (fun (x4:(cP X))=> x4) as proof of (cP Y) % 11.56/11.80 Found (fun (x4:(cP X))=> x4) as proof of ((cP X)->(cP Y)) % 11.56/11.80 Found x4:(cP X) % 11.56/11.80 Instantiate: X:=Y:fofType % 11.56/11.80 Found (fun (x4:(cP X))=> x4) as proof of (cP Y) % 11.56/11.80 Found (fun (x4:(cP X))=> x4) as proof of ((cP X)->(cP Y)) % 11.56/11.80 Found x4:(cP X) % 11.56/11.80 Instantiate: X:=Y:fofType % 11.56/11.80 Found (fun (x4:(cP X))=> x4) as proof of (cP Y) % 11.85/12.09 Found (fun (x4:(cP X))=> x4) as proof of ((cP X)->(cP Y)) % 11.85/12.09 Found x5:(cQ X) % 11.85/12.09 Found (fun (x5:(cQ X))=> x5) as proof of (cQ Y) % 11.85/12.09 Found (fun (x5:(cQ X))=> x5) as proof of ((cQ X)->(cQ Y)) % 11.85/12.09 Found x5:(cP X) % 11.85/12.09 Found (fun (x5:(cP X))=> x5) as proof of (cP Y) % 11.85/12.09 Found (fun (x5:(cP X))=> x5) as proof of ((cP X)->(cP Y)) % 11.85/12.09 Found False_rect00:=(False_rect0 ((or (cP Y)) (cQ Y))):((or (cP Y)) (cQ Y)) % 11.85/12.09 Found (False_rect0 ((or (cP Y)) (cQ Y))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.09 Found ((fun (P:Type)=> ((False_rect P) x50)) ((or (cP Y)) (cQ Y))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.09 Found ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.09 Found (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y)))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.09 Found (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y)))) as proof of (((x0 X)->False)->((or (cP Y)) (cQ Y))) % 11.85/12.09 Found ((or_ind10 (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.09 Found (((or_ind1 ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.09 Found ((((fun (P:Prop) (x5:(((x0 X)->False)->P)) (x6:((cQ X)->P))=> ((((((or_ind ((x0 X)->False)) (cQ X)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.09 Found (fun (x4:(x0 X))=> ((((fun (P:Prop) (x5:(((x0 X)->False)->P)) (x6:((cQ X)->P))=> ((((((or_ind ((x0 X)->False)) (cQ X)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X)))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.09 Found (fun (x4:(x0 X))=> ((((fun (P:Prop) (x5:(((x0 X)->False)->P)) (x6:((cQ X)->P))=> ((((((or_ind ((x0 X)->False)) (cQ X)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X)))) as proof of ((x0 X)->((or (cP Y)) (cQ Y))) % 11.85/12.09 Found ((or_ind00 (fun (x4:(x0 X))=> ((((fun (P:Prop) (x5:(((x0 X)->False)->P)) (x6:((cQ X)->P))=> ((((((or_ind ((x0 X)->False)) (cQ X)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X))))) ((or_introl (cP X)) (cQ Y))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.09 Found (((or_ind0 ((or (cP Y)) (cQ Y))) (fun (x4:(x0 X))=> ((((fun (P:Prop) (x5:(((x0 X)->False)->P)) (x6:((cQ X)->P))=> ((((((or_ind ((x0 X)->False)) (cQ X)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X))))) ((or_introl (cP X)) (cQ Y))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.09 Found ((((fun (P:Prop) (x4:((x0 X)->P)) (x5:((cP X)->P))=> ((((((or_ind (x0 X)) (cP X)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 X))=> ((((fun (P:Prop) (x5:(((x0 X)->False)->P)) (x6:((cQ X)->P))=> ((((((or_ind ((x0 X)->False)) (cQ X)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X))))) ((or_introl (cP X)) (cQ Y))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.09 Found (fun (x3:((or ((x0 X)->False)) (cQ X)))=> ((((fun (P:Prop) (x4:((x0 X)->P)) (x5:((cP X)->P))=> ((((((or_ind (x0 X)) (cP X)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 X))=> ((((fun (P:Prop) (x5:(((x0 X)->False)->P)) (x6:((cQ X)->P))=> ((((((or_ind ((x0 X)->False)) (cQ X)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X))))) ((or_introl (cP X)) (cQ Y)))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.09 Found (fun (x2:((or (x0 X)) (cP X))) (x3:((or ((x0 X)->False)) (cQ X)))=> ((((fun (P:Prop) (x4:((x0 X)->P)) (x5:((cP X)->P))=> ((((((or_ind (x0 X)) (cP X)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 X))=> ((((fun (P:Prop) (x5:(((x0 X)->False)->P)) (x6:((cQ X)->P))=> ((((((or_ind ((x0 X)->False)) (cQ X)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X))))) ((or_introl (cP X)) (cQ Y)))) as proof of (((or ((x0 X)->False)) (cQ X))->((or (cP Y)) (cQ Y))) % 11.85/12.10 Found (fun (x2:((or (x0 X)) (cP X))) (x3:((or ((x0 X)->False)) (cQ X)))=> ((((fun (P:Prop) (x4:((x0 X)->P)) (x5:((cP X)->P))=> ((((((or_ind (x0 X)) (cP X)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 X))=> ((((fun (P:Prop) (x5:(((x0 X)->False)->P)) (x6:((cQ X)->P))=> ((((((or_ind ((x0 X)->False)) (cQ X)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X))))) ((or_introl (cP X)) (cQ Y)))) as proof of (((or (x0 X)) (cP X))->(((or ((x0 X)->False)) (cQ X))->((or (cP Y)) (cQ Y)))) % 11.85/12.10 Found (and_rect00 (fun (x2:((or (x0 X)) (cP X))) (x3:((or ((x0 X)->False)) (cQ X)))=> ((((fun (P:Prop) (x4:((x0 X)->P)) (x5:((cP X)->P))=> ((((((or_ind (x0 X)) (cP X)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 X))=> ((((fun (P:Prop) (x5:(((x0 X)->False)->P)) (x6:((cQ X)->P))=> ((((((or_ind ((x0 X)->False)) (cQ X)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X))))) ((or_introl (cP X)) (cQ Y))))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.10 Found ((and_rect0 ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 X)) (cP X))) (x3:((or ((x0 X)->False)) (cQ X)))=> ((((fun (P:Prop) (x4:((x0 X)->P)) (x5:((cP X)->P))=> ((((((or_ind (x0 X)) (cP X)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 X))=> ((((fun (P:Prop) (x5:(((x0 X)->False)->P)) (x6:((cQ X)->P))=> ((((((or_ind ((x0 X)->False)) (cQ X)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X))))) ((or_introl (cP X)) (cQ Y))))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.10 Found (((fun (P:Type) (x2:(((or (x0 X)) (cP X))->(((or ((x0 X)->False)) (cQ X))->P)))=> (((((and_rect ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X))) P) x2) x10)) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 X)) (cP X))) (x3:((or ((x0 X)->False)) (cQ X)))=> ((((fun (P:Prop) (x4:((x0 X)->P)) (x5:((cP X)->P))=> ((((((or_ind (x0 X)) (cP X)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 X))=> ((((fun (P:Prop) (x5:(((x0 X)->False)->P)) (x6:((cQ X)->P))=> ((((((or_ind ((x0 X)->False)) (cQ X)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 X)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ X))))) ((or_introl (cP X)) (cQ Y))))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.10 Found (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y))))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.10 Found (fun (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y)))))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.11 Found (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y)))))) as proof of ((forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X))))->((or (cP Y)) (cQ Y))) % 11.85/12.11 Found (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y)))))) as proof of (forall (x:(fofType->Prop)), ((forall (X:fofType), ((and ((or (x X)) (cP X))) ((or ((x X)->False)) (cQ X))))->((or (cP Y)) (cQ Y)))) % 11.85/12.11 Found (ex_ind00 (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y))))))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.11 Found ((ex_ind0 ((or (cP Y)) (cQ Y))) (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y))))))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.11 Found (((fun (P:Prop) (x0:(forall (x:(fofType->Prop)), ((forall (X:fofType), ((and ((or (x X)) (cP X))) ((or ((x X)->False)) (cQ X))))->P)))=> (((((ex_ind (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) P) x0) x)) ((or (cP Y)) (cQ Y))) (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y))))))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.11 Found (fun (Y:fofType)=> (((fun (P:Prop) (x0:(forall (x:(fofType->Prop)), ((forall (X:fofType), ((and ((or (x X)) (cP X))) ((or ((x X)->False)) (cQ X))))->P)))=> (((((ex_ind (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) P) x0) x)) ((or (cP Y)) (cQ Y))) (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y)))))))) as proof of ((or (cP Y)) (cQ Y)) % 11.85/12.11 Found (fun (x:((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (Y:fofType)=> (((fun (P:Prop) (x0:(forall (x:(fofType->Prop)), ((forall (X:fofType), ((and ((or (x X)) (cP X))) ((or ((x X)->False)) (cQ X))))->P)))=> (((((ex_ind (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) P) x0) x)) ((or (cP Y)) (cQ Y))) (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y)))))))) as proof of (forall (Y:fofType), ((or (cP Y)) (cQ Y))) % 11.85/12.11 Found (fun (x:((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (Y:fofType)=> (((fun (P:Prop) (x0:(forall (x:(fofType->Prop)), ((forall (X:fofType), ((and ((or (x X)) (cP X))) ((or ((x X)->False)) (cQ X))))->P)))=> (((((ex_ind (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) P) x0) x)) ((or (cP Y)) (cQ Y))) (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y)))))))) as proof of (((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))->(forall (Y:fofType), ((or (cP Y)) (cQ Y)))) % 11.94/12.13 Found ((conj00 (fun (x:((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (Y:fofType)=> (((fun (P:Prop) (x0:(forall (x:(fofType->Prop)), ((forall (X:fofType), ((and ((or (x X)) (cP X))) ((or ((x X)->False)) (cQ X))))->P)))=> (((((ex_ind (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) P) x0) x)) ((or (cP Y)) (cQ Y))) (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y))))))))) (fun (x:(forall (Y:fofType), ((or (cP Y)) (cQ Y))))=> ((((ex_intro (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) cQ) (fun (X:fofType)=> ((((conj ((or (cQ X)) (cP X))) ((or ((cQ X)->False)) (cQ X))) (((or_comm_i (cP X)) (cQ X)) (x X))) (((or_comm_i (cQ X)) ((cQ X)->False)) (classic (cQ X)))))))) as proof of ((iff ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (forall (Y:fofType), ((or (cP Y)) (cQ Y)))) % 11.94/12.13 Found (((conj0 ((forall (Y:fofType), ((or (cP Y)) (cQ Y)))->((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))))) (fun (x:((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (Y:fofType)=> (((fun (P:Prop) (x0:(forall (x:(fofType->Prop)), ((forall (X:fofType), ((and ((or (x X)) (cP X))) ((or ((x X)->False)) (cQ X))))->P)))=> (((((ex_ind (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) P) x0) x)) ((or (cP Y)) (cQ Y))) (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y))))))))) (fun (x:(forall (Y:fofType), ((or (cP Y)) (cQ Y))))=> ((((ex_intro (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) cQ) (fun (X:fofType)=> ((((conj ((or (cQ X)) (cP X))) ((or ((cQ X)->False)) (cQ X))) (((or_comm_i (cP X)) (cQ X)) (x X))) (((or_comm_i (cQ X)) ((cQ X)->False)) (classic (cQ X)))))))) as proof of ((iff ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (forall (Y:fofType), ((or (cP Y)) (cQ Y)))) % 11.94/12.14 Found ((((conj (((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))->(forall (Y:fofType), ((or (cP Y)) (cQ Y))))) ((forall (Y:fofType), ((or (cP Y)) (cQ Y)))->((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))))) (fun (x:((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (Y:fofType)=> (((fun (P:Prop) (x0:(forall (x:(fofType->Prop)), ((forall (X:fofType), ((and ((or (x X)) (cP X))) ((or ((x X)->False)) (cQ X))))->P)))=> (((((ex_ind (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) P) x0) x)) ((or (cP Y)) (cQ Y))) (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y))))))))) (fun (x:(forall (Y:fofType), ((or (cP Y)) (cQ Y))))=> ((((ex_intro (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) cQ) (fun (X:fofType)=> ((((conj ((or (cQ X)) (cP X))) ((or ((cQ X)->False)) (cQ X))) (((or_comm_i (cP X)) (cQ X)) (x X))) (((or_comm_i (cQ X)) ((cQ X)->False)) (classic (cQ X)))))))) as proof of ((iff ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (forall (Y:fofType), ((or (cP Y)) (cQ Y)))) % 11.94/12.14 Found ((((conj (((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))->(forall (Y:fofType), ((or (cP Y)) (cQ Y))))) ((forall (Y:fofType), ((or (cP Y)) (cQ Y)))->((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))))) (fun (x:((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (Y:fofType)=> (((fun (P:Prop) (x0:(forall (x:(fofType->Prop)), ((forall (X:fofType), ((and ((or (x X)) (cP X))) ((or ((x X)->False)) (cQ X))))->P)))=> (((((ex_ind (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) P) x0) x)) ((or (cP Y)) (cQ Y))) (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y))))))))) (fun (x:(forall (Y:fofType), ((or (cP Y)) (cQ Y))))=> ((((ex_intro (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) cQ) (fun (X:fofType)=> ((((conj ((or (cQ X)) (cP X))) ((or ((cQ X)->False)) (cQ X))) (((or_comm_i (cP X)) (cQ X)) (x X))) (((or_comm_i (cQ X)) ((cQ X)->False)) (classic (cQ X)))))))) as proof of ((iff ((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (forall (Y:fofType), ((or (cP Y)) (cQ Y)))) % 11.94/12.14 Got proof ((((conj (((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))->(forall (Y:fofType), ((or (cP Y)) (cQ Y))))) ((forall (Y:fofType), ((or (cP Y)) (cQ Y)))->((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))))) (fun (x:((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (Y:fofType)=> (((fun (P:Prop) (x0:(forall (x:(fofType->Prop)), ((forall (X:fofType), ((and ((or (x X)) (cP X))) ((or ((x X)->False)) (cQ X))))->P)))=> (((((ex_ind (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) P) x0) x)) ((or (cP Y)) (cQ Y))) (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y))))))))) (fun (x:(forall (Y:fofType), ((or (cP Y)) (cQ Y))))=> ((((ex_intro (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) cQ) (fun (X:fofType)=> ((((conj ((or (cQ X)) (cP X))) ((or ((cQ X)->False)) (cQ X))) (((or_comm_i (cP X)) (cQ X)) (x X))) (((or_comm_i (cQ X)) ((cQ X)->False)) (classic (cQ X)))))))) % 11.94/12.14 Time elapsed = 11.509002s % 11.94/12.14 node=2818 cost=1270.000000 depth=32 % 11.94/12.14 :::::::::::::::::::::: % 11.94/12.14 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.94/12.14 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.94/12.14 ((((conj (((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))->(forall (Y:fofType), ((or (cP Y)) (cQ Y))))) ((forall (Y:fofType), ((or (cP Y)) (cQ Y)))->((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))))) (fun (x:((ex (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X))))))) (Y:fofType)=> (((fun (P:Prop) (x0:(forall (x:(fofType->Prop)), ((forall (X:fofType), ((and ((or (x X)) (cP X))) ((or ((x X)->False)) (cQ X))))->P)))=> (((((ex_ind (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) P) x0) x)) ((or (cP Y)) (cQ Y))) (fun (x0:(fofType->Prop)) (x1:(forall (X:fofType), ((and ((or (x0 X)) (cP X))) ((or ((x0 X)->False)) (cQ X)))))=> (((fun (P:Type) (x2:(((or (x0 Y)) (cP Y))->(((or ((x0 Y)->False)) (cQ Y))->P)))=> (((((and_rect ((or (x0 Y)) (cP Y))) ((or ((x0 Y)->False)) (cQ Y))) P) x2) (x1 Y))) ((or (cP Y)) (cQ Y))) (fun (x2:((or (x0 Y)) (cP Y))) (x3:((or ((x0 Y)->False)) (cQ Y)))=> ((((fun (P:Prop) (x4:((x0 Y)->P)) (x5:((cP Y)->P))=> ((((((or_ind (x0 Y)) (cP Y)) P) x4) x5) x2)) ((or (cP Y)) (cQ Y))) (fun (x4:(x0 Y))=> ((((fun (P:Prop) (x5:(((x0 Y)->False)->P)) (x6:((cQ Y)->P))=> ((((((or_ind ((x0 Y)->False)) (cQ Y)) P) x5) x6) x3)) ((or (cP Y)) (cQ Y))) (fun (x5:((x0 Y)->False))=> ((fun (P:Type)=> ((False_rect P) (x5 x4))) ((or (cP Y)) (cQ Y))))) ((or_intror (cP Y)) (cQ Y))))) ((or_introl (cP Y)) (cQ Y))))))))) (fun (x:(forall (Y:fofType), ((or (cP Y)) (cQ Y))))=> ((((ex_intro (fofType->Prop)) (fun (S:(fofType->Prop))=> (forall (X:fofType), ((and ((or (S X)) (cP X))) ((or ((S X)->False)) (cQ X)))))) cQ) (fun (X:fofType)=> ((((conj ((or (cQ X)) (cP X))) ((or ((cQ X)->False)) (cQ X))) (((or_comm_i (cP X)) (cQ X)) (x X))) (((or_comm_i (cQ X)) ((cQ X)->False)) (classic (cQ X)))))))) % 12.01/12.26 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------