YES

Problem:
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
 0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 0(1(2(1(x1)))) ->
 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

Proof:
 DP Processor:
  DPs:
   0#(1(2(1(x1)))) -> 0#(1(2(x1)))
   0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(x1))))))
   0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(x1)))))))))
   0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))
   0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))
   0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))
   0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))
   0#(1(2(1(x1)))) -> 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   0#(1(2(1(x1)))) ->
   0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  TRS:
   0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
   0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
   0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
   0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
   0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
   0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   0(1(2(1(x1)))) ->
   1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
    [0#](x0) = [0 0 1]x0 + [1],
    
              [0 0 1]     [0]
    [0](x0) = [0 0 0]x0 + [0]
              [1 0 1]     [1],
    
              [0 0 0]  
    [2](x0) = [0 0 0]x0
              [1 0 0]  ,
    
              [1 0 0]     [1]
    [1](x0) = [0 0 0]x0 + [0]
              [0 0 1]     [0]
   orientation:
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(x1)))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(x1))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(x1)))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1(2(x1))))))))))))))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1)))))))))))))))))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1))))))))))))))))))))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1)))))))))))))))))))))))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    
    0#(1(2(1(x1)))) = [1 0 0]x1 + [2] >= [1 0 0]x1 + [1] = 0#(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                   
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(x1))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                   
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                            
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                            
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                     
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                     
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                              
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                              
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                       
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                       
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                         
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                         
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                  
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                  
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                           
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                           
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                                                                                                                                                                              
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0
                                                                    (
                                                                    1(2(x1)))))))))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                                                                                                                                                                              
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1))))))))))))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1)))))))))))))))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                            
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1))))))))))))))))))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                   
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                 
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                      
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                             
    
                     [1 0 0]     [1]    [0 0 0]     [1]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    
    0(1(2(1(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
                     [1 0 0]     [3]    [1 0 0]     [2]                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                    
   problem:
    DPs:
     
    TRS:
     0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(x1))))))))))
     0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(x1)))))))))))))
     0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))
     0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))
     0(1(2(1(x1)))) -> 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
     0(1(2(1(x1)))) ->
     1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0
                                                                    (
                                                                    1
                                                                    (
                                                                    2
                                                                    (
                                                                    0(1(2(0(1(2(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
   Qed