MAYBE
Time: 1.006994
TRS:
 {          plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
          plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
         plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
         plus(zero(), y) -> y,
  times(x, plus(y, 1())) -> plus(times(x, plus(y, times(1(), 0()))), x),
           times(x, 1()) -> x,
           times(x, 0()) -> 0(),
        if(true(), x, y) -> x,
       if(false(), x, y) -> y,
            gt(s x, s y) -> gt(x, y),
         gt(s x, zero()) -> true(),
           gt(zero(), y) -> false(),
                   not x -> if(x, false(), true()),
                    id x -> x}
 DP:
  DP:
   {          plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x),
              plus#(s x, x) -> if#(gt(x, x), id x, id x),
              plus#(s x, x) -> gt#(x, x),
              plus#(s x, x) -> id# x,
            plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
            plus#(s x, s y) -> if#(gt(x, y), x, y),
            plus#(s x, s y) -> if#(not gt(x, y), id x, id y),
            plus#(s x, s y) -> gt#(x, y),
            plus#(s x, s y) -> not# gt(x, y),
            plus#(s x, s y) -> id# x,
            plus#(s x, s y) -> id# y,
           plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)),
           plus#(id x, s y) -> if#(gt(s y, y), y, s y),
           plus#(id x, s y) -> gt#(s y, y),
    times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())),
    times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x),
    times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0()))),
    times#(x, plus(y, 1())) -> times#(1(), 0()),
              gt#(s x, s y) -> gt#(x, y),
                     not# x -> if#(x, false(), true())}
  TRS:
  {          plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
           plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
          plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
          plus(zero(), y) -> y,
   times(x, plus(y, 1())) -> plus(times(x, plus(y, times(1(), 0()))), x),
            times(x, 1()) -> x,
            times(x, 0()) -> 0(),
         if(true(), x, y) -> x,
        if(false(), x, y) -> y,
             gt(s x, s y) -> gt(x, y),
          gt(s x, zero()) -> true(),
            gt(zero(), y) -> false(),
                    not x -> if(x, false(), true()),
                     id x -> x}
  EDG:
   {(plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(id x, s y) -> gt#(s y, y))
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(id x, s y) -> if#(gt(s y, y), y, s y))
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)))
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> id# y)
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> id# x)
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> not# gt(x, y))
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> gt#(x, y))
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> if#(not gt(x, y), id x, id y))
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> if#(gt(x, y), x, y))
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, x) -> id# x)
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, x) -> gt#(x, x))
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, x) -> if#(gt(x, x), id x, id x))
    (plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x), plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x))
    (plus#(id x, s y) -> gt#(s y, y), gt#(s x, s y) -> gt#(x, y))
    (plus#(s x, s y) -> gt#(x, y), gt#(s x, s y) -> gt#(x, y))
    (plus#(s x, x) -> gt#(x, x), gt#(s x, s y) -> gt#(x, y))
    (gt#(s x, s y) -> gt#(x, y), gt#(s x, s y) -> gt#(x, y))
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x))
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, x) -> if#(gt(x, x), id x, id x))
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, x) -> gt#(x, x))
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, x) -> id# x)
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> if#(gt(x, y), x, y))
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> if#(not gt(x, y), id x, id y))
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> gt#(x, y))
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> not# gt(x, y))
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> id# x)
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(s x, s y) -> id# y)
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)))
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(id x, s y) -> if#(gt(s y, y), y, s y))
    (plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)), plus#(id x, s y) -> gt#(s y, y))
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x))
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, x) -> if#(gt(x, x), id x, id x))
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, x) -> gt#(x, x))
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, x) -> id# x)
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> if#(gt(x, y), x, y))
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> if#(not gt(x, y), id x, id y))
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> gt#(x, y))
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> not# gt(x, y))
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> id# x)
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(s x, s y) -> id# y)
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)))
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(id x, s y) -> if#(gt(s y, y), y, s y))
    (plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)), plus#(id x, s y) -> gt#(s y, y))
    (plus#(s x, s y) -> not# gt(x, y), not# x -> if#(x, false(), true()))
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x))
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(s x, x) -> if#(gt(x, x), id x, id x))
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(s x, x) -> gt#(x, x))
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(s x, x) -> id# x)
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(s x, s y) -> if#(gt(x, y), x, y))
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(s x, s y) -> if#(not gt(x, y), id x, id y))
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(s x, s y) -> gt#(x, y))
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(s x, s y) -> not# gt(x, y))
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(s x, s y) -> id# x)
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(s x, s y) -> id# y)
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)))
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(id x, s y) -> if#(gt(s y, y), y, s y))
    (times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x), plus#(id x, s y) -> gt#(s y, y))
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x))
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(s x, x) -> if#(gt(x, x), id x, id x))
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(s x, x) -> gt#(x, x))
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(s x, x) -> id# x)
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)))
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(s x, s y) -> if#(gt(x, y), x, y))
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(s x, s y) -> if#(not gt(x, y), id x, id y))
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(s x, s y) -> gt#(x, y))
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(s x, s y) -> not# gt(x, y))
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(s x, s y) -> id# x)
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(s x, s y) -> id# y)
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y)))
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(id x, s y) -> if#(gt(s y, y), y, s y))
    (times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())), plus#(id x, s y) -> gt#(s y, y))
    (times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0()))), times#(x, plus(y, 1())) -> plus#(y, times(1(), 0())))
    (times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0()))), times#(x, plus(y, 1())) -> plus#(times(x, plus(y, times(1(), 0()))), x))
    (times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0()))), times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0()))))
    (times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0()))), times#(x, plus(y, 1())) -> times#(1(), 0()))}
   STATUS:
    arrows: 0.802500
    SCCS (3):
     Scc:
      {times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0())))}
     Scc:
      {   plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x),
        plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
       plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y))}
     Scc:
      {gt#(s x, s y) -> gt#(x, y)}
     
     SCC (1):
      Strict:
       {times#(x, plus(y, 1())) -> times#(x, plus(y, times(1(), 0())))}
      Weak:
      {          plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
               plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
              plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
              plus(zero(), y) -> y,
       times(x, plus(y, 1())) -> plus(times(x, plus(y, times(1(), 0()))), x),
                times(x, 1()) -> x,
                times(x, 0()) -> 0(),
             if(true(), x, y) -> x,
            if(false(), x, y) -> y,
                 gt(s x, s y) -> gt(x, y),
              gt(s x, zero()) -> true(),
                gt(zero(), y) -> false(),
                        not x -> if(x, false(), true()),
                         id x -> x}
      Open
     
     
     
     SCC (3):
      Strict:
       {   plus#(s x, x) -> plus#(if(gt(x, x), id x, id x), s x),
         plus#(s x, s y) -> plus#(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
        plus#(id x, s y) -> plus#(x, if(gt(s y, y), y, s y))}
      Weak:
      {          plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
               plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
              plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
              plus(zero(), y) -> y,
       times(x, plus(y, 1())) -> plus(times(x, plus(y, times(1(), 0()))), x),
                times(x, 1()) -> x,
                times(x, 0()) -> 0(),
             if(true(), x, y) -> x,
            if(false(), x, y) -> y,
                 gt(s x, s y) -> gt(x, y),
              gt(s x, zero()) -> true(),
                gt(zero(), y) -> false(),
                        not x -> if(x, false(), true()),
                         id x -> x}
      Open
     
     
     
     
     
     
     
     
     
     
     
     SCC (1):
      Strict:
       {gt#(s x, s y) -> gt#(x, y)}
      Weak:
      {          plus(s x, x) -> plus(if(gt(x, x), id x, id x), s x),
               plus(s x, s y) -> s s plus(if(gt(x, y), x, y), if(not gt(x, y), id x, id y)),
              plus(id x, s y) -> s plus(x, if(gt(s y, y), y, s y)),
              plus(zero(), y) -> y,
       times(x, plus(y, 1())) -> plus(times(x, plus(y, times(1(), 0()))), x),
                times(x, 1()) -> x,
                times(x, 0()) -> 0(),
             if(true(), x, y) -> x,
            if(false(), x, y) -> y,
                 gt(s x, s y) -> gt(x, y),
              gt(s x, zero()) -> true(),
                gt(zero(), y) -> false(),
                        not x -> if(x, false(), true()),
                         id x -> x}
      Open