(VAR x y z) (RULES le(0, y, z) -> greater(y, z) le(s(x), 0, z) -> false le(s(x), s(y), 0) -> false le(s(x), s(y), s(z)) -> le(x, y, z) greater(x, 0) -> first greater(0, s(y)) -> second greater(s(x), s(y)) -> greater(x, y) double(0) -> 0 double(s(x)) -> s(s(double(x))) triple(x) -> if(le(x, x, double(x)), x, 0, 0) if(false, x, y, z) -> true if(first, x, y, z) -> if(le(s(x), y, s(z)), s(x), y, s(z)) if(second, x, y, z) -> if(le(s(x), s(y), z), s(x), s(y), z) )