Input TRS: 1: active(zeros()) -> mark(cons(0(),zeros())) 2: active(U11(tt())) -> mark(tt()) 3: active(U21(tt())) -> mark(tt()) 4: active(U31(tt())) -> mark(tt()) 5: active(U41(tt(),V2)) -> mark(U42(isNatIList(V2))) 6: active(U42(tt())) -> mark(tt()) 7: active(U51(tt(),V2)) -> mark(U52(isNatList(V2))) 8: active(U52(tt())) -> mark(tt()) 9: active(U61(tt(),L,N)) -> mark(U62(isNat(N),L)) 10: active(U62(tt(),L)) -> mark(s(length(L))) 11: active(isNat(0())) -> mark(tt()) 12: active(isNat(length(V1))) -> mark(U11(isNatList(V1))) 13: active(isNat(s(V1))) -> mark(U21(isNat(V1))) 14: active(isNatIList(V)) -> mark(U31(isNatList(V))) 15: active(isNatIList(zeros())) -> mark(tt()) 16: active(isNatIList(cons(V1,V2))) -> mark(U41(isNat(V1),V2)) 17: active(isNatList(nil())) -> mark(tt()) 18: active(isNatList(cons(V1,V2))) -> mark(U51(isNat(V1),V2)) 19: active(length(nil())) -> mark(0()) 20: active(length(cons(N,L))) -> mark(U61(isNatList(L),L,N)) 21: mark(zeros()) -> active(zeros()) 22: mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 23: mark(0()) -> active(0()) 24: mark(U11(X)) -> active(U11(mark(X))) 25: mark(tt()) -> active(tt()) 26: mark(U21(X)) -> active(U21(mark(X))) 27: mark(U31(X)) -> active(U31(mark(X))) 28: mark(U41(X1,X2)) -> active(U41(mark(X1),X2)) 29: mark(U42(X)) -> active(U42(mark(X))) 30: mark(isNatIList(X)) -> active(isNatIList(X)) 31: mark(U51(X1,X2)) -> active(U51(mark(X1),X2)) 32: mark(U52(X)) -> active(U52(mark(X))) 33: mark(isNatList(X)) -> active(isNatList(X)) 34: mark(U61(X1,X2,X3)) -> active(U61(mark(X1),X2,X3)) 35: mark(U62(X1,X2)) -> active(U62(mark(X1),X2)) 36: mark(isNat(X)) -> active(isNat(X)) 37: mark(s(X)) -> active(s(mark(X))) 38: mark(length(X)) -> active(length(mark(X))) 39: mark(nil()) -> active(nil()) 40: cons(mark(X1),X2) -> cons(X1,X2) 41: cons(X1,mark(X2)) -> cons(X1,X2) 42: cons(active(X1),X2) -> cons(X1,X2) 43: cons(X1,active(X2)) -> cons(X1,X2) 44: U11(mark(X)) -> U11(X) 45: U11(active(X)) -> U11(X) 46: U21(mark(X)) -> U21(X) 47: U21(active(X)) -> U21(X) 48: U31(mark(X)) -> U31(X) 49: U31(active(X)) -> U31(X) 50: U41(mark(X1),X2) -> U41(X1,X2) 51: U41(X1,mark(X2)) -> U41(X1,X2) 52: U41(active(X1),X2) -> U41(X1,X2) 53: U41(X1,active(X2)) -> U41(X1,X2) 54: U42(mark(X)) -> U42(X) 55: U42(active(X)) -> U42(X) 56: isNatIList(mark(X)) -> isNatIList(X) 57: isNatIList(active(X)) -> isNatIList(X) 58: U51(mark(X1),X2) -> U51(X1,X2) 59: U51(X1,mark(X2)) -> U51(X1,X2) 60: U51(active(X1),X2) -> U51(X1,X2) 61: U51(X1,active(X2)) -> U51(X1,X2) 62: U52(mark(X)) -> U52(X) 63: U52(active(X)) -> U52(X) 64: isNatList(mark(X)) -> isNatList(X) 65: isNatList(active(X)) -> isNatList(X) 66: U61(mark(X1),X2,X3) -> U61(X1,X2,X3) 67: U61(X1,mark(X2),X3) -> U61(X1,X2,X3) 68: U61(X1,X2,mark(X3)) -> U61(X1,X2,X3) 69: U61(active(X1),X2,X3) -> U61(X1,X2,X3) 70: U61(X1,active(X2),X3) -> U61(X1,X2,X3) 71: U61(X1,X2,active(X3)) -> U61(X1,X2,X3) 72: U62(mark(X1),X2) -> U62(X1,X2) 73: U62(X1,mark(X2)) -> U62(X1,X2) 74: U62(active(X1),X2) -> U62(X1,X2) 75: U62(X1,active(X2)) -> U62(X1,X2) 76: isNat(mark(X)) -> isNat(X) 77: isNat(active(X)) -> isNat(X) 78: s(mark(X)) -> s(X) 79: s(active(X)) -> s(X) 80: length(mark(X)) -> length(X) 81: length(active(X)) -> length(X) Number of strict rules: 81 Direct Order(PosReal,>,Poly) ... removes: 4 15 19 14 12 2 U21(x1) weight: x1 isNatList(x1) weight: x1 U11(x1) weight: (/ 1 4) + x1 s(x1) weight: x1 U42(x1) weight: x1 isNatIList(x1) weight: (/ 6895 2) + x1 zeros() weight: 0 0() weight: 0 nil() weight: 0 U62(x1,x2) weight: (/ 42511 2) + x1 + 2 * x2 mark(x1) weight: x1 isNat(x1) weight: x1 U52(x1) weight: x1 U61(x1,x2,x3) weight: (/ 42511 2) + x1 + 2 * x2 + x3 active(x1) weight: x1 U31(x1) weight: (/ 1 4) + x1 cons(x1,x2) weight: x1 + 2 * x2 tt() weight: 0 U51(x1,x2) weight: x1 + x2 length(x1) weight: (/ 42511 2) + 2 * x1 U41(x1,x2) weight: (/ 6895 2) + x1 + x2 Number of strict rules: 75 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #cons(X1,active(X2)) -> #cons(X1,X2) #2: #mark(U42(X)) -> #active(U42(mark(X))) #3: #mark(U42(X)) -> #U42(mark(X)) #4: #mark(U42(X)) -> #mark(X) #5: #mark(U62(X1,X2)) -> #active(U62(mark(X1),X2)) #6: #mark(U62(X1,X2)) -> #U62(mark(X1),X2) #7: #mark(U62(X1,X2)) -> #mark(X1) #8: #U61(mark(X1),X2,X3) -> #U61(X1,X2,X3) #9: #U21(mark(X)) -> #U21(X) #10: #cons(active(X1),X2) -> #cons(X1,X2) #11: #cons(X1,mark(X2)) -> #cons(X1,X2) #12: #mark(s(X)) -> #active(s(mark(X))) #13: #mark(s(X)) -> #s(mark(X)) #14: #mark(s(X)) -> #mark(X) #15: #U62(X1,mark(X2)) -> #U62(X1,X2) #16: #U21(active(X)) -> #U21(X) #17: #U41(X1,active(X2)) -> #U41(X1,X2) #18: #U61(X1,X2,active(X3)) -> #U61(X1,X2,X3) #19: #U31(mark(X)) -> #U31(X) #20: #U62(X1,active(X2)) -> #U62(X1,X2) #21: #U62(active(X1),X2) -> #U62(X1,X2) #22: #U51(mark(X1),X2) -> #U51(X1,X2) #23: #U51(X1,active(X2)) -> #U51(X1,X2) #24: #mark(length(X)) -> #active(length(mark(X))) #25: #mark(length(X)) -> #length(mark(X)) #26: #mark(length(X)) -> #mark(X) #27: #active(U42(tt())) -> #mark(tt()) #28: #U51(X1,mark(X2)) -> #U51(X1,X2) #29: #U42(active(X)) -> #U42(X) #30: #U61(X1,mark(X2),X3) -> #U61(X1,X2,X3) #31: #cons(mark(X1),X2) -> #cons(X1,X2) #32: #U41(X1,mark(X2)) -> #U41(X1,X2) #33: #active(isNat(s(V1))) -> #mark(U21(isNat(V1))) #34: #active(isNat(s(V1))) -> #U21(isNat(V1)) #35: #active(isNat(s(V1))) -> #isNat(V1) #36: #active(U61(tt(),L,N)) -> #mark(U62(isNat(N),L)) #37: #active(U61(tt(),L,N)) -> #U62(isNat(N),L) #38: #active(U61(tt(),L,N)) -> #isNat(N) #39: #active(isNat(0())) -> #mark(tt()) #40: #isNatIList(active(X)) -> #isNatIList(X) #41: #isNat(mark(X)) -> #isNat(X) #42: #mark(U11(X)) -> #active(U11(mark(X))) #43: #mark(U11(X)) -> #U11(mark(X)) #44: #mark(U11(X)) -> #mark(X) #45: #U61(X1,active(X2),X3) -> #U61(X1,X2,X3) #46: #mark(0()) -> #active(0()) #47: #length(active(X)) -> #length(X) #48: #s(mark(X)) -> #s(X) #49: #U11(active(X)) -> #U11(X) #50: #U61(active(X1),X2,X3) -> #U61(X1,X2,X3) #51: #mark(U51(X1,X2)) -> #active(U51(mark(X1),X2)) #52: #mark(U51(X1,X2)) -> #U51(mark(X1),X2) #53: #mark(U51(X1,X2)) -> #mark(X1) #54: #s(active(X)) -> #s(X) #55: #isNatIList(mark(X)) -> #isNatIList(X) #56: #U52(mark(X)) -> #U52(X) #57: #mark(isNatIList(X)) -> #active(isNatIList(X)) #58: #U41(active(X1),X2) -> #U41(X1,X2) #59: #U31(active(X)) -> #U31(X) #60: #mark(tt()) -> #active(tt()) #61: #active(length(cons(N,L))) -> #mark(U61(isNatList(L),L,N)) #62: #active(length(cons(N,L))) -> #U61(isNatList(L),L,N) #63: #active(length(cons(N,L))) -> #isNatList(L) #64: #active(U51(tt(),V2)) -> #mark(U52(isNatList(V2))) #65: #active(U51(tt(),V2)) -> #U52(isNatList(V2)) #66: #active(U51(tt(),V2)) -> #isNatList(V2) #67: #mark(nil()) -> #active(nil()) #68: #active(U62(tt(),L)) -> #mark(s(length(L))) #69: #active(U62(tt(),L)) -> #s(length(L)) #70: #active(U62(tt(),L)) -> #length(L) #71: #isNatList(mark(X)) -> #isNatList(X) #72: #mark(isNatList(X)) -> #active(isNatList(X)) #73: #U62(mark(X1),X2) -> #U62(X1,X2) #74: #active(U41(tt(),V2)) -> #mark(U42(isNatIList(V2))) #75: #active(U41(tt(),V2)) -> #U42(isNatIList(V2)) #76: #active(U41(tt(),V2)) -> #isNatIList(V2) #77: #U11(mark(X)) -> #U11(X) #78: #isNatList(active(X)) -> #isNatList(X) #79: #mark(U41(X1,X2)) -> #active(U41(mark(X1),X2)) #80: #mark(U41(X1,X2)) -> #U41(mark(X1),X2) #81: #mark(U41(X1,X2)) -> #mark(X1) #82: #mark(cons(X1,X2)) -> #active(cons(mark(X1),X2)) #83: #mark(cons(X1,X2)) -> #cons(mark(X1),X2) #84: #mark(cons(X1,X2)) -> #mark(X1) #85: #mark(U61(X1,X2,X3)) -> #active(U61(mark(X1),X2,X3)) #86: #mark(U61(X1,X2,X3)) -> #U61(mark(X1),X2,X3) #87: #mark(U61(X1,X2,X3)) -> #mark(X1) #88: #mark(U31(X)) -> #active(U31(mark(X))) #89: #mark(U31(X)) -> #U31(mark(X)) #90: #mark(U31(X)) -> #mark(X) #91: #U51(active(X1),X2) -> #U51(X1,X2) #92: #active(isNatList(nil())) -> #mark(tt()) #93: #mark(U52(X)) -> #active(U52(mark(X))) #94: #mark(U52(X)) -> #U52(mark(X)) #95: #mark(U52(X)) -> #mark(X) #96: #U52(active(X)) -> #U52(X) #97: #mark(U21(X)) -> #active(U21(mark(X))) #98: #mark(U21(X)) -> #U21(mark(X)) #99: #mark(U21(X)) -> #mark(X) #100: #U61(X1,X2,mark(X3)) -> #U61(X1,X2,X3) #101: #mark(isNat(X)) -> #active(isNat(X)) #102: #mark(zeros()) -> #active(zeros()) #103: #active(isNatIList(cons(V1,V2))) -> #mark(U41(isNat(V1),V2)) #104: #active(isNatIList(cons(V1,V2))) -> #U41(isNat(V1),V2) #105: #active(isNatIList(cons(V1,V2))) -> #isNat(V1) #106: #active(U21(tt())) -> #mark(tt()) #107: #isNat(active(X)) -> #isNat(X) #108: #active(zeros()) -> #mark(cons(0(),zeros())) #109: #active(zeros()) -> #cons(0(),zeros()) #110: #U42(mark(X)) -> #U42(X) #111: #active(U52(tt())) -> #mark(tt()) #112: #length(mark(X)) -> #length(X) #113: #U41(mark(X1),X2) -> #U41(X1,X2) #114: #active(isNatList(cons(V1,V2))) -> #mark(U51(isNat(V1),V2)) #115: #active(isNatList(cons(V1,V2))) -> #U51(isNat(V1),V2) #116: #active(isNatList(cons(V1,V2))) -> #isNat(V1) Number of SCCs: 16, DPs: 72, edges: 414 SCC { #49 #77 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: x1 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #49 #77 Number of SCCs: 15, DPs: 70, edges: 410 SCC { #29 #110 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: x1 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #29 #110 Number of SCCs: 14, DPs: 68, edges: 406 SCC { #41 #107 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: x1 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #41 #107 Number of SCCs: 13, DPs: 66, edges: 402 SCC { #9 #16 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: x1 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #9 #16 Number of SCCs: 12, DPs: 64, edges: 398 SCC { #56 #96 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: x1 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #56 #96 Number of SCCs: 11, DPs: 62, edges: 394 SCC { #19 #59 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: x1 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #19 #59 Number of SCCs: 10, DPs: 60, edges: 390 SCC { #47 #112 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: x1 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #47 #112 Number of SCCs: 9, DPs: 58, edges: 386 SCC { #40 #55 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: x1 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #40 #55 Number of SCCs: 8, DPs: 56, edges: 382 SCC { #71 #78 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: x1 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #71 #78 Number of SCCs: 7, DPs: 54, edges: 378 SCC { #48 #54 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: x1 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #48 #54 Number of SCCs: 6, DPs: 52, edges: 374 SCC { #15 #20 #21 #73 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: x1 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #21 #73 Number of SCCs: 6, DPs: 50, edges: 362 SCC { #15 #20 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: x2 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #15 #20 Number of SCCs: 5, DPs: 48, edges: 358 SCC { #1 #10 #11 #31 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: x2 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #1 #11 Number of SCCs: 6, DPs: 46, edges: 346 SCC { #10 #31 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: x1 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #10 #31 Number of SCCs: 5, DPs: 44, edges: 342 SCC { #17 #32 #58 #113 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: x2 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #17 #32 Number of SCCs: 6, DPs: 42, edges: 330 SCC { #58 #113 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: x1 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #58 #113 Number of SCCs: 5, DPs: 40, edges: 326 SCC { #22 #23 #28 #91 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: x2 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #23 #28 Number of SCCs: 6, DPs: 38, edges: 314 SCC { #22 #91 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: x1 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #22 #91 Number of SCCs: 5, DPs: 36, edges: 310 SCC { #8 #18 #30 #45 #50 #100 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: x1 + x2 Usable rules: { } Removed DPs: #8 #30 #45 #50 Number of SCCs: 6, DPs: 32, edges: 278 SCC { #18 #100 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: 0 isNatList(x1) weight: 0 U11(x1) weight: 0 #cons(x1,x2) weight: 0 s(x1) weight: 0 #isNat(x1) weight: 0 U42(x1) weight: 0 isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: 0 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: 0 mark(x1) weight: (/ 1 2) + x1 isNat(x1) weight: 0 U52(x1) weight: 0 U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) + x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: 0 #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: 0 length(x1) weight: 0 #length(x1) weight: 0 U41(x1,x2) weight: 0 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: x3 Usable rules: { } Removed DPs: #18 #100 Number of SCCs: 5, DPs: 30, edges: 274 SCC { #4 #5 #7 #14 #24 #26 #33 #36 #44 #51 #53 #57 #61 #64 #68 #72 #74 #79 #81 #84 #85 #87 #90 #95 #99 #101..103 #108 #114 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: x1 isNatList(x1) weight: 0 U11(x1) weight: (/ 1 2) + x1 #cons(x1,x2) weight: 0 s(x1) weight: x1 #isNat(x1) weight: 0 U42(x1) weight: x1 isNatIList(x1) weight: (/ 1 2) zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: x1 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: (/ 1 2) + x1 + x2 mark(x1) weight: x1 isNat(x1) weight: 0 U52(x1) weight: x1 U61(x1,x2,x3) weight: (/ 1 2) + x1 + x2 + x3 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: x1 U31(x1) weight: (/ 1 2) + x1 #U41(x1,x2) weight: 0 cons(x1,x2) weight: x1 + x2 #active(x1) weight: x1 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: x1 length(x1) weight: (/ 1 2) + x1 #length(x1) weight: 0 U41(x1,x2) weight: (/ 1 2) + x1 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { 1 3 5..11 13 16..18 20..81 } Removed DPs: #7 #26 #44 #81 #87 #90 Number of SCCs: 6, DPs: 24, edges: 109 SCC { #4 #5 #14 #24 #33 #36 #51 #53 #57 #61 #64 #68 #72 #74 #79 #84 #85 #95 #99 #101..103 #108 #114 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: x1 isNatList(x1) weight: (/ 1 2) U11(x1) weight: x1 #cons(x1,x2) weight: 0 s(x1) weight: x1 #isNat(x1) weight: 0 U42(x1) weight: x1 isNatIList(x1) weight: (/ 1 2) zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: x1 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: (/ 77739 2) mark(x1) weight: x1 isNat(x1) weight: 0 U52(x1) weight: x1 U61(x1,x2,x3) weight: (/ 77739 2) #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: x1 U31(x1) weight: 0 #U41(x1,x2) weight: 0 cons(x1,x2) weight: x1 + x2 #active(x1) weight: x1 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: (/ 1 2) + x1 length(x1) weight: (/ 77739 2) #length(x1) weight: 0 U41(x1,x2) weight: (/ 1 2) #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { 1 3 5..11 13 16..18 20..81 } Removed DPs: #53 Number of SCCs: 6, DPs: 23, edges: 88 SCC { #4 #5 #14 #24 #33 #36 #51 #57 #61 #64 #68 #72 #74 #79 #84 #85 #95 #99 #101..103 #108 #114 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded. U21(x1) weight: x1 isNatList(x1) weight: (/ 1 4) + x1 U11(x1) weight: (/ 1 8) #cons(x1,x2) weight: 0 s(x1) weight: x1 #isNat(x1) weight: 0 U42(x1) weight: x1 isNatIList(x1) weight: (/ 1 8) + x1 zeros() weight: (/ 83607 8) #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: x1 0() weight: (/ 1 8) #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: (/ 1 8) U62(x1,x2) weight: max{0, (/ 3 8) + x2} mark(x1) weight: x1 isNat(x1) weight: (/ 83603 8) U52(x1) weight: x1 U61(x1,x2,x3) weight: max{(/ 1 4) + x3, (/ 3 8) + x2, (/ 1 8) + x1} #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: x1 U31(x1) weight: (/ 1 8) #U41(x1,x2) weight: 0 cons(x1,x2) weight: max{x2, (/ 83605 8) + x1} #active(x1) weight: x1 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: (/ 3 8) U51(x1,x2) weight: max{(/ 1 4) + x2, (/ 1 2) + x1} length(x1) weight: (/ 3 8) + x1 #length(x1) weight: 0 U41(x1,x2) weight: max{(/ 1 8) + x2, (/ 1 4) + x1} #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { 1 3 5..11 13 16..18 20..81 } Removed DPs: #84 Number of SCCs: 6, DPs: 20, edges: 64 SCC { #4 #5 #14 #24 #33 #36 #51 #57 #61 #64 #68 #72 #74 #79 #85 #95 #99 #101 #103 #114 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: x1 isNatList(x1) weight: (/ 1 8) + x1 U11(x1) weight: (/ 1 8) + x1 #cons(x1,x2) weight: 0 s(x1) weight: x1 #isNat(x1) weight: 0 U42(x1) weight: (/ 1 8) + x1 isNatIList(x1) weight: (/ 1 8) + x1 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: (/ 1 8) + x1 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: (/ 452161 8) mark(x1) weight: (/ 3 8) + x1 isNat(x1) weight: (/ 1 8) U52(x1) weight: (/ 1 8) + x1 U61(x1,x2,x3) weight: (/ 452161 8) #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 8) + x1 U31(x1) weight: (/ 1 8) #U41(x1,x2) weight: 0 cons(x1,x2) weight: (/ 3 8) + x1 + x2 #active(x1) weight: (/ 1 8) + x1 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: (/ 3 8) + x2 length(x1) weight: (/ 452161 8) #length(x1) weight: 0 U41(x1,x2) weight: (/ 3 8) + x2 #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { 48..53 56..61 64..77 80 81 } Removed DPs: #4 #64 #74 #95 #103 #114 Number of SCCs: 6, DPs: 10, edges: 20 SCC { #5 #14 #24 #33 #36 #61 #68 #85 #99 #101 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded. U21(x1) weight: max{0, (/ 1 32) + x1} isNatList(x1) weight: max{0, (/ 15 32) + x1} U11(x1) weight: (max (/ 15 32) 0) #cons(x1,x2) weight: 0 s(x1) weight: max{0, (/ 1 8) + x1} #isNat(x1) weight: 0 U42(x1) weight: (max (- (/ 1 32)) 0) isNatIList(x1) weight: max{0, (/ 1 32) + x1} zeros() weight: (/ 1 32) #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: max{0, (- (/ 3 16)) + x1} 0() weight: (/ 1 32) #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: (/ 1 32) U62(x1,x2) weight: 0 mark(x1) weight: max{0, (/ 15 16) + x1} isNat(x1) weight: max{0, (/ 9 32) + x1} U52(x1) weight: (max (- (/ 1 32)) 0) U61(x1,x2,x3) weight: 0 #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: max{0, (/ 1 2) + x1} U31(x1) weight: (max (/ 1 32) 0) #U41(x1,x2) weight: 0 cons(x1,x2) weight: (max (- (/ 3 8)) 0) #active(x1) weight: max{0, (- (/ 1 4)) + x1} #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: (/ 3 32) U51(x1,x2) weight: max{0, (- (/ 1 32)) + x2} length(x1) weight: (max (/ 1 32) 0) #length(x1) weight: 0 U41(x1,x2) weight: (max (- (/ 15 32)) 0) #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { 40..43 48..53 56..63 66..77 80 81 } Removed DPs: #33 #101 Number of SCCs: 6, DPs: 8, edges: 16 SCC { #5 #14 #24 #36 #61 #68 #85 #99 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: (/ 1 4) + x1 isNatList(x1) weight: (/ 1 4) U11(x1) weight: (/ 1 4) + x1 #cons(x1,x2) weight: 0 s(x1) weight: x1 #isNat(x1) weight: 0 U42(x1) weight: (/ 1 4) isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: (/ 1 8) + x1 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: (/ 1 4) mark(x1) weight: (/ 1 4) isNat(x1) weight: (/ 1 4) U52(x1) weight: (/ 1 4) + x1 U61(x1,x2,x3) weight: (/ 1 4) #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 4) U31(x1) weight: (/ 1 4) + x1 #U41(x1,x2) weight: 0 cons(x1,x2) weight: (/ 1 4) #active(x1) weight: (/ 1 8) + x1 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: (/ 1 4) length(x1) weight: (/ 1 4) #length(x1) weight: 0 U41(x1,x2) weight: (/ 1 4) #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { 1 3 5..11 13 16..18 20..39 50..53 56..61 64..77 80 81 } Removed DPs: #99 Number of SCCs: 6, DPs: 7, edges: 10 SCC { #5 #14 #24 #36 #61 #68 #85 } Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... succeeded. U21(x1) weight: x1_1 + x1_2; 0 isNatList(x1) weight: x1_1 + x1_2; 0 U11(x1) weight: 0; 0 #cons(x1,x2) weight: 0; 0 s(x1) weight: 0; x1_1 + x1_2 #isNat(x1) weight: 0; 0 U42(x1) weight: x1_1 + x1_2; x1_1 + x1_2 isNatIList(x1) weight: 0; 0 zeros() weight: 0; 0 #U52(x1) weight: 0; 0 #U42(x1) weight: 0; 0 #U62(x1,x2) weight: 0; 0 #mark(x1) weight: (/ 1 8) + x1_2; 0 0() weight: (/ 3 4); 0 #isNatList(x1) weight: 0; 0 #s(x1) weight: 0; 0 nil() weight: 0; (/ 3 4) U62(x1,x2) weight: 0; (/ 1 2) + x2_1 + x2_2 mark(x1) weight: x1_2; x1_1 isNat(x1) weight: x1_1 + x1_2; 0 U52(x1) weight: x1_1 + x1_2; 0 U61(x1,x2,x3) weight: 0; x2_1 + x2_2 + x1_1 + x1_2 #U51(x1,x2) weight: 0; 0 #U11(x1) weight: 0; 0 active(x1) weight: x1_2; x1_1 U31(x1) weight: 0; 0 #U41(x1,x2) weight: 0; 0 cons(x1,x2) weight: x2_1 + x2_2; x2_1 + x2_2 #active(x1) weight: x1_2; 0 #isNatIList(x1) weight: 0; 0 #U21(x1) weight: 0; 0 tt() weight: (/ 3 4); 0 U51(x1,x2) weight: x2_1 + x2_2; 0 length(x1) weight: 0; (/ 1 4) + x1_1 + x1_2 #length(x1) weight: 0; 0 U41(x1,x2) weight: 0; 0 #U31(x1) weight: 0; 0 #U61(x1,x2,x3) weight: 0; 0 Usable rules: { 1 3 5..11 13 16..18 20..81 } Removed DPs: #5 #24 #36 #61 #68 #85 Number of SCCs: 6, DPs: 1, edges: 1 SCC { #14 } Removing DPs: Order(PosReal,>,Sum)... succeeded. U21(x1) weight: (/ 1 4) + x1 isNatList(x1) weight: (/ 1 4) U11(x1) weight: (/ 1 4) + x1 #cons(x1,x2) weight: 0 s(x1) weight: (/ 1 4) + x1 #isNat(x1) weight: 0 U42(x1) weight: (/ 1 4) isNatIList(x1) weight: 0 zeros() weight: 0 #U52(x1) weight: 0 #U42(x1) weight: 0 #U62(x1,x2) weight: 0 #mark(x1) weight: x1 0() weight: 0 #isNatList(x1) weight: 0 #s(x1) weight: 0 nil() weight: 0 U62(x1,x2) weight: (/ 1 4) mark(x1) weight: (/ 1 4) isNat(x1) weight: (/ 1 4) U52(x1) weight: (/ 1 4) U61(x1,x2,x3) weight: (/ 1 4) #U51(x1,x2) weight: 0 #U11(x1) weight: 0 active(x1) weight: (/ 1 2) U31(x1) weight: (/ 1 4) + x1 #U41(x1,x2) weight: 0 cons(x1,x2) weight: (/ 1 4) #active(x1) weight: 0 #isNatIList(x1) weight: 0 #U21(x1) weight: 0 tt() weight: 0 U51(x1,x2) weight: (/ 1 4) length(x1) weight: (/ 1 4) #length(x1) weight: 0 U41(x1,x2) weight: (/ 1 4) #U31(x1) weight: 0 #U61(x1,x2,x3) weight: 0 Usable rules: { } Removed DPs: #14 Number of SCCs: 5, DPs: 0, edges: 0 YES