Input TRS: 1: a__zeros() -> cons(0(),zeros()) 2: a__and(tt(),X) -> mark(X) 3: a__length(nil()) -> 0() 4: a__length(cons(N,L)) -> s(a__length(mark(L))) 5: mark(zeros()) -> a__zeros() 6: mark(and(X1,X2)) -> a__and(mark(X1),X2) 7: mark(length(X)) -> a__length(mark(X)) 8: mark(cons(X1,X2)) -> cons(mark(X1),X2) 9: mark(0()) -> 0() 10: mark(tt()) -> tt() 11: mark(nil()) -> nil() 12: mark(s(X)) -> s(mark(X)) 13: a__zeros() -> zeros() 14: a__and(X1,X2) -> and(X1,X2) 15: a__length(X) -> length(X) Number of Rules: 15 Direct POLO(Sum) ... removes: 13 11 10 9 3 2 I(a__length) = x1 I(tt) = 2 I(mark) = x1 + 1 I(0) = 0 I(nil) = 1 I(and) = x1 + x2 I(a__and) = x1 + x2 I(s) = x1 I(length) = x1 I(a__zeros) = 1 I(zeros) = 0 I(cons) = x1 + x2 + 1 Number of Rules: 9 Direct POLO(Sum) ...Direct QLPOS ...Direct QKBOS ... failed.