Idea

Tengo la impresión de que el lenguaje de especificación permite expresar formulas demasiado complejas (con varios niveles de anidamiento, etc.). Esto puede que perjudique el funcionamiento del demostrador.

Probar reduciendo la complejidad de las fórmulas al permitir únicamente comparar variables. Cualquier cosa más compleja deberá ser simulada creando variables y hacerlas valer lo que uno quiere comparar a través de instrucciones del lenguaje de programación.