fof(t28_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v7_aff_2(A) => v11_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[t17_aff_2,t27_aff_2,t21_aff_2]), [file(aff_2,t28_aff_2),interesting(1.00)]). fof(t25_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v2_aff_2(A) => v4_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[t23_aff_2,t24_aff_2,d4_aff_2,t12_aff_1,t30_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t11_aff_1,t30_aff_1,t13_aff_1,t30_aff_1,t62_aff_1,t12_aff_1,t30_aff_1,t13_aff_1,t30_aff_1,t62_aff_1,t30_aff_1,t15_aff_1,d1_aff_1,t14_aff_1,d1_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,d1_aff_1,t13_aff_1,t13_aff_1,t14_aff_1,t14_aff_1,d1_aff_1,t14_aff_1,t14_aff_1,d1_aff_1,t30_aff_1,t65_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,t38_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t59_aff_1,t33_aff_1,t72_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t59_aff_1,t30_aff_1,t72_aff_1,t33_aff_1,t39_aff_1,t30_aff_1,t53_aff_1,d1_aff_2,t30_aff_1,t30_aff_1,t54_aff_1,t38_aff_1,t46_aff_1,t55_aff_1,t54_aff_1,t67_aff_1,t59_aff_1,t30_aff_1,t73_aff_1,t14_aff_1,t15_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t33_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,d1_aff_2,t14_aff_1,t33_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t15_aff_1,d1_aff_1,d1_aff_2,t33_aff_1,t13_aff_1,d1_aff_1,t14_aff_1,t13_aff_1,t14_aff_1,d1_aff_2,t14_aff_1,d1_aff_1,t15_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t13_aff_1,t14_aff_1,t45_aff_1,t38_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t59_aff_1,t33_aff_1,t72_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t59_aff_1,t30_aff_1,t72_aff_1,t33_aff_1,t13_aff_1,t39_aff_1,t62_aff_1,t30_aff_1,t53_aff_1,d1_aff_2,t30_aff_1,t30_aff_1,t54_aff_1,t30_aff_1,t65_aff_1,t38_aff_1,t46_aff_1,t55_aff_1,t54_aff_1,t67_aff_1,t59_aff_1,t30_aff_1,t73_aff_1,t14_aff_1,t15_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t33_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,d1_aff_2,t14_aff_1,t33_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t15_aff_1,d1_aff_1,d1_aff_2,t33_aff_1,t13_aff_1,d1_aff_1,t14_aff_1,t13_aff_1,t14_aff_1,d1_aff_2,t14_aff_1,d1_aff_1,t15_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t13_aff_1,t14_aff_1]), [file(aff_2,t25_aff_2),interesting(0.90)]). fof(t21_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v11_aff_2(A) <=> v12_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d12_aff_2,t16_aff_1,t63_aff_1,t50_aff_1,t57_aff_1,t37_aff_1,t13_aff_1,t41_aff_1,t37_aff_1,t30_aff_1,t73_aff_1,t13_aff_1,t54_aff_1,t46_aff_1,t13_aff_1,t14_aff_1,t13_aff_1,t59_aff_1,d1_aff_1,t15_aff_1,d1_aff_1,t14_aff_1,d11_aff_2,t13_aff_1,t14_aff_1,t14_aff_1,t59_aff_1,d1_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t30_aff_1,d11_aff_2,t12_aff_1,t59_aff_1,t58_aff_1,t38_aff_1,t63_aff_1,t50_aff_1,t15_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t15_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,d1_aff_1,t14_aff_1,t14_aff_1,d1_aff_1,t58_aff_1,t53_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t72_aff_1,t53_aff_1,t53_aff_1,t33_aff_1,d1_aff_1,t14_aff_1,t26_aff_1,t59_aff_1,t30_aff_1,t59_aff_1,t53_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t11_aff_1,t59_aff_1,t38_aff_1,t15_aff_1,d1_aff_1,t13_aff_1,t33_aff_1,t13_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t52_aff_1,t26_aff_1,t59_aff_1,d12_aff_2,t58_aff_1,t59_aff_1,t30_aff_1,t59_aff_1]), [file(aff_2,t21_aff_2),interesting(0.75)]). fof(t23_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v2_aff_2(A) => v13_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d13_aff_2,t59_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t11_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,t39_aff_1,t59_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t38_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t53_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t72_aff_1,t53_aff_1,t33_aff_1,t39_aff_1,t59_aff_1,t38_aff_1,t58_aff_1,t59_aff_1,t30_aff_1,t53_aff_1,t59_aff_1,t72_aff_1,t33_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t39_aff_1,t59_aff_1,t53_aff_1,t41_aff_1,t48_aff_1,t37_aff_1,t59_aff_1,t46_aff_1,t37_aff_1,t30_aff_1,t53_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t73_aff_1,t15_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t59_aff_1,t33_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t33_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t52_aff_1,t59_aff_1,t33_aff_1,t39_aff_1,t59_aff_1,t30_aff_1,t59_aff_1,t59_aff_1,t15_aff_1,t33_aff_1,t17_aff_1,t39_aff_1,t59_aff_1,t59_aff_1,d2_aff_2,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t30_aff_1,t59_aff_1,t59_aff_1]), [file(aff_2,t23_aff_2),interesting(0.72)]). fof(t17_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v7_aff_2(A) => v8_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d8_aff_2,t49_aff_1,t49_aff_1,t16_aff_1,t26_aff_1,d3_aff_1,t39_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t59_aff_1,t72_aff_1,t33_aff_1,t54_aff_1,t45_aff_1,d7_aff_2,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t57_aff_1,t46_aff_1,t37_aff_1,t33_aff_1,t17_aff_1,d1_aff_1,t13_aff_1,t59_aff_1,t30_aff_1,t13_aff_1,t62_aff_1,t16_aff_1,t14_aff_1,t30_aff_1,t16_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,d1_aff_1,t13_aff_1,t46_aff_1,t48_aff_1,t37_aff_1,t14_aff_1,t14_aff_1,t46_aff_1,t48_aff_1,t37_aff_1]), [file(aff_2,t17_aff_2),interesting(0.71)]). fof(t27_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v8_aff_2(A) => v12_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d12_aff_2,t72_aff_1,t63_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t16_aff_1,t59_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_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,t13_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t38_aff_1,t51_aff_1,t58_aff_1,t59_aff_1,t59_aff_1,t72_aff_1,t58_aff_1,t59_aff_1,t59_aff_1,t72_aff_1,t58_aff_1,t72_aff_1,t33_aff_1,t33_aff_1,t54_aff_1,t53_aff_1,t62_aff_1,t30_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,t53_aff_1,t13_aff_1,d8_aff_2,t33_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,t53_aff_1,t13_aff_1,t53_aff_1,t54_aff_1,t33_aff_1,d1_aff_1,t14_aff_1,t14_aff_1,d1_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,d8_aff_2,t15_aff_1,t16_aff_1,t17_aff_1,t59_aff_1,t30_aff_1,t39_aff_1,t30_aff_1,t59_aff_1,t33_aff_1]), [file(aff_2,t27_aff_2),interesting(0.70)]). fof(t19_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v9_aff_2(A) => v10_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d10_aff_2,t49_aff_1,t49_aff_1,d1_aff_1,t46_aff_1,t48_aff_1,t37_aff_1,t38_aff_1,t39_aff_1,t55_aff_1,t54_aff_1,t67_aff_1,t59_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t30_aff_1,t13_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t13_aff_1,t46_aff_1,t48_aff_1,t37_aff_1,t73_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t59_aff_1,t30_aff_1,t72_aff_1,t33_aff_1,t53_aff_1,d1_aff_1,t14_aff_1,d9_aff_2,t14_aff_1,d1_aff_1,t15_aff_1,t33_aff_1,t17_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,d1_aff_1,t14_aff_1,t14_aff_1,d1_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t30_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t13_aff_1,t39_aff_1,t62_aff_1,t30_aff_1]), [file(aff_2,t19_aff_2),interesting(0.68)]). 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) ) ) ), inference(mizar_proof,[status(thm)],[d5_aff_2,t38_aff_1,t16_aff_1,t13_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t30_aff_1,t14_aff_1,d1_aff_1,t14_aff_1,t15_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t13_aff_1,t38_aff_1,t62_aff_1,t30_aff_1,t46_aff_1,t48_aff_1,t37_aff_1,t30_aff_1,t13_aff_1,t62_aff_1,t14_aff_1,t30_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t73_aff_1,d1_aff_1,t14_aff_1,d1_aff_1,t14_aff_1,t30_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t62_aff_1,t30_aff_1,d4_aff_2,t14_aff_1,t15_aff_1,t23_aff_1,t30_aff_1,d4_aff_2,t12_aff_1,t30_aff_1,t30_aff_1,t13_aff_1,t30_aff_1,t62_aff_1,t12_aff_1,t30_aff_1,t13_aff_1,t30_aff_1,t62_aff_1,t30_aff_1,t15_aff_1,d1_aff_1,t14_aff_1,d1_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,d1_aff_1,t13_aff_1,t13_aff_1,t14_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t11_aff_1,t30_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,t38_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t53_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t72_aff_1,t33_aff_1,d1_aff_1,t14_aff_1,t53_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t30_aff_1,t53_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,d1_aff_1,t14_aff_1,t14_aff_1,d1_aff_1,t38_aff_1,d5_aff_2,t30_aff_1,t30_aff_1,t30_aff_1]), [file(aff_2,t16_aff_2),interesting(0.66)]). fof(t15_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v2_aff_2(A) <=> v3_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d3_aff_2,t30_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,t13_aff_1,t46_aff_1,t48_aff_1,t37_aff_1,t30_aff_1,t73_aff_1,d1_aff_1,t14_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,d2_aff_2,t14_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t30_aff_1,d2_aff_2,t12_aff_1,t30_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t30_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t30_aff_1,t38_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t53_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t30_aff_1,t72_aff_1,t53_aff_1,t33_aff_1,d1_aff_1,t14_aff_1,d3_aff_2,t30_aff_1,t30_aff_1]), [file(aff_2,t15_aff_2),interesting(0.65)]). fof(t22_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v13_aff_2(A) <=> v14_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d14_aff_2,t59_aff_1,t59_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t38_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t58_aff_1,t59_aff_1,t59_aff_1,t72_aff_1,t62_aff_1,t59_aff_1,t53_aff_1,d13_aff_2,t14_aff_1,d1_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t16_aff_1,t17_aff_1,t39_aff_1,t62_aff_1,t59_aff_1,d13_aff_2,t12_aff_1,t59_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t38_aff_1,t63_aff_1,t50_aff_1,t54_aff_1,t46_aff_1,t57_aff_1,t37_aff_1,t30_aff_1,t59_aff_1,t72_aff_1,t53_aff_1,t33_aff_1,d1_aff_1,t14_aff_1,d14_aff_2,t30_aff_1,t53_aff_1,t59_aff_1]), [file(aff_2,t22_aff_2),interesting(0.65)]). fof(t20_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v10_aff_2(A) => v7_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d7_aff_2,t12_aff_1,t49_aff_1,d1_aff_1,t46_aff_1,t48_aff_1,t37_aff_1,t38_aff_1,t39_aff_1,t55_aff_1,t54_aff_1,t67_aff_1,t59_aff_1,t13_aff_1,t30_aff_1,t62_aff_1,t12_aff_1,t13_aff_1,t30_aff_1,t62_aff_1,t30_aff_1,t38_aff_1,t63_aff_1,t50_aff_1,t13_aff_1,t46_aff_1,t57_aff_1,t48_aff_1,t37_aff_1,t33_aff_1,t73_aff_1,t39_aff_1,t53_aff_1,d1_aff_1,t14_aff_1,d10_aff_2,t30_aff_1,t13_aff_1,t30_aff_1,t62_aff_1,t30_aff_1]), [file(aff_2,t20_aff_2),interesting(0.64)]). fof(t18_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v8_aff_2(A) => v9_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d9_aff_2,t12_aff_1,t49_aff_1,t49_aff_1,t38_aff_1,t39_aff_1,t30_aff_1,t13_aff_1,t13_aff_1,t62_aff_1,t62_aff_1,t30_aff_1,t62_aff_1,t38_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t59_aff_1,t72_aff_1,t54_aff_1,t45_aff_1,t33_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,d8_aff_2,t39_aff_1,t30_aff_1,t33_aff_1,d1_aff_1,t13_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t11_aff_1,t30_aff_1]), [file(aff_2,t18_aff_2),interesting(0.62)]). fof(t29_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v11_aff_2(A) => v13_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d13_aff_2,t59_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t11_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,t39_aff_1,t59_aff_1,t14_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t13_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t38_aff_1,t63_aff_1,t50_aff_1,t63_aff_1,t50_aff_1,t58_aff_1,t58_aff_1,t53_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t72_aff_1,t53_aff_1,t53_aff_1,t33_aff_1,t39_aff_1,t59_aff_1,t33_aff_1,t39_aff_1,t59_aff_1,t52_aff_1,d11_aff_2,t53_aff_1,t33_aff_1,t39_aff_1,t59_aff_1,t33_aff_1,t39_aff_1,t59_aff_1,t51_aff_1,t53_aff_1,d11_aff_2,t53_aff_1,t14_aff_1,d1_aff_1,t15_aff_1,t39_aff_1,t59_aff_1,t14_aff_1,t13_aff_1]), [file(aff_2,t29_aff_2),interesting(0.61)]). fof(t26_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v4_aff_2(A) => v7_aff_2(A) ) ) ), inference(mizar_proof,[status(thm)],[d7_aff_2,t48_aff_1,t37_aff_1,t38_aff_1,t39_aff_1,t55_aff_1,t54_aff_1,t67_aff_1,t59_aff_1,d4_aff_2]), [file(aff_2,t26_aff_2),interesting(0.51)]). fof(t10_aff_2,theorem,( $true ), file(aff_2,t10_aff_2), [interesting(0.00)]). fof(t11_aff_2,theorem,( $true ), file(aff_2,t11_aff_2), [interesting(0.00)]). fof(t12_aff_2,theorem,( $true ), file(aff_2,t12_aff_2), [interesting(0.00)]). fof(t13_aff_2,theorem,( $true ), file(aff_2,t13_aff_2), [interesting(0.00)]). fof(t14_aff_2,theorem,( $true ), file(aff_2,t14_aff_2), [interesting(0.00)]). fof(d3_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v3_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,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)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & r2_hidden(D,B) & r2_hidden(D,C) & r2_hidden(E,B) & r2_hidden(F,B) & r2_hidden(G,B) & r2_hidden(I,C) & r2_hidden(J,C) & r2_analoaf(A,E,I,F,H) & r2_analoaf(A,F,J,G,I) & r2_analoaf(A,E,J,G,H) ) => ( B = C | D = E | D = H | D = F | D = I | D = G | D = J | F = G | r2_hidden(H,C) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d3_aff_2), [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(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(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(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(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(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(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(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(d2_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ( v2_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,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)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & r2_hidden(D,B) & r2_hidden(D,C) & r2_hidden(E,B) & r2_hidden(F,B) & r2_hidden(G,B) & r2_hidden(H,C) & r2_hidden(I,C) & r2_hidden(J,C) & r2_analoaf(A,E,I,F,H) & r2_analoaf(A,F,J,G,I) ) => ( B = C | D = E | D = H | D = F | D = I | D = G | D = J | r2_analoaf(A,E,J,G,H) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d2_aff_2), [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(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(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(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(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(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(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(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(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(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(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_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(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(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(d9_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v9_aff_2(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(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)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ( ( v1_aff_1(B,A) & r2_hidden(C,B) & r2_hidden(F,B) & r2_hidden(I,B) & r1_aff_1(A,C,D,G) & r1_aff_1(A,C,E,H) & r2_analoaf(A,E,F,H,I) & r2_analoaf(A,D,F,G,I) & r2_aff_1(A,D,E,B) ) => ( r2_hidden(D,B) | C = F | D = E | r2_analoaf(A,D,E,G,H) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d9_aff_2), [interesting(0.00)]). fof(t49_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_hidden(B,D) & r2_hidden(C,D) ) ) ) ) ) ), file(aff_1,t49_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(t54_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_hidden(B,D) & r2_hidden(C,D) & r3_aff_1(A,D,E) ) => r2_aff_1(A,B,C,E) ) ) ) ) ) ) ), file(aff_1,t54_aff_1), [interesting(0.00)]). fof(t45_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_aff_1(A,B,C,F) & r2_aff_1(A,D,E,F) ) => r2_analoaf(A,B,C,D,E) ) ) ) ) ) ) ) ), file(aff_1,t45_aff_1), [interesting(0.00)]). fof(d8_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v8_aff_2(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(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)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ( ( v1_aff_1(B,A) & r2_hidden(C,B) & r2_hidden(F,B) & r2_hidden(I,B) & r1_aff_1(A,C,D,G) & r2_analoaf(A,D,E,G,H) & r2_analoaf(A,E,F,H,I) & r2_analoaf(A,D,F,G,I) & r2_aff_1(A,D,E,B) ) => ( r2_hidden(D,B) | C = F | D = E | r1_aff_1(A,C,E,H) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d8_aff_2), [interesting(0.00)]). fof(d10_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v10_aff_2(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(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)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ( ( v1_aff_1(B,A) & r2_hidden(C,B) & r2_hidden(F,B) & r1_aff_1(A,C,D,G) & r1_aff_1(A,C,E,H) & r2_analoaf(A,D,E,G,H) & r2_analoaf(A,D,F,G,I) & r2_analoaf(A,E,F,H,I) & r2_aff_1(A,D,E,B) ) => ( r2_hidden(D,B) | C = F | D = E | r2_hidden(I,B) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d10_aff_2), [interesting(0.00)]). fof(t55_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))) => ( v1_aff_1(B,A) => r3_aff_1(A,B,B) ) ) ) ), file(aff_1,t55_aff_1), [interesting(0.00)]). fof(t67_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) & r2_aff_1(A,B,C,E) ) => ( B = C | r4_aff_1(A,D,E) ) ) ) ) ) ) ) ), file(aff_1,t67_aff_1), [interesting(0.00)]). fof(t1_aff_2,theorem,( $true ), file(aff_2,t1_aff_2), [interesting(0.00)]). fof(d7_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ( v7_aff_2(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(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)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ( ( v1_aff_1(B,A) & r2_hidden(C,B) & r2_hidden(F,B) & r2_hidden(I,B) & r1_aff_1(A,C,D,G) & r1_aff_1(A,C,E,H) & r2_analoaf(A,D,E,G,H) & r2_analoaf(A,D,F,G,I) & r2_aff_1(A,D,E,B) ) => ( r2_hidden(D,B) | C = F | D = E | r2_analoaf(A,E,F,H,I) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d7_aff_2), [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(d14_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v14_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,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)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & r2_hidden(D,B) & r2_hidden(E,B) & r2_hidden(F,B) & r4_aff_1(A,B,C) & r2_hidden(G,C) & r2_hidden(H,C) & r2_analoaf(A,D,H,E,G) & r2_analoaf(A,E,I,F,H) & r2_analoaf(A,D,I,F,G) ) => ( B = C | G = H | r2_hidden(I,C) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d14_aff_2), [interesting(0.00)]). fof(d13_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ( v13_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,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)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & r2_hidden(D,B) & r2_hidden(E,B) & r2_hidden(F,B) & r4_aff_1(A,B,C) & r2_hidden(G,C) & r2_hidden(H,C) & r2_hidden(I,C) & r2_analoaf(A,D,H,E,G) & r2_analoaf(A,E,I,F,H) ) => ( B = C | r2_analoaf(A,D,I,F,G) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d13_aff_2), [interesting(0.00)]). fof(t41_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_hidden(B,F) & r2_hidden(C,F) & v1_aff_1(F,A) ) => ( B = C | ( r2_aff_1(A,D,E,F) <=> r2_analoaf(A,D,E,B,C) ) ) ) ) ) ) ) ) ) ), file(aff_1,t41_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(d1_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v1_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,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)) => ( ( v1_aff_1(B,A) & v1_aff_1(C,A) & r2_hidden(D,B) & r2_hidden(E,B) & r2_hidden(F,B) & r2_hidden(G,C) & r2_hidden(H,C) & r2_hidden(I,C) & r2_analoaf(A,D,H,E,G) & r2_analoaf(A,E,I,F,H) ) => r2_analoaf(A,D,I,F,G) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d1_aff_2), [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(t24_aff_2,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v1_aff_2(A) <=> ( v2_aff_2(A) & v13_aff_2(A) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_aff_2,d1_aff_2,d13_aff_2,d1_aff_2,d1_aff_2,t72_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,t12_aff_1,t65_aff_1,t13_aff_1,t62_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,t12_aff_1,t30_aff_1,t65_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,t62_aff_1,t30_aff_1,t12_aff_1,t13_aff_1,t62_aff_1,t30_aff_1,t13_aff_1,t62_aff_1,t65_aff_1,t13_aff_1,t62_aff_1,t65_aff_1,t62_aff_1,t30_aff_1,t62_aff_1,t65_aff_1,d2_aff_2,d13_aff_2,t65_aff_1]), [file(aff_2,t24_aff_2),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(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(d12_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v12_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)) => ( ( r4_aff_1(A,B,C) & r2_hidden(E,B) & r2_hidden(H,B) & r2_hidden(F,C) & r2_hidden(I,C) & r2_hidden(G,D) & r2_hidden(J,D) & v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_analoaf(A,E,F,H,I) & r2_analoaf(A,E,G,H,J) & r2_analoaf(A,F,G,I,J) ) => ( B = C | B = D | r1_aff_1(A,E,F,G) | G = J | r4_aff_1(A,B,D) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d12_aff_2), [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(d11_aff_2,definition,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ( v11_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)) => ( ( r4_aff_1(A,B,C) & r4_aff_1(A,B,D) & r2_hidden(E,B) & r2_hidden(H,B) & r2_hidden(F,C) & r2_hidden(I,C) & r2_hidden(G,D) & r2_hidden(J,D) & v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_analoaf(A,E,F,H,I) & r2_analoaf(A,E,G,H,J) ) => ( B = C | B = D | r2_analoaf(A,F,G,I,J) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d11_aff_2), [interesting(0.00)]). fof(t2_aff_2,theorem,( $true ), file(aff_2,t2_aff_2), [interesting(0.00)]). fof(t3_aff_2,theorem,( $true ), file(aff_2,t3_aff_2), [interesting(0.00)]). fof(t4_aff_2,theorem,( $true ), file(aff_2,t4_aff_2), [interesting(0.00)]). fof(t5_aff_2,theorem,( $true ), file(aff_2,t5_aff_2), [interesting(0.00)]). fof(t6_aff_2,theorem,( $true ), file(aff_2,t6_aff_2), [interesting(0.00)]). fof(t7_aff_2,theorem,( $true ), file(aff_2,t7_aff_2), [interesting(0.00)]). fof(t8_aff_2,theorem,( $true ), file(aff_2,t8_aff_2), [interesting(0.00)]). fof(t9_aff_2,theorem,( $true ), file(aff_2,t9_aff_2), [interesting(0.00)]).