xmath
boyer
breadt
divide
equal
formul
heuris
model
rewrit
semant
simple
skolem
unify
.END