Input TRS: 1: active(zeros()) -> mark(cons(0(),zeros())) 2: active(U11(tt(),L)) -> mark(U12(tt(),L)) 3: active(U12(tt(),L)) -> mark(s(length(L))) 4: active(U21(tt(),IL,M,N)) -> mark(U22(tt(),IL,M,N)) 5: active(U22(tt(),IL,M,N)) -> mark(U23(tt(),IL,M,N)) 6: active(U23(tt(),IL,M,N)) -> mark(cons(N,take(M,IL))) 7: active(length(nil())) -> mark(0()) 8: active(length(cons(N,L))) -> mark(U11(tt(),L)) 9: active(take(0(),IL)) -> mark(nil()) 10: active(take(s(M),cons(N,IL))) -> mark(U21(tt(),IL,M,N)) 11: mark(zeros()) -> active(zeros()) 12: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 13: mark(0()) -> active(0()) 14: mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) 15: mark(tt()) -> active(tt()) 16: mark(U12(X1,X2)) -> active(U12(mark(X1),X2)) 17: mark(s(X)) -> active(s(mark(X))) 18: mark(length(X)) -> active(length(mark(X))) 19: mark(U21(X1,X2,X3,X4)) -> active(U21(mark(X1),X2,X3,X4)) 20: mark(U22(X1,X2,X3,X4)) -> active(U22(mark(X1),X2,X3,X4)) 21: mark(U23(X1,X2,X3,X4)) -> active(U23(mark(X1),X2,X3,X4)) 22: mark(take(X1,X2)) -> active(take(mark(X1),mark(X2))) 23: mark(nil()) -> active(nil()) 24: cons(mark(X1),X2) -> cons(X1,X2) 25: cons(X1,mark(X2)) -> cons(X1,X2) 26: cons(active(X1),X2) -> cons(X1,X2) 27: cons(X1,active(X2)) -> cons(X1,X2) 28: U11(mark(X1),X2) -> U11(X1,X2) 29: U11(X1,mark(X2)) -> U11(X1,X2) 30: U11(active(X1),X2) -> U11(X1,X2) 31: U11(X1,active(X2)) -> U11(X1,X2) 32: U12(mark(X1),X2) -> U12(X1,X2) 33: U12(X1,mark(X2)) -> U12(X1,X2) 34: U12(active(X1),X2) -> U12(X1,X2) 35: U12(X1,active(X2)) -> U12(X1,X2) 36: s(mark(X)) -> s(X) 37: s(active(X)) -> s(X) 38: length(mark(X)) -> length(X) 39: length(active(X)) -> length(X) 40: U21(mark(X1),X2,X3,X4) -> U21(X1,X2,X3,X4) 41: U21(X1,mark(X2),X3,X4) -> U21(X1,X2,X3,X4) 42: U21(X1,X2,mark(X3),X4) -> U21(X1,X2,X3,X4) 43: U21(X1,X2,X3,mark(X4)) -> U21(X1,X2,X3,X4) 44: U21(active(X1),X2,X3,X4) -> U21(X1,X2,X3,X4) 45: U21(X1,active(X2),X3,X4) -> U21(X1,X2,X3,X4) 46: U21(X1,X2,active(X3),X4) -> U21(X1,X2,X3,X4) 47: U21(X1,X2,X3,active(X4)) -> U21(X1,X2,X3,X4) 48: U22(mark(X1),X2,X3,X4) -> U22(X1,X2,X3,X4) 49: U22(X1,mark(X2),X3,X4) -> U22(X1,X2,X3,X4) 50: U22(X1,X2,mark(X3),X4) -> U22(X1,X2,X3,X4) 51: U22(X1,X2,X3,mark(X4)) -> U22(X1,X2,X3,X4) 52: U22(active(X1),X2,X3,X4) -> U22(X1,X2,X3,X4) 53: U22(X1,active(X2),X3,X4) -> U22(X1,X2,X3,X4) 54: U22(X1,X2,active(X3),X4) -> U22(X1,X2,X3,X4) 55: U22(X1,X2,X3,active(X4)) -> U22(X1,X2,X3,X4) 56: U23(mark(X1),X2,X3,X4) -> U23(X1,X2,X3,X4) 57: U23(X1,mark(X2),X3,X4) -> U23(X1,X2,X3,X4) 58: U23(X1,X2,mark(X3),X4) -> U23(X1,X2,X3,X4) 59: U23(X1,X2,X3,mark(X4)) -> U23(X1,X2,X3,X4) 60: U23(active(X1),X2,X3,X4) -> U23(X1,X2,X3,X4) 61: U23(X1,active(X2),X3,X4) -> U23(X1,X2,X3,X4) 62: U23(X1,X2,active(X3),X4) -> U23(X1,X2,X3,X4) 63: U23(X1,X2,X3,active(X4)) -> U23(X1,X2,X3,X4) 64: take(mark(X1),X2) -> take(X1,X2) 65: take(X1,mark(X2)) -> take(X1,X2) 66: take(active(X1),X2) -> take(X1,X2) 67: take(X1,active(X2)) -> take(X1,X2) Number of strict rules: 67 Direct Order(PosReal,>,Poly) ... removes: 7 9 U21(x1,x2,x3,x4) weight: (/ 1 8) + x1 + x2 + x3 + x4 U11(x1,x2) weight: (/ 1 8) + x1 + x2 s(x1) weight: x1 take(x1,x2) weight: (/ 1 8) + x1 + x2 U23(x1,x2,x3,x4) weight: (/ 1 8) + x1 + x2 + x3 + x4 zeros() weight: 0 U12(x1,x2) weight: (/ 1 8) + x1 + x2 0() weight: 0 nil() weight: 0 mark(x1) weight: x1 active(x1) weight: x1 cons(x1,x2) weight: x1 + x2 tt() weight: 0 U22(x1,x2,x3,x4) weight: (/ 1 8) + x1 + x2 + x3 + x4 length(x1) weight: (/ 1 8) + x1 Number of strict rules: 65 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #active(U11(tt(),L)) -> #mark(U12(tt(),L)) #2: #active(U11(tt(),L)) -> #U12(tt(),L) #3: #U21(X1,X2,X3,mark(X4)) -> #U21(X1,X2,X3,X4) #4: #U11(X1,mark(X2)) -> #U11(X1,X2) #5: #U12(X1,active(X2)) -> #U12(X1,X2) #6: #take(active(X1),X2) -> #take(X1,X2) #7: #U21(X1,X2,active(X3),X4) -> #U21(X1,X2,X3,X4) #8: #U21(X1,X2,mark(X3),X4) -> #U21(X1,X2,X3,X4) #9: #U21(X1,mark(X2),X3,X4) -> #U21(X1,X2,X3,X4) #10: #s(active(X)) -> #s(X) #11: #U21(X1,X2,X3,active(X4)) -> #U21(X1,X2,X3,X4) #12: #U22(X1,active(X2),X3,X4) -> #U22(X1,X2,X3,X4) #13: #U22(mark(X1),X2,X3,X4) -> #U22(X1,X2,X3,X4) #14: #U23(X1,X2,mark(X3),X4) -> #U23(X1,X2,X3,X4) #15: #U23(X1,active(X2),X3,X4) -> #U23(X1,X2,X3,X4) #16: #length(mark(X)) -> #length(X) #17: #active(U23(tt(),IL,M,N)) -> #mark(cons(N,take(M,IL))) #18: #active(U23(tt(),IL,M,N)) -> #cons(N,take(M,IL)) #19: #active(U23(tt(),IL,M,N)) -> #take(M,IL) #20: #U23(X1,X2,X3,mark(X4)) -> #U23(X1,X2,X3,X4) #21: #U22(X1,X2,X3,active(X4)) -> #U22(X1,X2,X3,X4) #22: #take(X1,active(X2)) -> #take(X1,X2) #23: #U21(mark(X1),X2,X3,X4) -> #U21(X1,X2,X3,X4) #24: #U22(X1,X2,X3,mark(X4)) -> #U22(X1,X2,X3,X4) #25: #mark(0()) -> #active(0()) #26: #mark(zeros()) -> #active(zeros()) #27: #U23(X1,mark(X2),X3,X4) -> #U23(X1,X2,X3,X4) #28: #cons(mark(X1),X2) -> #cons(X1,X2) #29: #mark(nil()) -> #active(nil()) #30: #U21(X1,active(X2),X3,X4) -> #U21(X1,X2,X3,X4) #31: #mark(cons(X1,X2)) -> #active(cons(mark(X1),X2)) #32: #mark(cons(X1,X2)) -> #cons(mark(X1),X2) #33: #mark(cons(X1,X2)) -> #mark(X1) #34: #U11(X1,active(X2)) -> #U11(X1,X2) #35: #U23(mark(X1),X2,X3,X4) -> #U23(X1,X2,X3,X4) #36: #mark(U11(X1,X2)) -> #active(U11(mark(X1),X2)) #37: #mark(U11(X1,X2)) -> #U11(mark(X1),X2) #38: #mark(U11(X1,X2)) -> #mark(X1) #39: #U23(X1,X2,active(X3),X4) -> #U23(X1,X2,X3,X4) #40: #U11(active(X1),X2) -> #U11(X1,X2) #41: #U22(active(X1),X2,X3,X4) -> #U22(X1,X2,X3,X4) #42: #U22(X1,mark(X2),X3,X4) -> #U22(X1,X2,X3,X4) #43: #cons(X1,mark(X2)) -> #cons(X1,X2) #44: #mark(U22(X1,X2,X3,X4)) -> #active(U22(mark(X1),X2,X3,X4)) #45: #mark(U22(X1,X2,X3,X4)) -> #U22(mark(X1),X2,X3,X4) #46: #mark(U22(X1,X2,X3,X4)) -> #mark(X1) #47: #length(active(X)) -> #length(X) #48: #active(take(s(M),cons(N,IL))) -> #mark(U21(tt(),IL,M,N)) #49: #active(take(s(M),cons(N,IL))) -> #U21(tt(),IL,M,N) #50: #take(mark(X1),X2) -> #take(X1,X2) #51: #U12(X1,mark(X2)) -> #U12(X1,X2) #52: #active(U22(tt(),IL,M,N)) -> #mark(U23(tt(),IL,M,N)) #53: #active(U22(tt(),IL,M,N)) -> #U23(tt(),IL,M,N) #54: #U21(active(X1),X2,X3,X4) -> #U21(X1,X2,X3,X4) #55: #take(X1,mark(X2)) -> #take(X1,X2) #56: #U11(mark(X1),X2) -> #U11(X1,X2) #57: #mark(take(X1,X2)) -> #active(take(mark(X1),mark(X2))) #58: #mark(take(X1,X2)) -> #take(mark(X1),mark(X2)) #59: #mark(take(X1,X2)) -> #mark(X1) #60: #mark(take(X1,X2)) -> #mark(X2) #61: #U12(active(X1),X2) -> #U12(X1,X2) #62: #cons(X1,active(X2)) -> #cons(X1,X2) #63: #U23(active(X1),X2,X3,X4) -> #U23(X1,X2,X3,X4) #64: #mark(s(X)) -> #active(s(mark(X))) #65: #mark(s(X)) -> #s(mark(X)) #66: #mark(s(X)) -> #mark(X) #67: #U12(mark(X1),X2) -> #U12(X1,X2) #68: #mark(U21(X1,X2,X3,X4)) -> #active(U21(mark(X1),X2,X3,X4)) #69: #mark(U21(X1,X2,X3,X4)) -> #U21(mark(X1),X2,X3,X4) #70: #mark(U21(X1,X2,X3,X4)) -> #mark(X1) #71: #U23(X1,X2,X3,active(X4)) -> #U23(X1,X2,X3,X4) #72: #cons(active(X1),X2) -> #cons(X1,X2) #73: #s(mark(X)) -> #s(X) #74: #mark(U23(X1,X2,X3,X4)) -> #active(U23(mark(X1),X2,X3,X4)) #75: #mark(U23(X1,X2,X3,X4)) -> #U23(mark(X1),X2,X3,X4) #76: #mark(U23(X1,X2,X3,X4)) -> #mark(X1) #77: #mark(U12(X1,X2)) -> #active(U12(mark(X1),X2)) #78: #mark(U12(X1,X2)) -> #U12(mark(X1),X2) #79: #mark(U12(X1,X2)) -> #mark(X1) #80: #active(U12(tt(),L)) -> #mark(s(length(L))) #81: #active(U12(tt(),L)) -> #s(length(L)) #82: #active(U12(tt(),L)) -> #length(L) #83: #active(zeros()) -> #mark(cons(0(),zeros())) #84: #active(zeros()) -> #cons(0(),zeros()) #85: #U22(X1,X2,active(X3),X4) -> #U22(X1,X2,X3,X4) #86: #active(length(cons(N,L))) -> #mark(U11(tt(),L)) #87: #active(length(cons(N,L))) -> #U11(tt(),L) #88: #mark(tt()) -> #active(tt()) #89: #active(U21(tt(),IL,M,N)) -> #mark(U22(tt(),IL,M,N)) #90: #active(U21(tt(),IL,M,N)) -> #U22(tt(),IL,M,N) #91: #U22(X1,X2,mark(X3),X4) -> #U22(X1,X2,X3,X4) #92: #mark(length(X)) -> #active(length(mark(X))) #93: #mark(length(X)) -> #length(mark(X)) #94: #mark(length(X)) -> #mark(X) Number of SCCs: 10, DPs: 70, edges: 465 SCC { #16 #47 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: x1 Usable rules: { } Removed DPs: #16 #47 Number of SCCs: 9, DPs: 68, edges: 461 SCC { #10 #73 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: x1 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #10 #73 Number of SCCs: 8, DPs: 66, edges: 457 SCC { #5 #51 #61 #67 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: x1 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #61 #67 Number of SCCs: 8, DPs: 64, edges: 445 SCC { #5 #51 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: x2 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #5 #51 Number of SCCs: 7, DPs: 62, edges: 441 SCC { #28 #43 #62 #72 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: x1 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #28 #72 Number of SCCs: 8, DPs: 60, edges: 429 SCC { #43 #62 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: x2 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #43 #62 Number of SCCs: 7, DPs: 58, edges: 425 SCC { #4 #34 #40 #56 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: x1 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #40 #56 Number of SCCs: 8, DPs: 56, edges: 413 SCC { #4 #34 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: x2 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #4 #34 Number of SCCs: 7, DPs: 54, edges: 409 SCC { #6 #22 #50 #55 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: x1 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #6 #50 Number of SCCs: 8, DPs: 52, edges: 397 SCC { #22 #55 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: x2 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #22 #55 Number of SCCs: 7, DPs: 50, edges: 393 SCC { #14 #15 #20 #27 #35 #39 #63 #71 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: x1 + x2 + x3 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #14 #15 #27 #35 #39 #63 Number of SCCs: 8, DPs: 44, edges: 333 SCC { #20 #71 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: x4 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #20 #71 Number of SCCs: 7, DPs: 42, edges: 329 SCC { #3 #7..9 #11 #23 #30 #54 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: x1 + x2 + x4 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #3 #9 #11 #23 #30 #54 Number of SCCs: 8, DPs: 36, edges: 269 SCC { #7 #8 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: x3 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #7 #8 Number of SCCs: 7, DPs: 34, edges: 265 SCC { #12 #13 #21 #24 #41 #42 #85 #91 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: x1 + x3 + x4 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #13 #21 #24 #41 #85 #91 Number of SCCs: 8, DPs: 28, edges: 205 SCC { #12 #42 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: 0 U11(x1,x2) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: 0 zeros() weight: 0 U12(x1,x2) weight: 0 #U12(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 2) + x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: x2 tt() weight: 0 U22(x1,x2,x3,x4) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 Usable rules: { } Removed DPs: #12 #42 Number of SCCs: 7, DPs: 26, edges: 201 SCC { #1 #17 #26 #33 #36 #38 #44 #46 #48 #52 #57 #59 #60 #66 #68 #70 #74 #76 #77 #79 #80 #83 #86 #89 #92 #94 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: (/ 1 2) + x1 + x2 + x3 + x4 U11(x1,x2) weight: (/ 1 2) + x1 + x2 #cons(x1,x2) weight: 0 s(x1) weight: x1 #take(x1,x2) weight: 0 take(x1,x2) weight: (/ 1 2) + x1 + x2 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: (/ 1 2) + x1 + x2 + x3 + x4 zeros() weight: 0 U12(x1,x2) weight: (/ 1 2) + x1 + x2 #U12(x1,x2) weight: 0 #mark(x1) weight: x1 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: x1 #U11(x1,x2) weight: 0 active(x1) weight: x1 cons(x1,x2) weight: x1 + x2 #active(x1) weight: x1 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: (/ 1 2) + x1 + x2 + x3 + x4 length(x1) weight: (/ 1 2) + x1 #length(x1) weight: 0 Usable rules: { 1..6 8 10..67 } Removed DPs: #38 #46 #59 #60 #70 #76 #79 #94 Number of SCCs: 8, DPs: 18, edges: 36 SCC { #1 #17 #26 #33 #36 #44 #48 #52 #57 #66 #68 #74 #77 #80 #83 #86 #89 #92 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1,x2,x3,x4) weight: (/ 3 8) + x1 + x3 + x4 U11(x1,x2) weight: (/ 1 8) + x1 #cons(x1,x2) weight: 0 s(x1) weight: x1 #take(x1,x2) weight: 0 take(x1,x2) weight: (/ 1 2) + x1 + x2 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: (/ 1 8) + x1 + x3 + x4 zeros() weight: 0 U12(x1,x2) weight: (/ 1 8) + x1 #U12(x1,x2) weight: 0 #mark(x1) weight: x1 0() weight: 0 #s(x1) weight: 0 nil() weight: 0 mark(x1) weight: x1 #U11(x1,x2) weight: 0 active(x1) weight: x1 cons(x1,x2) weight: x1 #active(x1) weight: x1 #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: (/ 1 4) + x1 + x3 + x4 length(x1) weight: (/ 1 8) #length(x1) weight: 0 Usable rules: { 1..6 8 10..67 } Removed DPs: #17 #48 #52 #89 Number of SCCs: 8, DPs: 10, edges: 20 SCC { #1 #26 #33 #36 #66 #77 #80 #83 #86 #92 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. U21(x1,x2,x3,x4) weight: max{0, (/ 1 2) + x2} U11(x1,x2) weight: max{0, (/ 3 8) + x1} #cons(x1,x2) weight: 0 s(x1) weight: x1 #take(x1,x2) weight: 0 take(x1,x2) weight: 0 #U23(x1,x2,x3,x4) weight: 0 U23(x1,x2,x3,x4) weight: max{0, (/ 3 8) + x1} zeros() weight: (/ 3 8) U12(x1,x2) weight: max{0, (/ 3 8) + x1} #U12(x1,x2) weight: 0 #mark(x1) weight: x1 0() weight: (/ 1 8) #s(x1) weight: 0 nil() weight: (/ 1 8) mark(x1) weight: (/ 1 2) + x1 #U11(x1,x2) weight: 0 active(x1) weight: (/ 1 8) + x1 cons(x1,x2) weight: max{x2, (/ 1 8) + x1} #active(x1) weight: (/ 3 8) #U21(x1,x2,x3,x4) weight: 0 #U22(x1,x2,x3,x4) weight: 0 tt() weight: 0 U22(x1,x2,x3,x4) weight: max{0, (/ 1 4) + x1} length(x1) weight: (/ 3 8) #length(x1) weight: 0 Usable rules: { 28..35 38 39 64..67 } Removed DPs: #33 Number of SCCs: 8, DPs: 7, edges: 10 SCC { #1 #36 #66 #77 #80 #86 #92 } 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