fof(t87_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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_boolealg(A,k3_boolealg(A,k3_boolealg(A,B,C),D),k3_boolealg(A,B,k3_boolealg(A,C,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_boolealg,t62_boolealg,t62_boolealg,t61_boolealg,t54_boolealg,d5_lattices,d5_lattices,d5_lattices,d7_lattices,t54_boolealg,t61_boolealg,t62_boolealg,t62_boolealg,t24_boolealg]), [file(boolealg,t87_boolealg),interesting(1.00)]). fof(t8_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r3_lattices(A,k1_boolealg(A,B,C),B) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_lattices]), [file(boolealg,t8_boolealg),interesting(0.93)]). fof(t15_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_boolealg(A,B,C) => r2_boolealg(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_boolealg,d4_boolealg]), [file(boolealg,t15_boolealg),interesting(0.90)]). fof(t69_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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)) => ( r3_boolealg(A,B,k3_lattices(A,C,D)) <=> ( r3_boolealg(A,B,C) | r3_boolealg(A,B,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_boolealg,d11_lattices,t39_lattices,d4_boolealg,d4_boolealg,t22_lattices,d11_lattices,t25_boolealg,d4_boolealg,d4_boolealg,d11_lattices,t27_boolealg,d4_boolealg]), [file(boolealg,t69_boolealg),interesting(0.85)]). fof(t63_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_boolealg(A,k1_boolealg(A,B,C),k1_boolealg(A,C,B)) => r1_boolealg(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_lattices,t47_lattices,t40_lattices,d7_lattices,t18_lattices,t47_lattices,d8_lattices,t31_lattices,t48_lattices,t43_lattices,d9_lattices,t21_lattices,t53_lattices,t49_lattices,t49_lattices,d7_lattices,t47_lattices,t40_lattices,d7_lattices,t18_lattices,t52_lattices,t53_lattices,t49_lattices,t49_lattices,d3_boolealg]), [file(boolealg,t63_boolealg),interesting(0.83)]). fof(t30_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(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)) => ( ( r3_boolealg(A,B,C) & r3_lattices(A,C,D) ) => r3_boolealg(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_boolealg,t27_lattices,t25_boolealg,d4_boolealg]), [file(boolealg,t30_boolealg),interesting(0.80)]). fof(t78_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ r2_boolealg(A,k4_lattices(A,B,C),k3_boolealg(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t70_boolealg,t69_boolealg]), [file(boolealg,t78_boolealg),interesting(0.80)]). fof(t33_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ~ r2_boolealg(A,B,k5_lattices(A)) ) ) ), inference(mizar_proof,[status(thm)],[d4_boolealg,t40_lattices]), [file(boolealg,t33_boolealg),interesting(0.77)]). fof(t16_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( r2_boolealg(A,B,B) <=> B != k5_lattices(A) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_boolealg,t18_lattices,t18_lattices,d4_boolealg]), [file(boolealg,t16_boolealg),interesting(0.76)]). fof(t31_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(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)) => ( r3_boolealg(A,B,k4_lattices(A,C,D)) => ( r3_boolealg(A,B,C) & r3_boolealg(A,B,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_boolealg,d7_lattices,d7_lattices,t40_lattices,d4_boolealg]), [file(boolealg,t31_boolealg),interesting(0.76)]). fof(t6_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(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)) => ( r3_lattices(A,B,C) => r3_lattices(A,k1_boolealg(A,B,D),C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_lattices,t23_lattices,t25_lattices]), [file(boolealg,t6_boolealg),interesting(0.75)]). fof(t70_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ r2_boolealg(A,k4_lattices(A,B,C),k1_boolealg(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_lattices,d7_lattices,t47_lattices,t40_lattices,t40_lattices,d4_boolealg]), [file(boolealg,t70_boolealg),interesting(0.75)]). fof(t21_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v12_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( ~ r2_boolealg(A,B,C) & r2_boolealg(A,C,B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_boolealg,d4_boolealg]), [file(boolealg,t21_boolealg),interesting(0.74)]). fof(t3_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(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)) => ( r3_lattices(A,k3_lattices(A,B,C),D) => ( r3_lattices(A,B,D) & r3_lattices(A,C,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_lattices,d9_lattices,t23_lattices,t27_lattices,d9_lattices,t23_lattices,t25_lattices]), [file(boolealg,t3_boolealg),interesting(0.74)]). fof(l5_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(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)) => ( ( r3_lattices(A,B,C) & r3_lattices(A,D,C) ) => r3_lattices(A,k3_lattices(A,B,D),C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t1_filter_0,t1_filter_0,t17_lattices,t25_lattices]), [file(boolealg,l5_boolealg),interesting(0.73)]). fof(t72_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ r2_boolealg(A,k1_boolealg(A,B,C),C) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_lattices,t47_lattices,t40_lattices,d4_boolealg]), [file(boolealg,t72_boolealg),interesting(0.72)]). fof(t67_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => r1_boolealg(A,k1_boolealg(A,B,k5_lattices(A)),B) ) ) ), inference(mizar_proof,[status(thm)],[t37_lattice4,t43_lattices]), [file(boolealg,t67_boolealg),interesting(0.72)]). fof(t76_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => r1_boolealg(A,k3_boolealg(A,B,k5_lattices(A)),B) ) ) ), inference(mizar_proof,[status(thm)],[t67_boolealg,t29_boolealg,t39_lattices]), [file(boolealg,t76_boolealg),interesting(0.71)]). fof(t25_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ( r3_lattices(A,B,k5_lattices(A)) => r1_boolealg(A,B,k5_lattices(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t41_lattices,t26_lattices]), [file(boolealg,t25_boolealg),interesting(0.69)]). fof(t71_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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_boolealg(A,B,k3_lattices(A,C,D)) <=> ( ~ r2_boolealg(A,B,C) & ~ r2_boolealg(A,B,D) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t69_boolealg]), [file(boolealg,t71_boolealg),interesting(0.69)]). fof(t66_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => r1_boolealg(A,k1_boolealg(A,B,B),k5_lattices(A)) ) ) ), inference(mizar_proof,[status(thm)],[t47_lattices]), [file(boolealg,t66_boolealg),interesting(0.68)]). fof(t7_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(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)) => ( r3_lattices(A,B,C) => r3_lattices(A,k1_boolealg(A,B,D),k1_boolealg(A,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_lattices]), [file(boolealg,t7_boolealg),interesting(0.67)]). fof(t4_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(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)) => r3_lattices(A,k4_lattices(A,B,C),k3_lattices(A,B,D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_lattices,t23_lattices,t25_lattices]), [file(boolealg,t4_boolealg),interesting(0.65)]). fof(t29_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => r1_boolealg(A,k1_boolealg(A,k5_lattices(A),B),k5_lattices(A)) ) ) ), inference(mizar_proof,[status(thm)],[t40_lattices]), [file(boolealg,t29_boolealg),interesting(0.65)]). fof(t34_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(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_boolealg(A,B,C) & r3_lattices(A,D,C) & r2_boolealg(A,B,D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t30_boolealg]), [file(boolealg,t34_boolealg),interesting(0.63)]). fof(t53_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k3_lattices(A,k4_lattices(A,B,C),k1_boolealg(A,B,C)),B) ) ) ) ), inference(mizar_proof,[status(thm)],[t31_lattices,d8_lattices,t31_lattices,t48_lattices,t43_lattices,d9_lattices]), [file(boolealg,t53_boolealg),interesting(0.61)]). fof(l87_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k1_boolealg(A,k3_lattices(A,B,C),k3_boolealg(A,B,C)),k4_lattices(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_lattices,t50_lattices,t50_lattices,t49_lattices,t49_lattices,d7_lattices,d11_lattices,d9_lattices,d11_lattices,t47_lattices,t39_lattices,d8_lattices,d11_lattices,t47_lattices,t39_lattices]), [file(boolealg,l87_boolealg),interesting(0.60)]). fof(t83_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k3_boolealg(A,k3_boolealg(A,B,C),k3_lattices(A,B,C)),k4_lattices(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_lattices,d11_lattices,d7_lattices,d7_lattices,t18_lattices,d7_lattices,t47_lattices,t40_lattices,t39_lattices,d7_lattices,d7_lattices,t18_lattices,d7_lattices,t47_lattices,t40_lattices,t39_lattices,l87_boolealg]), [file(boolealg,t83_boolealg),interesting(0.60)]). fof(t9_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r3_lattices(A,k1_boolealg(A,B,C),k2_boolealg(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_lattices]), [file(boolealg,t9_boolealg),interesting(0.60)]). fof(t32_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(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)) => ( r3_boolealg(A,B,k1_boolealg(A,C,D)) => r3_boolealg(A,B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_boolealg,d7_lattices,t40_lattices,d4_boolealg]), [file(boolealg,t32_boolealg),interesting(0.59)]). fof(t35_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(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_boolealg(A,B,C) & r2_boolealg(A,B,D) ) & r2_boolealg(A,B,k4_lattices(A,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t31_boolealg]), [file(boolealg,t35_boolealg),interesting(0.58)]). fof(t55_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k1_boolealg(A,B,k1_boolealg(A,B,C)),k4_lattices(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_lattices,t49_lattices,d11_lattices,t47_lattices,t39_lattices]), [file(boolealg,t55_boolealg),interesting(0.57)]). fof(t82_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k3_boolealg(A,k3_boolealg(A,B,C),k4_lattices(A,B,C)),k3_lattices(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_lattices,d11_lattices,t51_lattices,t50_lattices,t50_lattices,t49_lattices,t49_lattices,d7_lattices,d11_lattices,d7_lattices,t47_lattices,t40_lattices,t39_lattices,d7_lattices,t18_lattices,d11_lattices,d7_lattices,t47_lattices,t40_lattices,t39_lattices,d7_lattices,t18_lattices,d11_lattices,d7_lattices,d7_lattices,t47_lattices,t18_lattices,t40_lattices,t39_lattices,d11_lattices,d7_lattices,t18_lattices,d7_lattices,t47_lattices,t40_lattices,t39_lattices,d5_lattices,d11_lattices,t48_lattices,t43_lattices,t31_lattices,t48_lattices,t43_lattices]), [file(boolealg,t82_boolealg),interesting(0.57)]). fof(t57_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_boolealg(A,k4_lattices(A,B,C),k5_lattices(A)) <=> r1_boolealg(A,k1_boolealg(A,B,C),B) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_lattices,t27_lattices,t18_lattices,t8_boolealg,d3_boolealg,t50_lattices,t49_lattices,d11_lattices,t47_lattices,t47_lattices,t39_lattices,t41_lattices,d3_boolealg]), [file(boolealg,t57_boolealg),interesting(0.56)]). fof(t46_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_boolealg(A,k1_boolealg(A,B,C),k5_lattices(A)) <=> r3_lattices(A,B,C) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_lattices,t49_lattices,t27_lattices,t47_lattices,t41_lattices,d3_boolealg]), [file(boolealg,t46_boolealg),interesting(0.55)]). fof(t14_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(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_boolealg(A,k4_lattices(A,B,k1_boolealg(A,C,D)),k1_boolealg(A,k4_lattices(A,B,C),D)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_lattices]), [file(boolealg,t14_boolealg),interesting(0.55)]). fof(t77_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => r1_boolealg(A,k3_boolealg(A,B,B),k5_lattices(A)) ) ) ), inference(mizar_proof,[status(thm)],[t17_lattices,t66_boolealg]), [file(boolealg,t77_boolealg),interesting(0.55)]). fof(t39_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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)) => ( r3_lattices(A,B,C) => r3_lattices(A,k1_boolealg(A,D,C),k1_boolealg(A,D,B)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t53_lattices,t27_lattices]), [file(boolealg,t39_boolealg),interesting(0.54)]). fof(t84_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k3_boolealg(A,B,C),k1_boolealg(A,k3_lattices(A,B,C),k4_lattices(A,B,C))) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_boolealg,t50_boolealg,t24_boolealg]), [file(boolealg,t84_boolealg),interesting(0.54)]). fof(t79_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k3_lattices(A,B,C),k3_boolealg(A,B,k1_boolealg(A,C,B))) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_lattices,t48_lattices,t31_lattices,d8_lattices,t18_lattices,t18_lattices,t49_lattices,d11_lattices,t50_lattices,d7_lattices]), [file(boolealg,t79_boolealg),interesting(0.53)]). fof(t61_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k1_boolealg(A,k3_lattices(A,B,C),k4_lattices(A,B,C)),k3_lattices(A,k1_boolealg(A,B,C),k1_boolealg(A,C,B))) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_lattices,d11_lattices,d11_lattices,d11_lattices,t47_lattices,t47_lattices,t39_lattices,t39_lattices]), [file(boolealg,t61_boolealg),interesting(0.49)]). fof(t80_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k3_boolealg(A,B,k4_lattices(A,B,C)),k1_boolealg(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_lattices,t47_lattices,t40_lattices,t39_lattices,t50_lattices,d11_lattices,t47_lattices,t39_lattices]), [file(boolealg,t80_boolealg),interesting(0.48)]). fof(t38_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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)) => ( r3_lattices(A,k1_boolealg(A,B,C),D) => r3_lattices(A,B,k3_lattices(A,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t1_filter_0,t31_lattices,t48_lattices,t43_lattices,t22_lattices,t25_lattices]), [file(boolealg,t38_boolealg),interesting(0.47)]). fof(t48_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k3_lattices(A,B,C),k3_lattices(A,k1_boolealg(A,B,C),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_lattices,t48_lattices,t31_lattices]), [file(boolealg,t48_boolealg),interesting(0.47)]). fof(t49_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k1_boolealg(A,B,k3_lattices(A,B,C)),k5_lattices(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_lattices,t46_boolealg]), [file(boolealg,t49_boolealg),interesting(0.46)]). fof(t81_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k3_lattices(A,B,C),k3_lattices(A,k3_boolealg(A,B,C),k4_lattices(A,B,C))) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_boolealg,t53_boolealg,d5_lattices]), [file(boolealg,t81_boolealg),interesting(0.45)]). fof(t56_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k1_boolealg(A,k3_lattices(A,B,C),C),k1_boolealg(A,B,C)) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_lattices,t47_lattices,t39_lattices]), [file(boolealg,t56_boolealg),interesting(0.44)]). fof(t54_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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_boolealg(A,k1_boolealg(A,B,k1_boolealg(A,C,D)),k3_lattices(A,k1_boolealg(A,B,C),k4_lattices(A,B,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_lattices,t49_lattices,d11_lattices]), [file(boolealg,t54_boolealg),interesting(0.44)]). fof(t73_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ~ r2_boolealg(A,B,C) => ( r1_boolealg(A,k1_boolealg(A,k3_lattices(A,B,C),C),B) & r1_boolealg(A,k1_boolealg(A,k3_lattices(A,B,C),B),C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_boolealg,d11_lattices,t47_lattices,t39_lattices,t39_lattices,t31_lattices,t48_lattices,t43_lattices,t49_lattices,t51_lattices,t49_lattices,d11_lattices,t47_lattices,t39_lattices,t39_lattices,t31_lattices,t48_lattices,t43_lattices,t49_lattices,t51_lattices,t49_lattices]), [file(boolealg,t73_boolealg),interesting(0.37)]). fof(t44_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r3_lattices(A,B,k1_boolealg(A,C,B)) => r1_boolealg(A,B,k5_lattices(A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_lattices,t47_lattices,t40_lattices,t21_lattices]), [file(boolealg,t44_boolealg),interesting(0.34)]). fof(t51_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k4_lattices(A,k1_boolealg(A,B,C),C),k5_lattices(A)) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_lattices,t47_lattices,t40_lattices]), [file(boolealg,t51_boolealg),interesting(0.34)]). fof(t45_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r3_lattices(A,B,C) => r1_boolealg(A,C,k3_lattices(A,B,k1_boolealg(A,C,B))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t43_lattices,t48_lattices,d11_lattices,t21_lattices]), [file(boolealg,t45_boolealg),interesting(0.31)]). fof(t68_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k7_lattices(A,k1_boolealg(A,B,C)),k3_lattices(A,k7_lattices(A,B),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_lattices,t49_lattices]), [file(boolealg,t68_boolealg),interesting(0.28)]). fof(t36_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(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)) => ( ( r3_lattices(A,B,C) & r3_lattices(A,B,D) ) => ( r2_boolealg(A,C,D) | r1_boolealg(A,B,k5_lattices(A)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_boolealg,t7_filter_0,t25_boolealg]), [file(boolealg,t36_boolealg),interesting(0.25)]). fof(t59_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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_boolealg(A,k1_boolealg(A,B,k4_lattices(A,C,D)),k3_lattices(A,k1_boolealg(A,B,C),k1_boolealg(A,B,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_lattices,d11_lattices]), [file(boolealg,t59_boolealg),interesting(0.25)]). fof(t86_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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_boolealg(A,k1_boolealg(A,B,k3_boolealg(A,C,D)),k3_lattices(A,k1_boolealg(A,B,k3_lattices(A,C,D)),k4_lattices(A,k4_lattices(A,B,C),D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t84_boolealg,t54_boolealg,d7_lattices]), [file(boolealg,t86_boolealg),interesting(0.22)]). fof(t85_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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_boolealg(A,k1_boolealg(A,k3_boolealg(A,B,C),D),k3_lattices(A,k1_boolealg(A,B,k3_lattices(A,C,D)),k1_boolealg(A,C,k3_lattices(A,B,D)))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t24_boolealg,t62_boolealg,t62_boolealg]), [file(boolealg,t85_boolealg),interesting(0.20)]). fof(t88_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k7_lattices(A,k3_boolealg(A,B,C)),k3_lattices(A,k4_lattices(A,B,C),k4_lattices(A,k7_lattices(A,B),k7_lattices(A,C)))) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_lattices,t50_lattices,t50_lattices,t49_lattices,t49_lattices,d11_lattices,d11_lattices,d11_lattices,t47_lattices,t47_lattices,t39_lattices,t39_lattices]), [file(boolealg,t88_boolealg),interesting(0.18)]). fof(t26_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(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)) => ( ( r3_lattices(A,B,C) & r3_lattices(A,B,D) & r1_boolealg(A,k4_lattices(A,C,D),k5_lattices(A)) ) => r1_boolealg(A,B,k5_lattices(A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_filter_0,t25_boolealg]), [file(boolealg,t26_boolealg),interesting(0.16)]). fof(t58_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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_boolealg(A,k1_boolealg(A,B,k3_lattices(A,C,D)),k4_lattices(A,k1_boolealg(A,B,C),k1_boolealg(A,B,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_lattices,t18_lattices,d7_lattices,d7_lattices,d7_lattices]), [file(boolealg,t58_boolealg),interesting(0.16)]). fof(t22_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v11_lattices(A) & l3_lattices(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_boolealg(A,k3_lattices(A,k4_lattices(A,B,C),k4_lattices(A,B,D)),B) => r3_lattices(A,B,k3_lattices(A,C,D)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_lattices,t21_lattices]), [file(boolealg,t22_boolealg),interesting(0.15)]). fof(t28_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(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)) => ( ( r3_lattices(A,B,C) & r1_boolealg(A,k4_lattices(A,C,D),k5_lattices(A)) ) => r1_boolealg(A,k4_lattices(A,B,D),k5_lattices(A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_lattices,t25_boolealg]), [file(boolealg,t28_boolealg),interesting(0.14)]). fof(t75_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_boolealg(A,k3_lattices(A,k7_lattices(A,B),k7_lattices(A,C)),k3_lattices(A,B,C)) => ( r2_boolealg(A,C,k7_lattices(A,B)) | r2_boolealg(A,B,k7_lattices(A,C)) | ( r1_boolealg(A,B,k7_lattices(A,B)) & r1_boolealg(A,C,k7_lattices(A,C)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_boolealg,d4_boolealg,t31_lattices,t48_lattices,t39_lattices,t43_lattices,d9_lattices,t50_lattices,t22_lattices,t25_lattices,t31_lattices,t48_lattices,t39_lattices,t43_lattices,d9_lattices,t50_lattices,t49_lattices,t49_lattices,t49_lattices,t22_lattices,t25_lattices,t31_lattices,t48_lattices,t39_lattices,t43_lattices,d9_lattices,t49_lattices,t50_lattices,t49_lattices,t49_lattices,t22_lattices,t25_lattices,t31_lattices,t48_lattices,t39_lattices,t43_lattices,d9_lattices,t50_lattices,t22_lattices,t25_lattices,d3_boolealg]), [file(boolealg,t75_boolealg),interesting(0.08)]). fof(t1_filter_0,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(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)) => ( r3_lattices(A,B,C) => ( r3_lattices(A,k3_lattices(A,D,B),k3_lattices(A,D,C)) & r3_lattices(A,k3_lattices(A,B,D),k3_lattices(A,C,D)) & r3_lattices(A,k3_lattices(A,B,D),k3_lattices(A,D,C)) & r3_lattices(A,k3_lattices(A,D,B),k3_lattices(A,C,D)) ) ) ) ) ) ) ), file(filter_0,t1_filter_0), [interesting(0.00)]). fof(t17_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v6_lattices(A) & v8_lattices(A) & v9_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k1_lattices(A,B,B) = B ) ) ), file(lattices,t17_lattices), [interesting(0.00)]). fof(t25_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v5_lattices(A) & l2_lattices(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_lattices(A,B,C) & r1_lattices(A,C,D) ) => r1_lattices(A,B,D) ) ) ) ) ) ), file(lattices,t25_lattices), [interesting(0.00)]). fof(t10_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(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)) => ( ( r3_lattices(A,k1_boolealg(A,B,C),D) & r3_lattices(A,k1_boolealg(A,C,B),D) ) => r3_lattices(A,k2_boolealg(A,B,C),D) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l5_boolealg]), [file(boolealg,t10_boolealg),interesting(0.00)]). fof(t22_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v5_lattices(A) & v6_lattices(A) & v8_lattices(A) & v9_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_lattices(A,B,k1_lattices(A,B,C)) ) ) ) ), file(lattices,t22_lattices), [interesting(0.00)]). fof(t26_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v4_lattices(A) & l2_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( ( r1_lattices(A,B,C) & r1_lattices(A,C,B) ) => B = C ) ) ) ) ), file(lattices,t26_lattices), [interesting(0.00)]). fof(t11_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(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_boolealg(A,B,k3_lattices(A,C,D)) <=> ( r3_lattices(A,C,B) & r3_lattices(A,D,B) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( r3_lattices(A,C,E) & r3_lattices(A,D,E) ) => r3_lattices(A,B,E) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[l5_boolealg,t22_lattices,t22_lattices,l5_boolealg,t26_lattices]), [file(boolealg,t11_boolealg),interesting(0.00)]). fof(t7_filter_0,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(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)) => ( ( r3_lattices(A,B,C) & r3_lattices(A,B,D) ) => r3_lattices(A,B,k4_lattices(A,C,D)) ) ) ) ) ) ), file(filter_0,t7_filter_0), [interesting(0.00)]). fof(t23_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v6_lattices(A) & v8_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_lattices(A,k4_lattices(A,B,C),B) ) ) ) ), file(lattices,t23_lattices), [interesting(0.00)]). fof(d3_boolealg,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_boolealg(A,B,C) <=> ( r3_lattices(A,B,C) & r3_lattices(A,C,B) ) ) ) ) ) ), file(boolealg,d3_boolealg), [interesting(0.00)]). fof(t12_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(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_boolealg(A,B,k4_lattices(A,C,D)) <=> ( r3_lattices(A,B,C) & r3_lattices(A,B,D) & ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( r3_lattices(A,E,C) & r3_lattices(A,E,D) ) => r3_lattices(A,E,B) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_filter_0,t23_lattices,t7_filter_0,t23_lattices,d3_boolealg]), [file(boolealg,t12_boolealg),interesting(0.00)]). fof(t13_boolealg,theorem,( $true ), file(boolealg,t13_boolealg), [interesting(0.00)]). fof(d4_boolealg,definition,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_boolealg(A,B,C) <=> k4_lattices(A,B,C) != k5_lattices(A) ) ) ) ) ), file(boolealg,d4_boolealg), [interesting(0.00)]). fof(t18_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v6_lattices(A) & v8_lattices(A) & v9_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k4_lattices(A,B,B) = B ) ) ), file(lattices,t18_lattices), [interesting(0.00)]). fof(t17_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => r1_boolealg(A,k2_boolealg(A,B,C),k2_boolealg(A,C,B)) ) ) ) ), file(boolealg,t17_boolealg), [interesting(0.00)]). fof(t18_boolealg,theorem,( $true ), file(boolealg,t18_boolealg), [interesting(0.00)]). fof(t19_boolealg,theorem,( $true ), file(boolealg,t19_boolealg), [interesting(0.00)]). fof(t1_boolealg,theorem,( $true ), file(boolealg,t1_boolealg), [interesting(0.00)]). fof(t20_boolealg,theorem,( $true ), file(boolealg,t20_boolealg), [interesting(0.00)]). fof(d11_lattices,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l3_lattices(A) ) => ( v11_lattices(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)) => k2_lattices(A,B,k1_lattices(A,C,D)) = k1_lattices(A,k2_lattices(A,B,C),k2_lattices(A,B,D)) ) ) ) ) ) ), file(lattices,d11_lattices), [interesting(0.00)]). fof(t21_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v8_lattices(A) & v9_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_lattices(A,B,C) <=> k2_lattices(A,B,C) = B ) ) ) ) ), file(lattices,t21_lattices), [interesting(0.00)]). fof(t23_boolealg,theorem,( $true ), file(boolealg,t23_boolealg), [interesting(0.00)]). fof(t41_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => r3_lattices(A,k5_lattices(A),B) ) ) ), file(lattices,t41_lattices), [interesting(0.00)]). fof(t27_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v7_lattices(A) & v8_lattices(A) & v9_lattices(A) & l3_lattices(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_lattices(A,B,C) => r1_lattices(A,k2_lattices(A,B,D),k2_lattices(A,C,D)) ) ) ) ) ) ), file(lattices,t27_lattices), [interesting(0.00)]). fof(t2_boolealg,theorem,( $true ), file(boolealg,t2_boolealg), [interesting(0.00)]). fof(d7_lattices,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l1_lattices(A) ) => ( v7_lattices(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)) => k2_lattices(A,B,k2_lattices(A,C,D)) = k2_lattices(A,k2_lattices(A,B,C),D) ) ) ) ) ) ), file(lattices,d7_lattices), [interesting(0.00)]). fof(t40_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k4_lattices(A,k5_lattices(A),B) = k5_lattices(A) ) ) ), file(lattices,t40_lattices), [interesting(0.00)]). fof(t37_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(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_boolealg(A,B,C) => ( ~ r2_boolealg(A,k4_lattices(A,D,B),k4_lattices(A,D,C)) & ~ r2_boolealg(A,k4_lattices(A,B,D),k4_lattices(A,C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_lattices,d7_lattices,d4_boolealg,t40_lattices,t40_lattices,d4_boolealg]), [file(boolealg,t37_boolealg),interesting(0.00)]). fof(t31_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v11_lattices(A) & l3_lattices(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)) => k3_lattices(A,B,k4_lattices(A,C,D)) = k4_lattices(A,k3_lattices(A,B,C),k3_lattices(A,B,D)) ) ) ) ) ), file(lattices,t31_lattices), [interesting(0.00)]). fof(t48_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_lattices(A,k7_lattices(A,B),B) = k6_lattices(A) ) ) ), file(lattices,t48_lattices), [interesting(0.00)]). fof(t43_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v14_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k4_lattices(A,k6_lattices(A),B) = B ) ) ), file(lattices,t43_lattices), [interesting(0.00)]). fof(d9_lattices,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l3_lattices(A) ) => ( v9_lattices(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k2_lattices(A,B,k1_lattices(A,B,C)) = B ) ) ) ) ), file(lattices,d9_lattices), [interesting(0.00)]). fof(t53_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r3_lattices(A,B,C) => r3_lattices(A,k7_lattices(A,C),k7_lattices(A,B)) ) ) ) ) ), file(lattices,t53_lattices), [interesting(0.00)]). fof(t40_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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)) => ( ( r3_lattices(A,B,C) & r3_lattices(A,D,E) ) => r3_lattices(A,k1_boolealg(A,B,E),k1_boolealg(A,C,D)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t7_boolealg,t39_boolealg,t25_lattices]), [file(boolealg,t40_boolealg),interesting(0.00)]). fof(t47_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k4_lattices(A,k7_lattices(A,B),B) = k5_lattices(A) ) ) ), file(lattices,t47_lattices), [interesting(0.00)]). fof(t39_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k3_lattices(A,k5_lattices(A),B) = B ) ) ), file(lattices,t39_lattices), [interesting(0.00)]). fof(t41_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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)) => ( r3_lattices(A,B,k3_lattices(A,C,D)) => ( r3_lattices(A,k1_boolealg(A,B,C),D) & r3_lattices(A,k1_boolealg(A,B,D),C) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t27_lattices,d11_lattices,t47_lattices,t39_lattices,t23_lattices,t25_lattices,t27_lattices,d11_lattices,t47_lattices,t39_lattices,t23_lattices,t25_lattices]), [file(boolealg,t41_boolealg),interesting(0.00)]). fof(t50_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k7_lattices(A,k4_lattices(A,B,C)) = k3_lattices(A,k7_lattices(A,B),k7_lattices(A,C)) ) ) ) ), file(lattices,t50_lattices), [interesting(0.00)]). fof(t42_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r3_lattices(A,k7_lattices(A,B),k7_lattices(A,k4_lattices(A,B,C))) & r3_lattices(A,k7_lattices(A,C),k7_lattices(A,k4_lattices(A,B,C))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_lattices,t22_lattices,t50_lattices]), [file(boolealg,t42_boolealg),interesting(0.00)]). fof(t51_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k7_lattices(A,k3_lattices(A,B,C)) = k4_lattices(A,k7_lattices(A,B),k7_lattices(A,C)) ) ) ) ), file(lattices,t51_lattices), [interesting(0.00)]). fof(t43_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r3_lattices(A,k7_lattices(A,k3_lattices(A,B,C)),k7_lattices(A,B)) & r3_lattices(A,k7_lattices(A,k3_lattices(A,B,C)),k7_lattices(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t51_lattices,t23_lattices,t51_lattices,t23_lattices]), [file(boolealg,t43_boolealg),interesting(0.00)]). fof(t47_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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)) => ( ( r3_lattices(A,B,k3_lattices(A,C,D)) & r1_boolealg(A,k4_lattices(A,B,D),k5_lattices(A)) ) => r3_lattices(A,B,C) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t21_lattices,d11_lattices,t39_lattices,t21_lattices]), [file(boolealg,t47_boolealg),interesting(0.00)]). fof(t52_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( k4_lattices(A,B,C) = k5_lattices(A) <=> r3_lattices(A,B,k7_lattices(A,C)) ) ) ) ) ), file(lattices,t52_lattices), [interesting(0.00)]). fof(t49_lattices,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => k7_lattices(A,k7_lattices(A,B)) = B ) ) ), file(lattices,t49_lattices), [interesting(0.00)]). fof(t5_boolealg,theorem,( $true ), file(boolealg,t5_boolealg), [interesting(0.00)]). fof(t60_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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_boolealg(A,k4_lattices(A,B,k1_boolealg(A,C,D)),k1_boolealg(A,k4_lattices(A,B,C),k4_lattices(A,B,D))) & r1_boolealg(A,k4_lattices(A,k1_boolealg(A,C,D),B),k1_boolealg(A,k4_lattices(A,C,B),k4_lattices(A,D,B))) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_lattices,t59_boolealg,t46_boolealg,t39_lattices,t14_boolealg,t14_boolealg]), [file(boolealg,t60_boolealg),interesting(0.00)]). fof(d8_lattices,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l3_lattices(A) ) => ( v8_lattices(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => k1_lattices(A,k2_lattices(A,B,C),C) = C ) ) ) ) ), file(lattices,d8_lattices), [interesting(0.00)]). fof(t64_boolealg,theorem,( $true ), file(boolealg,t64_boolealg), [interesting(0.00)]). fof(t65_boolealg,theorem,( $true ), file(boolealg,t65_boolealg), [interesting(0.00)]). fof(t27_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v13_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_boolealg(A,k3_lattices(A,B,C),k5_lattices(A)) <=> ( r1_boolealg(A,B,k5_lattices(A)) & r1_boolealg(A,C,k5_lattices(A)) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t22_lattices,t41_lattices,t22_lattices,t41_lattices,d3_boolealg,t39_lattices]), [file(boolealg,t27_boolealg),interesting(0.00)]). fof(t74_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_boolealg(A,k3_lattices(A,k7_lattices(A,B),k7_lattices(A,C)),k3_lattices(A,B,C)) => ( r2_boolealg(A,B,k7_lattices(A,B)) | r2_boolealg(A,C,k7_lattices(A,C)) | ( r1_boolealg(A,B,k7_lattices(A,C)) & r1_boolealg(A,C,k7_lattices(A,B)) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d4_boolealg,d4_boolealg,d11_lattices,t39_lattices,d9_lattices,d11_lattices,t39_lattices,d11_lattices,t39_lattices,d9_lattices,d11_lattices,t39_lattices,d9_lattices,d9_lattices]), [file(boolealg,t74_boolealg),interesting(0.00)]). fof(t37_lattice4,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => k7_lattices(A,k5_lattices(A)) = k6_lattices(A) ) ), file(lattice4,t37_lattice4), [interesting(0.00)]). fof(t52_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_boolealg(A,k3_lattices(A,B,k1_boolealg(A,C,B)),k3_lattices(A,B,C)) & r1_boolealg(A,k3_lattices(A,k1_boolealg(A,C,B),B),k3_lattices(A,C,B)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t31_lattices,t48_lattices,t43_lattices,t31_lattices,t48_lattices,t43_lattices]), [file(boolealg,t52_boolealg),interesting(0.00)]). fof(d5_lattices,definition,( ! [A] : ( ( ~ v3_struct_0(A) & l2_lattices(A) ) => ( v5_lattices(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)) => k1_lattices(A,B,k1_lattices(A,C,D)) = k1_lattices(A,k1_lattices(A,B,C),D) ) ) ) ) ) ), file(lattices,d5_lattices), [interesting(0.00)]). fof(t24_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v11_lattices(A) & l3_lattices(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_boolealg(A,k1_boolealg(A,k3_lattices(A,B,C),D),k3_lattices(A,k1_boolealg(A,B,D),k1_boolealg(A,C,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d11_lattices]), [file(boolealg,t24_boolealg),interesting(0.00)]). fof(t62_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(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_boolealg(A,k1_boolealg(A,k1_boolealg(A,B,C),D),k1_boolealg(A,B,k3_lattices(A,C,D))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_lattices,t51_lattices]), [file(boolealg,t62_boolealg),interesting(0.00)]). fof(t50_boolealg,theorem,( ! [A] : ( ( ~ v3_struct_0(A) & v10_lattices(A) & v17_lattices(A) & l3_lattices(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_boolealg(A,k1_boolealg(A,B,k4_lattices(A,B,C)),k1_boolealg(A,B,C)) & r1_boolealg(A,k1_boolealg(A,B,k4_lattices(A,C,B)),k1_boolealg(A,B,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t50_lattices,d11_lattices,t47_lattices,t39_lattices,t50_lattices,d11_lattices,t47_lattices,t39_lattices]), [file(boolealg,t50_boolealg),interesting(0.00)]).