Input TRS: 1: min(x,0()) -> 0() 2: min(0(),y) -> 0() 3: min(s(x),s(y)) -> s(min(x,y)) 4: max(x,0()) -> x 5: max(0(),y) -> y 6: max(s(x),s(y)) -> s(max(x,y)) 7: -(x,0()) -> x 8: -(s(x),s(y)) -> -(x,y) 9: gcd(s(x),s(y)) -> gcd(-(max(x,y),min(x,y)),s(min(x,y))) 10: gcd(s(x),0()) -> s(x) 11: gcd(0(),s(y)) -> s(y) 12: min(x,y) ->= min(y,x) 13: max(x,y) ->= max(y,x) Number of strict rules: 11 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #max(s(x),s(y)) -> #max(x,y) #2: #max(x,y) ->? #max(y,x) #3: #gcd(s(x),s(y)) -> #gcd(-(max(x,y),min(x,y)),s(min(x,y))) #4: #gcd(s(x),s(y)) -> #-(max(x,y),min(x,y)) #5: #gcd(s(x),s(y)) -> #max(x,y) #6: #gcd(s(x),s(y)) -> #min(x,y) #7: #gcd(s(x),s(y)) -> #min(x,y) #8: #min(x,y) ->? #min(y,x) #9: #min(s(x),s(y)) -> #min(x,y) #10: #-(s(x),s(y)) -> #-(x,y) Number of SCCs: 4, DPs: 6, edges: 10 SCC { #10 } Removing DPs: Order(PosReal,>,Sum)... succeeded. s(x1) weight: (/ 1 2) + x1 gcd(x1,x2) weight: 0 #min(x1,x2) weight: 0 0() weight: 0 max(x1,x2) weight: 0 #max(x1,x2) weight: 0 -(x1,x2) weight: 0 min(x1,x2) weight: 0 #-(x1,x2) weight: x2 #gcd(x1,x2) weight: 0 Usable rules: { } Removed DPs: #10 Number of SCCs: 3, DPs: 5, edges: 9 SCC { #1 #2 } Removing DPs: Order(PosReal,>,Sum)... succeeded. s(x1) weight: (/ 1 4) + x1 gcd(x1,x2) weight: 0 #min(x1,x2) weight: 0 0() weight: 0 max(x1,x2) weight: 0 #max(x1,x2) weight: x1 + x2 -(x1,x2) weight: 0 min(x1,x2) weight: 0 #-(x1,x2) weight: 0 #gcd(x1,x2) weight: 0 Usable rules: { } Removed DPs: #1 Number of SCCs: 3, DPs: 4, edges: 6 SCC { #2 } 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