A good way to formalize IMO 2004 P1?

[thtrieu]

When I tried running GMB with

(param (A B C) acute-tri)
(assert (not (cong A B A C)))
(define M point (inter-lc (line A B) (diam B C) (rs-neq B)))
(define N point (inter-lc (line A C) (diam B C) (rs-neq C)))
(define O point (midp B C))
(define R point (inter-ll (i-bisector B A C) (i-bisector M O N)))
(define O1 point (circumcenter B M R))
(define O2 point (circumcenter C N R))
(define P point (inter-cc (circumcircle B M R) (circumcircle C N R) (rs-neq R)))
(eval (on-seg P B C))

It can find a pretty good solution. But when running with:

(param (a b c) acute-tri)
(assert (not (cong a b a c)))
(define o point (midp b c))
(param m point)
(assert (coll m a b))
(assert (cong o m o b)) 
(assert (not (= m b))) 
(param n point)
(assert (coll n a c))
(assert (cong o n o c)) 
(assert (not (= n c))) 
(param r point)
(assert (on-line r (i-bisector b a c)))
(assert (on-line r (i-bisector m o n)))
(define o1 point (circumcenter b m r))
(define o2 point (circumcenter c n r))
(param p point)
(assert (cong o1 p o1 r))
(assert (cong o2 p o2 r))
(assert (not (= p r)))
(eval (on-seg p b c))

It cannot. Is the reason that inter-ll and inter-cc makes the optimization problem much easier, or am I missing something?