%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU545^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 : n103.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:25 EDT 2014 % Result : Theorem 2.59s % Output : Proof 2.59s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU545^2 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n103.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:37:16 CDT 2014 % % CPUTime : 2.59 % 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 0xd07cf8>, <kernel.DependentProduct object at 0xd07cb0>) of role type named exu_type % Using role type % Declaring exu:((fofType->Prop)->Prop) % FOF formula (((eq ((fofType->Prop)->Prop)) exu) (fun (Xphi:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))))) of role definition named exu % A new definition: (((eq ((fofType->Prop)->Prop)) exu) (fun (Xphi:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))))) % Defined: exu:=(fun (Xphi:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy))))))) % FOF formula (<kernel.Constant object at 0xd07cf8>, <kernel.Sort object at 0xbe7710>) of role type named exuI1_type % Using role type % Declaring exuI1:Prop % FOF formula (((eq Prop) exuI1) (forall (Xphi:(fofType->Prop)), (((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy))))))->(exu (fun (Xx:fofType)=> (Xphi Xx)))))) of role definition named exuI1 % A new definition: (((eq Prop) exuI1) (forall (Xphi:(fofType->Prop)), (((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy))))))->(exu (fun (Xx:fofType)=> (Xphi Xx)))))) % Defined: exuI1:=(forall (Xphi:(fofType->Prop)), (((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy))))))->(exu (fun (Xx:fofType)=> (Xphi Xx))))) % FOF formula (exuI1->(forall (Xphi:(fofType->Prop)), (((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))->((forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy))))->(exu (fun (Xx:fofType)=> (Xphi Xx))))))) of role conjecture named exuI3 % Conjecture to prove = (exuI1->(forall (Xphi:(fofType->Prop)), (((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))->((forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy))))->(exu (fun (Xx:fofType)=> (Xphi Xx))))))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(exuI1->(forall (Xphi:(fofType->Prop)), (((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))->((forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy))))->(exu (fun (Xx:fofType)=> (Xphi Xx)))))))'] % Parameter fofType:Type. % Definition exu:=(fun (Xphi:(fofType->Prop))=> ((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy))))))):((fofType->Prop)->Prop). % Definition exuI1:=(forall (Xphi:(fofType->Prop)), (((ex fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy))))))->(exu (fun (Xx:fofType)=> (Xphi Xx))))):Prop. % Trying to prove (exuI1->(forall (Xphi:(fofType->Prop)), (((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))->((forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy))))->(exu (fun (Xx:fofType)=> (Xphi Xx))))))) % Found x3:(Xphi x2) % Instantiate: x4:=x2:fofType % Found x3 as proof of (Xphi x4) % Found eq_ref00:=(eq_ref0 x2):(((eq fofType) x2) x2) % Found (eq_ref0 x2) as proof of (((eq fofType) x2) Xy) % Found ((eq_ref fofType) x2) as proof of (((eq fofType) x2) Xy) % Found ((eq_ref fofType) x2) as proof of (((eq fofType) x2) Xy) % Found (fun (x00:(Xphi Xy))=> ((eq_ref fofType) x2)) as proof of (((eq fofType) x2) Xy) % Found eq_ref00:=(eq_ref0 x4):(((eq fofType) x4) x4) % Found (eq_ref0 x4) as proof of (((eq fofType) x4) Xy) % Found ((eq_ref fofType) x4) as proof of (((eq fofType) x4) Xy) % Found ((eq_ref fofType) x4) as proof of (((eq fofType) x4) Xy) % Found (fun (x00:(Xphi Xy))=> ((eq_ref fofType) x4)) as proof of (((eq fofType) x4) Xy) % Found x5:(P x4) % Instantiate: x4:=Xy:fofType % Found (fun (x5:(P x4))=> x5) as proof of (P Xy) % Found (fun (P:(fofType->Prop)) (x5:(P x4))=> x5) as proof of ((P x4)->(P Xy)) % Found (fun (x00:(Xphi Xy)) (P:(fofType->Prop)) (x5:(P x4))=> x5) as proof of (((eq fofType) x4) Xy) % Found eq_ref000:=(eq_ref00 P):((P x4)->(P x4)) % Found (eq_ref00 P) as proof of ((P x4)->(P Xy)) % Found ((eq_ref0 x4) P) as proof of ((P x4)->(P Xy)) % Found (((eq_ref fofType) x4) P) as proof of ((P x4)->(P Xy)) % Found (((eq_ref fofType) x4) P) as proof of ((P x4)->(P Xy)) % Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) x4) P)) as proof of ((P x4)->(P Xy)) % Found (fun (x00:(Xphi Xy)) (P:(fofType->Prop))=> (((eq_ref fofType) x4) P)) as proof of (((eq fofType) x4) Xy) % Found x4:(Xphi x3) % Instantiate: x2:=x3:fofType % Found x4 as proof of (Xphi x2) % Found eq_ref000:=(eq_ref00 P):((P x2)->(P x2)) % Found (eq_ref00 P) as proof of ((P x2)->(P Xy)) % Found ((eq_ref0 x2) P) as proof of ((P x2)->(P Xy)) % Found (((eq_ref fofType) x2) P) as proof of ((P x2)->(P Xy)) % Found (((eq_ref fofType) x2) P) as proof of ((P x2)->(P Xy)) % Found (fun (P:(fofType->Prop))=> (((eq_ref fofType) x2) P)) as proof of ((P x2)->(P Xy)) % Found (fun (x00:(Xphi Xy)) (P:(fofType->Prop))=> (((eq_ref fofType) x2) P)) as proof of (((eq fofType) x2) Xy) % Found x3:(P x2) % Instantiate: x2:=Xy:fofType % Found (fun (x3:(P x2))=> x3) as proof of (P Xy) % Found (fun (P:(fofType->Prop)) (x3:(P x2))=> x3) as proof of ((P x2)->(P Xy)) % Found (fun (x00:(Xphi Xy)) (P:(fofType->Prop)) (x3:(P x2))=> x3) as proof of (((eq fofType) x2) Xy) % Found x1000:=(x100 Xy):((Xphi Xy)->(((eq fofType) x4) Xy)) % Found (x100 Xy) as proof of ((Xphi Xy)->(((eq fofType) x4) Xy)) % Found ((fun (Xy0:fofType)=> ((x10 Xy0) x3)) Xy) as proof of ((Xphi Xy)->(((eq fofType) x4) Xy)) % Found ((fun (Xy0:fofType)=> (((x1 x4) Xy0) x3)) Xy) as proof of ((Xphi Xy)->(((eq fofType) x4) Xy)) % Found (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x4) Xy0) x3)) Xy)) as proof of ((Xphi Xy)->(((eq fofType) x4) Xy)) % Found (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x4) Xy0) x3)) Xy)) as proof of (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x4) Xy))) % Found ((conj00 x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x4) Xy0) x3)) Xy))) as proof of ((and (Xphi x4)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x4) Xy)))) % Found (((conj0 (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x4) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x4) Xy0) x3)) Xy))) as proof of ((and (Xphi x4)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x4) Xy)))) % Found ((((conj (Xphi x4)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x4) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x4) Xy0) x3)) Xy))) as proof of ((and (Xphi x4)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x4) Xy)))) % Found ((((conj (Xphi x4)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x4) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x4) Xy0) x3)) Xy))) as proof of ((and (Xphi x4)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x4) Xy)))) % Found (ex_intro000 ((((conj (Xphi x4)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x4) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x4) Xy0) x3)) Xy)))) as proof of (exu (fun (Xx:fofType)=> (Xphi Xx))) % Found ((ex_intro00 x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy)))) as proof of (exu (fun (Xx:fofType)=> (Xphi Xx))) % Found (((ex_intro0 (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy)))) as proof of (exu (fun (Xx:fofType)=> (Xphi Xx))) % Found ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy)))) as proof of (exu (fun (Xx:fofType)=> (Xphi Xx))) % Found (fun (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy))))) as proof of (exu (fun (Xx:fofType)=> (Xphi Xx))) % Found (fun (x2:fofType) (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy))))) as proof of ((Xphi x2)->(exu (fun (Xx:fofType)=> (Xphi Xx)))) % Found (fun (x2:fofType) (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy))))) as proof of (forall (x:fofType), ((Xphi x)->(exu (fun (Xx:fofType)=> (Xphi Xx))))) % Found (ex_ind00 (fun (x2:fofType) (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy)))))) as proof of (exu (fun (Xx:fofType)=> (Xphi Xx))) % Found ((ex_ind0 (exu (fun (Xx:fofType)=> (Xphi Xx)))) (fun (x2:fofType) (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy)))))) as proof of (exu (fun (Xx:fofType)=> (Xphi Xx))) % Found (((fun (P:Prop) (x2:(forall (x:fofType), ((Xphi x)->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> (Xphi Xx))) P) x2) x0)) (exu (fun (Xx:fofType)=> (Xphi Xx)))) (fun (x2:fofType) (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy)))))) as proof of (exu (fun (Xx:fofType)=> (Xphi Xx))) % Found (fun (x1:(forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy)))))=> (((fun (P:Prop) (x2:(forall (x:fofType), ((Xphi x)->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> (Xphi Xx))) P) x2) x0)) (exu (fun (Xx:fofType)=> (Xphi Xx)))) (fun (x2:fofType) (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy))))))) as proof of (exu (fun (Xx:fofType)=> (Xphi Xx))) % Found (fun (x0:((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))) (x1:(forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy)))))=> (((fun (P:Prop) (x2:(forall (x:fofType), ((Xphi x)->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> (Xphi Xx))) P) x2) x0)) (exu (fun (Xx:fofType)=> (Xphi Xx)))) (fun (x2:fofType) (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy))))))) as proof of ((forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy))))->(exu (fun (Xx:fofType)=> (Xphi Xx)))) % Found (fun (Xphi:(fofType->Prop)) (x0:((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))) (x1:(forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy)))))=> (((fun (P:Prop) (x2:(forall (x:fofType), ((Xphi x)->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> (Xphi Xx))) P) x2) x0)) (exu (fun (Xx:fofType)=> (Xphi Xx)))) (fun (x2:fofType) (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy))))))) as proof of (((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))->((forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy))))->(exu (fun (Xx:fofType)=> (Xphi Xx))))) % Found (fun (x:exuI1) (Xphi:(fofType->Prop)) (x0:((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))) (x1:(forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy)))))=> (((fun (P:Prop) (x2:(forall (x:fofType), ((Xphi x)->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> (Xphi Xx))) P) x2) x0)) (exu (fun (Xx:fofType)=> (Xphi Xx)))) (fun (x2:fofType) (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy))))))) as proof of (forall (Xphi:(fofType->Prop)), (((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))->((forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy))))->(exu (fun (Xx:fofType)=> (Xphi Xx)))))) % Found (fun (x:exuI1) (Xphi:(fofType->Prop)) (x0:((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))) (x1:(forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy)))))=> (((fun (P:Prop) (x2:(forall (x:fofType), ((Xphi x)->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> (Xphi Xx))) P) x2) x0)) (exu (fun (Xx:fofType)=> (Xphi Xx)))) (fun (x2:fofType) (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy))))))) as proof of (exuI1->(forall (Xphi:(fofType->Prop)), (((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))->((forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy))))->(exu (fun (Xx:fofType)=> (Xphi Xx))))))) % Got proof (fun (x:exuI1) (Xphi:(fofType->Prop)) (x0:((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))) (x1:(forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy)))))=> (((fun (P:Prop) (x2:(forall (x:fofType), ((Xphi x)->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> (Xphi Xx))) P) x2) x0)) (exu (fun (Xx:fofType)=> (Xphi Xx)))) (fun (x2:fofType) (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy))))))) % Time elapsed = 2.256787s % node=389 cost=577.000000 depth=23 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:exuI1) (Xphi:(fofType->Prop)) (x0:((ex fofType) (fun (Xx:fofType)=> (Xphi Xx)))) (x1:(forall (Xx:fofType) (Xy:fofType), ((Xphi Xx)->((Xphi Xy)->(((eq fofType) Xx) Xy)))))=> (((fun (P:Prop) (x2:(forall (x:fofType), ((Xphi x)->P)))=> (((((ex_ind fofType) (fun (Xx:fofType)=> (Xphi Xx))) P) x2) x0)) (exu (fun (Xx:fofType)=> (Xphi Xx)))) (fun (x2:fofType) (x3:(Xphi x2))=> ((((ex_intro fofType) (fun (Xx:fofType)=> ((and (Xphi Xx)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) Xx) Xy)))))) x2) ((((conj (Xphi x2)) (forall (Xy:fofType), ((Xphi Xy)->(((eq fofType) x2) Xy)))) x3) (fun (Xy:fofType)=> ((fun (Xy0:fofType)=> (((x1 x2) Xy0) x3)) Xy))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------