YES (VAR x) (RULES not(not(n0())) -> n0() and(x,not(n0())) -> x or(x,not(n0())) -> not(n0()) n1() -> not(n0()) or(x,n0()) -> x and(x,n0()) -> n0() ) (COMMENT Termination is shown by ELPO with interpretations on natural numbers and_A(x1,x2) = x1 + 1 n0_A = 1 n1_A = 1 or_A(x1,x2) = x1 + 1 not_A(x1) = 1 and#_A(x1,x2) = x1 + x2 n0#_A = 0 n1#_A = 0 or#_A(x1,x2) = x1 + x2 and precedence: n1 > n0 > not > or > and )