YES(?,O(n^1))

Problem:
 +(p1(),p1()) -> p2()
 +(p1(),+(p2(),p2())) -> p5()
 +(p5(),p5()) -> p10()
 +(+(x,y),z) -> +(x,+(y,z))
 +(p1(),+(p1(),x)) -> +(p2(),x)
 +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
 +(p2(),p1()) -> +(p1(),p2())
 +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
 +(p2(),+(p2(),p2())) -> +(p1(),p5())
 +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
 +(p5(),p1()) -> +(p1(),p5())
 +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
 +(p5(),p2()) -> +(p2(),p5())
 +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
 +(p5(),+(p5(),x)) -> +(p10(),x)
 +(p10(),p1()) -> +(p1(),p10())
 +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
 +(p10(),p2()) -> +(p2(),p10())
 +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
 +(p10(),p5()) -> +(p5(),p10())
 +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))

Proof:
 Complexity Transformation Processor:
  strict:
   +(p1(),p1()) -> p2()
   +(p1(),+(p2(),p2())) -> p5()
   +(p5(),p5()) -> p10()
   +(+(x,y),z) -> +(x,+(y,z))
   +(p1(),+(p1(),x)) -> +(p2(),x)
   +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
   +(p2(),p1()) -> +(p1(),p2())
   +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
   +(p2(),+(p2(),p2())) -> +(p1(),p5())
   +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
   +(p5(),p1()) -> +(p1(),p5())
   +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
   +(p5(),p2()) -> +(p2(),p5())
   +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
   +(p5(),+(p5(),x)) -> +(p10(),x)
   +(p10(),p1()) -> +(p1(),p10())
   +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
   +(p10(),p2()) -> +(p2(),p10())
   +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
   +(p10(),p5()) -> +(p5(),p10())
   +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [p10] = 0,
     
     [p5] = 0,
     
     [p2] = 1,
     
     [+](x0, x1) = x0 + x1,
     
     [p1] = 0
    orientation:
     +(p1(),p1()) = 0 >= 1 = p2()
     
     +(p1(),+(p2(),p2())) = 2 >= 0 = p5()
     
     +(p5(),p5()) = 0 >= 0 = p10()
     
     +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
     
     +(p1(),+(p1(),x)) = x >= x + 1 = +(p2(),x)
     
     +(p1(),+(p2(),+(p2(),x))) = x + 2 >= x = +(p5(),x)
     
     +(p2(),p1()) = 1 >= 1 = +(p1(),p2())
     
     +(p2(),+(p1(),x)) = x + 1 >= x + 1 = +(p1(),+(p2(),x))
     
     +(p2(),+(p2(),p2())) = 3 >= 0 = +(p1(),p5())
     
     +(p2(),+(p2(),+(p2(),x))) = x + 3 >= x = +(p1(),+(p5(),x))
     
     +(p5(),p1()) = 0 >= 0 = +(p1(),p5())
     
     +(p5(),+(p1(),x)) = x >= x = +(p1(),+(p5(),x))
     
     +(p5(),p2()) = 1 >= 1 = +(p2(),p5())
     
     +(p5(),+(p2(),x)) = x + 1 >= x + 1 = +(p2(),+(p5(),x))
     
     +(p5(),+(p5(),x)) = x >= x = +(p10(),x)
     
     +(p10(),p1()) = 0 >= 0 = +(p1(),p10())
     
     +(p10(),+(p1(),x)) = x >= x = +(p1(),+(p10(),x))
     
     +(p10(),p2()) = 1 >= 1 = +(p2(),p10())
     
     +(p10(),+(p2(),x)) = x + 1 >= x + 1 = +(p2(),+(p10(),x))
     
     +(p10(),p5()) = 0 >= 0 = +(p5(),p10())
     
     +(p10(),+(p5(),x)) = x >= x = +(p5(),+(p10(),x))
    problem:
     strict:
      +(p1(),p1()) -> p2()
      +(p5(),p5()) -> p10()
      +(+(x,y),z) -> +(x,+(y,z))
      +(p1(),+(p1(),x)) -> +(p2(),x)
      +(p2(),p1()) -> +(p1(),p2())
      +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
      +(p5(),p1()) -> +(p1(),p5())
      +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
      +(p5(),p2()) -> +(p2(),p5())
      +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
      +(p5(),+(p5(),x)) -> +(p10(),x)
      +(p10(),p1()) -> +(p1(),p10())
      +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
      +(p10(),p2()) -> +(p2(),p10())
      +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
      +(p10(),p5()) -> +(p5(),p10())
      +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
     weak:
      +(p1(),+(p2(),p2())) -> p5()
      +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
      +(p2(),+(p2(),p2())) -> +(p1(),p5())
      +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [p10] = 1,
       
       [p5] = 0,
       
       [p2] = 0,
       
       [+](x0, x1) = x0 + x1 + 1,
       
       [p1] = 0
      orientation:
       +(p1(),p1()) = 1 >= 0 = p2()
       
       +(p5(),p5()) = 1 >= 1 = p10()
       
       +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z))
       
       +(p1(),+(p1(),x)) = x + 2 >= x + 1 = +(p2(),x)
       
       +(p2(),p1()) = 1 >= 1 = +(p1(),p2())
       
       +(p2(),+(p1(),x)) = x + 2 >= x + 2 = +(p1(),+(p2(),x))
       
       +(p5(),p1()) = 1 >= 1 = +(p1(),p5())
       
       +(p5(),+(p1(),x)) = x + 2 >= x + 2 = +(p1(),+(p5(),x))
       
       +(p5(),p2()) = 1 >= 1 = +(p2(),p5())
       
       +(p5(),+(p2(),x)) = x + 2 >= x + 2 = +(p2(),+(p5(),x))
       
       +(p5(),+(p5(),x)) = x + 2 >= x + 2 = +(p10(),x)
       
       +(p10(),p1()) = 2 >= 2 = +(p1(),p10())
       
       +(p10(),+(p1(),x)) = x + 3 >= x + 3 = +(p1(),+(p10(),x))
       
       +(p10(),p2()) = 2 >= 2 = +(p2(),p10())
       
       +(p10(),+(p2(),x)) = x + 3 >= x + 3 = +(p2(),+(p10(),x))
       
       +(p10(),p5()) = 2 >= 2 = +(p5(),p10())
       
       +(p10(),+(p5(),x)) = x + 3 >= x + 3 = +(p5(),+(p10(),x))
       
       +(p1(),+(p2(),p2())) = 2 >= 0 = p5()
       
       +(p1(),+(p2(),+(p2(),x))) = x + 3 >= x + 1 = +(p5(),x)
       
       +(p2(),+(p2(),p2())) = 2 >= 1 = +(p1(),p5())
       
       +(p2(),+(p2(),+(p2(),x))) = x + 3 >= x + 2 = +(p1(),+(p5(),x))
      problem:
       strict:
        +(p5(),p5()) -> p10()
        +(+(x,y),z) -> +(x,+(y,z))
        +(p2(),p1()) -> +(p1(),p2())
        +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
        +(p5(),p1()) -> +(p1(),p5())
        +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
        +(p5(),p2()) -> +(p2(),p5())
        +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
        +(p5(),+(p5(),x)) -> +(p10(),x)
        +(p10(),p1()) -> +(p1(),p10())
        +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
        +(p10(),p2()) -> +(p2(),p10())
        +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
        +(p10(),p5()) -> +(p5(),p10())
        +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
       weak:
        +(p1(),p1()) -> p2()
        +(p1(),+(p1(),x)) -> +(p2(),x)
        +(p1(),+(p2(),p2())) -> p5()
        +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
        +(p2(),+(p2(),p2())) -> +(p1(),p5())
        +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [p10] = 0,
         
         [p5] = 1,
         
         [p2] = 1,
         
         [+](x0, x1) = x0 + x1,
         
         [p1] = 1
        orientation:
         +(p5(),p5()) = 2 >= 0 = p10()
         
         +(+(x,y),z) = x + y + z >= x + y + z = +(x,+(y,z))
         
         +(p2(),p1()) = 2 >= 2 = +(p1(),p2())
         
         +(p2(),+(p1(),x)) = x + 2 >= x + 2 = +(p1(),+(p2(),x))
         
         +(p5(),p1()) = 2 >= 2 = +(p1(),p5())
         
         +(p5(),+(p1(),x)) = x + 2 >= x + 2 = +(p1(),+(p5(),x))
         
         +(p5(),p2()) = 2 >= 2 = +(p2(),p5())
         
         +(p5(),+(p2(),x)) = x + 2 >= x + 2 = +(p2(),+(p5(),x))
         
         +(p5(),+(p5(),x)) = x + 2 >= x = +(p10(),x)
         
         +(p10(),p1()) = 1 >= 1 = +(p1(),p10())
         
         +(p10(),+(p1(),x)) = x + 1 >= x + 1 = +(p1(),+(p10(),x))
         
         +(p10(),p2()) = 1 >= 1 = +(p2(),p10())
         
         +(p10(),+(p2(),x)) = x + 1 >= x + 1 = +(p2(),+(p10(),x))
         
         +(p10(),p5()) = 1 >= 1 = +(p5(),p10())
         
         +(p10(),+(p5(),x)) = x + 1 >= x + 1 = +(p5(),+(p10(),x))
         
         +(p1(),p1()) = 2 >= 1 = p2()
         
         +(p1(),+(p1(),x)) = x + 2 >= x + 1 = +(p2(),x)
         
         +(p1(),+(p2(),p2())) = 3 >= 1 = p5()
         
         +(p1(),+(p2(),+(p2(),x))) = x + 3 >= x + 1 = +(p5(),x)
         
         +(p2(),+(p2(),p2())) = 3 >= 2 = +(p1(),p5())
         
         +(p2(),+(p2(),+(p2(),x))) = x + 3 >= x + 2 = +(p1(),+(p5(),x))
        problem:
         strict:
          +(+(x,y),z) -> +(x,+(y,z))
          +(p2(),p1()) -> +(p1(),p2())
          +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
          +(p5(),p1()) -> +(p1(),p5())
          +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
          +(p5(),p2()) -> +(p2(),p5())
          +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
          +(p10(),p1()) -> +(p1(),p10())
          +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
          +(p10(),p2()) -> +(p2(),p10())
          +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
          +(p10(),p5()) -> +(p5(),p10())
          +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
         weak:
          +(p5(),p5()) -> p10()
          +(p5(),+(p5(),x)) -> +(p10(),x)
          +(p1(),p1()) -> p2()
          +(p1(),+(p1(),x)) -> +(p2(),x)
          +(p1(),+(p2(),p2())) -> p5()
          +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
          +(p2(),+(p2(),p2())) -> +(p1(),p5())
          +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
        Bounds Processor:
         bound: 0
         enrichment: match
         automaton:
          final states: {5}
          transitions:
           +0(3,1) -> 5*
           +0(3,3) -> 5*
           +0(4,2) -> 5*
           +0(4,4) -> 5*
           +0(1,2) -> 5*
           +0(1,4) -> 5*
           +0(2,1) -> 5*
           +0(2,3) -> 5*
           +0(3,2) -> 5*
           +0(3,4) -> 5*
           +0(4,1) -> 5*
           +0(4,3) -> 5*
           +0(1,1) -> 5*
           +0(1,3) -> 5*
           +0(2,2) -> 5*
           +0(2,4) -> 5*
           p20() -> 5,1
           p10() -> 2*
           p50() -> 3*
           p100() -> 5,4
         problem:
          strict:
           +(+(x,y),z) -> +(x,+(y,z))
           +(p2(),p1()) -> +(p1(),p2())
           +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
           +(p5(),p1()) -> +(p1(),p5())
           +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
           +(p5(),p2()) -> +(p2(),p5())
           +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
           +(p10(),p1()) -> +(p1(),p10())
           +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
           +(p10(),p2()) -> +(p2(),p10())
           +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
           +(p10(),p5()) -> +(p5(),p10())
          weak:
           +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
           +(p5(),p5()) -> p10()
           +(p5(),+(p5(),x)) -> +(p10(),x)
           +(p1(),p1()) -> p2()
           +(p1(),+(p1(),x)) -> +(p2(),x)
           +(p1(),+(p2(),p2())) -> p5()
           +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
           +(p2(),+(p2(),p2())) -> +(p1(),p5())
           +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
         Bounds Processor:
          bound: 0
          enrichment: match
          automaton:
           final states: {5}
           transitions:
            +0(3,1) -> 5*
            +0(3,3) -> 5*
            +0(4,2) -> 5*
            +0(4,4) -> 5*
            +0(1,2) -> 5*
            +0(1,4) -> 5*
            +0(2,1) -> 5*
            +0(2,3) -> 5*
            +0(3,2) -> 5*
            +0(3,4) -> 5*
            +0(4,1) -> 5*
            +0(4,3) -> 5*
            +0(1,1) -> 5*
            +0(1,3) -> 5*
            +0(2,2) -> 5*
            +0(2,4) -> 5*
            p20() -> 5,1
            p10() -> 2*
            p50() -> 3*
            p100() -> 5,4
          problem:
           strict:
            +(+(x,y),z) -> +(x,+(y,z))
            +(p2(),p1()) -> +(p1(),p2())
            +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
            +(p5(),p1()) -> +(p1(),p5())
            +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
            +(p5(),p2()) -> +(p2(),p5())
            +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
            +(p10(),p1()) -> +(p1(),p10())
            +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
            +(p10(),p2()) -> +(p2(),p10())
            +(p10(),p5()) -> +(p5(),p10())
           weak:
            +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
            +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
            +(p5(),p5()) -> p10()
            +(p5(),+(p5(),x)) -> +(p10(),x)
            +(p1(),p1()) -> p2()
            +(p1(),+(p1(),x)) -> +(p2(),x)
            +(p1(),+(p2(),p2())) -> p5()
            +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
            +(p2(),+(p2(),p2())) -> +(p1(),p5())
            +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
          Bounds Processor:
           bound: 0
           enrichment: match
           automaton:
            final states: {5}
            transitions:
             +0(3,1) -> 5*
             +0(3,3) -> 5*
             +0(4,2) -> 5*
             +0(4,4) -> 5*
             +0(1,2) -> 5*
             +0(1,4) -> 5*
             +0(2,1) -> 5*
             +0(2,3) -> 5*
             +0(3,2) -> 5*
             +0(3,4) -> 5*
             +0(4,1) -> 5*
             +0(4,3) -> 5*
             +0(1,1) -> 5*
             +0(1,3) -> 5*
             +0(2,2) -> 5*
             +0(2,4) -> 5*
             p20() -> 5,1
             p10() -> 2*
             p50() -> 3*
             p100() -> 5,4
           problem:
            strict:
             +(+(x,y),z) -> +(x,+(y,z))
             +(p2(),p1()) -> +(p1(),p2())
             +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
             +(p5(),p1()) -> +(p1(),p5())
             +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
             +(p5(),p2()) -> +(p2(),p5())
             +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
             +(p10(),p1()) -> +(p1(),p10())
             +(p10(),p2()) -> +(p2(),p10())
             +(p10(),p5()) -> +(p5(),p10())
            weak:
             +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
             +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
             +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
             +(p5(),p5()) -> p10()
             +(p5(),+(p5(),x)) -> +(p10(),x)
             +(p1(),p1()) -> p2()
             +(p1(),+(p1(),x)) -> +(p2(),x)
             +(p1(),+(p2(),p2())) -> p5()
             +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
             +(p2(),+(p2(),p2())) -> +(p1(),p5())
             +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
           Bounds Processor:
            bound: 0
            enrichment: match
            automaton:
             final states: {5}
             transitions:
              +0(3,1) -> 5*
              +0(3,3) -> 5*
              +0(4,2) -> 5*
              +0(4,4) -> 5*
              +0(1,2) -> 5*
              +0(1,4) -> 5*
              +0(2,1) -> 5*
              +0(2,3) -> 5*
              +0(3,2) -> 5*
              +0(3,4) -> 5*
              +0(4,1) -> 5*
              +0(4,3) -> 5*
              +0(1,1) -> 5*
              +0(1,3) -> 5*
              +0(2,2) -> 5*
              +0(2,4) -> 5*
              p20() -> 5,1
              p10() -> 2*
              p50() -> 3*
              p100() -> 5,4
            problem:
             strict:
              +(+(x,y),z) -> +(x,+(y,z))
              +(p2(),p1()) -> +(p1(),p2())
              +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
              +(p5(),p1()) -> +(p1(),p5())
              +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
              +(p5(),p2()) -> +(p2(),p5())
              +(p10(),p1()) -> +(p1(),p10())
              +(p10(),p2()) -> +(p2(),p10())
              +(p10(),p5()) -> +(p5(),p10())
             weak:
              +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
              +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
              +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
              +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
              +(p5(),p5()) -> p10()
              +(p5(),+(p5(),x)) -> +(p10(),x)
              +(p1(),p1()) -> p2()
              +(p1(),+(p1(),x)) -> +(p2(),x)
              +(p1(),+(p2(),p2())) -> p5()
              +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
              +(p2(),+(p2(),p2())) -> +(p1(),p5())
              +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
            Bounds Processor:
             bound: 0
             enrichment: match
             automaton:
              final states: {5}
              transitions:
               +0(3,1) -> 5*
               +0(3,3) -> 5*
               +0(4,2) -> 5*
               +0(4,4) -> 5*
               +0(1,2) -> 5*
               +0(1,4) -> 5*
               +0(2,1) -> 5*
               +0(2,3) -> 5*
               +0(3,2) -> 5*
               +0(3,4) -> 5*
               +0(4,1) -> 5*
               +0(4,3) -> 5*
               +0(1,1) -> 5*
               +0(1,3) -> 5*
               +0(2,2) -> 5*
               +0(2,4) -> 5*
               p20() -> 5,1
               p10() -> 2*
               p50() -> 3*
               p100() -> 5,4
             problem:
              strict:
               +(+(x,y),z) -> +(x,+(y,z))
               +(p2(),p1()) -> +(p1(),p2())
               +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
               +(p5(),p1()) -> +(p1(),p5())
               +(p5(),p2()) -> +(p2(),p5())
               +(p10(),p1()) -> +(p1(),p10())
               +(p10(),p2()) -> +(p2(),p10())
               +(p10(),p5()) -> +(p5(),p10())
              weak:
               +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
               +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
               +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
               +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
               +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
               +(p5(),p5()) -> p10()
               +(p5(),+(p5(),x)) -> +(p10(),x)
               +(p1(),p1()) -> p2()
               +(p1(),+(p1(),x)) -> +(p2(),x)
               +(p1(),+(p2(),p2())) -> p5()
               +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
               +(p2(),+(p2(),p2())) -> +(p1(),p5())
               +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
             Bounds Processor:
              bound: 0
              enrichment: match
              automaton:
               final states: {5}
               transitions:
                +0(3,1) -> 5*
                +0(3,3) -> 5*
                +0(4,2) -> 5*
                +0(4,4) -> 5*
                +0(1,2) -> 5*
                +0(1,4) -> 5*
                +0(2,1) -> 5*
                +0(2,3) -> 5*
                +0(3,2) -> 5*
                +0(3,4) -> 5*
                +0(4,1) -> 5*
                +0(4,3) -> 5*
                +0(1,1) -> 5*
                +0(1,3) -> 5*
                +0(2,2) -> 5*
                +0(2,4) -> 5*
                p20() -> 5,1
                p10() -> 2*
                p50() -> 3*
                p100() -> 5,4
              problem:
               strict:
                +(+(x,y),z) -> +(x,+(y,z))
                +(p2(),p1()) -> +(p1(),p2())
                +(p5(),p1()) -> +(p1(),p5())
                +(p5(),p2()) -> +(p2(),p5())
                +(p10(),p1()) -> +(p1(),p10())
                +(p10(),p2()) -> +(p2(),p10())
                +(p10(),p5()) -> +(p5(),p10())
               weak:
                +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
                +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
                +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
                +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
                +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
                +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
                +(p5(),p5()) -> p10()
                +(p5(),+(p5(),x)) -> +(p10(),x)
                +(p1(),p1()) -> p2()
                +(p1(),+(p1(),x)) -> +(p2(),x)
                +(p1(),+(p2(),p2())) -> p5()
                +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
                +(p2(),+(p2(),p2())) -> +(p1(),p5())
                +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
              Bounds Processor:
               bound: 0
               enrichment: match
               automaton:
                final states: {5}
                transitions:
                 +0(3,1) -> 5*
                 +0(3,3) -> 5*
                 +0(4,2) -> 5*
                 +0(4,4) -> 5*
                 +0(1,2) -> 5*
                 +0(1,4) -> 5*
                 +0(2,1) -> 5*
                 +0(2,3) -> 5*
                 +0(3,2) -> 5*
                 +0(3,4) -> 5*
                 +0(4,1) -> 5*
                 +0(4,3) -> 5*
                 +0(1,1) -> 5*
                 +0(1,3) -> 5*
                 +0(2,2) -> 5*
                 +0(2,4) -> 5*
                 p20() -> 5,1
                 p10() -> 2*
                 p50() -> 3*
                 p100() -> 5,4
               problem:
                strict:
                 +(p2(),p1()) -> +(p1(),p2())
                 +(p5(),p1()) -> +(p1(),p5())
                 +(p5(),p2()) -> +(p2(),p5())
                 +(p10(),p1()) -> +(p1(),p10())
                 +(p10(),p2()) -> +(p2(),p10())
                 +(p10(),p5()) -> +(p5(),p10())
                weak:
                 +(+(x,y),z) -> +(x,+(y,z))
                 +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
                 +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
                 +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
                 +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
                 +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
                 +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
                 +(p5(),p5()) -> p10()
                 +(p5(),+(p5(),x)) -> +(p10(),x)
                 +(p1(),p1()) -> p2()
                 +(p1(),+(p1(),x)) -> +(p2(),x)
                 +(p1(),+(p2(),p2())) -> p5()
                 +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
                 +(p2(),+(p2(),p2())) -> +(p1(),p5())
                 +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
               Bounds Processor:
                bound: 1
                enrichment: match
                automaton:
                 final states: {5}
                 transitions:
                  +1(7,6) -> 5*
                  p11() -> 7*
                  p21() -> 6*
                  +0(3,1) -> 5*
                  +0(3,3) -> 5*
                  +0(4,2) -> 5*
                  +0(4,4) -> 5*
                  +0(1,2) -> 5*
                  +0(1,4) -> 5*
                  +0(2,1) -> 5*
                  +0(2,3) -> 5*
                  +0(3,2) -> 5*
                  +0(3,4) -> 5*
                  +0(4,1) -> 5*
                  +0(4,3) -> 5*
                  +0(1,1) -> 5*
                  +0(1,3) -> 5*
                  +0(2,2) -> 5*
                  +0(2,4) -> 5*
                  p20() -> 5,1
                  p10() -> 2*
                  p50() -> 3*
                  p100() -> 5,4
                problem:
                 strict:
                  +(p5(),p1()) -> +(p1(),p5())
                  +(p5(),p2()) -> +(p2(),p5())
                  +(p10(),p1()) -> +(p1(),p10())
                  +(p10(),p2()) -> +(p2(),p10())
                  +(p10(),p5()) -> +(p5(),p10())
                 weak:
                  +(p2(),p1()) -> +(p1(),p2())
                  +(+(x,y),z) -> +(x,+(y,z))
                  +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
                  +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
                  +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
                  +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
                  +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
                  +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
                  +(p5(),p5()) -> p10()
                  +(p5(),+(p5(),x)) -> +(p10(),x)
                  +(p1(),p1()) -> p2()
                  +(p1(),+(p1(),x)) -> +(p2(),x)
                  +(p1(),+(p2(),p2())) -> p5()
                  +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
                  +(p2(),+(p2(),p2())) -> +(p1(),p5())
                  +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
                Bounds Processor:
                 bound: 1
                 enrichment: match
                 automaton:
                  final states: {5}
                  transitions:
                   +1(7,6) -> 5*
                   p11() -> 7*
                   p51() -> 6*
                   +0(3,1) -> 5*
                   +0(3,3) -> 5*
                   +0(4,2) -> 5*
                   +0(4,4) -> 5*
                   +0(1,2) -> 5*
                   +0(1,4) -> 5*
                   +0(2,1) -> 5*
                   +0(2,3) -> 5*
                   +0(3,2) -> 5*
                   +0(3,4) -> 5*
                   +0(4,1) -> 5*
                   +0(4,3) -> 5*
                   +0(1,1) -> 5*
                   +0(1,3) -> 5*
                   +0(2,2) -> 5*
                   +0(2,4) -> 5*
                   p20() -> 5,3
                   p10() -> 2*
                   p50() -> 1*
                   p100() -> 5,4
                 problem:
                  strict:
                   +(p5(),p2()) -> +(p2(),p5())
                   +(p10(),p1()) -> +(p1(),p10())
                   +(p10(),p2()) -> +(p2(),p10())
                   +(p10(),p5()) -> +(p5(),p10())
                  weak:
                   +(p5(),p1()) -> +(p1(),p5())
                   +(p2(),p1()) -> +(p1(),p2())
                   +(+(x,y),z) -> +(x,+(y,z))
                   +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
                   +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
                   +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
                   +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
                   +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
                   +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
                   +(p5(),p5()) -> p10()
                   +(p5(),+(p5(),x)) -> +(p10(),x)
                   +(p1(),p1()) -> p2()
                   +(p1(),+(p1(),x)) -> +(p2(),x)
                   +(p1(),+(p2(),p2())) -> p5()
                   +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
                   +(p2(),+(p2(),p2())) -> +(p1(),p5())
                   +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
                 Bounds Processor:
                  bound: 1
                  enrichment: match
                  automaton:
                   final states: {5}
                   transitions:
                    +1(7,6) -> 5*
                    p21() -> 7*
                    p51() -> 6*
                    +0(3,1) -> 5*
                    +0(3,3) -> 5*
                    +0(4,2) -> 5*
                    +0(4,4) -> 5*
                    +0(1,2) -> 5*
                    +0(1,4) -> 5*
                    +0(2,1) -> 5*
                    +0(2,3) -> 5*
                    +0(3,2) -> 5*
                    +0(3,4) -> 5*
                    +0(4,1) -> 5*
                    +0(4,3) -> 5*
                    +0(1,1) -> 5*
                    +0(1,3) -> 5*
                    +0(2,2) -> 5*
                    +0(2,4) -> 5*
                    p20() -> 5,2
                    p10() -> 4*
                    p50() -> 1*
                    p100() -> 5,3
                  problem:
                   strict:
                    +(p10(),p1()) -> +(p1(),p10())
                    +(p10(),p2()) -> +(p2(),p10())
                    +(p10(),p5()) -> +(p5(),p10())
                   weak:
                    +(p5(),p2()) -> +(p2(),p5())
                    +(p5(),p1()) -> +(p1(),p5())
                    +(p2(),p1()) -> +(p1(),p2())
                    +(+(x,y),z) -> +(x,+(y,z))
                    +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
                    +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
                    +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
                    +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
                    +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
                    +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
                    +(p5(),p5()) -> p10()
                    +(p5(),+(p5(),x)) -> +(p10(),x)
                    +(p1(),p1()) -> p2()
                    +(p1(),+(p1(),x)) -> +(p2(),x)
                    +(p1(),+(p2(),p2())) -> p5()
                    +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
                    +(p2(),+(p2(),p2())) -> +(p1(),p5())
                    +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
                  Bounds Processor:
                   bound: 1
                   enrichment: match
                   automaton:
                    final states: {5}
                    transitions:
                     +1(7,6) -> 5*
                     p11() -> 7*
                     p101() -> 6*
                     +0(3,1) -> 5*
                     +0(3,3) -> 5*
                     +0(4,2) -> 5*
                     +0(4,4) -> 5*
                     +0(1,2) -> 5*
                     +0(1,4) -> 5*
                     +0(2,1) -> 5*
                     +0(2,3) -> 5*
                     +0(3,2) -> 5*
                     +0(3,4) -> 5*
                     +0(4,1) -> 5*
                     +0(4,3) -> 5*
                     +0(1,1) -> 5*
                     +0(1,3) -> 5*
                     +0(2,2) -> 5*
                     +0(2,4) -> 5*
                     p20() -> 5,3
                     p10() -> 2*
                     p50() -> 4*
                     p100() -> 5,1
                   problem:
                    strict:
                     +(p10(),p2()) -> +(p2(),p10())
                     +(p10(),p5()) -> +(p5(),p10())
                    weak:
                     +(p10(),p1()) -> +(p1(),p10())
                     +(p5(),p2()) -> +(p2(),p5())
                     +(p5(),p1()) -> +(p1(),p5())
                     +(p2(),p1()) -> +(p1(),p2())
                     +(+(x,y),z) -> +(x,+(y,z))
                     +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
                     +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
                     +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
                     +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
                     +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
                     +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
                     +(p5(),p5()) -> p10()
                     +(p5(),+(p5(),x)) -> +(p10(),x)
                     +(p1(),p1()) -> p2()
                     +(p1(),+(p1(),x)) -> +(p2(),x)
                     +(p1(),+(p2(),p2())) -> p5()
                     +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
                     +(p2(),+(p2(),p2())) -> +(p1(),p5())
                     +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
                   Bounds Processor:
                    bound: 1
                    enrichment: match
                    automaton:
                     final states: {5}
                     transitions:
                      +1(7,6) -> 5*
                      p21() -> 7*
                      p101() -> 6*
                      +0(3,1) -> 5*
                      +0(3,3) -> 5*
                      +0(4,2) -> 5*
                      +0(4,4) -> 5*
                      +0(1,2) -> 5*
                      +0(1,4) -> 5*
                      +0(2,1) -> 5*
                      +0(2,3) -> 5*
                      +0(3,2) -> 5*
                      +0(3,4) -> 5*
                      +0(4,1) -> 5*
                      +0(4,3) -> 5*
                      +0(1,1) -> 5*
                      +0(1,3) -> 5*
                      +0(2,2) -> 5*
                      +0(2,4) -> 5*
                      p20() -> 5,2
                      p10() -> 4*
                      p50() -> 3*
                      p100() -> 5,1
                    problem:
                     strict:
                      +(p10(),p5()) -> +(p5(),p10())
                     weak:
                      +(p10(),p2()) -> +(p2(),p10())
                      +(p10(),p1()) -> +(p1(),p10())
                      +(p5(),p2()) -> +(p2(),p5())
                      +(p5(),p1()) -> +(p1(),p5())
                      +(p2(),p1()) -> +(p1(),p2())
                      +(+(x,y),z) -> +(x,+(y,z))
                      +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
                      +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
                      +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
                      +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
                      +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
                      +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
                      +(p5(),p5()) -> p10()
                      +(p5(),+(p5(),x)) -> +(p10(),x)
                      +(p1(),p1()) -> p2()
                      +(p1(),+(p1(),x)) -> +(p2(),x)
                      +(p1(),+(p2(),p2())) -> p5()
                      +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
                      +(p2(),+(p2(),p2())) -> +(p1(),p5())
                      +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
                    Bounds Processor:
                     bound: 1
                     enrichment: match
                     automaton:
                      final states: {5}
                      transitions:
                       +1(7,6) -> 5*
                       p51() -> 7*
                       p101() -> 6*
                       +0(3,1) -> 5*
                       +0(3,3) -> 5*
                       +0(4,2) -> 5*
                       +0(4,4) -> 5*
                       +0(1,2) -> 5*
                       +0(1,4) -> 5*
                       +0(2,1) -> 5*
                       +0(2,3) -> 5*
                       +0(3,2) -> 5*
                       +0(3,4) -> 5*
                       +0(4,1) -> 5*
                       +0(4,3) -> 5*
                       +0(1,1) -> 5*
                       +0(1,3) -> 5*
                       +0(2,2) -> 5*
                       +0(2,4) -> 5*
                       p20() -> 5,3
                       p10() -> 4*
                       p50() -> 2*
                       p100() -> 5,1
                     problem:
                      strict:
                       
                      weak:
                       +(p10(),p5()) -> +(p5(),p10())
                       +(p10(),p2()) -> +(p2(),p10())
                       +(p10(),p1()) -> +(p1(),p10())
                       +(p5(),p2()) -> +(p2(),p5())
                       +(p5(),p1()) -> +(p1(),p5())
                       +(p2(),p1()) -> +(p1(),p2())
                       +(+(x,y),z) -> +(x,+(y,z))
                       +(p2(),+(p1(),x)) -> +(p1(),+(p2(),x))
                       +(p5(),+(p1(),x)) -> +(p1(),+(p5(),x))
                       +(p5(),+(p2(),x)) -> +(p2(),+(p5(),x))
                       +(p10(),+(p1(),x)) -> +(p1(),+(p10(),x))
                       +(p10(),+(p2(),x)) -> +(p2(),+(p10(),x))
                       +(p10(),+(p5(),x)) -> +(p5(),+(p10(),x))
                       +(p5(),p5()) -> p10()
                       +(p5(),+(p5(),x)) -> +(p10(),x)
                       +(p1(),p1()) -> p2()
                       +(p1(),+(p1(),x)) -> +(p2(),x)
                       +(p1(),+(p2(),p2())) -> p5()
                       +(p1(),+(p2(),+(p2(),x))) -> +(p5(),x)
                       +(p2(),+(p2(),p2())) -> +(p1(),p5())
                       +(p2(),+(p2(),+(p2(),x))) -> +(p1(),+(p5(),x))
                     Qed