Input TRS: 1: f(0(),Y) -> f(s(Y),s(Y)) 2: f(s(X),Y) -> f(X,Y) Number of strict rules: 2 Direct Order(PosReal,>,Poly) ... failed. Freezing f 1: f❆1_0(Y) -> f❆1_s(Y,s(Y)) 2: f❆1_s(X,Y) -> f(X,Y) 3: f(0(),_1) ->= f❆1_0(_1) 4: f(s(_1),_2) ->= f❆1_s(_1,_2) Number of strict rules: 2 Direct Order(PosReal,>,Poly) ... failed. Dependency Pairs: #1: #f❆1_s(X,Y) -> #f(X,Y) #2: #f(0(),_1) ->? #f❆1_0(_1) #3: #f❆1_0(Y) -> #f❆1_s(Y,s(Y)) #4: #f(s(_1),_2) ->? #f❆1_s(_1,_2) Number of SCCs: 1, DPs: 4, edges: 5 SCC { #1..4 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed. Removing edges: failed. Finding a loop... failed. MAYBE