MAYBE
Time: 0.008397
TRS:
 {          lt(x, 0()) -> false(),
          lt(0(), s x) -> true(),
          lt(s x, s y) -> lt(x, y),
         times(0(), y) -> 0(),
         times(s x, y) -> plus(y, times(x, y)),
          plus(0(), y) -> y,
          plus(s x, y) -> s plus(x, y),
         loop(x, c, y) -> if(lt(x, c), x, c, y),
                 fac x -> loop(x, s 0(), s 0()),
   if(true(), x, c, y) -> y,
  if(false(), x, c, y) -> loop(x, s c, times(y, s c))}
 DP:
  DP:
   {        lt#(s x, s y) -> lt#(x, y),
           times#(s x, y) -> times#(x, y),
           times#(s x, y) -> plus#(y, times(x, y)),
            plus#(s x, y) -> plus#(x, y),
           loop#(x, c, y) -> lt#(x, c),
           loop#(x, c, y) -> if#(lt(x, c), x, c, y),
                   fac# x -> loop#(x, s 0(), s 0()),
    if#(false(), x, c, y) -> times#(y, s c),
    if#(false(), x, c, y) -> loop#(x, s c, times(y, s c))}
  TRS:
  {          lt(x, 0()) -> false(),
           lt(0(), s x) -> true(),
           lt(s x, s y) -> lt(x, y),
          times(0(), y) -> 0(),
          times(s x, y) -> plus(y, times(x, y)),
           plus(0(), y) -> y,
           plus(s x, y) -> s plus(x, y),
          loop(x, c, y) -> if(lt(x, c), x, c, y),
                  fac x -> loop(x, s 0(), s 0()),
    if(true(), x, c, y) -> y,
   if(false(), x, c, y) -> loop(x, s c, times(y, s c))}
  EDG:
   {(lt#(s x, s y) -> lt#(x, y), lt#(s x, s y) -> lt#(x, y))
    (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
    (times#(s x, y) -> plus#(y, times(x, y)), plus#(s x, y) -> plus#(x, y))
    (if#(false(), x, c, y) -> loop#(x, s c, times(y, s c)), loop#(x, c, y) -> if#(lt(x, c), x, c, y))
    (if#(false(), x, c, y) -> loop#(x, s c, times(y, s c)), loop#(x, c, y) -> lt#(x, c))
    (if#(false(), x, c, y) -> times#(y, s c), times#(s x, y) -> times#(x, y))
    (if#(false(), x, c, y) -> times#(y, s c), times#(s x, y) -> plus#(y, times(x, y)))
    (fac# x -> loop#(x, s 0(), s 0()), loop#(x, c, y) -> lt#(x, c))
    (fac# x -> loop#(x, s 0(), s 0()), loop#(x, c, y) -> if#(lt(x, c), x, c, y))
    (loop#(x, c, y) -> if#(lt(x, c), x, c, y), if#(false(), x, c, y) -> times#(y, s c))
    (loop#(x, c, y) -> if#(lt(x, c), x, c, y), if#(false(), x, c, y) -> loop#(x, s c, times(y, s c)))
    (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)))
    (loop#(x, c, y) -> lt#(x, c), lt#(s x, s y) -> lt#(x, y))}
   STATUS:
    arrows: 0.827160
    SCCS (4):
     Scc:
      {       loop#(x, c, y) -> if#(lt(x, c), x, c, y),
       if#(false(), x, c, y) -> loop#(x, s c, times(y, s c))}
     Scc:
      {times#(s x, y) -> times#(x, y)}
     Scc:
      {plus#(s x, y) -> plus#(x, y)}
     Scc:
      {lt#(s x, s y) -> lt#(x, y)}
     
     
     SCC (2):
      Strict:
       {       loop#(x, c, y) -> if#(lt(x, c), x, c, y),
        if#(false(), x, c, y) -> loop#(x, s c, times(y, s c))}
      Weak:
      {          lt(x, 0()) -> false(),
               lt(0(), s x) -> true(),
               lt(s x, s y) -> lt(x, y),
              times(0(), y) -> 0(),
              times(s x, y) -> plus(y, times(x, y)),
               plus(0(), y) -> y,
               plus(s x, y) -> s plus(x, y),
              loop(x, c, y) -> if(lt(x, c), x, c, y),
                      fac x -> loop(x, s 0(), s 0()),
        if(true(), x, c, y) -> y,
       if(false(), x, c, y) -> loop(x, s c, times(y, s c))}
      Open
     
     SCC (1):
      Strict:
       {times#(s x, y) -> times#(x, y)}
      Weak:
      {          lt(x, 0()) -> false(),
               lt(0(), s x) -> true(),
               lt(s x, s y) -> lt(x, y),
              times(0(), y) -> 0(),
              times(s x, y) -> plus(y, times(x, y)),
               plus(0(), y) -> y,
               plus(s x, y) -> s plus(x, y),
              loop(x, c, y) -> if(lt(x, c), x, c, y),
                      fac x -> loop(x, s 0(), s 0()),
        if(true(), x, c, y) -> y,
       if(false(), x, c, y) -> loop(x, s c, times(y, s c))}
      Open
     
     SCC (1):
      Strict:
       {plus#(s x, y) -> plus#(x, y)}
      Weak:
      {          lt(x, 0()) -> false(),
               lt(0(), s x) -> true(),
               lt(s x, s y) -> lt(x, y),
              times(0(), y) -> 0(),
              times(s x, y) -> plus(y, times(x, y)),
               plus(0(), y) -> y,
               plus(s x, y) -> s plus(x, y),
              loop(x, c, y) -> if(lt(x, c), x, c, y),
                      fac x -> loop(x, s 0(), s 0()),
        if(true(), x, c, y) -> y,
       if(false(), x, c, y) -> loop(x, s c, times(y, s c))}
      Open
     
     SCC (1):
      Strict:
       {lt#(s x, s y) -> lt#(x, y)}
      Weak:
      {          lt(x, 0()) -> false(),
               lt(0(), s x) -> true(),
               lt(s x, s y) -> lt(x, y),
              times(0(), y) -> 0(),
              times(s x, y) -> plus(y, times(x, y)),
               plus(0(), y) -> y,
               plus(s x, y) -> s plus(x, y),
              loop(x, c, y) -> if(lt(x, c), x, c, y),
                      fac x -> loop(x, s 0(), s 0()),
        if(true(), x, c, y) -> y,
       if(false(), x, c, y) -> loop(x, s c, times(y, s c))}
      Open