(VAR x1 )
(RULES 
        2(7(x1)) -> 1(8(x1))
        2(8(1(x1))) -> 8(x1)
        2(8(x1)) -> 4(x1)
        5(9(x1)) -> 0(x1)
        4(x1) -> 5(2(3(x1)))
        5(3(x1)) -> 6(0(x1))
        2(8(x1)) -> 7(x1)
        4(7(x1)) -> 1(3(x1))
        5(2(6(x1))) -> 6(2(4(x1)))
        9(7(x1)) -> 7(5(x1))
        7(2(x1)) -> 4(x1)
        7(0(x1)) -> 9(3(x1))
        6(9(x1)) -> 9(x1)
        9(5(9(x1))) -> 5(7(x1))
        4(x1) -> 9(6(6(x1)))
        9(x1) -> 6(7(x1))
        6(2(x1)) -> 7(7(x1))
        2(4(x1)) -> 0(7(x1))
        6(6(x1)) -> 3(x1)
        0(3(x1)) -> 5(3(x1))
        
)