%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEV051^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 : n108.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:40 EDT 2014 % Result : Theorem 5.89s % Output : Proof 5.89s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEV051^5 : TPTP v6.1.0. Released v4.0.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n108.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 07:45:01 CDT 2014 % % CPUTime : 5.89 % 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 0x1dc7dd0>, <kernel.Type object at 0x1dc7518>) of role type named a_type % Using role type % Declaring a:Type % FOF formula ((and (forall (Xx:a), (((eq a) Xx) Xx))) (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)))) of role conjecture named cTHM557_pme % Conjecture to prove = ((and (forall (Xx:a), (((eq a) Xx) Xx))) (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)))):Prop % Parameter a_DUMMY:a. % We need to prove ['((and (forall (Xx:a), (((eq a) Xx) Xx))) (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv))))'] % Parameter a:Type. % Trying to prove ((and (forall (Xx:a), (((eq a) Xx) Xx))) (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)))) % Found eq_ref0:=(eq_ref a):(forall (a0:a), (((eq a) a0) a0)) % Found (eq_ref a) as proof of (forall (Xx:a), (((eq a) Xx) Xx)) % Found (eq_ref a) as proof of (forall (Xx:a), (((eq a) Xx) Xx)) % Found eq_ref000:=(eq_ref00 P):((P Xu)->(P Xu)) % Found (eq_ref00 P) as proof of (P0 Xu) % Found ((eq_ref0 Xu) P) as proof of (P0 Xu) % Found (((eq_ref a) Xu) P) as proof of (P0 Xu) % Found (((eq_ref a) Xu) P) as proof of (P0 Xu) % Found eq_ref00:=(eq_ref0 Xu):(((eq a) Xu) Xu) % Found (eq_ref0 Xu) as proof of (((eq a) Xu) b) % Found ((eq_ref a) Xu) as proof of (((eq a) Xu) b) % Found ((eq_ref a) Xu) as proof of (((eq a) Xu) b) % Found ((eq_ref a) Xu) as proof of (((eq a) Xu) b) % Found eq_ref00:=(eq_ref0 b):(((eq a) b) b) % Found (eq_ref0 b) as proof of (((eq a) b) Xv) % Found ((eq_ref a) b) as proof of (((eq a) b) Xv) % Found ((eq_ref a) b) as proof of (((eq a) b) Xv) % Found ((eq_ref a) b) as proof of (((eq a) b) Xv) % Found x10:=(x1 (fun (x2:a)=> (P Xu))):((P Xu)->(P Xu)) % Found (x1 (fun (x2:a)=> (P Xu))) as proof of (P0 Xu) % Found (x1 (fun (x2:a)=> (P Xu))) as proof of (P0 Xu) % Found eq_ref00:=(eq_ref0 Xv):(((eq a) Xv) Xv) % Found (eq_ref0 Xv) as proof of (((eq a) Xv) b) % Found ((eq_ref a) Xv) as proof of (((eq a) Xv) b) % Found ((eq_ref a) Xv) as proof of (((eq a) Xv) b) % Found ((eq_ref a) Xv) as proof of (((eq a) Xv) b) % Found eq_ref00:=(eq_ref0 b):(((eq a) b) b) % Found (eq_ref0 b) as proof of (((eq a) b) Xu) % Found ((eq_ref a) b) as proof of (((eq a) b) Xu) % Found ((eq_ref a) b) as proof of (((eq a) b) Xu) % Found ((eq_ref a) b) as proof of (((eq a) b) Xu) % Found x0:(((eq a) Xu) Xw) % Found x0 as proof of (((eq a) Xu) Xw) % Found eq_ref00:=(eq_ref0 Xv):(((eq a) Xv) Xv) % Found (eq_ref0 Xv) as proof of (((eq a) Xv) Xv) % Found ((eq_ref a) Xv) as proof of (((eq a) Xv) Xv) % Found ((eq_ref a) Xv) as proof of (((eq a) Xv) Xv) % Found (x10 ((eq_ref a) Xv)) as proof of (((eq a) Xw) Xv) % Found ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv)) as proof of (((eq a) Xw) Xv) % Found ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv)) as proof of (((eq a) Xw) Xv) % Found ((eq_trans0000 x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))) as proof of (((eq a) Xu) Xv) % Found (((eq_trans000 Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))) as proof of (((eq a) Xu) Xv) % Found ((((fun (b:a)=> ((eq_trans00 b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))) as proof of (((eq a) Xu) Xv) % Found ((((fun (b:a)=> (((eq_trans0 Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))) as proof of (((eq a) Xu) Xv) % Found ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))) as proof of (((eq a) Xu) Xv) % Found (fun (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv)))) as proof of (((eq a) Xu) Xv) % Found (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv)))) as proof of ((((eq a) Xv) Xw)->(((eq a) Xu) Xv)) % Found (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv)))) as proof of ((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->(((eq a) Xu) Xv))) % Found (and_rect00 (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))))) as proof of (((eq a) Xu) Xv) % Found ((and_rect0 (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))))) as proof of (((eq a) Xu) Xv) % Found (((fun (P:Type) (x0:((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->P)))=> (((((and_rect (((eq a) Xu) Xw)) (((eq a) Xv) Xw)) P) x0) x)) (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))))) as proof of (((eq a) Xu) Xv) % Found (fun (x:((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw)))=> (((fun (P:Type) (x0:((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->P)))=> (((((and_rect (((eq a) Xu) Xw)) (((eq a) Xv) Xw)) P) x0) x)) (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv)))))) as proof of (((eq a) Xu) Xv) % Found (fun (Xw:a) (x:((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw)))=> (((fun (P:Type) (x0:((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->P)))=> (((((and_rect (((eq a) Xu) Xw)) (((eq a) Xv) Xw)) P) x0) x)) (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv)))))) as proof of (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)) % Found (fun (Xv:a) (Xw:a) (x:((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw)))=> (((fun (P:Type) (x0:((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->P)))=> (((((and_rect (((eq a) Xu) Xw)) (((eq a) Xv) Xw)) P) x0) x)) (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv)))))) as proof of (forall (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv))) % Found (fun (Xu:a) (Xv:a) (Xw:a) (x:((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw)))=> (((fun (P:Type) (x0:((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->P)))=> (((((and_rect (((eq a) Xu) Xw)) (((eq a) Xv) Xw)) P) x0) x)) (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv)))))) as proof of (forall (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv))) % Found (fun (Xu:a) (Xv:a) (Xw:a) (x:((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw)))=> (((fun (P:Type) (x0:((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->P)))=> (((((and_rect (((eq a) Xu) Xw)) (((eq a) Xv) Xw)) P) x0) x)) (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv)))))) as proof of (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv))) % Found ((conj00 (eq_ref a)) (fun (Xu:a) (Xv:a) (Xw:a) (x:((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw)))=> (((fun (P:Type) (x0:((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->P)))=> (((((and_rect (((eq a) Xu) Xw)) (((eq a) Xv) Xw)) P) x0) x)) (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))))))) as proof of ((and (forall (Xx:a), (((eq a) Xx) Xx))) (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)))) % Found (((conj0 (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)))) (eq_ref a)) (fun (Xu:a) (Xv:a) (Xw:a) (x:((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw)))=> (((fun (P:Type) (x0:((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->P)))=> (((((and_rect (((eq a) Xu) Xw)) (((eq a) Xv) Xw)) P) x0) x)) (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))))))) as proof of ((and (forall (Xx:a), (((eq a) Xx) Xx))) (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)))) % Found ((((conj (forall (Xx:a), (((eq a) Xx) Xx))) (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)))) (eq_ref a)) (fun (Xu:a) (Xv:a) (Xw:a) (x:((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw)))=> (((fun (P:Type) (x0:((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->P)))=> (((((and_rect (((eq a) Xu) Xw)) (((eq a) Xv) Xw)) P) x0) x)) (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))))))) as proof of ((and (forall (Xx:a), (((eq a) Xx) Xx))) (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)))) % Found ((((conj (forall (Xx:a), (((eq a) Xx) Xx))) (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)))) (eq_ref a)) (fun (Xu:a) (Xv:a) (Xw:a) (x:((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw)))=> (((fun (P:Type) (x0:((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->P)))=> (((((and_rect (((eq a) Xu) Xw)) (((eq a) Xv) Xw)) P) x0) x)) (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))))))) as proof of ((and (forall (Xx:a), (((eq a) Xx) Xx))) (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)))) % Got proof ((((conj (forall (Xx:a), (((eq a) Xx) Xx))) (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)))) (eq_ref a)) (fun (Xu:a) (Xv:a) (Xw:a) (x:((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw)))=> (((fun (P:Type) (x0:((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->P)))=> (((((and_rect (((eq a) Xu) Xw)) (((eq a) Xv) Xw)) P) x0) x)) (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))))))) % Time elapsed = 5.543938s % node=858 cost=730.000000 depth=25 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % ((((conj (forall (Xx:a), (((eq a) Xx) Xx))) (forall (Xu:a) (Xv:a) (Xw:a), (((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw))->(((eq a) Xu) Xv)))) (eq_ref a)) (fun (Xu:a) (Xv:a) (Xw:a) (x:((and (((eq a) Xu) Xw)) (((eq a) Xv) Xw)))=> (((fun (P:Type) (x0:((((eq a) Xu) Xw)->((((eq a) Xv) Xw)->P)))=> (((((and_rect (((eq a) Xu) Xw)) (((eq a) Xv) Xw)) P) x0) x)) (((eq a) Xu) Xv)) (fun (x0:(((eq a) Xu) Xw)) (x1:(((eq a) Xv) Xw))=> ((((fun (b:a)=> ((((eq_trans a) Xu) b) Xv)) Xw) x0) ((x1 (fun (x3:a)=> (((eq a) x3) Xv))) ((eq_ref a) Xv))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------