%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU754^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 : n093.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32286.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Thu Jul 17 13:33:01 EDT 2014 % Result : Theorem 98.43s % Output : Proof 98.43s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SEU754^2 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n093.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:23:26 CDT 2014 % % CPUTime : 98.43 % 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 0x926d88>, <kernel.DependentProduct object at 0xb07cf8>) of role type named in_type % Using role type % Declaring in:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0xd57ef0>, <kernel.DependentProduct object at 0xb07cb0>) of role type named powerset_type % Using role type % Declaring powerset:(fofType->fofType) % FOF formula (<kernel.Constant object at 0x926998>, <kernel.DependentProduct object at 0xb07cb0>) of role type named binunion_type % Using role type % Declaring binunion:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x926a70>, <kernel.DependentProduct object at 0xb07cb0>) of role type named binintersect_type % Using role type % Declaring binintersect:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x926998>, <kernel.Sort object at 0x7f0ea8>) of role type named binintersectI_type % Using role type % Declaring binintersectI:Prop % FOF formula (((eq Prop) binintersectI) (forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) A)->(((in Xx) B)->((in Xx) ((binintersect A) B)))))) of role definition named binintersectI % A new definition: (((eq Prop) binintersectI) (forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) A)->(((in Xx) B)->((in Xx) ((binintersect A) B)))))) % Defined: binintersectI:=(forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) A)->(((in Xx) B)->((in Xx) ((binintersect A) B))))) % FOF formula (<kernel.Constant object at 0x926998>, <kernel.DependentProduct object at 0xb07d40>) of role type named setminus_type % Using role type % Declaring setminus:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x926998>, <kernel.Sort object at 0x7f0ea8>) of role type named setminusI_type % Using role type % Declaring setminusI:Prop % FOF formula (((eq Prop) setminusI) (forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) A)->((((in Xx) B)->False)->((in Xx) ((setminus A) B)))))) of role definition named setminusI % A new definition: (((eq Prop) setminusI) (forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) A)->((((in Xx) B)->False)->((in Xx) ((setminus A) B)))))) % Defined: setminusI:=(forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) A)->((((in Xx) B)->False)->((in Xx) ((setminus A) B))))) % FOF formula (<kernel.Constant object at 0xb07e18>, <kernel.Sort object at 0x7f0ea8>) of role type named setminusER_type % Using role type % Declaring setminusER:Prop % FOF formula (((eq Prop) setminusER) (forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) ((setminus A) B))->(((in Xx) B)->False)))) of role definition named setminusER % A new definition: (((eq Prop) setminusER) (forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) ((setminus A) B))->(((in Xx) B)->False)))) % Defined: setminusER:=(forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) ((setminus A) B))->(((in Xx) B)->False))) % FOF formula (<kernel.Constant object at 0xb07518>, <kernel.Sort object at 0x7f0ea8>) of role type named binunionTILcontra_type % Using role type % Declaring binunionTILcontra:Prop % FOF formula (((eq Prop) binunionTILcontra) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->((((in Xx) ((binunion X) Y))->False)->(((in Xx) X)->False))))))))) of role definition named binunionTILcontra % A new definition: (((eq Prop) binunionTILcontra) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->((((in Xx) ((binunion X) Y))->False)->(((in Xx) X)->False))))))))) % Defined: binunionTILcontra:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->((((in Xx) ((binunion X) Y))->False)->(((in Xx) X)->False)))))))) % FOF formula (<kernel.Constant object at 0xb07a28>, <kernel.Sort object at 0x7f0ea8>) of role type named binunionTIRcontra_type % Using role type % Declaring binunionTIRcontra:Prop % FOF formula (((eq Prop) binunionTIRcontra) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->((((in Xx) ((binunion X) Y))->False)->(((in Xx) Y)->False))))))))) of role definition named binunionTIRcontra % A new definition: (((eq Prop) binunionTIRcontra) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->((((in Xx) ((binunion X) Y))->False)->(((in Xx) Y)->False))))))))) % Defined: binunionTIRcontra:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->((((in Xx) ((binunion X) Y))->False)->(((in Xx) Y)->False)))))))) % FOF formula (binintersectI->(setminusI->(setminusER->(binunionTILcontra->(binunionTIRcontra->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))))))))))))))) of role conjecture named demorgan2a % Conjecture to prove = (binintersectI->(setminusI->(setminusER->(binunionTILcontra->(binunionTIRcontra->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))))))))))))))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(binintersectI->(setminusI->(setminusER->(binunionTILcontra->(binunionTIRcontra->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y)))))))))))))))'] % Parameter fofType:Type. % Parameter in:(fofType->(fofType->Prop)). % Parameter powerset:(fofType->fofType). % Parameter binunion:(fofType->(fofType->fofType)). % Parameter binintersect:(fofType->(fofType->fofType)). % Definition binintersectI:=(forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) A)->(((in Xx) B)->((in Xx) ((binintersect A) B))))):Prop. % Parameter setminus:(fofType->(fofType->fofType)). % Definition setminusI:=(forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) A)->((((in Xx) B)->False)->((in Xx) ((setminus A) B))))):Prop. % Definition setminusER:=(forall (A:fofType) (B:fofType) (Xx:fofType), (((in Xx) ((setminus A) B))->(((in Xx) B)->False))):Prop. % Definition binunionTILcontra:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->((((in Xx) ((binunion X) Y))->False)->(((in Xx) X)->False)))))))):Prop. % Definition binunionTIRcontra:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->((((in Xx) ((binunion X) Y))->False)->(((in Xx) Y)->False)))))))):Prop. % Trying to prove (binintersectI->(setminusI->(setminusER->(binunionTILcontra->(binunionTIRcontra->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))))))))))))))) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x6:((in Xx) A) % Found x6 as proof of ((in Xx) A) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x4:((in X) (powerset A)) % Found x4 as proof of ((in X) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x5:((in Y) (powerset A)) % Found x5 as proof of ((in Y) (powerset A)) % Found x10000:=(x1000 x7):(((in Xx) ((binunion X) Y))->False) % Found (x1000 x7) as proof of (((in Xx) ((binunion X) Y))->False) % Found ((x100 A) x7) as proof of (((in Xx) ((binunion X) Y))->False) % Found (((fun (A0:fofType)=> ((x10 A0) Xx)) A) x7) as proof of (((in Xx) ((binunion X) Y))->False) % Found (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7) as proof of (((in Xx) ((binunion X) Y))->False) % Found (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7) as proof of (((in Xx) ((binunion X) Y))->False) % Found ((x3000000 x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) Y)->False) % Found (((x300000 X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) Y)->False) % Found ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((x30000 X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) Y)->False) % Found ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((x3000 X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) Y)->False) % Found ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((x300 A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) Y)->False) % Found ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((x30 A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) Y)->False) % Found ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) Y)->False) % Found ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) Y)->False) % Found ((x0000 x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))) as proof of ((in Xx) ((setminus A) Y)) % Found (((x000 Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))) as proof of ((in Xx) ((setminus A) Y)) % Found ((((x00 Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))) as proof of ((in Xx) ((setminus A) Y)) % Found (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))) as proof of ((in Xx) ((setminus A) Y)) % Found (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))) as proof of ((in Xx) ((setminus A) Y)) % Found x10000:=(x1000 x7):(((in Xx) ((binunion X) Y))->False) % Found (x1000 x7) as proof of (((in Xx) ((binunion X) Y))->False) % Found ((x100 A) x7) as proof of (((in Xx) ((binunion X) Y))->False) % Found (((fun (A0:fofType)=> ((x10 A0) Xx)) A) x7) as proof of (((in Xx) ((binunion X) Y))->False) % Found (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7) as proof of (((in Xx) ((binunion X) Y))->False) % Found (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7) as proof of (((in Xx) ((binunion X) Y))->False) % Found ((x2000000 x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) X)->False) % Found (((x200000 Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) X)->False) % Found ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> (((x20000 Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) X)->False) % Found ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((x2000 x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) X)->False) % Found ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> (((((x200 A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) X)->False) % Found ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> (((((x20 A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) X)->False) % Found ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) X)->False) % Found ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)) as proof of (((in Xx) X)->False) % Found ((x0000 x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))) as proof of ((in Xx) ((setminus A) X)) % Found (((x000 Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))) as proof of ((in Xx) ((setminus A) X)) % Found ((((x00 X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))) as proof of ((in Xx) ((setminus A) X)) % Found (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))) as proof of ((in Xx) ((setminus A) X)) % Found (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))) as proof of ((in Xx) ((setminus A) X)) % Found ((x800 (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) as proof of ((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))) % Found (((x80 Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) as proof of ((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))) % Found ((((x8 ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) as proof of ((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))) % Found (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) as proof of ((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))) % Found (fun (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of ((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))) % Found (fun (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y)))) % Found (fun (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))))) % Found (fun (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y)))))) % Found (fun (Y:fofType) (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))))))) % Found (fun (x4:((in X) (powerset A))) (Y:fofType) (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y)))))))) % Found (fun (X:fofType) (x4:((in X) (powerset A))) (Y:fofType) (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))))))))) % Found (fun (A:fofType) (X:fofType) (x4:((in X) (powerset A))) (Y:fofType) (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (forall (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y)))))))))) % Found (fun (x3:binunionTIRcontra) (A:fofType) (X:fofType) (x4:((in X) (powerset A))) (Y:fofType) (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y)))))))))) % Found (fun (x2:binunionTILcontra) (x3:binunionTIRcontra) (A:fofType) (X:fofType) (x4:((in X) (powerset A))) (Y:fofType) (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (binunionTIRcontra->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))))))))))) % Found (fun (x1:setminusER) (x2:binunionTILcontra) (x3:binunionTIRcontra) (A:fofType) (X:fofType) (x4:((in X) (powerset A))) (Y:fofType) (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (binunionTILcontra->(binunionTIRcontra->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y)))))))))))) % Found (fun (x0:setminusI) (x1:setminusER) (x2:binunionTILcontra) (x3:binunionTIRcontra) (A:fofType) (X:fofType) (x4:((in X) (powerset A))) (Y:fofType) (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (setminusER->(binunionTILcontra->(binunionTIRcontra->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))))))))))))) % Found (fun (x:binintersectI) (x0:setminusI) (x1:setminusER) (x2:binunionTILcontra) (x3:binunionTIRcontra) (A:fofType) (X:fofType) (x4:((in X) (powerset A))) (Y:fofType) (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (setminusI->(setminusER->(binunionTILcontra->(binunionTIRcontra->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y)))))))))))))) % Found (fun (x:binintersectI) (x0:setminusI) (x1:setminusER) (x2:binunionTILcontra) (x3:binunionTIRcontra) (A:fofType) (X:fofType) (x4:((in X) (powerset A))) (Y:fofType) (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) as proof of (binintersectI->(setminusI->(setminusER->(binunionTILcontra->(binunionTIRcontra->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Xx:fofType), (((in Xx) A)->(((in Xx) ((setminus A) ((binunion X) Y)))->((in Xx) ((binintersect ((setminus A) X)) ((setminus A) Y))))))))))))))) % Got proof (fun (x:binintersectI) (x0:setminusI) (x1:setminusER) (x2:binunionTILcontra) (x3:binunionTIRcontra) (A:fofType) (X:fofType) (x4:((in X) (powerset A))) (Y:fofType) (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) % Time elapsed = 97.458749s % node=14547 cost=1855.000000 depth=35 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:binintersectI) (x0:setminusI) (x1:setminusER) (x2:binunionTILcontra) (x3:binunionTIRcontra) (A:fofType) (X:fofType) (x4:((in X) (powerset A))) (Y:fofType) (x5:((in Y) (powerset A))) (Xx:fofType) (x6:((in Xx) A)) (x7:((in Xx) ((setminus A) ((binunion X) Y))))=> (((((x ((setminus A) X)) ((setminus A) Y)) Xx) (((((x0 A) X) Xx) x6) ((((fun (Y0:fofType) (x10:((in Y0) (powerset A)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (Y0:fofType) (x10:((in Y0) (powerset A0)))=> ((((((fun (A0:fofType)=> ((x2 A0) X)) A0) x9) Y0) x10) Xx)) A) x4) Y0) x10) x6)) Y) x5) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7)))) (((((x0 A) Y) Xx) x6) ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> ((((fun (X0:fofType) (x9:((in X0) (powerset A)))=> (((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((((fun (A0:fofType) (X0:fofType) (x9:((in X0) (powerset A0)))=> ((((x3 A0) X0) x9) Y)) A0) X0) x9) x10) Xx)) A) X0) x9) x5)) X0) x9) x6)) X) x4) (((fun (A0:fofType)=> (((fun (A0:fofType)=> ((x1 A0) ((binunion X) Y))) A0) Xx)) A) x7))))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------