↑ Up

cocATP---0.2.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : cocATP---0.2.0
% Problem  : SEU929^5 : TPTP v6.1.0. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n097.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:33:23 EDT 2014

% Result   : Theorem 6.86s
% Output   : Proof 6.86s
% Verified : 
% SZS Type : None (Parsing solution fails)
% Syntax   : Number of formulae    : 0

% Comments : 
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % Problem  : SEU929^5 : TPTP v6.1.0. Released v4.0.0.
% % Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p
% % Computer : n097.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 11:43:06 CDT 2014
% % CPUTime  : 6.86 
% 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 0x222cdd0>, <kernel.DependentProduct object at 0x222c3f8>) of role type named f
% Using role type
% Declaring f:(fofType->fofType)
% FOF formula (<kernel.Constant object at 0x241a0e0>, <kernel.DependentProduct object at 0x222c758>) of role type named g
% Using role type
% Declaring g:(fofType->fofType)
% FOF formula ((forall (Xp:((fofType->fofType)->Prop)), (((and (Xp f)) (forall (Xj:(fofType->fofType)), ((Xp Xj)->(Xp (fun (Xx:fofType)=> (f (Xj Xx)))))))->(Xp g)))->(((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx))))) of role conjecture named cTHM170_pme
% Conjecture to prove = ((forall (Xp:((fofType->fofType)->Prop)), (((and (Xp f)) (forall (Xj:(fofType->fofType)), ((Xp Xj)->(Xp (fun (Xx:fofType)=> (f (Xj Xx)))))))->(Xp g)))->(((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx))))):Prop
% Parameter fofType_DUMMY:fofType.
% We need to prove ['((forall (Xp:((fofType->fofType)->Prop)), (((and (Xp f)) (forall (Xj:(fofType->fofType)), ((Xp Xj)->(Xp (fun (Xx:fofType)=> (f (Xj Xx)))))))->(Xp g)))->(((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx)))))']
% Parameter fofType:Type.
% Parameter f:(fofType->fofType).
% Parameter g:(fofType->fofType).
% Trying to prove ((forall (Xp:((fofType->fofType)->Prop)), (((and (Xp f)) (forall (Xj:(fofType->fofType)), ((Xp Xj)->(Xp (fun (Xx:fofType)=> (f (Xj Xx)))))))->(Xp g)))->(((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx)))))
% Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xx:fofType)=> (f (f Xx)))):(((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (f Xx)))) (fun (x:fofType)=> (f (f x))))
% Found (eta_expansion_dep00 (fun (Xx:fofType)=> (f (f Xx)))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (f Xx)))) (fun (Xx:fofType)=> (f (f Xx))))
% Found ((eta_expansion_dep0 (fun (x2:fofType)=> fofType)) (fun (Xx:fofType)=> (f (f Xx)))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (f Xx)))) (fun (Xx:fofType)=> (f (f Xx))))
% Found (((eta_expansion_dep fofType) (fun (x2:fofType)=> fofType)) (fun (Xx:fofType)=> (f (f Xx)))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (f Xx)))) (fun (Xx:fofType)=> (f (f Xx))))
% Found (((eta_expansion_dep fofType) (fun (x2:fofType)=> fofType)) (fun (Xx:fofType)=> (f (f Xx)))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (f Xx)))) (fun (Xx:fofType)=> (f (f Xx))))
% Found x00:(P (fun (Xx:fofType)=> (f (g Xx))))
% Found (fun (x00:(P (fun (Xx:fofType)=> (f (g Xx)))))=> x00) as proof of (P (fun (Xx:fofType)=> (f (g Xx))))
% Found (fun (x00:(P (fun (Xx:fofType)=> (f (g Xx)))))=> x00) as proof of (P0 (fun (Xx:fofType)=> (f (g Xx))))
% Found eq_ref00:=(eq_ref0 (fun (Xx:fofType)=> (f (f Xx)))):(((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (f Xx)))) (fun (Xx:fofType)=> (f (f Xx))))
% Found (eq_ref0 (fun (Xx:fofType)=> (f (f Xx)))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (f Xx)))) (fun (Xx:fofType)=> (f (f Xx))))
% Found ((eq_ref (fofType->fofType)) (fun (Xx:fofType)=> (f (f Xx)))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (f Xx)))) (fun (Xx:fofType)=> (f (f Xx))))
% Found ((eq_ref (fofType->fofType)) (fun (Xx:fofType)=> (f (f Xx)))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (f Xx)))) (fun (Xx:fofType)=> (f (f Xx))))
% Found x00:(P (fun (Xx:fofType)=> (f (g Xx))))
% Found (fun (x00:(P (fun (Xx:fofType)=> (f (g Xx)))))=> x00) as proof of (P (fun (Xx:fofType)=> (f (g Xx))))
% Found (fun (x00:(P (fun (Xx:fofType)=> (f (g Xx)))))=> x00) as proof of (P0 (fun (Xx:fofType)=> (f (g Xx))))
% Found x00:(P (fun (Xx:fofType)=> (f (g Xx))))
% Found (fun (x00:(P (fun (Xx:fofType)=> (f (g Xx)))))=> x00) as proof of (P (fun (Xx:fofType)=> (f (g Xx))))
% Found (fun (x00:(P (fun (Xx:fofType)=> (f (g Xx)))))=> x00) as proof of (P0 (fun (Xx:fofType)=> (f (g Xx))))
% Found eq_ref00:=(eq_ref0 (f (f x0))):(((eq fofType) (f (f x0))) (f (f x0)))
% Found (eq_ref0 (f (f x0))) as proof of (((eq fofType) (f (f x0))) (f (f x0)))
% Found ((eq_ref fofType) (f (f x0))) as proof of (((eq fofType) (f (f x0))) (f (f x0)))
% Found ((eq_ref fofType) (f (f x0))) as proof of (((eq fofType) (f (f x0))) (f (f x0)))
% Found eq_substitution00000:=(eq_substitution0000 f):((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0)))))
% Found (eq_substitution0000 f) as proof of ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0)))))
% Found ((eq_substitution000 (Xj (f x0))) f) as proof of ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0)))))
% Found (((eq_substitution00 (f (Xj x0))) (Xj (f x0))) f) as proof of ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0)))))
% Found ((((eq_substitution0 fofType) (f (Xj x0))) (Xj (f x0))) f) as proof of ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0)))))
% Found (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f) as proof of ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0)))))
% Found (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f)) as proof of ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0)))))
% Found (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f)) as proof of (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))
% Found ((conj00 ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f))) as proof of ((and (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0)))))))
% Found (((conj0 (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f))) as proof of ((and (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0)))))))
% Found ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f))) as proof of ((and (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0)))))))
% Found ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f))) as proof of ((and (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0)))))))
% Found (x1 ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f)))) as proof of (((eq fofType) (f (g x0))) (g (f x0)))
% Found ((x (fun (x2:(fofType->fofType))=> (((eq fofType) (f (x2 x0))) (x2 (f x0))))) ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f)))) as proof of (((eq fofType) (f (g x0))) (g (f x0)))
% Found (fun (x0:fofType)=> ((x (fun (x2:(fofType->fofType))=> (((eq fofType) (f (x2 x0))) (x2 (f x0))))) ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f))))) as proof of (((eq fofType) (f (g x0))) (g (f x0)))
% Found (fun (x0:fofType)=> ((x (fun (x2:(fofType->fofType))=> (((eq fofType) (f (x2 x0))) (x2 (f x0))))) ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f))))) as proof of (forall (x:fofType), (((eq fofType) (f (g x))) (g (f x))))
% Found (functional_extensionality_dep0000 (fun (x0:fofType)=> ((x (fun (x2:(fofType->fofType))=> (((eq fofType) (f (x2 x0))) (x2 (f x0))))) ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f)))))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx))))
% Found ((functional_extensionality_dep000 (fun (Xx:fofType)=> (g (f Xx)))) (fun (x0:fofType)=> ((x (fun (x2:(fofType->fofType))=> (((eq fofType) (f (x2 x0))) (x2 (f x0))))) ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f)))))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx))))
% Found (((functional_extensionality_dep00 (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx)))) (fun (x0:fofType)=> ((x (fun (x2:(fofType->fofType))=> (((eq fofType) (f (x2 x0))) (x2 (f x0))))) ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f)))))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx))))
% Found ((((functional_extensionality_dep0 (fun (x2:fofType)=> fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx)))) (fun (x0:fofType)=> ((x (fun (x2:(fofType->fofType))=> (((eq fofType) (f (x2 x0))) (x2 (f x0))))) ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f)))))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx))))
% Found (((((functional_extensionality_dep fofType) (fun (x2:fofType)=> fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx)))) (fun (x0:fofType)=> ((x (fun (x2:(fofType->fofType))=> (((eq fofType) (f (x2 x0))) (x2 (f x0))))) ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f)))))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx))))
% Found (fun (x:(forall (Xp:((fofType->fofType)->Prop)), (((and (Xp f)) (forall (Xj:(fofType->fofType)), ((Xp Xj)->(Xp (fun (Xx:fofType)=> (f (Xj Xx)))))))->(Xp g))))=> (((((functional_extensionality_dep fofType) (fun (x2:fofType)=> fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx)))) (fun (x0:fofType)=> ((x (fun (x2:(fofType->fofType))=> (((eq fofType) (f (x2 x0))) (x2 (f x0))))) ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f))))))) as proof of (((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx))))
% Found (fun (x:(forall (Xp:((fofType->fofType)->Prop)), (((and (Xp f)) (forall (Xj:(fofType->fofType)), ((Xp Xj)->(Xp (fun (Xx:fofType)=> (f (Xj Xx)))))))->(Xp g))))=> (((((functional_extensionality_dep fofType) (fun (x2:fofType)=> fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx)))) (fun (x0:fofType)=> ((x (fun (x2:(fofType->fofType))=> (((eq fofType) (f (x2 x0))) (x2 (f x0))))) ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f))))))) as proof of ((forall (Xp:((fofType->fofType)->Prop)), (((and (Xp f)) (forall (Xj:(fofType->fofType)), ((Xp Xj)->(Xp (fun (Xx:fofType)=> (f (Xj Xx)))))))->(Xp g)))->(((eq (fofType->fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx)))))
% Got proof (fun (x:(forall (Xp:((fofType->fofType)->Prop)), (((and (Xp f)) (forall (Xj:(fofType->fofType)), ((Xp Xj)->(Xp (fun (Xx:fofType)=> (f (Xj Xx)))))))->(Xp g))))=> (((((functional_extensionality_dep fofType) (fun (x2:fofType)=> fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx)))) (fun (x0:fofType)=> ((x (fun (x2:(fofType->fofType))=> (((eq fofType) (f (x2 x0))) (x2 (f x0))))) ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f)))))))
% Time elapsed = 6.495419s
% node=1147 cost=-20.000000 depth=21
% ::::::::::::::::::::::
% % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% (fun (x:(forall (Xp:((fofType->fofType)->Prop)), (((and (Xp f)) (forall (Xj:(fofType->fofType)), ((Xp Xj)->(Xp (fun (Xx:fofType)=> (f (Xj Xx)))))))->(Xp g))))=> (((((functional_extensionality_dep fofType) (fun (x2:fofType)=> fofType)) (fun (Xx:fofType)=> (f (g Xx)))) (fun (Xx:fofType)=> (g (f Xx)))) (fun (x0:fofType)=> ((x (fun (x2:(fofType->fofType))=> (((eq fofType) (f (x2 x0))) (x2 (f x0))))) ((((conj (((eq fofType) (f (f x0))) (f (f x0)))) (forall (Xj:(fofType->fofType)), ((((eq fofType) (f (Xj x0))) (Xj (f x0)))->(((eq fofType) (f (f (Xj x0)))) (f (Xj (f x0))))))) ((eq_ref fofType) (f (f x0)))) (fun (Xj:(fofType->fofType))=> (((((eq_substitution fofType) fofType) (f (Xj x0))) (Xj (f x0))) f)))))))
% % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% EOF
%------------------------------------------------------------------------------