YES

Problem:
 plus(x,0()) -> x
 plus(0(),y) -> y
 plus(s(x),y) -> s(plus(x,y))
 times(0(),y) -> 0()
 times(s(0()),y) -> y
 times(s(x),y) -> plus(y,times(x,y))
 div(0(),y) -> 0()
 div(x,y) -> quot(x,y,y)
 quot(0(),s(y),z) -> 0()
 quot(s(x),s(y),z) -> quot(x,y,z)
 quot(x,0(),s(z)) -> s(div(x,s(z)))
 div(div(x,y),z) -> div(x,times(y,z))

Proof:
 DP Processor:
  DPs:
   plus#(s(x),y) -> plus#(x,y)
   times#(s(x),y) -> times#(x,y)
   times#(s(x),y) -> plus#(y,times(x,y))
   div#(x,y) -> quot#(x,y,y)
   quot#(s(x),s(y),z) -> quot#(x,y,z)
   quot#(x,0(),s(z)) -> div#(x,s(z))
   div#(div(x,y),z) -> times#(y,z)
   div#(div(x,y),z) -> div#(x,times(y,z))
  TRS:
   plus(x,0()) -> x
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(x,y))
   times(0(),y) -> 0()
   times(s(0()),y) -> y
   times(s(x),y) -> plus(y,times(x,y))
   div(0(),y) -> 0()
   div(x,y) -> quot(x,y,y)
   quot(0(),s(y),z) -> 0()
   quot(s(x),s(y),z) -> quot(x,y,z)
   quot(x,0(),s(z)) -> s(div(x,s(z)))
   div(div(x,y),z) -> div(x,times(y,z))
  EDG Processor:
   DPs:
    plus#(s(x),y) -> plus#(x,y)
    times#(s(x),y) -> times#(x,y)
    times#(s(x),y) -> plus#(y,times(x,y))
    div#(x,y) -> quot#(x,y,y)
    quot#(s(x),s(y),z) -> quot#(x,y,z)
    quot#(x,0(),s(z)) -> div#(x,s(z))
    div#(div(x,y),z) -> times#(y,z)
    div#(div(x,y),z) -> div#(x,times(y,z))
   TRS:
    plus(x,0()) -> x
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(x,y))
    times(0(),y) -> 0()
    times(s(0()),y) -> y
    times(s(x),y) -> plus(y,times(x,y))
    div(0(),y) -> 0()
    div(x,y) -> quot(x,y,y)
    quot(0(),s(y),z) -> 0()
    quot(s(x),s(y),z) -> quot(x,y,z)
    quot(x,0(),s(z)) -> s(div(x,s(z)))
    div(div(x,y),z) -> div(x,times(y,z))
   graph:
    quot#(s(x),s(y),z) -> quot#(x,y,z) ->
    quot#(s(x),s(y),z) -> quot#(x,y,z)
    quot#(s(x),s(y),z) -> quot#(x,y,z) ->
    quot#(x,0(),s(z)) -> div#(x,s(z))
    quot#(x,0(),s(z)) -> div#(x,s(z)) -> div#(x,y) -> quot#(x,y,y)
    quot#(x,0(),s(z)) -> div#(x,s(z)) ->
    div#(div(x,y),z) -> times#(y,z)
    quot#(x,0(),s(z)) -> div#(x,s(z)) ->
    div#(div(x,y),z) -> div#(x,times(y,z))
    div#(div(x,y),z) -> div#(x,times(y,z)) ->
    div#(x,y) -> quot#(x,y,y)
    div#(div(x,y),z) -> div#(x,times(y,z)) ->
    div#(div(x,y),z) -> times#(y,z)
    div#(div(x,y),z) -> div#(x,times(y,z)) ->
    div#(div(x,y),z) -> div#(x,times(y,z))
    div#(div(x,y),z) -> times#(y,z) -> times#(s(x),y) -> times#(x,y)
    div#(div(x,y),z) -> times#(y,z) ->
    times#(s(x),y) -> plus#(y,times(x,y))
    div#(x,y) -> quot#(x,y,y) -> quot#(s(x),s(y),z) -> quot#(x,y,z)
    div#(x,y) -> quot#(x,y,y) -> quot#(x,0(),s(z)) -> div#(x,s(z))
    times#(s(x),y) -> times#(x,y) -> times#(s(x),y) -> times#(x,y)
    times#(s(x),y) -> times#(x,y) ->
    times#(s(x),y) -> plus#(y,times(x,y))
    times#(s(x),y) -> plus#(y,times(x,y)) -> plus#(s(x),y) -> plus#(x,y)
    plus#(s(x),y) -> plus#(x,y) -> plus#(s(x),y) -> plus#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 6
    #arcs: 16/64
    DPs:
     quot#(s(x),s(y),z) -> quot#(x,y,z)
     quot#(x,0(),s(z)) -> div#(x,s(z))
     div#(div(x,y),z) -> div#(x,times(y,z))
     div#(x,y) -> quot#(x,y,y)
    TRS:
     plus(x,0()) -> x
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     times(0(),y) -> 0()
     times(s(0()),y) -> y
     times(s(x),y) -> plus(y,times(x,y))
     div(0(),y) -> 0()
     div(x,y) -> quot(x,y,y)
     quot(0(),s(y),z) -> 0()
     quot(s(x),s(y),z) -> quot(x,y,z)
     quot(x,0(),s(z)) -> s(div(x,s(z)))
     div(div(x,y),z) -> div(x,times(y,z))
    Subterm Criterion Processor:
     simple projection:
      pi(div#) = 0
      pi(quot#) = 0
     problem:
      DPs:
       quot#(x,0(),s(z)) -> div#(x,s(z))
       div#(x,y) -> quot#(x,y,y)
      TRS:
       plus(x,0()) -> x
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       times(0(),y) -> 0()
       times(s(0()),y) -> y
       times(s(x),y) -> plus(y,times(x,y))
       div(0(),y) -> 0()
       div(x,y) -> quot(x,y,y)
       quot(0(),s(y),z) -> 0()
       quot(s(x),s(y),z) -> quot(x,y,z)
       quot(x,0(),s(z)) -> s(div(x,s(z)))
       div(div(x,y),z) -> div(x,times(y,z))
     Bounds Processor:
      bound: 2
      enrichment: top-dp
      automaton:
       final states: {12}
       transitions:
        div0(12,12) -> 10*
        div0(10,10) -> 10*
        div0(10,12) -> 10*
        div0(12,10) -> 10*
        quot0(12,10,10) -> 10*
        quot0(12,12,10) -> 10*
        quot0(10,10,12) -> 10*
        quot0(10,12,12) -> 10*
        quot0(12,10,12) -> 10*
        quot0(12,12,12) -> 10*
        quot0(10,10,10) -> 10*
        quot0(10,12,10) -> 10*
        div{#,1}(12,14) -> 10*
        div{#,1}(10,14) -> 12,10
        s1(10) -> 14*
        s1(12) -> 14*
        quot{#,1}(12,10,10) -> 12,10
        quot{#,1}(10,12,12) -> 10*
        quot{#,1}(12,12,12) -> 10*
        quot{#,1}(10,10,10) -> 12,10
        quot{#,2}(10,14,14) -> 12,10
        quot{#,2}(12,14,14) -> 10*
        quot{#,0}(12,10,10) -> 12*
        quot{#,0}(12,12,10) -> 12*
        quot{#,0}(10,10,12) -> 12*
        quot{#,0}(10,12,12) -> 12*
        quot{#,0}(12,10,12) -> 12*
        quot{#,0}(12,12,12) -> 12*
        quot{#,0}(10,10,10) -> 12*
        quot{#,0}(10,12,10) -> 12*
        00() -> 10*
        s0(10) -> 10*
        s0(12) -> 10*
        div{#,0}(10,10) -> 12,10
        div{#,0}(10,12) -> 10*
        div{#,0}(12,10) -> 12,10
        div{#,0}(12,12) -> 10*
        plus0(10,10) -> 10*
        plus0(10,12) -> 10*
        plus0(12,10) -> 10*
        plus0(12,12) -> 10*
        times0(12,12) -> 10*
        times0(10,10) -> 10*
        times0(10,12) -> 10*
        times0(12,10) -> 10*
        12 -> 10*
      problem:
       DPs:
        quot#(x,0(),s(z)) -> div#(x,s(z))
       TRS:
        plus(x,0()) -> x
        plus(0(),y) -> y
        plus(s(x),y) -> s(plus(x,y))
        times(0(),y) -> 0()
        times(s(0()),y) -> y
        times(s(x),y) -> plus(y,times(x,y))
        div(0(),y) -> 0()
        div(x,y) -> quot(x,y,y)
        quot(0(),s(y),z) -> 0()
        quot(s(x),s(y),z) -> quot(x,y,z)
        quot(x,0(),s(z)) -> s(div(x,s(z)))
        div(div(x,y),z) -> div(x,times(y,z))
      Bounds Processor:
       bound: 0
       enrichment: top-dp
       automaton:
        final states: {19}
        transitions:
         00() -> 17,16,15,11
         s0(15) -> 18*
         s0(17) -> 18*
         s0(19) -> 18*
         s0(14) -> 18*
         s0(16) -> 16,17,18
         s0(11) -> 18*
         s0(18) -> 18*
         s0(13) -> 18*
         div{#,0}(17,14) -> 13*
         div{#,0}(17,16) -> 13*
         div{#,0}(17,18) -> 19*
         div{#,0}(18,11) -> 13*
         div{#,0}(13,11) -> 13*
         div{#,0}(18,13) -> 13*
         div{#,0}(13,13) -> 13*
         div{#,0}(18,15) -> 13*
         div{#,0}(13,15) -> 13*
         div{#,0}(18,17) -> 13*
         div{#,0}(13,17) -> 13*
         div{#,0}(18,19) -> 13*
         div{#,0}(13,19) -> 13*
         div{#,0}(19,14) -> 13*
         div{#,0}(14,14) -> 13*
         div{#,0}(19,16) -> 13*
         div{#,0}(14,16) -> 13*
         div{#,0}(19,18) -> 19*
         div{#,0}(14,18) -> 19*
         div{#,0}(15,11) -> 13*
         div{#,0}(15,13) -> 13*
         div{#,0}(15,15) -> 13*
         div{#,0}(15,17) -> 13*
         div{#,0}(15,19) -> 13*
         div{#,0}(16,14) -> 13*
         div{#,0}(11,14) -> 13*
         div{#,0}(16,16) -> 13*
         div{#,0}(11,16) -> 13*
         div{#,0}(16,18) -> 19*
         div{#,0}(11,18) -> 19*
         div{#,0}(17,11) -> 13*
         div{#,0}(17,13) -> 13*
         div{#,0}(17,15) -> 13*
         div{#,0}(17,17) -> 13*
         div{#,0}(17,19) -> 13*
         div{#,0}(18,14) -> 13*
         div{#,0}(13,14) -> 13*
         div{#,0}(18,16) -> 13*
         div{#,0}(13,16) -> 13*
         div{#,0}(18,18) -> 19*
         div{#,0}(13,18) -> 19*
         div{#,0}(19,11) -> 13*
         div{#,0}(14,11) -> 13*
         div{#,0}(19,13) -> 13*
         div{#,0}(14,13) -> 13*
         div{#,0}(19,15) -> 13*
         div{#,0}(14,15) -> 13*
         div{#,0}(19,17) -> 13*
         div{#,0}(14,17) -> 13*
         div{#,0}(19,19) -> 13*
         div{#,0}(14,19) -> 13*
         div{#,0}(15,14) -> 13*
         div{#,0}(15,16) -> 13*
         div{#,0}(15,18) -> 19*
         div{#,0}(16,11) -> 13*
         div{#,0}(11,11) -> 13*
         div{#,0}(16,13) -> 13*
         div{#,0}(11,13) -> 13*
         div{#,0}(16,15) -> 13*
         div{#,0}(11,15) -> 13*
         div{#,0}(16,17) -> 13*
         div{#,0}(11,17) -> 13*
         div{#,0}(16,19) -> 13*
         div{#,0}(11,19) -> 13*
         plus0(17,14) -> 14*
         plus0(17,16) -> 14*
         plus0(17,18) -> 14*
         plus0(18,11) -> 14*
         plus0(13,11) -> 14*
         plus0(18,13) -> 14*
         plus0(13,13) -> 14*
         plus0(18,15) -> 14*
         plus0(13,15) -> 14*
         plus0(18,17) -> 14*
         plus0(13,17) -> 14*
         plus0(18,19) -> 14*
         plus0(13,19) -> 14*
         plus0(19,14) -> 14*
         plus0(14,14) -> 14*
         plus0(19,16) -> 14*
         plus0(14,16) -> 14*
         plus0(19,18) -> 14*
         plus0(14,18) -> 14*
         plus0(15,11) -> 14*
         plus0(15,13) -> 14*
         plus0(15,15) -> 14*
         plus0(15,17) -> 14*
         plus0(15,19) -> 14*
         plus0(16,14) -> 14*
         plus0(11,14) -> 14*
         plus0(16,16) -> 14*
         plus0(11,16) -> 14*
         plus0(16,18) -> 14*
         plus0(11,18) -> 14*
         plus0(17,11) -> 14*
         plus0(17,13) -> 14*
         plus0(17,15) -> 14*
         plus0(17,17) -> 14*
         plus0(17,19) -> 14*
         plus0(18,14) -> 14*
         plus0(13,14) -> 14*
         plus0(18,16) -> 14*
         plus0(13,16) -> 14*
         plus0(18,18) -> 14*
         plus0(13,18) -> 14*
         plus0(19,11) -> 14*
         plus0(14,11) -> 14*
         plus0(19,13) -> 14*
         plus0(14,13) -> 14*
         plus0(19,15) -> 14*
         plus0(14,15) -> 14*
         plus0(19,17) -> 14*
         plus0(14,17) -> 14*
         plus0(19,19) -> 14*
         plus0(14,19) -> 14*
         plus0(15,14) -> 14*
         plus0(15,16) -> 14*
         plus0(15,18) -> 14*
         plus0(16,11) -> 14*
         plus0(11,11) -> 14*
         plus0(16,13) -> 14*
         plus0(11,13) -> 14*
         plus0(16,15) -> 14*
         plus0(11,15) -> 14*
         plus0(16,17) -> 14*
         plus0(11,17) -> 14*
         plus0(16,19) -> 14*
         plus0(11,19) -> 14*
         times0(17,14) -> 15*
         times0(17,16) -> 15*
         times0(17,18) -> 15*
         times0(18,11) -> 15*
         times0(13,11) -> 15*
         times0(18,13) -> 15*
         times0(13,13) -> 15*
         times0(18,15) -> 15*
         times0(13,15) -> 15*
         times0(18,17) -> 15*
         times0(13,17) -> 15*
         times0(18,19) -> 15*
         times0(13,19) -> 15*
         times0(19,14) -> 15*
         times0(14,14) -> 15*
         times0(19,16) -> 15*
         times0(14,16) -> 15*
         times0(19,18) -> 15*
         times0(14,18) -> 15*
         times0(15,11) -> 15*
         times0(15,13) -> 15*
         times0(15,15) -> 15*
         times0(15,17) -> 15*
         times0(15,19) -> 15*
         times0(16,14) -> 15*
         times0(11,14) -> 15*
         times0(16,16) -> 15*
         times0(11,16) -> 15*
         times0(16,18) -> 15*
         times0(11,18) -> 15*
         times0(17,11) -> 15*
         times0(17,13) -> 15*
         times0(17,15) -> 15*
         times0(17,17) -> 15*
         times0(17,19) -> 15*
         times0(18,14) -> 15*
         times0(13,14) -> 15*
         times0(18,16) -> 15*
         times0(13,16) -> 15*
         times0(18,18) -> 15*
         times0(13,18) -> 15*
         times0(19,11) -> 15*
         times0(14,11) -> 15*
         times0(19,13) -> 15*
         times0(14,13) -> 15*
         times0(19,15) -> 15*
         times0(14,15) -> 15*
         times0(19,17) -> 15*
         times0(14,17) -> 15*
         times0(19,19) -> 15*
         times0(14,19) -> 15*
         times0(15,14) -> 15*
         times0(15,16) -> 15*
         times0(15,18) -> 15*
         times0(16,11) -> 15*
         times0(11,11) -> 15*
         times0(16,13) -> 15*
         times0(11,13) -> 15*
         times0(16,15) -> 15*
         times0(11,15) -> 15*
         times0(16,17) -> 15*
         times0(11,17) -> 15*
         times0(16,19) -> 15*
         times0(11,19) -> 15*
         div0(17,14) -> 16*
         div0(17,16) -> 16*
         div0(17,18) -> 16*
         div0(18,11) -> 16*
         div0(13,11) -> 16*
         div0(18,13) -> 16*
         div0(13,13) -> 16*
         div0(18,15) -> 16*
         div0(13,15) -> 16*
         div0(18,17) -> 16*
         div0(13,17) -> 16*
         div0(18,19) -> 16*
         div0(13,19) -> 16*
         div0(19,14) -> 16*
         div0(14,14) -> 16*
         div0(19,16) -> 16*
         div0(14,16) -> 16*
         div0(19,18) -> 16*
         div0(14,18) -> 16*
         div0(15,11) -> 16*
         div0(15,13) -> 16*
         div0(15,15) -> 16*
         div0(15,17) -> 16*
         div0(15,19) -> 16*
         div0(16,14) -> 16*
         div0(11,14) -> 16*
         div0(16,16) -> 16*
         div0(11,16) -> 16*
         div0(16,18) -> 16*
         div0(11,18) -> 16*
         div0(17,11) -> 16*
         div0(17,13) -> 16*
         div0(17,15) -> 16*
         div0(17,17) -> 16*
         div0(17,19) -> 16*
         div0(18,14) -> 16*
         div0(13,14) -> 16*
         div0(18,16) -> 16*
         div0(13,16) -> 16*
         div0(18,18) -> 16*
         div0(13,18) -> 16*
         div0(19,11) -> 16*
         div0(14,11) -> 16*
         div0(19,13) -> 16*
         div0(14,13) -> 16*
         div0(19,15) -> 16*
         div0(14,15) -> 16*
         div0(19,17) -> 16*
         div0(14,17) -> 16*
         div0(19,19) -> 16*
         div0(14,19) -> 16*
         div0(15,14) -> 16*
         div0(15,16) -> 16*
         div0(15,18) -> 16*
         div0(16,11) -> 16*
         div0(11,11) -> 16*
         div0(16,13) -> 16*
         div0(11,13) -> 16*
         div0(16,15) -> 16*
         div0(11,15) -> 16*
         div0(16,17) -> 16*
         div0(11,17) -> 16*
         div0(16,19) -> 16*
         div0(11,19) -> 16*
         quot0(13,14,17) -> 17*
         quot0(17,14,16) -> 17*
         quot0(16,16,15) -> 17*
         quot0(15,18,14) -> 17*
         quot0(19,19,19) -> 17*
         quot0(11,11,18) -> 17*
         quot0(14,13,16) -> 17*
         quot0(13,15,15) -> 17*
         quot0(11,19,13) -> 17*
         quot0(16,18,19) -> 17*
         quot0(19,11,15) -> 17*
         quot0(18,13,14) -> 17*
         quot0(17,15,13) -> 17*
         quot0(13,17,19) -> 17*
         quot0(14,14,13) -> 17*
         quot0(17,16,11) -> 17*
         quot0(19,13,19) -> 17*
         quot0(18,15,18) -> 17*
         quot0(17,17,17) -> 17*
         quot0(11,13,13) -> 17*
         quot0(14,15,11) -> 17*
         quot0(15,14,18) -> 17*
         quot0(14,16,17) -> 17*
         quot0(18,16,16) -> 17*
         quot0(17,18,15) -> 17*
         quot0(11,14,11) -> 17*
         quot0(13,11,19) -> 17*
         quot0(11,15,17) -> 17*
         quot0(15,15,16) -> 17*
         quot0(14,17,15) -> 17*
         quot0(13,19,14) -> 17*
         quot0(11,16,15) -> 17*
         quot0(17,11,17) -> 17*
         quot0(19,15,14) -> 17*
         quot0(18,17,13) -> 17*
         quot0(14,19,19) -> 17*
         quot0(16,14,14) -> 17*
         quot0(15,16,13) -> 17*
         quot0(18,18,11) -> 17*
         quot0(11,18,19) -> 17*
         quot0(19,17,18) -> 17*
         quot0(18,19,17) -> 17*
         quot0(14,11,15) -> 17*
         quot0(13,13,14) -> 17*
         quot0(15,17,11) -> 17*
         quot0(17,14,19) -> 17*
         quot0(16,16,18) -> 17*
         quot0(15,18,17) -> 17*
         quot0(19,18,16) -> 17*
         quot0(18,11,13) -> 17*
         quot0(14,13,19) -> 17*
         quot0(13,15,18) -> 17*
         quot0(16,17,16) -> 17*
         quot0(15,19,15) -> 17*
         quot0(13,16,16) -> 17*
         quot0(19,11,18) -> 17*
         quot0(18,13,17) -> 17*
         quot0(19,19,13) -> 17*
         quot0(15,11,11) -> 17*
         quot0(18,14,15) -> 17*
         quot0(17,16,14) -> 17*
         quot0(16,18,13) -> 17*
         quot0(16,11,16) -> 17*
         quot0(15,13,15) -> 17*
         quot0(14,15,14) -> 17*
         quot0(13,17,13) -> 17*
         quot0(16,19,11) -> 17*
         quot0(18,16,19) -> 17*
         quot0(17,18,18) -> 17*
         quot0(11,14,14) -> 17*
         quot0(13,18,11) -> 17*
         quot0(19,13,13) -> 17*
         quot0(15,15,19) -> 17*
         quot0(14,17,18) -> 17*
         quot0(13,19,17) -> 17*
         quot0(17,19,16) -> 17*
         quot0(19,14,11) -> 17*
         quot0(11,16,18) -> 17*
         quot0(14,18,16) -> 17*
         quot0(19,15,17) -> 17*
         quot0(13,11,13) -> 17*
         quot0(16,13,11) -> 17*
         quot0(11,17,16) -> 17*
         quot0(16,14,17) -> 17*
         quot0(19,16,15) -> 17*
         quot0(18,18,14) -> 17*
         quot0(14,11,18) -> 17*
         quot0(13,13,17) -> 17*
         quot0(17,13,16) -> 17*
         quot0(16,15,15) -> 16,17
         quot0(15,17,14) -> 17*
         quot0(14,19,13) -> 17*
         quot0(19,18,19) -> 17*
         quot0(13,14,15) -> 17*
         quot0(11,18,13) -> 17*
         quot0(16,17,19) -> 17*
         quot0(15,19,18) -> 17*
         quot0(11,11,16) -> 17*
         quot0(11,19,11) -> 17*
         quot0(17,14,13) -> 17*
         quot0(13,16,19) -> 17*
         quot0(15,11,14) -> 17*
         quot0(14,13,13) -> 17*
         quot0(17,15,11) -> 17*
         quot0(18,14,18) -> 17*
         quot0(17,16,17) -> 17*
         quot0(14,14,11) -> 17*
         quot0(16,11,19) -> 17*
         quot0(15,13,18) -> 17*
         quot0(14,15,17) -> 17*
         quot0(18,15,16) -> 17*
         quot0(17,17,15) -> 17*
         quot0(16,19,14) -> 17*
         quot0(11,13,11) -> 17*
         quot0(11,14,17) -> 17*
         quot0(15,14,16) -> 17*
         quot0(14,16,15) -> 17*
         quot0(13,18,14) -> 17*
         quot0(17,19,19) -> 17*
         quot0(11,15,15) -> 16,17
         quot0(19,14,14) -> 17*
         quot0(18,16,13) -> 17*
         quot0(14,18,19) -> 17*
         quot0(17,11,15) -> 17*
         quot0(16,13,14) -> 17*
         quot0(15,15,13) -> 17*
         quot0(18,17,11) -> 17*
         quot0(11,17,19) -> 17*
         quot0(19,16,18) -> 17*
         quot0(18,18,17) -> 17*
         quot0(15,16,11) -> 17*
         quot0(17,13,19) -> 17*
         quot0(16,15,18) -> 17*
         quot0(15,17,17) -> 17*
         quot0(19,17,16) -> 17*
         quot0(18,19,15) -> 17*
         quot0(13,14,18) -> 17*
         quot0(16,16,16) -> 17*
         quot0(15,18,15) -> 17*
         quot0(18,11,11) -> 17*
         quot0(11,11,19) -> 17*
         quot0(13,15,16) -> 17*
         quot0(11,19,14) -> 17*
         quot0(19,18,13) -> 17*
         quot0(15,11,17) -> 17*
         quot0(19,11,16) -> 17*
         quot0(18,13,15) -> 17*
         quot0(17,15,14) -> 17*
         quot0(16,17,13) -> 17*
         quot0(19,19,11) -> 17*
         quot0(14,14,14) -> 17*
         quot0(13,16,13) -> 17*
         quot0(16,18,11) -> 17*
         quot0(18,15,19) -> 17*
         quot0(17,17,18) -> 17*
         quot0(16,19,17) -> 17*
         quot0(11,13,14) -> 17*
         quot0(13,17,11) -> 17*
         quot0(15,14,19) -> 17*
         quot0(14,16,18) -> 17*
         quot0(13,18,17) -> 17*
         quot0(17,18,16) -> 17*
         quot0(16,11,13) -> 17*
         quot0(19,13,11) -> 17*
         quot0(11,15,18) -> 17*
         quot0(14,17,16) -> 17*
         quot0(13,19,15) -> 17*
         quot0(19,14,17) -> 17*
         quot0(11,16,16) -> 17*
         quot0(17,11,18) -> 17*
         quot0(16,13,17) -> 17*
         quot0(19,15,15) -> 17*
         quot0(18,17,14) -> 17*
         quot0(17,19,13) -> 17*
         quot0(13,11,11) -> 17*
         quot0(16,14,15) -> 17*
         quot0(15,16,14) -> 17*
         quot0(14,18,13) -> 17*
         quot0(19,17,19) -> 17*
         quot0(18,19,18) -> 17*
         quot0(14,11,16) -> 17*
         quot0(13,13,15) -> 17*
         quot0(11,17,13) -> 17*
         quot0(14,19,11) -> 17*
         quot0(16,16,19) -> 17*
         quot0(15,18,18) -> 16,17
         quot0(11,18,11) -> 17*
         quot0(18,11,14) -> 17*
         quot0(17,13,13) -> 17*
         quot0(13,15,19) -> 17*
         quot0(11,19,17) -> 17*
         quot0(15,19,16) -> 17*
         quot0(17,14,11) -> 17*
         quot0(19,11,19) -> 17*
         quot0(18,13,18) -> 17*
         quot0(17,15,17) -> 17*
         quot0(19,19,14) -> 17*
         quot0(11,11,13) -> 17*
         quot0(14,13,11) -> 17*
         quot0(14,14,17) -> 17*
         quot0(18,14,16) -> 17*
         quot0(17,16,15) -> 17*
         quot0(16,18,14) -> 17*
         quot0(11,13,17) -> 17*
         quot0(15,13,16) -> 17*
         quot0(14,15,15) -> 17*
         quot0(13,17,14) -> 17*
         quot0(17,18,19) -> 17*
         quot0(11,14,15) -> 17*
         quot0(19,13,14) -> 17*
         quot0(18,15,13) -> 17*
         quot0(14,17,19) -> 17*
         quot0(13,19,18) -> 17*
         quot0(15,14,13) -> 17*
         quot0(18,16,11) -> 17*
         quot0(11,16,19) -> 17*
         quot0(19,15,18) -> 17*
         quot0(18,17,17) -> 17*
         quot0(13,11,14) -> 17*
         quot0(15,15,11) -> 17*
         quot0(16,14,18) -> 17*
         quot0(15,16,17) -> 17*
         quot0(19,16,16) -> 17*
         quot0(18,18,15) -> 17*
         quot0(14,11,19) -> 17*
         quot0(13,13,18) -> 17*
         quot0(16,15,16) -> 17*
         quot0(15,17,15) -> 17*
         quot0(14,19,14) -> 17*
         quot0(13,14,16) -> 17*
         quot0(11,18,14) -> 17*
         quot0(18,11,17) -> 17*
         quot0(19,17,13) -> 17*
         quot0(15,19,19) -> 17*
         quot0(17,14,14) -> 17*
         quot0(16,16,13) -> 17*
         quot0(19,18,11) -> 17*
         quot0(19,19,17) -> 17*
         quot0(15,11,15) -> 17*
         quot0(14,13,14) -> 17*
         quot0(13,15,13) -> 17*
         quot0(16,17,11) -> 17*
         quot0(18,14,19) -> 17*
         quot0(17,16,18) -> 17*
         quot0(16,18,17) -> 17*
         quot0(13,16,11) -> 17*
         quot0(19,11,13) -> 17*
         quot0(15,13,19) -> 17*
         quot0(14,15,18) -> 17*
         quot0(13,17,17) -> 17*
         quot0(17,17,16) -> 17*
         quot0(16,19,15) -> 17*
         quot0(11,14,18) -> 17*
         quot0(14,16,16) -> 17*
         quot0(13,18,15) -> 17*
         quot0(19,13,17) -> 17*
         quot0(16,11,11) -> 17*
         quot0(11,15,16) -> 17*
         quot0(19,14,15) -> 17*
         quot0(18,16,14) -> 17*
         quot0(17,18,13) -> 17*
         quot0(13,11,17) -> 17*
         quot0(17,11,16) -> 17*
         quot0(16,13,15) -> 17*
         quot0(15,15,14) -> 17*
         quot0(14,17,13) -> 17*
         quot0(17,19,11) -> 17*
         quot0(19,16,19) -> 17*
         quot0(18,18,18) -> 17*
         quot0(11,16,13) -> 17*
         quot0(14,18,11) -> 17*
         quot0(16,15,19) -> 17*
         quot0(15,17,18) -> 17*
         quot0(14,19,17) -> 17*
         quot0(18,19,16) -> 17*
         quot0(11,17,11) -> 17*
         quot0(13,14,19) -> 17*
         quot0(11,18,17) -> 17*
         quot0(15,18,16) -> 17*
         quot0(14,11,13) -> 17*
         quot0(17,13,11) -> 17*
         quot0(11,19,15) -> 17*
         quot0(17,14,17) -> 17*
         quot0(19,18,14) -> 17*
         quot0(15,11,18) -> 17*
         quot0(14,13,17) -> 17*
         quot0(18,13,16) -> 17*
         quot0(17,15,15) -> 17*
         quot0(16,17,14) -> 17*
         quot0(15,19,13) -> 17*
         quot0(11,11,11) -> 17*
         quot0(14,14,15) -> 17*
         quot0(13,16,14) -> 17*
         quot0(17,17,19) -> 17*
         quot0(16,19,18) -> 17*
         quot0(11,13,15) -> 17*
         quot0(18,14,13) -> 17*
         quot0(14,16,19) -> 17*
         quot0(13,18,18) -> 17*
         quot0(16,11,14) -> 17*
         quot0(15,13,13) -> 17*
         quot0(18,15,11) -> 17*
         quot0(11,15,19) -> 17*
         quot0(13,19,16) -> 17*
         quot0(19,14,18) -> 17*
         quot0(18,16,17) -> 17*
         quot0(15,14,11) -> 17*
         quot0(17,11,19) -> 17*
         quot0(16,13,18) -> 17*
         quot0(15,15,17) -> 17*
         quot0(19,15,16) -> 17*
         quot0(18,17,15) -> 17*
         quot0(17,19,14) -> 17*
         quot0(16,14,16) -> 17*
         quot0(15,16,15) -> 17*
         quot0(14,18,14) -> 17*
         quot0(18,19,19) -> 17*
         quot0(13,13,16) -> 17*
         quot0(11,17,14) -> 17*
         quot0(19,16,13) -> 17*
         quot0(15,18,19) -> 17*
         quot0(18,11,15) -> 17*
         quot0(17,13,14) -> 17*
         quot0(16,15,13) -> 17*
         quot0(19,17,11) -> 17*
         quot0(11,19,18) -> 17*
         quot0(19,18,17) -> 17*
         quot0(13,14,13) -> 17*
         quot0(16,16,11) -> 17*
         quot0(18,13,19) -> 17*
         quot0(17,15,18) -> 17*
         quot0(16,17,17) -> 16,17
         quot0(19,19,15) -> 17*
         quot0(11,11,14) -> 17*
         quot0(13,15,11) -> 17*
         quot0(14,14,18) -> 17*
         quot0(13,16,17) -> 17*
         quot0(17,16,16) -> 17*
         quot0(16,18,15) -> 17*
         quot0(19,11,11) -> 17*
         quot0(11,13,18) -> 17*
         quot0(14,15,16) -> 17*
         quot0(13,17,15) -> 17*
         quot0(11,14,16) -> 17*
         quot0(16,11,17) -> 17*
         quot0(19,13,15) -> 17*
         quot0(18,15,14) -> 17*
         quot0(17,17,13) -> 17*
         quot0(13,19,19) -> 17*
         quot0(15,14,14) -> 16,17
         quot0(14,16,13) -> 17*
         quot0(17,18,11) -> 17*
         quot0(19,15,19) -> 17*
         quot0(18,17,18) -> 17*
         quot0(17,19,17) -> 17*
         quot0(13,11,15) -> 17*
         quot0(11,15,13) -> 17*
         quot0(14,17,11) -> 17*
         quot0(16,14,19) -> 17*
         quot0(15,16,18) -> 17*
         quot0(14,18,17) -> 17*
         quot0(18,18,16) -> 17*
         quot0(11,16,11) -> 17*
         quot0(17,11,13) -> 17*
         quot0(13,13,19) -> 17*
         quot0(11,17,17) -> 16,17
         quot0(15,17,16) -> 17*
         quot0(14,19,15) -> 17*
         quot0(11,18,15) -> 17*
         quot0(18,11,18) -> 17*
         quot0(17,13,17) -> 17*
         quot0(19,17,14) -> 17*
         quot0(18,19,13) -> 17*
         quot0(14,11,11) -> 17*
         quot0(17,14,15) -> 17*
         quot0(16,16,14) -> 17*
         quot0(15,18,13) -> 17*
         quot0(19,19,18) -> 17*
         quot0(11,11,17) -> 17*
         quot0(15,11,16) -> 17*
         quot0(14,13,15) -> 17*
         quot0(13,15,14) -> 17*
         quot0(15,19,11) -> 17*
         quot0(17,16,19) -> 17*
         quot0(16,18,18) -> 17*
         quot0(19,11,14) -> 17*
         quot0(18,13,13) -> 17*
         quot0(14,15,19) -> 17*
         quot0(13,17,18) -> 17*
         quot0(16,19,16) -> 17*
         quot0(18,14,11) -> 17*
         quot0(11,14,19) -> 17*
         quot0(13,18,16) -> 17*
         quot0(19,13,18) -> 17*
         quot0(18,15,17) -> 17*
         quot0(15,13,11) -> 17*
         quot0(15,14,17) -> 17*
         quot0(19,14,16) -> 17*
         quot0(18,16,15) -> 17*
         quot0(17,18,14) -> 17*
         quot0(13,11,18) -> 17*
         quot0(16,13,16) -> 17*
         quot0(15,15,15) -> 17*
         quot0(14,17,14) -> 17*
         quot0(13,19,13) -> 17*
         quot0(18,18,19) -> 17*
         quot0(11,16,14) -> 17*
         quot0(19,15,13) -> 17*
         quot0(15,17,19) -> 17*
         quot0(14,19,18) -> 17*
         quot0(16,14,13) -> 17*
         quot0(19,16,11) -> 17*
         quot0(11,18,18) -> 17*
         quot0(19,17,17) -> 17*
         quot0(14,11,14) -> 17*
         quot0(13,13,13) -> 17*
         quot0(16,15,11) -> 17*
         quot0(11,19,16) -> 17*
         quot0(17,14,18) -> 17*
         quot0(16,16,17) -> 17*
         quot0(19,18,15) -> 17*
         quot0(13,14,11) -> 17*
         quot0(15,11,19) -> 17*
         quot0(14,13,18) -> 17*
         quot0(13,15,17) -> 17*
         quot0(17,15,16) -> 17*
         quot0(16,17,15) -> 17*
         quot0(15,19,14) -> 17*
         quot0(14,14,16) -> 17*
         quot0(13,16,15) -> 17*
         quot0(19,11,17) -> 17*
         quot0(16,19,19) -> 16,17
         quot0(11,13,16) -> 17*
         quot0(18,14,14) -> 17*
         quot0(17,16,13) -> 17*
         quot0(13,18,19) -> 17*
         quot0(16,11,15) -> 17*
         quot0(15,13,14) -> 17*
         quot0(14,15,13) -> 17*
         quot0(17,17,11) -> 17*
         quot0(19,14,19) -> 17*
         quot0(18,16,18) -> 17*
         quot0(17,18,17) -> 17*
         quot0(11,14,13) -> 17*
         quot0(14,16,11) -> 17*
         quot0(16,13,19) -> 17*
         quot0(15,15,18) -> 17*
         quot0(14,17,17) -> 17*
         quot0(18,17,16) -> 17*
         quot0(17,19,15) -> 17*
         quot0(11,15,11) -> 17*
         quot0(11,16,17) -> 17*
         quot0(15,16,16) -> 16,17
         quot0(14,18,15) -> 17*
         quot0(17,11,11) -> 17*
         quot0(11,17,15) -> 17*
         quot0(19,16,14) -> 17*
         quot0(18,18,13) -> 17*
         quot0(14,11,17) -> 17*
         quot0(18,11,16) -> 17*
         quot0(17,13,15) -> 17*
         quot0(16,15,14) -> 17*
         quot0(15,17,13) -> 17*
         quot0(18,19,11) -> 17*
         quot0(11,19,19) -> 16,17
         quot0(19,18,18) -> 17*
         quot0(13,14,14) -> 17*
         quot0(15,18,11) -> 17*
         quot0(17,15,19) -> 17*
         quot0(16,17,18) -> 17*
         quot0(15,19,17) -> 17*
         quot0(19,19,16) -> 17*
         quot0(11,11,15) -> 17*
         quot0(14,14,19) -> 17*
         quot0(13,16,18) -> 17*
         quot0(16,18,16) -> 17*
         quot0(15,11,13) -> 17*
         quot0(18,13,11) -> 17*
         quot0(11,13,19) -> 17*
         quot0(13,17,16) -> 17*
         quot0(18,14,17) -> 17*
         quot0(16,11,18) -> 17*
         quot0(15,13,17) -> 17*
         quot0(19,13,16) -> 17*
         quot0(18,15,15) -> 17*
         quot0(17,17,14) -> 17*
         quot0(16,19,13) -> 17*
         quot0(15,14,15) -> 17*
         quot0(14,16,14) -> 17*
         quot0(13,18,13) -> 17*
         quot0(18,17,19) -> 17*
         quot0(17,19,18) -> 17*
         quot0(13,11,16) -> 17*
         quot0(11,15,14) -> 17*
         quot0(13,19,11) -> 17*
         quot0(19,14,13) -> 17*
         quot0(15,16,19) -> 17*
         quot0(14,18,18) -> 17*
         quot0(17,11,14) -> 17*
         quot0(16,13,13) -> 17*
         quot0(19,15,11) -> 17*
         quot0(11,17,18) -> 17*
         quot0(14,19,16) -> 17*
         quot0(19,16,17) -> 17*
         quot0(16,14,11) -> 17*
         quot0(11,18,16) -> 17*
         quot0(18,11,19) -> 17*
         quot0(17,13,18) -> 17*
         quot0(16,15,17) -> 17*
         quot0(19,17,15) -> 17*
         quot0(18,19,14) -> 17*
         quot0(13,13,11) -> 17*
         11 -> 14*
         13 -> 14*
         14 -> 15*
         15 -> 14*
         16 -> 15,14
         17 -> 14*
         18 -> 15,14
         19 -> 14*
       problem:
        DPs:
         
        TRS:
         plus(x,0()) -> x
         plus(0(),y) -> y
         plus(s(x),y) -> s(plus(x,y))
         times(0(),y) -> 0()
         times(s(0()),y) -> y
         times(s(x),y) -> plus(y,times(x,y))
         div(0(),y) -> 0()
         div(x,y) -> quot(x,y,y)
         quot(0(),s(y),z) -> 0()
         quot(s(x),s(y),z) -> quot(x,y,z)
         quot(x,0(),s(z)) -> s(div(x,s(z)))
         div(div(x,y),z) -> div(x,times(y,z))
       Qed
    
    DPs:
     times#(s(x),y) -> times#(x,y)
    TRS:
     plus(x,0()) -> x
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     times(0(),y) -> 0()
     times(s(0()),y) -> y
     times(s(x),y) -> plus(y,times(x,y))
     div(0(),y) -> 0()
     div(x,y) -> quot(x,y,y)
     quot(0(),s(y),z) -> 0()
     quot(s(x),s(y),z) -> quot(x,y,z)
     quot(x,0(),s(z)) -> s(div(x,s(z)))
     div(div(x,y),z) -> div(x,times(y,z))
    Subterm Criterion Processor:
     simple projection:
      pi(times#) = 0
     problem:
      DPs:
       
      TRS:
       plus(x,0()) -> x
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       times(0(),y) -> 0()
       times(s(0()),y) -> y
       times(s(x),y) -> plus(y,times(x,y))
       div(0(),y) -> 0()
       div(x,y) -> quot(x,y,y)
       quot(0(),s(y),z) -> 0()
       quot(s(x),s(y),z) -> quot(x,y,z)
       quot(x,0(),s(z)) -> s(div(x,s(z)))
       div(div(x,y),z) -> div(x,times(y,z))
     Qed
    
    DPs:
     plus#(s(x),y) -> plus#(x,y)
    TRS:
     plus(x,0()) -> x
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     times(0(),y) -> 0()
     times(s(0()),y) -> y
     times(s(x),y) -> plus(y,times(x,y))
     div(0(),y) -> 0()
     div(x,y) -> quot(x,y,y)
     quot(0(),s(y),z) -> 0()
     quot(s(x),s(y),z) -> quot(x,y,z)
     quot(x,0(),s(z)) -> s(div(x,s(z)))
     div(div(x,y),z) -> div(x,times(y,z))
    Subterm Criterion Processor:
     simple projection:
      pi(plus#) = 0
     problem:
      DPs:
       
      TRS:
       plus(x,0()) -> x
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       times(0(),y) -> 0()
       times(s(0()),y) -> y
       times(s(x),y) -> plus(y,times(x,y))
       div(0(),y) -> 0()
       div(x,y) -> quot(x,y,y)
       quot(0(),s(y),z) -> 0()
       quot(s(x),s(y),z) -> quot(x,y,z)
       quot(x,0(),s(z)) -> s(div(x,s(z)))
       div(div(x,y),z) -> div(x,times(y,z))
     Qed