%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SYO378^5 : TPTP v7.5.0. Bugfixed v5.2.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n016.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:17 EDT 2022 % Result : Theorem 5.46s 5.68s % Output : Proof 5.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SYO378^5 : TPTP v7.5.0. Bugfixed v5.2.0. % 0.06/0.12 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.33 % Computer : n016.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 : Sat Mar 12 09:29:00 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 % 0.76/0.93 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 0.76/0.93 FOF formula (<kernel.Constant object at 0x275fd40>, <kernel.Constant object at 0x275f2d8>) of role type named c_type % 0.76/0.93 Using role type % 0.76/0.93 Declaring c:fofType % 0.76/0.93 FOF formula (<kernel.Constant object at 0x2b59c933aa70>, <kernel.DependentProduct object at 0x275f098>) of role type named cQDP0_type % 0.76/0.93 Using role type % 0.76/0.93 Declaring cQDP0:(fofType->Prop) % 0.76/0.93 FOF formula (<kernel.Constant object at 0x275fd40>, <kernel.DependentProduct object at 0x275f440>) of role type named cQDP1_type % 0.76/0.93 Using role type % 0.76/0.93 Declaring cQDP1:((fofType->Prop)->Prop) % 0.76/0.93 FOF formula (<kernel.Constant object at 0x275f098>, <kernel.DependentProduct object at 0x2b59c931cef0>) of role type named cQDP2_type % 0.76/0.93 Using role type % 0.76/0.93 Declaring cQDP2:(((fofType->Prop)->Prop)->Prop) % 0.76/0.93 FOF formula (((eq (fofType->Prop)) cQDP0) (fun (Xz:fofType)=> (((eq fofType) Xz) c))) of role definition named cQDP0_def % 0.76/0.93 A new definition: (((eq (fofType->Prop)) cQDP0) (fun (Xz:fofType)=> (((eq fofType) Xz) c))) % 0.76/0.93 Defined: cQDP0:=(fun (Xz:fofType)=> (((eq fofType) Xz) c)) % 0.76/0.93 FOF formula (((eq ((fofType->Prop)->Prop)) cQDP1) (fun (Xz:(fofType->Prop))=> ((and (((eq (fofType->Prop)) Xz) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (Xz Xt)))))) of role definition named cQDP1_def % 0.76/0.93 A new definition: (((eq ((fofType->Prop)->Prop)) cQDP1) (fun (Xz:(fofType->Prop))=> ((and (((eq (fofType->Prop)) Xz) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (Xz Xt)))))) % 0.76/0.93 Defined: cQDP1:=(fun (Xz:(fofType->Prop))=> ((and (((eq (fofType->Prop)) Xz) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (Xz Xt))))) % 0.76/0.93 FOF formula (((eq (((fofType->Prop)->Prop)->Prop)) cQDP2) (fun (Xz:((fofType->Prop)->Prop))=> ((and (((eq ((fofType->Prop)->Prop)) Xz) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (Xz Xt)))))) of role definition named cQDP2_def % 0.76/0.93 A new definition: (((eq (((fofType->Prop)->Prop)->Prop)) cQDP2) (fun (Xz:((fofType->Prop)->Prop))=> ((and (((eq ((fofType->Prop)->Prop)) Xz) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (Xz Xt)))))) % 0.76/0.93 Defined: cQDP2:=(fun (Xz:((fofType->Prop)->Prop))=> ((and (((eq ((fofType->Prop)->Prop)) Xz) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (Xz Xt))))) % 0.76/0.93 FOF formula ((ex ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))) of role conjecture named cQDTHM2 % 0.76/0.93 Conjecture to prove = ((ex ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))):Prop % 0.76/0.93 We need to prove ['((ex ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs)))'] % 0.76/0.93 Parameter fofType:Type. % 0.76/0.93 Parameter c:fofType. % 0.76/0.93 Definition cQDP0:=(fun (Xz:fofType)=> (((eq fofType) Xz) c)):(fofType->Prop). % 0.76/0.93 Definition cQDP1:=(fun (Xz:(fofType->Prop))=> ((and (((eq (fofType->Prop)) Xz) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (Xz Xt))))):((fofType->Prop)->Prop). % 0.76/0.93 Definition cQDP2:=(fun (Xz:((fofType->Prop)->Prop))=> ((and (((eq ((fofType->Prop)->Prop)) Xz) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (Xz Xt))))):(((fofType->Prop)->Prop)->Prop). % 0.76/0.93 Trying to prove ((ex ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))) % 0.76/0.93 Found eta_expansion000:=(eta_expansion00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 0.76/0.93 Found (eta_expansion00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 0.76/0.93 Found ((eta_expansion0 Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 0.76/0.93 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 0.76/0.93 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 0.76/0.93 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 0.76/0.93 Found eq_ref00:=(eq_ref0 x):(((eq ((fofType->Prop)->Prop)) x) x) % 0.76/0.93 Found (eq_ref0 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 0.76/0.93 Found ((eq_ref ((fofType->Prop)->Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 0.76/0.93 Found ((eq_ref ((fofType->Prop)->Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 0.76/0.93 Found ((eq_ref ((fofType->Prop)->Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 1.66/1.87 Found eq_ref00:=(eq_ref0 ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))):(((eq Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) % 1.66/1.87 Found (eq_ref0 ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) as proof of (((eq Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) b) % 1.66/1.87 Found ((eq_ref Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) as proof of (((eq Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) b) % 1.66/1.87 Found ((eq_ref Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) as proof of (((eq Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) b) % 1.66/1.87 Found ((eq_ref Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) as proof of (((eq Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) b) % 1.66/1.87 Found eq_ref00:=(eq_ref0 ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))):(((eq Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) % 1.66/1.87 Found (eq_ref0 ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) as proof of (((eq Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) b) % 1.66/1.87 Found ((eq_ref Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) as proof of (((eq Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) b) % 1.66/1.87 Found ((eq_ref Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) as proof of (((eq Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) b) % 1.66/1.87 Found ((eq_ref Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) as proof of (((eq Prop) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) b) % 1.66/1.87 Found eq_ref00:=(eq_ref0 a):(((eq ((fofType->Prop)->Prop)) a) a) % 1.66/1.87 Found (eq_ref0 a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found ((eq_ref ((fofType->Prop)->Prop)) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found ((eq_ref ((fofType->Prop)->Prop)) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found ((eq_ref ((fofType->Prop)->Prop)) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found eta_expansion000:=(eta_expansion00 a):(((eq ((fofType->Prop)->Prop)) a) (fun (x:(fofType->Prop))=> (a x))) % 1.66/1.87 Found (eta_expansion00 a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found ((eta_expansion0 Prop) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found (((eta_expansion (fofType->Prop)) Prop) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found (((eta_expansion (fofType->Prop)) Prop) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found (((eta_expansion (fofType->Prop)) Prop) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found eq_ref00:=(eq_ref0 a):(((eq ((fofType->Prop)->Prop)) a) a) % 1.66/1.87 Found (eq_ref0 a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found ((eq_ref ((fofType->Prop)->Prop)) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found ((eq_ref ((fofType->Prop)->Prop)) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found ((eq_ref ((fofType->Prop)->Prop)) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found eta_expansion000:=(eta_expansion00 a):(((eq ((fofType->Prop)->Prop)) a) (fun (x:(fofType->Prop))=> (a x))) % 1.66/1.87 Found (eta_expansion00 a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found ((eta_expansion0 Prop) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 1.66/1.87 Found (((eta_expansion (fofType->Prop)) Prop) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 3.52/3.70 Found (((eta_expansion (fofType->Prop)) Prop) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 3.52/3.70 Found (((eta_expansion (fofType->Prop)) Prop) a) as proof of (((eq ((fofType->Prop)->Prop)) a) (fun (Xt:(fofType->Prop))=> (x Xt))) % 3.52/3.70 Found eta_expansion000:=(eta_expansion00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 3.52/3.70 Found (eta_expansion00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found ((eta_expansion0 Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found eta_expansion000:=(eta_expansion00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 3.52/3.70 Found (eta_expansion00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found ((eta_expansion0 Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found eta_expansion000:=(eta_expansion00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 3.52/3.70 Found (eta_expansion00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found ((eta_expansion0 Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found eta_expansion_dep000:=(eta_expansion_dep00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 3.52/3.70 Found (eta_expansion_dep00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found ((eta_expansion_dep0 (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found eq_ref00:=(eq_ref0 x0):(((eq (fofType->Prop)) x0) x0) % 3.52/3.70 Found (eq_ref0 x0) as proof of (((eq (fofType->Prop)) x0) cQDP0) % 3.52/3.70 Found ((eq_ref (fofType->Prop)) x0) as proof of (((eq (fofType->Prop)) x0) cQDP0) % 3.52/3.70 Found ((eq_ref (fofType->Prop)) x0) as proof of (((eq (fofType->Prop)) x0) cQDP0) % 3.52/3.70 Found ((eq_ref (fofType->Prop)) x0) as proof of (((eq (fofType->Prop)) x0) cQDP0) % 3.52/3.70 Found eq_ref00:=(eq_ref0 x0):(((eq (fofType->Prop)) x0) x0) % 3.52/3.70 Found (eq_ref0 x0) as proof of (((eq (fofType->Prop)) x0) cQDP0) % 3.52/3.70 Found ((eq_ref (fofType->Prop)) x0) as proof of (((eq (fofType->Prop)) x0) cQDP0) % 3.52/3.70 Found ((eq_ref (fofType->Prop)) x0) as proof of (((eq (fofType->Prop)) x0) cQDP0) % 3.52/3.70 Found ((eq_ref (fofType->Prop)) x0) as proof of (((eq (fofType->Prop)) x0) cQDP0) % 3.52/3.70 Found iff_sym:=(fun (A:Prop) (B:Prop) (H:((iff A) B))=> ((((conj (B->A)) (A->B)) (((proj2 (A->B)) (B->A)) H)) (((proj1 (A->B)) (B->A)) H))):(forall (A:Prop) (B:Prop), (((iff A) B)->((iff B) A))) % 3.52/3.70 Instantiate: b:=(forall (A:Prop) (B:Prop), (((iff A) B)->((iff B) A))):Prop % 3.52/3.70 Found iff_sym as proof of b % 3.52/3.70 Found eta_expansion000:=(eta_expansion00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 3.52/3.70 Found (eta_expansion00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found ((eta_expansion0 Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 3.52/3.70 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found ((conj00 (((eta_expansion (fofType->Prop)) Prop) x)) iff_sym) as proof of ((and (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) % 4.05/4.23 Found (((conj0 b) (((eta_expansion (fofType->Prop)) Prop) x)) iff_sym) as proof of ((and (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) % 4.05/4.23 Found ((((conj (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) (((eta_expansion (fofType->Prop)) Prop) x)) iff_sym) as proof of ((and (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) % 4.05/4.23 Found ((((conj (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) (((eta_expansion (fofType->Prop)) Prop) x)) iff_sym) as proof of ((and (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) % 4.05/4.23 Found ((((conj (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) (((eta_expansion (fofType->Prop)) Prop) x)) iff_sym) as proof of (P b) % 4.05/4.23 Found eta_expansion000:=(eta_expansion00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 4.05/4.23 Found (eta_expansion00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found ((eta_expansion0 Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found eta_expansion_dep000:=(eta_expansion_dep00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 4.05/4.23 Found (eta_expansion_dep00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found ((eta_expansion_dep0 (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found iff_sym:=(fun (A:Prop) (B:Prop) (H:((iff A) B))=> ((((conj (B->A)) (A->B)) (((proj2 (A->B)) (B->A)) H)) (((proj1 (A->B)) (B->A)) H))):(forall (A:Prop) (B:Prop), (((iff A) B)->((iff B) A))) % 4.05/4.23 Instantiate: b:=(forall (A:Prop) (B:Prop), (((iff A) B)->((iff B) A))):Prop % 4.05/4.23 Found iff_sym as proof of b % 4.05/4.23 Found eta_expansion000:=(eta_expansion00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 4.05/4.23 Found (eta_expansion00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found ((eta_expansion0 Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.05/4.23 Found ((conj00 (((eta_expansion (fofType->Prop)) Prop) x)) iff_sym) as proof of ((and (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) % 4.05/4.23 Found (((conj0 b) (((eta_expansion (fofType->Prop)) Prop) x)) iff_sym) as proof of ((and (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) % 4.05/4.23 Found ((((conj (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) (((eta_expansion (fofType->Prop)) Prop) x)) iff_sym) as proof of ((and (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) % 4.05/4.23 Found ((((conj (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) (((eta_expansion (fofType->Prop)) Prop) x)) iff_sym) as proof of ((and (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) % 4.05/4.23 Found ((((conj (((eq ((fofType->Prop)->Prop)) x) cQDP1)) b) (((eta_expansion (fofType->Prop)) Prop) x)) iff_sym) as proof of (P b) % 4.05/4.23 Found eta_expansion000:=(eta_expansion00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 4.86/5.09 Found (eta_expansion00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found ((eta_expansion0 Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found eta_expansion000:=(eta_expansion00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 4.86/5.09 Found (eta_expansion00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found ((eta_expansion0 Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found eq_ref00:=(eq_ref0 x):(((eq ((fofType->Prop)->Prop)) x) x) % 4.86/5.09 Found (eq_ref0 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found ((eq_ref ((fofType->Prop)->Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found ((eq_ref ((fofType->Prop)->Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found ((eq_ref ((fofType->Prop)->Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found eta_expansion_dep000:=(eta_expansion_dep00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 4.86/5.09 Found (eta_expansion_dep00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found ((eta_expansion_dep0 (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found eta_expansion000:=(eta_expansion00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 4.86/5.09 Found (eta_expansion00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found ((eta_expansion0 Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found eta_expansion000:=(eta_expansion00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 4.86/5.09 Found (eta_expansion00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found ((eta_expansion0 Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found eta_expansion_dep000:=(eta_expansion_dep00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 4.86/5.09 Found (eta_expansion_dep00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found ((eta_expansion_dep0 (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 4.86/5.09 Found (((eta_expansion_dep (fofType->Prop)) (fun (x1:(fofType->Prop))=> Prop)) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 5.43/5.60 Found eta_expansion000:=(eta_expansion00 x):(((eq ((fofType->Prop)->Prop)) x) (fun (x0:(fofType->Prop))=> (x x0))) % 5.43/5.60 Found (eta_expansion00 x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 5.43/5.60 Found ((eta_expansion0 Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 5.43/5.60 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 5.43/5.60 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 5.43/5.60 Found (((eta_expansion (fofType->Prop)) Prop) x) as proof of (((eq ((fofType->Prop)->Prop)) x) cQDP1) % 5.43/5.60 Found eq_ref00:=(eq_ref0 a):(((eq Prop) a) a) % 5.43/5.60 Found (eq_ref0 a) as proof of (((eq Prop) a) b) % 5.43/5.60 Found ((eq_ref Prop) a) as proof of (((eq Prop) a) b) % 5.43/5.60 Found ((eq_ref Prop) a) as proof of (((eq Prop) a) b) % 5.43/5.60 Found ((eq_ref Prop) a) as proof of (((eq Prop) a) b) % 5.43/5.60 Found eq_ref00:=(eq_ref0 b):(((eq Prop) b) b) % 5.43/5.60 Found (eq_ref0 b) as proof of (((eq Prop) b) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) % 5.43/5.60 Found ((eq_ref Prop) b) as proof of (((eq Prop) b) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) % 5.43/5.60 Found ((eq_ref Prop) b) as proof of (((eq Prop) b) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) % 5.43/5.60 Found ((eq_ref Prop) b) as proof of (((eq Prop) b) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) % 5.43/5.60 Found x2:(P x1) % 5.43/5.60 Instantiate: x1:=c:fofType % 5.43/5.60 Found (fun (x2:(P x1))=> x2) as proof of (P c) % 5.43/5.60 Found (fun (P:(fofType->Prop)) (x2:(P x1))=> x2) as proof of ((P x1)->(P c)) % 5.43/5.60 Found (fun (P:(fofType->Prop)) (x2:(P x1))=> x2) as proof of (x0 x1) % 5.43/5.60 Found (ex_intro200 (fun (P:(fofType->Prop)) (x2:(P x1))=> x2)) as proof of ((ex fofType) (fun (Xt:fofType)=> (x0 Xt))) % 5.43/5.60 Found ((ex_intro20 c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)) as proof of ((ex fofType) (fun (Xt:fofType)=> (x0 Xt))) % 5.43/5.60 Found (((ex_intro2 (fun (Xt:fofType)=> (x0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)) as proof of ((ex fofType) (fun (Xt:fofType)=> (x0 Xt))) % 5.43/5.60 Found ((((ex_intro fofType) (fun (Xt:fofType)=> (x0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)) as proof of ((ex fofType) (fun (Xt:fofType)=> (x0 Xt))) % 5.43/5.60 Found ((((ex_intro fofType) (fun (Xt:fofType)=> (x0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)) as proof of ((ex fofType) (fun (Xt:fofType)=> (x0 Xt))) % 5.43/5.60 Found ((conj10 ((eq_ref (fofType->Prop)) x0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (x0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2))) as proof of ((and (((eq (fofType->Prop)) x0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x0 Xt)))) % 5.43/5.60 Found (((conj1 ((ex fofType) (fun (Xt:fofType)=> (x0 Xt)))) ((eq_ref (fofType->Prop)) x0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (x0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2))) as proof of ((and (((eq (fofType->Prop)) x0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x0 Xt)))) % 5.43/5.60 Found ((((conj (((eq (fofType->Prop)) x0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x0 Xt)))) ((eq_ref (fofType->Prop)) x0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (x0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2))) as proof of ((and (((eq (fofType->Prop)) x0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x0 Xt)))) % 5.43/5.60 Found ((((conj (((eq (fofType->Prop)) x0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x0 Xt)))) ((eq_ref (fofType->Prop)) x0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (x0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2))) as proof of ((and (((eq (fofType->Prop)) x0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x0 Xt)))) % 5.43/5.60 Found ((((conj (((eq (fofType->Prop)) x0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x0 Xt)))) ((eq_ref (fofType->Prop)) x0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (x0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2))) as proof of (x x0) % 5.43/5.60 Found (ex_intro100 ((((conj (((eq (fofType->Prop)) x0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x0 Xt)))) ((eq_ref (fofType->Prop)) x0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (x0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)))) as proof of ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) % 5.43/5.60 Found ((ex_intro10 cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)))) as proof of ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) % 5.43/5.61 Found (((ex_intro1 (fun (Xt:(fofType->Prop))=> (x Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)))) as proof of ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) % 5.43/5.61 Found ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)))) as proof of ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) % 5.43/5.61 Found ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)))) as proof of ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) % 5.43/5.61 Found ((conj00 (((eta_expansion (fofType->Prop)) Prop) x)) ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2))))) as proof of ((and (((eq ((fofType->Prop)->Prop)) x) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) % 5.43/5.61 Found (((conj0 ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) (((eta_expansion (fofType->Prop)) Prop) x)) ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2))))) as proof of ((and (((eq ((fofType->Prop)->Prop)) x) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) % 5.43/5.61 Found ((((conj (((eq ((fofType->Prop)->Prop)) x) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) (((eta_expansion (fofType->Prop)) Prop) x)) ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2))))) as proof of ((and (((eq ((fofType->Prop)->Prop)) x) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) % 5.43/5.61 Found ((((conj (((eq ((fofType->Prop)->Prop)) x) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) (((eta_expansion (fofType->Prop)) Prop) x)) ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2))))) as proof of ((and (((eq ((fofType->Prop)->Prop)) x) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) % 5.43/5.61 Found ((((conj (((eq ((fofType->Prop)->Prop)) x) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) (((eta_expansion (fofType->Prop)) Prop) x)) ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2))))) as proof of (cQDP2 x) % 5.43/5.61 Found (ex_intro000 ((((conj (((eq ((fofType->Prop)->Prop)) x) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt)))) (((eta_expansion (fofType->Prop)) Prop) x)) ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> (x Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)))))) as proof of ((ex ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))) % 5.46/5.62 Found ((ex_intro00 (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt)))))) ((((conj (((eq ((fofType->Prop)->Prop)) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt)))))) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> ((fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))) Xt)))) (((eta_expansion (fofType->Prop)) Prop) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))))) ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> ((fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))) Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)))))) as proof of ((ex ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))) % 5.46/5.62 Found (((ex_intro0 (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt)))))) ((((conj (((eq ((fofType->Prop)->Prop)) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt)))))) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> ((fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))) Xt)))) (((eta_expansion (fofType->Prop)) Prop) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))))) ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> ((fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))) Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)))))) as proof of ((ex ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))) % 5.46/5.62 Found ((((ex_intro ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt)))))) ((((conj (((eq ((fofType->Prop)->Prop)) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt)))))) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> ((fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))) Xt)))) (((eta_expansion (fofType->Prop)) Prop) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))))) ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> ((fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))) Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)))))) as proof of ((ex ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))) % 5.46/5.68 Found ((((ex_intro ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt)))))) ((((conj (((eq ((fofType->Prop)->Prop)) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt)))))) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> ((fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))) Xt)))) (((eta_expansion (fofType->Prop)) Prop) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))))) ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> ((fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))) Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)))))) as proof of ((ex ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))) % 5.46/5.68 Got proof ((((ex_intro ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt)))))) ((((conj (((eq ((fofType->Prop)->Prop)) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt)))))) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> ((fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))) Xt)))) (((eta_expansion (fofType->Prop)) Prop) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))))) ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> ((fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))) Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)))))) % 5.46/5.68 Time elapsed = 5.014801s % 5.46/5.68 node=1314 cost=5476.000000 depth=27 % 5.46/5.68 :::::::::::::::::::::: % 5.46/5.68 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.46/5.68 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.46/5.68 ((((ex_intro ((fofType->Prop)->Prop)) (fun (Xs:((fofType->Prop)->Prop))=> (cQDP2 Xs))) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt)))))) ((((conj (((eq ((fofType->Prop)->Prop)) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt)))))) cQDP1)) ((ex (fofType->Prop)) (fun (Xt:(fofType->Prop))=> ((fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))) Xt)))) (((eta_expansion (fofType->Prop)) Prop) (fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))))) ((((ex_intro (fofType->Prop)) (fun (Xt:(fofType->Prop))=> ((fun (x3:(fofType->Prop))=> ((and (((eq (fofType->Prop)) x3) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (x3 Xt))))) Xt))) cQDP0) ((((conj (((eq (fofType->Prop)) cQDP0) cQDP0)) ((ex fofType) (fun (Xt:fofType)=> (cQDP0 Xt)))) ((eq_ref (fofType->Prop)) cQDP0)) ((((ex_intro fofType) (fun (Xt:fofType)=> (cQDP0 Xt))) c) (fun (P:(fofType->Prop)) (x2:(P c))=> x2)))))) % 5.46/5.68 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------