%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU638^2 : TPTP v6.1.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n089.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Thu Jul 17 13:32:40 EDT 2014 % Result : Theorem 38.21s % Output : Proof 38.21s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU638^2 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n089.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 10:59:21 CDT 2014 % % CPUTime : 38.21 % Python 2.7.5 % Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % FOF formula (<kernel.Constant object at 0x210f200>, <kernel.DependentProduct object at 0x210f290>) of role type named in_type % Using role type % Declaring in:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x20831b8>, <kernel.Single object at 0x210fe18>) of role type named emptyset_type % Using role type % Declaring emptyset:fofType % FOF formula (<kernel.Constant object at 0x210f290>, <kernel.DependentProduct object at 0x210ffc8>) of role type named setadjoin_type % Using role type % Declaring setadjoin:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x210f0e0>, <kernel.DependentProduct object at 0x210ff80>) of role type named dsetconstr_type % Using role type % Declaring dsetconstr:(fofType->((fofType->Prop)->fofType)) % FOF formula (<kernel.Constant object at 0x210f518>, <kernel.Sort object at 0x1b135a8>) of role type named dsetconstrEL_type % Using role type % Declaring dsetconstrEL:Prop % FOF formula (((eq Prop) dsetconstrEL) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->((in Xx) A)))) of role definition named dsetconstrEL % A new definition: (((eq Prop) dsetconstrEL) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->((in Xx) A)))) % Defined: dsetconstrEL:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->((in Xx) A))) % FOF formula (<kernel.Constant object at 0x210f908>, <kernel.Sort object at 0x1b135a8>) of role type named dsetconstrER_type % Using role type % Declaring dsetconstrER:Prop % FOF formula (((eq Prop) dsetconstrER) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->(Xphi Xx)))) of role definition named dsetconstrER % A new definition: (((eq Prop) dsetconstrER) (forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->(Xphi Xx)))) % Defined: dsetconstrER:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->(Xphi Xx))) % FOF formula (<kernel.Constant object at 0x210f128>, <kernel.DependentProduct object at 0x210f710>) of role type named singleton_type % Using role type % Declaring singleton:(fofType->Prop) % FOF formula (((eq (fofType->Prop)) singleton) (fun (A:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (((eq fofType) A) ((setadjoin Xx) emptyset))))))) of role definition named singleton % A new definition: (((eq (fofType->Prop)) singleton) (fun (A:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (((eq fofType) A) ((setadjoin Xx) emptyset))))))) % Defined: singleton:=(fun (A:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (((eq fofType) A) ((setadjoin Xx) emptyset)))))) % FOF formula (<kernel.Constant object at 0x210f710>, <kernel.DependentProduct object at 0x210f758>) of role type named ex1_type % Using role type % Declaring ex1:(fofType->((fofType->Prop)->Prop)) % FOF formula (((eq (fofType->((fofType->Prop)->Prop))) ex1) (fun (A:fofType) (Xphi:(fofType->Prop))=> (singleton ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))))) of role definition named ex1 % A new definition: (((eq (fofType->((fofType->Prop)->Prop))) ex1) (fun (A:fofType) (Xphi:(fofType->Prop))=> (singleton ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))))) % Defined: ex1:=(fun (A:fofType) (Xphi:(fofType->Prop))=> (singleton ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) % FOF formula (dsetconstrEL->(dsetconstrER->(forall (A:fofType) (Xphi:(fofType->Prop)), (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))))))) of role conjecture named ex1E1 % Conjecture to prove = (dsetconstrEL->(dsetconstrER->(forall (A:fofType) (Xphi:(fofType->Prop)), (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))))))):Prop % We need to prove ['(dsetconstrEL->(dsetconstrER->(forall (A:fofType) (Xphi:(fofType->Prop)), (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))))))'] % Parameter fofType:Type. % Parameter in:(fofType->(fofType->Prop)). % Parameter emptyset:fofType. % Parameter setadjoin:(fofType->(fofType->fofType)). % Parameter dsetconstr:(fofType->((fofType->Prop)->fofType)). % Definition dsetconstrEL:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->((in Xx) A))):Prop. % Definition dsetconstrER:=(forall (A:fofType) (Xphi:(fofType->Prop)) (Xx:fofType), (((in Xx) ((dsetconstr A) (fun (Xy:fofType)=> (Xphi Xy))))->(Xphi Xx))):Prop. % Definition singleton:=(fun (A:fofType)=> ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (((eq fofType) A) ((setadjoin Xx) emptyset)))))):(fofType->Prop). % Definition ex1:=(fun (A:fofType) (Xphi:(fofType->Prop))=> (singleton ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))):(fofType->((fofType->Prop)->Prop)). % Trying to prove (dsetconstrEL->(dsetconstrER->(forall (A:fofType) (Xphi:(fofType->Prop)), (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))))))) % Found x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))) % Instantiate: b:=(fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> ((fun (Xx:fofType)=> (Xphi Xx)) Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> ((fun (Xx:fofType)=> (Xphi Xx)) Xx)))) ((setadjoin Xx) emptyset)))):(fofType->Prop) % Found x1 as proof of (P b) % Found eta_expansion000:=(eta_expansion00 (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))):(((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) (fun (x:fofType)=> ((and ((in x) A)) (Xphi x)))) % Found (eta_expansion00 (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found ((eta_expansion0 Prop) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found (((eta_expansion fofType) Prop) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found (((eta_expansion fofType) Prop) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found (((eta_expansion fofType) Prop) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))) % Instantiate: f:=(fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> ((fun (Xx:fofType)=> (Xphi Xx)) Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> ((fun (Xx:fofType)=> (Xphi Xx)) Xx)))) ((setadjoin Xx) emptyset)))):(fofType->Prop) % Found x1 as proof of (P f) % Found eq_ref00:=(eq_ref0 (f x4)):(((eq Prop) (f x4)) (f x4)) % Found (eq_ref0 (f x4)) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found (fun (x4:fofType)=> ((eq_ref Prop) (f x4))) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found (fun (x4:fofType)=> ((eq_ref Prop) (f x4))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) (Xphi x)))) % Found x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))) % Instantiate: f:=(fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> ((fun (Xx:fofType)=> (Xphi Xx)) Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> ((fun (Xx:fofType)=> (Xphi Xx)) Xx)))) ((setadjoin Xx) emptyset)))):(fofType->Prop) % Found x1 as proof of (P f) % Found eq_ref00:=(eq_ref0 (f x4)):(((eq Prop) (f x4)) (f x4)) % Found (eq_ref0 (f x4)) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found (fun (x4:fofType)=> ((eq_ref Prop) (f x4))) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found (fun (x4:fofType)=> ((eq_ref Prop) (f x4))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) (Xphi x)))) % Found x1:((ex1 A) Xphi) % Instantiate: b:=(fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset)))):(fofType->Prop) % Found x1 as proof of (P b) % Found eq_ref00:=(eq_ref0 (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))):(((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found (eq_ref0 (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found ((eq_ref (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found ((eq_ref (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found ((eq_ref (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found x1:((ex1 A) Xphi) % Instantiate: f:=(fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset)))):(fofType->Prop) % Found x1 as proof of (P f) % Found eq_ref00:=(eq_ref0 (f x4)):(((eq Prop) (f x4)) (f x4)) % Found (eq_ref0 (f x4)) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found (fun (x4:fofType)=> ((eq_ref Prop) (f x4))) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found (fun (x4:fofType)=> ((eq_ref Prop) (f x4))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) (Xphi x)))) % Found x1:((ex1 A) Xphi) % Instantiate: f:=(fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset)))):(fofType->Prop) % Found x1 as proof of (P f) % Found eq_ref00:=(eq_ref0 (f x4)):(((eq Prop) (f x4)) (f x4)) % Found (eq_ref0 (f x4)) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found ((eq_ref Prop) (f x4)) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found (fun (x4:fofType)=> ((eq_ref Prop) (f x4))) as proof of (((eq Prop) (f x4)) ((and ((in x4) A)) (Xphi x4))) % Found (fun (x4:fofType)=> ((eq_ref Prop) (f x4))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) (Xphi x)))) % Found x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))) % Instantiate: b:=(fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> ((fun (Xx:fofType)=> (Xphi Xx)) Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> ((fun (Xx:fofType)=> (Xphi Xx)) Xx)))) ((setadjoin Xx) emptyset)))):(fofType->Prop) % Found x1 as proof of (P b) % Found eta_expansion000:=(eta_expansion00 (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))):(((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) (fun (x:fofType)=> ((and ((in x) A)) (Xphi x)))) % Found (eta_expansion00 (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found ((eta_expansion0 Prop) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found (((eta_expansion fofType) Prop) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found (((eta_expansion fofType) Prop) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found (((eta_expansion fofType) Prop) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))) % Instantiate: f:=(fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> ((fun (Xx:fofType)=> (Xphi Xx)) Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> ((fun (Xx:fofType)=> (Xphi Xx)) Xx)))) ((setadjoin Xx) emptyset)))):(fofType->Prop) % Found x1 as proof of (P f) % Found x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))) % Instantiate: f:=(fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> ((fun (Xx:fofType)=> (Xphi Xx)) Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> ((fun (Xx:fofType)=> (Xphi Xx)) Xx)))) ((setadjoin Xx) emptyset)))):(fofType->Prop) % Found x1 as proof of (P f) % Found eq_ref00:=(eq_ref0 (f x6)):(((eq Prop) (f x6)) (f x6)) % Found (eq_ref0 (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found ((eq_ref Prop) (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found ((eq_ref Prop) (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found (fun (x6:fofType)=> ((eq_ref Prop) (f x6))) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found (fun (x6:fofType)=> ((eq_ref Prop) (f x6))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) (Xphi x)))) % Found eq_ref00:=(eq_ref0 (f x6)):(((eq Prop) (f x6)) (f x6)) % Found (eq_ref0 (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found ((eq_ref Prop) (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found ((eq_ref Prop) (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found (fun (x6:fofType)=> ((eq_ref Prop) (f x6))) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found (fun (x6:fofType)=> ((eq_ref Prop) (f x6))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) (Xphi x)))) % Found x1:((ex1 A) Xphi) % Instantiate: b:=(fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset)))):(fofType->Prop) % Found x1 as proof of (P b) % Found eta_expansion000:=(eta_expansion00 (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))):(((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) (fun (x:fofType)=> ((and ((in x) A)) (Xphi x)))) % Found (eta_expansion00 (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found ((eta_expansion0 Prop) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found (((eta_expansion fofType) Prop) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found (((eta_expansion fofType) Prop) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found (((eta_expansion fofType) Prop) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) b) % Found x1:((ex1 A) Xphi) % Instantiate: f:=(fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset)))):(fofType->Prop) % Found x1 as proof of (P f) % Found x1:((ex1 A) Xphi) % Instantiate: f:=(fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset)))):(fofType->Prop) % Found x1 as proof of (P f) % Found eq_ref00:=(eq_ref0 (f x6)):(((eq Prop) (f x6)) (f x6)) % Found (eq_ref0 (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found ((eq_ref Prop) (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found ((eq_ref Prop) (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found (fun (x6:fofType)=> ((eq_ref Prop) (f x6))) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found (fun (x6:fofType)=> ((eq_ref Prop) (f x6))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) (Xphi x)))) % Found eq_ref00:=(eq_ref0 (f x6)):(((eq Prop) (f x6)) (f x6)) % Found (eq_ref0 (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found ((eq_ref Prop) (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found ((eq_ref Prop) (f x6)) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found (fun (x6:fofType)=> ((eq_ref Prop) (f x6))) as proof of (((eq Prop) (f x6)) ((and ((in x6) A)) (Xphi x6))) % Found (fun (x6:fofType)=> ((eq_ref Prop) (f x6))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) (Xphi x)))) % Found x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) % Instantiate: A0:=A:fofType;x6:=x2:fofType % Found x4 as proof of ((in x6) ((dsetconstr A0) (fun (Xy:fofType)=> (Xphi Xy)))) % Found (x0000 x4) as proof of (Xphi x6) % Found ((x000 Xphi) x4) as proof of (Xphi x6) % Found (((x00 A) Xphi) x4) as proof of (Xphi x6) % Found ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x6)) A) Xphi) x4) as proof of (Xphi x6) % Found ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x6)) A) Xphi) x4) as proof of (Xphi x6) % Found x7000:=(x700 x4):((in x6) A) % Found (x700 x4) as proof of ((in x6) A) % Found ((x70 Xphi) x4) as proof of ((in x6) A) % Found (((fun (Xphi0:(fofType->Prop))=> ((x7 Xphi0) x6)) Xphi) x4) as proof of ((in x6) A) % Found (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x6)) Xphi) x4) as proof of ((in x6) A) % Found (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x6)) Xphi) x4) as proof of ((in x6) A) % Found ((conj00 (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x6)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x6)) A) Xphi) x4)) as proof of ((and ((in x6) A)) (Xphi x6)) % Found (((conj0 (Xphi x6)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x6)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x6)) A) Xphi) x4)) as proof of ((and ((in x6) A)) (Xphi x6)) % Found ((((conj ((in x6) A)) (Xphi x6)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x6)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x6)) A) Xphi) x4)) as proof of ((and ((in x6) A)) (Xphi x6)) % Found ((((conj ((in x6) A)) (Xphi x6)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x6)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x6)) A) Xphi) x4)) as proof of ((and ((in x6) A)) (Xphi x6)) % Found (ex_intro000 ((((conj ((in x6) A)) (Xphi x6)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x6)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x6)) A) Xphi) x4))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found ((ex_intro00 x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found (((ex_intro0 (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found (fun (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))) as proof of ((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) % Found (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))) as proof of (((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))))) % Found (and_rect00 (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found ((and_rect0 ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found (fun (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))))) as proof of (((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) % Found (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))))) as proof of (forall (x:fofType), (((and ((in x) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x) emptyset)))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))))) % Found (ex_ind00 (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found ((ex_ind0 ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found (fun (x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))))))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) % Found (fun (Xphi:(fofType->Prop)) (x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))))))) as proof of (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) % Found (fun (A:fofType) (Xphi:(fofType->Prop)) (x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))))))) as proof of (forall (Xphi:(fofType->Prop)), (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))))) % Found (fun (x0:dsetconstrER) (A:fofType) (Xphi:(fofType->Prop)) (x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))))))) as proof of (forall (A:fofType) (Xphi:(fofType->Prop)), (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))))) % Found (fun (x:dsetconstrEL) (x0:dsetconstrER) (A:fofType) (Xphi:(fofType->Prop)) (x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))))))) as proof of (dsetconstrER->(forall (A:fofType) (Xphi:(fofType->Prop)), (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))))) % Found (fun (x:dsetconstrEL) (x0:dsetconstrER) (A:fofType) (Xphi:(fofType->Prop)) (x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))))))) as proof of (dsetconstrEL->(dsetconstrER->(forall (A:fofType) (Xphi:(fofType->Prop)), (((ex1 A) (fun (Xx:fofType)=> (Xphi Xx)))->((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))))))) % Got proof (fun (x:dsetconstrEL) (x0:dsetconstrER) (A:fofType) (Xphi:(fofType->Prop)) (x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))))))) % Time elapsed = 37.594368s % node=4837 cost=1170.000000 depth=30 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:dsetconstrEL) (x0:dsetconstrER) (A:fofType) (Xphi:(fofType->Prop)) (x1:((ex1 A) (fun (Xx:fofType)=> (Xphi Xx))))=> (((fun (P:Prop) (x2:(forall (x:fofType), (((and ((in x) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x) emptyset)))->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> ((and ((in Xx) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin Xx) emptyset))))) P) x2) x1)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x2:fofType) (x3:((and ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))))=> (((fun (P:Type) (x4:(((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))->((((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))->P)))=> (((((and_rect ((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset))) P) x4) x3)) ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx))))) (fun (x4:((in x2) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx))))) (x5:(((eq fofType) ((dsetconstr A) (fun (Xx:fofType)=> (Xphi Xx)))) ((setadjoin x2) emptyset)))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) (Xphi Xx)))) x2) ((((conj ((in x2) A)) (Xphi x2)) (((fun (Xphi0:(fofType->Prop))=> (((x A) Xphi0) x2)) Xphi) x4)) ((((fun (A0:fofType) (Xphi0:(fofType->Prop))=> (((x0 A0) Xphi0) x2)) A) Xphi) x4)))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------