%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : SEU762^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 : n092.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:03 EDT 2014 % Result : Theorem 9.52s % Output : Proof 9.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 : SEU762^2 : TPTP v6.1.0. Released v3.7.0. % % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % % Computer : n092.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:25:11 CDT 2014 % % CPUTime : 9.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 0x1fa4320>, <kernel.DependentProduct object at 0x1fa4f80>) of role type named in_type % Using role type % Declaring in:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x1faec20>, <kernel.DependentProduct object at 0x22c2b48>) of role type named powerset_type % Using role type % Declaring powerset:(fofType->fofType) % FOF formula (<kernel.Constant object at 0x1fa4488>, <kernel.DependentProduct object at 0x22c28c0>) of role type named subset_type % Using role type % Declaring subset:(fofType->(fofType->Prop)) % FOF formula (<kernel.Constant object at 0x1fa4f80>, <kernel.DependentProduct object at 0x22c2b90>) of role type named binintersect_type % Using role type % Declaring binintersect:(fofType->(fofType->fofType)) % FOF formula (<kernel.Constant object at 0x1fa4cf8>, <kernel.Sort object at 0x1fab1b8>) of role type named binintersectT_lem_type % Using role type % Declaring binintersectT_lem:Prop % FOF formula (((eq Prop) binintersectT_lem) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->((in ((binintersect X) Y)) (powerset A))))))) of role definition named binintersectT_lem % A new definition: (((eq Prop) binintersectT_lem) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->((in ((binintersect X) Y)) (powerset A))))))) % Defined: binintersectT_lem:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->((in ((binintersect X) Y)) (powerset A)))))) % FOF formula (<kernel.Constant object at 0x1fa4e60>, <kernel.Sort object at 0x1fab1b8>) of role type named woz13rule1_type % Using role type % Declaring woz13rule1:Prop % FOF formula (((eq Prop) woz13rule1) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(((subset X) Z)->((subset ((binintersect X) Y)) Z))))))))) of role definition named woz13rule1 % A new definition: (((eq Prop) woz13rule1) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(((subset X) Z)->((subset ((binintersect X) Y)) Z))))))))) % Defined: woz13rule1:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(((subset X) Z)->((subset ((binintersect X) Y)) Z)))))))) % FOF formula (<kernel.Constant object at 0x1fa4e60>, <kernel.Sort object at 0x1fab1b8>) of role type named woz13rule2_type % Using role type % Declaring woz13rule2:Prop % FOF formula (((eq Prop) woz13rule2) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(((subset Y) Z)->((subset ((binintersect X) Y)) Z))))))))) of role definition named woz13rule2 % A new definition: (((eq Prop) woz13rule2) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(((subset Y) Z)->((subset ((binintersect X) Y)) Z))))))))) % Defined: woz13rule2:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(((subset Y) Z)->((subset ((binintersect X) Y)) Z)))))))) % FOF formula (<kernel.Constant object at 0x1fa4f80>, <kernel.Sort object at 0x1fab1b8>) of role type named woz13rule3_type % Using role type % Declaring woz13rule3:Prop % FOF formula (((eq Prop) woz13rule3) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(((subset X) Y)->(((subset X) Z)->((subset X) ((binintersect Y) Z))))))))))) of role definition named woz13rule3 % A new definition: (((eq Prop) woz13rule3) (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(((subset X) Y)->(((subset X) Z)->((subset X) ((binintersect Y) Z))))))))))) % Defined: woz13rule3:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(((subset X) Y)->(((subset X) Z)->((subset X) ((binintersect Y) Z)))))))))) % FOF formula (binintersectT_lem->(woz13rule1->(woz13rule2->(woz13rule3->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W)))))))))))))))) of role conjecture named woz13rule4 % Conjecture to prove = (binintersectT_lem->(woz13rule1->(woz13rule2->(woz13rule3->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W)))))))))))))))):Prop % Parameter fofType_DUMMY:fofType. % We need to prove ['(binintersectT_lem->(woz13rule1->(woz13rule2->(woz13rule3->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W))))))))))))))))'] % Parameter fofType:Type. % Parameter in:(fofType->(fofType->Prop)). % Parameter powerset:(fofType->fofType). % Parameter subset:(fofType->(fofType->Prop)). % Parameter binintersect:(fofType->(fofType->fofType)). % Definition binintersectT_lem:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->((in ((binintersect X) Y)) (powerset A)))))):Prop. % Definition woz13rule1:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(((subset X) Z)->((subset ((binintersect X) Y)) Z)))))))):Prop. % Definition woz13rule2:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(((subset Y) Z)->((subset ((binintersect X) Y)) Z)))))))):Prop. % Definition woz13rule3:=(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(((subset X) Y)->(((subset X) Z)->((subset X) ((binintersect Y) Z)))))))))):Prop. % Trying to prove (binintersectT_lem->(woz13rule1->(woz13rule2->(woz13rule3->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W)))))))))))))))) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x90000:=(x9000 x6):((in ((binintersect Z) W)) (powerset A)) % Found (x9000 x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((x900 W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((x90 x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((((x9 Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found x90000:=(x9000 x6):((in ((binintersect Z) W)) (powerset A)) % Found (x9000 x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((x900 W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((x90 x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((((x9 Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found x90000:=(x9000 x6):((in ((binintersect Z) W)) (powerset A)) % Found (x9000 x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((x900 W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((x90 x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((((x9 Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found x90000:=(x9000 x6):((in ((binintersect Z) W)) (powerset A)) % Found (x9000 x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((x900 W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((x90 x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((((x9 Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found x90000:=(x9000 x6):((in ((binintersect Z) W)) (powerset A)) % Found (x9000 x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((x900 W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((x90 x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((((x9 Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found x90000:=(x9000 x6):((in ((binintersect Z) W)) (powerset A)) % Found (x9000 x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((x900 W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((x90 x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((((x9 Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found x90000:=(x9000 x6):((in ((binintersect Z) W)) (powerset A)) % Found (x9000 x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((x900 W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((x90 x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((((x9 Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found x90000:=(x9000 x6):((in ((binintersect Z) W)) (powerset A)) % Found (x9000 x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((x900 W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((x90 x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((((x9 Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found x90000:=(x9000 x6):((in ((binintersect Z) W)) (powerset A)) % Found (x9000 x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((x900 W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((x90 x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((((x9 Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found x90000:=(x9000 x6):((in ((binintersect Z) W)) (powerset A)) % Found (x9000 x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((x900 W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((x90 x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((((x9 Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found x90000:=(x9000 x6):((in ((binintersect Z) W)) (powerset A)) % Found (x9000 x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((x900 W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((x90 x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((((x9 Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found x90000:=(x9000 x6):((in ((binintersect Z) W)) (powerset A)) % Found (x9000 x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((x900 W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((x90 x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found ((((x9 Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found (((((x A) Z) x5) W) x6) as proof of ((in ((binintersect Z) W)) (powerset A)) % Found x90000:=(x9000 x4):((in ((binintersect X) Y)) (powerset A)) % Found (x9000 x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((x900 Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((x90 x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((((x9 X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found x90000:=(x9000 x4):((in ((binintersect X) Y)) (powerset A)) % Found (x9000 x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((x900 Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((x90 x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((((x9 X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found x90000:=(x9000 x4):((in ((binintersect X) Y)) (powerset A)) % Found (x9000 x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((x900 Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((x90 x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((((x9 X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found x90000:=(x9000 x4):((in ((binintersect X) Y)) (powerset A)) % Found (x9000 x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((x900 Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((x90 x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((((x9 X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found x90000:=(x9000 x4):((in ((binintersect X) Y)) (powerset A)) % Found (x9000 x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((x900 Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((x90 x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((((x9 X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found x90000:=(x9000 x4):((in ((binintersect X) Y)) (powerset A)) % Found (x9000 x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((x900 Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((x90 x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((((x9 X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found x90000:=(x9000 x4):((in ((binintersect X) Y)) (powerset A)) % Found (x9000 x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((x900 Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((x90 x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((((x9 X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found x90000:=(x9000 x4):((in ((binintersect X) Y)) (powerset A)) % Found (x9000 x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((x900 Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((x90 x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((((x9 X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found x90000:=(x9000 x4):((in ((binintersect X) Y)) (powerset A)) % Found (x9000 x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((x900 Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((x90 x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((((x9 X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found x90000:=(x9000 x4):((in ((binintersect X) Y)) (powerset A)) % Found (x9000 x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((x900 Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((x90 x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((((x9 X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found x90000:=(x9000 x4):((in ((binintersect X) Y)) (powerset A)) % Found (x9000 x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((x900 Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((x90 x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((((x9 X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found x90000:=(x9000 x4):((in ((binintersect X) Y)) (powerset A)) % Found (x9000 x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((x900 Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((x90 x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found ((((x9 X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found (((((x A) X) x3) Y) x4) as proof of ((in ((binintersect X) Y)) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x4:((in Y) (powerset A)) % Found x4 as proof of ((in Y) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x5:((in Z) (powerset A)) % Found x5 as proof of ((in Z) (powerset A)) % Found x6:((in W) (powerset A)) % Found x6 as proof of ((in W) (powerset A)) % Found x3:((in X) (powerset A)) % Found x3 as proof of ((in X) (powerset A)) % Found x100000000:=(x10000000 x6):((subset ((binintersect X) Y)) W) % Found (x10000000 x6) as proof of ((subset ((binintersect X) Y)) W) % Found ((x1000000 x4) x6) as proof of ((subset ((binintersect X) Y)) W) % Found (((x100000 x3) x4) x6) as proof of ((subset ((binintersect X) Y)) W) % Found ((((x10000 A) x3) x4) x6) as proof of ((subset ((binintersect X) Y)) W) % Found (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> (((((x1000 A0) x9) x11) x12) x8)) A) x3) x4) x6) as proof of ((subset ((binintersect X) Y)) W) % Found (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> ((((x100 A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6) as proof of ((subset ((binintersect X) Y)) W) % Found (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> (((x10 A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6) as proof of ((subset ((binintersect X) Y)) W) % Found (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6) as proof of ((subset ((binintersect X) Y)) W) % Found (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6) as proof of ((subset ((binintersect X) Y)) W) % Found x000000000:=(x00000000 x5):((subset ((binintersect X) Y)) Z) % Found (x00000000 x5) as proof of ((subset ((binintersect X) Y)) Z) % Found ((x0000000 x4) x5) as proof of ((subset ((binintersect X) Y)) Z) % Found (((x000000 x3) x4) x5) as proof of ((subset ((binintersect X) Y)) Z) % Found ((((x00000 A) x3) x4) x5) as proof of ((subset ((binintersect X) Y)) Z) % Found (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> (((((x0000 A0) x9) x10) x11) x7)) A) x3) x4) x5) as proof of ((subset ((binintersect X) Y)) Z) % Found (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> ((((x000 A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5) as proof of ((subset ((binintersect X) Y)) Z) % Found (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> (((x00 A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5) as proof of ((subset ((binintersect X) Y)) Z) % Found (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5) as proof of ((subset ((binintersect X) Y)) Z) % Found (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5) as proof of ((subset ((binintersect X) Y)) Z) % Found (((((x20000 (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6)) as proof of ((subset ((binintersect X) Y)) ((binintersect Z) W)) % Found ((((((x2000 A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6)) as proof of ((subset ((binintersect X) Y)) ((binintersect Z) W)) % Found (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> ((((x200 A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6)) as proof of ((subset ((binintersect X) Y)) ((binintersect Z) W)) % Found (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> (((x20 A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6)) as proof of ((subset ((binintersect X) Y)) ((binintersect Z) W)) % Found (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6)) as proof of ((subset ((binintersect X) Y)) ((binintersect Z) W)) % Found (fun (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of ((subset ((binintersect X) Y)) ((binintersect Z) W)) % Found (fun (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W))) % Found (fun (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W)))) % Found (fun (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W))))) % Found (fun (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W)))))) % Found (fun (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W))))))) % Found (fun (x4:((in Y) (powerset A))) (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W)))))))) % Found (fun (Y:fofType) (x4:((in Y) (powerset A))) (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W))))))))) % Found (fun (x3:((in X) (powerset A))) (Y:fofType) (x4:((in Y) (powerset A))) (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W)))))))))) % Found (fun (X:fofType) (x3:((in X) (powerset A))) (Y:fofType) (x4:((in Y) (powerset A))) (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W))))))))))) % Found (fun (A:fofType) (X:fofType) (x3:((in X) (powerset A))) (Y:fofType) (x4:((in Y) (powerset A))) (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (forall (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W)))))))))))) % Found (fun (x2:woz13rule3) (A:fofType) (X:fofType) (x3:((in X) (powerset A))) (Y:fofType) (x4:((in Y) (powerset A))) (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W)))))))))))) % Found (fun (x1:woz13rule2) (x2:woz13rule3) (A:fofType) (X:fofType) (x3:((in X) (powerset A))) (Y:fofType) (x4:((in Y) (powerset A))) (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (woz13rule3->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W))))))))))))) % Found (fun (x0:woz13rule1) (x1:woz13rule2) (x2:woz13rule3) (A:fofType) (X:fofType) (x3:((in X) (powerset A))) (Y:fofType) (x4:((in Y) (powerset A))) (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (woz13rule2->(woz13rule3->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W)))))))))))))) % Found (fun (x:binintersectT_lem) (x0:woz13rule1) (x1:woz13rule2) (x2:woz13rule3) (A:fofType) (X:fofType) (x3:((in X) (powerset A))) (Y:fofType) (x4:((in Y) (powerset A))) (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (woz13rule1->(woz13rule2->(woz13rule3->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W))))))))))))))) % Found (fun (x:binintersectT_lem) (x0:woz13rule1) (x1:woz13rule2) (x2:woz13rule3) (A:fofType) (X:fofType) (x3:((in X) (powerset A))) (Y:fofType) (x4:((in Y) (powerset A))) (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) as proof of (binintersectT_lem->(woz13rule1->(woz13rule2->(woz13rule3->(forall (A:fofType) (X:fofType), (((in X) (powerset A))->(forall (Y:fofType), (((in Y) (powerset A))->(forall (Z:fofType), (((in Z) (powerset A))->(forall (W:fofType), (((in W) (powerset A))->(((subset X) Z)->(((subset Y) W)->((subset ((binintersect X) Y)) ((binintersect Z) W)))))))))))))))) % Got proof (fun (x:binintersectT_lem) (x0:woz13rule1) (x1:woz13rule2) (x2:woz13rule3) (A:fofType) (X:fofType) (x3:((in X) (powerset A))) (Y:fofType) (x4:((in Y) (powerset A))) (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) % Time elapsed = 9.044915s % node=1649 cost=1672.000000 depth=29 % :::::::::::::::::::::: % % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % (fun (x:binintersectT_lem) (x0:woz13rule1) (x1:woz13rule2) (x2:woz13rule3) (A:fofType) (X:fofType) (x3:((in X) (powerset A))) (Y:fofType) (x4:((in Y) (powerset A))) (Z:fofType) (x5:((in Z) (powerset A))) (W:fofType) (x6:((in W) (powerset A))) (x7:((subset X) Z)) (x8:((subset Y) W))=> (((((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0))) (x10:((in Z) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in ((binintersect X) Y)) (powerset A0)))=> ((((fun (A0:fofType)=> ((x2 A0) ((binintersect X) Y))) A0) x9) Z)) A0) x9) x10) W)) A) (((((x A) X) x3) Y) x4)) x5) x6) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0))) (x11:((in Z) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x10:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x0 A0) X)) A0) x9) Y)) A0) x9) x10) Z)) A0) x9) x10) x11) x7)) A) x3) x4) x5)) (((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0))) (x12:((in W) (powerset A0)))=> ((((((fun (A0:fofType) (x9:((in X) (powerset A0))) (x11:((in Y) (powerset A0)))=> (((((fun (A0:fofType) (x9:((in X) (powerset A0)))=> ((((fun (A0:fofType)=> ((x1 A0) X)) A0) x9) Y)) A0) x9) x11) W)) A0) x9) x11) x12) x8)) A) x3) x4) x6))) % % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % EOF %------------------------------------------------------------------------------