check_ast_ac.cpp

#include "ast.h"
#include "ast_gen.h"
#include "parser.h"

void check_ast_ac(size_t& good, size_t& bad) {
    AstGen::Gen const
        x = Ast::Identifier("x"),
        y = Ast::Identifier("y"),
        z = Ast::Identifier("z");

#define CHECK_AST(expr, ast) ++(Parser::check_ast(expr, ast)?good:bad)

#pragma GCC diagnostic push
#pragma GCC diagnostic ignored "-Wlogical-not-parentheses"
#pragma GCC diagnostic ignored "-Wparentheses"
    CHECK_AST(" not (x)* not y< +z",  not (x)* not y< +z);
    CHECK_AST(" not (x* not y)< +z",  not (x* not y)< +z);
    CHECK_AST(" not x*( not y)< +z",  not x*( not y)< +z);
    CHECK_AST(" not x* not (y)< +z",  not x* not (y)< +z);
    CHECK_AST("( not x)* not y< -z", ( not x)* not y< -z);
    CHECK_AST("( not x* not y)< -z", ( not x* not y)< -z);
    CHECK_AST(" not (x)* not y< -z",  not (x)* not y< -z);
    CHECK_AST(" not (x* not y)< -z",  not (x* not y)< -z);
    CHECK_AST(" not x*( not y)< -z",  not x*( not y)< -z);
    CHECK_AST(" not x* not (y)< -z",  not x* not (y)< -z);
    CHECK_AST("( not x)* not y< not z", ( not x)* not y< not z);
    CHECK_AST("( not x* not y)< not z", ( not x* not y)< not z);
    CHECK_AST(" not (x)* not y< not z",  not (x)* not y< not z);
    CHECK_AST(" not (x* not y)< not z",  not (x* not y)< not z);
    CHECK_AST(" not x*( not y)< not z",  not x*( not y)< not z);
    CHECK_AST(" not x* not (y)< not z",  not x* not (y)< not z);
    CHECK_AST("(x)*y<=z", (x)*y<=z);
    CHECK_AST("(x*y)<=z", (x*y)<=z);
    CHECK_AST("x*(y)<=z", x*(y)<=z);
    CHECK_AST("(x)*y<= +z", (x)*y<= +z);
    CHECK_AST("(x*y)<= +z", (x*y)<= +z);
    CHECK_AST("x*(y)<= +z", x*(y)<= +z);
    CHECK_AST("(x)*y<= -z", (x)*y<= -z);
    CHECK_AST("(x*y)<= -z", (x*y)<= -z);
    CHECK_AST("x*(y)<= -z", x*(y)<= -z);
    CHECK_AST("(x)*y<= not z", (x)*y<= not z);
    CHECK_AST("(x*y)<= not z", (x*y)<= not z);
    CHECK_AST("x*(y)<= not z", x*(y)<= not z);
    CHECK_AST("(x)* +y<=z", (x)* +y<=z);
    CHECK_AST("(x* +y)<=z", (x* +y)<=z);
    CHECK_AST("x*( +y)<=z", x*( +y)<=z);
    CHECK_AST("x* +(y)<=z", x* +(y)<=z);
    CHECK_AST("(x)* +y<= +z", (x)* +y<= +z);
    CHECK_AST("(x* +y)<= +z", (x* +y)<= +z);
    CHECK_AST("x*( +y)<= +z", x*( +y)<= +z);
    CHECK_AST("x* +(y)<= +z", x* +(y)<= +z);
    CHECK_AST("(x)* +y<= -z", (x)* +y<= -z);
    CHECK_AST("(x* +y)<= -z", (x* +y)<= -z);
    CHECK_AST("x*( +y)<= -z", x*( +y)<= -z);
    CHECK_AST("x* +(y)<= -z", x* +(y)<= -z);
    CHECK_AST("(x)* +y<= not z", (x)* +y<= not z);
    CHECK_AST("(x* +y)<= not z", (x* +y)<= not z);
    CHECK_AST("x*( +y)<= not z", x*( +y)<= not z);
    CHECK_AST("x* +(y)<= not z", x* +(y)<= not z);
    CHECK_AST("(x)* -y<=z", (x)* -y<=z);
    CHECK_AST("(x* -y)<=z", (x* -y)<=z);
    CHECK_AST("x*( -y)<=z", x*( -y)<=z);
    CHECK_AST("x* -(y)<=z", x* -(y)<=z);
    CHECK_AST("(x)* -y<= +z", (x)* -y<= +z);
    CHECK_AST("(x* -y)<= +z", (x* -y)<= +z);
    CHECK_AST("x*( -y)<= +z", x*( -y)<= +z);
    CHECK_AST("x* -(y)<= +z", x* -(y)<= +z);
    CHECK_AST("(x)* -y<= -z", (x)* -y<= -z);
    CHECK_AST("(x* -y)<= -z", (x* -y)<= -z);
    CHECK_AST("x*( -y)<= -z", x*( -y)<= -z);
    CHECK_AST("x* -(y)<= -z", x* -(y)<= -z);
    CHECK_AST("(x)* -y<= not z", (x)* -y<= not z);
    CHECK_AST("(x* -y)<= not z", (x* -y)<= not z);
    CHECK_AST("x*( -y)<= not z", x*( -y)<= not z);
    CHECK_AST("x* -(y)<= not z", x* -(y)<= not z);
    CHECK_AST("(x)* not y<=z", (x)* not y<=z);
    CHECK_AST("(x* not y)<=z", (x* not y)<=z);
    CHECK_AST("x*( not y)<=z", x*( not y)<=z);
    CHECK_AST("x* not (y)<=z", x* not (y)<=z);
    CHECK_AST("(x)* not y<= +z", (x)* not y<= +z);
    CHECK_AST("(x* not y)<= +z", (x* not y)<= +z);
    CHECK_AST("x*( not y)<= +z", x*( not y)<= +z);
    CHECK_AST("x* not (y)<= +z", x* not (y)<= +z);
    CHECK_AST("(x)* not y<= -z", (x)* not y<= -z);
    CHECK_AST("(x* not y)<= -z", (x* not y)<= -z);
    CHECK_AST("x*( not y)<= -z", x*( not y)<= -z);
    CHECK_AST("x* not (y)<= -z", x* not (y)<= -z);
    CHECK_AST("(x)* not y<= not z", (x)* not y<= not z);
    CHECK_AST("(x* not y)<= not z", (x* not y)<= not z);
    CHECK_AST("x*( not y)<= not z", x*( not y)<= not z);
    CHECK_AST("x* not (y)<= not z", x* not (y)<= not z);
    CHECK_AST("( +x)*y<=z", ( +x)*y<=z);
    CHECK_AST("( +x*y)<=z", ( +x*y)<=z);
    CHECK_AST(" +(x)*y<=z",  +(x)*y<=z);
    CHECK_AST(" +(x*y)<=z",  +(x*y)<=z);
    CHECK_AST(" +x*(y)<=z",  +x*(y)<=z);
    CHECK_AST("( +x)*y<= +z", ( +x)*y<= +z);
    CHECK_AST("( +x*y)<= +z", ( +x*y)<= +z);
    CHECK_AST(" +(x)*y<= +z",  +(x)*y<= +z);
    CHECK_AST(" +(x*y)<= +z",  +(x*y)<= +z);
    CHECK_AST(" +x*(y)<= +z",  +x*(y)<= +z);
    CHECK_AST("( +x)*y<= -z", ( +x)*y<= -z);
    CHECK_AST("( +x*y)<= -z", ( +x*y)<= -z);
    CHECK_AST(" +(x)*y<= -z",  +(x)*y<= -z);
    CHECK_AST(" +(x*y)<= -z",  +(x*y)<= -z);
    CHECK_AST(" +x*(y)<= -z",  +x*(y)<= -z);
    CHECK_AST("( +x)*y<= not z", ( +x)*y<= not z);
    CHECK_AST("( +x*y)<= not z", ( +x*y)<= not z);
    CHECK_AST(" +(x)*y<= not z",  +(x)*y<= not z);
    CHECK_AST(" +(x*y)<= not z",  +(x*y)<= not z);
    CHECK_AST(" +x*(y)<= not z",  +x*(y)<= not z);
    CHECK_AST("( +x)* +y<=z", ( +x)* +y<=z);
    CHECK_AST("( +x* +y)<=z", ( +x* +y)<=z);
    CHECK_AST(" +(x)* +y<=z",  +(x)* +y<=z);
    CHECK_AST(" +(x* +y)<=z",  +(x* +y)<=z);
    CHECK_AST(" +x*( +y)<=z",  +x*( +y)<=z);
    CHECK_AST(" +x* +(y)<=z",  +x* +(y)<=z);
    CHECK_AST("( +x)* +y<= +z", ( +x)* +y<= +z);
    CHECK_AST("( +x* +y)<= +z", ( +x* +y)<= +z);
    CHECK_AST(" +(x)* +y<= +z",  +(x)* +y<= +z);
    CHECK_AST(" +(x* +y)<= +z",  +(x* +y)<= +z);
    CHECK_AST(" +x*( +y)<= +z",  +x*( +y)<= +z);
    CHECK_AST(" +x* +(y)<= +z",  +x* +(y)<= +z);
    CHECK_AST("( +x)* +y<= -z", ( +x)* +y<= -z);
    CHECK_AST("( +x* +y)<= -z", ( +x* +y)<= -z);
    CHECK_AST(" +(x)* +y<= -z",  +(x)* +y<= -z);
    CHECK_AST(" +(x* +y)<= -z",  +(x* +y)<= -z);
    CHECK_AST(" +x*( +y)<= -z",  +x*( +y)<= -z);
    CHECK_AST(" +x* +(y)<= -z",  +x* +(y)<= -z);
    CHECK_AST("( +x)* +y<= not z", ( +x)* +y<= not z);
    CHECK_AST("( +x* +y)<= not z", ( +x* +y)<= not z);
    CHECK_AST(" +(x)* +y<= not z",  +(x)* +y<= not z);
    CHECK_AST(" +(x* +y)<= not z",  +(x* +y)<= not z);
    CHECK_AST(" +x*( +y)<= not z",  +x*( +y)<= not z);
    CHECK_AST(" +x* +(y)<= not z",  +x* +(y)<= not z);
    CHECK_AST("( +x)* -y<=z", ( +x)* -y<=z);
    CHECK_AST("( +x* -y)<=z", ( +x* -y)<=z);
    CHECK_AST(" +(x)* -y<=z",  +(x)* -y<=z);
    CHECK_AST(" +(x* -y)<=z",  +(x* -y)<=z);
    CHECK_AST(" +x*( -y)<=z",  +x*( -y)<=z);
    CHECK_AST(" +x* -(y)<=z",  +x* -(y)<=z);
    CHECK_AST("( +x)* -y<= +z", ( +x)* -y<= +z);
    CHECK_AST("( +x* -y)<= +z", ( +x* -y)<= +z);
    CHECK_AST(" +(x)* -y<= +z",  +(x)* -y<= +z);
    CHECK_AST(" +(x* -y)<= +z",  +(x* -y)<= +z);
    CHECK_AST(" +x*( -y)<= +z",  +x*( -y)<= +z);
    CHECK_AST(" +x* -(y)<= +z",  +x* -(y)<= +z);
    CHECK_AST("( +x)* -y<= -z", ( +x)* -y<= -z);
    CHECK_AST("( +x* -y)<= -z", ( +x* -y)<= -z);
    CHECK_AST(" +(x)* -y<= -z",  +(x)* -y<= -z);
    CHECK_AST(" +(x* -y)<= -z",  +(x* -y)<= -z);
    CHECK_AST(" +x*( -y)<= -z",  +x*( -y)<= -z);
    CHECK_AST(" +x* -(y)<= -z",  +x* -(y)<= -z);
    CHECK_AST("( +x)* -y<= not z", ( +x)* -y<= not z);
    CHECK_AST("( +x* -y)<= not z", ( +x* -y)<= not z);
    CHECK_AST(" +(x)* -y<= not z",  +(x)* -y<= not z);
    CHECK_AST(" +(x* -y)<= not z",  +(x* -y)<= not z);
    CHECK_AST(" +x*( -y)<= not z",  +x*( -y)<= not z);
    CHECK_AST(" +x* -(y)<= not z",  +x* -(y)<= not z);
    CHECK_AST("( +x)* not y<=z", ( +x)* not y<=z);
    CHECK_AST("( +x* not y)<=z", ( +x* not y)<=z);
    CHECK_AST(" +(x)* not y<=z",  +(x)* not y<=z);
    CHECK_AST(" +(x* not y)<=z",  +(x* not y)<=z);
    CHECK_AST(" +x*( not y)<=z",  +x*( not y)<=z);
    CHECK_AST(" +x* not (y)<=z",  +x* not (y)<=z);
    CHECK_AST("( +x)* not y<= +z", ( +x)* not y<= +z);
    CHECK_AST("( +x* not y)<= +z", ( +x* not y)<= +z);
    CHECK_AST(" +(x)* not y<= +z",  +(x)* not y<= +z);
    CHECK_AST(" +(x* not y)<= +z",  +(x* not y)<= +z);
    CHECK_AST(" +x*( not y)<= +z",  +x*( not y)<= +z);
    CHECK_AST(" +x* not (y)<= +z",  +x* not (y)<= +z);
    CHECK_AST("( +x)* not y<= -z", ( +x)* not y<= -z);
    CHECK_AST("( +x* not y)<= -z", ( +x* not y)<= -z);
    CHECK_AST(" +(x)* not y<= -z",  +(x)* not y<= -z);
    CHECK_AST(" +(x* not y)<= -z",  +(x* not y)<= -z);
    CHECK_AST(" +x*( not y)<= -z",  +x*( not y)<= -z);
    CHECK_AST(" +x* not (y)<= -z",  +x* not (y)<= -z);
    CHECK_AST("( +x)* not y<= not z", ( +x)* not y<= not z);
    CHECK_AST("( +x* not y)<= not z", ( +x* not y)<= not z);
    CHECK_AST(" +(x)* not y<= not z",  +(x)* not y<= not z);
    CHECK_AST(" +(x* not y)<= not z",  +(x* not y)<= not z);
    CHECK_AST(" +x*( not y)<= not z",  +x*( not y)<= not z);
    CHECK_AST(" +x* not (y)<= not z",  +x* not (y)<= not z);
    CHECK_AST("( -x)*y<=z", ( -x)*y<=z);
    CHECK_AST("( -x*y)<=z", ( -x*y)<=z);
    CHECK_AST(" -(x)*y<=z",  -(x)*y<=z);
    CHECK_AST(" -(x*y)<=z",  -(x*y)<=z);
    CHECK_AST(" -x*(y)<=z",  -x*(y)<=z);
    CHECK_AST("( -x)*y<= +z", ( -x)*y<= +z);
    CHECK_AST("( -x*y)<= +z", ( -x*y)<= +z);
    CHECK_AST(" -(x)*y<= +z",  -(x)*y<= +z);
    CHECK_AST(" -(x*y)<= +z",  -(x*y)<= +z);
    CHECK_AST(" -x*(y)<= +z",  -x*(y)<= +z);
    CHECK_AST("( -x)*y<= -z", ( -x)*y<= -z);
    CHECK_AST("( -x*y)<= -z", ( -x*y)<= -z);
    CHECK_AST(" -(x)*y<= -z",  -(x)*y<= -z);
    CHECK_AST(" -(x*y)<= -z",  -(x*y)<= -z);
    CHECK_AST(" -x*(y)<= -z",  -x*(y)<= -z);
    CHECK_AST("( -x)*y<= not z", ( -x)*y<= not z);
    CHECK_AST("( -x*y)<= not z", ( -x*y)<= not z);
    CHECK_AST(" -(x)*y<= not z",  -(x)*y<= not z);
    CHECK_AST(" -(x*y)<= not z",  -(x*y)<= not z);
    CHECK_AST(" -x*(y)<= not z",  -x*(y)<= not z);
    CHECK_AST("( -x)* +y<=z", ( -x)* +y<=z);
    CHECK_AST("( -x* +y)<=z", ( -x* +y)<=z);
    CHECK_AST(" -(x)* +y<=z",  -(x)* +y<=z);
    CHECK_AST(" -(x* +y)<=z",  -(x* +y)<=z);
    CHECK_AST(" -x*( +y)<=z",  -x*( +y)<=z);
    CHECK_AST(" -x* +(y)<=z",  -x* +(y)<=z);
    CHECK_AST("( -x)* +y<= +z", ( -x)* +y<= +z);
    CHECK_AST("( -x* +y)<= +z", ( -x* +y)<= +z);
    CHECK_AST(" -(x)* +y<= +z",  -(x)* +y<= +z);
    CHECK_AST(" -(x* +y)<= +z",  -(x* +y)<= +z);
    CHECK_AST(" -x*( +y)<= +z",  -x*( +y)<= +z);
    CHECK_AST(" -x* +(y)<= +z",  -x* +(y)<= +z);
    CHECK_AST("( -x)* +y<= -z", ( -x)* +y<= -z);
    CHECK_AST("( -x* +y)<= -z", ( -x* +y)<= -z);
    CHECK_AST(" -(x)* +y<= -z",  -(x)* +y<= -z);
    CHECK_AST(" -(x* +y)<= -z",  -(x* +y)<= -z);
    CHECK_AST(" -x*( +y)<= -z",  -x*( +y)<= -z);
    CHECK_AST(" -x* +(y)<= -z",  -x* +(y)<= -z);
    CHECK_AST("( -x)* +y<= not z", ( -x)* +y<= not z);
    CHECK_AST("( -x* +y)<= not z", ( -x* +y)<= not z);
    CHECK_AST(" -(x)* +y<= not z",  -(x)* +y<= not z);
    CHECK_AST(" -(x* +y)<= not z",  -(x* +y)<= not z);
    CHECK_AST(" -x*( +y)<= not z",  -x*( +y)<= not z);
    CHECK_AST(" -x* +(y)<= not z",  -x* +(y)<= not z);
    CHECK_AST("( -x)* -y<=z", ( -x)* -y<=z);
    CHECK_AST("( -x* -y)<=z", ( -x* -y)<=z);
    CHECK_AST(" -(x)* -y<=z",  -(x)* -y<=z);
    CHECK_AST(" -(x* -y)<=z",  -(x* -y)<=z);
    CHECK_AST(" -x*( -y)<=z",  -x*( -y)<=z);
    CHECK_AST(" -x* -(y)<=z",  -x* -(y)<=z);
    CHECK_AST("( -x)* -y<= +z", ( -x)* -y<= +z);
    CHECK_AST("( -x* -y)<= +z", ( -x* -y)<= +z);
    CHECK_AST(" -(x)* -y<= +z",  -(x)* -y<= +z);
    CHECK_AST(" -(x* -y)<= +z",  -(x* -y)<= +z);
    CHECK_AST(" -x*( -y)<= +z",  -x*( -y)<= +z);
    CHECK_AST(" -x* -(y)<= +z",  -x* -(y)<= +z);
    CHECK_AST("( -x)* -y<= -z", ( -x)* -y<= -z);
    CHECK_AST("( -x* -y)<= -z", ( -x* -y)<= -z);
    CHECK_AST(" -(x)* -y<= -z",  -(x)* -y<= -z);
    CHECK_AST(" -(x* -y)<= -z",  -(x* -y)<= -z);
    CHECK_AST(" -x*( -y)<= -z",  -x*( -y)<= -z);
    CHECK_AST(" -x* -(y)<= -z",  -x* -(y)<= -z);
    CHECK_AST("( -x)* -y<= not z", ( -x)* -y<= not z);
    CHECK_AST("( -x* -y)<= not z", ( -x* -y)<= not z);
    CHECK_AST(" -(x)* -y<= not z",  -(x)* -y<= not z);
    CHECK_AST(" -(x* -y)<= not z",  -(x* -y)<= not z);
    CHECK_AST(" -x*( -y)<= not z",  -x*( -y)<= not z);
    CHECK_AST(" -x* -(y)<= not z",  -x* -(y)<= not z);
    CHECK_AST("( -x)* not y<=z", ( -x)* not y<=z);
    CHECK_AST("( -x* not y)<=z", ( -x* not y)<=z);
    CHECK_AST(" -(x)* not y<=z",  -(x)* not y<=z);
    CHECK_AST(" -(x* not y)<=z",  -(x* not y)<=z);
    CHECK_AST(" -x*( not y)<=z",  -x*( not y)<=z);
    CHECK_AST(" -x* not (y)<=z",  -x* not (y)<=z);
    CHECK_AST("( -x)* not y<= +z", ( -x)* not y<= +z);
    CHECK_AST("( -x* not y)<= +z", ( -x* not y)<= +z);
    CHECK_AST(" -(x)* not y<= +z",  -(x)* not y<= +z);
    CHECK_AST(" -(x* not y)<= +z",  -(x* not y)<= +z);
    CHECK_AST(" -x*( not y)<= +z",  -x*( not y)<= +z);
    CHECK_AST(" -x* not (y)<= +z",  -x* not (y)<= +z);
    CHECK_AST("( -x)* not y<= -z", ( -x)* not y<= -z);
    CHECK_AST("( -x* not y)<= -z", ( -x* not y)<= -z);
    CHECK_AST(" -(x)* not y<= -z",  -(x)* not y<= -z);
    CHECK_AST(" -(x* not y)<= -z",  -(x* not y)<= -z);
    CHECK_AST(" -x*( not y)<= -z",  -x*( not y)<= -z);
    CHECK_AST(" -x* not (y)<= -z",  -x* not (y)<= -z);
    CHECK_AST("( -x)* not y<= not z", ( -x)* not y<= not z);
    CHECK_AST("( -x* not y)<= not z", ( -x* not y)<= not z);
    CHECK_AST(" -(x)* not y<= not z",  -(x)* not y<= not z);
    CHECK_AST(" -(x* not y)<= not z",  -(x* not y)<= not z);
    CHECK_AST(" -x*( not y)<= not z",  -x*( not y)<= not z);
    CHECK_AST(" -x* not (y)<= not z",  -x* not (y)<= not z);
    CHECK_AST("( not x)*y<=z", ( not x)*y<=z);
    CHECK_AST("( not x*y)<=z", ( not x*y)<=z);
    CHECK_AST(" not (x)*y<=z",  not (x)*y<=z);
    CHECK_AST(" not (x*y)<=z",  not (x*y)<=z);
    CHECK_AST(" not x*(y)<=z",  not x*(y)<=z);
    CHECK_AST("( not x)*y<= +z", ( not x)*y<= +z);
    CHECK_AST("( not x*y)<= +z", ( not x*y)<= +z);
    CHECK_AST(" not (x)*y<= +z",  not (x)*y<= +z);
    CHECK_AST(" not (x*y)<= +z",  not (x*y)<= +z);
    CHECK_AST(" not x*(y)<= +z",  not x*(y)<= +z);
    CHECK_AST("( not x)*y<= -z", ( not x)*y<= -z);
    CHECK_AST("( not x*y)<= -z", ( not x*y)<= -z);
    CHECK_AST(" not (x)*y<= -z",  not (x)*y<= -z);
    CHECK_AST(" not (x*y)<= -z",  not (x*y)<= -z);
    CHECK_AST(" not x*(y)<= -z",  not x*(y)<= -z);
    CHECK_AST("( not x)*y<= not z", ( not x)*y<= not z);
    CHECK_AST("( not x*y)<= not z", ( not x*y)<= not z);
    CHECK_AST(" not (x)*y<= not z",  not (x)*y<= not z);
    CHECK_AST(" not (x*y)<= not z",  not (x*y)<= not z);
    CHECK_AST(" not x*(y)<= not z",  not x*(y)<= not z);
    CHECK_AST("( not x)* +y<=z", ( not x)* +y<=z);
    CHECK_AST("( not x* +y)<=z", ( not x* +y)<=z);
    CHECK_AST(" not (x)* +y<=z",  not (x)* +y<=z);
    CHECK_AST(" not (x* +y)<=z",  not (x* +y)<=z);
    CHECK_AST(" not x*( +y)<=z",  not x*( +y)<=z);
    CHECK_AST(" not x* +(y)<=z",  not x* +(y)<=z);
    CHECK_AST("( not x)* +y<= +z", ( not x)* +y<= +z);
    CHECK_AST("( not x* +y)<= +z", ( not x* +y)<= +z);
    CHECK_AST(" not (x)* +y<= +z",  not (x)* +y<= +z);
    CHECK_AST(" not (x* +y)<= +z",  not (x* +y)<= +z);
    CHECK_AST(" not x*( +y)<= +z",  not x*( +y)<= +z);
    CHECK_AST(" not x* +(y)<= +z",  not x* +(y)<= +z);
    CHECK_AST("( not x)* +y<= -z", ( not x)* +y<= -z);
    CHECK_AST("( not x* +y)<= -z", ( not x* +y)<= -z);
    CHECK_AST(" not (x)* +y<= -z",  not (x)* +y<= -z);
    CHECK_AST(" not (x* +y)<= -z",  not (x* +y)<= -z);
    CHECK_AST(" not x*( +y)<= -z",  not x*( +y)<= -z);
    CHECK_AST(" not x* +(y)<= -z",  not x* +(y)<= -z);
    CHECK_AST("( not x)* +y<= not z", ( not x)* +y<= not z);
    CHECK_AST("( not x* +y)<= not z", ( not x* +y)<= not z);
    CHECK_AST(" not (x)* +y<= not z",  not (x)* +y<= not z);
    CHECK_AST(" not (x* +y)<= not z",  not (x* +y)<= not z);
    CHECK_AST(" not x*( +y)<= not z",  not x*( +y)<= not z);
    CHECK_AST(" not x* +(y)<= not z",  not x* +(y)<= not z);
    CHECK_AST("( not x)* -y<=z", ( not x)* -y<=z);
    CHECK_AST("( not x* -y)<=z", ( not x* -y)<=z);
    CHECK_AST(" not (x)* -y<=z",  not (x)* -y<=z);
    CHECK_AST(" not (x* -y)<=z",  not (x* -y)<=z);
    CHECK_AST(" not x*( -y)<=z",  not x*( -y)<=z);
    CHECK_AST(" not x* -(y)<=z",  not x* -(y)<=z);
    CHECK_AST("( not x)* -y<= +z", ( not x)* -y<= +z);
    CHECK_AST("( not x* -y)<= +z", ( not x* -y)<= +z);
    CHECK_AST(" not (x)* -y<= +z",  not (x)* -y<= +z);
    CHECK_AST(" not (x* -y)<= +z",  not (x* -y)<= +z);
    CHECK_AST(" not x*( -y)<= +z",  not x*( -y)<= +z);
    CHECK_AST(" not x* -(y)<= +z",  not x* -(y)<= +z);
    CHECK_AST("( not x)* -y<= -z", ( not x)* -y<= -z);
    CHECK_AST("( not x* -y)<= -z", ( not x* -y)<= -z);
    CHECK_AST(" not (x)* -y<= -z",  not (x)* -y<= -z);
    CHECK_AST(" not (x* -y)<= -z",  not (x* -y)<= -z);
    CHECK_AST(" not x*( -y)<= -z",  not x*( -y)<= -z);
    CHECK_AST(" not x* -(y)<= -z",  not x* -(y)<= -z);
    CHECK_AST("( not x)* -y<= not z", ( not x)* -y<= not z);
    CHECK_AST("( not x* -y)<= not z", ( not x* -y)<= not z);
    CHECK_AST(" not (x)* -y<= not z",  not (x)* -y<= not z);
    CHECK_AST(" not (x* -y)<= not z",  not (x* -y)<= not z);
    CHECK_AST(" not x*( -y)<= not z",  not x*( -y)<= not z);
    CHECK_AST(" not x* -(y)<= not z",  not x* -(y)<= not z);
    CHECK_AST("( not x)* not y<=z", ( not x)* not y<=z);
    CHECK_AST("( not x* not y)<=z", ( not x* not y)<=z);
    CHECK_AST(" not (x)* not y<=z",  not (x)* not y<=z);
    CHECK_AST(" not (x* not y)<=z",  not (x* not y)<=z);
    CHECK_AST(" not x*( not y)<=z",  not x*( not y)<=z);
    CHECK_AST(" not x* not (y)<=z",  not x* not (y)<=z);
    CHECK_AST("( not x)* not y<= +z", ( not x)* not y<= +z);
    CHECK_AST("( not x* not y)<= +z", ( not x* not y)<= +z);
    CHECK_AST(" not (x)* not y<= +z",  not (x)* not y<= +z);
    CHECK_AST(" not (x* not y)<= +z",  not (x* not y)<= +z);
    CHECK_AST(" not x*( not y)<= +z",  not x*( not y)<= +z);
    CHECK_AST(" not x* not (y)<= +z",  not x* not (y)<= +z);
    CHECK_AST("( not x)* not y<= -z", ( not x)* not y<= -z);
    CHECK_AST("( not x* not y)<= -z", ( not x* not y)<= -z);
    CHECK_AST(" not (x)* not y<= -z",  not (x)* not y<= -z);
    CHECK_AST(" not (x* not y)<= -z",  not (x* not y)<= -z);
    CHECK_AST(" not x*( not y)<= -z",  not x*( not y)<= -z);
    CHECK_AST(" not x* not (y)<= -z",  not x* not (y)<= -z);
    CHECK_AST("( not x)* not y<= not z", ( not x)* not y<= not z);
    CHECK_AST("( not x* not y)<= not z", ( not x* not y)<= not z);
    CHECK_AST(" not (x)* not y<= not z",  not (x)* not y<= not z);
    CHECK_AST(" not (x* not y)<= not z",  not (x* not y)<= not z);
    CHECK_AST(" not x*( not y)<= not z",  not x*( not y)<= not z);
    CHECK_AST(" not x* not (y)<= not z",  not x* not (y)<= not z);
    CHECK_AST("(x)*y>z", (x)*y>z);
    CHECK_AST("(x*y)>z", (x*y)>z);
    CHECK_AST("x*(y)>z", x*(y)>z);
    CHECK_AST("(x)*y> +z", (x)*y> +z);
    CHECK_AST("(x*y)> +z", (x*y)> +z);
    CHECK_AST("x*(y)> +z", x*(y)> +z);
    CHECK_AST("(x)*y> -z", (x)*y> -z);
    CHECK_AST("(x*y)> -z", (x*y)> -z);
    CHECK_AST("x*(y)> -z", x*(y)> -z);
    CHECK_AST("(x)*y> not z", (x)*y> not z);
    CHECK_AST("(x*y)> not z", (x*y)> not z);
    CHECK_AST("x*(y)> not z", x*(y)> not z);
    CHECK_AST("(x)* +y>z", (x)* +y>z);
    CHECK_AST("(x* +y)>z", (x* +y)>z);
    CHECK_AST("x*( +y)>z", x*( +y)>z);
    CHECK_AST("x* +(y)>z", x* +(y)>z);
    CHECK_AST("(x)* +y> +z", (x)* +y> +z);
    CHECK_AST("(x* +y)> +z", (x* +y)> +z);
    CHECK_AST("x*( +y)> +z", x*( +y)> +z);
    CHECK_AST("x* +(y)> +z", x* +(y)> +z);
    CHECK_AST("(x)* +y> -z", (x)* +y> -z);
    CHECK_AST("(x* +y)> -z", (x* +y)> -z);
    CHECK_AST("x*( +y)> -z", x*( +y)> -z);
    CHECK_AST("x* +(y)> -z", x* +(y)> -z);
    CHECK_AST("(x)* +y> not z", (x)* +y> not z);
    CHECK_AST("(x* +y)> not z", (x* +y)> not z);
    CHECK_AST("x*( +y)> not z", x*( +y)> not z);
    CHECK_AST("x* +(y)> not z", x* +(y)> not z);
    CHECK_AST("(x)* -y>z", (x)* -y>z);
    CHECK_AST("(x* -y)>z", (x* -y)>z);
    CHECK_AST("x*( -y)>z", x*( -y)>z);
    CHECK_AST("x* -(y)>z", x* -(y)>z);
    CHECK_AST("(x)* -y> +z", (x)* -y> +z);
    CHECK_AST("(x* -y)> +z", (x* -y)> +z);
    CHECK_AST("x*( -y)> +z", x*( -y)> +z);
    CHECK_AST("x* -(y)> +z", x* -(y)> +z);
    CHECK_AST("(x)* -y> -z", (x)* -y> -z);
    CHECK_AST("(x* -y)> -z", (x* -y)> -z);
    CHECK_AST("x*( -y)> -z", x*( -y)> -z);
    CHECK_AST("x* -(y)> -z", x* -(y)> -z);
    CHECK_AST("(x)* -y> not z", (x)* -y> not z);
    CHECK_AST("(x* -y)> not z", (x* -y)> not z);
    CHECK_AST("x*( -y)> not z", x*( -y)> not z);
    CHECK_AST("x* -(y)> not z", x* -(y)> not z);
    CHECK_AST("(x)* not y>z", (x)* not y>z);
    CHECK_AST("(x* not y)>z", (x* not y)>z);
    CHECK_AST("x*( not y)>z", x*( not y)>z);
    CHECK_AST("x* not (y)>z", x* not (y)>z);
    CHECK_AST("(x)* not y> +z", (x)* not y> +z);
    CHECK_AST("(x* not y)> +z", (x* not y)> +z);
    CHECK_AST("x*( not y)> +z", x*( not y)> +z);
    CHECK_AST("x* not (y)> +z", x* not (y)> +z);
    CHECK_AST("(x)* not y> -z", (x)* not y> -z);
    CHECK_AST("(x* not y)> -z", (x* not y)> -z);
    CHECK_AST("x*( not y)> -z", x*( not y)> -z);
    CHECK_AST("x* not (y)> -z", x* not (y)> -z);
    CHECK_AST("(x)* not y> not z", (x)* not y> not z);
    CHECK_AST("(x* not y)> not z", (x* not y)> not z);
    CHECK_AST("x*( not y)> not z", x*( not y)> not z);
    CHECK_AST("x* not (y)> not z", x* not (y)> not z);
    CHECK_AST("( +x)*y>z", ( +x)*y>z);
    CHECK_AST("( +x*y)>z", ( +x*y)>z);
    CHECK_AST(" +(x)*y>z",  +(x)*y>z);
    CHECK_AST(" +(x*y)>z",  +(x*y)>z);
    CHECK_AST(" +x*(y)>z",  +x*(y)>z);
    CHECK_AST("( +x)*y> +z", ( +x)*y> +z);
    CHECK_AST("( +x*y)> +z", ( +x*y)> +z);
    CHECK_AST(" +(x)*y> +z",  +(x)*y> +z);
    CHECK_AST(" +(x*y)> +z",  +(x*y)> +z);
    CHECK_AST(" +x*(y)> +z",  +x*(y)> +z);
    CHECK_AST("( +x)*y> -z", ( +x)*y> -z);
    CHECK_AST("( +x*y)> -z", ( +x*y)> -z);
    CHECK_AST(" +(x)*y> -z",  +(x)*y> -z);
    CHECK_AST(" +(x*y)> -z",  +(x*y)> -z);
    CHECK_AST(" +x*(y)> -z",  +x*(y)> -z);
    CHECK_AST("( +x)*y> not z", ( +x)*y> not z);
    CHECK_AST("( +x*y)> not z", ( +x*y)> not z);
    CHECK_AST(" +(x)*y> not z",  +(x)*y> not z);
    CHECK_AST(" +(x*y)> not z",  +(x*y)> not z);
    CHECK_AST(" +x*(y)> not z",  +x*(y)> not z);
    CHECK_AST("( +x)* +y>z", ( +x)* +y>z);
    CHECK_AST("( +x* +y)>z", ( +x* +y)>z);
    CHECK_AST(" +(x)* +y>z",  +(x)* +y>z);
    CHECK_AST(" +(x* +y)>z",  +(x* +y)>z);
    CHECK_AST(" +x*( +y)>z",  +x*( +y)>z);
    CHECK_AST(" +x* +(y)>z",  +x* +(y)>z);
    CHECK_AST("( +x)* +y> +z", ( +x)* +y> +z);
    CHECK_AST("( +x* +y)> +z", ( +x* +y)> +z);
    CHECK_AST(" +(x)* +y> +z",  +(x)* +y> +z);
    CHECK_AST(" +(x* +y)> +z",  +(x* +y)> +z);
    CHECK_AST(" +x*( +y)> +z",  +x*( +y)> +z);
    CHECK_AST(" +x* +(y)> +z",  +x* +(y)> +z);
    CHECK_AST("( +x)* +y> -z", ( +x)* +y> -z);
    CHECK_AST("( +x* +y)> -z", ( +x* +y)> -z);
    CHECK_AST(" +(x)* +y> -z",  +(x)* +y> -z);
    CHECK_AST(" +(x* +y)> -z",  +(x* +y)> -z);
    CHECK_AST(" +x*( +y)> -z",  +x*( +y)> -z);
    CHECK_AST(" +x* +(y)> -z",  +x* +(y)> -z);
    CHECK_AST("( +x)* +y> not z", ( +x)* +y> not z);
    CHECK_AST("( +x* +y)> not z", ( +x* +y)> not z);
    CHECK_AST(" +(x)* +y> not z",  +(x)* +y> not z);
    CHECK_AST(" +(x* +y)> not z",  +(x* +y)> not z);
    CHECK_AST(" +x*( +y)> not z",  +x*( +y)> not z);
    CHECK_AST(" +x* +(y)> not z",  +x* +(y)> not z);
    CHECK_AST("( +x)* -y>z", ( +x)* -y>z);
    CHECK_AST("( +x* -y)>z", ( +x* -y)>z);
    CHECK_AST(" +(x)* -y>z",  +(x)* -y>z);
    CHECK_AST(" +(x* -y)>z",  +(x* -y)>z);
    CHECK_AST(" +x*( -y)>z",  +x*( -y)>z);
    CHECK_AST(" +x* -(y)>z",  +x* -(y)>z);
    CHECK_AST("( +x)* -y> +z", ( +x)* -y> +z);
    CHECK_AST("( +x* -y)> +z", ( +x* -y)> +z);
    CHECK_AST(" +(x)* -y> +z",  +(x)* -y> +z);
    CHECK_AST(" +(x* -y)> +z",  +(x* -y)> +z);
    CHECK_AST(" +x*( -y)> +z",  +x*( -y)> +z);
    CHECK_AST(" +x* -(y)> +z",  +x* -(y)> +z);
    CHECK_AST("( +x)* -y> -z", ( +x)* -y> -z);
    CHECK_AST("( +x* -y)> -z", ( +x* -y)> -z);
    CHECK_AST(" +(x)* -y> -z",  +(x)* -y> -z);
    CHECK_AST(" +(x* -y)> -z",  +(x* -y)> -z);
    CHECK_AST(" +x*( -y)> -z",  +x*( -y)> -z);
    CHECK_AST(" +x* -(y)> -z",  +x* -(y)> -z);
    CHECK_AST("( +x)* -y> not z", ( +x)* -y> not z);
    CHECK_AST("( +x* -y)> not z", ( +x* -y)> not z);
    CHECK_AST(" +(x)* -y> not z",  +(x)* -y> not z);
    CHECK_AST(" +(x* -y)> not z",  +(x* -y)> not z);
    CHECK_AST(" +x*( -y)> not z",  +x*( -y)> not z);
    CHECK_AST(" +x* -(y)> not z",  +x* -(y)> not z);
    CHECK_AST("( +x)* not y>z", ( +x)* not y>z);
    CHECK_AST("( +x* not y)>z", ( +x* not y)>z);
    CHECK_AST(" +(x)* not y>z",  +(x)* not y>z);
    CHECK_AST(" +(x* not y)>z",  +(x* not y)>z);
    CHECK_AST(" +x*( not y)>z",  +x*( not y)>z);
    CHECK_AST(" +x* not (y)>z",  +x* not (y)>z);
    CHECK_AST("( +x)* not y> +z", ( +x)* not y> +z);
    CHECK_AST("( +x* not y)> +z", ( +x* not y)> +z);
    CHECK_AST(" +(x)* not y> +z",  +(x)* not y> +z);
    CHECK_AST(" +(x* not y)> +z",  +(x* not y)> +z);
    CHECK_AST(" +x*( not y)> +z",  +x*( not y)> +z);
    CHECK_AST(" +x* not (y)> +z",  +x* not (y)> +z);
    CHECK_AST("( +x)* not y> -z", ( +x)* not y> -z);
    CHECK_AST("( +x* not y)> -z", ( +x* not y)> -z);
    CHECK_AST(" +(x)* not y> -z",  +(x)* not y> -z);
    CHECK_AST(" +(x* not y)> -z",  +(x* not y)> -z);
    CHECK_AST(" +x*( not y)> -z",  +x*( not y)> -z);
    CHECK_AST(" +x* not (y)> -z",  +x* not (y)> -z);
    CHECK_AST("( +x)* not y> not z", ( +x)* not y> not z);
    CHECK_AST("( +x* not y)> not z", ( +x* not y)> not z);
    CHECK_AST(" +(x)* not y> not z",  +(x)* not y> not z);
    CHECK_AST(" +(x* not y)> not z",  +(x* not y)> not z);
    CHECK_AST(" +x*( not y)> not z",  +x*( not y)> not z);
    CHECK_AST(" +x* not (y)> not z",  +x* not (y)> not z);
    CHECK_AST("( -x)*y>z", ( -x)*y>z);
    CHECK_AST("( -x*y)>z", ( -x*y)>z);
    CHECK_AST(" -(x)*y>z",  -(x)*y>z);
    CHECK_AST(" -(x*y)>z",  -(x*y)>z);
    CHECK_AST(" -x*(y)>z",  -x*(y)>z);
    CHECK_AST("( -x)*y> +z", ( -x)*y> +z);
    CHECK_AST("( -x*y)> +z", ( -x*y)> +z);
    CHECK_AST(" -(x)*y> +z",  -(x)*y> +z);
    CHECK_AST(" -(x*y)> +z",  -(x*y)> +z);
    CHECK_AST(" -x*(y)> +z",  -x*(y)> +z);
    CHECK_AST("( -x)*y> -z", ( -x)*y> -z);
    CHECK_AST("( -x*y)> -z", ( -x*y)> -z);
    CHECK_AST(" -(x)*y> -z",  -(x)*y> -z);
    CHECK_AST(" -(x*y)> -z",  -(x*y)> -z);
    CHECK_AST(" -x*(y)> -z",  -x*(y)> -z);
    CHECK_AST("( -x)*y> not z", ( -x)*y> not z);
    CHECK_AST("( -x*y)> not z", ( -x*y)> not z);
    CHECK_AST(" -(x)*y> not z",  -(x)*y> not z);
    CHECK_AST(" -(x*y)> not z",  -(x*y)> not z);
    CHECK_AST(" -x*(y)> not z",  -x*(y)> not z);
    CHECK_AST("( -x)* +y>z", ( -x)* +y>z);
    CHECK_AST("( -x* +y)>z", ( -x* +y)>z);
    CHECK_AST(" -(x)* +y>z",  -(x)* +y>z);
    CHECK_AST(" -(x* +y)>z",  -(x* +y)>z);
    CHECK_AST(" -x*( +y)>z",  -x*( +y)>z);
    CHECK_AST(" -x* +(y)>z",  -x* +(y)>z);
    CHECK_AST("( -x)* +y> +z", ( -x)* +y> +z);
    CHECK_AST("( -x* +y)> +z", ( -x* +y)> +z);
    CHECK_AST(" -(x)* +y> +z",  -(x)* +y> +z);
    CHECK_AST(" -(x* +y)> +z",  -(x* +y)> +z);
    CHECK_AST(" -x*( +y)> +z",  -x*( +y)> +z);
    CHECK_AST(" -x* +(y)> +z",  -x* +(y)> +z);
    CHECK_AST("( -x)* +y> -z", ( -x)* +y> -z);
    CHECK_AST("( -x* +y)> -z", ( -x* +y)> -z);
    CHECK_AST(" -(x)* +y> -z",  -(x)* +y> -z);
    CHECK_AST(" -(x* +y)> -z",  -(x* +y)> -z);
    CHECK_AST(" -x*( +y)> -z",  -x*( +y)> -z);
    CHECK_AST(" -x* +(y)> -z",  -x* +(y)> -z);
    CHECK_AST("( -x)* +y> not z", ( -x)* +y> not z);
    CHECK_AST("( -x* +y)> not z", ( -x* +y)> not z);
    CHECK_AST(" -(x)* +y> not z",  -(x)* +y> not z);
    CHECK_AST(" -(x* +y)> not z",  -(x* +y)> not z);
    CHECK_AST(" -x*( +y)> not z",  -x*( +y)> not z);
    CHECK_AST(" -x* +(y)> not z",  -x* +(y)> not z);
    CHECK_AST("( -x)* -y>z", ( -x)* -y>z);
    CHECK_AST("( -x* -y)>z", ( -x* -y)>z);
    CHECK_AST(" -(x)* -y>z",  -(x)* -y>z);
    CHECK_AST(" -(x* -y)>z",  -(x* -y)>z);
    CHECK_AST(" -x*( -y)>z",  -x*( -y)>z);
    CHECK_AST(" -x* -(y)>z",  -x* -(y)>z);
    CHECK_AST("( -x)* -y> +z", ( -x)* -y> +z);
    CHECK_AST("( -x* -y)> +z", ( -x* -y)> +z);
    CHECK_AST(" -(x)* -y> +z",  -(x)* -y> +z);
    CHECK_AST(" -(x* -y)> +z",  -(x* -y)> +z);
    CHECK_AST(" -x*( -y)> +z",  -x*( -y)> +z);
    CHECK_AST(" -x* -(y)> +z",  -x* -(y)> +z);
    CHECK_AST("( -x)* -y> -z", ( -x)* -y> -z);
    CHECK_AST("( -x* -y)> -z", ( -x* -y)> -z);
    CHECK_AST(" -(x)* -y> -z",  -(x)* -y> -z);
    CHECK_AST(" -(x* -y)> -z",  -(x* -y)> -z);
    CHECK_AST(" -x*( -y)> -z",  -x*( -y)> -z);
    CHECK_AST(" -x* -(y)> -z",  -x* -(y)> -z);
    CHECK_AST("( -x)* -y> not z", ( -x)* -y> not z);
    CHECK_AST("( -x* -y)> not z", ( -x* -y)> not z);
    CHECK_AST(" -(x)* -y> not z",  -(x)* -y> not z);
    CHECK_AST(" -(x* -y)> not z",  -(x* -y)> not z);
    CHECK_AST(" -x*( -y)> not z",  -x*( -y)> not z);
    CHECK_AST(" -x* -(y)> not z",  -x* -(y)> not z);
    CHECK_AST("( -x)* not y>z", ( -x)* not y>z);
    CHECK_AST("( -x* not y)>z", ( -x* not y)>z);
    CHECK_AST(" -(x)* not y>z",  -(x)* not y>z);
    CHECK_AST(" -(x* not y)>z",  -(x* not y)>z);
    CHECK_AST(" -x*( not y)>z",  -x*( not y)>z);
    CHECK_AST(" -x* not (y)>z",  -x* not (y)>z);
    CHECK_AST("( -x)* not y> +z", ( -x)* not y> +z);
    CHECK_AST("( -x* not y)> +z", ( -x* not y)> +z);
    CHECK_AST(" -(x)* not y> +z",  -(x)* not y> +z);
    CHECK_AST(" -(x* not y)> +z",  -(x* not y)> +z);
    CHECK_AST(" -x*( not y)> +z",  -x*( not y)> +z);
    CHECK_AST(" -x* not (y)> +z",  -x* not (y)> +z);
    CHECK_AST("( -x)* not y> -z", ( -x)* not y> -z);
    CHECK_AST("( -x* not y)> -z", ( -x* not y)> -z);
    CHECK_AST(" -(x)* not y> -z",  -(x)* not y> -z);
    CHECK_AST(" -(x* not y)> -z",  -(x* not y)> -z);
    CHECK_AST(" -x*( not y)> -z",  -x*( not y)> -z);
    CHECK_AST(" -x* not (y)> -z",  -x* not (y)> -z);
    CHECK_AST("( -x)* not y> not z", ( -x)* not y> not z);
    CHECK_AST("( -x* not y)> not z", ( -x* not y)> not z);
    CHECK_AST(" -(x)* not y> not z",  -(x)* not y> not z);
    CHECK_AST(" -(x* not y)> not z",  -(x* not y)> not z);
    CHECK_AST(" -x*( not y)> not z",  -x*( not y)> not z);
    CHECK_AST(" -x* not (y)> not z",  -x* not (y)> not z);
    CHECK_AST("( not x)*y>z", ( not x)*y>z);
    CHECK_AST("( not x*y)>z", ( not x*y)>z);
    CHECK_AST(" not (x)*y>z",  not (x)*y>z);
    CHECK_AST(" not (x*y)>z",  not (x*y)>z);
    CHECK_AST(" not x*(y)>z",  not x*(y)>z);
    CHECK_AST("( not x)*y> +z", ( not x)*y> +z);
    CHECK_AST("( not x*y)> +z", ( not x*y)> +z);
    CHECK_AST(" not (x)*y> +z",  not (x)*y> +z);
    CHECK_AST(" not (x*y)> +z",  not (x*y)> +z);
    CHECK_AST(" not x*(y)> +z",  not x*(y)> +z);
    CHECK_AST("( not x)*y> -z", ( not x)*y> -z);
    CHECK_AST("( not x*y)> -z", ( not x*y)> -z);
    CHECK_AST(" not (x)*y> -z",  not (x)*y> -z);
    CHECK_AST(" not (x*y)> -z",  not (x*y)> -z);
    CHECK_AST(" not x*(y)> -z",  not x*(y)> -z);
    CHECK_AST("( not x)*y> not z", ( not x)*y> not z);
    CHECK_AST("( not x*y)> not z", ( not x*y)> not z);
    CHECK_AST(" not (x)*y> not z",  not (x)*y> not z);
    CHECK_AST(" not (x*y)> not z",  not (x*y)> not z);
    CHECK_AST(" not x*(y)> not z",  not x*(y)> not z);
    CHECK_AST("( not x)* +y>z", ( not x)* +y>z);
    CHECK_AST("( not x* +y)>z", ( not x* +y)>z);
    CHECK_AST(" not (x)* +y>z",  not (x)* +y>z);
    CHECK_AST(" not (x* +y)>z",  not (x* +y)>z);
    CHECK_AST(" not x*( +y)>z",  not x*( +y)>z);
    CHECK_AST(" not x* +(y)>z",  not x* +(y)>z);
    CHECK_AST("( not x)* +y> +z", ( not x)* +y> +z);
    CHECK_AST("( not x* +y)> +z", ( not x* +y)> +z);
    CHECK_AST(" not (x)* +y> +z",  not (x)* +y> +z);
    CHECK_AST(" not (x* +y)> +z",  not (x* +y)> +z);
    CHECK_AST(" not x*( +y)> +z",  not x*( +y)> +z);
    CHECK_AST(" not x* +(y)> +z",  not x* +(y)> +z);
    CHECK_AST("( not x)* +y> -z", ( not x)* +y> -z);
    CHECK_AST("( not x* +y)> -z", ( not x* +y)> -z);
    CHECK_AST(" not (x)* +y> -z",  not (x)* +y> -z);
    CHECK_AST(" not (x* +y)> -z",  not (x* +y)> -z);
    CHECK_AST(" not x*( +y)> -z",  not x*( +y)> -z);
    CHECK_AST(" not x* +(y)> -z",  not x* +(y)> -z);
    CHECK_AST("( not x)* +y> not z", ( not x)* +y> not z);
    CHECK_AST("( not x* +y)> not z", ( not x* +y)> not z);
    CHECK_AST(" not (x)* +y> not z",  not (x)* +y> not z);
    CHECK_AST(" not (x* +y)> not z",  not (x* +y)> not z);
    CHECK_AST(" not x*( +y)> not z",  not x*( +y)> not z);
    CHECK_AST(" not x* +(y)> not z",  not x* +(y)> not z);
    CHECK_AST("( not x)* -y>z", ( not x)* -y>z);
    CHECK_AST("( not x* -y)>z", ( not x* -y)>z);
    CHECK_AST(" not (x)* -y>z",  not (x)* -y>z);
    CHECK_AST(" not (x* -y)>z",  not (x* -y)>z);
    CHECK_AST(" not x*( -y)>z",  not x*( -y)>z);
    CHECK_AST(" not x* -(y)>z",  not x* -(y)>z);
    CHECK_AST("( not x)* -y> +z", ( not x)* -y> +z);
    CHECK_AST("( not x* -y)> +z", ( not x* -y)> +z);
    CHECK_AST(" not (x)* -y> +z",  not (x)* -y> +z);
    CHECK_AST(" not (x* -y)> +z",  not (x* -y)> +z);
    CHECK_AST(" not x*( -y)> +z",  not x*( -y)> +z);
    CHECK_AST(" not x* -(y)> +z",  not x* -(y)> +z);
    CHECK_AST("( not x)* -y> -z", ( not x)* -y> -z);
    CHECK_AST("( not x* -y)> -z", ( not x* -y)> -z);
    CHECK_AST(" not (x)* -y> -z",  not (x)* -y> -z);
    CHECK_AST(" not (x* -y)> -z",  not (x* -y)> -z);
    CHECK_AST(" not x*( -y)> -z",  not x*( -y)> -z);
    CHECK_AST(" not x* -(y)> -z",  not x* -(y)> -z);
    CHECK_AST("( not x)* -y> not z", ( not x)* -y> not z);
    CHECK_AST("( not x* -y)> not z", ( not x* -y)> not z);
    CHECK_AST(" not (x)* -y> not z",  not (x)* -y> not z);
    CHECK_AST(" not (x* -y)> not z",  not (x* -y)> not z);
    CHECK_AST(" not x*( -y)> not z",  not x*( -y)> not z);
    CHECK_AST(" not x* -(y)> not z",  not x* -(y)> not z);
    CHECK_AST("( not x)* not y>z", ( not x)* not y>z);
    CHECK_AST("( not x* not y)>z", ( not x* not y)>z);
    CHECK_AST(" not (x)* not y>z",  not (x)* not y>z);
    CHECK_AST(" not (x* not y)>z",  not (x* not y)>z);
    CHECK_AST(" not x*( not y)>z",  not x*( not y)>z);
    CHECK_AST(" not x* not (y)>z",  not x* not (y)>z);
    CHECK_AST("( not x)* not y> +z", ( not x)* not y> +z);
    CHECK_AST("( not x* not y)> +z", ( not x* not y)> +z);
    CHECK_AST(" not (x)* not y> +z",  not (x)* not y> +z);
    CHECK_AST(" not (x* not y)> +z",  not (x* not y)> +z);
    CHECK_AST(" not x*( not y)> +z",  not x*( not y)> +z);
    CHECK_AST(" not x* not (y)> +z",  not x* not (y)> +z);
    CHECK_AST("( not x)* not y> -z", ( not x)* not y> -z);
    CHECK_AST("( not x* not y)> -z", ( not x* not y)> -z);
    CHECK_AST(" not (x)* not y> -z",  not (x)* not y> -z);
    CHECK_AST(" not (x* not y)> -z",  not (x* not y)> -z);
    CHECK_AST(" not x*( not y)> -z",  not x*( not y)> -z);
    CHECK_AST(" not x* not (y)> -z",  not x* not (y)> -z);
    CHECK_AST("( not x)* not y> not z", ( not x)* not y> not z);
    CHECK_AST("( not x* not y)> not z", ( not x* not y)> not z);
    CHECK_AST(" not (x)* not y> not z",  not (x)* not y> not z);
    CHECK_AST(" not (x* not y)> not z",  not (x* not y)> not z);
    CHECK_AST(" not x*( not y)> not z",  not x*( not y)> not z);
    CHECK_AST(" not x* not (y)> not z",  not x* not (y)> not z);
    CHECK_AST("(x)*y>=z", (x)*y>=z);
    CHECK_AST("(x*y)>=z", (x*y)>=z);
    CHECK_AST("x*(y)>=z", x*(y)>=z);
    CHECK_AST("(x)*y>= +z", (x)*y>= +z);
    CHECK_AST("(x*y)>= +z", (x*y)>= +z);
    CHECK_AST("x*(y)>= +z", x*(y)>= +z);
    CHECK_AST("(x)*y>= -z", (x)*y>= -z);
    CHECK_AST("(x*y)>= -z", (x*y)>= -z);
    CHECK_AST("x*(y)>= -z", x*(y)>= -z);
    CHECK_AST("(x)*y>= not z", (x)*y>= not z);
    CHECK_AST("(x*y)>= not z", (x*y)>= not z);
    CHECK_AST("x*(y)>= not z", x*(y)>= not z);
    CHECK_AST("(x)* +y>=z", (x)* +y>=z);
    CHECK_AST("(x* +y)>=z", (x* +y)>=z);
    CHECK_AST("x*( +y)>=z", x*( +y)>=z);
    CHECK_AST("x* +(y)>=z", x* +(y)>=z);
    CHECK_AST("(x)* +y>= +z", (x)* +y>= +z);
    CHECK_AST("(x* +y)>= +z", (x* +y)>= +z);
    CHECK_AST("x*( +y)>= +z", x*( +y)>= +z);
    CHECK_AST("x* +(y)>= +z", x* +(y)>= +z);
    CHECK_AST("(x)* +y>= -z", (x)* +y>= -z);
    CHECK_AST("(x* +y)>= -z", (x* +y)>= -z);
    CHECK_AST("x*( +y)>= -z", x*( +y)>= -z);
    CHECK_AST("x* +(y)>= -z", x* +(y)>= -z);
    CHECK_AST("(x)* +y>= not z", (x)* +y>= not z);
    CHECK_AST("(x* +y)>= not z", (x* +y)>= not z);
    CHECK_AST("x*( +y)>= not z", x*( +y)>= not z);
    CHECK_AST("x* +(y)>= not z", x* +(y)>= not z);
    CHECK_AST("(x)* -y>=z", (x)* -y>=z);
    CHECK_AST("(x* -y)>=z", (x* -y)>=z);
    CHECK_AST("x*( -y)>=z", x*( -y)>=z);
    CHECK_AST("x* -(y)>=z", x* -(y)>=z);
    CHECK_AST("(x)* -y>= +z", (x)* -y>= +z);
    CHECK_AST("(x* -y)>= +z", (x* -y)>= +z);
    CHECK_AST("x*( -y)>= +z", x*( -y)>= +z);
    CHECK_AST("x* -(y)>= +z", x* -(y)>= +z);
    CHECK_AST("(x)* -y>= -z", (x)* -y>= -z);
    CHECK_AST("(x* -y)>= -z", (x* -y)>= -z);
    CHECK_AST("x*( -y)>= -z", x*( -y)>= -z);
    CHECK_AST("x* -(y)>= -z", x* -(y)>= -z);
    CHECK_AST("(x)* -y>= not z", (x)* -y>= not z);
    CHECK_AST("(x* -y)>= not z", (x* -y)>= not z);
    CHECK_AST("x*( -y)>= not z", x*( -y)>= not z);
    CHECK_AST("x* -(y)>= not z", x* -(y)>= not z);
    CHECK_AST("(x)* not y>=z", (x)* not y>=z);
    CHECK_AST("(x* not y)>=z", (x* not y)>=z);
    CHECK_AST("x*( not y)>=z", x*( not y)>=z);
    CHECK_AST("x* not (y)>=z", x* not (y)>=z);
    CHECK_AST("(x)* not y>= +z", (x)* not y>= +z);
    CHECK_AST("(x* not y)>= +z", (x* not y)>= +z);
    CHECK_AST("x*( not y)>= +z", x*( not y)>= +z);
    CHECK_AST("x* not (y)>= +z", x* not (y)>= +z);
    CHECK_AST("(x)* not y>= -z", (x)* not y>= -z);
    CHECK_AST("(x* not y)>= -z", (x* not y)>= -z);
    CHECK_AST("x*( not y)>= -z", x*( not y)>= -z);
    CHECK_AST("x* not (y)>= -z", x* not (y)>= -z);
    CHECK_AST("(x)* not y>= not z", (x)* not y>= not z);
    CHECK_AST("(x* not y)>= not z", (x* not y)>= not z);
    CHECK_AST("x*( not y)>= not z", x*( not y)>= not z);
    CHECK_AST("x* not (y)>= not z", x* not (y)>= not z);
    CHECK_AST("( +x)*y>=z", ( +x)*y>=z);
    CHECK_AST("( +x*y)>=z", ( +x*y)>=z);
    CHECK_AST(" +(x)*y>=z",  +(x)*y>=z);
    CHECK_AST(" +(x*y)>=z",  +(x*y)>=z);
    CHECK_AST(" +x*(y)>=z",  +x*(y)>=z);
    CHECK_AST("( +x)*y>= +z", ( +x)*y>= +z);
    CHECK_AST("( +x*y)>= +z", ( +x*y)>= +z);
    CHECK_AST(" +(x)*y>= +z",  +(x)*y>= +z);
    CHECK_AST(" +(x*y)>= +z",  +(x*y)>= +z);
    CHECK_AST(" +x*(y)>= +z",  +x*(y)>= +z);
    CHECK_AST("( +x)*y>= -z", ( +x)*y>= -z);
    CHECK_AST("( +x*y)>= -z", ( +x*y)>= -z);
    CHECK_AST(" +(x)*y>= -z",  +(x)*y>= -z);
    CHECK_AST(" +(x*y)>= -z",  +(x*y)>= -z);
    CHECK_AST(" +x*(y)>= -z",  +x*(y)>= -z);
    CHECK_AST("( +x)*y>= not z", ( +x)*y>= not z);
    CHECK_AST("( +x*y)>= not z", ( +x*y)>= not z);
    CHECK_AST(" +(x)*y>= not z",  +(x)*y>= not z);
    CHECK_AST(" +(x*y)>= not z",  +(x*y)>= not z);
    CHECK_AST(" +x*(y)>= not z",  +x*(y)>= not z);
    CHECK_AST("( +x)* +y>=z", ( +x)* +y>=z);
    CHECK_AST("( +x* +y)>=z", ( +x* +y)>=z);
    CHECK_AST(" +(x)* +y>=z",  +(x)* +y>=z);
    CHECK_AST(" +(x* +y)>=z",  +(x* +y)>=z);
    CHECK_AST(" +x*( +y)>=z",  +x*( +y)>=z);
    CHECK_AST(" +x* +(y)>=z",  +x* +(y)>=z);
    CHECK_AST("( +x)* +y>= +z", ( +x)* +y>= +z);
    CHECK_AST("( +x* +y)>= +z", ( +x* +y)>= +z);
    CHECK_AST(" +(x)* +y>= +z",  +(x)* +y>= +z);
    CHECK_AST(" +(x* +y)>= +z",  +(x* +y)>= +z);
    CHECK_AST(" +x*( +y)>= +z",  +x*( +y)>= +z);
    CHECK_AST(" +x* +(y)>= +z",  +x* +(y)>= +z);
    CHECK_AST("( +x)* +y>= -z", ( +x)* +y>= -z);
    CHECK_AST("( +x* +y)>= -z", ( +x* +y)>= -z);
    CHECK_AST(" +(x)* +y>= -z",  +(x)* +y>= -z);
    CHECK_AST(" +(x* +y)>= -z",  +(x* +y)>= -z);
    CHECK_AST(" +x*( +y)>= -z",  +x*( +y)>= -z);
    CHECK_AST(" +x* +(y)>= -z",  +x* +(y)>= -z);
    CHECK_AST("( +x)* +y>= not z", ( +x)* +y>= not z);
    CHECK_AST("( +x* +y)>= not z", ( +x* +y)>= not z);
    CHECK_AST(" +(x)* +y>= not z",  +(x)* +y>= not z);
    CHECK_AST(" +(x* +y)>= not z",  +(x* +y)>= not z);
    CHECK_AST(" +x*( +y)>= not z",  +x*( +y)>= not z);
    CHECK_AST(" +x* +(y)>= not z",  +x* +(y)>= not z);
    CHECK_AST("( +x)* -y>=z", ( +x)* -y>=z);
    CHECK_AST("( +x* -y)>=z", ( +x* -y)>=z);
    CHECK_AST(" +(x)* -y>=z",  +(x)* -y>=z);
    CHECK_AST(" +(x* -y)>=z",  +(x* -y)>=z);
    CHECK_AST(" +x*( -y)>=z",  +x*( -y)>=z);
    CHECK_AST(" +x* -(y)>=z",  +x* -(y)>=z);
    CHECK_AST("( +x)* -y>= +z", ( +x)* -y>= +z);
    CHECK_AST("( +x* -y)>= +z", ( +x* -y)>= +z);
    CHECK_AST(" +(x)* -y>= +z",  +(x)* -y>= +z);
    CHECK_AST(" +(x* -y)>= +z",  +(x* -y)>= +z);
    CHECK_AST(" +x*( -y)>= +z",  +x*( -y)>= +z);
    CHECK_AST(" +x* -(y)>= +z",  +x* -(y)>= +z);
    CHECK_AST("( +x)* -y>= -z", ( +x)* -y>= -z);
    CHECK_AST("( +x* -y)>= -z", ( +x* -y)>= -z);
    CHECK_AST(" +(x)* -y>= -z",  +(x)* -y>= -z);
    CHECK_AST(" +(x* -y)>= -z",  +(x* -y)>= -z);
    CHECK_AST(" +x*( -y)>= -z",  +x*( -y)>= -z);
    CHECK_AST(" +x* -(y)>= -z",  +x* -(y)>= -z);
    CHECK_AST("( +x)* -y>= not z", ( +x)* -y>= not z);
    CHECK_AST("( +x* -y)>= not z", ( +x* -y)>= not z);
    CHECK_AST(" +(x)* -y>= not z",  +(x)* -y>= not z);
    CHECK_AST(" +(x* -y)>= not z",  +(x* -y)>= not z);
    CHECK_AST(" +x*( -y)>= not z",  +x*( -y)>= not z);
    CHECK_AST(" +x* -(y)>= not z",  +x* -(y)>= not z);
    CHECK_AST("( +x)* not y>=z", ( +x)* not y>=z);
    CHECK_AST("( +x* not y)>=z", ( +x* not y)>=z);
    CHECK_AST(" +(x)* not y>=z",  +(x)* not y>=z);
    CHECK_AST(" +(x* not y)>=z",  +(x* not y)>=z);
    CHECK_AST(" +x*( not y)>=z",  +x*( not y)>=z);
    CHECK_AST(" +x* not (y)>=z",  +x* not (y)>=z);
    CHECK_AST("( +x)* not y>= +z", ( +x)* not y>= +z);
    CHECK_AST("( +x* not y)>= +z", ( +x* not y)>= +z);
    CHECK_AST(" +(x)* not y>= +z",  +(x)* not y>= +z);
    CHECK_AST(" +(x* not y)>= +z",  +(x* not y)>= +z);
    CHECK_AST(" +x*( not y)>= +z",  +x*( not y)>= +z);
    CHECK_AST(" +x* not (y)>= +z",  +x* not (y)>= +z);
    CHECK_AST("( +x)* not y>= -z", ( +x)* not y>= -z);
    CHECK_AST("( +x* not y)>= -z", ( +x* not y)>= -z);
    CHECK_AST(" +(x)* not y>= -z",  +(x)* not y>= -z);
    CHECK_AST(" +(x* not y)>= -z",  +(x* not y)>= -z);
    CHECK_AST(" +x*( not y)>= -z",  +x*( not y)>= -z);
    CHECK_AST(" +x* not (y)>= -z",  +x* not (y)>= -z);
    CHECK_AST("( +x)* not y>= not z", ( +x)* not y>= not z);
    CHECK_AST("( +x* not y)>= not z", ( +x* not y)>= not z);
    CHECK_AST(" +(x)* not y>= not z",  +(x)* not y>= not z);
    CHECK_AST(" +(x* not y)>= not z",  +(x* not y)>= not z);
    CHECK_AST(" +x*( not y)>= not z",  +x*( not y)>= not z);
    CHECK_AST(" +x* not (y)>= not z",  +x* not (y)>= not z);
    CHECK_AST("( -x)*y>=z", ( -x)*y>=z);
    CHECK_AST("( -x*y)>=z", ( -x*y)>=z);
    CHECK_AST(" -(x)*y>=z",  -(x)*y>=z);
    CHECK_AST(" -(x*y)>=z",  -(x*y)>=z);
    CHECK_AST(" -x*(y)>=z",  -x*(y)>=z);
    CHECK_AST("( -x)*y>= +z", ( -x)*y>= +z);
    CHECK_AST("( -x*y)>= +z", ( -x*y)>= +z);
    CHECK_AST(" -(x)*y>= +z",  -(x)*y>= +z);
    CHECK_AST(" -(x*y)>= +z",  -(x*y)>= +z);
    CHECK_AST(" -x*(y)>= +z",  -x*(y)>= +z);
    CHECK_AST("( -x)*y>= -z", ( -x)*y>= -z);
    CHECK_AST("( -x*y)>= -z", ( -x*y)>= -z);
    CHECK_AST(" -(x)*y>= -z",  -(x)*y>= -z);
    CHECK_AST(" -(x*y)>= -z",  -(x*y)>= -z);
    CHECK_AST(" -x*(y)>= -z",  -x*(y)>= -z);
    CHECK_AST("( -x)*y>= not z", ( -x)*y>= not z);
    CHECK_AST("( -x*y)>= not z", ( -x*y)>= not z);
    CHECK_AST(" -(x)*y>= not z",  -(x)*y>= not z);
    CHECK_AST(" -(x*y)>= not z",  -(x*y)>= not z);
    CHECK_AST(" -x*(y)>= not z",  -x*(y)>= not z);
    CHECK_AST("( -x)* +y>=z", ( -x)* +y>=z);
    CHECK_AST("( -x* +y)>=z", ( -x* +y)>=z);
    CHECK_AST(" -(x)* +y>=z",  -(x)* +y>=z);
    CHECK_AST(" -(x* +y)>=z",  -(x* +y)>=z);
    CHECK_AST(" -x*( +y)>=z",  -x*( +y)>=z);
    CHECK_AST(" -x* +(y)>=z",  -x* +(y)>=z);
    CHECK_AST("( -x)* +y>= +z", ( -x)* +y>= +z);
    CHECK_AST("( -x* +y)>= +z", ( -x* +y)>= +z);
    CHECK_AST(" -(x)* +y>= +z",  -(x)* +y>= +z);
    CHECK_AST(" -(x* +y)>= +z",  -(x* +y)>= +z);
    CHECK_AST(" -x*( +y)>= +z",  -x*( +y)>= +z);
    CHECK_AST(" -x* +(y)>= +z",  -x* +(y)>= +z);
    CHECK_AST("( -x)* +y>= -z", ( -x)* +y>= -z);
    CHECK_AST("( -x* +y)>= -z", ( -x* +y)>= -z);
    CHECK_AST(" -(x)* +y>= -z",  -(x)* +y>= -z);
    CHECK_AST(" -(x* +y)>= -z",  -(x* +y)>= -z);
    CHECK_AST(" -x*( +y)>= -z",  -x*( +y)>= -z);
    CHECK_AST(" -x* +(y)>= -z",  -x* +(y)>= -z);
    CHECK_AST("( -x)* +y>= not z", ( -x)* +y>= not z);
    CHECK_AST("( -x* +y)>= not z", ( -x* +y)>= not z);
    CHECK_AST(" -(x)* +y>= not z",  -(x)* +y>= not z);
    CHECK_AST(" -(x* +y)>= not z",  -(x* +y)>= not z);
    CHECK_AST(" -x*( +y)>= not z",  -x*( +y)>= not z);
    CHECK_AST(" -x* +(y)>= not z",  -x* +(y)>= not z);
    CHECK_AST("( -x)* -y>=z", ( -x)* -y>=z);
    CHECK_AST("( -x* -y)>=z", ( -x* -y)>=z);
    CHECK_AST(" -(x)* -y>=z",  -(x)* -y>=z);
    CHECK_AST(" -(x* -y)>=z",  -(x* -y)>=z);
    CHECK_AST(" -x*( -y)>=z",  -x*( -y)>=z);
    CHECK_AST(" -x* -(y)>=z",  -x* -(y)>=z);
    CHECK_AST("( -x)* -y>= +z", ( -x)* -y>= +z);
    CHECK_AST("( -x* -y)>= +z", ( -x* -y)>= +z);
    CHECK_AST(" -(x)* -y>= +z",  -(x)* -y>= +z);
    CHECK_AST(" -(x* -y)>= +z",  -(x* -y)>= +z);
    CHECK_AST(" -x*( -y)>= +z",  -x*( -y)>= +z);
    CHECK_AST(" -x* -(y)>= +z",  -x* -(y)>= +z);
    CHECK_AST("( -x)* -y>= -z", ( -x)* -y>= -z);
    CHECK_AST("( -x* -y)>= -z", ( -x* -y)>= -z);
    CHECK_AST(" -(x)* -y>= -z",  -(x)* -y>= -z);
    CHECK_AST(" -(x* -y)>= -z",  -(x* -y)>= -z);
    CHECK_AST(" -x*( -y)>= -z",  -x*( -y)>= -z);
    CHECK_AST(" -x* -(y)>= -z",  -x* -(y)>= -z);
    CHECK_AST("( -x)* -y>= not z", ( -x)* -y>= not z);
    CHECK_AST("( -x* -y)>= not z", ( -x* -y)>= not z);
    CHECK_AST(" -(x)* -y>= not z",  -(x)* -y>= not z);
    CHECK_AST(" -(x* -y)>= not z",  -(x* -y)>= not z);
    CHECK_AST(" -x*( -y)>= not z",  -x*( -y)>= not z);
    CHECK_AST(" -x* -(y)>= not z",  -x* -(y)>= not z);
    CHECK_AST("( -x)* not y>=z", ( -x)* not y>=z);
    CHECK_AST("( -x* not y)>=z", ( -x* not y)>=z);
    CHECK_AST(" -(x)* not y>=z",  -(x)* not y>=z);
    CHECK_AST(" -(x* not y)>=z",  -(x* not y)>=z);
    CHECK_AST(" -x*( not y)>=z",  -x*( not y)>=z);
    CHECK_AST(" -x* not (y)>=z",  -x* not (y)>=z);
    CHECK_AST("( -x)* not y>= +z", ( -x)* not y>= +z);
    CHECK_AST("( -x* not y)>= +z", ( -x* not y)>= +z);
    CHECK_AST(" -(x)* not y>= +z",  -(x)* not y>= +z);
    CHECK_AST(" -(x* not y)>= +z",  -(x* not y)>= +z);
    CHECK_AST(" -x*( not y)>= +z",  -x*( not y)>= +z);
    CHECK_AST(" -x* not (y)>= +z",  -x* not (y)>= +z);
    CHECK_AST("( -x)* not y>= -z", ( -x)* not y>= -z);
    CHECK_AST("( -x* not y)>= -z", ( -x* not y)>= -z);
    CHECK_AST(" -(x)* not y>= -z",  -(x)* not y>= -z);
    CHECK_AST(" -(x* not y)>= -z",  -(x* not y)>= -z);
    CHECK_AST(" -x*( not y)>= -z",  -x*( not y)>= -z);
    CHECK_AST(" -x* not (y)>= -z",  -x* not (y)>= -z);
    CHECK_AST("( -x)* not y>= not z", ( -x)* not y>= not z);
    CHECK_AST("( -x* not y)>= not z", ( -x* not y)>= not z);
    CHECK_AST(" -(x)* not y>= not z",  -(x)* not y>= not z);
    CHECK_AST(" -(x* not y)>= not z",  -(x* not y)>= not z);
    CHECK_AST(" -x*( not y)>= not z",  -x*( not y)>= not z);
    CHECK_AST(" -x* not (y)>= not z",  -x* not (y)>= not z);
    CHECK_AST("( not x)*y>=z", ( not x)*y>=z);
    CHECK_AST("( not x*y)>=z", ( not x*y)>=z);
    CHECK_AST(" not (x)*y>=z",  not (x)*y>=z);
    CHECK_AST(" not (x*y)>=z",  not (x*y)>=z);
    CHECK_AST(" not x*(y)>=z",  not x*(y)>=z);
    CHECK_AST("( not x)*y>= +z", ( not x)*y>= +z);
    CHECK_AST("( not x*y)>= +z", ( not x*y)>= +z);
    CHECK_AST(" not (x)*y>= +z",  not (x)*y>= +z);
    CHECK_AST(" not (x*y)>= +z",  not (x*y)>= +z);
    CHECK_AST(" not x*(y)>= +z",  not x*(y)>= +z);
    CHECK_AST("( not x)*y>= -z", ( not x)*y>= -z);
    CHECK_AST("( not x*y)>= -z", ( not x*y)>= -z);
    CHECK_AST(" not (x)*y>= -z",  not (x)*y>= -z);
    CHECK_AST(" not (x*y)>= -z",  not (x*y)>= -z);
    CHECK_AST(" not x*(y)>= -z",  not x*(y)>= -z);
    CHECK_AST("( not x)*y>= not z", ( not x)*y>= not z);
    CHECK_AST("( not x*y)>= not z", ( not x*y)>= not z);
    CHECK_AST(" not (x)*y>= not z",  not (x)*y>= not z);
    CHECK_AST(" not (x*y)>= not z",  not (x*y)>= not z);
    CHECK_AST(" not x*(y)>= not z",  not x*(y)>= not z);
    CHECK_AST("( not x)* +y>=z", ( not x)* +y>=z);
    CHECK_AST("( not x* +y)>=z", ( not x* +y)>=z);
    CHECK_AST(" not (x)* +y>=z",  not (x)* +y>=z);
    CHECK_AST(" not (x* +y)>=z",  not (x* +y)>=z);
    CHECK_AST(" not x*( +y)>=z",  not x*( +y)>=z);
    CHECK_AST(" not x* +(y)>=z",  not x* +(y)>=z);
    CHECK_AST("( not x)* +y>= +z", ( not x)* +y>= +z);
    CHECK_AST("( not x* +y)>= +z", ( not x* +y)>= +z);
    CHECK_AST(" not (x)* +y>= +z",  not (x)* +y>= +z);
    CHECK_AST(" not (x* +y)>= +z",  not (x* +y)>= +z);
    CHECK_AST(" not x*( +y)>= +z",  not x*( +y)>= +z);
    CHECK_AST(" not x* +(y)>= +z",  not x* +(y)>= +z);
    CHECK_AST("( not x)* +y>= -z", ( not x)* +y>= -z);
    CHECK_AST("( not x* +y)>= -z", ( not x* +y)>= -z);
    CHECK_AST(" not (x)* +y>= -z",  not (x)* +y>= -z);
    CHECK_AST(" not (x* +y)>= -z",  not (x* +y)>= -z);
    CHECK_AST(" not x*( +y)>= -z",  not x*( +y)>= -z);
    CHECK_AST(" not x* +(y)>= -z",  not x* +(y)>= -z);
    CHECK_AST("( not x)* +y>= not z", ( not x)* +y>= not z);
    CHECK_AST("( not x* +y)>= not z", ( not x* +y)>= not z);
    CHECK_AST(" not (x)* +y>= not z",  not (x)* +y>= not z);
    CHECK_AST(" not (x* +y)>= not z",  not (x* +y)>= not z);
    CHECK_AST(" not x*( +y)>= not z",  not x*( +y)>= not z);
    CHECK_AST(" not x* +(y)>= not z",  not x* +(y)>= not z);
    CHECK_AST("( not x)* -y>=z", ( not x)* -y>=z);
    CHECK_AST("( not x* -y)>=z", ( not x* -y)>=z);
    CHECK_AST(" not (x)* -y>=z",  not (x)* -y>=z);
    CHECK_AST(" not (x* -y)>=z",  not (x* -y)>=z);
    CHECK_AST(" not x*( -y)>=z",  not x*( -y)>=z);
    CHECK_AST(" not x* -(y)>=z",  not x* -(y)>=z);
    CHECK_AST("( not x)* -y>= +z", ( not x)* -y>= +z);
    CHECK_AST("( not x* -y)>= +z", ( not x* -y)>= +z);
    CHECK_AST(" not (x)* -y>= +z",  not (x)* -y>= +z);
    CHECK_AST(" not (x* -y)>= +z",  not (x* -y)>= +z);
    CHECK_AST(" not x*( -y)>= +z",  not x*( -y)>= +z);
    CHECK_AST(" not x* -(y)>= +z",  not x* -(y)>= +z);
    CHECK_AST("( not x)* -y>= -z", ( not x)* -y>= -z);
    CHECK_AST("( not x* -y)>= -z", ( not x* -y)>= -z);
    CHECK_AST(" not (x)* -y>= -z",  not (x)* -y>= -z);
    CHECK_AST(" not (x* -y)>= -z",  not (x* -y)>= -z);
    CHECK_AST(" not x*( -y)>= -z",  not x*( -y)>= -z);
    CHECK_AST(" not x* -(y)>= -z",  not x* -(y)>= -z);
    CHECK_AST("( not x)* -y>= not z", ( not x)* -y>= not z);
    CHECK_AST("( not x* -y)>= not z", ( not x* -y)>= not z);
    CHECK_AST(" not (x)* -y>= not z",  not (x)* -y>= not z);
    CHECK_AST(" not (x* -y)>= not z",  not (x* -y)>= not z);
    CHECK_AST(" not x*( -y)>= not z",  not x*( -y)>= not z);
    CHECK_AST(" not x* -(y)>= not z",  not x* -(y)>= not z);

    auto total = good + bad;
    std::cout
        << "check_ast_ac: " << good << " out of " << total
        << " (" << std::setprecision(1) << std::fixed << (100.0*good/total) << "%)\n";
}