↑ Up

cocATP---0.2.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : cocATP---0.2.0
% Problem  : SEU699^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 : n092.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:51 EDT 2014

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

% Comments : 
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % Problem  : SEU699^2 : TPTP v6.1.0. Released v3.7.0.
% % Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p
% % Computer : n092.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:14:26 CDT 2014
% % CPUTime  : 8.27 
% 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 0x1dac290>, <kernel.DependentProduct object at 0x1daaea8>) of role type named in_type
% Using role type
% Declaring in:(fofType->(fofType->Prop))
% FOF formula (<kernel.Constant object at 0x1dac0e0>, <kernel.DependentProduct object at 0x1daa908>) of role type named funcSet_type
% Using role type
% Declaring funcSet:(fofType->(fofType->fofType))
% FOF formula (<kernel.Constant object at 0x1dac7e8>, <kernel.DependentProduct object at 0x1daa908>) of role type named ap_type
% Using role type
% Declaring ap:(fofType->(fofType->(fofType->(fofType->fofType))))
% FOF formula (<kernel.Constant object at 0x1dac290>, <kernel.Sort object at 0x1e5cb48>) of role type named ap2p_type
% Using role type
% Declaring ap2p:Prop
% FOF formula (((eq Prop) ap2p) (forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))))) of role definition named ap2p
% A new definition: (((eq Prop) ap2p) (forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B))))))
% Defined: ap2p:=(forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))))
% FOF formula (<kernel.Constant object at 0x1dac290>, <kernel.DependentProduct object at 0x1daacb0>) of role type named lam_type
% Using role type
% Declaring lam:(fofType->(fofType->((fofType->fofType)->fofType)))
% FOF formula (<kernel.Constant object at 0x1dac0e0>, <kernel.Sort object at 0x1e5cb48>) of role type named lam2p_type
% Using role type
% Declaring lam2p:Prop
% FOF formula (((eq Prop) lam2p) (forall (A:fofType) (B:fofType) (Xf:(fofType->fofType)), ((forall (Xx:fofType), (((in Xx) A)->((in (Xf Xx)) B)))->((in (((lam A) B) (fun (Xx:fofType)=> (Xf Xx)))) ((funcSet A) B))))) of role definition named lam2p
% A new definition: (((eq Prop) lam2p) (forall (A:fofType) (B:fofType) (Xf:(fofType->fofType)), ((forall (Xx:fofType), (((in Xx) A)->((in (Xf Xx)) B)))->((in (((lam A) B) (fun (Xx:fofType)=> (Xf Xx)))) ((funcSet A) B)))))
% Defined: lam2p:=(forall (A:fofType) (B:fofType) (Xf:(fofType->fofType)), ((forall (Xx:fofType), (((in Xx) A)->((in (Xf Xx)) B)))->((in (((lam A) B) (fun (Xx:fofType)=> (Xf Xx)))) ((funcSet A) B))))
% FOF formula (<kernel.Constant object at 0x1daaef0>, <kernel.Sort object at 0x1e5cb48>) of role type named funcext2_type
% Using role type
% Declaring funcext2:Prop
% FOF formula (((eq Prop) funcext2) (forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(forall (Xg:fofType), (((in Xg) ((funcSet A) B))->((forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) Xf) Xx)) ((((ap A) B) Xg) Xx))))->(((eq fofType) Xf) Xg))))))) of role definition named funcext2
% A new definition: (((eq Prop) funcext2) (forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(forall (Xg:fofType), (((in Xg) ((funcSet A) B))->((forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) Xf) Xx)) ((((ap A) B) Xg) Xx))))->(((eq fofType) Xf) Xg)))))))
% Defined: funcext2:=(forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(forall (Xg:fofType), (((in Xg) ((funcSet A) B))->((forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) Xf) Xx)) ((((ap A) B) Xg) Xx))))->(((eq fofType) Xf) Xg))))))
% FOF formula (<kernel.Constant object at 0x1daaab8>, <kernel.Sort object at 0x1e5cb48>) of role type named beta2_type
% Using role type
% Declaring beta2:Prop
% FOF formula (((eq Prop) beta2) (forall (A:fofType) (B:fofType) (Xf:(fofType->fofType)), ((forall (Xx:fofType), (((in Xx) A)->((in (Xf Xx)) B)))->(forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) (((lam A) B) (fun (Xy:fofType)=> (Xf Xy)))) Xx)) (Xf Xx))))))) of role definition named beta2
% A new definition: (((eq Prop) beta2) (forall (A:fofType) (B:fofType) (Xf:(fofType->fofType)), ((forall (Xx:fofType), (((in Xx) A)->((in (Xf Xx)) B)))->(forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) (((lam A) B) (fun (Xy:fofType)=> (Xf Xy)))) Xx)) (Xf Xx)))))))
% Defined: beta2:=(forall (A:fofType) (B:fofType) (Xf:(fofType->fofType)), ((forall (Xx:fofType), (((in Xx) A)->((in (Xf Xx)) B)))->(forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) (((lam A) B) (fun (Xy:fofType)=> (Xf Xy)))) Xx)) (Xf Xx))))))
% FOF formula (ap2p->(lam2p->(funcext2->(beta2->(forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf))))))) of role conjecture named eta2
% Conjecture to prove = (ap2p->(lam2p->(funcext2->(beta2->(forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf))))))):Prop
% Parameter fofType_DUMMY:fofType.
% We need to prove ['(ap2p->(lam2p->(funcext2->(beta2->(forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf)))))))']
% Parameter fofType:Type.
% Parameter in:(fofType->(fofType->Prop)).
% Parameter funcSet:(fofType->(fofType->fofType)).
% Parameter ap:(fofType->(fofType->(fofType->(fofType->fofType)))).
% Definition ap2p:=(forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B))))):Prop.
% Parameter lam:(fofType->(fofType->((fofType->fofType)->fofType))).
% Definition lam2p:=(forall (A:fofType) (B:fofType) (Xf:(fofType->fofType)), ((forall (Xx:fofType), (((in Xx) A)->((in (Xf Xx)) B)))->((in (((lam A) B) (fun (Xx:fofType)=> (Xf Xx)))) ((funcSet A) B)))):Prop.
% Definition funcext2:=(forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(forall (Xg:fofType), (((in Xg) ((funcSet A) B))->((forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) Xf) Xx)) ((((ap A) B) Xg) Xx))))->(((eq fofType) Xf) Xg)))))):Prop.
% Definition beta2:=(forall (A:fofType) (B:fofType) (Xf:(fofType->fofType)), ((forall (Xx:fofType), (((in Xx) A)->((in (Xf Xx)) B)))->(forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) (((lam A) B) (fun (Xy:fofType)=> (Xf Xy)))) Xx)) (Xf Xx)))))):Prop.
% Trying to prove (ap2p->(lam2p->(funcext2->(beta2->(forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf)))))))
% Found eq_ref00:=(eq_ref0 (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))):(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))
% Found (eq_ref0 (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) as proof of (((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) b)
% Found ((eq_ref fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) as proof of (((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) b)
% Found ((eq_ref fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) as proof of (((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) b)
% Found ((eq_ref fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) as proof of (((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) b)
% Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b)
% Found (eq_ref0 b) as proof of (((eq fofType) b) Xf)
% Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xf)
% Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xf)
% Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xf)
% Found x3:((in Xf) ((funcSet A) B))
% Found x3 as proof of ((in Xf) ((funcSet A) B))
% Found eq_ref00:=(eq_ref0 Xf):(((eq fofType) Xf) Xf)
% Found (eq_ref0 Xf) as proof of (((eq fofType) Xf) b)
% Found ((eq_ref fofType) Xf) as proof of (((eq fofType) Xf) b)
% Found ((eq_ref fofType) Xf) as proof of (((eq fofType) Xf) b)
% Found ((eq_ref fofType) Xf) as proof of (((eq fofType) Xf) b)
% Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b)
% Found (eq_ref0 b) as proof of (((eq fofType) b) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))
% Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))
% Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))
% Found ((eq_ref fofType) b) as proof of (((eq fofType) b) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))
% Found x3:((in Xf) ((funcSet A) B))
% Found x3 as proof of ((in Xf) ((funcSet A) B))
% Found x4:(P (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))
% Instantiate: b:=(((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))):fofType
% Found x4 as proof of (P0 b)
% Found eq_ref00:=(eq_ref0 Xf):(((eq fofType) Xf) Xf)
% Found (eq_ref0 Xf) as proof of (((eq fofType) Xf) b)
% Found ((eq_ref fofType) Xf) as proof of (((eq fofType) Xf) b)
% Found ((eq_ref fofType) Xf) as proof of (((eq fofType) Xf) b)
% Found ((eq_ref fofType) Xf) as proof of (((eq fofType) Xf) b)
% Found x3:((in Xf) ((funcSet A) B))
% Found x3 as proof of ((in Xf) ((funcSet A) B))
% Found x4000:=(x400 x3):(forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))
% Found (x400 x3) as proof of (forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))
% Found ((x40 Xf) x3) as proof of (forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))
% Found (((x4 B) Xf) x3) as proof of (forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))
% Found ((((x A) B) Xf) x3) as proof of (forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))
% Found ((((x A) B) Xf) x3) as proof of (forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))
% Found (x2000 ((((x A) B) Xf) x3)) as proof of (forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xx)) ((((ap A) B) Xf) Xx))))
% Found ((x200 (((ap A) B) Xf)) ((((x A) B) Xf) x3)) as proof of (forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xx)) ((((ap A) B) Xf) Xx))))
% Found (((x20 B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)) as proof of (forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xx)) ((((ap A) B) Xf) Xx))))
% Found ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)) as proof of (forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xx)) ((((ap A) B) Xf) Xx))))
% Found ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)) as proof of (forall (Xx:fofType), (((in Xx) A)->(((eq fofType) ((((ap A) B) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xx)) ((((ap A) B) Xf) Xx))))
% Found x4000:=(x400 x3):(forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))
% Found (x400 x3) as proof of (forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))
% Found ((x40 Xf) x3) as proof of (forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))
% Found (((x4 B) Xf) x3) as proof of (forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))
% Found ((((x A) B) Xf) x3) as proof of (forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))
% Found ((((x A) B) Xf) x3) as proof of (forall (Xx:fofType), (((in Xx) A)->((in ((((ap A) B) Xf) Xx)) B)))
% Found (x0000 ((((x A) B) Xf) x3)) as proof of ((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A) B))
% Found ((x000 (((ap A) B) Xf)) ((((x A) B) Xf) x3)) as proof of ((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A) B))
% Found (((x00 B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)) as proof of ((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A) B))
% Found ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)) as proof of ((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A) B))
% Found ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)) as proof of ((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A) B))
% Found (((x1000 ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) as proof of (((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf)
% Found (((((x100 A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) as proof of (((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf)
% Found ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> ((((x10 A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) as proof of (((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf)
% Found ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> (((((fun (A0:fofType) (B0:fofType)=> (((x1 A0) B0) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))) A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) as proof of (((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf)
% Found (fun (x3:((in Xf) ((funcSet A) B)))=> ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> (((((fun (A0:fofType) (B0:fofType)=> (((x1 A0) B0) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))) A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)))) as proof of (((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf)
% Found (fun (Xf:fofType) (x3:((in Xf) ((funcSet A) B)))=> ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> (((((fun (A0:fofType) (B0:fofType)=> (((x1 A0) B0) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))) A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)))) as proof of (((in Xf) ((funcSet A) B))->(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf))
% Found (fun (B:fofType) (Xf:fofType) (x3:((in Xf) ((funcSet A) B)))=> ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> (((((fun (A0:fofType) (B0:fofType)=> (((x1 A0) B0) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))) A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)))) as proof of (forall (Xf:fofType), (((in Xf) ((funcSet A) B))->(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf)))
% Found (fun (A:fofType) (B:fofType) (Xf:fofType) (x3:((in Xf) ((funcSet A) B)))=> ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> (((((fun (A0:fofType) (B0:fofType)=> (((x1 A0) B0) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))) A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)))) as proof of (forall (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf)))
% Found (fun (x2:beta2) (A:fofType) (B:fofType) (Xf:fofType) (x3:((in Xf) ((funcSet A) B)))=> ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> (((((fun (A0:fofType) (B0:fofType)=> (((x1 A0) B0) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))) A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)))) as proof of (forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf)))
% Found (fun (x1:funcext2) (x2:beta2) (A:fofType) (B:fofType) (Xf:fofType) (x3:((in Xf) ((funcSet A) B)))=> ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> (((((fun (A0:fofType) (B0:fofType)=> (((x1 A0) B0) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))) A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)))) as proof of (beta2->(forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf))))
% Found (fun (x0:lam2p) (x1:funcext2) (x2:beta2) (A:fofType) (B:fofType) (Xf:fofType) (x3:((in Xf) ((funcSet A) B)))=> ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> (((((fun (A0:fofType) (B0:fofType)=> (((x1 A0) B0) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))) A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)))) as proof of (funcext2->(beta2->(forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf)))))
% Found (fun (x:ap2p) (x0:lam2p) (x1:funcext2) (x2:beta2) (A:fofType) (B:fofType) (Xf:fofType) (x3:((in Xf) ((funcSet A) B)))=> ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> (((((fun (A0:fofType) (B0:fofType)=> (((x1 A0) B0) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))) A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)))) as proof of (lam2p->(funcext2->(beta2->(forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf))))))
% Found (fun (x:ap2p) (x0:lam2p) (x1:funcext2) (x2:beta2) (A:fofType) (B:fofType) (Xf:fofType) (x3:((in Xf) ((funcSet A) B)))=> ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> (((((fun (A0:fofType) (B0:fofType)=> (((x1 A0) B0) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))) A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3)))) as proof of (ap2p->(lam2p->(funcext2->(beta2->(forall (A:fofType) (B:fofType) (Xf:fofType), (((in Xf) ((funcSet A) B))->(((eq fofType) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) Xf)))))))
% Got proof (fun (x:ap2p) (x0:lam2p) (x1:funcext2) (x2:beta2) (A:fofType) (B:fofType) (Xf:fofType) (x3:((in Xf) ((funcSet A) B)))=> ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> (((((fun (A0:fofType) (B0:fofType)=> (((x1 A0) B0) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))) A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))))
% Time elapsed = 7.882508s
% node=866 cost=807.000000 depth=22
% ::::::::::::::::::::::
% % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% (fun (x:ap2p) (x0:lam2p) (x1:funcext2) (x2:beta2) (A:fofType) (B:fofType) (Xf:fofType) (x3:((in Xf) ((funcSet A) B)))=> ((((((fun (A0:fofType) (B0:fofType) (x4:((in (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx)))) ((funcSet A0) B0)))=> (((((fun (A0:fofType) (B0:fofType)=> (((x1 A0) B0) (((lam A) B) (fun (Xx:fofType)=> ((((ap A) B) Xf) Xx))))) A0) B0) x4) Xf)) A) B) ((((x0 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))) x3) ((((x2 A) B) (((ap A) B) Xf)) ((((x A) B) Xf) x3))))
% % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% EOF
%------------------------------------------------------------------------------