Problem: a() -> f(b()) h(b(),f(c())) -> c() b() -> f(b()) b() -> f(c()) h(c(),c()) -> c() Proof: sorted: (order-sorted) 0:a() -> f(b()) b() -> f(b()) b() -> f(c()) 1:h(b(),f(c())) -> c() b() -> f(b()) b() -> f(c()) h(c(),c()) -> c() ----- sorts [0>4, 1>2, 1>3, 2>4, 3>4, 4>5] sort attachment (non-strict) a : 0 f : 4 -> 4 b : 4 h : 2 x 3 -> 1 c : 5 ----- 0:a() -> f(b()) b() -> f(b()) b() -> f(c()) Nonconfluence Processor: terms: f(f(f(c()))) *<- b() ->* f(c()) Qed 1:h(b(),f(c())) -> c() b() -> f(b()) b() -> f(c()) h(c(),c()) -> c() Open