1.21/1.31 NO 1.21/1.31 1.21/1.31 Problem: 1.21/1.31 f(a()) -> b() 1.21/1.31 a() -> a'() 1.21/1.31 f(b()) -> c() 1.21/1.31 1.21/1.31 Proof: 1.21/1.31 Uncurry Processor: 1.21/1.31 f5(f(),a()) -> b() 1.21/1.31 a() -> a'() 1.21/1.31 f5(f(),b()) -> c() 1.21/1.31 Ground Confluence Processor: 1.21/1.31 not UNR by decision procedure. 1.21/1.32 EOF