let R_trs_default_variable = variables "n,y,x" ;

let R_trs_default_signature =
 signature "shuffle : 1;
    _shuffle : 1;
    reverse : 1;
    _reverse : 1;
    add : 2;
    _add : 2;
    nil : 0;
    _nil : 0;
    app : 2;
    _app : 2" ;

let R_trs_default_algebra = algebra R_trs_default_signature ;

#Set_sat_solver "minisat2";
let b = (((ordering_solve (order_constraints R_trs_default_algebra "    app(add(n, x), y) >= add(n, app(x, y))/\    app(nil, y) >= y/\  reverse(add(n, x)) >= app(reverse(x), add(n, nil))/\    reverse(nil) >= nil/\_shuffle(add(n, x)) > _shuffle(reverse(x))")))) and


(((ordering_solve (order_constraints R_trs_default_algebra "_reverse(add(n, x)) > _reverse(x)")))) and


(((ordering_solve (order_constraints R_trs_default_algebra "_app(add(n, x), y) > _app(x, y)")))) ;#verbose 3 ;
b ;