Problem (2023PKUSummerp3): In $\triangle ABC$, $BC$ is the longest side. The perpendicular bisector of $AC$ intersects $BC, AB$ at $D,E$ respectively, and the symmetric point of $B$ w.r.t. this perpendicular bisector is $F$. The perpendicular bisector of $AB$ intersects $BC,AC$ at $J,K$ respectively, and the symmetric point of $C$ w.r.t. this perpendicular bisector is $L$. $BL \cap CF = N$, $\odot(BJL) \cap JN = J,R$, $\odot(CDF) \cap DN = D,Q$. The parallel line of $BC$ passes through $N$ and intersects $EK$ at $P$. $FL \cap BC = M$. $l$ is the diameter of $\odot(ABC)$ parallel to BC. Prove that $QR, MP$ and $l$ are cocurrent.
AlphaGeometry formalization: a b c = triangle; d = on_bline a c, on_line b c; e = on_bline a c, on_line a b; f = reflect b d e; j = on_bline a b, on_line b c; k = on_bline a b, on_line a c; l = reflect c j k; n = on_line b l, on_line c f; o1 = circumcenter b j l; r = on_circle o1 b, on_line j n; o2 = circumcenter c d f; q = on_circle o2 c, on_line d n; p = on_pline n b c, on_line e k; m = on_line f l, on_line b c; o = circumcenter a b c; x = on_line q r, on_line m p ? para o x b c
HAGeo formalization: A B C = triangle; l1 = perpendicular_bisector A C; BC = line B C; D = intersection l1 BC; AB = line A B; E = intersection l1 AB; DE = line D E; F = reflect_point_wrt_line B DE; l2 = perpendicular_bisector A B; J = intersection l2 BC; AC = line A C; K = intersection l2 AC; JK = line J K; L = reflect_point_wrt_line C JK; BL = line B L; CF = line C F; N = intersection BL CF; O1 = circumcenter B J L; (O1) = circle_center_point O1 B; JN = line J N; R = intersection (O1) JN; O2 = circumcenter C D F; (O2) = circle_center_point O2 C; DN = line D N; Q = intersection (O2) DN; l3 = parallel_line N BC; EK = line E K; P = intersection l3 EK; FL = line F L; M = intersection FL BC; O = circumcenter A B C; QR = line Q R; MP = line M P; X = intersection QR MP; OX = line O X; Prove: parallel OX BC
Difficulty score: 5.7