fof(t14_aff_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v3_aff_3(A) => v4_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d4_aff_2,t30_aff_1,t39_aff_1,t30_aff_1,t39_aff_1,t30_aff_1,t33_aff_1,t69_aff_1,t15_aff_1,t33_aff_1,t69_aff_1,t12_aff_1,t13_aff_1,t33_aff_1,t69_aff_1,t13_aff_1,t15_aff_1,t33_aff_1,t69_aff_1,t26_aff_1,d3_aff_1,t15_aff_1,d2_aff_1,t71_aff_1,t43_aff_1,t46_aff_1,t63_aff_1,t50_aff_1,t57_aff_1,t37_aff_1,t53_aff_1,t13_aff_1,t33_aff_1,t23_aff_1,t33_aff_1,t23_aff_1,t11_aff_1,t30_aff_1,t74_aff_1,t63_aff_1,t50_aff_1,t57_aff_1,t37_aff_1,t33_aff_1,t73_aff_1,t26_aff_1,d3_aff_1,t51_aff_1,t58_aff_1,t15_aff_1,d2_aff_1,t37_aff_1,t57_aff_1,t13_aff_1,t46_aff_1,t37_aff_1,t33_aff_1,t15_aff_1,t33_aff_1,t23_aff_1,t13_aff_1,t15_aff_1,t33_aff_1,t23_aff_1,t30_aff_1,t57_aff_1,t48_aff_1,t37_aff_1,t15_aff_1,t39_aff_1,t30_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t33_aff_1,t73_aff_1,t15_aff_1,t59_aff_1,t30_aff_1,t30_aff_1,t26_aff_1,d3_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t39_aff_1,t30_aff_1,t15_aff_1,t33_aff_1,t17_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t15_aff_1,t59_aff_1,t39_aff_1,t15_aff_1,t39_aff_1,t30_aff_1,t33_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t15_aff_1,t17_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t53_aff_1,t53_aff_1,t15_aff_1,d3_aff_3,t30_aff_1,t59_aff_1,t30_aff_1,t26_aff_1,d2_aff_1,d3_aff_1,t51_aff_1,t59_aff_1,t30_aff_1,t30_aff_1,t65_aff_1]), [file(aff_3,t14_aff_3),interesting(1.00)]). fof(t12_aff_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v4_aff_2(A) => v3_aff_3(A) ) ) ), inference(mizar_proof,[status(thm)],[t16_aff_2,d3_aff_3,t16_aff_1,t16_aff_1,t26_aff_1,d2_aff_1,d3_aff_1,t33_aff_1,t13_aff_1,t15_aff_1,t69_aff_1,t14_aff_1,t13_aff_1,t15_aff_1,t69_aff_1,t14_aff_1,t69_aff_1,t69_aff_1,t15_aff_1,t39_aff_1,t71_aff_1,t71_aff_1,t26_aff_1,d2_aff_1,d3_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t59_aff_1,t30_aff_1,t72_aff_1,t53_aff_1,t13_aff_1,t30_aff_1,t59_aff_1,t33_aff_1,t39_aff_1,t26_aff_1,d2_aff_1,d3_aff_1,t26_aff_1,d3_aff_1,d1_aff_1,d2_aff_1,t30_aff_1,t33_aff_1,t30_aff_1,t30_aff_1,t30_aff_1,t30_aff_1,t14_aff_1,t13_aff_1,d4_aff_2,d1_aff_1,t14_aff_1,d5_aff_2]), [file(aff_3,t12_aff_3),interesting(0.76)]). fof(t11_aff_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v4_aff_2(A) => v1_aff_3(A) ) ) ), inference(mizar_proof,[status(thm)],[d1_aff_3,t16_aff_1,t26_aff_1,d2_aff_1,d3_aff_1,t39_aff_1,t30_aff_1,t33_aff_1,t69_aff_1,t13_aff_1,t15_aff_1,t33_aff_1,t69_aff_1,t13_aff_1,t15_aff_1,t33_aff_1,t23_aff_1,t30_aff_1,t33_aff_1,t26_aff_1,d2_aff_1,d3_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t59_aff_1,t30_aff_1,t72_aff_1,t30_aff_1,t59_aff_1,t33_aff_1,t39_aff_1,t30_aff_1,t13_aff_1,t53_aff_1,d4_aff_2,d1_aff_1,t14_aff_1,t53_aff_1,t13_aff_1,d4_aff_2,t14_aff_1]), [file(aff_3,t11_aff_3),interesting(0.69)]). fof(t16_aff_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v6_aff_3(A) <=> v8_aff_3(A) ) ) ), inference(mizar_proof,[status(thm)],[d8_aff_3,t16_aff_1,t38_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t39_aff_1,t13_aff_1,t59_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t15_aff_1,t39_aff_1,t33_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t15_aff_1,t16_aff_1,t59_aff_1,t17_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t33_aff_1,t15_aff_1,t39_aff_1,d1_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t39_aff_1,t33_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t59_aff_1,t13_aff_1,t39_aff_1,t59_aff_1,t62_aff_1,t33_aff_1,t15_aff_1,t33_aff_1,t17_aff_1,t33_aff_1,t39_aff_1,t30_aff_1,t15_aff_1,t33_aff_1,t17_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t13_aff_1,t14_aff_1,t52_aff_1,t52_aff_1,t15_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t59_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t16_aff_1,t17_aff_1,t13_aff_1,d1_aff_1,t39_aff_1,t39_aff_1,t15_aff_1,t33_aff_1,t39_aff_1,t59_aff_1,t39_aff_1,t30_aff_1,d6_aff_3,t52_aff_1,d6_aff_3,t16_aff_1,t38_aff_1,t58_aff_1,t53_aff_1,t52_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t39_aff_1,t15_aff_1,t39_aff_1,t11_aff_1,t59_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t15_aff_1,t16_aff_1,t59_aff_1,t17_aff_1,t39_aff_1,t11_aff_1,t15_aff_1,t59_aff_1,d1_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t33_aff_1,t17_aff_1,t65_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t15_aff_1,t59_aff_1,d1_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t59_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t15_aff_1,t16_aff_1,t59_aff_1,t17_aff_1,t39_aff_1,t59_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t59_aff_1,t15_aff_1,d8_aff_3,t53_aff_1]), [file(aff_3,t16_aff_3),interesting(0.24)]). fof(t18_aff_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v4_aff_3(A) => v6_aff_3(A) ) ) ), inference(mizar_proof,[status(thm)],[d6_aff_3,t16_aff_1,t58_aff_1,t15_aff_1,t39_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t39_aff_1,t11_aff_1,t59_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t15_aff_1,t16_aff_1,t59_aff_1,t17_aff_1,t15_aff_1,d1_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t11_aff_1,t59_aff_1,t38_aff_1,t52_aff_1,t53_aff_1,t72_aff_1,t58_aff_1,t53_aff_1,t15_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t59_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t59_aff_1,d1_aff_1,t15_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t33_aff_1,t17_aff_1,t65_aff_1,t30_aff_1,t59_aff_1,t30_aff_1,t59_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t59_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t15_aff_1,t16_aff_1,t59_aff_1,t17_aff_1,t39_aff_1,t59_aff_1,d4_aff_3,t59_aff_1]), [file(aff_3,t18_aff_3),interesting(0.24)]). fof(t15_aff_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v6_aff_3(A) => v5_aff_3(A) ) ) ), inference(mizar_proof,[status(thm)],[d5_aff_3,t58_aff_1,t16_aff_1,t26_aff_1,d2_aff_1,d3_aff_1,t51_aff_1,t59_aff_1,t59_aff_1,t30_aff_1,t30_aff_1,t59_aff_1,t26_aff_1,d2_aff_1,d3_aff_1,t30_aff_1,t30_aff_1,t59_aff_1,t30_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t58_aff_1,t59_aff_1,t72_aff_1,t58_aff_1,t57_aff_1,t37_aff_1,t30_aff_1,t30_aff_1,t59_aff_1,t33_aff_1,t39_aff_1,t59_aff_1,t59_aff_1,t33_aff_1,t73_aff_1,t15_aff_1,t33_aff_1,t53_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t59_aff_1,d2_aff_1,t30_aff_1,t30_aff_1,t26_aff_1,t33_aff_1,t39_aff_1,d2_aff_1,t59_aff_1,t59_aff_1,d2_aff_1,t30_aff_1,t26_aff_1,t33_aff_1,t39_aff_1,d2_aff_1,t59_aff_1,d6_aff_3,t14_aff_1,d1_aff_1,t15_aff_1,d2_aff_1,t30_aff_1,t15_aff_1,t26_aff_1,t59_aff_1,d2_aff_1,t30_aff_1,t33_aff_1,t53_aff_1,t39_aff_1,t59_aff_1,t72_aff_1,t58_aff_1,t57_aff_1,t37_aff_1,t30_aff_1,t30_aff_1,t59_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t59_aff_1,d2_aff_1,t73_aff_1,t15_aff_1,t33_aff_1,t53_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t59_aff_1,d2_aff_1,t30_aff_1,t30_aff_1,t26_aff_1,t33_aff_1,t39_aff_1,d2_aff_1,t59_aff_1,t59_aff_1,d2_aff_1,t30_aff_1,t26_aff_1,t33_aff_1,t39_aff_1,d2_aff_1,t59_aff_1,d6_aff_3,t14_aff_1,d1_aff_1,d2_aff_1,t30_aff_1,t15_aff_1,t26_aff_1,t59_aff_1,d2_aff_1,t30_aff_1,t33_aff_1,t53_aff_1,t39_aff_1,t59_aff_1]), [file(aff_3,t15_aff_3),interesting(0.22)]). fof(t13_aff_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v3_aff_3(A) => v4_aff_3(A) ) ) ), inference(mizar_proof,[status(thm)],[d4_aff_3,t16_aff_1,t39_aff_1,t30_aff_1,t13_aff_1,t33_aff_1,t23_aff_1,t14_aff_1,t13_aff_1,t15_aff_1,t69_aff_1,t13_aff_1,t15_aff_1,t69_aff_1,t69_aff_1,t58_aff_1,t59_aff_1,t38_aff_1,t39_aff_1,t72_aff_1,t39_aff_1,t30_aff_1,t30_aff_1,t33_aff_1,t17_aff_1,t39_aff_1,t30_aff_1,t30_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t39_aff_1,t30_aff_1,d3_aff_3,t30_aff_1,t72_aff_1,t33_aff_1,t15_aff_1,t17_aff_1,t17_aff_1,t39_aff_1,t30_aff_1,t30_aff_1,t39_aff_1,t30_aff_1,t30_aff_1,t33_aff_1,t17_aff_1,t15_aff_1,t39_aff_1,t39_aff_1,t13_aff_1,t30_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t39_aff_1,t30_aff_1,t15_aff_1,t13_aff_1,d3_aff_3,t30_aff_1]), [file(aff_3,t13_aff_3),interesting(0.21)]). fof(t17_aff_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v5_aff_3(A) <=> v7_aff_3(A) ) ) ), inference(mizar_proof,[status(thm)],[d7_aff_3,t16_aff_1,t15_aff_1,t39_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t39_aff_1,t13_aff_1,t59_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t15_aff_1,t39_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t15_aff_1,d1_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t15_aff_1,t59_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t16_aff_1,t59_aff_1,t38_aff_1,t13_aff_1,t14_aff_1,t52_aff_1,t33_aff_1,t39_aff_1,t59_aff_1,t15_aff_1,t33_aff_1,t17_aff_1,t15_aff_1,t33_aff_1,t17_aff_1,t15_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t30_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t30_aff_1,t53_aff_1,d5_aff_3,t52_aff_1,d5_aff_3,t58_aff_1,t16_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t59_aff_1,t38_aff_1,t53_aff_1,t15_aff_1,t52_aff_1,t15_aff_1,t33_aff_1,t17_aff_1,t33_aff_1,t39_aff_1,t59_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t59_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t59_aff_1,d7_aff_3,t53_aff_1]), [file(aff_3,t17_aff_3),interesting(0.14)]). fof(t9_aff_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v1_aff_3(A) => v2_aff_3(A) ) ) ), inference(mizar_proof,[status(thm)],[d2_aff_3,t16_aff_1,t26_aff_1,d2_aff_1,d3_aff_1,t16_aff_1,t30_aff_1,t16_aff_1,t33_aff_1,t39_aff_1,t30_aff_1,t69_aff_1,t30_aff_1,t13_aff_1,t15_aff_1,t69_aff_1,t30_aff_1,t15_aff_1,t26_aff_1,d2_aff_1,d3_aff_1,t15_aff_1,t39_aff_1,t33_aff_1,t23_aff_1,t15_aff_1,t33_aff_1,d1_aff_3]), [file(aff_3,t9_aff_3),interesting(0.02)]). fof(d1_aff_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v1_aff_3(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ! [L] : ( m1_subset_1(L,u1_struct_0(A)) => ! [M] : ( m1_subset_1(M,u1_struct_0(A)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_hidden(E,B) & r2_hidden(F,B) & r2_hidden(G,B) & r2_hidden(E,C) & r2_hidden(H,C) & r2_hidden(I,C) & r2_hidden(E,D) & r2_hidden(J,D) & r2_hidden(K,D) & r1_aff_1(A,H,F,L) & r1_aff_1(A,I,G,L) & r1_aff_1(A,H,J,M) & r1_aff_1(A,I,K,M) & r2_analoaf(A,F,J,G,K) ) => ( C = B | C = D | B = D | E = F | E = H | E = J | L = M | r1_aff_1(A,H,F,J) | r1_aff_1(A,I,G,K) | F = G | r2_analoaf(A,F,J,L,M) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_3,d1_aff_3), [interesting(0.00)]). fof(t16_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_aff_1(A,B,B,C) & r1_aff_1(A,B,C,C) & r1_aff_1(A,B,C,B) ) ) ) ) ), file(aff_1,t16_aff_1), [interesting(0.00)]). fof(t26_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_hidden(B,k2_aff_1(A,B,C)) & r2_hidden(C,k2_aff_1(A,B,C)) ) ) ) ) ), file(aff_1,t26_aff_1), [interesting(0.00)]). fof(d2_aff_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( D = k1_aff_1(A,B,C) <=> ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_hidden(E,D) <=> r1_aff_1(A,B,C,E) ) ) ) ) ) ) ) ), file(aff_1,d2_aff_1), [interesting(0.00)]). fof(d3_aff_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( v1_aff_1(B,A) <=> ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & C != D & B = k2_aff_1(A,C,D) ) ) ) ) ) ), file(aff_1,d3_aff_1), [interesting(0.00)]). fof(t30_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) => ~ ( v1_aff_1(D,A) & v1_aff_1(E,A) & r2_hidden(B,D) & r2_hidden(C,D) & r2_hidden(B,E) & r2_hidden(C,E) & B != C & D != E ) ) ) ) ) ) ), file(aff_1,t30_aff_1), [interesting(0.00)]). fof(t33_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_aff_1(A,B,C,D) <=> ? [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) & v1_aff_1(E,A) & r2_hidden(B,E) & r2_hidden(C,E) & r2_hidden(D,E) ) ) ) ) ) ) ), file(aff_1,t33_aff_1), [interesting(0.00)]). fof(t39_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(E,A) & r2_hidden(B,E) & r2_hidden(C,E) & r1_aff_1(A,B,C,D) ) => ( B = C | r2_hidden(D,E) ) ) ) ) ) ) ) ), file(aff_1,t39_aff_1), [interesting(0.00)]). fof(t13_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_analoaf(A,B,C,D,E) => ( r2_analoaf(A,B,C,E,D) & r2_analoaf(A,C,B,D,E) & r2_analoaf(A,C,B,E,D) & r2_analoaf(A,D,E,B,C) & r2_analoaf(A,D,E,C,B) & r2_analoaf(A,E,D,B,C) & r2_analoaf(A,E,D,C,B) ) ) ) ) ) ) ) ), file(aff_1,t13_aff_1), [interesting(0.00)]). fof(t15_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_aff_1(A,B,C,D) => ( r1_aff_1(A,B,D,C) & r1_aff_1(A,C,B,D) & r1_aff_1(A,C,D,B) & r1_aff_1(A,D,B,C) & r1_aff_1(A,D,C,B) ) ) ) ) ) ) ), file(aff_1,t15_aff_1), [interesting(0.00)]). fof(t23_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( r1_aff_1(A,B,D,E) & r2_analoaf(A,C,D,C,E) ) => ( r1_aff_1(A,B,C,D) | D = E ) ) ) ) ) ) ) ), file(aff_1,t23_aff_1), [interesting(0.00)]). fof(d2_aff_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v2_aff_3(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ! [L] : ( m1_subset_1(L,u1_struct_0(A)) => ! [M] : ( m1_subset_1(M,u1_struct_0(A)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_hidden(E,B) & r2_hidden(F,B) & r2_hidden(G,B) & r2_hidden(E,C) & r2_hidden(H,C) & r2_hidden(I,C) & r2_hidden(E,D) & r2_hidden(J,D) & r2_hidden(K,D) & r1_aff_1(A,H,F,L) & r1_aff_1(A,I,G,L) & r1_aff_1(A,H,J,M) & r1_aff_1(A,I,K,M) & r2_analoaf(A,F,J,L,M) ) => ( C = B | C = D | B = D | E = F | E = H | E = J | L = M | J = M | r1_aff_1(A,H,F,J) | r1_aff_1(A,I,G,K) | r2_analoaf(A,F,J,G,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_3,d2_aff_3), [interesting(0.00)]). fof(t12_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r2_analoaf(A,B,C,D,D) & r2_analoaf(A,D,D,B,C) ) ) ) ) ) ), file(aff_1,t12_aff_1), [interesting(0.00)]). fof(t10_aff_3,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v2_aff_3(A) => v1_aff_3(A) ) ) ), inference(mizar_proof,[status(thm)],[d1_aff_3,t16_aff_1,t26_aff_1,d2_aff_1,d3_aff_1,t16_aff_1,t30_aff_1,t30_aff_1,t30_aff_1,t16_aff_1,t33_aff_1,t39_aff_1,t30_aff_1,t13_aff_1,t15_aff_1,t33_aff_1,t23_aff_1,t15_aff_1,t33_aff_1,d2_aff_3,t15_aff_1,t26_aff_1,d2_aff_1,d3_aff_1,t33_aff_1,t39_aff_1,t30_aff_1,t30_aff_1,d2_aff_1,t30_aff_1,t33_aff_1,t39_aff_1,t30_aff_1,t30_aff_1,t12_aff_1,t39_aff_1,t30_aff_1,t30_aff_1,d2_aff_1,t30_aff_1,t33_aff_1,t39_aff_1,t30_aff_1,t30_aff_1,t12_aff_1]), [file(aff_3,t10_aff_3),interesting(0.00)]). fof(t69_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ( ( r1_aff_1(A,B,C,E) & r1_aff_1(A,B,D,F) & r2_analoaf(A,C,D,E,F) & E = B ) => ( r1_aff_1(A,B,C,D) | F = B ) ) ) ) ) ) ) ) ), file(aff_1,t69_aff_1), [interesting(0.00)]). fof(t63_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ~ ( v1_aff_1(C,A) & ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ~ ( r2_hidden(B,D) & r4_aff_1(A,C,D) ) ) ) ) ) ) ), file(aff_1,t63_aff_1), [interesting(0.00)]). fof(t50_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( r3_aff_1(A,B,C) => ( v1_aff_1(B,A) & v1_aff_1(C,A) ) ) ) ) ) ), file(aff_1,t50_aff_1), [interesting(0.00)]). fof(t58_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ~ ( ~ ( r4_aff_1(A,B,C) & r4_aff_1(A,C,D) ) & ~ ( r4_aff_1(A,B,C) & r4_aff_1(A,D,C) ) & ~ ( r4_aff_1(A,C,B) & r4_aff_1(A,C,D) ) & ~ ( r4_aff_1(A,C,B) & r4_aff_1(A,D,C) ) ) => r4_aff_1(A,B,D) ) ) ) ) ) ), file(aff_1,t58_aff_1), [interesting(0.00)]). fof(t59_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ( r4_aff_1(A,C,D) & r2_hidden(B,C) & r2_hidden(B,D) ) => C = D ) ) ) ) ) ), file(aff_1,t59_aff_1), [interesting(0.00)]). fof(t72_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ~ ( v1_aff_1(B,A) & v1_aff_1(C,A) & ~ r4_aff_1(A,B,C) & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ~ ( r2_hidden(D,B) & r2_hidden(D,C) ) ) ) ) ) ) ), file(aff_1,t72_aff_1), [interesting(0.00)]). fof(t53_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ! [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(A))) => ( ( r2_hidden(B,F) & r2_hidden(C,F) & r2_hidden(D,G) & r2_hidden(E,G) & r3_aff_1(A,F,G) ) => r2_analoaf(A,B,C,D,E) ) ) ) ) ) ) ) ) ), file(aff_1,t53_aff_1), [interesting(0.00)]). fof(d4_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ( v4_aff_2(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ( ( r2_hidden(E,B) & r2_hidden(E,C) & r2_hidden(E,D) & r2_hidden(F,B) & r2_hidden(I,B) & r2_hidden(G,C) & r2_hidden(J,C) & r2_hidden(H,D) & r2_hidden(K,D) & v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_analoaf(A,F,G,I,J) & r2_analoaf(A,F,H,I,K) ) => ( E = F | E = G | E = H | B = C | B = D | r2_analoaf(A,G,H,J,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d4_aff_2), [interesting(0.00)]). fof(d1_aff_1,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_aff_1(A,B,C,D) <=> r2_analoaf(A,B,C,B,D) ) ) ) ) ) ), file(aff_1,d1_aff_1), [interesting(0.00)]). fof(t14_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ~ ( B != C & ~ ( ~ ( r2_analoaf(A,B,C,D,E) & r2_analoaf(A,B,C,F,G) ) & ~ ( r2_analoaf(A,B,C,D,E) & r2_analoaf(A,F,G,B,C) ) & ~ ( r2_analoaf(A,D,E,B,C) & r2_analoaf(A,F,G,B,C) ) & ~ ( r2_analoaf(A,D,E,B,C) & r2_analoaf(A,B,C,F,G) ) ) & ~ r2_analoaf(A,D,E,F,G) ) ) ) ) ) ) ) ) ), file(aff_1,t14_aff_1), [interesting(0.00)]). fof(t16_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v4_aff_2(A) <=> v5_aff_2(A) ) ) ), file(aff_2,t16_aff_2), [interesting(0.00)]). fof(d3_aff_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v3_aff_3(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ! [L] : ( m1_subset_1(L,u1_struct_0(A)) => ! [M] : ( m1_subset_1(M,u1_struct_0(A)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_hidden(E,B) & r2_hidden(F,B) & r2_hidden(G,B) & r2_hidden(E,C) & r2_hidden(H,C) & r2_hidden(I,C) & r2_hidden(J,D) & r2_hidden(K,D) & r1_aff_1(A,H,F,L) & r1_aff_1(A,I,G,L) & r1_aff_1(A,H,J,M) & r1_aff_1(A,I,K,M) & r2_analoaf(A,F,J,G,K) & r2_analoaf(A,F,J,L,M) ) => ( C = B | C = D | B = D | E = F | E = H | E = J | L = M | r1_aff_1(A,H,F,J) | r1_aff_1(A,I,G,K) | J = K | r2_hidden(E,D) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_3,d3_aff_3), [interesting(0.00)]). fof(t71_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(D,A) & r2_hidden(B,D) & r2_hidden(C,D) ) => ( B = C | D = k2_aff_1(A,B,C) ) ) ) ) ) ) ), file(aff_1,t71_aff_1), [interesting(0.00)]). fof(d5_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v5_aff_2(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ( ( r2_hidden(E,B) & r2_hidden(E,C) & r2_hidden(F,B) & r2_hidden(I,B) & r2_hidden(G,C) & r2_hidden(J,C) & r2_hidden(H,D) & r2_hidden(K,D) & v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_analoaf(A,F,G,I,J) & r2_analoaf(A,F,H,I,K) & r2_analoaf(A,G,H,J,K) ) => ( E = F | E = G | E = H | B = C | B = D | r1_aff_1(A,F,G,H) | H = K | r2_hidden(E,D) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d5_aff_2), [interesting(0.00)]). fof(d4_aff_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v4_aff_3(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ! [L] : ( m1_subset_1(L,u1_struct_0(A)) => ! [M] : ( m1_subset_1(M,u1_struct_0(A)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_hidden(E,B) & r2_hidden(F,B) & r2_hidden(G,B) & r2_hidden(H,C) & r2_hidden(I,C) & r2_hidden(E,D) & r2_hidden(J,D) & r2_hidden(K,D) & r1_aff_1(A,H,F,L) & r1_aff_1(A,I,G,L) & r1_aff_1(A,H,J,M) & r1_aff_1(A,I,K,M) & r2_analoaf(A,F,J,G,K) & r2_analoaf(A,F,J,L,M) ) => ( C = B | C = D | B = D | E = F | E = H | E = J | L = M | r1_aff_1(A,H,F,J) | r1_aff_1(A,I,G,K) | H = I | F = G | r2_hidden(E,C) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_3,d4_aff_3), [interesting(0.00)]). fof(t38_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ( D = k2_aff_1(A,B,C) => ( B = C | ( v1_aff_1(D,A) & r2_hidden(B,D) & r2_hidden(C,D) & B != C ) ) ) & ( ( v1_aff_1(D,A) & r2_hidden(B,D) & r2_hidden(C,D) ) => ( B = C | ( B != C & D = k2_aff_1(A,B,C) ) ) ) ) ) ) ) ) ), file(aff_1,t38_aff_1), [interesting(0.00)]). fof(t17_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ( ( r1_aff_1(A,B,C,D) & r1_aff_1(A,B,C,E) & r1_aff_1(A,B,C,F) ) => ( B = C | r1_aff_1(A,D,E,F) ) ) ) ) ) ) ) ) ), file(aff_1,t17_aff_1), [interesting(0.00)]). fof(t43_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( B != C => r2_aff_1(A,B,C,k2_aff_1(A,B,C)) ) ) ) ) ), file(aff_1,t43_aff_1), [interesting(0.00)]). fof(t46_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ( ( r2_aff_1(A,B,C,F) & r2_analoaf(A,B,C,D,E) ) => ( B = C | r2_aff_1(A,D,E,F) ) ) ) ) ) ) ) ) ), file(aff_1,t46_aff_1), [interesting(0.00)]). fof(t57_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) => ( ( r2_aff_1(A,B,C,D) & r4_aff_1(A,D,E) ) => r2_aff_1(A,B,C,E) ) ) ) ) ) ) ), file(aff_1,t57_aff_1), [interesting(0.00)]). fof(t37_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(D,A) & r2_hidden(B,D) ) => ( r2_hidden(C,D) <=> r2_aff_1(A,B,C,D) ) ) ) ) ) ) ), file(aff_1,t37_aff_1), [interesting(0.00)]). fof(t11_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_analoaf(A,B,C,C,B) & r2_analoaf(A,B,C,B,C) ) ) ) ) ), file(aff_1,t11_aff_1), [interesting(0.00)]). fof(t74_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( ~ r2_analoaf(A,B,C,D,E) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( r1_aff_1(A,B,C,F) & r1_aff_1(A,D,E,F) ) ) ) ) ) ) ) ) ), file(aff_1,t74_aff_1), [interesting(0.00)]). fof(t73_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ~ ( v1_aff_1(D,A) & ~ r2_aff_1(A,B,C,D) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( r2_hidden(E,D) & r1_aff_1(A,B,C,E) ) ) ) ) ) ) ) ), file(aff_1,t73_aff_1), [interesting(0.00)]). fof(t51_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ( r3_aff_1(A,B,C) <=> ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & ? [E] : ( m1_subset_1(E,u1_struct_0(A)) & ? [F] : ( m1_subset_1(F,u1_struct_0(A)) & ? [G] : ( m1_subset_1(G,u1_struct_0(A)) & D != E & F != G & r2_analoaf(A,D,E,F,G) & B = k2_aff_1(A,D,E) & C = k2_aff_1(A,F,G) ) ) ) ) ) ) ) ) ), file(aff_1,t51_aff_1), [interesting(0.00)]). fof(t48_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( r2_aff_1(A,B,C,D) => r2_aff_1(A,C,B,D) ) ) ) ) ) ), file(aff_1,t48_aff_1), [interesting(0.00)]). fof(t65_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(F,A) & r2_hidden(B,F) & r2_hidden(C,F) & r2_hidden(D,F) & r2_hidden(E,F) ) => r2_analoaf(A,B,C,D,E) ) ) ) ) ) ) ) ), file(aff_1,t65_aff_1), [interesting(0.00)]). fof(d5_aff_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v5_aff_3(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ! [L] : ( m1_subset_1(L,u1_struct_0(A)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_hidden(E,B) & r2_hidden(F,B) & r2_hidden(G,C) & r2_hidden(H,C) & r2_hidden(I,D) & r2_hidden(J,D) & r4_aff_1(A,B,C) & r4_aff_1(A,B,D) & r1_aff_1(A,G,E,K) & r1_aff_1(A,H,F,K) & r1_aff_1(A,G,I,L) & r1_aff_1(A,H,J,L) & r2_analoaf(A,E,I,F,J) ) => ( B = C | B = D | C = D | r1_aff_1(A,G,E,I) | r1_aff_1(A,H,F,J) | K = L | E = F | r2_analoaf(A,E,I,K,L) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_3,d5_aff_3), [interesting(0.00)]). fof(d6_aff_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v6_aff_3(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ! [L] : ( m1_subset_1(L,u1_struct_0(A)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_hidden(E,B) & r2_hidden(F,B) & r2_hidden(G,C) & r2_hidden(H,C) & r2_hidden(I,D) & r2_hidden(J,D) & r4_aff_1(A,B,C) & r4_aff_1(A,B,D) & r1_aff_1(A,G,E,K) & r1_aff_1(A,H,F,K) & r1_aff_1(A,G,I,L) & r1_aff_1(A,H,J,L) & r2_analoaf(A,E,I,K,L) ) => ( B = C | B = D | C = D | r1_aff_1(A,G,E,I) | r1_aff_1(A,H,F,J) | K = L | r2_analoaf(A,E,I,F,J) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_3,d6_aff_3), [interesting(0.00)]). fof(d8_aff_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v8_aff_3(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ! [L] : ( m1_subset_1(L,u1_struct_0(A)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_hidden(E,B) & r2_hidden(F,B) & r2_hidden(G,C) & r2_hidden(H,C) & r2_hidden(I,D) & r2_hidden(J,D) & r4_aff_1(A,B,C) & r1_aff_1(A,G,E,K) & r1_aff_1(A,H,F,K) & r1_aff_1(A,G,I,L) & r1_aff_1(A,H,J,L) & r2_analoaf(A,E,I,F,J) & r2_analoaf(A,E,I,K,L) ) => ( B = C | B = D | C = D | r1_aff_1(A,G,E,I) | r1_aff_1(A,H,F,J) | K = L | I = J | r4_aff_1(A,B,D) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_3,d8_aff_3), [interesting(0.00)]). fof(t62_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(F,A) & r2_hidden(B,F) & r2_hidden(C,F) & r2_hidden(D,F) & r2_analoaf(A,B,C,D,E) ) => ( B = C | r2_hidden(E,F) ) ) ) ) ) ) ) ) ), file(aff_1,t62_aff_1), [interesting(0.00)]). fof(t52_aff_1,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ! [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(F,A) & v1_aff_1(G,A) & r2_hidden(B,F) & r2_hidden(C,F) & r2_hidden(D,G) & r2_hidden(E,G) ) => ( B = C | D = E | ( r3_aff_1(A,F,G) <=> r2_analoaf(A,B,C,D,E) ) ) ) ) ) ) ) ) ) ) ), file(aff_1,t52_aff_1), [interesting(0.00)]). fof(d7_aff_3,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v7_aff_3(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ! [L] : ( m1_subset_1(L,u1_struct_0(A)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_hidden(E,B) & r2_hidden(F,B) & r2_hidden(G,C) & r2_hidden(H,C) & r2_hidden(I,D) & r2_hidden(J,D) & r4_aff_1(A,B,D) & r1_aff_1(A,G,E,K) & r1_aff_1(A,H,F,K) & r1_aff_1(A,G,I,L) & r1_aff_1(A,H,J,L) & r2_analoaf(A,E,I,F,J) & r2_analoaf(A,E,I,K,L) ) => ( B = C | B = D | C = D | r1_aff_1(A,G,E,I) | r1_aff_1(A,H,F,J) | K = L | E = F | r4_aff_1(A,B,C) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_3,d7_aff_3), [interesting(0.00)]). fof(t1_aff_3,theorem,( $true ), file(aff_3,t1_aff_3), [interesting(0.00)]). fof(t2_aff_3,theorem,( $true ), file(aff_3,t2_aff_3), [interesting(0.00)]). fof(t3_aff_3,theorem,( $true ), file(aff_3,t3_aff_3), [interesting(0.00)]). fof(t4_aff_3,theorem,( $true ), file(aff_3,t4_aff_3), [interesting(0.00)]). fof(t5_aff_3,theorem,( $true ), file(aff_3,t5_aff_3), [interesting(0.00)]). fof(t6_aff_3,theorem,( $true ), file(aff_3,t6_aff_3), [interesting(0.00)]). fof(t7_aff_3,theorem,( $true ), file(aff_3,t7_aff_3), [interesting(0.00)]). fof(t8_aff_3,theorem,( $true ), file(aff_3,t8_aff_3), [interesting(0.00)]).