YES TRS: cond(true(),x) -> cond(and(even(x),gr(x,0())),p(x)) and(x,false()) -> false() and(false(),x) -> false() and(true(),true()) -> true() even(0()) -> true() even(s(0())) -> false() even(s(s(x))) -> even(x) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y())) -> gr(x,y()) p(0()) -> 0() p(s(x)) -> x max/plus interpretations on N: cond_A(x1,x2) = max{0, 1, -8 + x2} cond#_A(x1,x2) = max{19, 15 + x1, 9 + x2} true_A = 6 true#_A = 5 and_A(x1,x2) = max{0, -8 + x1, x2} and#_A(x1,x2) = max{8, x1, 0} even_A(x1) = max{1, -3 + x1} even#_A(x1) = max{8, 7 + x1} gr_A(x1,x2) = max{3, -10 + x1, -7} gr#_A(x1,x2) = max{2, 4, 3} 0_A = 9 0#_A = 4 p_A(x1) = max{9, -1 + x1} p#_A(x1) = max{20, 3} false_A = 0 false#_A = 1 s_A(x1) = max{2, 16 + x1} s#_A(x1) = max{0, 6} y_A = 3 y#_A = 5 precedence: cond > and > true = p > 0 > false > even > s > y > gr