また
同じ条件を
(E x)(A y)[ 0 <= x /\ x <= a /\ x^2 - 2 x = m /\ [ [ 0 <= y /\ y<= a ] ==> y^2 - 2 y >= m ] ].
と入力すると，QEPCADは
a >= 0 /\ m + 1 >= 0 /\ m - a^2 + 2 a <= 0 /\ [ [ a - 1 >= 0
/\ m + 1 = 0 ] \/ [ a - 1 < 0 /\ m - a^2 + 2 a = 0 ] ]
と答えます．
同じ条件を
(E x)(A y)[ 0 <= x /\ x <= a /\ x^2 - 2 x = m /\ [ [ 0 <= y /\ y<= a ] ==> y^2 - 2 y >= m ] ].
と入力すると，QEPCADは
a >= 0 /\ m + 1 >= 0 /\ m - a^2 + 2 a <= 0 /\ [ [ a - 1 >= 0
/\ m + 1 = 0 ] \/ [ a - 1 < 0 /\ m - a^2 + 2 a = 0 ] ]
と答えます．