(VAR x1 ) (RULES 0(x1) -> 1(x1) 4(5(4(5(x1)))) -> 4(4(5(5(x1)))) 5(5(5(5(5(5(4(4(4(4(4(4(x1)))))))))))) -> 2(x1) )