(VAR u v x y z ) (RULES if(true, x, y) -> x if(false, x, y) -> y if(x, y, y) -> y if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v)) if(x, if(x, y, z), z) -> if(x, y, z) if(x, y, if(x, y, z)) -> if(x, y, z) )