(VAR x)
(RULES 
  0(0(0(1(2(1(1(1(0(0(1(0(1(x))))))))))))) -> 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x)))))))))))))))))
  0(0(1(0(0(1(1(1(0(1(2(0(1(x))))))))))))) -> 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x)))))))))))))))))
  0(0(1(0(1(0(1(0(0(1(0(2(0(x))))))))))))) -> 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x)))))))))))))))))
  0(0(1(1(1(1(1(2(1(1(2(1(1(x))))))))))))) -> 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x)))))))))))))))))
  0(1(0(2(0(2(1(0(0(1(0(1(1(x))))))))))))) -> 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x)))))))))))))))))
  0(1(0(2(2(1(1(2(1(2(2(0(1(x))))))))))))) -> 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x)))))))))))))))))
  0(1(1(0(1(1(0(1(0(2(1(0(0(x))))))))))))) -> 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x)))))))))))))))))
  0(1(1(1(2(1(2(0(1(2(1(0(1(x))))))))))))) -> 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x)))))))))))))))))
  0(2(0(0(1(1(2(0(1(0(1(0(2(x))))))))))))) -> 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x)))))))))))))))))
  1(0(2(0(0(2(0(1(2(0(1(0(1(x))))))))))))) -> 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x)))))))))))))))))
  1(0(2(0(2(1(0(2(0(1(1(2(0(x))))))))))))) -> 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x)))))))))))))))))
  1(1(0(0(2(2(2(0(1(2(0(1(1(x))))))))))))) -> 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x)))))))))))))))))
  1(2(0(1(0(2(0(1(0(1(2(1(0(x))))))))))))) -> 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x)))))))))))))))))
  1(2(1(2(0(0(0(1(1(1(0(0(1(x))))))))))))) -> 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x)))))))))))))))))
  2(0(0(0(2(2(0(2(2(0(1(0(1(x))))))))))))) -> 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x)))))))))))))))))
  2(0(2(1(0(0(1(0(0(0(1(1(1(x))))))))))))) -> 0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x)))))))))))))))))
  2(0(2(1(1(1(1(0(2(0(1(0(1(x))))))))))))) -> 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x)))))))))))))))))
  2(1(2(2(1(1(2(2(0(1(1(0(1(x))))))))))))) -> 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x)))))))))))))))))
  2(2(1(1(1(1(0(1(1(2(0(1(0(x))))))))))))) -> 0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x)))))))))))))))))
)
(COMMENT
TPDB SRS_Standard/ICFP_2010/140654
)