Problem:
 a1() -> b1()
 a1() -> c1()
 b1() -> b2()
 c1() -> c2()
 a2() -> b2()
 a2() -> c2()
 b2() -> b3()
 c2() -> c3()
 a3() -> b3()
 a3() -> c3()
 b3() -> b4()
 c3() -> c4()
 a4() -> b4()
 a4() -> c4()
 b4() -> b5()
 c4() -> c5()
 a5() -> b5()
 a5() -> c5()
 b5() -> b6()
 c5() -> c6()
 a6() -> b6()
 a6() -> c6()
 b6() -> b7()
 c6() -> b7()
 b7() -> b1()
 b7() -> c1()

Proof:
 Uncurry Processor:
  a1() -> b1()
  a1() -> c1()
  b1() -> b2()
  c1() -> c2()
  a2() -> b2()
  a2() -> c2()
  b2() -> b3()
  c2() -> c3()
  a3() -> b3()
  a3() -> c3()
  b3() -> b4()
  c3() -> c4()
  a4() -> b4()
  a4() -> c4()
  b4() -> b5()
  c4() -> c5()
  a5() -> b5()
  a5() -> c5()
  b5() -> b6()
  c5() -> c6()
  a6() -> b6()
  a6() -> c6()
  b6() -> b7()
  c6() -> b7()
  b7() -> b1()
  b7() -> c1()
  Ground Confluence Processor:
   confluent by decision procedure.