MAYBE

Problem:
 f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) ->
 f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))))))

Proof:
 Uncurry Processor:
  a1(a1(b1(a1(a1(b1(a1(x))))))) -> a1(b1(a1(a1(b1(a1(a1(a1(b1(x)))))))))
  f(a(),x1) -> a1(x1)
  f(b(),x1) -> b1(x1)
  Matrix Interpretation Processor: dim=3
   
   interpretation:
               [1 0 0]     [0]
    [b1](x0) = [0 0 1]x0 + [0]
               [0 0 0]     [1],
    
               [1 0 0]  
    [a1](x0) = [1 0 0]x0
               [0 0 0]  ,
    
                  [1 0 0]     [1 1 1]     [1]
    [f](x0, x1) = [0 0 0]x0 + [1 1 1]x1 + [0]
                  [0 0 1]     [0 1 0]     [0],
    
          [0]
    [b] = [0]
          [1],
    
          [0]
    [a] = [0]
          [0]
   orientation:
                                    [1 0 0]     [1 0 0]                                         
    a1(a1(b1(a1(a1(b1(a1(x))))))) = [1 0 0]x >= [1 0 0]x = a1(b1(a1(a1(b1(a1(a1(a1(b1(x)))))))))
                                    [0 0 0]     [0 0 0]                                         
    
                [1 1 1]     [1]    [1 0 0]           
    f(a(),x1) = [1 1 1]x1 + [0] >= [1 0 0]x1 = a1(x1)
                [0 1 0]     [0]    [0 0 0]           
    
                [1 1 1]     [1]    [1 0 0]     [0]         
    f(b(),x1) = [1 1 1]x1 + [0] >= [0 0 1]x1 + [0] = b1(x1)
                [0 1 0]     [1]    [0 0 0]     [1]         
   problem:
    a1(a1(b1(a1(a1(b1(a1(x))))))) -> a1(b1(a1(a1(b1(a1(a1(a1(b1(x)))))))))
   DP Processor:
    DPs:
     a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(x))
     a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(x)))
     a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(a1(b1(x))))
     a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(a1(a1(a1(b1(x))))))
     a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(a1(a1(a1(b1(x)))))))
     a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(a1(a1(b1(a1(a1(a1(b1(x)))))))))
    TRS:
     a1(a1(b1(a1(a1(b1(a1(x))))))) -> a1(b1(a1(a1(b1(a1(a1(a1(b1(x)))))))))
    EDG Processor:
     DPs:
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(x))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(x)))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(a1(b1(x))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(a1(a1(a1(b1(x))))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(a1(a1(a1(b1(x)))))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(a1(a1(b1(a1(a1(a1(b1(x)))))))))
     TRS:
      a1(a1(b1(a1(a1(b1(a1(x))))))) -> a1(b1(a1(a1(b1(a1(a1(a1(b1(x)))))))))
     graph:
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(a1(a1(a1(b1(x))))))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(x))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(a1(a1(a1(b1(x))))))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(x)))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(a1(a1(a1(b1(x))))))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(a1(b1(x))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(a1(a1(a1(b1(x))))))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(a1(a1(a1(b1(x))))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(a1(a1(a1(b1(x))))))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(a1(a1(a1(b1(x)))))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(a1(a1(a1(b1(x))))))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(a1(a1(b1(a1(a1(a1(b1(x)))))))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(x))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(x))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(x))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(x)))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(x))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(a1(b1(x))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(x))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(a1(a1(a1(b1(x))))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(x))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(a1(a1(a1(b1(x)))))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(x))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(a1(a1(b1(a1(a1(a1(b1(x)))))))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(a1(b1(x)))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(x))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(a1(b1(x)))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(x)))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(a1(b1(x)))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(a1(b1(x))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(a1(b1(x)))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(a1(a1(a1(b1(x))))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(a1(b1(x)))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(a1(a1(a1(b1(x)))))))
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(a1(b1(x)))) ->
      a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(b1(a1(a1(b1(a1(a1(a1(b1(x)))))))))
     SCC Processor:
      #sccs: 1
      #rules: 3
      #arcs: 18/36
      DPs:
       a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(a1(a1(a1(b1(x)))))))
       a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(a1(b1(x))))
       a{1,#}(a1(b1(a1(a1(b1(a1(x))))))) -> a{1,#}(a1(b1(x)))
      TRS:
       a1(a1(b1(a1(a1(b1(a1(x))))))) -> a1(b1(a1(a1(b1(a1(a1(a1(b1(x)))))))))
      Open