%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU647^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 : n114.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:42 EDT 2014 % Result : Theorem 26.51s % Output : Proof 26.51s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU647^2 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n114.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 32286.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Thu Jul 17 11:01:46 CDT 2014 % % CPUTime : 26.51 % 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 0x1be2200>, <kernel.DependentProduct object at 0x1be0200>) of role type named in_type % Using role type % Declaring in:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x1bc2518>, <kernel.Single object at 0x1be2128>) of role type named emptyset_type % Using role type % Declaring emptyset:fofType % FOF formula (<kernel.Constant object at 0x1be23f8>, <kernel.DependentProduct object at 0x1be03f8>) of role type named setadjoin_type % Using role type % Declaring setadjoin:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x1be2830>, <kernel.Sort object at 0x1a98cb0>) of role type named setadjoinIL_type % Using role type % Declaring setadjoinIL:Prop % FOF formula (((eq Prop) setadjoinIL) (forall (Xx:fofType) (Xy:fofType), ((in Xx) ((setadjoin Xx) Xy)))) of role definition named setadjoinIL % A new definition: (((eq Prop) setadjoinIL) (forall (Xx:fofType) (Xy:fofType), ((in Xx) ((setadjoin Xx) Xy)))) % Defined: setadjoinIL:=(forall (Xx:fofType) (Xy:fofType), ((in Xx) ((setadjoin Xx) Xy))) % FOF formula (<kernel.Constant object at 0x1be2830>, <kernel.Sort object at 0x1a98cb0>) of role type named setukpairinjL1_type % Using role type % Declaring setukpairinjL1:Prop % FOF formula (((eq Prop) setukpairinjL1) (forall (Xx:fofType) (Xy:fofType) (Xz:fofType), (((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset)))->(((eq fofType) Xx) Xz)))) of role definition named setukpairinjL1 % A new definition: (((eq Prop) setukpairinjL1) (forall (Xx:fofType) (Xy:fofType) (Xz:fofType), (((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset)))->(((eq fofType) Xx) Xz)))) % Defined: setukpairinjL1:=(forall (Xx:fofType) (Xy:fofType) (Xz:fofType), (((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset)))->(((eq fofType) Xx) Xz))) % FOF formula (setadjoinIL->(setukpairinjL1->(forall (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType), ((((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))->(((eq fofType) Xx) Xz))))) of role conjecture named setukpairinjL2 % Conjecture to prove = (setadjoinIL->(setukpairinjL1->(forall (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType), ((((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))->(((eq fofType) Xx) Xz))))):Prop % We need to prove ['(setadjoinIL->(setukpairinjL1->(forall (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType), ((((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))->(((eq fofType) Xx) Xz)))))'] % Parameter fofType:Type. % Parameter in:(fofType->(fofType->Prop)). % Parameter emptyset:fofType. % Parameter setadjoin:(fofType->(fofType->fofType)). % Definition setadjoinIL:=(forall (Xx:fofType) (Xy:fofType), ((in Xx) ((setadjoin Xx) Xy))):Prop. % Definition setukpairinjL1:=(forall (Xx:fofType) (Xy:fofType) (Xz:fofType), (((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset)))->(((eq fofType) Xx) Xz))):Prop. % Trying to prove (setadjoinIL->(setukpairinjL1->(forall (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType), ((((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))->(((eq fofType) Xx) Xz))))) % Found x10:=(x1 (fun (x2:fofType)=> (P Xx))):((P Xx)->(P Xx)) % Found (x1 (fun (x2:fofType)=> (P Xx))) as proof of (P0 Xx) % Found (x1 (fun (x2:fofType)=> (P Xx))) as proof of (P0 Xx) % Found eq_ref00:=(eq_ref0 Xx):(((eq fofType) Xx) Xx) % Found (eq_ref0 Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found eq_ref00:=(eq_ref0 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found x2:(P Xx) % Instantiate: b:=Xx:fofType % Found x2 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found x10:=(x1 (fun (x2:fofType)=> (P Xx))):((P Xx)->(P Xx)) % Found (x1 (fun (x2:fofType)=> (P Xx))) as proof of (P0 Xx) % Found (x1 (fun (x2:fofType)=> (P Xx))) as proof of (P0 Xx) % Found eq_ref00:=(eq_ref0 Xx):(((eq fofType) Xx) Xx) % Found (eq_ref0 Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found x10:=(x1 (fun (x2:fofType)=> (P Xx))):((P Xx)->(P Xx)) % Found (x1 (fun (x2:fofType)=> (P Xx))) as proof of (P0 Xx) % Found (x1 (fun (x2:fofType)=> (P Xx))) as proof of (P0 Xx) % Found eq_ref00:=(eq_ref0 Xx):(((eq fofType) Xx) Xx) % Found (eq_ref0 Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (P b) % Found ((eq_ref fofType) b) as proof of (P b) % Found ((eq_ref fofType) b) as proof of (P b) % Found ((eq_ref fofType) b) as proof of (P b) % Found eq_ref00:=(eq_ref0 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found x2:(P Xz) % Instantiate: b:=Xz:fofType % Found x2 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 Xx):(((eq fofType) Xx) Xx) % Found (eq_ref0 Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found x10:=(x1 (fun (x2:fofType)=> (P Xz))):((P Xz)->(P Xz)) % Found (x1 (fun (x2:fofType)=> (P Xz))) as proof of (P0 Xz) % Found (x1 (fun (x2:fofType)=> (P Xz))) as proof of (P0 Xz) % Found eq_ref00:=(eq_ref0 Xx):(((eq fofType) Xx) Xx) % Found (eq_ref0 Xx) as proof of (((eq fofType) Xx) b0) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b0) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b0) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b0) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) Xz) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) Xz) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) Xz) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) Xz) % Found x10:=(x1 (fun (x2:fofType)=> (P b))):((P b)->(P b)) % Found (x1 (fun (x2:fofType)=> (P b))) as proof of (P0 b) % Found (x1 (fun (x2:fofType)=> (P b))) as proof of (P0 b) % Found x10:=(x1 (fun (x2:fofType)=> (P Xz))):((P Xz)->(P Xz)) % Found (x1 (fun (x2:fofType)=> (P Xz))) as proof of (P0 Xz) % Found (x1 (fun (x2:fofType)=> (P Xz))) as proof of (P0 Xz) % Found eq_ref00:=(eq_ref0 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found eq_ref00:=(eq_ref0 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found eq_ref00:=(eq_ref0 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found eq_ref00:=(eq_ref0 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found x10:=(x1 (fun (x2:fofType)=> (P Xx))):((P Xx)->(P Xx)) % Found (x1 (fun (x2:fofType)=> (P Xx))) as proof of (P0 Xx) % Found (x1 (fun (x2:fofType)=> (P Xx))) as proof of (P0 Xx) % Found x10:=(x1 (fun (x2:fofType)=> (P b))):((P b)->(P b)) % Found (x1 (fun (x2:fofType)=> (P b))) as proof of (P0 b) % Found (x1 (fun (x2:fofType)=> (P b))) as proof of (P0 b) % Found eq_ref00:=(eq_ref0 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b0) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b0) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b0) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b0) % Found eq_ref00:=(eq_ref0 b0):(((eq fofType) b0) b0) % Found (eq_ref0 b0) as proof of (((eq fofType) b0) Xx) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) Xx) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) Xx) % Found ((eq_ref fofType) b0) as proof of (((eq fofType) b0) Xx) % Found eq_ref00:=(eq_ref0 Xx):(((eq fofType) Xx) Xx) % Found (eq_ref0 Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found eq_ref00:=(eq_ref0 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b0) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b0) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b0) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) 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 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found eq_ref00:=(eq_ref0 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xx) % 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 Xx):(((eq fofType) Xx) Xx) % Found (eq_ref0 Xx) as proof of (((eq fofType) Xx) b0) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b0) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b0) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b0) % Found x10:=(x1 (fun (x2:fofType)=> (P Xx))):((P Xx)->(P Xx)) % Found (x1 (fun (x2:fofType)=> (P Xx))) as proof of (P0 Xx) % Found (x1 (fun (x2:fofType)=> (P Xx))) as proof of (P0 Xx) % Found x2:(P Xx) % Instantiate: b:=Xx:fofType % Found x2 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found x2:(P Xx) % Instantiate: Xx0:=Xx:fofType % Found x2 as proof of (P0 Xx0) % Found x30:=(x3 ((setadjoin ((setadjoin Xx0) ((setadjoin Xy0) emptyset))) emptyset)):((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx0) ((setadjoin Xy0) emptyset))) emptyset))) % Found (x3 ((setadjoin ((setadjoin Xx0) ((setadjoin Xy0) emptyset))) emptyset)) as proof of ((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx0) emptyset)) ((setadjoin ((setadjoin Xx0) ((setadjoin Xy0) emptyset))) emptyset))) % Found ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx0) ((setadjoin Xy0) emptyset))) emptyset)) as proof of ((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx0) emptyset)) ((setadjoin ((setadjoin Xx0) ((setadjoin Xy0) emptyset))) emptyset))) % Found ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx0) ((setadjoin Xy0) emptyset))) emptyset)) as proof of ((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx0) emptyset)) ((setadjoin ((setadjoin Xx0) ((setadjoin Xy0) emptyset))) emptyset))) % Found ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx0) ((setadjoin Xy0) emptyset))) emptyset)) as proof of ((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx0) emptyset)) ((setadjoin ((setadjoin Xx0) ((setadjoin Xy0) emptyset))) emptyset))) % Found eq_ref00:=(eq_ref0 Xx):(((eq fofType) Xx) Xx) % Found (eq_ref0 Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found x10:=(x1 (fun (x2:fofType)=> (P Xx))):((P Xx)->(P Xx)) % Found (x1 (fun (x2:fofType)=> (P Xx))) as proof of (P0 Xx) % Found (x1 (fun (x2:fofType)=> (P Xx))) as proof of (P0 Xx) % Found eq_ref00:=(eq_ref0 Xx):(((eq fofType) Xx) Xx) % Found (eq_ref0 Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found eq_ref00:=(eq_ref0 b):(((eq fofType) b) b) % Found (eq_ref0 b) as proof of (P b) % Found ((eq_ref fofType) b) as proof of (P b) % Found ((eq_ref fofType) b) as proof of (P b) % Found ((eq_ref fofType) b) as proof of (P b) % Found eq_ref00:=(eq_ref0 Xz):(((eq fofType) Xz) Xz) % Found (eq_ref0 Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found ((eq_ref fofType) Xz) as proof of (((eq fofType) Xz) b) % Found x2:(P Xz) % Instantiate: b:=Xz:fofType % Found x2 as proof of (P0 b) % Found eq_ref00:=(eq_ref0 Xx):(((eq fofType) Xx) Xx) % Found (eq_ref0 Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found ((eq_ref fofType) Xx) as proof of (((eq fofType) Xx) b) % Found x10:=(x1 (fun (x2:fofType)=> (P Xz))):((P Xz)->(P Xz)) % Found (x1 (fun (x2:fofType)=> (P Xz))) as proof of (P0 Xz) % Found (x1 (fun (x2:fofType)=> (P Xz))) as proof of (P0 Xz) % Found x10:=(x1 (fun (x2:fofType)=> (P Xz))):((P Xz)->(P Xz)) % Found (x1 (fun (x2:fofType)=> (P Xz))) as proof of (P0 Xz) % Found (x1 (fun (x2:fofType)=> (P Xz))) as proof of (P0 Xz) % Found x1:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) % Instantiate: a:=((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset)):fofType;b:=((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)):fofType % Found x1 as proof of (((eq fofType) a) b) % Found x2:(P Xx) % Instantiate: a:=Xx:fofType % Found x2 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) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found ((eq_ref fofType) b) as proof of (((eq fofType) b) Xz) % Found x1:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) % Instantiate: Xy0:=Xy:fofType;b:=((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)):fofType % Found x1 as proof of (((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) b) % Found x20:=(x2 ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)):((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) % Found (x2 ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)) as proof of (P b) % Found ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)) as proof of (P b) % Found ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)) as proof of (P b) % Found ((eq_sym0000 x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) as proof of ((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) % Found ((eq_sym0000 x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) as proof of ((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) % Found (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) b))=> ((eq_sym000 x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) as proof of ((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) % Found (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((eq_sym00 ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) as proof of ((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) % Found (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> ((((eq_sym0 ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) as proof of ((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) % Found (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) as proof of ((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) % Found (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) as proof of ((in ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) % Found (x0000 (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy0) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))) as proof of (((eq fofType) Xx) Xz) % Found ((x000 Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))) as proof of (((eq fofType) Xx) Xz) % Found (((fun (Xy0:fofType)=> ((x00 Xy0) Xz)) Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))) as proof of (((eq fofType) Xx) Xz) % Found (((fun (Xy0:fofType)=> (((x0 Xx) Xy0) Xz)) Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))) as proof of (((eq fofType) Xx) Xz) % Found (fun (x1:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((fun (Xy0:fofType)=> (((x0 Xx) Xy0) Xz)) Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))) as proof of (((eq fofType) Xx) Xz) % Found (fun (Xu:fofType) (x1:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((fun (Xy0:fofType)=> (((x0 Xx) Xy0) Xz)) Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))) as proof of ((((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))->(((eq fofType) Xx) Xz)) % Found (fun (Xz:fofType) (Xu:fofType) (x1:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((fun (Xy0:fofType)=> (((x0 Xx) Xy0) Xz)) Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))) as proof of (forall (Xu:fofType), ((((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))->(((eq fofType) Xx) Xz))) % Found (fun (Xy:fofType) (Xz:fofType) (Xu:fofType) (x1:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((fun (Xy0:fofType)=> (((x0 Xx) Xy0) Xz)) Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))) as proof of (forall (Xz:fofType) (Xu:fofType), ((((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))->(((eq fofType) Xx) Xz))) % Found (fun (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType) (x1:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((fun (Xy0:fofType)=> (((x0 Xx) Xy0) Xz)) Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))) as proof of (forall (Xy:fofType) (Xz:fofType) (Xu:fofType), ((((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))->(((eq fofType) Xx) Xz))) % Found (fun (x0:setukpairinjL1) (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType) (x1:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((fun (Xy0:fofType)=> (((x0 Xx) Xy0) Xz)) Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))) as proof of (forall (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType), ((((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))->(((eq fofType) Xx) Xz))) % Found (fun (x:setadjoinIL) (x0:setukpairinjL1) (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType) (x1:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((fun (Xy0:fofType)=> (((x0 Xx) Xy0) Xz)) Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))) as proof of (setukpairinjL1->(forall (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType), ((((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))->(((eq fofType) Xx) Xz)))) % Found (fun (x:setadjoinIL) (x0:setukpairinjL1) (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType) (x1:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((fun (Xy0:fofType)=> (((x0 Xx) Xy0) Xz)) Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))) as proof of (setadjoinIL->(setukpairinjL1->(forall (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType), ((((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset)))->(((eq fofType) Xx) Xz))))) % Got proof (fun (x:setadjoinIL) (x0:setukpairinjL1) (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType) (x1:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((fun (Xy0:fofType)=> (((x0 Xx) Xy0) Xz)) Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))) % Time elapsed = 25.965649s % node=5272 cost=2085.000000 depth=21 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:setadjoinIL) (x0:setukpairinjL1) (Xx:fofType) (Xy:fofType) (Xz:fofType) (Xu:fofType) (x1:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((fun (Xy0:fofType)=> (((x0 Xx) Xy0) Xz)) Xy) (((fun (x2:(((eq fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))=> (((((eq_sym fofType) ((setadjoin ((setadjoin Xx) emptyset)) ((setadjoin ((setadjoin Xx) ((setadjoin Xy) emptyset))) emptyset))) ((setadjoin ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))) x2) (in ((setadjoin Xz) emptyset)))) x1) ((x ((setadjoin Xz) emptyset)) ((setadjoin ((setadjoin Xz) ((setadjoin Xu) emptyset))) emptyset))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------