(VAR f x y xs g ys) (RULES ap(ap(map,f),xs) -> ap(ap(ap(if,ap(isEmpty,xs)),f),xs) ap(ap(ap(if,true),f),xs) -> null ap(ap(ap(if,null),f),xs) -> ap(ap(cons,ap(f,ap(last,xs))),ap(ap(if2,f),xs)) ap(ap(if2,f),xs) -> ap(ap(map,f),ap(dropLast,xs)) ap(isEmpty,null) -> true ap(isEmpty,ap(ap(cons,x),xs)) -> null ap(last,ap(ap(cons,x),null)) -> x ap(last,ap(ap(cons,x),ap(ap(cons,y),ys))) -> ap(last,ap(ap(cons,y),ys)) ap(dropLast,ap(ap(cons,x),null)) -> null ap(dropLast,ap(ap(cons,x),ap(ap(cons,y),ys))) -> ap(ap(cons,x),ap(dropLast,ap(ap(cons,y),ys))) ) (COMMENT dropped these rules due to restrictions on secret examples ap(dropLast,nil) -> nil ap(ap(ap(if,false),f),xs) -> ap(ap(cons,ap(f,ap(last,xs))),ap(ap(map,f),ap(dropLast,xs))) and therefore added the second if->if2, and the if2->map rule moreover, to get the correct nr of functionsymbols, I identified nil and false to null the original system is ap(ap(map,f),xs) -> ap(ap(ap(if,ap(isEmpty,xs)),f),xs) ap(ap(ap(if,true),f),xs) -> nil ap(ap(ap(if,false),f),xs) -> ap(ap(cons,ap(f,ap(last,xs))),ap(ap(map,f),ap(dropLast,xs))) ap(isEmpty,nil) -> true ap(isEmpty,ap(ap(cons,x),xs)) -> false ap(last,ap(ap(cons,x),nil)) -> x ap(last,ap(ap(cons,x),ap(ap(cons,y),ys))) -> ap(last,ap(ap(cons,y),ys)) ap(dropLast,nil) -> nil ap(dropLast,ap(ap(cons,x),nil)) -> nil ap(dropLast,ap(ap(cons,x),ap(ap(cons,y),ys))) -> ap(ap(cons,x),ap(dropLast,ap(ap(cons,y),ys))) but in this TRS the second if-rule has 11 function-symbols )