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))))))))))))))))))))))))))))))))))

Proof:
 String Reversal Processor:
  1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1))))))))))
  1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))
  1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))
  1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))
  1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))
  1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))
  1(2(1(0(x1)))) ->
  2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))
  1(2(1(0(x1)))) ->
  2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))
  1(2(1(0(x1)))) ->
  2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))
  DP Processor:
   DPs:
    1#(2(1(0(x1)))) -> 1#(x1)
    1#(2(1(0(x1)))) -> 1#(2(1(x1)))
    1#(2(1(0(x1)))) -> 1#(1(2(1(x1))))
    1#(2(1(0(x1)))) -> 1#(0(1(1(2(1(x1))))))
    1#(2(1(0(x1)))) -> 1#(0(2(1(0(1(1(2(1(x1)))))))))
    1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))
    1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))
    1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))
    1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))
    1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))
    1#(2(1(0(x1)))) ->
    1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))
    1#(2(1(0(x1)))) ->
    1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))
    1#(2(1(0(x1)))) ->
    1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))
   TRS:
    1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1))))))))))
    1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))
    1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))
    1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))
    1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))
    1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))
    1(2(1(0(x1)))) ->
    2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))
    1(2(1(0(x1)))) ->
    2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))
    1(2(1(0(x1)))) ->
    2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))
   EDG Processor:
    DPs:
     1#(2(1(0(x1)))) -> 1#(x1)
     1#(2(1(0(x1)))) -> 1#(2(1(x1)))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1))))
     1#(2(1(0(x1)))) -> 1#(0(1(1(2(1(x1))))))
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(1(1(2(1(x1)))))))))
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))
     1#(2(1(0(x1)))) ->
     1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))
     1#(2(1(0(x1)))) ->
     1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))
     1#(2(1(0(x1)))) ->
     1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))
    TRS:
     1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1))))))))))
     1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))
     1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))
     1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))
     1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))
     1(2(1(0(x1)))) ->
     2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))
     1(2(1(0(x1)))) ->
     2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))
     1(2(1(0(x1)))) ->
     2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))
     1(2(1(0(x1)))) ->
     2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))
    graph:
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) -> 1#(2(1(0(x1)))) -> 1#(x1)
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) ->
     1#(2(1(0(x1)))) -> 1#(2(1(x1)))
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) ->
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1))))
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) ->
     1#(2(1(0(x1)))) -> 1#(0(1(1(2(1(x1))))))
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(1(1(2(1(x1)))))))))
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) ->
     1#(2(1(0(x1)))) ->
     1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) ->
     1#(2(1(0(x1)))) ->
     1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(2(1(x1))) ->
     1#(2(1(0(x1)))) ->
     1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) -> 1#(x1)
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) -> 1#(2(1(x1)))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1))))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) -> 1#(0(1(1(2(1(x1))))))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(1(1(2(1(x1)))))))))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) ->
     1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) ->
     1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(1(2(1(x1)))) ->
     1#(2(1(0(x1)))) ->
     1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(x1)
     1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(2(1(x1)))
     1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(1(2(1(x1))))
     1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(0(1(1(2(1(x1))))))
     1#(2(1(0(x1)))) -> 1#(x1) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(1(1(2(1(x1)))))))))
     1#(2(1(0(x1)))) -> 1#(x1) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))
     1#(2(1(0(x1)))) -> 1#(x1) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))
     1#(2(1(0(x1)))) -> 1#(x1) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(x1) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(x1) ->
     1#(2(1(0(x1)))) -> 1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(x1) ->
     1#(2(1(0(x1)))) ->
     1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(x1) ->
     1#(2(1(0(x1)))) ->
     1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))
     1#(2(1(0(x1)))) -> 1#(x1) ->
     1#(2(1(0(x1)))) ->
     1#(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))
    SCC Processor:
     #sccs: 1
     #rules: 3
     #arcs: 39/169
     DPs:
      1#(2(1(0(x1)))) -> 1#(2(1(x1)))
      1#(2(1(0(x1)))) -> 1#(1(2(1(x1))))
      1#(2(1(0(x1)))) -> 1#(x1)
     TRS:
      1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1))))))))))
      1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))
      1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))
      1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))
      1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))
      1(2(1(0(x1)))) ->
      2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))
      1(2(1(0(x1)))) ->
      2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))
      1(2(1(0(x1)))) ->
      2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))
      1(2(1(0(x1)))) ->
      2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))
     Arctic Interpretation Processor:
      dimension: 1
      usable rules:
       1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1))))))))))
       1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))
       1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))
       1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))
       1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))
       1(2(1(0(x1)))) ->
       2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))
       1(2(1(0(x1)))) ->
       2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))
       1(2(1(0(x1)))) ->
       2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))
       1(2(1(0(x1)))) ->
       2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))
      interpretation:
       [1#](x0) = x0 + 0,
       
       [0](x0) = 4x0 + 10,
       
       [2](x0) = -4x0 + 0,
       
       [1](x0) = x0 + 4
      orientation:
       1#(2(1(0(x1)))) = x1 + 6 >= -4x1 + 0 = 1#(2(1(x1)))
       
       1#(2(1(0(x1)))) = x1 + 6 >= -4x1 + 4 = 1#(1(2(1(x1))))
       
       1#(2(1(0(x1)))) = x1 + 6 >= x1 + 0 = 1#(x1)
       
       1(2(1(0(x1)))) = x1 + 6 >= -4x1 + 6 = 2(1(0(2(1(0(1(1(2(1(x1))))))))))
       
       1(2(1(0(x1)))) = x1 + 6 >= -4x1 + 6 = 2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))
       
       1(2(1(0(x1)))) = x1 + 6 >= -4x1 + 6 = 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))
       
       1(2(1(0(x1)))) = x1 + 6 >= -4x1 + 6 = 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))
       
       1(2(1(0(x1)))) = x1 + 6 >= -4x1 + 6 = 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))
       
       1(2(1(0(x1)))) = x1 + 6 >= -4x1 + 6 = 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))
       
       1(2(1(0(x1)))) = x1 + 6 >= -4x1 + 6 = 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))
       
       1(2(1(0(x1)))) = x1 + 6 >= -4x1 + 6 = 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))
       
       1(2(1(0(x1)))) = x1 + 6 >= -4x1 + 6 = 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))
      problem:
       DPs:
        1#(2(1(0(x1)))) -> 1#(x1)
       TRS:
        1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1))))))))))
        1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))
        1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))
        1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))
        1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))
        1(2(1(0(x1)))) ->
        2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))
        1(2(1(0(x1)))) ->
        2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))
        1(2(1(0(x1)))) ->
        2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))
        1(2(1(0(x1)))) ->
        2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))
      Restore Modifier:
       DPs:
        1#(2(1(0(x1)))) -> 1#(x1)
       TRS:
        1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1))))))))))
        1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))
        1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))
        1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))
        1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))
        1(2(1(0(x1)))) ->
        2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))
        1(2(1(0(x1)))) ->
        2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))
        1(2(1(0(x1)))) ->
        2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))
        1(2(1(0(x1)))) ->
        2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))
       EDG Processor:
        DPs:
         1#(2(1(0(x1)))) -> 1#(x1)
        TRS:
         1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1))))))))))
         1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))
         1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))
         1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))
         1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))
         1(2(1(0(x1)))) ->
         2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))
         1(2(1(0(x1)))) ->
         2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))
         1(2(1(0(x1)))) ->
         2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))
         1(2(1(0(x1)))) ->
         2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))
        graph:
         1#(2(1(0(x1)))) -> 1#(x1) -> 1#(2(1(0(x1)))) -> 1#(x1)
        CDG Processor:
         DPs:
          1#(2(1(0(x1)))) -> 1#(x1)
         TRS:
          1(2(1(0(x1)))) -> 2(1(0(2(1(0(1(1(2(1(x1))))))))))
          1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))
          1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))
          1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))
          1(2(1(0(x1)))) -> 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))
          1(2(1(0(x1)))) ->
          2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))
          1(2(1(0(x1)))) ->
          2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))
          1(2(1(0(x1)))) ->
          2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))
          1(2(1(0(x1)))) ->
          2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x1))))))))))))))))))))))))))))))))))
         graph:
          
         Qed