Input TRS:
1: a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
2: f(a(x),a(y)) -> a(f(x,y))
3: f(b(x),b(y)) -> b(f(x,y))
Dependency Pairs:
#1: #a(a(f(x,y))) -> #f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
#2: #a(a(f(x,y))) -> #a(b(a(b(a(x)))))
#3: #a(a(f(x,y))) -> #a(b(a(x)))
#4: #a(a(f(x,y))) -> #a(x)
#5: #a(a(f(x,y))) -> #a(b(a(b(a(y)))))
#6: #a(a(f(x,y))) -> #a(b(a(y)))
#7: #a(a(f(x,y))) -> #a(y)
#8: #f(a(x),a(y)) -> #a(f(x,y))
#9: #f(a(x),a(y)) -> #f(x,y)
#10: #f(b(x),b(y)) -> #f(x,y)
Number of SCCs: 1
SCC { #1 #4 #7 #8 #9 #10 }
QKBOPS(sum)... removes: #4 #7
I(a) = x1 \pi(a) = 1
I(b) = x1 \pi(b) = 1
I(f) = x1 + x2 \pi(f) = [1]
I(#a) = x1 \pi(#a) = 1
I(#f) = x1 + x2 \pi(#f) = [1]
PREC: f = #f
USABLE RULES: { 3..1 }
Number of SCCs: 1
SCC { #1 #8 #9 #10 }
QKBOPS(sum)... failed.