NO

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

Proof:
 String Reversal Processor:
  0(0(0(0(x1)))) -> 1(1(0(0(x1))))
  1(0(0(1(x1)))) -> 0(1(0(0(x1))))
  DP Processor:
   DPs:
    0#(0(0(0(x1)))) -> 1#(0(0(x1)))
    0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
    1#(0(0(1(x1)))) -> 0#(x1)
    1#(0(0(1(x1)))) -> 0#(0(x1))
    1#(0(0(1(x1)))) -> 1#(0(0(x1)))
    1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
   TRS:
    0(0(0(0(x1)))) -> 1(1(0(0(x1))))
    1(0(0(1(x1)))) -> 0(1(0(0(x1))))
   TDG Processor:
    DPs:
     0#(0(0(0(x1)))) -> 1#(0(0(x1)))
     0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
     1#(0(0(1(x1)))) -> 0#(x1)
     1#(0(0(1(x1)))) -> 0#(0(x1))
     1#(0(0(1(x1)))) -> 1#(0(0(x1)))
     1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
    TRS:
     0(0(0(0(x1)))) -> 1(1(0(0(x1))))
     1(0(0(1(x1)))) -> 0(1(0(0(x1))))
    graph:
     1#(0(0(1(x1)))) -> 1#(0(0(x1))) ->
     1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
     1#(0(0(1(x1)))) -> 1#(0(0(x1))) ->
     1#(0(0(1(x1)))) -> 1#(0(0(x1)))
     1#(0(0(1(x1)))) -> 1#(0(0(x1))) -> 1#(0(0(1(x1)))) -> 0#(0(x1))
     1#(0(0(1(x1)))) -> 1#(0(0(x1))) -> 1#(0(0(1(x1)))) -> 0#(x1)
     1#(0(0(1(x1)))) -> 0#(1(0(0(x1)))) ->
     0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
     1#(0(0(1(x1)))) -> 0#(1(0(0(x1)))) ->
     0#(0(0(0(x1)))) -> 1#(0(0(x1)))
     1#(0(0(1(x1)))) -> 0#(0(x1)) -> 0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
     1#(0(0(1(x1)))) -> 0#(0(x1)) -> 0#(0(0(0(x1)))) -> 1#(0(0(x1)))
     1#(0(0(1(x1)))) -> 0#(x1) -> 0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
     1#(0(0(1(x1)))) -> 0#(x1) -> 0#(0(0(0(x1)))) -> 1#(0(0(x1)))
     0#(0(0(0(x1)))) -> 1#(1(0(0(x1)))) ->
     1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
     0#(0(0(0(x1)))) -> 1#(1(0(0(x1)))) ->
     1#(0(0(1(x1)))) -> 1#(0(0(x1)))
     0#(0(0(0(x1)))) -> 1#(1(0(0(x1)))) ->
     1#(0(0(1(x1)))) -> 0#(0(x1))
     0#(0(0(0(x1)))) -> 1#(1(0(0(x1)))) -> 1#(0(0(1(x1)))) -> 0#(x1)
     0#(0(0(0(x1)))) -> 1#(0(0(x1))) ->
     1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
     0#(0(0(0(x1)))) -> 1#(0(0(x1))) ->
     1#(0(0(1(x1)))) -> 1#(0(0(x1)))
     0#(0(0(0(x1)))) -> 1#(0(0(x1))) -> 1#(0(0(1(x1)))) -> 0#(0(x1))
     0#(0(0(0(x1)))) -> 1#(0(0(x1))) -> 1#(0(0(1(x1)))) -> 0#(x1)
    Arctic Interpretation Processor:
     dimension: 2
     usable rules:
      0(0(0(0(x1)))) -> 1(1(0(0(x1))))
      1(0(0(1(x1)))) -> 0(1(0(0(x1))))
     interpretation:
      [1#](x0) = [-& 3 ]x0 + [0],
      
      [0#](x0) = [0 3]x0 + [0],
      
                [-& 1 ]     [3]
      [1](x0) = [1  -&]x0 + [0],
      
                [0  1 ]     [0]
      [0](x0) = [1  -&]x0 + [2]
     orientation:
      0#(0(0(0(x1)))) = [6 5]x1 + [7] >= [4 5]x1 + [5] = 1#(0(0(x1)))
      
      0#(0(0(0(x1)))) = [6 5]x1 + [7] >= [6 5]x1 + [7] = 1#(1(0(0(x1))))
      
      1#(0(0(1(x1)))) = [6 5]x1 + [7] >= [0 3]x1 + [0] = 0#(x1)
      
      1#(0(0(1(x1)))) = [6 5]x1 + [7] >= [4 1]x1 + [5] = 0#(0(x1))
      
      1#(0(0(1(x1)))) = [6 5]x1 + [7] >= [4 5]x1 + [5] = 1#(0(0(x1)))
      
      1#(0(0(1(x1)))) = [6 5]x1 + [7] >= [6 5]x1 + [7] = 0#(1(0(0(x1))))
      
                       [4 3]     [5]    [4 3]     [5]                 
      0(0(0(0(x1)))) = [3 4]x1 + [4] >= [3 4]x1 + [4] = 1(1(0(0(x1))))
      
                       [4 3]     [5]    [4 3]     [5]                 
      1(0(0(1(x1)))) = [3 4]x1 + [6] >= [3 4]x1 + [4] = 0(1(0(0(x1))))
     problem:
      DPs:
       0#(0(0(0(x1)))) -> 1#(0(0(x1)))
       0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
       1#(0(0(1(x1)))) -> 1#(0(0(x1)))
       1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
      TRS:
       0(0(0(0(x1)))) -> 1(1(0(0(x1))))
       1(0(0(1(x1)))) -> 0(1(0(0(x1))))
     Restore Modifier:
      DPs:
       0#(0(0(0(x1)))) -> 1#(0(0(x1)))
       0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
       1#(0(0(1(x1)))) -> 1#(0(0(x1)))
       1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
      TRS:
       0(0(0(0(x1)))) -> 1(1(0(0(x1))))
       1(0(0(1(x1)))) -> 0(1(0(0(x1))))
      EDG Processor:
       DPs:
        0#(0(0(0(x1)))) -> 1#(0(0(x1)))
        0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
        1#(0(0(1(x1)))) -> 1#(0(0(x1)))
        1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
       TRS:
        0(0(0(0(x1)))) -> 1(1(0(0(x1))))
        1(0(0(1(x1)))) -> 0(1(0(0(x1))))
       graph:
        1#(0(0(1(x1)))) -> 1#(0(0(x1))) ->
        1#(0(0(1(x1)))) -> 1#(0(0(x1)))
        1#(0(0(1(x1)))) -> 1#(0(0(x1))) ->
        1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
        1#(0(0(1(x1)))) -> 0#(1(0(0(x1)))) ->
        0#(0(0(0(x1)))) -> 1#(0(0(x1)))
        1#(0(0(1(x1)))) -> 0#(1(0(0(x1)))) ->
        0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
        0#(0(0(0(x1)))) -> 1#(1(0(0(x1)))) ->
        1#(0(0(1(x1)))) -> 1#(0(0(x1)))
        0#(0(0(0(x1)))) -> 1#(1(0(0(x1)))) ->
        1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
        0#(0(0(0(x1)))) -> 1#(0(0(x1))) ->
        1#(0(0(1(x1)))) -> 1#(0(0(x1)))
        0#(0(0(0(x1)))) -> 1#(0(0(x1))) -> 1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
       Arctic Interpretation Processor:
        dimension: 2
        usable rules:
         0(0(0(0(x1)))) -> 1(1(0(0(x1))))
         1(0(0(1(x1)))) -> 0(1(0(0(x1))))
        interpretation:
         [1#](x0) = [-& 1 ]x0 + [0],
         
         [0#](x0) = [0 1]x0 + [0],
         
                   [-& -&]     [0]
         [1](x0) = [3  1 ]x0 + [3],
         
                   [0  -&]     [0]
         [0](x0) = [3  1 ]x0 + [3]
        orientation:
         0#(0(0(0(x1)))) = [6 4]x1 + [6] >= [5 3]x1 + [5] = 1#(0(0(x1)))
         
         0#(0(0(0(x1)))) = [6 4]x1 + [6] >= [6 4]x1 + [6] = 1#(1(0(0(x1))))
         
         1#(0(0(1(x1)))) = [6 4]x1 + [6] >= [5 3]x1 + [5] = 1#(0(0(x1)))
         
         1#(0(0(1(x1)))) = [6 4]x1 + [6] >= [6 4]x1 + [6] = 0#(1(0(0(x1))))
         
                          [0  -&]     [0]    [-& -&]     [0]                 
         0(0(0(0(x1)))) = [6  4 ]x1 + [6] >= [6  4 ]x1 + [6] = 1(1(0(0(x1))))
         
                          [-& -&]     [0]    [-& -&]     [0]                 
         1(0(0(1(x1)))) = [6  4 ]x1 + [6] >= [6  4 ]x1 + [6] = 0(1(0(0(x1))))
        problem:
         DPs:
          0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
          1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
         TRS:
          0(0(0(0(x1)))) -> 1(1(0(0(x1))))
          1(0(0(1(x1)))) -> 0(1(0(0(x1))))
        Restore Modifier:
         DPs:
          0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
          1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
         TRS:
          0(0(0(0(x1)))) -> 1(1(0(0(x1))))
          1(0(0(1(x1)))) -> 0(1(0(0(x1))))
         EDG Processor:
          DPs:
           0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
           1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
          TRS:
           0(0(0(0(x1)))) -> 1(1(0(0(x1))))
           1(0(0(1(x1)))) -> 0(1(0(0(x1))))
          graph:
           1#(0(0(1(x1)))) -> 0#(1(0(0(x1)))) ->
           0#(0(0(0(x1)))) -> 1#(1(0(0(x1))))
           0#(0(0(0(x1)))) -> 1#(1(0(0(x1)))) -> 1#(0(0(1(x1)))) -> 0#(1(0(0(x1))))
          Loop Processor:
           loop length: 15
           terms:
            1(0(0(1(0(0(1(0(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            0(1(0(0(0(0(1(0(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            0(1(0(0(0(0(0(1(0(0(0(0(0(0(0(0(1(x1)))))))))))))))))
            0(1(0(0(0(0(0(1(1(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            0(1(0(1(1(0(0(1(1(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            0(1(0(1(0(1(0(0(1(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            0(1(0(1(0(0(1(0(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            0(1(0(0(1(0(0(0(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            0(1(0(0(1(1(1(0(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            0(0(1(0(0(1(1(0(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            0(0(0(1(0(0(1(0(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            0(0(0(0(1(0(0(0(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            1(1(0(0(1(0(0(0(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            1(0(1(0(0(0(0(0(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))
            1(0(1(0(0(1(1(0(0(1(0(0(0(0(0(0(1(x1)))))))))))))))))
           context: []
           substitution:
            x1 -> x1
           Qed