MAYBE

Problem:
 b(b(0(),y),x) -> y
 c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
 a(y,0()) -> b(y,0())

Proof:
 DP Processor:
  DPs:
   c#(c(c(y))) -> b#(0(),y)
   c#(c(c(y))) -> c#(b(0(),y))
   c#(c(c(y))) -> a#(c(b(0(),y)),0())
   c#(c(c(y))) -> a#(a(c(b(0(),y)),0()),0())
   c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0()))
   c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
   a#(y,0()) -> b#(y,0())
  TRS:
   b(b(0(),y),x) -> y
   c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
   a(y,0()) -> b(y,0())
  EDG Processor:
   DPs:
    c#(c(c(y))) -> b#(0(),y)
    c#(c(c(y))) -> c#(b(0(),y))
    c#(c(c(y))) -> a#(c(b(0(),y)),0())
    c#(c(c(y))) -> a#(a(c(b(0(),y)),0()),0())
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0()))
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
    a#(y,0()) -> b#(y,0())
   TRS:
    b(b(0(),y),x) -> y
    c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
    a(y,0()) -> b(y,0())
   graph:
    c#(c(c(y))) -> a#(a(c(b(0(),y)),0()),0()) ->
    a#(y,0()) -> b#(y,0())
    c#(c(c(y))) -> a#(c(b(0(),y)),0()) ->
    a#(y,0()) -> b#(y,0())
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> b#(0(),y)
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> c#(b(0(),y))
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> a#(c(b(0(),y)),0())
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> a#(a(c(b(0(),y)),0()),0())
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0()))
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0())) ->
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0()))) ->
    c#(c(c(y))) -> b#(0(),y)
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0()))) ->
    c#(c(c(y))) -> c#(b(0(),y))
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0()))) ->
    c#(c(c(y))) -> a#(c(b(0(),y)),0())
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0()))) ->
    c#(c(c(y))) -> a#(a(c(b(0(),y)),0()),0())
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0()))) ->
    c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0()))
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0()))) ->
    c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 14/49
    DPs:
     c#(c(c(y))) -> c#(a(a(c(b(0(),y)),0()),0()))
     c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
    TRS:
     b(b(0(),y),x) -> y
     c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
     a(y,0()) -> b(y,0())
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [c#](x0) = x0,
      
      [a](x0, x1) = x0,
      
      [c](x0) = x0 + 1,
      
      [b](x0, x1) = x0 + x1,
      
      [0] = 0
     orientation:
      c#(c(c(y))) = y + 2 >= y + 1 = c#(a(a(c(b(0(),y)),0()),0()))
      
      c#(c(c(y))) = y + 2 >= y + 2 = c#(c(a(a(c(b(0(),y)),0()),0())))
      
      b(b(0(),y),x) = x + y >= y = y
      
      c(c(c(y))) = y + 3 >= y + 3 = c(c(a(a(c(b(0(),y)),0()),0())))
      
      a(y,0()) = y >= y = b(y,0())
     problem:
      DPs:
       c#(c(c(y))) -> c#(c(a(a(c(b(0(),y)),0()),0())))
      TRS:
       b(b(0(),y),x) -> y
       c(c(c(y))) -> c(c(a(a(c(b(0(),y)),0()),0())))
       a(y,0()) -> b(y,0())
     Open