YES 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: sorted: (order) 0:a1() -> b1() a1() -> c1() b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() 1:b1() -> b2() c1() -> c2() a2() -> b2() a2() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() 2:b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() a3() -> b3() a3() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() 3:b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() a4() -> b4() a4() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() 4:b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() a5() -> b5() a5() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() 5:b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() a6() -> b6() a6() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() ----- sorts [0>6, 1>6, 2>6, 3>6, 4>6, 5>6] sort attachment (non-strict) a1 : 0 b1 : 6 c1 : 6 b2 : 6 c2 : 6 a2 : 1 b3 : 6 c3 : 6 a3 : 2 b4 : 6 c4 : 6 a4 : 3 b5 : 6 c5 : 6 a5 : 4 b6 : 6 c6 : 6 a6 : 5 b7 : 6 ----- 0:a1() -> b1() a1() -> c1() b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() Uncurry Processor: a1() -> b1() a1() -> c1() b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() Ground Confluence Processor: confluent by decision procedure. 1:b1() -> b2() c1() -> c2() a2() -> b2() a2() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() Uncurry Processor: b1() -> b2() c1() -> c2() a2() -> b2() a2() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() Ground Confluence Processor: confluent by decision procedure. 2:b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() a3() -> b3() a3() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() Uncurry Processor: b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() a3() -> b3() a3() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() Ground Confluence Processor: confluent by decision procedure. 3:b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() a4() -> b4() a4() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() Uncurry Processor: b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() a4() -> b4() a4() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() Ground Confluence Processor: confluent by decision procedure. 4:b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() a5() -> b5() a5() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() Uncurry Processor: b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() a5() -> b5() a5() -> c5() b5() -> b6() c5() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() Ground Confluence Processor: confluent by decision procedure. 5:b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() a6() -> b6() a6() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() Uncurry Processor: b1() -> b2() c1() -> c2() b2() -> b3() c2() -> c3() b3() -> b4() c3() -> c4() b4() -> b5() c4() -> c5() b5() -> b6() c5() -> c6() a6() -> b6() a6() -> c6() b6() -> b7() c6() -> b7() b7() -> b1() b7() -> c1() Ground Confluence Processor: confluent by decision procedure.