%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU505^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 : n110.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:19 EDT 2014 % Result : Theorem 15.71s % Output : Proof 15.71s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU505^2 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n110.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:25:56 CDT 2014 % % CPUTime : 15.71 % 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 0x1631440>, <kernel.DependentProduct object at 0x1769710>) of role type named in_type % Using role type % Declaring in:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x1b9a878>, <kernel.Sort object at 0x19fc878>) of role type named setextAx_type % Using role type % Declaring setextAx:Prop % FOF formula (((eq Prop) setextAx) (forall (A:fofType) (B:fofType), ((forall (Xx:fofType), ((iff ((in Xx) A)) ((in Xx) B)))->(((eq fofType) A) B)))) of role definition named setextAx % A new definition: (((eq Prop) setextAx) (forall (A:fofType) (B:fofType), ((forall (Xx:fofType), ((iff ((in Xx) A)) ((in Xx) B)))->(((eq fofType) A) B)))) % Defined: setextAx:=(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), ((iff ((in Xx) A)) ((in Xx) B)))->(((eq fofType) A) B))) % FOF formula (setextAx->(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B))))) of role conjecture named setext % Conjecture to prove = (setextAx->(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B))))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(setextAx->(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B)))))'] % Parameter fofType:Type. % Parameter in:(fofType->(fofType->Prop)). % Definition setextAx:=(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), ((iff ((in Xx) A)) ((in Xx) B)))->(((eq fofType) A) B))):Prop. % Trying to prove (setextAx->(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B))))) % Found x30:(P A) % Found (fun (x30:(P A))=> x30) as proof of (P A) % Found (fun (x30:(P A))=> x30) as proof of (P0 A) % Found x20:(P A) % Found (fun (x20:(P A))=> x20) as proof of (P A) % Found (fun (x20:(P A))=> x20) as proof of (P0 A) % Found eq_ref00:=(eq_ref0 A):(((eq fofType) A) A) % Found (eq_ref0 A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) B) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) B) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) B) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) B) % Found x30:(P B) % Found (fun (x30:(P B))=> x30) as proof of (P B) % Found (fun (x30:(P B))=> x30) as proof of (P0 B) % Found eq_ref00:=(eq_ref0 B):(((eq fofType) B) B) % Found (eq_ref0 B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found x2:(P A) % Instantiate: A0:=A:fofType % Found x2 as proof of (P0 A0) % Found iff_refl0:=(iff_refl ((in Xx) A0)):((iff ((in Xx) A0)) ((in Xx) A0)) % Found (iff_refl ((in Xx) A0)) as proof of ((iff ((in Xx) A0)) ((in Xx) B)) % Found (iff_refl ((in Xx) A0)) as proof of ((iff ((in Xx) A0)) ((in Xx) B)) % Found (fun (Xx:fofType)=> (iff_refl ((in Xx) A0))) as proof of ((iff ((in Xx) A0)) ((in Xx) B)) % Found (fun (Xx:fofType)=> (iff_refl ((in Xx) A0))) as proof of (forall (Xx:fofType), ((iff ((in Xx) A0)) ((in Xx) B))) % Found x2:(P A) % Instantiate: b:=A:fofType % Found x2 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 B):(((eq fofType) B) B) % Found (eq_ref0 B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found eq_ref00:=(eq_ref0 A):(((eq fofType) A) A) % Found (eq_ref0 A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) B) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) B) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) B) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) B) % Found eq_ref00:=(eq_ref0 B):(((eq fofType) B) B) % Found (eq_ref0 B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found x2:(P0 b) % Instantiate: b:=A:fofType % Found (fun (x2:(P0 b))=> x2) as proof of (P0 A) % Found (fun (P0:(fofType->Prop)) (x2:(P0 b))=> x2) as proof of ((P0 b)->(P0 A)) % Found (fun (P0:(fofType->Prop)) (x2:(P0 b))=> x2) as proof of (P b) % Found x2:(P B) % Instantiate: b:=B:fofType % Found x2 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 A):(((eq fofType) A) A) % Found (eq_ref0 A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found x2:(P B) % Instantiate: A0:=B:fofType % Found x2 as proof of (P0 A0) % Found iff_refl0:=(iff_refl ((in Xx) A0)):((iff ((in Xx) A0)) ((in Xx) A0)) % Found (iff_refl ((in Xx) A0)) as proof of ((iff ((in Xx) A0)) ((in Xx) A)) % Found (iff_refl ((in Xx) A0)) as proof of ((iff ((in Xx) A0)) ((in Xx) A)) % Found (fun (Xx:fofType)=> (iff_refl ((in Xx) A0))) as proof of ((iff ((in Xx) A0)) ((in Xx) A)) % Found (fun (Xx:fofType)=> (iff_refl ((in Xx) A0))) as proof of (forall (Xx:fofType), ((iff ((in Xx) A0)) ((in Xx) A))) % Found x30:(P1 B) % Found (fun (x30:(P1 B))=> x30) as proof of (P1 B) % Found (fun (x30:(P1 B))=> x30) as proof of (P2 B) % Found x30:(P1 B) % Found (fun (x30:(P1 B))=> x30) as proof of (P1 B) % Found (fun (x30:(P1 B))=> x30) as proof of (P2 B) % Found x20:(P A) % Found (fun (x20:(P A))=> x20) as proof of (P A) % Found (fun (x20:(P A))=> x20) as proof of (P0 A) % Found eq_ref00:=(eq_ref0 A):(((eq fofType) A) A) % Found (eq_ref0 A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) B) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) B) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) B) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) B) % Found x30:(P b) % Found (fun (x30:(P b))=> x30) as proof of (P b) % Found (fun (x30:(P b))=> x30) as proof of (P0 b) % Found eq_ref00:=(eq_ref0 A):(((eq fofType) A) A) % Found (eq_ref0 A) as proof of (((eq fofType) A) b0) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b0) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b0) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b0) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) B) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) B) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) B) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) B) % Found eq_ref00:=(eq_ref0 B):(((eq fofType) B) B) % Found (eq_ref0 B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found eq_ref00:=(eq_ref0 B):(((eq fofType) B) B) % Found (eq_ref0 B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found eq_ref00:=(eq_ref0 B):(((eq fofType) B) B) % Found (eq_ref0 B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found x20:(P b) % Found (fun (x20:(P b))=> x20) as proof of (P b) % Found (fun (x20:(P b))=> x20) as proof of (P0 b) % Found x30:(P A) % Found (fun (x30:(P A))=> x30) as proof of (P A) % Found (fun (x30:(P A))=> x30) as proof of (P0 A) % Found eq_ref00:=(eq_ref0 B):(((eq fofType) B) B) % Found (eq_ref0 B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found x20:(P B) % Found (fun (x20:(P B))=> x20) as proof of (P B) % Found (fun (x20:(P B))=> x20) as proof of (P0 B) % Found eq_ref00:=(eq_ref0 B):(((eq fofType) B) B) % Found (eq_ref0 B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) A) % Found x20:(P A) % Found (fun (x20:(P A))=> x20) as proof of (P A) % Found (fun (x20:(P A))=> x20) as proof of (P0 A) % Found x30:(P b) % Found (fun (x30:(P b))=> x30) as proof of (P b) % Found (fun (x30:(P b))=> x30) as proof of (P0 b) % Found x30:(P B) % Found (fun (x30:(P B))=> x30) as proof of (P B) % Found (fun (x30:(P B))=> x30) as proof of (P0 B) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) A) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) A) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) A) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) A) % Found eq_ref00:=(eq_ref0 B):(((eq fofType) B) B) % Found (eq_ref0 B) as proof of (((eq fofType) B) b0) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b0) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b0) % Found ((eq_ref fofType) B) as proof of (((eq fofType) B) b0) % Found eq_ref00:=(eq_ref0 A):(((eq fofType) A) A) % Found (eq_ref0 A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found ((eq_ref fofType) A) as proof of (((eq fofType) A) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) B) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) B) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) B) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) B) % Found x20:(P b) % Found (fun (x20:(P b))=> x20) as proof of (P b) % Found (fun (x20:(P b))=> x20) as proof of (P0 b) % Found x30:(P B) % Found (fun (x30:(P B))=> x30) as proof of (P B) % Found (fun (x30:(P B))=> x30) as proof of (P0 B) % Found x30:(P B) % Found (fun (x30:(P B))=> x30) as proof of (P B) % Found (fun (x30:(P B))=> x30) as proof of (P0 B) % Found x10:=(x1 Xx):(((in Xx) B)->((in Xx) A)) % Found (x1 Xx) as proof of (((in Xx) B)->((in Xx) A)) % Found (x1 Xx) as proof of (((in Xx) B)->((in Xx) A)) % Found x00:=(x0 Xx):(((in Xx) A)->((in Xx) B)) % Found (x0 Xx) as proof of (((in Xx) A)->((in Xx) B)) % Found (x0 Xx) as proof of (((in Xx) A)->((in Xx) B)) % Found ((conj00 (x0 Xx)) (x1 Xx)) as proof of ((and (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) % Found (((conj0 (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx)) as proof of ((and (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) % Found ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx)) as proof of ((and (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) % Found ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx)) as proof of ((and (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) % Found (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx))) as proof of ((iff ((in Xx) A)) ((in Xx) B)) % Found (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx))) as proof of (forall (Xx:fofType), ((iff ((in Xx) A)) ((in Xx) B))) % Found (x20 (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx)))) as proof of (((eq fofType) A) B) % Found ((x2 B) (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx)))) as proof of (((eq fofType) A) B) % Found (((x A) B) (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx)))) as proof of (((eq fofType) A) B) % Found (fun (x1:(forall (Xx:fofType), (((in Xx) B)->((in Xx) A))))=> (((x A) B) (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx))))) as proof of (((eq fofType) A) B) % Found (fun (x0:(forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))) (x1:(forall (Xx:fofType), (((in Xx) B)->((in Xx) A))))=> (((x A) B) (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx))))) as proof of ((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B)) % Found (fun (B:fofType) (x0:(forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))) (x1:(forall (Xx:fofType), (((in Xx) B)->((in Xx) A))))=> (((x A) B) (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx))))) as proof of ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B))) % Found (fun (A:fofType) (B:fofType) (x0:(forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))) (x1:(forall (Xx:fofType), (((in Xx) B)->((in Xx) A))))=> (((x A) B) (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx))))) as proof of (forall (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B)))) % Found (fun (x:setextAx) (A:fofType) (B:fofType) (x0:(forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))) (x1:(forall (Xx:fofType), (((in Xx) B)->((in Xx) A))))=> (((x A) B) (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx))))) as proof of (forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B)))) % Found (fun (x:setextAx) (A:fofType) (B:fofType) (x0:(forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))) (x1:(forall (Xx:fofType), (((in Xx) B)->((in Xx) A))))=> (((x A) B) (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx))))) as proof of (setextAx->(forall (A:fofType) (B:fofType), ((forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))->((forall (Xx:fofType), (((in Xx) B)->((in Xx) A)))->(((eq fofType) A) B))))) % Got proof (fun (x:setextAx) (A:fofType) (B:fofType) (x0:(forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))) (x1:(forall (Xx:fofType), (((in Xx) B)->((in Xx) A))))=> (((x A) B) (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx))))) % Time elapsed = 15.247514s % node=3250 cost=1411.000000 depth=16 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:setextAx) (A:fofType) (B:fofType) (x0:(forall (Xx:fofType), (((in Xx) A)->((in Xx) B)))) (x1:(forall (Xx:fofType), (((in Xx) B)->((in Xx) A))))=> (((x A) B) (fun (Xx:fofType)=> ((((conj (((in Xx) A)->((in Xx) B))) (((in Xx) B)->((in Xx) A))) (x0 Xx)) (x1 Xx))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------