Input TRS: 1: f(f(a(),x),a()) -> f(f(f(x,a()),f(a(),a())),a()) Number of strict rules: 1 Direct Order(PosReal,>,Poly) ... failed. Freezing f 1: f❆2_a(x,a()) -> f(f(f(x,a()),f❆1_a(a())),a()) 2: f(a(),_1) ->= f❆1_a(_1) 3: f(f❆1_a(_1),_2) ->= f❆2_a(_1,_2) Number of strict rules: 1 Direct Order(PosReal,>,Poly) ... failed. Dependency Pairs: #1: #f(f❆1_a(_1),_2) ->? #f❆2_a(_1,_2) #2: #f❆2_a(x,a()) -> #f(f(f(x,a()),f❆1_a(a())),a()) #3: #f❆2_a(x,a()) -> #f(f(x,a()),f❆1_a(a())) #4: #f❆2_a(x,a()) -> #f(x,a()) Number of SCCs: 1, DPs: 4, edges: 6 SCC { #1..4 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. a() weight: (/ 1 2) f❆2_a(x1,x2) weight: 0 #f❆2_a(x1,x2) weight: max{0, (/ 1 4) + x2} f(x1,x2) weight: max{0, x1} #f(x1,x2) weight: max{0, (/ 1 4) + x2} f❆1_a(x1) weight: (/ 1 4) Usable rules: { } Removed DPs: #3 Number of SCCs: 1, DPs: 3, edges: 4 SCC { #1 #2 #4 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded. a() status: [] precedence above: f❆2_a(x1,x2) status: [] precedence above: f #f❆2_a(x1,x2) status: [x1] precedence above: f❆2_a f f❆1_a f(x1,x2) status: [] precedence above: f❆2_a #f(x1,x2) status: x1 f❆1_a(x1) status: [x1] precedence above: f❆2_a #f❆2_a f Usable rules: { 1 3 } Removed DPs: #2 #4 Number of SCCs: 0, DPs: 0, edges: 0 YES