↑ Up

cocATP---0.2.0.THM-Prf.s

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

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

% Comments : 
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % Problem  : SEU888^5 : TPTP v6.1.0. Released v4.0.0.
% % Command  : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p
% % Computer : n091.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:40:51 CDT 2014
% % CPUTime  : 9.91 
% 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 0x1b4fdd0>, <kernel.Type object at 0x1b4f3f8>) of role type named b_type
% Using role type
% Declaring b:Type
% FOF formula (<kernel.Constant object at 0x1f27248>, <kernel.Type object at 0x1b4fb48>) of role type named a_type
% Using role type
% Declaring a:Type
% FOF formula (<kernel.Constant object at 0x1b4f8c0>, <kernel.DependentProduct object at 0x1b4f758>) of role type named g
% Using role type
% Declaring g:(b->a)
% FOF formula (<kernel.Constant object at 0x1b4f3f8>, <kernel.Constant object at 0x1b4f758>) of role type named z
% Using role type
% Declaring z:a
% FOF formula (<kernel.Constant object at 0x1b4f488>, <kernel.Constant object at 0x1b4f758>) of role type named y
% Using role type
% Declaring y:b
% FOF formula (<kernel.Constant object at 0x1b4f8c0>, <kernel.Constant object at 0x1b4f758>) of role type named x
% Using role type
% Declaring x:b
% FOF formula (((or (((eq a) z) (g x))) (((eq a) z) (g y)))->((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))) of role conjecture named cTHM500C_WFF_pme
% Conjecture to prove = (((or (((eq a) z) (g x))) (((eq a) z) (g y)))->((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))):Prop
% We need to prove ['(((or (((eq a) z) (g x))) (((eq a) z) (g y)))->((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))))']
% Parameter b:Type.
% Parameter a:Type.
% Parameter g:(b->a).
% Parameter z:a.
% Parameter y:b.
% Parameter x:b.
% Trying to prove (((or (((eq a) z) (g x))) (((eq a) z) (g y)))->((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))))
% Found eq_ref00:=(eq_ref0 x00):(((eq b) x00) x00)
% Found (eq_ref0 x00) as proof of (((eq b) x00) y)
% Found ((eq_ref b) x00) as proof of (((eq b) x00) y)
% Found ((eq_ref b) x00) as proof of (((eq b) x00) y)
% Found ((eq_ref b) x00) as proof of (((eq b) x00) y)
% Found (or_intror00 ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found ((or_intror0 (((eq b) x00) y)) ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found (((or_intror (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found (((or_intror (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found eq_substitution00000:=(eq_substitution0000 (fun (x3:a)=> x3)):((((eq a) z) (g y))->(((eq a) z) (g y)))
% Found (eq_substitution0000 (fun (x3:a)=> x3)) as proof of ((((eq a) z) (g y))->(((eq a) z) (g x00)))
% Found ((eq_substitution000 (g y)) (fun (x3:a)=> x3)) as proof of ((((eq a) z) (g y))->(((eq a) z) (g x00)))
% Found (((eq_substitution00 z) (g y)) (fun (x3:a)=> x3)) as proof of ((((eq a) z) (g y))->(((eq a) z) (g x00)))
% Found ((((eq_substitution0 a) z) (g y)) (fun (x3:a)=> x3)) as proof of ((((eq a) z) (g y))->(((eq a) z) (g x00)))
% Found (((((eq_substitution a) a) z) (g y)) (fun (x3:a)=> x3)) as proof of ((((eq a) z) (g y))->(((eq a) z) (g x00)))
% Found (((((eq_substitution a) a) z) (g y)) (fun (x3:a)=> x3)) as proof of ((((eq a) z) (g y))->(((eq a) z) (g x00)))
% Found x01:(((eq a) z) (g x))
% Instantiate: x00:=x:b
% Found (fun (x01:(((eq a) z) (g x)))=> x01) as proof of (((eq a) z) (g x00))
% Found (fun (x01:(((eq a) z) (g x)))=> x01) as proof of ((((eq a) z) (g x))->(((eq a) z) (g x00)))
% Found x01:(((eq a) z) (g y))
% Instantiate: x00:=y:b
% Found (fun (x01:(((eq a) z) (g y)))=> x01) as proof of (((eq a) z) (g x00))
% Found (fun (x01:(((eq a) z) (g y)))=> x01) as proof of ((((eq a) z) (g y))->(((eq a) z) (g x00)))
% Found x01:(((eq a) z) (g y))
% Instantiate: x00:=y:b
% Found x01 as proof of (((eq a) z) (g x00))
% Found x01:(((eq a) z) (g x))
% Instantiate: x00:=x:b
% Found x01 as proof of (((eq a) z) (g x00))
% Found x0100:=(x010 x1):(P (g y))
% Found (x010 x1) as proof of (P (g x00))
% Found ((x01 P) x1) as proof of (P (g x00))
% Found (fun (x01:(((eq a) z) (g y)))=> ((x01 P) x1)) as proof of (P (g x00))
% Found (fun (x01:(((eq a) z) (g y)))=> ((x01 P) x1)) as proof of ((((eq a) z) (g y))->(P (g x00)))
% Found eq_sym010:=(eq_sym01 (g y)):((((eq a) z) (g y))->(((eq a) (g y)) z))
% Found (eq_sym01 (g y)) as proof of ((((eq a) z) (g y))->(((eq a) (g x00)) z))
% Found ((eq_sym0 z) (g y)) as proof of ((((eq a) z) (g y))->(((eq a) (g x00)) z))
% Found ((eq_sym0 z) (g y)) as proof of ((((eq a) z) (g y))->(((eq a) (g x00)) z))
% Found x00:(((eq a) z) (g x))
% Instantiate: x01:=x:b
% Found x00 as proof of (((eq a) z) (g x01))
% Found x00:(((eq a) z) (g y))
% Instantiate: x01:=y:b
% Found x00 as proof of (((eq a) z) (g x01))
% Found eq_sym010:=(eq_sym01 (g y)):((((eq a) z) (g y))->(((eq a) (g y)) z))
% Found (eq_sym01 (g y)) as proof of ((((eq a) z) (g y))->(((eq a) (g x00)) z))
% Found ((eq_sym0 z) (g y)) as proof of ((((eq a) z) (g y))->(((eq a) (g x00)) z))
% Found ((eq_sym0 z) (g y)) as proof of ((((eq a) z) (g y))->(((eq a) (g x00)) z))
% Found ((eq_sym0 z) (g y)) as proof of ((((eq a) z) (g y))->(((eq a) (g x00)) z))
% Found eq_sym010:=(eq_sym01 (g x)):((((eq a) z) (g x))->(((eq a) (g x)) z))
% Found (eq_sym01 (g x)) as proof of ((((eq a) z) (g x))->(((eq a) (g x00)) z))
% Found ((eq_sym0 z) (g x)) as proof of ((((eq a) z) (g x))->(((eq a) (g x00)) z))
% Found ((eq_sym0 z) (g x)) as proof of ((((eq a) z) (g x))->(((eq a) (g x00)) z))
% Found ((eq_sym0 z) (g x)) as proof of ((((eq a) z) (g x))->(((eq a) (g x00)) z))
% Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))):(((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) (fun (x0:b)=> ((and ((or (((eq b) x0) x)) (((eq b) x0) y))) (((eq a) z) (g x0)))))
% Found (eta_expansion_dep00 (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) b0)
% Found ((eta_expansion_dep0 (fun (x2:b)=> Prop)) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) b0)
% Found (((eta_expansion_dep b) (fun (x2:b)=> Prop)) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) b0)
% Found (((eta_expansion_dep b) (fun (x2:b)=> Prop)) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) b0)
% Found (((eta_expansion_dep b) (fun (x2:b)=> Prop)) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) as proof of (((eq (b->Prop)) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) b0)
% Found eq_ref00:=(eq_ref0 x00):(((eq b) x00) x00)
% Found (eq_ref0 x00) as proof of (((eq b) x00) y)
% Found ((eq_ref b) x00) as proof of (((eq b) x00) y)
% Found ((eq_ref b) x00) as proof of (((eq b) x00) y)
% Found (or_intror00 ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found ((or_intror0 (((eq b) x00) y)) ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found (((or_intror (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found (((or_intror (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found (conj00 (((or_intror (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00))) as proof of ((((eq a) z) (g y))->((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found ((conj0 (((eq a) z) (g y))) (((or_intror (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00))) as proof of ((((eq a) z) (g y))->((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found (((conj ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g y))) (((or_intror (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00))) as proof of ((((eq a) z) (g y))->((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found (((conj ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g y))) (((or_intror (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00))) as proof of ((((eq a) z) (g y))->((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found (((conj ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g y))) (((or_intror (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00))) as proof of ((((eq a) z) (g y))->((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found eq_ref00:=(eq_ref0 x00):(((eq b) x00) x00)
% Found (eq_ref0 x00) as proof of (((eq b) x00) x)
% Found ((eq_ref b) x00) as proof of (((eq b) x00) x)
% Found ((eq_ref b) x00) as proof of (((eq b) x00) x)
% Found (or_introl00 ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found ((or_introl0 (((eq b) x00) y)) ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found (((or_introl (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found (((or_introl (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found (conj00 (((or_introl (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00))) as proof of ((((eq a) z) (g x))->((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found ((conj0 (((eq a) z) (g x))) (((or_introl (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00))) as proof of ((((eq a) z) (g x))->((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found (((conj ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00))) as proof of ((((eq a) z) (g x))->((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found (((conj ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00))) as proof of ((((eq a) z) (g x))->((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found (((conj ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00))) as proof of ((((eq a) z) (g x))->((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found eq_ref00:=(eq_ref0 x00):(((eq b) x00) x00)
% Found (eq_ref0 x00) as proof of (((eq b) x00) y)
% Found ((eq_ref b) x00) as proof of (((eq b) x00) y)
% Found ((eq_ref b) x00) as proof of (((eq b) x00) y)
% Found (or_intror00 ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found ((or_intror0 (((eq b) x00) y)) ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found (((or_intror (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found (((or_intror (((eq b) x00) x)) (((eq b) x00) y)) ((eq_ref b) x00)) as proof of ((or (((eq b) x00) x)) (((eq b) x00) y))
% Found eq_ref00:=(eq_ref0 (f x00)):(((eq Prop) (f x00)) (f x00))
% Found (eq_ref0 (f x00)) as proof of (((eq Prop) (f x00)) ((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found ((eq_ref Prop) (f x00)) as proof of (((eq Prop) (f x00)) ((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found ((eq_ref Prop) (f x00)) as proof of (((eq Prop) (f x00)) ((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found (fun (x00:b)=> ((eq_ref Prop) (f x00))) as proof of (((eq Prop) (f x00)) ((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found (fun (x00:b)=> ((eq_ref Prop) (f x00))) as proof of (forall (x0:b), (((eq Prop) (f x0)) ((and ((or (((eq b) x0) x)) (((eq b) x0) y))) (((eq a) z) (g x0)))))
% Found eq_ref00:=(eq_ref0 (f x00)):(((eq Prop) (f x00)) (f x00))
% Found (eq_ref0 (f x00)) as proof of (((eq Prop) (f x00)) ((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found ((eq_ref Prop) (f x00)) as proof of (((eq Prop) (f x00)) ((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found ((eq_ref Prop) (f x00)) as proof of (((eq Prop) (f x00)) ((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found (fun (x00:b)=> ((eq_ref Prop) (f x00))) as proof of (((eq Prop) (f x00)) ((and ((or (((eq b) x00) x)) (((eq b) x00) y))) (((eq a) z) (g x00))))
% Found (fun (x00:b)=> ((eq_ref Prop) (f x00))) as proof of (forall (x0:b), (((eq Prop) (f x0)) ((and ((or (((eq b) x0) x)) (((eq b) x0) y))) (((eq a) z) (g x0)))))
% Found eq_ref00:=(eq_ref0 x01):(((eq b) x01) x01)
% Found (eq_ref0 x01) as proof of (((eq b) x01) x)
% Found ((eq_ref b) x01) as proof of (((eq b) x01) x)
% Found ((eq_ref b) x01) as proof of (((eq b) x01) x)
% Found (or_introl00 ((eq_ref b) x01)) as proof of ((or (((eq b) x01) x)) (((eq b) x01) y))
% Found ((or_introl0 (((eq b) x01) y)) ((eq_ref b) x01)) as proof of ((or (((eq b) x01) x)) (((eq b) x01) y))
% Found (((or_introl (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01)) as proof of ((or (((eq b) x01) x)) (((eq b) x01) y))
% Found (((or_introl (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01)) as proof of ((or (((eq b) x01) x)) (((eq b) x01) y))
% Found ((conj00 (((or_introl (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01))) x00) as proof of ((and ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01)))
% Found (((conj0 (((eq a) z) (g x01))) (((or_introl (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01))) x00) as proof of ((and ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01)))
% Found ((((conj ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01))) (((or_introl (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01))) x00) as proof of ((and ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01)))
% Found ((((conj ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01))) (((or_introl (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01))) x00) as proof of ((and ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01)))
% Found (ex_intro000 ((((conj ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01))) (((or_introl (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01))) x00)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found ((ex_intro00 x) ((((conj ((or (((eq b) x) x)) (((eq b) x) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x) x)) (((eq b) x) y)) ((eq_ref b) x))) x00)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found (((ex_intro0 (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) x) ((((conj ((or (((eq b) x) x)) (((eq b) x) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x) x)) (((eq b) x) y)) ((eq_ref b) x))) x00)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) x) ((((conj ((or (((eq b) x) x)) (((eq b) x) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x) x)) (((eq b) x) y)) ((eq_ref b) x))) x00)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found (fun (x00:(((eq a) z) (g x)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) x) ((((conj ((or (((eq b) x) x)) (((eq b) x) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x) x)) (((eq b) x) y)) ((eq_ref b) x))) x00))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found (fun (x00:(((eq a) z) (g x)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) x) ((((conj ((or (((eq b) x) x)) (((eq b) x) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x) x)) (((eq b) x) y)) ((eq_ref b) x))) x00))) as proof of ((((eq a) z) (g x))->((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))))
% Found eq_ref00:=(eq_ref0 x01):(((eq b) x01) x01)
% Found (eq_ref0 x01) as proof of (((eq b) x01) y)
% Found ((eq_ref b) x01) as proof of (((eq b) x01) y)
% Found ((eq_ref b) x01) as proof of (((eq b) x01) y)
% Found (or_intror00 ((eq_ref b) x01)) as proof of ((or (((eq b) x01) x)) (((eq b) x01) y))
% Found ((or_intror0 (((eq b) x01) y)) ((eq_ref b) x01)) as proof of ((or (((eq b) x01) x)) (((eq b) x01) y))
% Found (((or_intror (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01)) as proof of ((or (((eq b) x01) x)) (((eq b) x01) y))
% Found (((or_intror (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01)) as proof of ((or (((eq b) x01) x)) (((eq b) x01) y))
% Found ((conj00 (((or_intror (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01))) x00) as proof of ((and ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01)))
% Found (((conj0 (((eq a) z) (g x01))) (((or_intror (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01))) x00) as proof of ((and ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01)))
% Found ((((conj ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01))) (((or_intror (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01))) x00) as proof of ((and ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01)))
% Found ((((conj ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01))) (((or_intror (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01))) x00) as proof of ((and ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01)))
% Found (ex_intro000 ((((conj ((or (((eq b) x01) x)) (((eq b) x01) y))) (((eq a) z) (g x01))) (((or_intror (((eq b) x01) x)) (((eq b) x01) y)) ((eq_ref b) x01))) x00)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found ((ex_intro00 y) ((((conj ((or (((eq b) y) x)) (((eq b) y) y))) (((eq a) z) (g y))) (((or_intror (((eq b) y) x)) (((eq b) y) y)) ((eq_ref b) y))) x00)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found (((ex_intro0 (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) y) ((((conj ((or (((eq b) y) x)) (((eq b) y) y))) (((eq a) z) (g y))) (((or_intror (((eq b) y) x)) (((eq b) y) y)) ((eq_ref b) y))) x00)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) y) ((((conj ((or (((eq b) y) x)) (((eq b) y) y))) (((eq a) z) (g y))) (((or_intror (((eq b) y) x)) (((eq b) y) y)) ((eq_ref b) y))) x00)) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found (fun (x00:(((eq a) z) (g y)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) y) ((((conj ((or (((eq b) y) x)) (((eq b) y) y))) (((eq a) z) (g y))) (((or_intror (((eq b) y) x)) (((eq b) y) y)) ((eq_ref b) y))) x00))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found (fun (x00:(((eq a) z) (g y)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) y) ((((conj ((or (((eq b) y) x)) (((eq b) y) y))) (((eq a) z) (g y))) (((or_intror (((eq b) y) x)) (((eq b) y) y)) ((eq_ref b) y))) x00))) as proof of ((((eq a) z) (g y))->((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))))
% Found ((or_ind00 (fun (x00:(((eq a) z) (g x)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) x) ((((conj ((or (((eq b) x) x)) (((eq b) x) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x) x)) (((eq b) x) y)) ((eq_ref b) x))) x00)))) (fun (x00:(((eq a) z) (g y)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) y) ((((conj ((or (((eq b) y) x)) (((eq b) y) y))) (((eq a) z) (g y))) (((or_intror (((eq b) y) x)) (((eq b) y) y)) ((eq_ref b) y))) x00)))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found (((or_ind0 ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))) (fun (x00:(((eq a) z) (g x)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) x) ((((conj ((or (((eq b) x) x)) (((eq b) x) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x) x)) (((eq b) x) y)) ((eq_ref b) x))) x00)))) (fun (x00:(((eq a) z) (g y)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) y) ((((conj ((or (((eq b) y) x)) (((eq b) y) y))) (((eq a) z) (g y))) (((or_intror (((eq b) y) x)) (((eq b) y) y)) ((eq_ref b) y))) x00)))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found ((((fun (P:Prop) (x1:((((eq a) z) (g x))->P)) (x2:((((eq a) z) (g y))->P))=> ((((((or_ind (((eq a) z) (g x))) (((eq a) z) (g y))) P) x1) x2) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))) (fun (x00:(((eq a) z) (g x)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) x) ((((conj ((or (((eq b) x) x)) (((eq b) x) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x) x)) (((eq b) x) y)) ((eq_ref b) x))) x00)))) (fun (x00:(((eq a) z) (g y)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) y) ((((conj ((or (((eq b) y) x)) (((eq b) y) y))) (((eq a) z) (g y))) (((or_intror (((eq b) y) x)) (((eq b) y) y)) ((eq_ref b) y))) x00)))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found (fun (x0:((or (((eq a) z) (g x))) (((eq a) z) (g y))))=> ((((fun (P:Prop) (x1:((((eq a) z) (g x))->P)) (x2:((((eq a) z) (g y))->P))=> ((((((or_ind (((eq a) z) (g x))) (((eq a) z) (g y))) P) x1) x2) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))) (fun (x00:(((eq a) z) (g x)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) x) ((((conj ((or (((eq b) x) x)) (((eq b) x) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x) x)) (((eq b) x) y)) ((eq_ref b) x))) x00)))) (fun (x00:(((eq a) z) (g y)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) y) ((((conj ((or (((eq b) y) x)) (((eq b) y) y))) (((eq a) z) (g y))) (((or_intror (((eq b) y) x)) (((eq b) y) y)) ((eq_ref b) y))) x00))))) as proof of ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))
% Found (fun (x0:((or (((eq a) z) (g x))) (((eq a) z) (g y))))=> ((((fun (P:Prop) (x1:((((eq a) z) (g x))->P)) (x2:((((eq a) z) (g y))->P))=> ((((((or_ind (((eq a) z) (g x))) (((eq a) z) (g y))) P) x1) x2) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))) (fun (x00:(((eq a) z) (g x)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) x) ((((conj ((or (((eq b) x) x)) (((eq b) x) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x) x)) (((eq b) x) y)) ((eq_ref b) x))) x00)))) (fun (x00:(((eq a) z) (g y)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) y) ((((conj ((or (((eq b) y) x)) (((eq b) y) y))) (((eq a) z) (g y))) (((or_intror (((eq b) y) x)) (((eq b) y) y)) ((eq_ref b) y))) x00))))) as proof of (((or (((eq a) z) (g x))) (((eq a) z) (g y)))->((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))))
% Got proof (fun (x0:((or (((eq a) z) (g x))) (((eq a) z) (g y))))=> ((((fun (P:Prop) (x1:((((eq a) z) (g x))->P)) (x2:((((eq a) z) (g y))->P))=> ((((((or_ind (((eq a) z) (g x))) (((eq a) z) (g y))) P) x1) x2) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))) (fun (x00:(((eq a) z) (g x)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) x) ((((conj ((or (((eq b) x) x)) (((eq b) x) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x) x)) (((eq b) x) y)) ((eq_ref b) x))) x00)))) (fun (x00:(((eq a) z) (g y)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) y) ((((conj ((or (((eq b) y) x)) (((eq b) y) y))) (((eq a) z) (g y))) (((or_intror (((eq b) y) x)) (((eq b) y) y)) ((eq_ref b) y))) x00)))))
% Time elapsed = 9.511568s
% node=1486 cost=476.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 (x0:((or (((eq a) z) (g x))) (((eq a) z) (g y))))=> ((((fun (P:Prop) (x1:((((eq a) z) (g x))->P)) (x2:((((eq a) z) (g y))->P))=> ((((((or_ind (((eq a) z) (g x))) (((eq a) z) (g y))) P) x1) x2) x0)) ((ex b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt)))))) (fun (x00:(((eq a) z) (g x)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) x) ((((conj ((or (((eq b) x) x)) (((eq b) x) y))) (((eq a) z) (g x))) (((or_introl (((eq b) x) x)) (((eq b) x) y)) ((eq_ref b) x))) x00)))) (fun (x00:(((eq a) z) (g y)))=> ((((ex_intro b) (fun (Xt:b)=> ((and ((or (((eq b) Xt) x)) (((eq b) Xt) y))) (((eq a) z) (g Xt))))) y) ((((conj ((or (((eq b) y) x)) (((eq b) y) y))) (((eq a) z) (g y))) (((or_intror (((eq b) y) x)) (((eq b) y) y)) ((eq_ref b) y))) x00)))))
% % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% EOF
%------------------------------------------------------------------------------