Input TRS:
1: f(a(),x) -> f(x,f(b(),x))
e1: f(f(x,y),z) ->= f(x,f(y,z)) [relative]
e2: f(x,f(y,z)) ->= f(f(x,y),z) [relative]
Number of Rules: 1
Direct POLO(Sum) ...Direct Mat2b ...Direct Mat3b ... failed.
Dependency Pairs:
#1: # f(x,f(y,z)) -> # f(f(x,y),z) [relative]
#2: # f(x,f(y,z)) -> # f(x,y) [relative]
#3: # f(f(x,y),z) -> # f(x,f(y,z)) [relative]
#4: # f(f(x,y),z) -> # f(y,z) [relative]
#5: # f(a(),x) -> # f(x,f(b(),x))
#6: # f(a(),x) -> # f(b(),x)
Number of SCCs: 1
SCC { #1..6 }
POLO(Sum)... QLPOS... QWPOpS(mSum)... Mat3b... failed.