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