Problem (2021SilkRoadp3): In a triangle $ABC$, $M$ is the midpoint of the $AB$. A point $B_1$ is marked on $AC$ such that $CB=CB_1$. Circle $\omega$ and $\omega_1$, the circumcircles of triangles $ABC$ and $BMB_1$, respectively, intersect again at $K$. Let $Q$ be the midpoint of the arc $ACB$ on $\omega$. Let $B_1Q$ and $BC$ intersect at $E$. Prove that $KC$ bisects $B_1E$.
AlphaGeometry formalization: a b c = triangle; m = midpoint a b; b1 = on_line a c, eqdistance b1 c c b; o = circumcenter a b c; o1 = circumcenter b m b1; k = on_circle o a, on_circle o1 b; q = on_bline a b, on_circle o a; e = on_line b1 q, on_line b c; m1 = midpoint b1 e ? coll m1 k c
HAGeo formalization: A B C = triangle; M = midpoint A B; AC = line A C; (C,B) = circle_center_point C B; B1 = intersection AC (C,B); O = circumcenter A B C; (ABC) = circle_center_point O A; O1 = circumcenter B M B1; (BMB1) = circle_center_point O1 B; K = intersection (ABC) (BMB1); Q = midarc A C B; B1Q = line B1 Q; BC = line B C; E = intersection B1Q BC; L = midpoint B1 E; Prove: collinear C K L
Difficulty score: 4.2