MAYBE

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

Proof:
 DP Processor:
  DPs:
   c#(a(c(c(y)),x)) -> a#(x,0())
   c#(a(c(c(y)),x)) -> c#(a(x,0()))
   c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
   c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
   c#(a(c(c(y)),x)) -> a#(c(c(c(a(x,0())))),y)
  TRS:
   a(a(y,0()),0()) -> y
   c(c(y)) -> y
   c(a(c(c(y)),x)) -> a(c(c(c(a(x,0())))),y)
  TDG Processor:
   DPs:
    c#(a(c(c(y)),x)) -> a#(x,0())
    c#(a(c(c(y)),x)) -> c#(a(x,0()))
    c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
    c#(a(c(c(y)),x)) -> a#(c(c(c(a(x,0())))),y)
   TRS:
    a(a(y,0()),0()) -> y
    c(c(y)) -> y
    c(a(c(c(y)),x)) -> a(c(c(c(a(x,0())))),y)
   graph:
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0())))) ->
    c#(a(c(c(y)),x)) -> a#(c(c(c(a(x,0())))),y)
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0())))) ->
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0())))) ->
    c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0())))) ->
    c#(a(c(c(y)),x)) -> c#(a(x,0()))
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0())))) ->
    c#(a(c(c(y)),x)) -> a#(x,0())
    c#(a(c(c(y)),x)) -> c#(c(a(x,0()))) ->
    c#(a(c(c(y)),x)) -> a#(c(c(c(a(x,0())))),y)
    c#(a(c(c(y)),x)) -> c#(c(a(x,0()))) ->
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
    c#(a(c(c(y)),x)) -> c#(c(a(x,0()))) ->
    c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
    c#(a(c(c(y)),x)) -> c#(c(a(x,0()))) ->
    c#(a(c(c(y)),x)) -> c#(a(x,0()))
    c#(a(c(c(y)),x)) -> c#(c(a(x,0()))) ->
    c#(a(c(c(y)),x)) -> a#(x,0())
    c#(a(c(c(y)),x)) -> c#(a(x,0())) ->
    c#(a(c(c(y)),x)) -> a#(c(c(c(a(x,0())))),y)
    c#(a(c(c(y)),x)) -> c#(a(x,0())) ->
    c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
    c#(a(c(c(y)),x)) -> c#(a(x,0())) ->
    c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
    c#(a(c(c(y)),x)) -> c#(a(x,0())) ->
    c#(a(c(c(y)),x)) -> c#(a(x,0()))
    c#(a(c(c(y)),x)) -> c#(a(x,0())) -> c#(a(c(c(y)),x)) -> a#(x,0())
   Restore Modifier:
    DPs:
     c#(a(c(c(y)),x)) -> a#(x,0())
     c#(a(c(c(y)),x)) -> c#(a(x,0()))
     c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
     c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
     c#(a(c(c(y)),x)) -> a#(c(c(c(a(x,0())))),y)
    TRS:
     a(a(y,0()),0()) -> y
     c(c(y)) -> y
     c(a(c(c(y)),x)) -> a(c(c(c(a(x,0())))),y)
    SCC Processor:
     #sccs: 1
     #rules: 3
     #arcs: 15/25
     DPs:
      c#(a(c(c(y)),x)) -> c#(c(c(a(x,0()))))
      c#(a(c(c(y)),x)) -> c#(a(x,0()))
      c#(a(c(c(y)),x)) -> c#(c(a(x,0())))
     TRS:
      a(a(y,0()),0()) -> y
      c(c(y)) -> y
      c(a(c(c(y)),x)) -> a(c(c(c(a(x,0())))),y)
     Open