Input TRS: 1: and(true()) -> X 2: if(true()) -> X 3: if(false()) -> Y 4: add(|0|()) -> X 5: and(false()) -> false() 6: add(s()) -> s() 7: first(|0|(),X) -> nil() 8: first(s(),cons()) -> cons() 9: from() -> cons() Extra variable in rule 2. NO