MAYBE

Problem:
 t(N) -> cs(r(q(N)),nt(ns(N)))
 q(0()) -> 0()
 q(s(X)) -> s(p(q(X),d(X)))
 d(0()) -> 0()
 d(s(X)) -> s(s(d(X)))
 p(0(),X) -> X
 p(X,0()) -> X
 p(s(X),s(Y)) -> s(s(p(X,Y)))
 f(0(),X) -> nil()
 f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z)))
 t(X) -> nt(X)
 s(X) -> ns(X)
 f(X1,X2) -> nf(X1,X2)
 a(nt(X)) -> t(a(X))
 a(ns(X)) -> s(a(X))
 a(nf(X1,X2)) -> f(a(X1),a(X2))
 a(X) -> X

Proof:
 DP Processor:
  DPs:
   t#(N) -> q#(N)
   q#(s(X)) -> d#(X)
   q#(s(X)) -> q#(X)
   q#(s(X)) -> p#(q(X),d(X))
   q#(s(X)) -> s#(p(q(X),d(X)))
   d#(s(X)) -> d#(X)
   d#(s(X)) -> s#(d(X))
   d#(s(X)) -> s#(s(d(X)))
   p#(s(X),s(Y)) -> p#(X,Y)
   p#(s(X),s(Y)) -> s#(p(X,Y))
   p#(s(X),s(Y)) -> s#(s(p(X,Y)))
   f#(s(X),cs(Y,Z)) -> a#(Z)
   a#(nt(X)) -> a#(X)
   a#(nt(X)) -> t#(a(X))
   a#(ns(X)) -> a#(X)
   a#(ns(X)) -> s#(a(X))
   a#(nf(X1,X2)) -> a#(X2)
   a#(nf(X1,X2)) -> a#(X1)
   a#(nf(X1,X2)) -> f#(a(X1),a(X2))
  TRS:
   t(N) -> cs(r(q(N)),nt(ns(N)))
   q(0()) -> 0()
   q(s(X)) -> s(p(q(X),d(X)))
   d(0()) -> 0()
   d(s(X)) -> s(s(d(X)))
   p(0(),X) -> X
   p(X,0()) -> X
   p(s(X),s(Y)) -> s(s(p(X,Y)))
   f(0(),X) -> nil()
   f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z)))
   t(X) -> nt(X)
   s(X) -> ns(X)
   f(X1,X2) -> nf(X1,X2)
   a(nt(X)) -> t(a(X))
   a(ns(X)) -> s(a(X))
   a(nf(X1,X2)) -> f(a(X1),a(X2))
   a(X) -> X
  ADG Processor:
   DPs:
    t#(N) -> q#(N)
    q#(s(X)) -> d#(X)
    q#(s(X)) -> q#(X)
    q#(s(X)) -> p#(q(X),d(X))
    q#(s(X)) -> s#(p(q(X),d(X)))
    d#(s(X)) -> d#(X)
    d#(s(X)) -> s#(d(X))
    d#(s(X)) -> s#(s(d(X)))
    p#(s(X),s(Y)) -> p#(X,Y)
    p#(s(X),s(Y)) -> s#(p(X,Y))
    p#(s(X),s(Y)) -> s#(s(p(X,Y)))
    f#(s(X),cs(Y,Z)) -> a#(Z)
    a#(nt(X)) -> a#(X)
    a#(nt(X)) -> t#(a(X))
    a#(ns(X)) -> a#(X)
    a#(ns(X)) -> s#(a(X))
    a#(nf(X1,X2)) -> a#(X2)
    a#(nf(X1,X2)) -> a#(X1)
    a#(nf(X1,X2)) -> f#(a(X1),a(X2))
   TRS:
    t(N) -> cs(r(q(N)),nt(ns(N)))
    q(0()) -> 0()
    q(s(X)) -> s(p(q(X),d(X)))
    d(0()) -> 0()
    d(s(X)) -> s(s(d(X)))
    p(0(),X) -> X
    p(X,0()) -> X
    p(s(X),s(Y)) -> s(s(p(X,Y)))
    f(0(),X) -> nil()
    f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z)))
    t(X) -> nt(X)
    s(X) -> ns(X)
    f(X1,X2) -> nf(X1,X2)
    a(nt(X)) -> t(a(X))
    a(ns(X)) -> s(a(X))
    a(nf(X1,X2)) -> f(a(X1),a(X2))
    a(X) -> X
   graph:
    a#(nf(X1,X2)) -> a#(X2) -> a#(nt(X)) -> a#(X)
    a#(nf(X1,X2)) -> a#(X2) -> a#(nt(X)) -> t#(a(X))
    a#(nf(X1,X2)) -> a#(X2) -> a#(ns(X)) -> a#(X)
    a#(nf(X1,X2)) -> a#(X2) -> a#(ns(X)) -> s#(a(X))
    a#(nf(X1,X2)) -> a#(X2) -> a#(nf(X1,X2)) -> a#(X2)
    a#(nf(X1,X2)) -> a#(X2) -> a#(nf(X1,X2)) -> a#(X1)
    a#(nf(X1,X2)) -> a#(X2) -> a#(nf(X1,X2)) -> f#(a(X1),a(X2))
    a#(nf(X1,X2)) -> a#(X1) -> a#(nt(X)) -> a#(X)
    a#(nf(X1,X2)) -> a#(X1) -> a#(nt(X)) -> t#(a(X))
    a#(nf(X1,X2)) -> a#(X1) -> a#(ns(X)) -> a#(X)
    a#(nf(X1,X2)) -> a#(X1) -> a#(ns(X)) -> s#(a(X))
    a#(nf(X1,X2)) -> a#(X1) -> a#(nf(X1,X2)) -> a#(X2)
    a#(nf(X1,X2)) -> a#(X1) -> a#(nf(X1,X2)) -> a#(X1)
    a#(nf(X1,X2)) -> a#(X1) -> a#(nf(X1,X2)) -> f#(a(X1),a(X2))
    a#(nf(X1,X2)) -> f#(a(X1),a(X2)) -> f#(s(X),cs(Y,Z)) -> a#(Z)
    a#(nt(X)) -> a#(X) -> a#(nt(X)) -> a#(X)
    a#(nt(X)) -> a#(X) -> a#(nt(X)) -> t#(a(X))
    a#(nt(X)) -> a#(X) -> a#(ns(X)) -> a#(X)
    a#(nt(X)) -> a#(X) -> a#(ns(X)) -> s#(a(X))
    a#(nt(X)) -> a#(X) -> a#(nf(X1,X2)) -> a#(X2)
    a#(nt(X)) -> a#(X) -> a#(nf(X1,X2)) -> a#(X1)
    a#(nt(X)) -> a#(X) -> a#(nf(X1,X2)) -> f#(a(X1),a(X2))
    a#(nt(X)) -> t#(a(X)) -> t#(N) -> q#(N)
    a#(ns(X)) -> a#(X) -> a#(nt(X)) -> a#(X)
    a#(ns(X)) -> a#(X) -> a#(nt(X)) -> t#(a(X))
    a#(ns(X)) -> a#(X) -> a#(ns(X)) -> a#(X)
    a#(ns(X)) -> a#(X) -> a#(ns(X)) -> s#(a(X))
    a#(ns(X)) -> a#(X) -> a#(nf(X1,X2)) -> a#(X2)
    a#(ns(X)) -> a#(X) -> a#(nf(X1,X2)) -> a#(X1)
    a#(ns(X)) -> a#(X) -> a#(nf(X1,X2)) -> f#(a(X1),a(X2))
    f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(nt(X)) -> a#(X)
    f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(nt(X)) -> t#(a(X))
    f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(ns(X)) -> a#(X)
    f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(ns(X)) -> s#(a(X))
    f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(nf(X1,X2)) -> a#(X2)
    f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(nf(X1,X2)) -> a#(X1)
    f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(nf(X1,X2)) -> f#(a(X1),a(X2))
    p#(s(X),s(Y)) -> p#(X,Y) -> p#(s(X),s(Y)) -> p#(X,Y)
    p#(s(X),s(Y)) -> p#(X,Y) -> p#(s(X),s(Y)) -> s#(p(X,Y))
    p#(s(X),s(Y)) -> p#(X,Y) -> p#(s(X),s(Y)) -> s#(s(p(X,Y)))
    d#(s(X)) -> d#(X) -> d#(s(X)) -> d#(X)
    d#(s(X)) -> d#(X) -> d#(s(X)) -> s#(d(X))
    d#(s(X)) -> d#(X) -> d#(s(X)) -> s#(s(d(X)))
    q#(s(X)) -> p#(q(X),d(X)) -> p#(s(X),s(Y)) -> p#(X,Y)
    q#(s(X)) -> p#(q(X),d(X)) -> p#(s(X),s(Y)) -> s#(p(X,Y))
    q#(s(X)) -> p#(q(X),d(X)) -> p#(s(X),s(Y)) -> s#(s(p(X,Y)))
    q#(s(X)) -> d#(X) -> d#(s(X)) -> d#(X)
    q#(s(X)) -> d#(X) -> d#(s(X)) -> s#(d(X))
    q#(s(X)) -> d#(X) -> d#(s(X)) -> s#(s(d(X)))
    q#(s(X)) -> q#(X) -> q#(s(X)) -> d#(X)
    q#(s(X)) -> q#(X) -> q#(s(X)) -> q#(X)
    q#(s(X)) -> q#(X) -> q#(s(X)) -> p#(q(X),d(X))
    q#(s(X)) -> q#(X) -> q#(s(X)) -> s#(p(q(X),d(X)))
    t#(N) -> q#(N) -> q#(s(X)) -> d#(X)
    t#(N) -> q#(N) -> q#(s(X)) -> q#(X)
    t#(N) -> q#(N) -> q#(s(X)) -> p#(q(X),d(X))
    t#(N) -> q#(N) -> q#(s(X)) -> s#(p(q(X),d(X)))
   SCC Processor:
    #sccs: 4
    #rules: 9
    #arcs: 57/361
    DPs:
     a#(nf(X1,X2)) -> a#(X2)
     a#(nf(X1,X2)) -> f#(a(X1),a(X2))
     f#(s(X),cs(Y,Z)) -> a#(Z)
     a#(nf(X1,X2)) -> a#(X1)
     a#(ns(X)) -> a#(X)
     a#(nt(X)) -> a#(X)
    TRS:
     t(N) -> cs(r(q(N)),nt(ns(N)))
     q(0()) -> 0()
     q(s(X)) -> s(p(q(X),d(X)))
     d(0()) -> 0()
     d(s(X)) -> s(s(d(X)))
     p(0(),X) -> X
     p(X,0()) -> X
     p(s(X),s(Y)) -> s(s(p(X,Y)))
     f(0(),X) -> nil()
     f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z)))
     t(X) -> nt(X)
     s(X) -> ns(X)
     f(X1,X2) -> nf(X1,X2)
     a(nt(X)) -> t(a(X))
     a(ns(X)) -> s(a(X))
     a(nf(X1,X2)) -> f(a(X1),a(X2))
     a(X) -> X
    Open
    
    DPs:
     q#(s(X)) -> q#(X)
    TRS:
     t(N) -> cs(r(q(N)),nt(ns(N)))
     q(0()) -> 0()
     q(s(X)) -> s(p(q(X),d(X)))
     d(0()) -> 0()
     d(s(X)) -> s(s(d(X)))
     p(0(),X) -> X
     p(X,0()) -> X
     p(s(X),s(Y)) -> s(s(p(X,Y)))
     f(0(),X) -> nil()
     f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z)))
     t(X) -> nt(X)
     s(X) -> ns(X)
     f(X1,X2) -> nf(X1,X2)
     a(nt(X)) -> t(a(X))
     a(ns(X)) -> s(a(X))
     a(nf(X1,X2)) -> f(a(X1),a(X2))
     a(X) -> X
    Open
    
    DPs:
     d#(s(X)) -> d#(X)
    TRS:
     t(N) -> cs(r(q(N)),nt(ns(N)))
     q(0()) -> 0()
     q(s(X)) -> s(p(q(X),d(X)))
     d(0()) -> 0()
     d(s(X)) -> s(s(d(X)))
     p(0(),X) -> X
     p(X,0()) -> X
     p(s(X),s(Y)) -> s(s(p(X,Y)))
     f(0(),X) -> nil()
     f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z)))
     t(X) -> nt(X)
     s(X) -> ns(X)
     f(X1,X2) -> nf(X1,X2)
     a(nt(X)) -> t(a(X))
     a(ns(X)) -> s(a(X))
     a(nf(X1,X2)) -> f(a(X1),a(X2))
     a(X) -> X
    Open
    
    DPs:
     p#(s(X),s(Y)) -> p#(X,Y)
    TRS:
     t(N) -> cs(r(q(N)),nt(ns(N)))
     q(0()) -> 0()
     q(s(X)) -> s(p(q(X),d(X)))
     d(0()) -> 0()
     d(s(X)) -> s(s(d(X)))
     p(0(),X) -> X
     p(X,0()) -> X
     p(s(X),s(Y)) -> s(s(p(X,Y)))
     f(0(),X) -> nil()
     f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z)))
     t(X) -> nt(X)
     s(X) -> ns(X)
     f(X1,X2) -> nf(X1,X2)
     a(nt(X)) -> t(a(X))
     a(ns(X)) -> s(a(X))
     a(nf(X1,X2)) -> f(a(X1),a(X2))
     a(X) -> X
    Open