MAYBE
Time: 0.011580
TRS:
 {                          from X -> cons(X, n__from n__s X),
                            from X -> n__from X,
             sel(0(), cons(X, XS)) -> X,
             sel(s N, cons(X, XS)) -> sel(N, activate XS),
                        activate X -> X,
                activate n__from X -> from activate X,
                   activate n__s X -> s activate X,
        activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2),
                               s X -> n__s X,
                     minus(X, 0()) -> 0(),
                   minus(s X, s Y) -> minus(X, Y),
                    quot(0(), s Y) -> 0(),
                    quot(s X, s Y) -> s quot(minus(X, Y), s Y),
                 zWquot(XS, nil()) -> nil(),
                    zWquot(X1, X2) -> n__zWquot(X1, X2),
  zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)),
                 zWquot(nil(), XS) -> nil()}
 DP:
  DP:
   {           sel#(s N, cons(X, XS)) -> sel#(N, activate XS),
               sel#(s N, cons(X, XS)) -> activate# XS,
                  activate# n__from X -> from# activate X,
                  activate# n__from X -> activate# X,
                     activate# n__s X -> activate# X,
                     activate# n__s X -> s# activate X,
          activate# n__zWquot(X1, X2) -> activate# X1,
          activate# n__zWquot(X1, X2) -> activate# X2,
          activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2),
                     minus#(s X, s Y) -> minus#(X, Y),
                      quot#(s X, s Y) -> s# quot(minus(X, Y), s Y),
                      quot#(s X, s Y) -> minus#(X, Y),
                      quot#(s X, s Y) -> quot#(minus(X, Y), s Y),
    zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS,
    zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS,
    zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)}
  TRS:
  {                          from X -> cons(X, n__from n__s X),
                             from X -> n__from X,
              sel(0(), cons(X, XS)) -> X,
              sel(s N, cons(X, XS)) -> sel(N, activate XS),
                         activate X -> X,
                 activate n__from X -> from activate X,
                    activate n__s X -> s activate X,
         activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2),
                                s X -> n__s X,
                      minus(X, 0()) -> 0(),
                    minus(s X, s Y) -> minus(X, Y),
                     quot(0(), s Y) -> 0(),
                     quot(s X, s Y) -> s quot(minus(X, Y), s Y),
                  zWquot(XS, nil()) -> nil(),
                     zWquot(X1, X2) -> n__zWquot(X1, X2),
   zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)),
                  zWquot(nil(), XS) -> nil()}
  UR:
   {                          from X -> cons(X, n__from n__s X),
                              from X -> n__from X,
                          activate X -> X,
                  activate n__from X -> from activate X,
                     activate n__s X -> s activate X,
          activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2),
                                 s X -> n__s X,
                       minus(X, 0()) -> 0(),
                     minus(s X, s Y) -> minus(X, Y),
                      quot(0(), s Y) -> 0(),
                      quot(s X, s Y) -> s quot(minus(X, Y), s Y),
                   zWquot(XS, nil()) -> nil(),
                      zWquot(X1, X2) -> n__zWquot(X1, X2),
    zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)),
                   zWquot(nil(), XS) -> nil(),
                             a(x, y) -> x,
                             a(x, y) -> y}
   EDG:
    {(activate# n__s X -> activate# X, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2))
     (activate# n__s X -> activate# X, activate# n__zWquot(X1, X2) -> activate# X2)
     (activate# n__s X -> activate# X, activate# n__zWquot(X1, X2) -> activate# X1)
     (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__from X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__from X -> from# activate X)
     (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2))
     (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__zWquot(X1, X2) -> activate# X2)
     (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__zWquot(X1, X2) -> activate# X1)
     (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__s X -> s# activate X)
     (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__s X -> activate# X)
     (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__from X -> activate# X)
     (sel#(s N, cons(X, XS)) -> activate# XS, activate# n__from X -> from# activate X)
     (sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> activate# XS)
     (sel#(s N, cons(X, XS)) -> sel#(N, activate XS), sel#(s N, cons(X, XS)) -> sel#(N, activate XS))
     (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> quot#(minus(X, Y), s Y))
     (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> minus#(X, Y))
     (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> s# quot(minus(X, Y), s Y))
     (minus#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> minus#(X, Y))
     (zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), quot#(s X, s Y) -> quot#(minus(X, Y), s Y))
     (zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), quot#(s X, s Y) -> minus#(X, Y))
     (zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), quot#(s X, s Y) -> s# quot(minus(X, Y), s Y))
     (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__from X -> from# activate X)
     (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__from X -> activate# X)
     (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__s X -> activate# X)
     (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__s X -> s# activate X)
     (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__zWquot(X1, X2) -> activate# X1)
     (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__zWquot(X1, X2) -> activate# X2)
     (activate# n__zWquot(X1, X2) -> activate# X2, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2))
     (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, s Y) -> minus#(X, Y))
     (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__from X -> from# activate X)
     (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__from X -> activate# X)
     (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
     (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
     (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__zWquot(X1, X2) -> activate# X1)
     (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__zWquot(X1, X2) -> activate# X2)
     (activate# n__zWquot(X1, X2) -> activate# X1, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2))
     (activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2), zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS)
     (activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2), zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS)
     (activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2), zWquot#(cons(X, XS), cons(Y, YS)) -> quot#(X, Y))
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__from X -> from# activate X)
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__from X -> activate# X)
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__s X -> activate# X)
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__s X -> s# activate X)
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__zWquot(X1, X2) -> activate# X1)
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__zWquot(X1, X2) -> activate# X2)
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2))
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__from X -> from# activate X)
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__from X -> activate# X)
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__s X -> activate# X)
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__s X -> s# activate X)
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__zWquot(X1, X2) -> activate# X1)
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__zWquot(X1, X2) -> activate# X2)
     (zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2))
     (activate# n__from X -> activate# X, activate# n__from X -> from# activate X)
     (activate# n__from X -> activate# X, activate# n__from X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__from X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__from X -> activate# X, activate# n__zWquot(X1, X2) -> activate# X1)
     (activate# n__from X -> activate# X, activate# n__zWquot(X1, X2) -> activate# X2)
     (activate# n__from X -> activate# X, activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2))}
    STATUS:
     arrows: 0.757812
     SCCS (4):
      Scc:
       {sel#(s N, cons(X, XS)) -> sel#(N, activate XS)}
      Scc:
       {              activate# n__from X -> activate# X,
                         activate# n__s X -> activate# X,
              activate# n__zWquot(X1, X2) -> activate# X1,
              activate# n__zWquot(X1, X2) -> activate# X2,
              activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2),
        zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS,
        zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS}
      Scc:
       {quot#(s X, s Y) -> quot#(minus(X, Y), s Y)}
      Scc:
       {minus#(s X, s Y) -> minus#(X, Y)}
      
      SCC (1):
       Strict:
        {sel#(s N, cons(X, XS)) -> sel#(N, activate XS)}
       Weak:
       {                          from X -> cons(X, n__from n__s X),
                                  from X -> n__from X,
                   sel(0(), cons(X, XS)) -> X,
                   sel(s N, cons(X, XS)) -> sel(N, activate XS),
                              activate X -> X,
                      activate n__from X -> from activate X,
                         activate n__s X -> s activate X,
              activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2),
                                     s X -> n__s X,
                           minus(X, 0()) -> 0(),
                         minus(s X, s Y) -> minus(X, Y),
                          quot(0(), s Y) -> 0(),
                          quot(s X, s Y) -> s quot(minus(X, Y), s Y),
                       zWquot(XS, nil()) -> nil(),
                          zWquot(X1, X2) -> n__zWquot(X1, X2),
        zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)),
                       zWquot(nil(), XS) -> nil()}
       Open
      
      SCC (7):
       Strict:
        {              activate# n__from X -> activate# X,
                          activate# n__s X -> activate# X,
               activate# n__zWquot(X1, X2) -> activate# X1,
               activate# n__zWquot(X1, X2) -> activate# X2,
               activate# n__zWquot(X1, X2) -> zWquot#(activate X1, activate X2),
         zWquot#(cons(X, XS), cons(Y, YS)) -> activate# XS,
         zWquot#(cons(X, XS), cons(Y, YS)) -> activate# YS}
       Weak:
       {                          from X -> cons(X, n__from n__s X),
                                  from X -> n__from X,
                   sel(0(), cons(X, XS)) -> X,
                   sel(s N, cons(X, XS)) -> sel(N, activate XS),
                              activate X -> X,
                      activate n__from X -> from activate X,
                         activate n__s X -> s activate X,
              activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2),
                                     s X -> n__s X,
                           minus(X, 0()) -> 0(),
                         minus(s X, s Y) -> minus(X, Y),
                          quot(0(), s Y) -> 0(),
                          quot(s X, s Y) -> s quot(minus(X, Y), s Y),
                       zWquot(XS, nil()) -> nil(),
                          zWquot(X1, X2) -> n__zWquot(X1, X2),
        zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)),
                       zWquot(nil(), XS) -> nil()}
       Open
      
      SCC (1):
       Strict:
        {quot#(s X, s Y) -> quot#(minus(X, Y), s Y)}
       Weak:
       {                          from X -> cons(X, n__from n__s X),
                                  from X -> n__from X,
                   sel(0(), cons(X, XS)) -> X,
                   sel(s N, cons(X, XS)) -> sel(N, activate XS),
                              activate X -> X,
                      activate n__from X -> from activate X,
                         activate n__s X -> s activate X,
              activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2),
                                     s X -> n__s X,
                           minus(X, 0()) -> 0(),
                         minus(s X, s Y) -> minus(X, Y),
                          quot(0(), s Y) -> 0(),
                          quot(s X, s Y) -> s quot(minus(X, Y), s Y),
                       zWquot(XS, nil()) -> nil(),
                          zWquot(X1, X2) -> n__zWquot(X1, X2),
        zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)),
                       zWquot(nil(), XS) -> nil()}
       Open
      
      SCC (1):
       Strict:
        {minus#(s X, s Y) -> minus#(X, Y)}
       Weak:
       {                          from X -> cons(X, n__from n__s X),
                                  from X -> n__from X,
                   sel(0(), cons(X, XS)) -> X,
                   sel(s N, cons(X, XS)) -> sel(N, activate XS),
                              activate X -> X,
                      activate n__from X -> from activate X,
                         activate n__s X -> s activate X,
              activate n__zWquot(X1, X2) -> zWquot(activate X1, activate X2),
                                     s X -> n__s X,
                           minus(X, 0()) -> 0(),
                         minus(s X, s Y) -> minus(X, Y),
                          quot(0(), s Y) -> 0(),
                          quot(s X, s Y) -> s quot(minus(X, Y), s Y),
                       zWquot(XS, nil()) -> nil(),
                          zWquot(X1, X2) -> n__zWquot(X1, X2),
        zWquot(cons(X, XS), cons(Y, YS)) -> cons(quot(X, Y), n__zWquot(activate XS, activate YS)),
                       zWquot(nil(), XS) -> nil()}
       Open