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