let R_trs_default_variable = variables "y,x" ;

let R_trs_default_signature =
 signature "0 : 0;
    _0 : 0;
    false : 0;
    _false : 0;
    minus : 2;
    _minus : 2;
    pred : 1;
    _pred : 1;
    true : 0;
    _true : 0;
    s : 1;
    _s : 1;
    gcd : 2;
    _gcd : 2;
    le : 2;
    _le : 2;
    if_95_gcd : 3;
    _if_95_gcd : 3" ;

let R_trs_default_algebra = algebra R_trs_default_signature ;

#Set_sat_solver "minisat2";
let b = (((ordering_solve (order_constraints R_trs_default_algebra "    _if_95_gcd(false, x, y) >= _gcd(minus(y, x), x)/\   _gcd(s(x), s(y)) >= _if_95_gcd(le(y, x), s(x), s(y))/\  le(0, y) >= true/\  le(s(x), 0) >= false/\  le(s(x), s(y)) >= le(x, y)/\    minus(x, 0) >= x/\  minus(x, s(y)) >= pred(minus(x, y))/\   pred(s(x)) >= x/\_if_95_gcd(true, x, y) > _gcd(minus(x, y), y)")) and
 (((ordering_solve (order_constraints R_trs_default_algebra "   _gcd(s(x), s(y)) >= _if_95_gcd(le(y, x), s(x), s(y))/\  le(0, y) >= true/\  le(s(x), 0) >= false/\  le(s(x), s(y)) >= le(x, y)/\    minus(x, 0) >= x/\  minus(x, s(y)) >= pred(minus(x, y))/\   pred(s(x)) >= x/\_if_95_gcd(false, x, y) > _gcd(minus(y, x), x)"))) or

 ((ordering_solve (order_constraints R_trs_default_algebra "    _if_95_gcd(false, x, y) >= _gcd(minus(y, x), x)/\   le(0, y) >= true/\  le(s(x), 0) >= false/\  le(s(x), s(y)) >= le(x, y)/\    minus(x, 0) >= x/\  minus(x, s(y)) >= pred(minus(x, y))/\   pred(s(x)) >= x/\_gcd(s(x), s(y)) > _if_95_gcd(le(y, x), s(x), s(y))"))))) or

 ((ordering_solve (order_constraints R_trs_default_algebra "    _if_95_gcd(true, x, y) >= _gcd(minus(x, y), y)/\    _gcd(s(x), s(y)) >= _if_95_gcd(le(y, x), s(x), s(y))/\  le(0, y) >= true/\  le(s(x), 0) >= false/\  le(s(x), s(y)) >= le(x, y)/\    minus(x, 0) >= x/\  minus(x, s(y)) >= pred(minus(x, y))/\   pred(s(x)) >= x/\_if_95_gcd(false, x, y) > _gcd(minus(y, x), x)")) and
 (((ordering_solve (order_constraints R_trs_default_algebra "   _gcd(s(x), s(y)) >= _if_95_gcd(le(y, x), s(x), s(y))/\  le(0, y) >= true/\  le(s(x), 0) >= false/\  le(s(x), s(y)) >= le(x, y)/\    minus(x, 0) >= x/\  minus(x, s(y)) >= pred(minus(x, y))/\   pred(s(x)) >= x/\_if_95_gcd(true, x, y) > _gcd(minus(x, y), y)"))) or

 ((ordering_solve (order_constraints R_trs_default_algebra "    _if_95_gcd(true, x, y) >= _gcd(minus(x, y), y)/\    le(0, y) >= true/\  le(s(x), 0) >= false/\  le(s(x), s(y)) >= le(x, y)/\    minus(x, 0) >= x/\  minus(x, s(y)) >= pred(minus(x, y))/\   pred(s(x)) >= x/\_gcd(s(x), s(y)) > _if_95_gcd(le(y, x), s(x), s(y))"))))) or

 ((ordering_solve (order_constraints R_trs_default_algebra "    _if_95_gcd(true, x, y) >= _gcd(minus(x, y), y)/\    _if_95_gcd(false, x, y) >= _gcd(minus(y, x), x)/\   le(0, y) >= true/\  le(s(x), 0) >= false/\  le(s(x), s(y)) >= le(x, y)/\    minus(x, 0) >= x/\  minus(x, s(y)) >= pred(minus(x, y))/\   pred(s(x)) >= x/\_gcd(s(x), s(y)) > _if_95_gcd(le(y, x), s(x), s(y))")))) and


(((ordering_solve (order_constraints R_trs_default_algebra "_minus(x, s(y)) > _minus(x, y)")))) and


(((ordering_solve (order_constraints R_trs_default_algebra "_le(s(x), s(y)) > _le(x, y)")))) ;#verbose 3 ;
b ;