MAYBE
Time: 0.004320
TRS:
 {                     inc s x -> s inc x,
                       inc 0() -> s 0(),
      ifPlus(false(), x, y, z) -> plus(x, z),
       ifPlus(true(), x, y, z) -> y,
                      eq(x, x) -> true(),
                  eq(s x, s y) -> eq(x, y),
                  eq(s x, 0()) -> false(),
                  eq(0(), s x) -> false(),
                  eq(0(), 0()) -> true(),
                   minus(x, x) -> 0(),
                 minus(x, 0()) -> x,
               minus(s x, s y) -> minus(x, y),
                 minus(0(), x) -> 0(),
                    plus(x, y) -> ifPlus(eq(x, 0()), minus(x, s 0()), x, inc x),
            timesIter(x, y, z) -> ifTimes(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)),
                   times(x, y) -> timesIter(x, y, 0()),
  ifTimes(false(), x, y, z, u) -> timesIter(x, y, u),
   ifTimes(true(), x, y, z, u) -> z,
                           f() -> g(),
                           f() -> h()}
 DP:
  DP:
   {                     inc# s x -> inc# x,
        ifPlus#(false(), x, y, z) -> plus#(x, z),
                    eq#(s x, s y) -> eq#(x, y),
                 minus#(s x, s y) -> minus#(x, y),
                      plus#(x, y) -> inc# x,
                      plus#(x, y) -> ifPlus#(eq(x, 0()), minus(x, s 0()), x, inc x),
                      plus#(x, y) -> eq#(x, 0()),
                      plus#(x, y) -> minus#(x, s 0()),
              timesIter#(x, y, z) -> eq#(x, 0()),
              timesIter#(x, y, z) -> minus#(x, s 0()),
              timesIter#(x, y, z) -> plus#(y, z),
              timesIter#(x, y, z) -> ifTimes#(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)),
                     times#(x, y) -> timesIter#(x, y, 0()),
    ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, u)}
  TRS:
  {                     inc s x -> s inc x,
                        inc 0() -> s 0(),
       ifPlus(false(), x, y, z) -> plus(x, z),
        ifPlus(true(), x, y, z) -> y,
                       eq(x, x) -> true(),
                   eq(s x, s y) -> eq(x, y),
                   eq(s x, 0()) -> false(),
                   eq(0(), s x) -> false(),
                   eq(0(), 0()) -> true(),
                    minus(x, x) -> 0(),
                  minus(x, 0()) -> x,
                minus(s x, s y) -> minus(x, y),
                  minus(0(), x) -> 0(),
                     plus(x, y) -> ifPlus(eq(x, 0()), minus(x, s 0()), x, inc x),
             timesIter(x, y, z) -> ifTimes(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)),
                    times(x, y) -> timesIter(x, y, 0()),
   ifTimes(false(), x, y, z, u) -> timesIter(x, y, u),
    ifTimes(true(), x, y, z, u) -> z,
                            f() -> g(),
                            f() -> h()}
  EDG:
   {(timesIter#(x, y, z) -> minus#(x, s 0()), minus#(s x, s y) -> minus#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (ifPlus#(false(), x, y, z) -> plus#(x, z), plus#(x, y) -> minus#(x, s 0()))
    (ifPlus#(false(), x, y, z) -> plus#(x, z), plus#(x, y) -> eq#(x, 0()))
    (ifPlus#(false(), x, y, z) -> plus#(x, z), plus#(x, y) -> ifPlus#(eq(x, 0()), minus(x, s 0()), x, inc x))
    (ifPlus#(false(), x, y, z) -> plus#(x, z), plus#(x, y) -> inc# x)
    (plus#(x, y) -> ifPlus#(eq(x, 0()), minus(x, s 0()), x, inc x), ifPlus#(false(), x, y, z) -> plus#(x, z))
    (plus#(x, y) -> inc# x, inc# s x -> inc# x)
    (timesIter#(x, y, z) -> ifTimes#(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)), ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, u))
    (times#(x, y) -> timesIter#(x, y, 0()), timesIter#(x, y, z) -> eq#(x, 0()))
    (times#(x, y) -> timesIter#(x, y, 0()), timesIter#(x, y, z) -> minus#(x, s 0()))
    (times#(x, y) -> timesIter#(x, y, 0()), timesIter#(x, y, z) -> plus#(y, z))
    (times#(x, y) -> timesIter#(x, y, 0()), timesIter#(x, y, z) -> ifTimes#(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)))
    (inc# s x -> inc# x, inc# s x -> inc# x)
    (timesIter#(x, y, z) -> plus#(y, z), plus#(x, y) -> inc# x)
    (timesIter#(x, y, z) -> plus#(y, z), plus#(x, y) -> ifPlus#(eq(x, 0()), minus(x, s 0()), x, inc x))
    (timesIter#(x, y, z) -> plus#(y, z), plus#(x, y) -> eq#(x, 0()))
    (timesIter#(x, y, z) -> plus#(y, z), plus#(x, y) -> minus#(x, s 0()))
    (ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, u), timesIter#(x, y, z) -> eq#(x, 0()))
    (ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, u), timesIter#(x, y, z) -> minus#(x, s 0()))
    (ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, u), timesIter#(x, y, z) -> plus#(y, z))
    (ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, u), timesIter#(x, y, z) -> ifTimes#(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)))
    (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y))
    (plus#(x, y) -> minus#(x, s 0()), minus#(s x, s y) -> minus#(x, y))}
   STATUS:
    arrows: 0.877551
    SCCS (5):
     Scc:
      {          timesIter#(x, y, z) -> ifTimes#(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)),
       ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, u)}
     Scc:
      {ifPlus#(false(), x, y, z) -> plus#(x, z),
                     plus#(x, y) -> ifPlus#(eq(x, 0()), minus(x, s 0()), x, inc x)}
     Scc:
      {inc# s x -> inc# x}
     Scc:
      {eq#(s x, s y) -> eq#(x, y)}
     Scc:
      {minus#(s x, s y) -> minus#(x, y)}
     
     
     SCC (2):
      Strict:
       {          timesIter#(x, y, z) -> ifTimes#(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)),
        ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, u)}
      Weak:
      {                     inc s x -> s inc x,
                            inc 0() -> s 0(),
           ifPlus(false(), x, y, z) -> plus(x, z),
            ifPlus(true(), x, y, z) -> y,
                           eq(x, x) -> true(),
                       eq(s x, s y) -> eq(x, y),
                       eq(s x, 0()) -> false(),
                       eq(0(), s x) -> false(),
                       eq(0(), 0()) -> true(),
                        minus(x, x) -> 0(),
                      minus(x, 0()) -> x,
                    minus(s x, s y) -> minus(x, y),
                      minus(0(), x) -> 0(),
                         plus(x, y) -> ifPlus(eq(x, 0()), minus(x, s 0()), x, inc x),
                 timesIter(x, y, z) -> ifTimes(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)),
                        times(x, y) -> timesIter(x, y, 0()),
       ifTimes(false(), x, y, z, u) -> timesIter(x, y, u),
        ifTimes(true(), x, y, z, u) -> z,
                                f() -> g(),
                                f() -> h()}
      Open
     
     SCC (2):
      Strict:
       {ifPlus#(false(), x, y, z) -> plus#(x, z),
                      plus#(x, y) -> ifPlus#(eq(x, 0()), minus(x, s 0()), x, inc x)}
      Weak:
      {                     inc s x -> s inc x,
                            inc 0() -> s 0(),
           ifPlus(false(), x, y, z) -> plus(x, z),
            ifPlus(true(), x, y, z) -> y,
                           eq(x, x) -> true(),
                       eq(s x, s y) -> eq(x, y),
                       eq(s x, 0()) -> false(),
                       eq(0(), s x) -> false(),
                       eq(0(), 0()) -> true(),
                        minus(x, x) -> 0(),
                      minus(x, 0()) -> x,
                    minus(s x, s y) -> minus(x, y),
                      minus(0(), x) -> 0(),
                         plus(x, y) -> ifPlus(eq(x, 0()), minus(x, s 0()), x, inc x),
                 timesIter(x, y, z) -> ifTimes(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)),
                        times(x, y) -> timesIter(x, y, 0()),
       ifTimes(false(), x, y, z, u) -> timesIter(x, y, u),
        ifTimes(true(), x, y, z, u) -> z,
                                f() -> g(),
                                f() -> h()}
      Open
     
     
     SCC (1):
      Strict:
       {inc# s x -> inc# x}
      Weak:
      {                     inc s x -> s inc x,
                            inc 0() -> s 0(),
           ifPlus(false(), x, y, z) -> plus(x, z),
            ifPlus(true(), x, y, z) -> y,
                           eq(x, x) -> true(),
                       eq(s x, s y) -> eq(x, y),
                       eq(s x, 0()) -> false(),
                       eq(0(), s x) -> false(),
                       eq(0(), 0()) -> true(),
                        minus(x, x) -> 0(),
                      minus(x, 0()) -> x,
                    minus(s x, s y) -> minus(x, y),
                      minus(0(), x) -> 0(),
                         plus(x, y) -> ifPlus(eq(x, 0()), minus(x, s 0()), x, inc x),
                 timesIter(x, y, z) -> ifTimes(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)),
                        times(x, y) -> timesIter(x, y, 0()),
       ifTimes(false(), x, y, z, u) -> timesIter(x, y, u),
        ifTimes(true(), x, y, z, u) -> z,
                                f() -> g(),
                                f() -> h()}
      Open
     
     SCC (1):
      Strict:
       {eq#(s x, s y) -> eq#(x, y)}
      Weak:
      {                     inc s x -> s inc x,
                            inc 0() -> s 0(),
           ifPlus(false(), x, y, z) -> plus(x, z),
            ifPlus(true(), x, y, z) -> y,
                           eq(x, x) -> true(),
                       eq(s x, s y) -> eq(x, y),
                       eq(s x, 0()) -> false(),
                       eq(0(), s x) -> false(),
                       eq(0(), 0()) -> true(),
                        minus(x, x) -> 0(),
                      minus(x, 0()) -> x,
                    minus(s x, s y) -> minus(x, y),
                      minus(0(), x) -> 0(),
                         plus(x, y) -> ifPlus(eq(x, 0()), minus(x, s 0()), x, inc x),
                 timesIter(x, y, z) -> ifTimes(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)),
                        times(x, y) -> timesIter(x, y, 0()),
       ifTimes(false(), x, y, z, u) -> timesIter(x, y, u),
        ifTimes(true(), x, y, z, u) -> z,
                                f() -> g(),
                                f() -> h()}
      Open
     
     
     SCC (1):
      Strict:
       {minus#(s x, s y) -> minus#(x, y)}
      Weak:
      {                     inc s x -> s inc x,
                            inc 0() -> s 0(),
           ifPlus(false(), x, y, z) -> plus(x, z),
            ifPlus(true(), x, y, z) -> y,
                           eq(x, x) -> true(),
                       eq(s x, s y) -> eq(x, y),
                       eq(s x, 0()) -> false(),
                       eq(0(), s x) -> false(),
                       eq(0(), 0()) -> true(),
                        minus(x, x) -> 0(),
                      minus(x, 0()) -> x,
                    minus(s x, s y) -> minus(x, y),
                      minus(0(), x) -> 0(),
                         plus(x, y) -> ifPlus(eq(x, 0()), minus(x, s 0()), x, inc x),
                 timesIter(x, y, z) -> ifTimes(eq(x, 0()), minus(x, s 0()), y, z, plus(y, z)),
                        times(x, y) -> timesIter(x, y, 0()),
       ifTimes(false(), x, y, z, u) -> timesIter(x, y, u),
        ifTimes(true(), x, y, z, u) -> z,
                                f() -> g(),
                                f() -> h()}
      Open