%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU596^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 : n185.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:34 EDT 2014 % Result : Theorem 48.52s % Output : Proof 48.52s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU596^2 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n185.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:50:31 CDT 2014 % % CPUTime : 48.52 % 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 0x25bb998>, <kernel.DependentProduct object at 0x25bb5a8>) of role type named in_type % Using role type % Declaring in:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x2611908>, <kernel.Single object at 0x25bb368>) of role type named emptyset_type % Using role type % Declaring emptyset:fofType % FOF formula (<kernel.Constant object at 0x25bb5a8>, <kernel.Sort object at 0x20a51b8>) of role type named emptyI_type % Using role type % Declaring emptyI:Prop % FOF formula (((eq Prop) emptyI) (forall (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->False))->(((eq fofType) A) emptyset)))) of role definition named emptyI % A new definition: (((eq Prop) emptyI) (forall (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->False))->(((eq fofType) A) emptyset)))) % Defined: emptyI:=(forall (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->False))->(((eq fofType) A) emptyset))) % FOF formula (<kernel.Constant object at 0x25bbb90>, <kernel.DependentProduct object at 0x25bbf38>) of role type named binintersect_type % Using role type % Declaring binintersect:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x25bb050>, <kernel.Sort object at 0x20a51b8>) of role type named binintersectEL_type % Using role type % Declaring binintersectEL:Prop % FOF formula (((eq Prop) binintersectEL) (forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) ((binintersect A) B))->((in Xx) A)))) of role definition named binintersectEL % A new definition: (((eq Prop) binintersectEL) (forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) ((binintersect A) B))->((in Xx) A)))) % Defined: binintersectEL:=(forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) ((binintersect A) B))->((in Xx) A))) % FOF formula (<kernel.Constant object at 0x25bb5a8>, <kernel.Sort object at 0x20a51b8>) of role type named binintersectER_type % Using role type % Declaring binintersectER:Prop % FOF formula (((eq Prop) binintersectER) (forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) ((binintersect A) B))->((in Xx) B)))) of role definition named binintersectER % A new definition: (((eq Prop) binintersectER) (forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) ((binintersect A) B))->((in Xx) B)))) % Defined: binintersectER:=(forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) ((binintersect A) B))->((in Xx) B))) % FOF formula (emptyI->(binintersectEL->(binintersectER->(forall (A:fofType) (B:fofType), ((((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False)->(((eq fofType) ((binintersect A) B)) emptyset)))))) of role conjecture named disjointsetsI1 % Conjecture to prove = (emptyI->(binintersectEL->(binintersectER->(forall (A:fofType) (B:fofType), ((((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False)->(((eq fofType) ((binintersect A) B)) emptyset)))))):Prop % We need to prove ['(emptyI->(binintersectEL->(binintersectER->(forall (A:fofType) (B:fofType), ((((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False)->(((eq fofType) ((binintersect A) B)) emptyset))))))'] % Parameter fofType:Type. % Parameter in:(fofType->(fofType->Prop)). % Parameter emptyset:fofType. % Definition emptyI:=(forall (A:fofType), ((forall (Xx:fofType), (((in Xx) A)->False))->(((eq fofType) A) emptyset))):Prop. % Parameter binintersect:(fofType->(fofType->fofType)). % Definition binintersectEL:=(forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) ((binintersect A) B))->((in Xx) A))):Prop. % Definition binintersectER:=(forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) ((binintersect A) B))->((in Xx) B))):Prop. % Trying to prove (emptyI->(binintersectEL->(binintersectER->(forall (A:fofType) (B:fofType), ((((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False)->(((eq fofType) ((binintersect A) B)) emptyset)))))) % Found x40:(P ((binintersect A) B)) % Found (fun (x40:(P ((binintersect A) B)))=> x40) as proof of (P ((binintersect A) B)) % Found (fun (x40:(P ((binintersect A) B)))=> x40) as proof of (P0 ((binintersect A) B)) % Found x40:(P ((binintersect A) B)) % Found (fun (x40:(P ((binintersect A) B)))=> x40) as proof of (P ((binintersect A) B)) % Found (fun (x40:(P ((binintersect A) B)))=> x40) as proof of (P0 ((binintersect A) B)) % Found x30:(P ((binintersect A) B)) % Found (fun (x30:(P ((binintersect A) B)))=> x30) as proof of (P ((binintersect A) B)) % Found (fun (x30:(P ((binintersect A) B)))=> x30) as proof of (P0 ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 ((binintersect A) B)):(((eq fofType) ((binintersect A) B)) ((binintersect A) B)) % Found (eq_ref0 ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found x30:(P ((binintersect A) B)) % Found (fun (x30:(P ((binintersect A) B)))=> x30) as proof of (P ((binintersect A) B)) % Found (fun (x30:(P ((binintersect A) B)))=> x30) as proof of (P0 ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 ((binintersect A) B)):(((eq fofType) ((binintersect A) B)) ((binintersect A) B)) % Found (eq_ref0 ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found x20:False % Found (fun (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of False % Found (fun (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (((in Xx) ((binintersect A) B))->False) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found x20:False % Found (fun (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of False % Found (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (((in Xx) ((binintersect A) B))->False) % Found (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (forall (Xx:fofType), (((in Xx) ((binintersect A) B))->False)) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found x20:False % Found (fun (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of False % Found (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (((in Xx) ((binintersect A) B))->False) % Found (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (forall (Xx:fofType), (((in Xx) ((binintersect A) B))->False)) % Found (x3 (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20)) as proof of (((eq fofType) ((binintersect A) B)) emptyset) % Found ((x ((binintersect A) B)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20)) as proof of (((eq fofType) ((binintersect A) B)) emptyset) % Found ((x ((binintersect A) B)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20)) as proof of (((eq fofType) ((binintersect A) B)) emptyset) % Found x20:False % Found (fun (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of False % Found (fun (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (((in Xx) ((binintersect A) B))->False) % Found x20:False % Found (fun (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of False % Found (fun (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (((in Xx) ((binintersect A) B))->False) % Found x20:False % Found (fun (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of False % Found (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (((in Xx) ((binintersect A) B))->False) % Found (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (forall (Xx:fofType), (((in Xx) ((binintersect A) B))->False)) % Found x20:False % Found (fun (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of False % Found (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (((in Xx) ((binintersect A) B))->False) % Found (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (forall (Xx:fofType), (((in Xx) ((binintersect A) B))->False)) % Found x3:(P ((binintersect A) B)) % Instantiate: A0:=((binintersect A) B):fofType % Found x3 as proof of (P0 A0) % Found x3:(P ((binintersect A) B)) % Instantiate: A0:=((binintersect A) B):fofType % Found x3 as proof of (P0 A0) % Found x3:(P ((binintersect A) B)) % Instantiate: b:=((binintersect A) B):fofType % Found x3 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found x20:False % Found (fun (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of False % Found (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (((in Xx) ((binintersect A) B))->False) % Found (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20) as proof of (forall (Xx:fofType), (((in Xx) ((binintersect A) B))->False)) % Found (x30 (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20)) as proof of ((P ((binintersect A) B))->(P emptyset)) % Found (x30 (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20)) as proof of ((P ((binintersect A) B))->(P emptyset)) % Found ((fun (x4:(forall (Xx:fofType), (((in Xx) ((binintersect A) B))->False)))=> ((x3 x4) P)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20)) as proof of ((P ((binintersect A) B))->(P emptyset)) % Found ((fun (x4:(forall (Xx:fofType), (((in Xx) ((binintersect A) B))->False)))=> (((x ((binintersect A) B)) x4) P)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20)) as proof of ((P ((binintersect A) B))->(P emptyset)) % Found ((fun (x4:(forall (Xx:fofType), (((in Xx) ((binintersect A) B))->False)))=> (((x ((binintersect A) B)) x4) P)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> x20)) as proof of ((P ((binintersect A) B))->(P emptyset)) % Found x3:(P ((binintersect A) B)) % Instantiate: b:=((binintersect A) B):fofType % Found x3 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found x20:False % Found (fun (x4:((in Xx) b))=> x20) as proof of False % Found (fun (x4:((in Xx) b))=> x20) as proof of (((in Xx) b)->False) % Found x20:False % Found (fun (x4:((in Xx) b))=> x20) as proof of False % Found (fun (Xx:fofType) (x4:((in Xx) b))=> x20) as proof of (((in Xx) b)->False) % Found (fun (Xx:fofType) (x4:((in Xx) b))=> x20) as proof of (forall (Xx:fofType), (((in Xx) b)->False)) % Found x4:(P0 A0) % Instantiate: A0:=((binintersect A) B):fofType % Found (fun (x4:(P0 A0))=> x4) as proof of (P0 ((binintersect A) B)) % Found (fun (P0:(fofType->Prop)) (x4:(P0 A0))=> x4) as proof of ((P0 A0)->(P0 ((binintersect A) B))) % Found (fun (P0:(fofType->Prop)) (x4:(P0 A0))=> x4) as proof of (P A0) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found eq_ref00:=(eq_ref0 ((binintersect A) B)):(((eq fofType) ((binintersect A) B)) ((binintersect A) B)) % Found (eq_ref0 ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found x3:(P0 b) % Instantiate: b:=((binintersect A) B):fofType % Found (fun (x3:(P0 b))=> x3) as proof of (P0 ((binintersect A) B)) % Found (fun (P0:(fofType->Prop)) (x3:(P0 b))=> x3) as proof of ((P0 b)->(P0 ((binintersect A) B))) % Found (fun (P0:(fofType->Prop)) (x3:(P0 b))=> x3) as proof of (P b) % Found x3:(P emptyset) % Instantiate: b:=emptyset:fofType % Found x3 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 ((binintersect A) B)):(((eq fofType) ((binintersect A) B)) ((binintersect A) B)) % Found (eq_ref0 ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found x20:False % Found (fun (x4:((in Xx) b))=> x20) as proof of False % Found (fun (Xx:fofType) (x4:((in Xx) b))=> x20) as proof of (((in Xx) b)->False) % Found (fun (Xx:fofType) (x4:((in Xx) b))=> x20) as proof of (forall (Xx:fofType), (((in Xx) b)->False)) % Found (x3 (fun (Xx:fofType) (x4:((in Xx) b))=> x20)) as proof of (((eq fofType) b) emptyset) % Found ((x b) (fun (Xx:fofType) (x4:((in Xx) b))=> x20)) as proof of (((eq fofType) b) emptyset) % Found ((x b) (fun (Xx:fofType) (x4:((in Xx) b))=> x20)) as proof of (((eq fofType) b) emptyset) % Found x4:(P0 A0) % Instantiate: A0:=((binintersect A) B):fofType % Found (fun (x4:(P0 A0))=> x4) as proof of (P0 ((binintersect A) B)) % Found (fun (P0:(fofType->Prop)) (x4:(P0 A0))=> x4) as proof of ((P0 A0)->(P0 ((binintersect A) B))) % Found (fun (P0:(fofType->Prop)) (x4:(P0 A0))=> x4) as proof of (P A0) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found eq_ref00:=(eq_ref0 ((binintersect A) B)):(((eq fofType) ((binintersect A) B)) ((binintersect A) B)) % Found (eq_ref0 ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found x30:(P ((binintersect A) B)) % Found (fun (x30:(P ((binintersect A) B)))=> x30) as proof of (P ((binintersect A) B)) % Found (fun (x30:(P ((binintersect A) B)))=> x30) as proof of (P0 ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 ((binintersect A) B)):(((eq fofType) ((binintersect A) B)) ((binintersect A) B)) % Found (eq_ref0 ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found x3:(P0 b) % Instantiate: b:=((binintersect A) B):fofType % Found (fun (x3:(P0 b))=> x3) as proof of (P0 ((binintersect A) B)) % Found (fun (P0:(fofType->Prop)) (x3:(P0 b))=> x3) as proof of ((P0 b)->(P0 ((binintersect A) B))) % Found (fun (P0:(fofType->Prop)) (x3:(P0 b))=> x3) as proof of (P b) % Found x40:(P b) % Found (fun (x40:(P b))=> x40) as proof of (P b) % Found (fun (x40:(P b))=> x40) as proof of (P0 b) % Found x3:(P emptyset) % Instantiate: b:=emptyset:fofType % Found x3 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 ((binintersect A) B)):(((eq fofType) ((binintersect A) B)) ((binintersect A) B)) % Found (eq_ref0 ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found x30:(P ((binintersect A) B)) % Found (fun (x30:(P ((binintersect A) B)))=> x30) as proof of (P ((binintersect A) B)) % Found (fun (x30:(P ((binintersect A) B)))=> x30) as proof of (P0 ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found eq_ref00:=(eq_ref0 ((binintersect A) B)):(((eq fofType) ((binintersect A) B)) ((binintersect A) B)) % Found (eq_ref0 ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found x40:(P b) % Found (fun (x40:(P b))=> x40) as proof of (P b) % Found (fun (x40:(P b))=> x40) as proof of (P0 b) % Found x40:(P ((binintersect A) B)) % Found (fun (x40:(P ((binintersect A) B)))=> x40) as proof of (P ((binintersect A) B)) % Found (fun (x40:(P ((binintersect A) B)))=> x40) as proof of (P0 ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) 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 x40:(P ((binintersect A) B)) % Found (fun (x40:(P ((binintersect A) B)))=> x40) as proof of (P ((binintersect A) B)) % Found (fun (x40:(P ((binintersect A) B)))=> x40) as proof of (P0 ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found x20:False % Found (fun (x5:((in Xx) A0))=> x20) as proof of False % Found (fun (x5:((in Xx) A0))=> x20) as proof of (((in Xx) A0)->False) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found x30:(P emptyset) % Found (fun (x30:(P emptyset))=> x30) as proof of (P emptyset) % Found (fun (x30:(P emptyset))=> x30) as proof of (P0 emptyset) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) 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) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found x20:False % Found (fun (x5:((in Xx) A0))=> x20) as proof of False % Found (fun (x5:((in Xx) A0))=> x20) as proof of (((in Xx) A0)->False) % Found x20:False % Found (fun (x5:((in Xx) A0))=> x20) as proof of False % Found (fun (Xx:fofType) (x5:((in Xx) A0))=> x20) as proof of (((in Xx) A0)->False) % Found (fun (Xx:fofType) (x5:((in Xx) A0))=> x20) as proof of (forall (Xx:fofType), (((in Xx) A0)->False)) % Found x30:(P ((binintersect A) B)) % Found (fun (x30:(P ((binintersect A) B)))=> x30) as proof of (P ((binintersect A) B)) % Found (fun (x30:(P ((binintersect A) B)))=> x30) as proof of (P0 ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 ((binintersect A) B)):(((eq fofType) ((binintersect A) B)) ((binintersect A) B)) % Found (eq_ref0 ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b0) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b0) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b0) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b0) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) emptyset) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) emptyset) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) emptyset) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) emptyset) % Found x20:False % Found (fun (x5:((in Xx) A0))=> x20) as proof of False % Found (fun (Xx:fofType) (x5:((in Xx) A0))=> x20) as proof of (((in Xx) A0)->False) % Found (fun (Xx:fofType) (x5:((in Xx) A0))=> x20) as proof of (forall (Xx:fofType), (((in Xx) A0)->False)) % 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 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 eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))):(((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) (fun (x:fofType)=> ((and ((in x) A)) ((in x) B)))) % Found (eta_expansion_dep00 (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found ((eta_expansion_dep0 (fun (x4:fofType)=> Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found (((eta_expansion_dep fofType) (fun (x4:fofType)=> Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found (((eta_expansion_dep fofType) (fun (x4:fofType)=> Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found (((eta_expansion_dep fofType) (fun (x4:fofType)=> Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found x20:False % Found (fun (x4:((in Xx) b))=> x20) as proof of False % Found (fun (x4:((in Xx) b))=> x20) as proof of (((in Xx) b)->False) % Found eq_ref00:=(eq_ref0 ((binintersect A) B)):(((eq fofType) ((binintersect A) B)) ((binintersect A) B)) % Found (eq_ref0 ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found x30:(P emptyset) % Found (fun (x30:(P emptyset))=> x30) as proof of (P emptyset) % Found (fun (x30:(P emptyset))=> x30) as proof of (P0 emptyset) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b) % Found eq_ref00:=(eq_ref0 (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))):(((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) % Found (eq_ref0 (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found ((eq_ref (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found ((eq_ref (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found ((eq_ref (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found x20:False % Found (fun (x4:((in Xx) b))=> x20) as proof of False % Found (fun (Xx:fofType) (x4:((in Xx) b))=> x20) as proof of (((in Xx) b)->False) % Found (fun (Xx:fofType) (x4:((in Xx) b))=> x20) as proof of (forall (Xx:fofType), (((in Xx) b)->False)) % Found x30:(P ((binintersect A) B)) % Found (fun (x30:(P ((binintersect A) B)))=> x30) as proof of (P ((binintersect A) B)) % Found (fun (x30:(P ((binintersect A) B)))=> x30) as proof of (P0 ((binintersect A) B)) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) emptyset) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) emptyset) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) emptyset) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) emptyset) % Found eq_ref00:=(eq_ref0 ((binintersect A) B)):(((eq fofType) ((binintersect A) B)) ((binintersect A) B)) % Found (eq_ref0 ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b0) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b0) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b0) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b0) % Found x30:(P emptyset) % Found (fun (x30:(P emptyset))=> x30) as proof of (P emptyset) % Found (fun (x30:(P emptyset))=> x30) as proof of (P0 emptyset) % 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 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 (f x3)):(((eq Prop) (f x3)) (f x3)) % Found (eq_ref0 (f x3)) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found (fun (x3:fofType)=> ((eq_ref Prop) (f x3))) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found (fun (x3:fofType)=> ((eq_ref Prop) (f x3))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) ((in x) B)))) % Found eq_ref00:=(eq_ref0 (f x3)):(((eq Prop) (f x3)) (f x3)) % Found (eq_ref0 (f x3)) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found (fun (x3:fofType)=> ((eq_ref Prop) (f x3))) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found (fun (x3:fofType)=> ((eq_ref Prop) (f x3))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) ((in x) B)))) % Found x3:(P ((binintersect A) B)) % Instantiate: A0:=((binintersect A) B):fofType % Found x3 as proof of (P0 A0) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) emptyset) % Found eq_ref00:=(eq_ref0 ((binintersect A) B)):(((eq fofType) ((binintersect A) B)) ((binintersect A) B)) % Found (eq_ref0 ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % Found ((eq_ref fofType) ((binintersect A) B)) as proof of (((eq fofType) ((binintersect A) B)) b) % 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 emptyset):(((eq fofType) emptyset) emptyset) % Found (eq_ref0 emptyset) as proof of (((eq fofType) emptyset) b0) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b0) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b0) % Found ((eq_ref fofType) emptyset) as proof of (((eq fofType) emptyset) b0) % Found x20:False % Found (fun (x4:((in Xx) A0))=> x20) as proof of False % Found (fun (x4:((in Xx) A0))=> x20) as proof of (((in Xx) A0)->False) % Found eq_ref00:=(eq_ref0 (f x3)):(((eq Prop) (f x3)) (f x3)) % Found (eq_ref0 (f x3)) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found (fun (x3:fofType)=> ((eq_ref Prop) (f x3))) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found (fun (x3:fofType)=> ((eq_ref Prop) (f x3))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) ((in x) B)))) % Found eq_ref00:=(eq_ref0 (f x3)):(((eq Prop) (f x3)) (f x3)) % Found (eq_ref0 (f x3)) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found ((eq_ref Prop) (f x3)) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found (fun (x3:fofType)=> ((eq_ref Prop) (f x3))) as proof of (((eq Prop) (f x3)) ((and ((in x3) A)) ((in x3) B))) % Found (fun (x3:fofType)=> ((eq_ref Prop) (f x3))) as proof of (forall (x:fofType), (((eq Prop) (f x)) ((and ((in x) A)) ((in x) B)))) % Found x20:False % Found (fun (x4:((in Xx) A0))=> x20) as proof of False % Found (fun (x4:((in Xx) A0))=> x20) as proof of (((in Xx) A0)->False) % Found x20:False % Found (fun (x5:((in Xx) A0))=> x20) as proof of False % Found (fun (Xx:fofType) (x5:((in Xx) A0))=> x20) as proof of (((in Xx) A0)->False) % Found (fun (Xx:fofType) (x5:((in Xx) A0))=> x20) as proof of (forall (Xx:fofType), (((in Xx) A0)->False)) % Found ((x40 (fun (Xx:fofType) (x5:((in Xx) A0))=> x20)) x3) as proof of (P emptyset) % Found ((x40 (fun (Xx:fofType) (x5:((in Xx) A0))=> x20)) x3) as proof of (P emptyset) % Found (((fun (x5:(forall (Xx:fofType), (((in Xx) A0)->False)))=> ((x4 x5) P)) (fun (Xx:fofType) (x5:((in Xx) A0))=> x20)) x3) as proof of (P emptyset) % Found (((fun (x5:(forall (Xx:fofType), (((in Xx) ((binintersect A) B))->False)))=> (((x ((binintersect A) B)) x5) P)) (fun (Xx:fofType) (x5:((in Xx) ((binintersect A) B)))=> x20)) x3) as proof of (P emptyset) % Found (((fun (x5:(forall (Xx:fofType), (((in Xx) ((binintersect A) B))->False)))=> (((x ((binintersect A) B)) x5) P)) (fun (Xx:fofType) (x5:((in Xx) ((binintersect A) B)))=> x20)) x3) as proof of (P emptyset) % Found eta_expansion_dep000:=(eta_expansion_dep00 (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))):(((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) (fun (x:fofType)=> ((and ((in x) A)) ((in x) B)))) % Found (eta_expansion_dep00 (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found ((eta_expansion_dep0 (fun (x5:fofType)=> Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found (((eta_expansion_dep fofType) (fun (x5:fofType)=> Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found (((eta_expansion_dep fofType) (fun (x5:fofType)=> Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found (((eta_expansion_dep fofType) (fun (x5:fofType)=> Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) as proof of (((eq (fofType->Prop)) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) b) % Found x20:False % Found (fun (x4:((in Xx) A0))=> x20) as proof of False % Found (fun (Xx:fofType) (x4:((in Xx) A0))=> x20) as proof of (((in Xx) A0)->False) % Found (fun (Xx:fofType) (x4:((in Xx) A0))=> x20) as proof of (forall (Xx:fofType), (((in Xx) A0)->False)) % Found x4:((in Xx) ((binintersect A) B)) % Instantiate: B0:=B:fofType;x5:=Xx:fofType % Found x4 as proof of ((in x5) ((binintersect A) B0)) % Found (x0000 x4) as proof of ((in x5) A) % Found ((x000 B) x4) as proof of ((in x5) A) % Found (((fun (B0:fofType)=> ((x00 B0) x5)) B) x4) as proof of ((in x5) A) % Found (((fun (B0:fofType)=> (((x0 A) B0) x5)) B) x4) as proof of ((in x5) A) % Found (((fun (B0:fofType)=> (((x0 A) B0) x5)) B) x4) as proof of ((in x5) A) % Found x10000:=(x1000 x4):((in x5) B) % Found (x1000 x4) as proof of ((in x5) B) % Found ((x100 A) x4) as proof of ((in x5) B) % Found (((fun (A0:fofType)=> ((x10 A0) x5)) A) x4) as proof of ((in x5) B) % Found (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) x5)) A) x4) as proof of ((in x5) B) % Found (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) x5)) A) x4) as proof of ((in x5) B) % Found ((conj00 (((fun (B0:fofType)=> (((x0 A) B0) x5)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) x5)) A) x4)) as proof of ((and ((in x5) A)) ((in x5) B)) % Found (((conj0 ((in x5) B)) (((fun (B0:fofType)=> (((x0 A) B0) x5)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) x5)) A) x4)) as proof of ((and ((in x5) A)) ((in x5) B)) % Found ((((conj ((in x5) A)) ((in x5) B)) (((fun (B0:fofType)=> (((x0 A) B0) x5)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) x5)) A) x4)) as proof of ((and ((in x5) A)) ((in x5) B)) % Found ((((conj ((in x5) A)) ((in x5) B)) (((fun (B0:fofType)=> (((x0 A) B0) x5)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) x5)) A) x4)) as proof of ((and ((in x5) A)) ((in x5) B)) % Found (ex_intro000 ((((conj ((in x5) A)) ((in x5) B)) (((fun (B0:fofType)=> (((x0 A) B0) x5)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) x5)) A) x4))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) % Found ((ex_intro00 Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) % Found (((ex_intro0 (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) % Found ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) % Found ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))) as proof of ((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) % Found (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4)))) as proof of False % Found (fun (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))))) as proof of False % Found (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))))) as proof of (((in Xx) ((binintersect A) B))->False) % Found (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))))) as proof of (forall (Xx:fofType), (((in Xx) ((binintersect A) B))->False)) % Found (x3 (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4)))))) as proof of (((eq fofType) ((binintersect A) B)) emptyset) % Found ((x ((binintersect A) B)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4)))))) as proof of (((eq fofType) ((binintersect A) B)) emptyset) % Found (fun (x2:(((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False))=> ((x ((binintersect A) B)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))))))) as proof of (((eq fofType) ((binintersect A) B)) emptyset) % Found (fun (B:fofType) (x2:(((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False))=> ((x ((binintersect A) B)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))))))) as proof of ((((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False)->(((eq fofType) ((binintersect A) B)) emptyset)) % Found (fun (A:fofType) (B:fofType) (x2:(((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False))=> ((x ((binintersect A) B)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))))))) as proof of (forall (B:fofType), ((((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False)->(((eq fofType) ((binintersect A) B)) emptyset))) % Found (fun (x1:binintersectER) (A:fofType) (B:fofType) (x2:(((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False))=> ((x ((binintersect A) B)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))))))) as proof of (forall (A:fofType) (B:fofType), ((((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False)->(((eq fofType) ((binintersect A) B)) emptyset))) % Found (fun (x0:binintersectEL) (x1:binintersectER) (A:fofType) (B:fofType) (x2:(((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False))=> ((x ((binintersect A) B)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))))))) as proof of (binintersectER->(forall (A:fofType) (B:fofType), ((((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False)->(((eq fofType) ((binintersect A) B)) emptyset)))) % Found (fun (x:emptyI) (x0:binintersectEL) (x1:binintersectER) (A:fofType) (B:fofType) (x2:(((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False))=> ((x ((binintersect A) B)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))))))) as proof of (binintersectEL->(binintersectER->(forall (A:fofType) (B:fofType), ((((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False)->(((eq fofType) ((binintersect A) B)) emptyset))))) % Found (fun (x:emptyI) (x0:binintersectEL) (x1:binintersectER) (A:fofType) (B:fofType) (x2:(((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False))=> ((x ((binintersect A) B)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))))))) as proof of (emptyI->(binintersectEL->(binintersectER->(forall (A:fofType) (B:fofType), ((((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False)->(((eq fofType) ((binintersect A) B)) emptyset)))))) % Got proof (fun (x:emptyI) (x0:binintersectEL) (x1:binintersectER) (A:fofType) (B:fofType) (x2:(((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False))=> ((x ((binintersect A) B)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))))))) % Time elapsed = 47.811183s % node=8679 cost=1092.000000 depth=26 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:emptyI) (x0:binintersectEL) (x1:binintersectER) (A:fofType) (B:fofType) (x2:(((ex fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B))))->False))=> ((x ((binintersect A) B)) (fun (Xx:fofType) (x4:((in Xx) ((binintersect A) B)))=> (x2 ((((ex_intro fofType) (fun (Xx:fofType)=> ((and ((in Xx) A)) ((in Xx) B)))) Xx) ((((conj ((in Xx) A)) ((in Xx) B)) (((fun (B0:fofType)=> (((x0 A) B0) Xx)) B) x4)) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) B)) A0) Xx)) A) x4))))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------