Input TRS: 1: active(U11(tt(),M,N)) -> mark(U12(tt(),M,N)) 2: active(U12(tt(),M,N)) -> mark(s(plus(N,M))) 3: active(U21(tt(),M,N)) -> mark(U22(tt(),M,N)) 4: active(U22(tt(),M,N)) -> mark(plus(x(N,M),N)) 5: active(plus(N,0())) -> mark(N) 6: active(plus(N,s(M))) -> mark(U11(tt(),M,N)) 7: active(x(N,0())) -> mark(0()) 8: active(x(N,s(M))) -> mark(U21(tt(),M,N)) 9: mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3)) 10: mark(tt()) -> active(tt()) 11: mark(U12(X1,X2,X3)) -> active(U12(mark(X1),X2,X3)) 12: mark(s(X)) -> active(s(mark(X))) 13: mark(plus(X1,X2)) -> active(plus(mark(X1),mark(X2))) 14: mark(U21(X1,X2,X3)) -> active(U21(mark(X1),X2,X3)) 15: mark(U22(X1,X2,X3)) -> active(U22(mark(X1),X2,X3)) 16: mark(x(X1,X2)) -> active(x(mark(X1),mark(X2))) 17: mark(0()) -> active(0()) 18: U11(mark(X1),X2,X3) -> U11(X1,X2,X3) 19: U11(X1,mark(X2),X3) -> U11(X1,X2,X3) 20: U11(X1,X2,mark(X3)) -> U11(X1,X2,X3) 21: U11(active(X1),X2,X3) -> U11(X1,X2,X3) 22: U11(X1,active(X2),X3) -> U11(X1,X2,X3) 23: U11(X1,X2,active(X3)) -> U11(X1,X2,X3) 24: U12(mark(X1),X2,X3) -> U12(X1,X2,X3) 25: U12(X1,mark(X2),X3) -> U12(X1,X2,X3) 26: U12(X1,X2,mark(X3)) -> U12(X1,X2,X3) 27: U12(active(X1),X2,X3) -> U12(X1,X2,X3) 28: U12(X1,active(X2),X3) -> U12(X1,X2,X3) 29: U12(X1,X2,active(X3)) -> U12(X1,X2,X3) 30: s(mark(X)) -> s(X) 31: s(active(X)) -> s(X) 32: plus(mark(X1),X2) -> plus(X1,X2) 33: plus(X1,mark(X2)) -> plus(X1,X2) 34: plus(active(X1),X2) -> plus(X1,X2) 35: plus(X1,active(X2)) -> plus(X1,X2) 36: U21(mark(X1),X2,X3) -> U21(X1,X2,X3) 37: U21(X1,mark(X2),X3) -> U21(X1,X2,X3) 38: U21(X1,X2,mark(X3)) -> U21(X1,X2,X3) 39: U21(active(X1),X2,X3) -> U21(X1,X2,X3) 40: U21(X1,active(X2),X3) -> U21(X1,X2,X3) 41: U21(X1,X2,active(X3)) -> U21(X1,X2,X3) 42: U22(mark(X1),X2,X3) -> U22(X1,X2,X3) 43: U22(X1,mark(X2),X3) -> U22(X1,X2,X3) 44: U22(X1,X2,mark(X3)) -> U22(X1,X2,X3) 45: U22(active(X1),X2,X3) -> U22(X1,X2,X3) 46: U22(X1,active(X2),X3) -> U22(X1,X2,X3) 47: U22(X1,X2,active(X3)) -> U22(X1,X2,X3) 48: x(mark(X1),X2) -> x(X1,X2) 49: x(X1,mark(X2)) -> x(X1,X2) 50: x(active(X1),X2) -> x(X1,X2) 51: x(X1,active(X2)) -> x(X1,X2) Number of strict rules: 51 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #active(U12(tt(),M,N)) -> #mark(s(plus(N,M))) #2: #active(U12(tt(),M,N)) -> #s(plus(N,M)) #3: #active(U12(tt(),M,N)) -> #plus(N,M) #4: #U22(X1,mark(X2),X3) -> #U22(X1,X2,X3) #5: #U12(X1,X2,active(X3)) -> #U12(X1,X2,X3) #6: #plus(X1,active(X2)) -> #plus(X1,X2) #7: #U22(X1,active(X2),X3) -> #U22(X1,X2,X3) #8: #U22(mark(X1),X2,X3) -> #U22(X1,X2,X3) #9: #U21(X1,X2,active(X3)) -> #U21(X1,X2,X3) #10: #U21(X1,mark(X2),X3) -> #U21(X1,X2,X3) #11: #U22(X1,X2,active(X3)) -> #U22(X1,X2,X3) #12: #x(mark(X1),X2) -> #x(X1,X2) #13: #U21(X1,X2,mark(X3)) -> #U21(X1,X2,X3) #14: #active(plus(N,s(M))) -> #mark(U11(tt(),M,N)) #15: #active(plus(N,s(M))) -> #U11(tt(),M,N) #16: #U21(X1,active(X2),X3) -> #U21(X1,X2,X3) #17: #x(X1,active(X2)) -> #x(X1,X2) #18: #mark(plus(X1,X2)) -> #active(plus(mark(X1),mark(X2))) #19: #mark(plus(X1,X2)) -> #plus(mark(X1),mark(X2)) #20: #mark(plus(X1,X2)) -> #mark(X1) #21: #mark(plus(X1,X2)) -> #mark(X2) #22: #mark(U11(X1,X2,X3)) -> #active(U11(mark(X1),X2,X3)) #23: #mark(U11(X1,X2,X3)) -> #U11(mark(X1),X2,X3) #24: #mark(U11(X1,X2,X3)) -> #mark(X1) #25: #mark(U12(X1,X2,X3)) -> #active(U12(mark(X1),X2,X3)) #26: #mark(U12(X1,X2,X3)) -> #U12(mark(X1),X2,X3) #27: #mark(U12(X1,X2,X3)) -> #mark(X1) #28: #U12(mark(X1),X2,X3) -> #U12(X1,X2,X3) #29: #U11(X1,X2,active(X3)) -> #U11(X1,X2,X3) #30: #U22(active(X1),X2,X3) -> #U22(X1,X2,X3) #31: #mark(s(X)) -> #active(s(mark(X))) #32: #mark(s(X)) -> #s(mark(X)) #33: #mark(s(X)) -> #mark(X) #34: #s(active(X)) -> #s(X) #35: #mark(U21(X1,X2,X3)) -> #active(U21(mark(X1),X2,X3)) #36: #mark(U21(X1,X2,X3)) -> #U21(mark(X1),X2,X3) #37: #mark(U21(X1,X2,X3)) -> #mark(X1) #38: #s(mark(X)) -> #s(X) #39: #x(X1,mark(X2)) -> #x(X1,X2) #40: #U12(X1,mark(X2),X3) -> #U12(X1,X2,X3) #41: #U11(X1,X2,mark(X3)) -> #U11(X1,X2,X3) #42: #active(x(N,0())) -> #mark(0()) #43: #U21(active(X1),X2,X3) -> #U21(X1,X2,X3) #44: #mark(tt()) -> #active(tt()) #45: #plus(X1,mark(X2)) -> #plus(X1,X2) #46: #active(plus(N,0())) -> #mark(N) #47: #U22(X1,X2,mark(X3)) -> #U22(X1,X2,X3) #48: #U12(X1,active(X2),X3) -> #U12(X1,X2,X3) #49: #U11(X1,active(X2),X3) -> #U11(X1,X2,X3) #50: #plus(active(X1),X2) -> #plus(X1,X2) #51: #U12(active(X1),X2,X3) -> #U12(X1,X2,X3) #52: #mark(0()) -> #active(0()) #53: #plus(mark(X1),X2) -> #plus(X1,X2) #54: #U11(X1,mark(X2),X3) -> #U11(X1,X2,X3) #55: #U12(X1,X2,mark(X3)) -> #U12(X1,X2,X3) #56: #U21(mark(X1),X2,X3) -> #U21(X1,X2,X3) #57: #U11(active(X1),X2,X3) -> #U11(X1,X2,X3) #58: #mark(x(X1,X2)) -> #active(x(mark(X1),mark(X2))) #59: #mark(x(X1,X2)) -> #x(mark(X1),mark(X2)) #60: #mark(x(X1,X2)) -> #mark(X1) #61: #mark(x(X1,X2)) -> #mark(X2) #62: #active(U21(tt(),M,N)) -> #mark(U22(tt(),M,N)) #63: #active(U21(tt(),M,N)) -> #U22(tt(),M,N) #64: #active(U11(tt(),M,N)) -> #mark(U12(tt(),M,N)) #65: #active(U11(tt(),M,N)) -> #U12(tt(),M,N) #66: #active(x(N,s(M))) -> #mark(U21(tt(),M,N)) #67: #active(x(N,s(M))) -> #U21(tt(),M,N) #68: #mark(U22(X1,X2,X3)) -> #active(U22(mark(X1),X2,X3)) #69: #mark(U22(X1,X2,X3)) -> #U22(mark(X1),X2,X3) #70: #mark(U22(X1,X2,X3)) -> #mark(X1) #71: #active(U22(tt(),M,N)) -> #mark(plus(x(N,M),N)) #72: #active(U22(tt(),M,N)) -> #plus(x(N,M),N) #73: #active(U22(tt(),M,N)) -> #x(N,M) #74: #x(active(X1),X2) -> #x(X1,X2) #75: #U11(mark(X1),X2,X3) -> #U11(X1,X2,X3) Number of SCCs: 8, DPs: 56, edges: 349 SCC { #34 #38 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: 0 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: 0 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: 0 #s(x1) weight: x1 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2,x3) weight: 0 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #34 #38 Number of SCCs: 7, DPs: 54, edges: 345 SCC { #12 #17 #39 #74 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: 0 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: 0 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: x1 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2,x3) weight: 0 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #12 #74 Number of SCCs: 7, DPs: 52, edges: 333 SCC { #17 #39 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: 0 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: 0 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: x2 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2,x3) weight: 0 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #17 #39 Number of SCCs: 6, DPs: 50, edges: 329 SCC { #6 #45 #50 #53 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: x2 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: 0 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2,x3) weight: 0 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #6 #45 Number of SCCs: 7, DPs: 48, edges: 317 SCC { #50 #53 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: x1 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: 0 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2,x3) weight: 0 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #50 #53 Number of SCCs: 6, DPs: 46, edges: 313 SCC { #4 #7 #8 #11 #30 #47 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: 0 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: 0 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2,x3) weight: x1 + x3 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #8 #11 #30 #47 Number of SCCs: 7, DPs: 42, edges: 281 SCC { #4 #7 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: 0 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: 0 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2,x3) weight: x2 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #4 #7 Number of SCCs: 6, DPs: 40, edges: 277 SCC { #9 #10 #13 #16 #43 #56 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: 0 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: 0 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: x2 + x3 #U22(x1,x2,x3) weight: 0 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #9 #10 #13 #16 Number of SCCs: 7, DPs: 36, edges: 245 SCC { #43 #56 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: 0 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: 0 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: x1 #U22(x1,x2,x3) weight: 0 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #43 #56 Number of SCCs: 6, DPs: 34, edges: 241 SCC { #5 #28 #40 #48 #51 #55 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: 0 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: x1 + x2 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2,x3) weight: 0 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #28 #40 #48 #51 Number of SCCs: 7, DPs: 30, edges: 209 SCC { #5 #55 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: 0 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: x3 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: 0 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2,x3) weight: 0 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #5 #55 Number of SCCs: 6, DPs: 28, edges: 205 SCC { #29 #41 #49 #54 #57 #75 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: 0 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: 0 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: x1 + x2 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2,x3) weight: 0 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #49 #54 #57 #75 Number of SCCs: 7, DPs: 24, edges: 173 SCC { #29 #41 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3) weight: 0 U11(x1,x2,x3) weight: 0 s(x1) weight: 0 #plus(x1,x2) weight: 0 U12(x1,x2,x3) weight: 0 x(x1,x2) weight: 0 #U12(x1,x2,x3) weight: 0 #mark(x1) weight: 0 0() weight: 0 #x(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: (/ 1 2) + x1 plus(x1,x2) weight: 0 #U11(x1,x2,x3) weight: x3 active(x1) weight: (/ 1 2) + x1 #active(x1) weight: 0 #U21(x1,x2,x3) weight: 0 #U22(x1,x2,x3) weight: 0 tt() weight: 0 U22(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #29 #41 Number of SCCs: 6, DPs: 22, edges: 169 SCC { #1 #14 #18 #20..22 #24 #25 #27 #33 #35 #37 #46 #58 #60..62 #64 #66 #68 #70 #71 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. U21(x1,x2,x3) weight: max{31892 + x3, (/ 1 4) + x2, (/ 127567 4) + x1} U11(x1,x2,x3) weight: max{x3, 31892 + x2, (/ 127567 4) + x1} s(x1) weight: x1 #plus(x1,x2) weight: 0 U12(x1,x2,x3) weight: max{x3, 31892 + x2, (/ 1 4) + x1} x(x1,x2) weight: max{(/ 1 4) + x2, 31892 + x1} #U12(x1,x2,x3) weight: 0 #mark(x1) weight: x1 0() weight: (/ 127569 4) #x(x1,x2) weight: 0 #s(x1) weight: 0 mark(x1) weight: x1 plus(x1,x2) weight: max{31892 + x2, x1} #U11(x1,x2,x3) weight: 0 active(x1) weight: x1 #active(x1) weight: x1 #U21(x1,x2,x3) weight: 0 #U22(x1,x2,x3) weight: 0 tt() weight: (/ 1 4) U22(x1,x2,x3) weight: max{31892 + x3, (/ 1 4) + x2, (/ 63783 2) + x1} Usable rules: { 1..51 } Removed DPs: #21 #24 #27 #37 #60 #61 #70 Number of SCCs: 7, DPs: 15, edges: 38 SCC { #1 #14 #18 #20 #22 #25 #33 #35 #46 #58 #62 #64 #66 #68 #71 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded. U21(x1,x2,x3) status: [x3,x2,x1] precedence above: U11 s U12 x #mark 0 mark plus active #active tt U22 U11(x1,x2,x3) status: [x2,x3,x1] precedence above: s U12 plus active tt s(x1) status: [x1] precedence above: active tt #plus(x1,x2) status: [x1] precedence above: U12(x1,x2,x3) status: [x2,x3,x1] precedence above: U11 s plus active tt x(x1,x2) status: [x1,x2] precedence above: U21 U11 s U12 #mark 0 mark plus active #active tt U22 #U12(x1,x2,x3) status: [x2,x3] precedence above: #mark(x1) status: [x1] precedence above: U11 s U12 mark plus active #active tt 0() status: [] precedence above: #x(x1,x2) status: [x2] precedence above: #s(x1) status: [] precedence above: mark(x1) status: x1 plus(x1,x2) status: [x2,x1] precedence above: U11 s U12 active tt #U11(x1,x2,x3) status: [x1,x3,x2] precedence above: active(x1) status: x1 #active(x1) status: [x1] precedence above: U11 s U12 #mark mark plus active tt #U21(x1,x2,x3) status: [x3,x1,x2] precedence above: #U22(x1,x2,x3) status: [x3] precedence above: tt() status: [] precedence above: U22(x1,x2,x3) status: [x3,x2,x1] precedence above: U21 U11 s U12 x #mark 0 mark plus active #active tt Usable rules: { 1..51 } Removed DPs: #20 #33 #46 #66 #71 Number of SCCs: 6, DPs: 0, edges: 0 YES