ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.3: error when applying the reduction pair processor with usable rules to remove from the DP problem
  pairs:
  
  +#(s(x), s(y)) -> +#(x, y)
  +#(+(x, y), z) -> +#(x, +(y, z))
  +#(+(x, y), z) -> +#(y, z)
  rules:
  
  +(x, h) -> x
  +(h, x) -> x
  +(s(x), s(y)) -> s(s(+(x, y)))
  +(+(x, y), z) -> +(x, +(y, z))
  a(h, h, h, x) -> s(x)
  a(l, x, s(y), h) -> a(l, x, y, s(h))
  a(l, x, s(y), s(z)) -> a(l, x, y, a(l, x, s(y), z))
  a(l, s(x), h, z) -> a(l, x, z, z)
  a(s(l), h, h, z) -> a(l, z, h, z)
  app(nil, k) -> k
  app(l, nil) -> l
  app(cons(x, l), k) -> cons(x, app(l, k))
  s(h) -> 1
  sum(cons(x, nil)) -> cons(x, nil)
  sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h, h), l))
  
   the pairs 
  +#(s(x), s(y)) -> +#(x, y)
  +#(+(x, y), z) -> +#(x, +(y, z))
  +#(+(x, y), z) -> +#(y, z)
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MS and the level mapping defined by 
  pi(+#) = [(epsilon,0),(1,1)]
  Argument Filter: 
  pi(+#/2) = []
  pi(+/2) = [2,1]
  pi(s/1) = [1]
  pi(h/0) = []
  pi(1/0) = []
  
  RPO with the following precedence
  precedence(+#[2]) = 1
  precedence(+[2]) = 0
  precedence(s[1]) = 0
  precedence(h[0]) = 2
  precedence(1[0]) = 3
  
  precedence(_) = 0
  and the following status
  status(+#[2]) = lex
  status(+[2]) = lex
  status(s[1]) = lex
  status(h[0]) = lex
  status(1[0]) = lex
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair +#(s(x), s(y)) -> +#(x, y) strictly:
  [(+#(s(x), s(y)),0),(s(x),1)] >mu [(+#(x, y),0),(x,1)] could not be ensured