fof(t67_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(A,k2_binarith(A,B)) = B ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t65_binari_6,t66_binari_6,t23_binarith,t23_binarith,t18_binarith,t50_margrel1,t23_binarith,t21_binarith,t25_binarith,t25_binarith]), [file(binari_6,t67_binari_6),interesting(1.00)]). fof(t87_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(k9_margrel1(A),k2_bvfunc_1(A,B)) = B ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t40_margrel1,t18_binari_6,t86_binari_6,t22_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t52_margrel1,t16_binarith,t22_binarith,t18_binarith,t50_margrel1]), [file(binari_6,t87_binari_6),interesting(0.87)]). fof(t72_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(A,k2_bvfunc_1(A,B)) = k9_margrel1(B) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t70_binari_6,t71_binari_6,t22_binarith,t18_binarith,t50_margrel1]), [file(binari_6,t72_binari_6),interesting(0.74)]). fof(t37_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_bvfunc_1(A,k1_bvfunc_1(A,B)) = k1_bvfunc_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t20_binarith,t21_binarith]), [file(binari_6,t37_binari_6),interesting(0.71)]). fof(t66_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k9_margrel1(k2_binarith(A,B))) = k10_margrel1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t10_binarith,t9_binarith,t40_margrel1,t9_binarith,t40_margrel1,t52_margrel1,t22_binarith,t46_margrel1,t7_binarith,t22_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t52_margrel1,t16_binarith]), [file(binari_6,t66_binari_6),interesting(0.68)]). fof(t18_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k2_bvfunc_1(A,B)) = k10_margrel1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t52_margrel1,t22_binarith,t46_margrel1,t7_binarith,t22_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t52_margrel1,t16_binarith]), [file(binari_6,t18_binari_6),interesting(0.68)]). fof(t7_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => k2_bvfunc_1(k8_margrel1,A) = A ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t1_binari_6,t19_binarith,t50_margrel1]), [file(binari_6,t7_binari_6),interesting(0.67)]). fof(t1_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => k1_bvfunc_1(k8_margrel1,A) = A ) ), inference(mizar_proof,[status(thm)],[d16_margrel1,t7_binarith]), [file(binari_6,t1_binari_6),interesting(0.66)]). fof(t6_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => k1_bvfunc_1(k9_margrel1(A),A) = A ) ), inference(mizar_proof,[status(thm)],[t40_margrel1,t21_binarith]), [file(binari_6,t6_binari_6),interesting(0.64)]). fof(t14_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k10_margrel1(A,B)) = k10_margrel1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t52_margrel1,t16_binarith]), [file(binari_6,t14_binari_6),interesting(0.63)]). fof(t25_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(A,k1_binarith(A,B)) = k1_binarith(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t20_binarith,t21_binarith]), [file(binari_6,t25_binari_6),interesting(0.63)]). fof(t34_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_bvfunc_1(A,k10_margrel1(A,B)) = k1_bvfunc_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t23_binarith,t18_binarith,t50_margrel1]), [file(binari_6,t34_binari_6),interesting(0.62)]). fof(t49_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binari_5(A,k1_binari_5(A,B)) = k1_bvfunc_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t43_binari_6,t18_binarith,t50_margrel1]), [file(binari_6,t49_binari_6),interesting(0.62)]). fof(t63_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(A,k10_margrel1(A,B)) = k10_margrel1(A,k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t62_binari_6,t23_binarith,t21_binarith,t25_binarith,t22_binarith,t46_margrel1,t7_binarith,t9_binarith,t22_binarith,t46_margrel1,t7_binarith]), [file(binari_6,t63_binari_6),interesting(0.60)]). fof(t71_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k9_margrel1(k2_bvfunc_1(A,B))) = k10_margrel1(A,k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t9_binarith,t10_binarith,t40_margrel1,t10_binarith,t40_margrel1,t22_binarith,t52_margrel1,t16_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith]), [file(binari_6,t71_binari_6),interesting(0.60)]). fof(t65_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(k9_margrel1(A),k2_binarith(A,B)) = k10_margrel1(k9_margrel1(A),B) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t22_binarith,t52_margrel1,t16_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith]), [file(binari_6,t65_binari_6),interesting(0.56)]). fof(t73_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(A,k1_binari_5(A,B)) = k1_bvfunc_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t9_binarith,t25_binarith,t40_margrel1,t52_margrel1,t16_binarith,t23_binarith,t18_binarith,t50_margrel1]), [file(binari_6,t73_binari_6),interesting(0.56)]). fof(t38_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ( k1_bvfunc_1(A,k2_bvfunc_1(A,B)) = k1_bvfunc_1(A,B) & k1_bvfunc_1(A,k2_bvfunc_1(A,B)) = k1_bvfunc_1(A,k1_bvfunc_1(A,B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t31_binari_6,t21_binarith,t18_binarith,t19_binarith,t50_margrel1,t37_binari_6]), [file(binari_6,t38_binari_6),interesting(0.55)]). fof(t46_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binari_5(A,k2_binarith(A,B)) = k1_bvfunc_1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t9_binari_5,t16_binarith,t23_binari_5,t34_binari_6,t9_binarith,t20_binarith,t18_binarith,t19_binarith,t50_margrel1]), [file(binari_6,t46_binari_6),interesting(0.55)]). fof(t74_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(A,k3_binari_5(A,B)) = k1_bvfunc_1(B,A) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t40_margrel1,t10_binarith,t52_margrel1,t16_binarith,t25_binarith,t23_binarith,t18_binarith,t50_margrel1]), [file(binari_6,t74_binari_6),interesting(0.55)]). fof(t10_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => k2_bvfunc_1(k9_margrel1(A),A) = k7_margrel1 ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t6_binari_6,t5_binari_6,t46_margrel1]), [file(binari_6,t10_binari_6),interesting(0.54)]). fof(t27_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(A,k2_bvfunc_1(A,B)) = k1_bvfunc_1(B,A) ) ) ), inference(mizar_proof,[status(thm)],[t22_binari_6,t18_binarith,t19_binarith,t50_margrel1,t20_binarith,t21_binarith]), [file(binari_6,t27_binari_6),interesting(0.54)]). fof(t5_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ( k1_bvfunc_1(A,k9_margrel1(A)) = k9_margrel1(A) & k9_margrel1(k1_bvfunc_1(A,k9_margrel1(A))) = A ) ) ), inference(mizar_proof,[status(thm)],[t21_binarith,t40_margrel1]), [file(binari_6,t5_binari_6),interesting(0.53)]). fof(t40_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_bvfunc_1(A,k3_binari_5(A,B)) = k9_margrel1(A) ) ) ), inference(mizar_proof,[status(thm)],[t33_binari_6,t21_binarith,t25_binarith]), [file(binari_6,t40_binari_6),interesting(0.53)]). fof(t55_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k3_binari_5(A,k10_margrel1(A,B)) = k9_margrel1(A) ) ) ), inference(mizar_proof,[status(thm)],[t15_binari_5,t21_binarith,t10_binarith,t23_binarith,t21_binarith,t25_binarith]), [file(binari_6,t55_binari_6),interesting(0.53)]). fof(t2_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => k1_bvfunc_1(k7_margrel1,A) = k8_margrel1 ) ), inference(mizar_proof,[status(thm)],[d16_margrel1,t19_binarith]), [file(binari_6,t2_binari_6),interesting(0.53)]). fof(t20_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k3_binari_5(A,B)) = k7_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t13_binari_6,t46_margrel1,t49_margrel1]), [file(binari_6,t20_binari_6),interesting(0.52)]). fof(t50_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binari_5(A,k3_binari_5(A,B)) = k8_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t44_binari_6,t18_binarith,t19_binarith]), [file(binari_6,t50_binari_6),interesting(0.52)]). fof(t60_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k3_binari_5(A,k1_binari_5(A,B)) = k7_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t53_binari_6,t46_margrel1,t49_margrel1]), [file(binari_6,t60_binari_6),interesting(0.52)]). fof(t68_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k9_margrel1(k1_bvfunc_1(A,B))) = k10_margrel1(A,k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t10_binarith,t40_margrel1,t52_margrel1,t16_binarith]), [file(binari_6,t68_binari_6),interesting(0.52)]). fof(t8_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => k2_bvfunc_1(k7_margrel1,A) = k9_margrel1(A) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t2_binari_6,t7_binarith,t50_margrel1]), [file(binari_6,t8_binari_6),interesting(0.52)]). fof(t17_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k1_bvfunc_1(A,B)) = k10_margrel1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[t22_binarith,t46_margrel1,t7_binarith]), [file(binari_6,t17_binari_6),interesting(0.51)]). fof(t28_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(A,k1_binari_5(A,B)) = k8_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_6,t18_binarith,t19_binarith]), [file(binari_6,t28_binari_6),interesting(0.51)]). fof(t29_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(A,k3_binari_5(A,B)) = k1_bvfunc_1(B,A) ) ) ), inference(mizar_proof,[status(thm)],[t24_binari_6,t18_binarith,t50_margrel1]), [file(binari_6,t29_binari_6),interesting(0.51)]). fof(t61_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k3_binari_5(A,k3_binari_5(A,B)) = k10_margrel1(k9_margrel1(A),B) ) ) ), inference(mizar_proof,[status(thm)],[t54_binari_6,t46_margrel1,t7_binarith]), [file(binari_6,t61_binari_6),interesting(0.51)]). fof(t15_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k1_binarith(A,B)) = k1_binarith(A,k10_margrel1(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t22_binarith,t16_binarith]), [file(binari_6,t15_binari_6),interesting(0.50)]). fof(t58_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k3_binari_5(A,k1_bvfunc_1(A,B)) = k7_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t20_binarith,t18_binarith,t19_binarith,t41_margrel1]), [file(binari_6,t58_binari_6),interesting(0.50)]). fof(t70_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(k9_margrel1(A),k2_bvfunc_1(A,B)) = k10_margrel1(k9_margrel1(A),k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t52_margrel1,t25_binarith,t22_binarith,t46_margrel1,t7_binarith]), [file(binari_6,t70_binari_6),interesting(0.50)]). fof(t19_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k1_binari_5(A,B)) = k10_margrel1(A,k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t12_binari_6,t46_margrel1,t7_binarith]), [file(binari_6,t19_binari_6),interesting(0.49)]). fof(t85_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k9_margrel1(k1_bvfunc_1(A,B)) = k10_margrel1(A,k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t10_binarith,t40_margrel1]), [file(binari_6,t85_binari_6),interesting(0.49)]). fof(t16_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k2_binarith(A,B)) = k10_margrel1(A,k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t22_binarith,t52_margrel1,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t16_binarith]), [file(binari_6,t16_binari_6),interesting(0.48)]). fof(t86_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k9_margrel1(k2_bvfunc_1(A,B)) = k1_binarith(k10_margrel1(A,k9_margrel1(B)),k10_margrel1(B,k9_margrel1(A))) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t9_binarith,t85_binari_6,t85_binari_6]), [file(binari_6,t86_binari_6),interesting(0.48)]). fof(t13_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k10_margrel1(A,k3_binari_5(B,C)) = k10_margrel1(k10_margrel1(A,k9_margrel1(B)),k9_margrel1(C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_binarith,t52_margrel1]), [file(binari_6,t13_binari_6),interesting(0.45)]). fof(t59_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k3_binari_5(A,k2_bvfunc_1(A,B)) = k10_margrel1(k9_margrel1(A),B) ) ) ), inference(mizar_proof,[status(thm)],[t52_binari_6,t18_binarith,t19_binarith,t50_margrel1,t20_binarith,t21_binarith,t10_binarith,t40_margrel1]), [file(binari_6,t59_binari_6),interesting(0.45)]). fof(t23_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binarith(A,k1_binari_5(B,C)) = k1_binarith(k1_binarith(A,k9_margrel1(B)),k9_margrel1(C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_binarith,t20_binarith]), [file(binari_6,t23_binari_6),interesting(0.44)]). fof(t47_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binari_5(A,k1_bvfunc_1(A,B)) = k9_margrel1(k10_margrel1(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t41_binari_6,t18_binarith,t50_margrel1,t9_binarith]), [file(binari_6,t47_binari_6),interesting(0.43)]). fof(t69_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(A,k1_bvfunc_1(A,B)) = k1_binarith(k9_margrel1(A),k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t25_binarith,t68_binari_6,t23_binarith,t18_binarith,t50_margrel1]), [file(binari_6,t69_binari_6),interesting(0.43)]). fof(t57_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k3_binari_5(A,k2_binarith(A,B)) = k10_margrel1(k9_margrel1(A),k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t51_binari_6,t23_binarith,t18_binarith,t50_margrel1,t23_binarith,t20_binarith,t18_binarith,t19_binarith,t50_margrel1,t20_binarith,t21_binarith,t10_binarith]), [file(binari_6,t57_binari_6),interesting(0.42)]). fof(t26_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(A,k1_bvfunc_1(A,B)) = k8_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t20_binarith,t18_binarith,t19_binarith]), [file(binari_6,t26_binari_6),interesting(0.41)]). fof(t35_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_bvfunc_1(A,k1_binarith(A,B)) = k8_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t20_binarith,t18_binarith,t19_binarith]), [file(binari_6,t35_binari_6),interesting(0.41)]). fof(t64_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(A,k1_binarith(A,B)) = k10_margrel1(k9_margrel1(A),B) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t22_binarith,t46_margrel1,t7_binarith,t10_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith]), [file(binari_6,t64_binari_6),interesting(0.41)]). fof(t81_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(k9_margrel1(A),k2_bvfunc_1(A,B)) = k1_binarith(k9_margrel1(A),B) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t23_binarith,t20_binarith,t21_binarith,t20_binarith,t18_binarith,t19_binarith,t50_margrel1]), [file(binari_6,t81_binari_6),interesting(0.40)]). fof(t83_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(k9_margrel1(A),k1_bvfunc_1(A,B)) = k10_margrel1(A,B) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t40_margrel1,t22_binarith,t46_margrel1,t7_binarith,t10_binarith,t40_margrel1,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith]), [file(binari_6,t83_binari_6),interesting(0.40)]). fof(t48_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binari_5(A,k2_bvfunc_1(A,B)) = k9_margrel1(k10_margrel1(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t42_binari_6,t22_binarith,t46_margrel1,t7_binarith,t22_binarith,t52_margrel1,t46_margrel1,t49_margrel1,t7_binarith,t52_margrel1,t16_binarith]), [file(binari_6,t48_binari_6),interesting(0.39)]). fof(t3_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ( k1_bvfunc_1(A,A) = k8_margrel1 & k9_margrel1(k1_bvfunc_1(A,A)) = k7_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t18_binarith,t41_margrel1]), [file(binari_6,t3_binari_6),interesting(0.39)]). fof(t53_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k3_binari_5(A,k1_binari_5(B,C)) = k10_margrel1(k10_margrel1(k9_margrel1(A),B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_binarith,t40_margrel1,t52_margrel1]), [file(binari_6,t53_binari_6),interesting(0.37)]). fof(t44_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binari_5(A,k3_binari_5(B,C)) = k1_binarith(k1_binarith(k9_margrel1(A),B),C) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_binarith,t40_margrel1,t20_binarith]), [file(binari_6,t44_binari_6),interesting(0.36)]). fof(t45_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binari_5(A,k10_margrel1(A,B)) = k9_margrel1(k10_margrel1(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t6_binari_5,t16_binarith]), [file(binari_6,t45_binari_6),interesting(0.35)]). fof(t4_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k9_margrel1(k1_bvfunc_1(A,B)) = k10_margrel1(A,k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t10_binarith,t40_margrel1]), [file(binari_6,t4_binari_6),interesting(0.35)]). fof(t54_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k3_binari_5(A,k3_binari_5(B,C)) = k1_binarith(k10_margrel1(k9_margrel1(A),B),k10_margrel1(k9_margrel1(A),C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_binarith,t40_margrel1,t22_binarith]), [file(binari_6,t54_binari_6),interesting(0.35)]). fof(t80_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(k9_margrel1(A),k1_bvfunc_1(A,B)) = k1_binarith(k9_margrel1(A),B) ) ) ), inference(mizar_proof,[status(thm)],[t20_binarith,t21_binarith]), [file(binari_6,t80_binari_6),interesting(0.35)]). fof(t36_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_bvfunc_1(A,k2_binarith(A,B)) = k1_binarith(k9_margrel1(A),k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t30_binari_6,t23_binarith,t18_binarith,t50_margrel1,t20_binarith,t23_binarith,t18_binarith,t50_margrel1,t20_binarith,t21_binarith]), [file(binari_6,t36_binari_6),interesting(0.34)]). fof(t79_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(k9_margrel1(A),k3_binari_5(A,B)) = k10_margrel1(k9_margrel1(A),k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t10_binarith,t52_margrel1,t16_binarith]), [file(binari_6,t79_binari_6),interesting(0.34)]). fof(t12_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k10_margrel1(A,k1_binari_5(B,C)) = k1_binarith(k10_margrel1(A,k9_margrel1(B)),k10_margrel1(A,k9_margrel1(C))) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_binarith,t22_binarith]), [file(binari_6,t12_binari_6),interesting(0.33)]). fof(t39_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_bvfunc_1(A,k1_binari_5(A,B)) = k9_margrel1(k10_margrel1(A,B)) ) ) ), inference(mizar_proof,[status(thm)],[t32_binari_6,t21_binarith,t9_binarith]), [file(binari_6,t39_binari_6),interesting(0.33)]). fof(t82_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k1_binarith(k9_margrel1(A),k1_binari_5(A,B)) = k1_binarith(k9_margrel1(A),k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t9_binarith,t20_binarith,t21_binarith]), [file(binari_6,t82_binari_6),interesting(0.33)]). fof(t22_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binarith(A,k2_bvfunc_1(B,C)) = k10_margrel1(k1_binarith(k1_binarith(A,k9_margrel1(B)),C),k1_binarith(k1_binarith(A,k9_margrel1(C)),B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t23_binarith,t20_binarith,t20_binarith]), [file(binari_6,t22_binari_6),interesting(0.30)]). fof(t62_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k2_binarith(A,k10_margrel1(B,C)) = k10_margrel1(k1_binarith(A,k10_margrel1(B,C)),k1_binarith(k9_margrel1(A),k9_margrel1(k10_margrel1(B,C)))) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t23_binarith,t23_binarith,t18_binarith,t50_margrel1,t23_binarith,t18_binarith,t50_margrel1]), [file(binari_6,t62_binari_6),interesting(0.30)]). fof(t32_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_bvfunc_1(A,k1_binari_5(B,C)) = k1_binarith(k1_binarith(k9_margrel1(A),k9_margrel1(B)),k9_margrel1(C)) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_binarith,t20_binarith]), [file(binari_6,t32_binari_6),interesting(0.29)]). fof(t9_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ( k2_bvfunc_1(A,A) = k8_margrel1 & k9_margrel1(k2_bvfunc_1(A,A)) = k7_margrel1 ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t16_binarith,t3_binari_6,t41_margrel1]), [file(binari_6,t9_binari_6),interesting(0.29)]). fof(t76_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k10_margrel1(k9_margrel1(A),k2_bvfunc_1(B,C)) = k10_margrel1(k10_margrel1(k9_margrel1(A),k1_binarith(k9_margrel1(B),C)),k1_binarith(k9_margrel1(C),B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t52_margrel1]), [file(binari_6,t76_binari_6),interesting(0.26)]). fof(t56_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k3_binari_5(A,k1_binarith(A,B)) = k10_margrel1(k9_margrel1(A),k9_margrel1(B)) ) ) ), inference(mizar_proof,[status(thm)],[t16_binari_5,t21_binarith,t10_binarith]), [file(binari_6,t56_binari_6),interesting(0.24)]). fof(t77_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(k9_margrel1(A),k2_bvfunc_1(A,B)) = k10_margrel1(k10_margrel1(k9_margrel1(A),k9_margrel1(B)),k1_binarith(k9_margrel1(A),B)) ) ) ), inference(mizar_proof,[status(thm)],[t76_binari_6,t22_binarith,t46_margrel1,t7_binarith]), [file(binari_6,t77_binari_6),interesting(0.22)]). fof(t78_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(k9_margrel1(A),k1_binari_5(A,B)) = k1_binarith(k9_margrel1(A),k10_margrel1(k9_margrel1(A),k9_margrel1(B))) ) ) ), inference(mizar_proof,[status(thm)],[t9_binarith,t22_binarith,t16_binarith]), [file(binari_6,t78_binari_6),interesting(0.17)]). fof(t75_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(k9_margrel1(A),k1_bvfunc_1(A,B)) = k1_binarith(k9_margrel1(A),k10_margrel1(k9_margrel1(A),B)) ) ) ), inference(mizar_proof,[status(thm)],[t22_binarith,t16_binarith]), [file(binari_6,t75_binari_6),interesting(0.16)]). fof(t42_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binari_5(A,k2_bvfunc_1(B,C)) = k9_margrel1(k10_margrel1(k10_margrel1(A,k1_binarith(k9_margrel1(B),C)),k1_binarith(k9_margrel1(C),B))) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t52_margrel1]), [file(binari_6,t42_binari_6),interesting(0.14)]). fof(t51_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k3_binari_5(A,k2_binarith(B,C)) = k9_margrel1(k1_binarith(k1_binarith(A,k10_margrel1(k9_margrel1(B),C)),k10_margrel1(B,k9_margrel1(C)))) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t20_binarith]), [file(binari_6,t51_binari_6),interesting(0.14)]). fof(t52_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k3_binari_5(A,k2_bvfunc_1(B,C)) = k9_margrel1(k10_margrel1(k1_binarith(k1_binarith(A,k9_margrel1(B)),C),k1_binarith(k1_binarith(A,k9_margrel1(C)),B))) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t23_binarith,t20_binarith,t20_binarith]), [file(binari_6,t52_binari_6),interesting(0.14)]). fof(t30_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_bvfunc_1(A,k2_binarith(B,C)) = k1_binarith(k1_binarith(k9_margrel1(A),k10_margrel1(k9_margrel1(B),C)),k10_margrel1(B,k9_margrel1(C))) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t20_binarith]), [file(binari_6,t30_binari_6),interesting(0.13)]). fof(t11_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k10_margrel1(A,k2_bvfunc_1(B,C)) = k10_margrel1(k10_margrel1(A,k1_binarith(k9_margrel1(B),C)),k1_binarith(k9_margrel1(C),B)) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t52_margrel1]), [file(binari_6,t11_binari_6),interesting(0.12)]). fof(t21_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binarith(A,k2_binarith(B,C)) = k1_binarith(k1_binarith(A,k10_margrel1(k9_margrel1(B),C)),k10_margrel1(B,k9_margrel1(C))) ) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t20_binarith]), [file(binari_6,t21_binari_6),interesting(0.12)]). fof(t31_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_bvfunc_1(A,k2_bvfunc_1(B,C)) = k10_margrel1(k1_binarith(k1_binarith(k9_margrel1(A),k9_margrel1(B)),C),k1_binarith(k1_binarith(k9_margrel1(A),B),k9_margrel1(C))) ) ) ) ), inference(mizar_proof,[status(thm)],[t23_binari_5,t23_binarith,t20_binarith,t20_binarith]), [file(binari_6,t31_binari_6),interesting(0.12)]). fof(t43_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ( k1_binari_5(A,k1_binari_5(B,C)) = k10_margrel1(k1_binarith(k9_margrel1(A),B),k1_binarith(k9_margrel1(A),C)) & k1_binari_5(A,k1_binari_5(B,C)) = k10_margrel1(k1_bvfunc_1(A,B),k1_bvfunc_1(A,C)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_binarith,t40_margrel1,t23_binarith]), [file(binari_6,t43_binari_6),interesting(0.08)]). fof(t24_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ( k1_binarith(A,k3_binari_5(B,C)) = k10_margrel1(k1_binarith(A,k9_margrel1(B)),k1_binarith(A,k9_margrel1(C))) & k1_binarith(A,k3_binari_5(B,C)) = k10_margrel1(k1_bvfunc_1(B,A),k1_bvfunc_1(C,A)) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_binarith,t23_binarith]), [file(binari_6,t24_binari_6),interesting(0.07)]). fof(t41_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ( k1_binari_5(A,k1_bvfunc_1(B,C)) = k10_margrel1(k1_binarith(k9_margrel1(A),B),k1_binarith(k9_margrel1(A),k9_margrel1(C))) & k1_binari_5(A,k1_bvfunc_1(B,C)) = k10_margrel1(k1_bvfunc_1(A,B),k1_bvfunc_1(A,k9_margrel1(C))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t9_binarith,t10_binarith,t40_margrel1,t23_binarith]), [file(binari_6,t41_binari_6),interesting(0.07)]). fof(t84_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(k9_margrel1(A),k1_bvfunc_1(B,A)) = k1_binarith(k10_margrel1(A,k1_binarith(A,k9_margrel1(B))),k10_margrel1(k9_margrel1(A),B)) ) ) ), inference(mizar_proof,[status(thm)],[d2_binarith,t40_margrel1,t10_binarith,t40_margrel1,t52_margrel1,t16_binarith]), [file(binari_6,t84_binari_6),interesting(0.01)]). fof(t23_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_bvfunc_1(A,B) = k10_margrel1(k1_bvfunc_1(A,B),k1_bvfunc_1(B,A)) ) ) ), file(binari_5,t23_binari_5), [interesting(0.00)]). fof(t40_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k9_margrel1(k9_margrel1(A)) = A ) ), file(margrel1,t40_margrel1), [interesting(0.00)]). fof(t21_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,A) = A ) ), file(binarith,t21_binarith), [interesting(0.00)]). fof(t46_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(A,k9_margrel1(A)) = k7_margrel1 ) ), file(margrel1,t46_margrel1), [interesting(0.00)]). fof(t52_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k10_margrel1(A,k10_margrel1(B,C)) = k10_margrel1(k10_margrel1(A,B),C) ) ) ) ), file(margrel1,t52_margrel1), [interesting(0.00)]). fof(t16_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(A,A) = A ) ), file(binarith,t16_binarith), [interesting(0.00)]). fof(t22_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k10_margrel1(A,k1_binarith(B,C)) = k1_binarith(k10_margrel1(A,B),k10_margrel1(A,C)) ) ) ) ), file(binarith,t22_binarith), [interesting(0.00)]). fof(d2_binarith,definition,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k2_binarith(A,B) = k1_binarith(k10_margrel1(k9_margrel1(A),B),k10_margrel1(A,k9_margrel1(B))) ) ) ), file(binarith,d2_binarith), [interesting(0.00)]). fof(t49_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(k7_margrel1,A) = k7_margrel1 ) ), file(margrel1,t49_margrel1), [interesting(0.00)]). fof(t7_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k7_margrel1) = A ) ), file(binarith,t7_binarith), [interesting(0.00)]). fof(t9_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k9_margrel1(k10_margrel1(A,B)) = k1_binarith(k9_margrel1(A),k9_margrel1(B)) ) ) ), file(binarith,t9_binarith), [interesting(0.00)]). fof(t10_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k9_margrel1(k1_binarith(A,B)) = k10_margrel1(k9_margrel1(A),k9_margrel1(B)) ) ) ), file(binarith,t10_binarith), [interesting(0.00)]). fof(t20_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binarith(k1_binarith(A,B),C) = k1_binarith(A,k1_binarith(B,C)) ) ) ) ), file(binarith,t20_binarith), [interesting(0.00)]). fof(t18_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k9_margrel1(A)) = k8_margrel1 ) ), file(binarith,t18_binarith), [interesting(0.00)]). fof(t19_binarith,theorem,( ! [A] : ( v2_margrel1(A) => k1_binarith(A,k8_margrel1) = k8_margrel1 ) ), file(binarith,t19_binarith), [interesting(0.00)]). fof(t23_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binarith(A,k10_margrel1(B,C)) = k10_margrel1(k1_binarith(A,B),k1_binarith(A,C)) ) ) ) ), file(binarith,t23_binarith), [interesting(0.00)]). fof(t50_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => k10_margrel1(k8_margrel1,A) = A ) ), file(margrel1,t50_margrel1), [interesting(0.00)]). fof(t33_binari_6,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => ( k1_bvfunc_1(A,k3_binari_5(B,C)) = k10_margrel1(k1_binarith(k9_margrel1(A),k9_margrel1(B)),k1_binarith(k9_margrel1(A),k9_margrel1(C))) & k1_bvfunc_1(A,k3_binari_5(B,C)) = k10_margrel1(k1_bvfunc_1(A,k9_margrel1(B)),k1_bvfunc_1(A,k9_margrel1(C))) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t10_binarith,t23_binarith]), [file(binari_6,t33_binari_6),interesting(0.00)]). fof(t25_binarith,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => k10_margrel1(A,k1_binarith(A,B)) = A ) ) ), file(binarith,t25_binarith), [interesting(0.00)]). fof(t6_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binari_5(A,k10_margrel1(B,C)) = k9_margrel1(k10_margrel1(k10_margrel1(A,B),C)) ) ) ) ), file(binari_5,t6_binari_5), [interesting(0.00)]). fof(t9_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k1_binari_5(A,k2_binarith(B,C)) = k2_bvfunc_1(k10_margrel1(A,B),k10_margrel1(A,C)) ) ) ) ), file(binari_5,t9_binari_5), [interesting(0.00)]). fof(t15_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k3_binari_5(A,k10_margrel1(B,C)) = k1_binarith(k9_margrel1(k1_binarith(A,B)),k9_margrel1(k1_binarith(A,C))) ) ) ) ), file(binari_5,t15_binari_5), [interesting(0.00)]). fof(t16_binari_5,theorem,( ! [A] : ( v2_margrel1(A) => ! [B] : ( v2_margrel1(B) => ! [C] : ( v2_margrel1(C) => k3_binari_5(A,k1_binarith(B,C)) = k9_margrel1(k1_binarith(k1_binarith(A,B),C)) ) ) ) ), file(binari_5,t16_binari_5), [interesting(0.00)]). fof(t41_margrel1,theorem,( ! [A] : ( v2_margrel1(A) => ( ( A = k7_margrel1 => k9_margrel1(A) = k8_margrel1 ) & ( k9_margrel1(A) = k8_margrel1 => A = k7_margrel1 ) & ( A = k8_margrel1 => k9_margrel1(A) = k7_margrel1 ) & ( k9_margrel1(A) = k7_margrel1 => A = k8_margrel1 ) ) ) ), file(margrel1,t41_margrel1), [interesting(0.00)]). fof(d16_margrel1,definition,( ! [A] : ( v2_margrel1(A) => ( ( A = k7_margrel1 => k9_margrel1(A) = k8_margrel1 ) & ( A != k7_margrel1 => k9_margrel1(A) = k7_margrel1 ) ) ) ), file(margrel1,d16_margrel1), [interesting(0.00)]).