MAYBE

Problem:
 *(X,+(Y,1())) -> +(*(X,+(Y,*(1(),0()))),X)
 *(X,1()) -> X
 *(X,0()) -> X
 *(X,0()) -> 0()

Proof:
 DP Processor:
  DPs:
   *#(X,+(Y,1())) -> *#(1(),0())
   *#(X,+(Y,1())) -> *#(X,+(Y,*(1(),0())))
  TRS:
   *(X,+(Y,1())) -> +(*(X,+(Y,*(1(),0()))),X)
   *(X,1()) -> X
   *(X,0()) -> X
   *(X,0()) -> 0()
  SCC Processor:
   #sccs: 1
   #rules: 2
   #arcs: 4/4
   DPs:
    *#(X,+(Y,1())) -> *#(1(),0())
    *#(X,+(Y,1())) -> *#(X,+(Y,*(1(),0())))
   TRS:
    *(X,+(Y,1())) -> +(*(X,+(Y,*(1(),0()))),X)
    *(X,1()) -> X
    *(X,0()) -> X
    *(X,0()) -> 0()
   Matrix Interpretation Processor:
    dimension: 1
    interpretation:
     [*#](x0, x1) = x1,
     
     [0] = 0,
     
     [*](x0, x1) = x0,
     
     [+](x0, x1) = x1,
     
     [1] = 1
    orientation:
     *#(X,+(Y,1())) = 1 >= 0 = *#(1(),0())
     
     *#(X,+(Y,1())) = 1 >= 1 = *#(X,+(Y,*(1(),0())))
     
     *(X,+(Y,1())) = X >= X = +(*(X,+(Y,*(1(),0()))),X)
     
     *(X,1()) = X >= X = X
     
     *(X,0()) = X >= X = X
     
     *(X,0()) = X >= 0 = 0()
    problem:
     DPs:
      *#(X,+(Y,1())) -> *#(X,+(Y,*(1(),0())))
     TRS:
      *(X,+(Y,1())) -> +(*(X,+(Y,*(1(),0()))),X)
      *(X,1()) -> X
      *(X,0()) -> X
      *(X,0()) -> 0()
    Open