MAYBE
Time: 0.005566
TRS:
 {                        cons(X1, X2) -> n__cons(X1, X2),
                                from X -> cons(X, n__from s X),
                                from X -> n__from X,
  2ndspos(s N, cons(X, n__cons(Y, Z))) -> rcons(posrecip activate Y, 2ndsneg(N, activate Z)),
                       2ndspos(0(), Z) -> rnil(),
                            activate X -> X,
                    activate n__from X -> from X,
              activate n__cons(X1, X2) -> cons(X1, X2),
  2ndsneg(s N, cons(X, n__cons(Y, Z))) -> rcons(negrecip activate Y, 2ndspos(N, activate Z)),
                       2ndsneg(0(), Z) -> rnil(),
                                  pi X -> 2ndspos(X, from 0()),
                          plus(s X, Y) -> s plus(X, Y),
                          plus(0(), Y) -> Y,
                         times(s X, Y) -> plus(Y, times(X, Y)),
                         times(0(), Y) -> 0(),
                              square X -> times(X, X)}
 DP:
  DP:
   {                              from# X -> cons#(X, n__from s X),
    2ndspos#(s N, cons(X, n__cons(Y, Z))) -> activate# Z,
    2ndspos#(s N, cons(X, n__cons(Y, Z))) -> activate# Y,
    2ndspos#(s N, cons(X, n__cons(Y, Z))) -> 2ndsneg#(N, activate Z),
                      activate# n__from X -> from# X,
                activate# n__cons(X1, X2) -> cons#(X1, X2),
    2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> 2ndspos#(N, activate Z),
    2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> activate# Z,
    2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> activate# Y,
                                    pi# X -> from# 0(),
                                    pi# X -> 2ndspos#(X, from 0()),
                            plus#(s X, Y) -> plus#(X, Y),
                           times#(s X, Y) -> plus#(Y, times(X, Y)),
                           times#(s X, Y) -> times#(X, Y),
                                square# X -> times#(X, X)}
  TRS:
  {                        cons(X1, X2) -> n__cons(X1, X2),
                                 from X -> cons(X, n__from s X),
                                 from X -> n__from X,
   2ndspos(s N, cons(X, n__cons(Y, Z))) -> rcons(posrecip activate Y, 2ndsneg(N, activate Z)),
                        2ndspos(0(), Z) -> rnil(),
                             activate X -> X,
                     activate n__from X -> from X,
               activate n__cons(X1, X2) -> cons(X1, X2),
   2ndsneg(s N, cons(X, n__cons(Y, Z))) -> rcons(negrecip activate Y, 2ndspos(N, activate Z)),
                        2ndsneg(0(), Z) -> rnil(),
                                   pi X -> 2ndspos(X, from 0()),
                           plus(s X, Y) -> s plus(X, Y),
                           plus(0(), Y) -> Y,
                          times(s X, Y) -> plus(Y, times(X, Y)),
                          times(0(), Y) -> 0(),
                               square X -> times(X, X)}
  UR:
   {            cons(X1, X2) -> n__cons(X1, X2),
                      from X -> cons(X, n__from s X),
                      from X -> n__from X,
                  activate X -> X,
          activate n__from X -> from X,
    activate n__cons(X1, X2) -> cons(X1, X2),
                plus(s X, Y) -> s plus(X, Y),
                plus(0(), Y) -> Y,
               times(s X, Y) -> plus(Y, times(X, Y)),
               times(0(), Y) -> 0(),
                     a(x, y) -> x,
                     a(x, y) -> y}
   EDG:
    {(2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> activate# Z, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> activate# Z, activate# n__from X -> from# X)
     (2ndspos#(s N, cons(X, n__cons(Y, Z))) -> 2ndsneg#(N, activate Z), 2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> activate# Y)
     (2ndspos#(s N, cons(X, n__cons(Y, Z))) -> 2ndsneg#(N, activate Z), 2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> activate# Z)
     (2ndspos#(s N, cons(X, n__cons(Y, Z))) -> 2ndsneg#(N, activate Z), 2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> 2ndspos#(N, activate Z))
     (2ndspos#(s N, cons(X, n__cons(Y, Z))) -> activate# Y, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (2ndspos#(s N, cons(X, n__cons(Y, Z))) -> activate# Y, activate# n__from X -> from# X)
     (plus#(s X, Y) -> plus#(X, Y), plus#(s X, Y) -> plus#(X, Y))
     (square# X -> times#(X, X), times#(s X, Y) -> times#(X, Y))
     (square# X -> times#(X, X), times#(s X, Y) -> plus#(Y, times(X, Y)))
     (pi# X -> from# 0(), from# X -> cons#(X, n__from s X))
     (times#(s X, Y) -> times#(X, Y), times#(s X, Y) -> plus#(Y, times(X, Y)))
     (times#(s X, Y) -> times#(X, Y), times#(s X, Y) -> times#(X, Y))
     (activate# n__from X -> from# X, from# X -> cons#(X, n__from s X))
     (2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> activate# Y, activate# n__from X -> from# X)
     (2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> activate# Y, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> 2ndspos#(N, activate Z), 2ndspos#(s N, cons(X, n__cons(Y, Z))) -> activate# Z)
     (2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> 2ndspos#(N, activate Z), 2ndspos#(s N, cons(X, n__cons(Y, Z))) -> activate# Y)
     (2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> 2ndspos#(N, activate Z), 2ndspos#(s N, cons(X, n__cons(Y, Z))) -> 2ndsneg#(N, activate Z))
     (times#(s X, Y) -> plus#(Y, times(X, Y)), plus#(s X, Y) -> plus#(X, Y))
     (2ndspos#(s N, cons(X, n__cons(Y, Z))) -> activate# Z, activate# n__from X -> from# X)
     (2ndspos#(s N, cons(X, n__cons(Y, Z))) -> activate# Z, activate# n__cons(X1, X2) -> cons#(X1, X2))}
    STATUS:
     arrows: 0.902222
     SCCS (3):
      Scc:
       {times#(s X, Y) -> times#(X, Y)}
      Scc:
       {2ndspos#(s N, cons(X, n__cons(Y, Z))) -> 2ndsneg#(N, activate Z),
        2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> 2ndspos#(N, activate Z)}
      Scc:
       {plus#(s X, Y) -> plus#(X, Y)}
      
      
      
      SCC (1):
       Strict:
        {times#(s X, Y) -> times#(X, Y)}
       Weak:
       {                        cons(X1, X2) -> n__cons(X1, X2),
                                      from X -> cons(X, n__from s X),
                                      from X -> n__from X,
        2ndspos(s N, cons(X, n__cons(Y, Z))) -> rcons(posrecip activate Y, 2ndsneg(N, activate Z)),
                             2ndspos(0(), Z) -> rnil(),
                                  activate X -> X,
                          activate n__from X -> from X,
                    activate n__cons(X1, X2) -> cons(X1, X2),
        2ndsneg(s N, cons(X, n__cons(Y, Z))) -> rcons(negrecip activate Y, 2ndspos(N, activate Z)),
                             2ndsneg(0(), Z) -> rnil(),
                                        pi X -> 2ndspos(X, from 0()),
                                plus(s X, Y) -> s plus(X, Y),
                                plus(0(), Y) -> Y,
                               times(s X, Y) -> plus(Y, times(X, Y)),
                               times(0(), Y) -> 0(),
                                    square X -> times(X, X)}
       Open
      SCC (2):
       Strict:
        {2ndspos#(s N, cons(X, n__cons(Y, Z))) -> 2ndsneg#(N, activate Z),
         2ndsneg#(s N, cons(X, n__cons(Y, Z))) -> 2ndspos#(N, activate Z)}
       Weak:
       {                        cons(X1, X2) -> n__cons(X1, X2),
                                      from X -> cons(X, n__from s X),
                                      from X -> n__from X,
        2ndspos(s N, cons(X, n__cons(Y, Z))) -> rcons(posrecip activate Y, 2ndsneg(N, activate Z)),
                             2ndspos(0(), Z) -> rnil(),
                                  activate X -> X,
                          activate n__from X -> from X,
                    activate n__cons(X1, X2) -> cons(X1, X2),
        2ndsneg(s N, cons(X, n__cons(Y, Z))) -> rcons(negrecip activate Y, 2ndspos(N, activate Z)),
                             2ndsneg(0(), Z) -> rnil(),
                                        pi X -> 2ndspos(X, from 0()),
                                plus(s X, Y) -> s plus(X, Y),
                                plus(0(), Y) -> Y,
                               times(s X, Y) -> plus(Y, times(X, Y)),
                               times(0(), Y) -> 0(),
                                    square X -> times(X, X)}
       Open
      
      
      
      
      SCC (1):
       Strict:
        {plus#(s X, Y) -> plus#(X, Y)}
       Weak:
       {                        cons(X1, X2) -> n__cons(X1, X2),
                                      from X -> cons(X, n__from s X),
                                      from X -> n__from X,
        2ndspos(s N, cons(X, n__cons(Y, Z))) -> rcons(posrecip activate Y, 2ndsneg(N, activate Z)),
                             2ndspos(0(), Z) -> rnil(),
                                  activate X -> X,
                          activate n__from X -> from X,
                    activate n__cons(X1, X2) -> cons(X1, X2),
        2ndsneg(s N, cons(X, n__cons(Y, Z))) -> rcons(negrecip activate Y, 2ndspos(N, activate Z)),
                             2ndsneg(0(), Z) -> rnil(),
                                        pi X -> 2ndspos(X, from 0()),
                                plus(s X, Y) -> s plus(X, Y),
                                plus(0(), Y) -> Y,
                               times(s X, Y) -> plus(Y, times(X, Y)),
                               times(0(), Y) -> 0(),
                                    square X -> times(X, X)}
       Open