YES Problem: c(z,x,a()) -> f(b(b(f(z),z),x)) b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) f(c(c(z,a(),a()),x,a())) -> z Proof: DP Processor: DPs: c#(z,x,a()) -> f#(z) c#(z,x,a()) -> b#(f(z),z) c#(z,x,a()) -> b#(b(f(z),z),x) c#(z,x,a()) -> f#(b(b(f(z),z),x)) b#(y,b(z,a())) -> f#(a()) b#(y,b(z,a())) -> c#(f(a()),y,z) b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z)) TRS: c(z,x,a()) -> f(b(b(f(z),z),x)) b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) f(c(c(z,a(),a()),x,a())) -> z EDG Processor: DPs: c#(z,x,a()) -> f#(z) c#(z,x,a()) -> b#(f(z),z) c#(z,x,a()) -> b#(b(f(z),z),x) c#(z,x,a()) -> f#(b(b(f(z),z),x)) b#(y,b(z,a())) -> f#(a()) b#(y,b(z,a())) -> c#(f(a()),y,z) b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z)) TRS: c(z,x,a()) -> f(b(b(f(z),z),x)) b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) f(c(c(z,a(),a()),x,a())) -> z graph: b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) -> b#(y,b(z,a())) -> f#(a()) b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) -> b#(y,b(z,a())) -> c#(f(a()),y,z) b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) -> b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) -> b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z)) b#(y,b(z,a())) -> c#(f(a()),y,z) -> c#(z,x,a()) -> f#(z) b#(y,b(z,a())) -> c#(f(a()),y,z) -> c#(z,x,a()) -> b#(f(z),z) b#(y,b(z,a())) -> c#(f(a()),y,z) -> c#(z,x,a()) -> b#(b(f(z),z),x) b#(y,b(z,a())) -> c#(f(a()),y,z) -> c#(z,x,a()) -> f#(b(b(f(z),z),x)) c#(z,x,a()) -> b#(b(f(z),z),x) -> b#(y,b(z,a())) -> f#(a()) c#(z,x,a()) -> b#(b(f(z),z),x) -> b#(y,b(z,a())) -> c#(f(a()),y,z) c#(z,x,a()) -> b#(b(f(z),z),x) -> b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) c#(z,x,a()) -> b#(b(f(z),z),x) -> b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z)) c#(z,x,a()) -> b#(f(z),z) -> b#(y,b(z,a())) -> f#(a()) c#(z,x,a()) -> b#(f(z),z) -> b#(y,b(z,a())) -> c#(f(a()),y,z) c#(z,x,a()) -> b#(f(z),z) -> b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) c#(z,x,a()) -> b#(f(z),z) -> b#(y,b(z,a())) -> f#(b(c(f(a()),y,z),z)) SCC Processor: #sccs: 1 #rules: 4 #arcs: 16/64 DPs: b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) b#(y,b(z,a())) -> c#(f(a()),y,z) c#(z,x,a()) -> b#(b(f(z),z),x) c#(z,x,a()) -> b#(f(z),z) TRS: c(z,x,a()) -> f(b(b(f(z),z),x)) b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) f(c(c(z,a(),a()),x,a())) -> z Bounds Processor: bound: 2 enrichment: top-dp automaton: final states: {36} transitions: b2(228,152) -> 229* c{#,0}(34,36,33) -> 36* c{#,0}(32,33,29) -> 35* c{#,0}(30,34,31) -> 35* c{#,0}(36,31,35) -> 35* c{#,0}(32,36,30) -> 35* c{#,0}(36,30,30) -> 35* c{#,0}(36,33,31) -> 35* c{#,0}(31,33,36) -> 35* c{#,0}(29,30,32) -> 35* c{#,0}(29,33,33) -> 35* c{#,0}(31,35,32) -> 35* c{#,0}(29,36,34) -> 35* c{#,0}(35,29,32) -> 35* c{#,0}(33,30,34) -> 35* c{#,0}(29,35,29) -> 35* c{#,0}(35,32,33) -> 35* c{#,0}(33,29,29) -> 35* c{#,0}(33,33,35) -> 35* c{#,0}(31,30,31) -> 35* c{#,0}(35,35,34) -> 35* c{#,0}(33,32,30) -> 35* c{#,0}(35,34,29) -> 35* c{#,0}(33,35,31) -> 35* c{#,0}(32,29,36) -> 35* c{#,0}(30,29,33) -> 35* c{#,0}(34,34,36) -> 36* c{#,0}(32,31,32) -> 35* c{#,0}(30,32,34) -> 35* c{#,0}(32,34,33) -> 35* c{#,0}(30,31,29) -> 35* c{#,0}(30,35,35) -> 35* c{#,0}(34,36,32) -> 36* c{#,0}(30,34,30) -> 35* c{#,0}(34,29,35) -> 36* c{#,0}(36,31,34) -> 35* c{#,0}(32,36,29) -> 35* c{#,0}(36,30,29) -> 35* c{#,0}(36,34,35) -> 35* c{#,0}(34,31,31) -> 36* c{#,0}(36,33,30) -> 35* c{#,0}(29,31,36) -> 35* c{#,0}(36,36,31) -> 35* c{#,0}(31,36,36) -> 35* c{#,0}(29,33,32) -> 35* c{#,0}(35,30,36) -> 35* c{#,0}(29,36,33) -> 35* c{#,0}(33,30,33) -> 35* c{#,0}(31,31,35) -> 35* c{#,0}(35,32,32) -> 35* c{#,0}(33,33,34) -> 35* c{#,0}(31,30,30) -> 35* c{#,0}(35,35,33) -> 35* c{#,0}(33,32,29) -> 35* c{#,0}(33,36,35) -> 35* c{#,0}(31,33,31) -> 35* c{#,0}(33,35,30) -> 35* c{#,0}(32,32,36) -> 35* c{#,0}(30,29,32) -> 35* c{#,0}(30,32,33) -> 35* c{#,0}(32,34,32) -> 35* c{#,0}(30,35,34) -> 35* c{#,0}(34,29,34) -> 36* c{#,0}(30,34,29) -> 35* c{#,0}(36,31,33) -> 35* c{#,0}(34,32,35) -> 36* c{#,0}(32,29,31) -> 35* c{#,0}(36,34,34) -> 35* c{#,0}(34,31,30) -> 36* c{#,0}(36,33,29) -> 35* c{#,0}(34,34,31) -> 36* c{#,0}(36,36,30) -> 35* c{#,0}(29,34,36) -> 35* c{#,0}(29,36,32) -> 35* c{#,0}(29,29,35) -> 35* c{#,0}(35,33,36) -> 35* c{#,0}(33,30,32) -> 35* c{#,0}(31,31,34) -> 35* c{#,0}(33,33,33) -> 35* c{#,0}(31,30,29) -> 35* c{#,0}(31,34,35) -> 35* c{#,0}(29,31,31) -> 35* c{#,0}(35,35,32) -> 35* c{#,0}(33,36,34) -> 35* c{#,0}(31,33,30) -> 35* c{#,0}(33,35,29) -> 35* c{#,0}(31,36,31) -> 35* c{#,0}(35,30,31) -> 35* c{#,0}(30,30,36) -> 35* c{#,0}(32,35,36) -> 35* c{#,0}(30,32,32) -> 35* c{#,0}(36,29,36) -> 35* c{#,0}(30,35,33) -> 35* c{#,0}(34,29,33) -> 36* c{#,0}(32,30,35) -> 35* c{#,0}(36,31,32) -> 35* c{#,0}(34,32,34) -> 36* c{#,0}(32,29,30) -> 35* c{#,0}(36,34,33) -> 35* c{#,0}(34,31,29) -> 36* c{#,0}(34,35,35) -> 36* c{#,0}(32,32,31) -> 35* c{#,0}(34,34,30) -> 36* c{#,0}(36,36,29) -> 35* c{#,0}(33,31,36) -> 35* c{#,0}(29,29,34) -> 35* c{#,0}(31,31,33) -> 35* c{#,0}(29,32,35) -> 35* c{#,0}(35,36,36) -> 35* c{#,0}(33,33,32) -> 35* c{#,0}(31,34,34) -> 35* c{#,0}(29,31,30) -> 35* c{#,0}(33,36,33) -> 35* c{#,0}(31,33,29) -> 35* c{#,0}(29,34,31) -> 35* c{#,0}(31,36,30) -> 35* c{#,0}(35,31,35) -> 35* c{#,0}(35,30,30) -> 35* c{#,0}(35,33,31) -> 35* c{#,0}(30,33,36) -> 35* c{#,0}(30,35,32) -> 35* c{#,0}(36,32,36) -> 35* c{#,0}(34,29,32) -> 36* c{#,0}(32,30,34) -> 35* c{#,0}(34,32,33) -> 36* c{#,0}(32,29,29) -> 35* c{#,0}(32,33,35) -> 35* c{#,0}(30,30,31) -> 35* c{#,0}(36,34,32) -> 35* c{#,0}(34,35,34) -> 36* c{#,0}(32,32,30) -> 35* c{#,0}(34,34,29) -> 36* c{#,0}(32,35,31) -> 35* c{#,0}(36,29,31) -> 35* c{#,0}(31,29,36) -> 35* c{#,0}(29,29,33) -> 35* c{#,0}(33,34,36) -> 35* c{#,0}(31,31,32) -> 35* c{#,0}(29,32,34) -> 35* c{#,0}(31,34,33) -> 35* c{#,0}(29,31,29) -> 35* c{#,0}(29,35,35) -> 35* c{#,0}(33,36,32) -> 35* c{#,0}(33,29,35) -> 35* c{#,0}(29,34,30) -> 35* c{#,0}(31,36,29) -> 35* c{#,0}(35,31,34) -> 35* c{#,0}(35,30,29) -> 35* c{#,0}(35,34,35) -> 35* c{#,0}(33,31,31) -> 35* c{#,0}(35,33,30) -> 35* c{#,0}(35,36,31) -> 35* c{#,0}(30,36,36) -> 35* c{#,0}(34,30,36) -> 36* c{#,0}(32,30,33) -> 35* c{#,0}(30,31,35) -> 35* c{#,0}(36,35,36) -> 35* c{#,0}(34,32,32) -> 36* c{#,0}(32,33,34) -> 35* c{#,0}(30,30,30) -> 35* c{#,0}(34,35,33) -> 36* c{#,0}(32,32,29) -> 35* c{#,0}(32,36,35) -> 35* c{#,0}(30,33,31) -> 35* c{#,0}(36,30,35) -> 35* c{#,0}(32,35,30) -> 35* c{#,0}(36,29,30) -> 35* c{#,0}(36,32,31) -> 35* c{#,0}(31,32,36) -> 35* c{#,0}(29,29,32) -> 35* c{#,0}(29,32,33) -> 35* c{#,0}(31,34,32) -> 35* c{#,0}(29,35,34) -> 35* c{#,0}(29,34,29) -> 35* c{#,0}(33,29,34) -> 35* c{#,0}(35,31,33) -> 35* c{#,0}(33,32,35) -> 35* c{#,0}(31,29,31) -> 35* c{#,0}(35,34,34) -> 35* c{#,0}(33,31,30) -> 35* c{#,0}(35,33,29) -> 35* c{#,0}(33,34,31) -> 35* c{#,0}(35,36,30) -> 35* c{#,0}(34,33,36) -> 36* c{#,0}(32,30,32) -> 35* c{#,0}(30,31,34) -> 35* c{#,0}(32,33,33) -> 35* c{#,0}(30,30,29) -> 35* c{#,0}(30,34,35) -> 35* c{#,0}(34,35,32) -> 36* c{#,0}(32,36,34) -> 35* c{#,0}(30,33,30) -> 35* c{#,0}(36,30,34) -> 35* c{#,0}(32,35,29) -> 35* c{#,0}(30,36,31) -> 35* c{#,0}(36,29,29) -> 35* c{#,0}(36,33,35) -> 35* c{#,0}(34,30,31) -> 36* c{#,0}(36,32,30) -> 35* c{#,0}(29,30,36) -> 35* c{#,0}(36,35,31) -> 35* c{#,0}(31,35,36) -> 35* c{#,0}(29,32,32) -> 35* c{#,0}(35,29,36) -> 35* c{#,0}(29,35,33) -> 35* c{#,0}(33,29,33) -> 35* c{#,0}(31,30,35) -> 35* c{#,0}(35,31,32) -> 35* c{#,0}(33,32,34) -> 35* c{#,0}(31,29,30) -> 35* c{#,0}(35,34,33) -> 35* c{#,0}(33,31,29) -> 35* c{#,0}(33,35,35) -> 35* c{#,0}(31,32,31) -> 35* c{#,0}(33,34,30) -> 35* c{#,0}(35,36,29) -> 35* c{#,0}(32,31,36) -> 35* c{#,0}(30,31,33) -> 35* c{#,0}(34,36,36) -> 36* c{#,0}(32,33,32) -> 35* c{#,0}(30,34,34) -> 35* c{#,0}(32,36,33) -> 35* c{#,0}(30,33,29) -> 35* c{#,0}(36,30,33) -> 35* c{#,0}(30,36,30) -> 35* c{#,0}(34,31,35) -> 36* c{#,0}(36,33,34) -> 35* c{#,0}(34,30,30) -> 36* c{#,0}(36,32,29) -> 35* c{#,0}(36,36,35) -> 35* c{#,0}(34,33,31) -> 36* c{#,0}(36,35,30) -> 35* c{#,0}(29,33,36) -> 35* c{#,0}(29,35,32) -> 35* c{#,0}(35,32,36) -> 35* c{#,0}(33,29,32) -> 35* c{#,0}(31,30,34) -> 35* c{#,0}(33,32,33) -> 35* c{#,0}(31,29,29) -> 35* c{#,0}(31,33,35) -> 35* c{#,0}(29,30,31) -> 35* c{#,0}(35,34,32) -> 35* c{#,0}(33,35,34) -> 35* c{#,0}(31,32,30) -> 35* c{#,0}(33,34,29) -> 35* c{#,0}(31,35,31) -> 35* c{#,0}(35,29,31) -> 35* c{#,0}(30,29,36) -> 35* c{#,0}(32,34,36) -> 35* c{#,0}(30,31,32) -> 35* c{#,0}(30,34,33) -> 35* c{#,0}(32,36,32) -> 35* c{#,0}(32,29,35) -> 35* c{#,0}(36,30,32) -> 35* c{#,0}(30,36,29) -> 35* c{#,0}(34,31,34) -> 36* c{#,0}(36,33,33) -> 35* c{#,0}(34,30,29) -> 36* c{#,0}(34,34,35) -> 36* c{#,0}(32,31,31) -> 35* c{#,0}(36,36,34) -> 35* c{#,0}(34,33,30) -> 36* c{#,0}(36,35,29) -> 35* c{#,0}(34,36,31) -> 36* c{#,0}(29,36,36) -> 35* c{#,0}(33,30,36) -> 35* c{#,0}(31,30,33) -> 35* c{#,0}(29,31,35) -> 35* c{#,0}(35,35,36) -> 35* c{#,0}(33,32,32) -> 35* c{#,0}(31,33,34) -> 35* c{#,0}(29,30,30) -> 35* c{#,0}(33,35,33) -> 35* c{#,0}(31,32,29) -> 35* c{#,0}(31,36,35) -> 35* c{#,0}(29,33,31) -> 35* c{#,0}(31,35,30) -> 35* c{#,0}(35,30,35) -> 35* c{#,0}(35,29,30) -> 35* c{#,0}(35,32,31) -> 35* c{#,0}(30,32,36) -> 35* c{#,0}(30,34,32) -> 35* c{#,0}(36,31,36) -> 35* c{#,0}(32,29,34) -> 35* c{#,0}(34,31,33) -> 36* c{#,0}(32,32,35) -> 35* c{#,0}(30,29,31) -> 35* c{#,0}(36,33,32) -> 35* c{#,0}(34,34,34) -> 36* c{#,0}(32,31,30) -> 35* c{#,0}(36,36,33) -> 35* c{#,0}(34,33,29) -> 36* c{#,0}(32,34,31) -> 35* c{#,0}(34,36,30) -> 36* c{#,0}(33,33,36) -> 35* c{#,0}(31,30,32) -> 35* c{#,0}(29,31,34) -> 35* c{#,0}(31,33,33) -> 35* c{#,0}(29,30,29) -> 35* c{#,0}(29,34,35) -> 35* c{#,0}(33,35,32) -> 35* c{#,0}(31,36,34) -> 35* c{#,0}(29,33,30) -> 35* c{#,0}(35,30,34) -> 35* c{#,0}(31,35,29) -> 35* c{#,0}(29,36,31) -> 35* c{#,0}(35,29,29) -> 35* c{#,0}(35,33,35) -> 35* c{#,0}(33,30,31) -> 35* c{#,0}(35,32,30) -> 35* c{#,0}(35,35,31) -> 35* c{#,0}(30,35,36) -> 35* c{#,0}(34,29,36) -> 36* c{#,0}(32,29,33) -> 35* c{#,0}(30,30,35) -> 35* c{#,0}(36,34,36) -> 35* c{#,0}(34,31,32) -> 36* c{#,0}(32,32,34) -> 35* c{#,0}(30,29,30) -> 35* c{#,0}(34,34,33) -> 36* c{#,0}(32,31,29) -> 35* c{#,0}(32,35,35) -> 35* c{#,0}(30,32,31) -> 35* c{#,0}(36,36,32) -> 35* c{#,0}(36,29,35) -> 35* c{#,0}(32,34,30) -> 35* c{#,0}(34,36,29) -> 36* c{#,0}(36,31,31) -> 35* c{#,0}(31,31,36) -> 35* c{#,0}(29,31,33) -> 35* c{#,0}(33,36,36) -> 35* c{#,0}(31,33,32) -> 35* c{#,0}(29,34,34) -> 35* c{#,0}(31,36,33) -> 35* c{#,0}(29,33,29) -> 35* c{#,0}(35,30,33) -> 35* c{#,0}(29,36,30) -> 35* c{#,0}(33,31,35) -> 35* c{#,0}(35,33,34) -> 35* c{#,0}(33,30,30) -> 35* c{#,0}(35,32,29) -> 35* c{#,0}(35,36,35) -> 35* c{#,0}(33,33,31) -> 35* c{#,0}(35,35,30) -> 35* c{#,0}(34,32,36) -> 36* c{#,0}(32,29,32) -> 35* c{#,0}(30,30,34) -> 35* c{#,0}(32,32,33) -> 35* c{#,0}(30,29,29) -> 35* c{#,0}(30,33,35) -> 35* c{#,0}(34,34,32) -> 36* c{#,0}(32,35,34) -> 35* c{#,0}(30,32,30) -> 35* c{#,0}(36,29,34) -> 35* c{#,0}(32,34,29) -> 35* c{#,0}(30,35,31) -> 35* c{#,0}(36,32,35) -> 35* c{#,0}(34,29,31) -> 36* c{#,0}(36,31,30) -> 35* c{#,0}(29,29,36) -> 35* c{#,0}(36,34,31) -> 35* c{#,0}(31,34,36) -> 35* c{#,0}(29,31,32) -> 35* c{#,0}(29,34,33) -> 35* c{#,0}(31,36,32) -> 35* c{#,0}(31,29,35) -> 35* c{#,0}(35,30,32) -> 35* c{#,0}(29,36,29) -> 35* c{#,0}(33,31,34) -> 35* c{#,0}(35,33,33) -> 35* c{#,0}(33,30,29) -> 35* c{#,0}(33,34,35) -> 35* c{#,0}(31,31,31) -> 35* c{#,0}(35,36,34) -> 35* c{#,0}(33,33,30) -> 35* c{#,0}(35,35,29) -> 35* c{#,0}(33,36,31) -> 35* c{#,0}(32,30,36) -> 35* c{#,0}(30,30,33) -> 35* c{#,0}(34,35,36) -> 36* c{#,0}(32,32,32) -> 35* c{#,0}(30,33,34) -> 35* c{#,0}(32,35,33) -> 35* c{#,0}(30,32,29) -> 35* c{#,0}(30,36,35) -> 35* c{#,0}(36,29,33) -> 35* c{#,0}(34,30,35) -> 36* c{#,0}(30,35,30) -> 35* c{#,0}(36,32,34) -> 35* c{#,0}(34,29,30) -> 36* c{#,0}(36,31,29) -> 35* c{#,0}(36,35,35) -> 35* c{#,0}(34,32,31) -> 36* c{#,0}(36,34,30) -> 35* c{#,0}(29,32,36) -> 35* c{#,0}(29,34,32) -> 35* c{#,0}(35,31,36) -> 35* c{#,0}(31,29,34) -> 35* c{#,0}(33,31,33) -> 35* c{#,0}(31,32,35) -> 35* c{#,0}(29,29,31) -> 35* c{#,0}(35,33,32) -> 35* c{#,0}(33,34,34) -> 35* c{#,0}(31,31,30) -> 35* c{#,0}(35,36,33) -> 35* c{#,0}(33,33,29) -> 35* c{#,0}(31,34,31) -> 35* c{#,0}(33,36,30) -> 35* c{#,0}(32,33,36) -> 35* c{#,0}(30,30,32) -> 35* c{#,0}(30,33,33) -> 35* c{#,0}(32,35,32) -> 35* c{#,0}(30,36,34) -> 35* c{#,0}(36,29,32) -> 35* c{#,0}(30,35,29) -> 35* c{#,0}(34,30,34) -> 36* c{#,0}(36,32,33) -> 35* c{#,0}(34,29,29) -> 36* c{#,0}(34,33,35) -> 36* c{#,0}(32,30,31) -> 35* c{#,0}(36,35,34) -> 35* c{#,0}(34,32,30) -> 36* c{#,0}(36,34,29) -> 35* c{#,0}(34,35,31) -> 36* c{#,0}(29,35,36) -> 35* c{#,0}(33,29,36) -> 35* c{#,0}(31,29,33) -> 35* c{#,0}(29,30,35) -> 35* c{#,0}(35,34,36) -> 35* c{#,0}(33,31,32) -> 35* c{#,0}(31,32,34) -> 35* c{#,0}(29,29,30) -> 35* c{#,0}(33,34,33) -> 35* c{#,0}(31,31,29) -> 35* c{#,0}(31,35,35) -> 35* c{#,0}(29,32,31) -> 35* c{#,0}(35,36,32) -> 35* c{#,0}(35,29,35) -> 35* c{#,0}(31,34,30) -> 35* c{#,0}(33,36,29) -> 35* c{#,0}(35,31,31) -> 35* c{#,0}(30,31,36) -> 35* c{#,0}(32,36,36) -> 35* c{#,0}(30,33,32) -> 35* c{#,0}(36,30,36) -> 35* c{#,0}(30,36,33) -> 35* c{#,0}(34,30,33) -> 36* c{#,0}(32,31,35) -> 35* c{#,0}(36,32,32) -> 35* c{#,0}(34,33,34) -> 36* c{#,0}(32,30,30) -> 35* c{#,0}(36,35,33) -> 35* c{#,0}(34,32,29) -> 36* c{#,0}(34,36,35) -> 36* c{#,0}(32,33,31) -> 35* c{#,0}(34,35,30) -> 36* c{#,0}(33,32,36) -> 35* c{#,0}(31,29,32) -> 35* c{#,0}(29,30,34) -> 35* c{#,0}(31,32,33) -> 35* c{#,0}(29,29,29) -> 35* c{#,0}(29,33,35) -> 35* c{#,0}(33,34,32) -> 35* c{#,0}(31,35,34) -> 35* c{#,0}(29,32,30) -> 35* c{#,0}(31,34,29) -> 35* c{#,0}(35,29,34) -> 35* c{#,0}(29,35,31) -> 35* c{#,0}(35,32,35) -> 35* c{#,0}(33,29,31) -> 35* c{#,0}(35,31,30) -> 35* c{#,0}(35,34,31) -> 35* c{#,0}(30,34,36) -> 35* c{#,0}(30,36,32) -> 35* c{#,0}(30,29,35) -> 35* c{#,0}(36,33,36) -> 35* c{#,0}(34,30,32) -> 36* c{#,0}(32,31,34) -> 35* c{#,0}(34,33,33) -> 36* c{#,0}(32,30,29) -> 35* c{#,0}(32,34,35) -> 35* c{#,0}(30,31,31) -> 35* c{#,0}(36,35,32) -> 35* c{#,0}(34,36,34) -> 36* c{#,0}(32,33,30) -> 35* c{#,0}(34,35,29) -> 36* c{#,0}(32,36,31) -> 35* c{#,0}(36,30,31) -> 35* c{#,0}(31,30,36) -> 35* c{#,0}(29,30,33) -> 35* c{#,0}(33,35,36) -> 35* c{#,0}(31,32,32) -> 35* c{#,0}(29,33,34) -> 35* c{#,0}(31,35,33) -> 35* c{#,0}(29,32,29) -> 35* c{#,0}(29,36,35) -> 35* c{#,0}(35,29,33) -> 35* c{#,0}(33,30,35) -> 35* c{#,0}(29,35,30) -> 35* c{#,0}(35,32,34) -> 35* c{#,0}(33,29,30) -> 35* c{#,0}(35,31,29) -> 35* c{#,0}(35,35,35) -> 35* c{#,0}(33,32,31) -> 35* c{#,0}(35,34,30) -> 35* c{#,0}(34,31,36) -> 36* c{#,0}(30,29,34) -> 35* c{#,0}(32,31,33) -> 35* c{#,0}(30,32,35) -> 35* c{#,0}(36,36,36) -> 35* c{#,0}(34,33,32) -> 36* c{#,0}(32,34,34) -> 35* c{#,0}(30,31,30) -> 35* b{#,1}(140,29) -> 36,29 b{#,1}(140,31) -> 36,29 b{#,1}(140,33) -> 36,35,29 b{#,1}(140,35) -> 36,29 b{#,1}(140,30) -> 36,29 b{#,1}(140,32) -> 36,29 b{#,1}(140,34) -> 36,29 b{#,1}(140,36) -> 36,29 b{#,1}(139,77) -> 35,36,29 c1(77,140,32) -> 140* c1(77,140,29) -> 140* c1(77,140,36) -> 140* c1(77,140,33) -> 140* c1(77,140,30) -> 140* c1(77,140,31) -> 140* c1(77,140,34) -> 140* c1(77,140,35) -> 140* c{#,2}(152,140,29) -> 35,36,29 c{#,2}(152,140,36) -> 35,36,29 c{#,2}(152,140,33) -> 35,36,29 c{#,2}(152,140,30) -> 35,36,29 c{#,2}(152,140,31) -> 35,36,29 c{#,2}(152,140,34) -> 35,36,29 c{#,2}(152,140,35) -> 35,36,29 c{#,2}(152,140,32) -> 35,36,29 f1(262) -> 140* f1(77) -> 139* f1(76) -> 77* a1() -> 76* c{#,1}(77,30,34) -> 35,36,29 c{#,1}(77,32,34) -> 36,29 c{#,1}(77,34,34) -> 29* c{#,1}(77,36,34) -> 29* c{#,1}(77,30,31) -> 35,36,29 c{#,1}(77,32,31) -> 36,29 c{#,1}(77,29,36) -> 29* c{#,1}(77,34,31) -> 29* c{#,1}(77,31,36) -> 29* c{#,1}(77,36,31) -> 29* c{#,1}(77,33,36) -> 35,29 c{#,1}(77,35,36) -> 29* c{#,1}(77,29,33) -> 29* c{#,1}(77,31,33) -> 29* c{#,1}(77,33,33) -> 35,29 c{#,1}(77,35,33) -> 29* c{#,1}(77,29,30) -> 29* c{#,1}(77,31,30) -> 29* c{#,1}(77,33,30) -> 35,29 c{#,1}(77,35,30) -> 29* c{#,1}(77,30,32) -> 35,36,29 c{#,1}(77,32,32) -> 36,29 c{#,1}(77,34,32) -> 29* c{#,1}(77,36,32) -> 29* c{#,1}(77,30,29) -> 35,36,29 c{#,1}(77,32,29) -> 36,29 c{#,1}(77,34,29) -> 29* c{#,1}(77,36,29) -> 29* c{#,1}(77,30,35) -> 35,36,29 c{#,1}(77,32,35) -> 36,29 c{#,1}(77,34,35) -> 29* c{#,1}(77,36,35) -> 29* c{#,1}(77,29,34) -> 29* c{#,1}(77,31,34) -> 29* c{#,1}(77,33,34) -> 35,29 c{#,1}(77,35,34) -> 29* c{#,1}(77,29,31) -> 29* c{#,1}(77,31,31) -> 29* c{#,1}(77,33,31) -> 35,29 c{#,1}(77,30,36) -> 35,36,29 c{#,1}(77,35,31) -> 29* c{#,1}(77,32,36) -> 36,29 c{#,1}(77,34,36) -> 29* c{#,1}(77,36,36) -> 29* c{#,1}(77,30,33) -> 35,36,29 c{#,1}(77,32,33) -> 36,29 c{#,1}(77,34,33) -> 29* c{#,1}(77,36,33) -> 29* c{#,1}(77,30,30) -> 35,36,29 c{#,1}(77,32,30) -> 36,29 c{#,1}(77,34,30) -> 29* c{#,1}(77,36,30) -> 29* c{#,1}(77,29,32) -> 29* c{#,1}(77,31,32) -> 29* c{#,1}(77,33,32) -> 35,29 c{#,1}(77,35,32) -> 29* c{#,1}(77,29,29) -> 29* c{#,1}(77,31,29) -> 29* c{#,1}(77,33,29) -> 35,29 c{#,1}(77,35,29) -> 29* c{#,1}(77,29,35) -> 29* c{#,1}(77,31,35) -> 29* c{#,1}(77,33,35) -> 35,29 c{#,1}(77,35,35) -> 29* b1(140,140) -> 262* b1(139,77) -> 140* b{#,2}(228,152) -> 35,36,29,33 b{#,2}(229,140) -> 35,36,29,33 b{#,0}(32,30) -> 36,29 b{#,0}(32,32) -> 36,29 b{#,0}(32,34) -> 29* b{#,0}(32,36) -> 36,29 b{#,0}(33,29) -> 35,29 b{#,0}(33,31) -> 29* b{#,0}(33,33) -> 35,29 b{#,0}(33,35) -> 35,29 b{#,0}(34,30) -> 29* b{#,0}(29,30) -> 29* b{#,0}(34,32) -> 29* b{#,0}(29,32) -> 29* b{#,0}(34,34) -> 29* b{#,0}(29,34) -> 29* b{#,0}(34,36) -> 29* b{#,0}(29,36) -> 29* b{#,0}(35,29) -> 29* b{#,0}(30,29) -> 35,36,29 b{#,0}(35,31) -> 29* b{#,0}(30,31) -> 35,36,29 b{#,0}(35,33) -> 29* b{#,0}(30,33) -> 35,36,29 b{#,0}(35,35) -> 29* b{#,0}(30,35) -> 35,36,29 b{#,0}(36,30) -> 29* b{#,0}(31,30) -> 29* b{#,0}(36,32) -> 29* b{#,0}(31,32) -> 29* b{#,0}(36,34) -> 29* b{#,0}(31,34) -> 29* b{#,0}(36,36) -> 29* b{#,0}(31,36) -> 29* b{#,0}(32,29) -> 36,29 b{#,0}(32,31) -> 36,29 b{#,0}(32,33) -> 36,29 b{#,0}(32,35) -> 36,29 b{#,0}(33,30) -> 35,29 b{#,0}(33,32) -> 35,29 b{#,0}(33,34) -> 36,29 b{#,0}(33,36) -> 35,29 b{#,0}(34,29) -> 29* b{#,0}(29,29) -> 29* b{#,0}(34,31) -> 35,29 b{#,0}(29,31) -> 29* b{#,0}(34,33) -> 29* b{#,0}(29,33) -> 29* b{#,0}(34,35) -> 29* b{#,0}(29,35) -> 29* b{#,0}(35,30) -> 29* b{#,0}(30,30) -> 35,36,29 b{#,0}(35,32) -> 29* b{#,0}(30,32) -> 35,36,29 b{#,0}(35,34) -> 29* b{#,0}(30,34) -> 35,36,29 b{#,0}(35,36) -> 29* b{#,0}(30,36) -> 35,36,29 b{#,0}(36,29) -> 29* b{#,0}(31,29) -> 29* b{#,0}(36,31) -> 29* b{#,0}(31,31) -> 29* b{#,0}(36,33) -> 29* b{#,0}(31,33) -> 29* b{#,0}(36,35) -> 29* b{#,0}(31,35) -> 29* f2(152) -> 228* f2(151) -> 152* b0(32,30) -> 30* b0(32,32) -> 30* b0(32,34) -> 30* b0(32,36) -> 30* b0(33,29) -> 30* b0(33,31) -> 30* b0(33,33) -> 30* b0(33,35) -> 30* b0(34,30) -> 30* b0(29,30) -> 30* b0(34,32) -> 30* b0(29,32) -> 30* b0(34,34) -> 30* b0(29,34) -> 30* b0(34,36) -> 30* b0(29,36) -> 30* b0(35,29) -> 30* b0(30,29) -> 30* b0(35,31) -> 30* b0(30,31) -> 30* b0(35,33) -> 30* b0(30,33) -> 30* b0(35,35) -> 30* b0(30,35) -> 30* b0(36,30) -> 30* b0(31,30) -> 30* b0(36,32) -> 30* b0(31,32) -> 30* b0(36,34) -> 30* b0(31,34) -> 30* b0(36,36) -> 30* b0(31,36) -> 30* b0(32,29) -> 30* b0(32,31) -> 30* b0(32,33) -> 30* b0(32,35) -> 30* b0(33,30) -> 30* b0(33,32) -> 30* b0(33,34) -> 30* b0(33,36) -> 30* b0(34,29) -> 30* b0(29,29) -> 30* b0(34,31) -> 30* b0(29,31) -> 30* b0(34,33) -> 30* b0(29,33) -> 30* b0(34,35) -> 30* b0(29,35) -> 30* b0(35,30) -> 30* b0(30,30) -> 30* b0(35,32) -> 30* b0(30,32) -> 30* b0(35,34) -> 30* b0(30,34) -> 30* b0(35,36) -> 30* b0(30,36) -> 30* b0(36,29) -> 30* b0(31,29) -> 30* b0(36,31) -> 30* b0(31,31) -> 30* b0(36,33) -> 30* b0(31,33) -> 30* b0(36,35) -> 30* b0(31,35) -> 30* a0() -> 31* a2() -> 151* c0(34,36,33) -> 32* c0(32,33,29) -> 32* c0(30,34,31) -> 32* c0(36,31,35) -> 32* c0(32,36,30) -> 32* c0(36,30,30) -> 32* c0(36,33,31) -> 32* c0(31,33,36) -> 32* c0(29,30,32) -> 32* c0(29,33,33) -> 32* c0(31,35,32) -> 32* c0(29,36,34) -> 32* c0(35,29,32) -> 32* c0(33,30,34) -> 32* c0(29,35,29) -> 32* c0(35,32,33) -> 32* c0(33,29,29) -> 32* c0(33,33,35) -> 32* c0(31,30,31) -> 32* c0(35,35,34) -> 32* c0(33,32,30) -> 32* c0(35,34,29) -> 32* c0(33,35,31) -> 32* c0(32,29,36) -> 32* c0(30,29,33) -> 32* c0(34,34,36) -> 32* c0(32,31,32) -> 32* c0(30,32,34) -> 32* c0(32,34,33) -> 32* c0(30,31,29) -> 32* c0(30,35,35) -> 32* c0(34,36,32) -> 32* c0(30,34,30) -> 32* c0(34,29,35) -> 32* c0(36,31,34) -> 32* c0(32,36,29) -> 32* c0(36,30,29) -> 32* c0(36,34,35) -> 32* c0(34,31,31) -> 32* c0(36,33,30) -> 32* c0(29,31,36) -> 32* c0(36,36,31) -> 32* c0(31,36,36) -> 32* c0(29,33,32) -> 32* c0(35,30,36) -> 32* c0(29,36,33) -> 32* c0(33,30,33) -> 32* c0(31,31,35) -> 32* c0(35,32,32) -> 32* c0(33,33,34) -> 32* c0(31,30,30) -> 32* c0(35,35,33) -> 32* c0(33,32,29) -> 32* c0(33,36,35) -> 32* c0(31,33,31) -> 32* c0(33,35,30) -> 32* c0(32,32,36) -> 32* c0(30,29,32) -> 32* c0(30,32,33) -> 32* c0(32,34,32) -> 32* c0(30,35,34) -> 32* c0(34,29,34) -> 32* c0(30,34,29) -> 32* c0(36,31,33) -> 32* c0(34,32,35) -> 32* c0(32,29,31) -> 32* c0(36,34,34) -> 32* c0(34,31,30) -> 32* c0(36,33,29) -> 32* c0(34,34,31) -> 32* c0(36,36,30) -> 32* c0(29,34,36) -> 32* c0(29,36,32) -> 32* c0(29,29,35) -> 32* c0(35,33,36) -> 32* c0(33,30,32) -> 32* c0(31,31,34) -> 32* c0(33,33,33) -> 32* c0(31,30,29) -> 32* c0(31,34,35) -> 32* c0(29,31,31) -> 32* c0(35,35,32) -> 32* c0(33,36,34) -> 32* c0(31,33,30) -> 32* c0(33,35,29) -> 32* c0(31,36,31) -> 32* c0(35,30,31) -> 32* c0(30,30,36) -> 32* c0(32,35,36) -> 32* c0(30,32,32) -> 32* c0(36,29,36) -> 32* c0(30,35,33) -> 32* c0(34,29,33) -> 32* c0(32,30,35) -> 32* c0(36,31,32) -> 32* c0(34,32,34) -> 32* c0(32,29,30) -> 32* c0(36,34,33) -> 32* c0(34,31,29) -> 32* c0(34,35,35) -> 32* c0(32,32,31) -> 32* c0(34,34,30) -> 32* c0(36,36,29) -> 32* c0(33,31,36) -> 32* c0(29,29,34) -> 32* c0(31,31,33) -> 32* c0(29,32,35) -> 32* c0(35,36,36) -> 32* c0(33,33,32) -> 32* c0(31,34,34) -> 32* c0(29,31,30) -> 32* c0(33,36,33) -> 32* c0(31,33,29) -> 32* c0(29,34,31) -> 32* c0(31,36,30) -> 32* c0(35,31,35) -> 32* c0(35,30,30) -> 32* c0(35,33,31) -> 32* c0(30,33,36) -> 32* c0(30,35,32) -> 32* c0(36,32,36) -> 32* c0(34,29,32) -> 32* c0(32,30,34) -> 32* c0(34,32,33) -> 32* c0(32,29,29) -> 32* c0(32,33,35) -> 32* c0(30,30,31) -> 32* c0(36,34,32) -> 32* c0(34,35,34) -> 32* c0(32,32,30) -> 32* c0(34,34,29) -> 32* c0(32,35,31) -> 32* c0(36,29,31) -> 32* c0(31,29,36) -> 32* c0(29,29,33) -> 32* c0(33,34,36) -> 32* c0(31,31,32) -> 32* c0(29,32,34) -> 32* c0(31,34,33) -> 32* c0(29,31,29) -> 32* c0(29,35,35) -> 32* c0(33,36,32) -> 32* c0(29,34,30) -> 32* c0(33,29,35) -> 32* c0(31,36,29) -> 32* c0(35,31,34) -> 32* c0(35,30,29) -> 32* c0(35,34,35) -> 32* c0(33,31,31) -> 32* c0(35,33,30) -> 32* c0(35,36,31) -> 32* c0(30,36,36) -> 32* c0(34,30,36) -> 32* c0(32,30,33) -> 32* c0(30,31,35) -> 32* c0(36,35,36) -> 32* c0(34,32,32) -> 32* c0(32,33,34) -> 32* c0(30,30,30) -> 32* c0(34,35,33) -> 32* c0(32,32,29) -> 32* c0(32,36,35) -> 32* c0(30,33,31) -> 32* c0(36,30,35) -> 32* c0(32,35,30) -> 32* c0(36,29,30) -> 32* c0(36,32,31) -> 32* c0(31,32,36) -> 32* c0(29,29,32) -> 32* c0(29,32,33) -> 32* c0(31,34,32) -> 32* c0(29,35,34) -> 32* c0(29,34,29) -> 32* c0(33,29,34) -> 32* c0(35,31,33) -> 32* c0(33,32,35) -> 32* c0(31,29,31) -> 32* c0(35,34,34) -> 32* c0(33,31,30) -> 32* c0(35,33,29) -> 32* c0(33,34,31) -> 32* c0(35,36,30) -> 32* c0(34,33,36) -> 32* c0(32,30,32) -> 32* c0(30,31,34) -> 32* c0(32,33,33) -> 32* c0(30,30,29) -> 32* c0(30,34,35) -> 32* c0(34,35,32) -> 32* c0(32,36,34) -> 32* c0(30,33,30) -> 32* c0(36,30,34) -> 32* c0(32,35,29) -> 32* c0(30,36,31) -> 32* c0(36,29,29) -> 32* c0(36,33,35) -> 32* c0(34,30,31) -> 32* c0(36,32,30) -> 32* c0(29,30,36) -> 32* c0(36,35,31) -> 32* c0(31,35,36) -> 32* c0(29,32,32) -> 32* c0(35,29,36) -> 32* c0(29,35,33) -> 32* c0(33,29,33) -> 32* c0(31,30,35) -> 32* c0(35,31,32) -> 32* c0(33,32,34) -> 32* c0(31,29,30) -> 32* c0(35,34,33) -> 32* c0(33,31,29) -> 32* c0(33,35,35) -> 32* c0(31,32,31) -> 32* c0(33,34,30) -> 32* c0(35,36,29) -> 32* c0(32,31,36) -> 32* c0(30,31,33) -> 32* c0(34,36,36) -> 32* c0(32,33,32) -> 32* c0(30,34,34) -> 32* c0(32,36,33) -> 32* c0(30,33,29) -> 32* c0(36,30,33) -> 32* c0(30,36,30) -> 32* c0(34,31,35) -> 32* c0(36,33,34) -> 32* c0(34,30,30) -> 32* c0(36,32,29) -> 32* c0(36,36,35) -> 32* c0(34,33,31) -> 32* c0(36,35,30) -> 32* c0(29,33,36) -> 32* c0(29,35,32) -> 32* c0(35,32,36) -> 32* c0(33,29,32) -> 32* c0(31,30,34) -> 32* c0(33,32,33) -> 32* c0(31,29,29) -> 32* c0(31,33,35) -> 32* c0(29,30,31) -> 32* c0(35,34,32) -> 32* c0(33,35,34) -> 32* c0(31,32,30) -> 32* c0(33,34,29) -> 32* c0(31,35,31) -> 32* c0(35,29,31) -> 32* c0(30,29,36) -> 32* c0(32,34,36) -> 32* c0(30,31,32) -> 32* c0(30,34,33) -> 32* c0(32,36,32) -> 32* c0(32,29,35) -> 32* c0(36,30,32) -> 32* c0(30,36,29) -> 32* c0(34,31,34) -> 32* c0(36,33,33) -> 32* c0(34,30,29) -> 32* c0(34,34,35) -> 32* c0(32,31,31) -> 32* c0(36,36,34) -> 32* c0(34,33,30) -> 32* c0(36,35,29) -> 32* c0(34,36,31) -> 32* c0(29,36,36) -> 32* c0(33,30,36) -> 32* c0(31,30,33) -> 32* c0(29,31,35) -> 32* c0(35,35,36) -> 32* c0(33,32,32) -> 32* c0(31,33,34) -> 32* c0(29,30,30) -> 32* c0(33,35,33) -> 32* c0(31,32,29) -> 32* c0(31,36,35) -> 32* c0(29,33,31) -> 32* c0(31,35,30) -> 32* c0(35,30,35) -> 32* c0(35,29,30) -> 32* c0(35,32,31) -> 32* c0(30,32,36) -> 32* c0(30,34,32) -> 32* c0(36,31,36) -> 32* c0(32,29,34) -> 32* c0(34,31,33) -> 32* c0(32,32,35) -> 32* c0(30,29,31) -> 32* c0(36,33,32) -> 32* c0(34,34,34) -> 32* c0(32,31,30) -> 32* c0(36,36,33) -> 32* c0(34,33,29) -> 32* c0(32,34,31) -> 32* c0(34,36,30) -> 32* c0(33,33,36) -> 32* c0(31,30,32) -> 32* c0(29,31,34) -> 32* c0(31,33,33) -> 32* c0(29,30,29) -> 32* c0(29,34,35) -> 32* c0(33,35,32) -> 32* c0(31,36,34) -> 32* c0(29,33,30) -> 32* c0(35,30,34) -> 32* c0(31,35,29) -> 32* c0(29,36,31) -> 32* c0(35,29,29) -> 32* c0(35,33,35) -> 32* c0(33,30,31) -> 32* c0(35,32,30) -> 32* c0(35,35,31) -> 32* c0(30,35,36) -> 32* c0(34,29,36) -> 32* c0(32,29,33) -> 32* c0(30,30,35) -> 32* c0(36,34,36) -> 32* c0(34,31,32) -> 32* c0(32,32,34) -> 32* c0(30,29,30) -> 32* c0(34,34,33) -> 32* c0(32,31,29) -> 32* c0(32,35,35) -> 32* c0(30,32,31) -> 32* c0(36,36,32) -> 32* c0(36,29,35) -> 32* c0(32,34,30) -> 32* c0(34,36,29) -> 32* c0(36,31,31) -> 32* c0(31,31,36) -> 32* c0(29,31,33) -> 32* c0(33,36,36) -> 32* c0(31,33,32) -> 32* c0(29,34,34) -> 32* c0(31,36,33) -> 32* c0(29,33,29) -> 32* c0(35,30,33) -> 32* c0(29,36,30) -> 32* c0(33,31,35) -> 32* c0(35,33,34) -> 32* c0(33,30,30) -> 32* c0(35,32,29) -> 32* c0(35,36,35) -> 32* c0(33,33,31) -> 32* c0(35,35,30) -> 32* c0(34,32,36) -> 32* c0(32,29,32) -> 32* c0(30,30,34) -> 32* c0(32,32,33) -> 32* c0(30,29,29) -> 32* c0(30,33,35) -> 32* c0(34,34,32) -> 32* c0(32,35,34) -> 32* c0(30,32,30) -> 32* c0(36,29,34) -> 32* c0(32,34,29) -> 32* c0(30,35,31) -> 32* c0(36,32,35) -> 32* c0(34,29,31) -> 32* c0(36,31,30) -> 32* c0(29,29,36) -> 32* c0(36,34,31) -> 32* c0(31,34,36) -> 32* c0(29,31,32) -> 32* c0(29,34,33) -> 32* c0(31,36,32) -> 32* c0(31,29,35) -> 32* c0(35,30,32) -> 32* c0(29,36,29) -> 32* c0(33,31,34) -> 32* c0(35,33,33) -> 32* c0(33,30,29) -> 32* c0(33,34,35) -> 32* c0(31,31,31) -> 32* c0(35,36,34) -> 32* c0(33,33,30) -> 32* c0(35,35,29) -> 32* c0(33,36,31) -> 32* c0(32,30,36) -> 32* c0(30,30,33) -> 32* c0(34,35,36) -> 32* c0(32,32,32) -> 32* c0(30,33,34) -> 32* c0(32,35,33) -> 32* c0(30,32,29) -> 32* c0(30,36,35) -> 32* c0(36,29,33) -> 32* c0(34,30,35) -> 32* c0(30,35,30) -> 32* c0(36,32,34) -> 32* c0(34,29,30) -> 32* c0(36,31,29) -> 32* c0(36,35,35) -> 32* c0(34,32,31) -> 32* c0(36,34,30) -> 32* c0(29,32,36) -> 32* c0(29,34,32) -> 32* c0(35,31,36) -> 32* c0(31,29,34) -> 32* c0(33,31,33) -> 32* c0(31,32,35) -> 32* c0(29,29,31) -> 32* c0(35,33,32) -> 32* c0(33,34,34) -> 32* c0(31,31,30) -> 32* c0(35,36,33) -> 32* c0(33,33,29) -> 32* c0(31,34,31) -> 32* c0(33,36,30) -> 32* c0(32,33,36) -> 32* c0(30,30,32) -> 32* c0(30,33,33) -> 32* c0(32,35,32) -> 32* c0(30,36,34) -> 32* c0(36,29,32) -> 32* c0(30,35,29) -> 32* c0(34,30,34) -> 32* c0(36,32,33) -> 32* c0(34,29,29) -> 32* c0(34,33,35) -> 32* c0(32,30,31) -> 32* c0(36,35,34) -> 32* c0(34,32,30) -> 32* c0(36,34,29) -> 32* c0(34,35,31) -> 32* c0(29,35,36) -> 32* c0(33,29,36) -> 32* c0(31,29,33) -> 32* c0(29,30,35) -> 32* c0(35,34,36) -> 32* c0(33,31,32) -> 32* c0(31,32,34) -> 32* c0(29,29,30) -> 32* c0(33,34,33) -> 32* c0(31,31,29) -> 32* c0(31,35,35) -> 32* c0(29,32,31) -> 32* c0(35,36,32) -> 32* c0(35,29,35) -> 32* c0(31,34,30) -> 32* c0(33,36,29) -> 32* c0(35,31,31) -> 32* c0(30,31,36) -> 32* c0(32,36,36) -> 32* c0(30,33,32) -> 32* c0(36,30,36) -> 32* c0(30,36,33) -> 32* c0(34,30,33) -> 32* c0(32,31,35) -> 32* c0(36,32,32) -> 32* c0(34,33,34) -> 32* c0(32,30,30) -> 32* c0(36,35,33) -> 32* c0(34,32,29) -> 32* c0(34,36,35) -> 32* c0(32,33,31) -> 32* c0(34,35,30) -> 32* c0(33,32,36) -> 32* c0(31,29,32) -> 32* c0(29,30,34) -> 32* c0(31,32,33) -> 32* c0(29,29,29) -> 32* c0(29,33,35) -> 32* c0(33,34,32) -> 32* c0(31,35,34) -> 32* c0(29,32,30) -> 32* c0(31,34,29) -> 32* c0(35,29,34) -> 32* c0(29,35,31) -> 32* c0(35,32,35) -> 32* c0(33,29,31) -> 32* c0(35,31,30) -> 32* c0(35,34,31) -> 32* c0(30,34,36) -> 32* c0(30,36,32) -> 32* c0(30,29,35) -> 32* c0(36,33,36) -> 32* c0(34,30,32) -> 32* c0(32,31,34) -> 32* c0(34,33,33) -> 32* c0(32,30,29) -> 32* c0(32,34,35) -> 32* c0(30,31,31) -> 32* c0(36,35,32) -> 32* c0(34,36,34) -> 32* c0(32,33,30) -> 32* c0(34,35,29) -> 32* c0(32,36,31) -> 32* c0(36,30,31) -> 32* c0(31,30,36) -> 32* c0(29,30,33) -> 32* c0(33,35,36) -> 32* c0(31,32,32) -> 32* c0(29,33,34) -> 32* c0(31,35,33) -> 32* c0(29,32,29) -> 32* c0(29,36,35) -> 32* c0(35,29,33) -> 32* c0(33,30,35) -> 32* c0(29,35,30) -> 32* c0(35,32,34) -> 32* c0(33,29,30) -> 32* c0(35,31,29) -> 32* c0(35,35,35) -> 32* c0(33,32,31) -> 32* c0(35,34,30) -> 32* c0(34,31,36) -> 32* c0(30,29,34) -> 32* c0(32,31,33) -> 32* c0(30,32,35) -> 32* c0(36,36,36) -> 32* c0(34,33,32) -> 32* c0(32,34,34) -> 32* c0(30,31,30) -> 32* f0(35) -> 33* f0(30) -> 30,32,33 f0(32) -> 33* f0(34) -> 33* f0(29) -> 33* f0(36) -> 33* f0(31) -> 34* f0(33) -> 33* 29 -> 33* 30 -> 33* 31 -> 33* 32 -> 33* 34 -> 33* 35 -> 33* 36 -> 33* problem: DPs: b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) c#(z,x,a()) -> b#(b(f(z),z),x) c#(z,x,a()) -> b#(f(z),z) TRS: c(z,x,a()) -> f(b(b(f(z),z),x)) b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) f(c(c(z,a(),a()),x,a())) -> z Matrix Interpretation Processor: dimension: 1 interpretation: [b#](x0, x1) = 0, [c#](x0, x1, x2) = x0 + x1 + x2, [b](x0, x1) = 0, [f](x0) = x0, [c](x0, x1, x2) = x0, [a] = 1 orientation: b#(y,b(z,a())) = 0 >= 0 = b#(c(f(a()),y,z),z) c#(z,x,a()) = x + z + 1 >= 0 = b#(b(f(z),z),x) c#(z,x,a()) = x + z + 1 >= 0 = b#(f(z),z) c(z,x,a()) = z >= 0 = f(b(b(f(z),z),x)) b(y,b(z,a())) = 0 >= 0 = f(b(c(f(a()),y,z),z)) f(c(c(z,a(),a()),x,a())) = z >= z = z problem: DPs: b#(y,b(z,a())) -> b#(c(f(a()),y,z),z) TRS: c(z,x,a()) -> f(b(b(f(z),z),x)) b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) f(c(c(z,a(),a()),x,a())) -> z Subterm Criterion Processor: simple projection: pi(b#) = 1 problem: DPs: TRS: c(z,x,a()) -> f(b(b(f(z),z),x)) b(y,b(z,a())) -> f(b(c(f(a()),y,z),z)) f(c(c(z,a(),a()),x,a())) -> z Qed