Input TRS: 1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) 2: a____(X,nil()) -> mark(X) 3: a____(nil(),X) -> mark(X) 4: a__and(tt(),X) -> mark(X) 5: a__isList(V) -> a__isNeList(V) 6: a__isList(nil()) -> tt() 7: a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) 8: a__isNeList(V) -> a__isQid(V) 9: a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) 10: a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) 11: a__isNePal(V) -> a__isQid(V) 12: a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) 13: a__isPal(V) -> a__isNePal(V) 14: a__isPal(nil()) -> tt() 15: a__isQid(a()) -> tt() 16: a__isQid(e()) -> tt() 17: a__isQid(i()) -> tt() 18: a__isQid(o()) -> tt() 19: a__isQid(u()) -> tt() 20: mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) 21: mark(and(X1,X2)) -> a__and(mark(X1),X2) 22: mark(isList(X)) -> a__isList(X) 23: mark(isNeList(X)) -> a__isNeList(X) 24: mark(isQid(X)) -> a__isQid(X) 25: mark(isNePal(X)) -> a__isNePal(X) 26: mark(isPal(X)) -> a__isPal(X) 27: mark(nil()) -> nil() 28: mark(tt()) -> tt() 29: mark(a()) -> a() 30: mark(e()) -> e() 31: mark(i()) -> i() 32: mark(o()) -> o() 33: mark(u()) -> u() 34: a____(X1,X2) -> __(X1,X2) 35: a__and(X1,X2) -> and(X1,X2) 36: a__isList(X) -> isList(X) 37: a__isNeList(X) -> isNeList(X) 38: a__isQid(X) -> isQid(X) 39: a__isNePal(X) -> isNePal(X) 40: a__isPal(X) -> isPal(X) Number of strict rules: 40 Direct Order(PosReal,>,Poly) ... removes: 18 4 15 8 3 16 19 17 5 10 7 14 12 11 9 13 6 2 a() weight: 0 isNeList(x1) weight: (/ 1 4) + 2 * x1 isPal(x1) weight: (/ 17923 8) + x1 u() weight: 0 and(x1,x2) weight: (/ 1 8) + x1 + x2 isNePal(x1) weight: (/ 8961 4) + x1 isQid(x1) weight: (/ 1 8) + x1 a____(x1,x2) weight: (/ 5 16) + x1 + x2 a__isList(x1) weight: (/ 3 8) + 2 * x1 a__isNeList(x1) weight: (/ 1 4) + 2 * x1 o() weight: 0 isList(x1) weight: (/ 3 8) + 2 * x1 nil() weight: 0 mark(x1) weight: x1 a__isNePal(x1) weight: (/ 8961 4) + x1 i() weight: 0 e() weight: 0 a__isPal(x1) weight: (/ 17923 8) + x1 tt() weight: 0 a__isQid(x1) weight: (/ 1 8) + x1 a__and(x1,x2) weight: (/ 1 8) + x1 + x2 __(x1,x2) weight: (/ 5 16) + x1 + x2 Number of strict rules: 22 Direct Order(PosReal,>,Poly) ... removes: 1 a() weight: 0 isNeList(x1) weight: (/ 1 4) + 2 * x1 isPal(x1) weight: (/ 17923 8) + x1 u() weight: 0 and(x1,x2) weight: (/ 1 8) + x1 + x2 isNePal(x1) weight: (/ 8961 4) + x1 isQid(x1) weight: (/ 1 8) + x1 a____(x1,x2) weight: (/ 13445 16) + 2 * x1 + x2 a__isList(x1) weight: (/ 3 8) + 2 * x1 a__isNeList(x1) weight: (/ 1 4) + 2 * x1 o() weight: 0 isList(x1) weight: (/ 3 8) + 2 * x1 nil() weight: 0 mark(x1) weight: x1 a__isNePal(x1) weight: (/ 8961 4) + x1 i() weight: 0 e() weight: 0 a__isPal(x1) weight: (/ 17923 8) + x1 tt() weight: 0 a__isQid(x1) weight: (/ 1 8) + x1 a__and(x1,x2) weight: (/ 1 8) + x1 + x2 __(x1,x2) weight: (/ 13445 16) + 2 * x1 + x2 Number of strict rules: 21 Direct Order(PosReal,>,Poly) ... removes: 36 26 34 22 39 20 25 23 24 40 38 37 a() weight: 0 isNeList(x1) weight: (/ 3 16) + 2 * x1 isPal(x1) weight: (/ 35843 16) + x1 u() weight: 0 and(x1,x2) weight: x1 + x2 isNePal(x1) weight: (/ 35843 16) + x1 isQid(x1) weight: (/ 1 8) + x1 a____(x1,x2) weight: (/ 3 16) + 2 * x1 + x2 a__isList(x1) weight: (/ 5 16) + 2 * x1 a__isNeList(x1) weight: (/ 1 4) + 2 * x1 o() weight: 0 isList(x1) weight: (/ 1 4) + 2 * x1 nil() weight: 0 mark(x1) weight: 2 * x1 a__isNePal(x1) weight: (/ 8961 4) + x1 i() weight: 0 e() weight: 0 a__isPal(x1) weight: (/ 8961 4) + x1 tt() weight: 0 a__isQid(x1) weight: (/ 3 16) + x1 a__and(x1,x2) weight: x1 + x2 __(x1,x2) weight: (/ 1 8) + 2 * x1 + x2 Number of strict rules: 9 Direct Order(PosReal,>,Poly) ... removes: 21 35 a() weight: 0 isNeList(x1) weight: (/ 1 16) + 2 * x1 isPal(x1) weight: (/ 35843 16) + x1 u() weight: 0 and(x1,x2) weight: (/ 1 8) + x1 + x2 isNePal(x1) weight: (/ 8961 4) + x1 isQid(x1) weight: (/ 1 8) + x1 a____(x1,x2) weight: (/ 3 16) + 2 * x1 + x2 a__isList(x1) weight: (/ 1 8) + 2 * x1 a__isNeList(x1) weight: (/ 1 8) + 2 * x1 o() weight: 0 isList(x1) weight: (/ 1 16) + 2 * x1 nil() weight: 0 mark(x1) weight: 2 * x1 a__isNePal(x1) weight: (/ 35845 16) + x1 i() weight: 0 e() weight: 0 a__isPal(x1) weight: (/ 35845 16) + x1 tt() weight: 0 a__isQid(x1) weight: (/ 3 16) + x1 a__and(x1,x2) weight: (/ 3 16) + x1 + x2 __(x1,x2) weight: (/ 1 8) + 2 * x1 + x2 Number of strict rules: 7 Direct Order(PosReal,>,Poly) ... removes: 32 27 28 33 30 31 29 a() weight: 0 isNeList(x1) weight: (/ 1 32) + 2 * x1 isPal(x1) weight: (/ 71683 32) + x1 u() weight: 0 and(x1,x2) weight: (/ 1 16) + x1 + x2 isNePal(x1) weight: (/ 71679 32) + x1 isQid(x1) weight: (/ 1 32) + x1 a____(x1,x2) weight: (/ 1 32) + x1 + x2 a__isList(x1) weight: (/ 3 32) + 2 * x1 a__isNeList(x1) weight: (/ 1 32) + 2 * x1 o() weight: 0 isList(x1) weight: (/ 1 32) + 2 * x1 nil() weight: 0 mark(x1) weight: (/ 1 32) + 2 * x1 a__isNePal(x1) weight: 2240 + x1 i() weight: 0 e() weight: 0 a__isPal(x1) weight: (/ 71683 32) + x1 tt() weight: 0 a__isQid(x1) weight: (/ 1 16) + x1 a__and(x1,x2) weight: (/ 3 32) + x1 + x2 __(x1,x2) weight: (/ 1 8) + 2 * x1 + x2 Number of strict rules: 0 YES