YES Problem: f(a()) -> g(h(a())) h(g(x)) -> g(h(f(x))) k(x,h(x),a()) -> h(x) k(f(x),y,x) -> f(x) Proof: DP Processor: DPs: f#(a()) -> h#(a()) h#(g(x)) -> f#(x) h#(g(x)) -> h#(f(x)) TRS: f(a()) -> g(h(a())) h(g(x)) -> g(h(f(x))) k(x,h(x),a()) -> h(x) k(f(x),y,x) -> f(x) EDG Processor: DPs: f#(a()) -> h#(a()) h#(g(x)) -> f#(x) h#(g(x)) -> h#(f(x)) TRS: f(a()) -> g(h(a())) h(g(x)) -> g(h(f(x))) k(x,h(x),a()) -> h(x) k(f(x),y,x) -> f(x) graph: h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> f#(x) h#(g(x)) -> h#(f(x)) -> h#(g(x)) -> h#(f(x)) h#(g(x)) -> f#(x) -> f#(a()) -> h#(a()) SCC Processor: #sccs: 1 #rules: 1 #arcs: 3/9 DPs: h#(g(x)) -> h#(f(x)) TRS: f(a()) -> g(h(a())) h(g(x)) -> g(h(f(x))) k(x,h(x),a()) -> h(x) k(f(x),y,x) -> f(x) Bounds Processor: bound: 2 enrichment: match automaton: final states: {6} transitions: h{#,0}(40) -> 6* h{#,0}(5) -> 6* h{#,0}(37) -> 6* h{#,0}(27) -> 6* h{#,0}(39) -> 6* h{#,0}(4) -> 6* h{#,0}(41) -> 6* h{#,0}(26) -> 6* h{#,0}(1) -> 6* h{#,0}(38) -> 6* h{#,0}(28) -> 6* h{#,0}(3) -> 6* g0(50) -> 1* g0(40) -> 1* g0(5) -> 1* g0(37) -> 1* g0(27) -> 1* g0(2) -> 1* g0(39) -> 1* g0(41) -> 1* g0(26) -> 1* g0(1) -> 1* g0(38) -> 1* g0(28) -> 1* g0(3) -> 1* k0(41,38,27) -> 5* k0(4,3,26) -> 5* k0(50,2,4) -> 5* k0(1,1,3) -> 5* k0(40,28,5) -> 5* k0(37,1,41) -> 5* k0(2,40,38) -> 5* k0(38,5,26) -> 5* k0(26,39,26) -> 5* k0(41,28,50) -> 5* k0(4,37,5) -> 5* k0(5,1,40) -> 5* k0(4,26,2) -> 5* k0(40,38,3) -> 5* k0(5,37,50) -> 5* k0(3,3,2) -> 5* k0(41,41,28) -> 5* k0(50,5,5) -> 5* k0(38,39,5) -> 5* k0(1,4,4) -> 5* k0(39,3,40) -> 5* k0(27,37,40) -> 5* k0(4,27,28) -> 5* k0(5,50,28) -> 5* k0(37,5,2) -> 5* k0(38,28,2) -> 5* k0(27,26,37) -> 5* k0(5,4,41) -> 5* k0(2,37,2) -> 5* k0(3,1,37) -> 5* k0(40,41,4) -> 5* k0(41,5,39) -> 5* k0(27,40,41) -> 5* k0(50,39,50) -> 5* k0(4,50,4) -> 5* k0(37,3,37) -> 5* k0(4,39,1) -> 5* k0(3,4,38) -> 5* k0(27,3,26) -> 5* k0(40,39,39) -> 5* k0(5,1,5) -> 5* k0(38,41,1) -> 5* k0(1,41,50) -> 5* k0(41,2,3) -> 5* k0(1,26,41) -> 5* k0(2,50,1) -> 5* k0(28,1,40) -> 5* k0(39,3,5) -> 5* k0(27,37,5) -> 5* k0(38,50,39) -> 5* k0(37,27,39) -> 5* k0(27,26,2) -> 5* k0(40,3,50) -> 5* k0(28,37,50) -> 5* k0(26,3,2) -> 5* k0(50,37,40) -> 5* k0(37,1,27) -> 5* k0(28,50,28) -> 5* k0(3,28,40) -> 5* k0(27,27,28) -> 5* k0(50,26,37) -> 5* k0(41,5,4) -> 5* k0(28,4,41) -> 5* k0(3,2,28) -> 5* k0(26,1,37) -> 5* k0(40,26,26) -> 5* k0(5,3,1) -> 5* k0(1,39,40) -> 5* k0(37,4,28) -> 5* k0(50,40,41) -> 5* k0(27,50,4) -> 5* k0(1,28,37) -> 5* k0(39,5,1) -> 5* k0(27,39,1) -> 5* k0(26,4,38) -> 5* k0(50,3,26) -> 5* k0(38,37,26) -> 5* k0(28,1,5) -> 5* k0(37,27,4) -> 5* k0(4,38,27) -> 5* k0(5,27,3) -> 5* k0(50,37,5) -> 5* k0(3,28,5) -> 5* k0(41,27,41) -> 5* k0(38,40,27) -> 5* k0(50,26,2) -> 5* k0(1,5,26) -> 5* k0(4,28,50) -> 5* k0(26,28,40) -> 5* k0(50,27,28) -> 5* k0(4,41,28) -> 5* k0(3,38,3) -> 5* k0(41,37,39) -> 5* k0(1,39,5) -> 5* k0(39,38,41) -> 5* k0(2,3,40) -> 5* k0(26,2,28) -> 5* k0(37,40,3) -> 5* k0(1,28,2) -> 5* k0(39,27,38) -> 5* k0(28,3,1) -> 5* k0(50,50,4) -> 5* k0(39,1,26) -> 5* k0(3,41,4) -> 5* k0(41,40,40) -> 5* k0(4,5,39) -> 5* k0(50,39,1) -> 5* k0(5,2,27) -> 5* k0(37,38,38) -> 5* k0(5,38,37) -> 5* k0(3,39,39) -> 5* k0(39,4,27) -> 5* k0(27,38,27) -> 5* k0(38,1,2) -> 5* k0(28,27,3) -> 5* k0(1,41,1) -> 5* k0(39,40,37) -> 5* k0(26,28,5) -> 5* k0(4,2,3) -> 5* k0(37,41,39) -> 5* k0(41,37,4) -> 5* k0(27,28,50) -> 5* k0(5,41,38) -> 5* k0(41,26,1) -> 5* k0(2,3,5) -> 5* k0(40,2,41) -> 5* k0(1,50,39) -> 5* k0(27,41,28) -> 5* k0(38,4,3) -> 5* k0(26,38,3) -> 5* k0(3,3,50) -> 5* k0(4,5,4) -> 5* k0(37,5,50) -> 5* k0(41,40,5) -> 5* k0(39,37,1) -> 5* k0(38,2,38) -> 5* k0(26,41,4) -> 5* k0(3,26,26) -> 5* k0(27,5,39) -> 5* k0(5,38,2) -> 5* k0(41,50,3) -> 5* k0(28,2,27) -> 5* k0(37,28,26) -> 5* k0(39,40,2) -> 5* k0(2,5,1) -> 5* k0(40,4,37) -> 5* k0(28,38,37) -> 5* k0(26,39,39) -> 5* k0(50,38,27) -> 5* k0(1,37,26) -> 5* k0(38,26,40) -> 5* k0(27,2,3) -> 5* k0(50,28,50) -> 5* k0(28,41,38) -> 5* k0(4,27,41) -> 5* k0(26,3,50) -> 5* k0(50,41,28) -> 5* k0(1,40,27) -> 5* k0(40,1,1) -> 5* k0(40,28,39) -> 5* k0(27,5,4) -> 5* k0(4,37,39) -> 5* k0(2,38,41) -> 5* k0(2,27,38) -> 5* k0(26,26,26) -> 5* k0(50,5,39) -> 5* k0(28,38,2) -> 5* k0(2,1,26) -> 5* k0(4,40,40) -> 5* k0(40,5,28) -> 5* k0(38,26,5) -> 5* k0(5,37,28) -> 5* k0(39,26,50) -> 5* k0(41,38,26) -> 5* k0(39,39,28) -> 5* k0(2,4,27) -> 5* k0(50,2,3) -> 5* k0(1,1,2) -> 5* k0(40,28,4) -> 5* k0(37,1,40) -> 5* k0(2,40,37) -> 5* k0(27,27,41) -> 5* k0(5,1,39) -> 5* k0(37,37,50) -> 5* k0(4,37,4) -> 5* k0(3,2,41) -> 5* k0(41,41,27) -> 5* k0(4,26,1) -> 5* k0(37,50,28) -> 5* k0(50,5,4) -> 5* k0(38,39,4) -> 5* k0(1,4,3) -> 5* k0(39,3,39) -> 5* k0(27,37,39) -> 5* k0(5,50,27) -> 5* k0(38,28,1) -> 5* k0(37,4,41) -> 5* k0(4,40,5) -> 5* k0(5,4,40) -> 5* k0(2,37,1) -> 5* k0(40,41,3) -> 5* k0(1,2,38) -> 5* k0(27,40,40) -> 5* k0(4,50,3) -> 5* k0(28,37,28) -> 5* k0(40,50,41) -> 5* k0(37,1,5) -> 5* k0(2,40,2) -> 5* k0(40,39,38) -> 5* k0(3,4,37) -> 5* k0(5,1,4) -> 5* k0(38,1,50) -> 5* k0(41,2,2) -> 5* k0(50,27,41) -> 5* k0(1,26,40) -> 5* k0(39,3,4) -> 5* k0(27,37,4) -> 5* k0(28,1,39) -> 5* k0(38,50,38) -> 5* k0(26,2,41) -> 5* k0(27,26,1) -> 5* k0(5,4,5) -> 5* k0(28,50,27) -> 5* k0(3,1,1) -> 5* k0(3,28,39) -> 5* k0(41,5,3) -> 5* k0(27,40,5) -> 5* k0(28,4,40) -> 5* k0(37,3,1) -> 5* k0(38,27,27) -> 5* k0(50,40,40) -> 5* k0(27,50,3) -> 5* k0(5,38,50) -> 5* k0(41,3,38) -> 5* k0(3,5,28) -> 5* k0(39,40,50) -> 5* k0(26,4,37) -> 5* k0(1,26,5) -> 5* k0(28,1,4) -> 5* k0(37,27,3) -> 5* k0(2,26,50) -> 5* k0(4,38,26) -> 5* k0(2,39,28) -> 5* k0(50,37,4) -> 5* k0(3,28,4) -> 5* k0(41,27,40) -> 5* k0(38,40,26) -> 5* k0(50,26,1) -> 5* k0(41,1,28) -> 5* k0(28,4,5) -> 5* k0(26,1,1) -> 5* k0(26,28,39) -> 5* k0(4,41,27) -> 5* k0(50,40,5) -> 5* k0(1,39,4) -> 5* k0(39,38,40) -> 5* k0(2,3,39) -> 5* k0(1,28,1) -> 5* k0(39,27,37) -> 5* k0(5,39,41) -> 5* k0(50,50,3) -> 5* k0(28,38,50) -> 5* k0(5,28,38) -> 5* k0(3,41,3) -> 5* k0(37,2,27) -> 5* k0(26,5,28) -> 5* k0(39,41,41) -> 5* k0(5,2,26) -> 5* k0(37,38,37) -> 5* k0(3,50,41) -> 5* k0(41,27,5) -> 5* k0(3,39,38) -> 5* k0(39,4,26) -> 5* k0(27,38,26) -> 5* k0(1,1,50) -> 5* k0(26,28,4) -> 5* k0(37,41,38) -> 5* k0(41,37,3) -> 5* k0(4,2,2) -> 5* k0(5,5,27) -> 5* k0(39,38,5) -> 5* k0(2,3,4) -> 5* k0(40,2,40) -> 5* k0(5,41,37) -> 5* k0(1,50,38) -> 5* k0(5,26,28) -> 5* k0(38,4,2) -> 5* k0(27,41,27) -> 5* k0(39,27,2) -> 5* k0(39,28,28) -> 5* k0(41,40,4) -> 5* k0(4,5,3) -> 5* k0(40,5,41) -> 5* k0(28,39,41) -> 5* k0(37,38,2) -> 5* k0(38,2,37) -> 5* k0(26,41,3) -> 5* k0(28,28,38) -> 5* k0(5,38,1) -> 5* k0(1,27,27) -> 5* k0(28,2,26) -> 5* k0(41,38,39) -> 5* k0(4,3,38) -> 5* k0(26,50,41) -> 5* k0(39,40,1) -> 5* k0(2,40,50) -> 5* k0(38,5,38) -> 5* k0(26,39,38) -> 5* k0(50,38,26) -> 5* k0(40,2,5) -> 5* k0(5,41,2) -> 5* k0(38,26,39) -> 5* k0(28,5,27) -> 5* k0(41,2,50) -> 5* k0(27,2,2) -> 5* k0(28,41,37) -> 5* k0(4,27,40) -> 5* k0(28,26,28) -> 5* k0(1,40,26) -> 5* k0(50,41,27) -> 5* k0(4,1,28) -> 5* k0(27,5,3) -> 5* k0(38,3,28) -> 5* k0(2,38,40) -> 5* k0(2,27,37) -> 5* k0(40,4,1) -> 5* k0(28,38,1) -> 5* k0(27,3,38) -> 5* k0(41,28,27) -> 5* k0(37,37,28) -> 5* k0(2,41,41) -> 5* k0(38,26,4) -> 5* k0(5,37,27) -> 5* k0(28,41,2) -> 5* k0(4,27,5) -> 5* k0(39,39,27) -> 5* k0(2,4,26) -> 5* k0(50,2,2) -> 5* k0(40,28,3) -> 5* k0(5,27,50) -> 5* k0(37,1,39) -> 5* k0(27,27,40) -> 5* k0(4,37,3) -> 5* k0(5,1,38) -> 5* k0(5,40,28) -> 5* k0(2,38,5) -> 5* k0(40,37,41) -> 5* k0(3,2,40) -> 5* k0(41,41,26) -> 5* k0(27,1,28) -> 5* k0(37,50,27) -> 5* k0(1,4,2) -> 5* k0(2,27,2) -> 5* k0(40,26,38) -> 5* k0(50,5,3) -> 5* k0(38,39,3) -> 5* k0(5,50,26) -> 5* k0(37,4,40) -> 5* k0(2,28,28) -> 5* k0(4,40,4) -> 5* k0(5,4,39) -> 5* k0(3,5,41) -> 5* k0(50,3,38) -> 5* k0(38,37,38) -> 5* k0(1,2,37) -> 5* k0(40,3,27) -> 5* k0(28,37,27) -> 5* k0(40,50,40) -> 5* k0(4,38,39) -> 5* k0(37,1,4) -> 5* k0(2,40,1) -> 5* k0(40,39,37) -> 5* k0(27,27,5) -> 5* k0(38,40,39) -> 5* k0(1,5,38) -> 5* k0(5,1,3) -> 5* k0(28,27,50) -> 5* k0(3,2,5) -> 5* k0(41,1,41) -> 5* k0(50,27,40) -> 5* k0(1,26,39) -> 5* k0(28,40,28) -> 5* k0(39,3,3) -> 5* k0(27,37,3) -> 5* k0(4,2,50) -> 5* k0(28,1,38) -> 5* k0(38,50,37) -> 5* k0(37,4,5) -> 5* k0(26,2,40) -> 5* k0(50,1,28) -> 5* k0(5,4,4) -> 5* k0(38,4,50) -> 5* k0(28,50,26) -> 5* k0(41,5,2) -> 5* k0(27,40,4) -> 5* k0(28,4,39) -> 5* k0(1,3,28) -> 5* k0(26,5,41) -> 5* k0(40,50,5) -> 5* k0(37,38,50) -> 5* k0(38,27,26) -> 5* k0(3,4,1) -> 5* k0(41,3,37) -> 5* k0(40,39,2) -> 5* k0(27,38,39) -> 5* k0(4,28,27) -> 5* k0(50,27,5) -> 5* k0(1,26,4) -> 5* k0(28,1,3) -> 5* k0(38,50,2) -> 5* k0(26,2,5) -> 5* k0(5,41,50) -> 5* k0(5,26,41) -> 5* k0(2,39,27) -> 5* k0(50,37,3) -> 5* k0(27,2,50) -> 5* k0(3,28,3) -> 5* k0(41,27,39) -> 5* k0(39,28,41) -> 5* k0(28,4,4) -> 5* k0(41,1,27) -> 5* k0(3,37,41) -> 5* k0(4,41,26) -> 5* k0(1,39,3) -> 5* k0(50,40,4) -> 5* k0(3,26,38) -> 5* k0(37,39,41) -> 5* k0(37,28,38) -> 5* k0(5,39,40) -> 5* k0(41,4,28) -> 5* k0(26,4,1) -> 5* k0(5,28,37) -> 5* k0(50,38,39) -> 5* k0(1,37,38) -> 5* k0(37,2,26) -> 5* k0(27,28,27) -> 5* k0(39,41,40) -> 5* k0(3,3,27) -> 5* k0(3,50,40) -> 5* k0(40,38,28) -> 5* k0(41,27,4) -> 5* k0(28,41,50) -> 5* k0(3,39,37) -> 5* k0(28,26,41) -> 5* k0(50,2,50) -> 5* k0(1,40,39) -> 5* k0(37,5,27) -> 5* k0(26,28,3) -> 5* k0(4,1,41) -> 5* k0(5,5,26) -> 5* k0(37,41,37) -> 5* k0(37,26,28) -> 5* k0(39,38,4) -> 5* k0(2,3,3) -> 5* k0(40,2,39) -> 5* k0(1,50,37) -> 5* k0(39,27,1) -> 5* k0(38,3,41) -> 5* k0(26,37,41) -> 5* k0(27,41,26) -> 5* k0(26,26,38) -> 5* k0(1,4,50) -> 5* k0(5,39,5) -> 5* k0(5,28,2) -> 5* k0(41,40,3) -> 5* k0(4,5,2) -> 5* k0(39,41,5) -> 5* k0(40,5,40) -> 5* k0(28,39,40) -> 5* k0(37,38,1) -> 5* k0(28,28,37) -> 5* k0(3,50,5) -> 5* k0(50,28,27) -> 5* k0(1,27,26) -> 5* k0(3,39,2) -> 5* k0(41,38,38) -> 5* k0(4,3,37) -> 5* k0(26,3,27) -> 5* k0(26,50,40) -> 5* k0(37,41,2) -> 5* k0(38,5,37) -> 5* k0(26,39,37) -> 5* k0(40,2,4) -> 5* k0(5,41,1) -> 5* k0(1,50,2) -> 5* k0(41,41,39) -> 5* k0(27,1,41) -> 5* k0(28,5,26) -> 5* k0(5,50,39) -> 5* k0(4,27,39) -> 5* k0(50,41,26) -> 5* k0(2,28,41) -> 5* k0(40,5,5) -> 5* k0(28,39,5) -> 5* k0(4,1,27) -> 5* k0(38,2,1) -> 5* k0(41,5,50) -> 5* k0(27,5,2) -> 5* k0(28,28,2) -> 5* k0(39,26,27) -> 5* k0(26,50,5) -> 5* k0(4,4,28) -> 5* k0(40,39,50) -> 5* k0(26,39,2) -> 5* k0(27,3,37) -> 5* k0(41,28,26) -> 5* k0(37,37,27) -> 5* k0(2,41,40) -> 5* k0(38,26,3) -> 5* k0(5,37,26) -> 5* k0(3,38,28) -> 5* k0(28,41,1) -> 5* k0(4,27,4) -> 5* k0(37,27,50) -> 5* k0(38,50,50) -> 5* k0(50,1,41) -> 5* k0(39,39,26) -> 5* k0(37,1,38) -> 5* k0(37,40,28) -> 5* k0(28,50,39) -> 5* k0(27,27,39) -> 5* k0(5,40,27) -> 5* k0(2,38,4) -> 5* k0(40,37,40) -> 5* k0(3,2,39) -> 5* k0(27,1,27) -> 5* k0(37,50,26) -> 5* k0(2,27,1) -> 5* k0(40,26,37) -> 5* k0(50,5,2) -> 5* k0(1,3,41) -> 5* k0(37,4,39) -> 5* k0(4,40,3) -> 5* k0(27,4,28) -> 5* k0(2,41,5) -> 5* k0(40,40,41) -> 5* k0(3,5,40) -> 5* k0(50,3,37) -> 5* k0(38,37,37) -> 5* k0(4,38,38) -> 5* k0(40,3,26) -> 5* k0(28,37,26) -> 5* k0(26,38,28) -> 5* k0(37,1,3) -> 5* k0(27,27,4) -> 5* k0(1,5,37) -> 5* k0(5,1,2) -> 5* k0(38,40,38) -> 5* k0(40,37,5) -> 5* k0(3,2,4) -> 5* k0(41,1,40) -> 5* k0(50,27,39) -> 5* k0(4,41,39) -> 5* k0(28,40,27) -> 5* k0(40,26,2) -> 5* k0(41,37,50) -> 5* k0(39,3,2) -> 5* k0(26,2,39) -> 5* k0(50,1,27) -> 5* k0(37,4,4) -> 5* k0(41,50,28) -> 5* k0(40,27,28) -> 5* k0(5,4,3) -> 5* k0(3,5,5) -> 5* k0(41,4,41) -> 5* k0(38,37,2) -> 5* k0(1,2,1) -> 5* k0(39,1,37) -> 5* k0(27,40,3) -> 5* k0(4,5,50) -> 5* k0(2,26,27) -> 5* k0(26,5,40) -> 5* k0(50,4,28) -> 5* k0(40,50,4) -> 5* k0(5,2,38) -> 5* k0(40,39,1) -> 5* k0(3,39,50) -> 5* k0(39,4,38) -> 5* k0(27,38,38) -> 5* k0(4,28,26) -> 5* k0(41,1,5) -> 5* k0(50,27,4) -> 5* k0(1,26,3) -> 5* k0(37,41,50) -> 5* k0(28,1,2) -> 5* k0(37,26,41) -> 5* k0(38,50,1) -> 5* k0(26,2,4) -> 5* k0(1,50,50) -> 5* k0(5,26,40) -> 5* k0(27,41,39) -> 5* k0(2,39,26) -> 5* k0(39,28,40) -> 5* k0(28,4,3) -> 5* k0(26,5,5) -> 5* k0(3,37,40) -> 5* k0(39,2,28) -> 5* k0(50,40,3) -> 5* k0(3,26,37) -> 5* k0(27,5,50) -> 5* k0(41,3,1) -> 5* k0(37,39,40) -> 5* k0(28,2,38) -> 5* k0(37,28,37) -> 5* k0(3,40,41) -> 5* k0(26,39,50) -> 5* k0(50,38,38) -> 5* k0(1,37,37) -> 5* k0(27,28,26) -> 5* k0(5,26,5) -> 5* k0(40,38,27) -> 5* k0(3,3,26) -> 5* k0(41,27,3) -> 5* k0(39,28,5) -> 5* k0(28,26,40) -> 5* k0(1,40,38) -> 5* k0(37,5,26) -> 5* k0(50,41,39) -> 5* k0(40,28,50) -> 5* k0(3,37,5) -> 5* k0(4,1,40) -> 5* k0(4,37,50) -> 5* k0(2,3,2) -> 5* k0(40,41,28) -> 5* k0(3,26,2) -> 5* k0(39,38,3) -> 5* k0(38,3,40) -> 5* k0(26,37,40) -> 5* k0(37,39,5) -> 5* k0(4,50,28) -> 5* k0(3,27,28) -> 5* k0(37,28,2) -> 5* k0(5,39,4) -> 5* k0(26,26,37) -> 5* k0(50,5,50) -> 5* k0(4,4,41) -> 5* k0(5,28,1) -> 5* k0(1,37,2) -> 5* k0(2,1,37) -> 5* k0(40,5,39) -> 5* k0(39,41,4) -> 5* k0(26,40,41) -> 5* k0(3,50,4) -> 5* k0(41,2,27) -> 5* k0(50,28,26) -> 5* k0(3,39,1) -> 5* k0(41,38,37) -> 5* k0(28,26,5) -> 5* k0(39,39,39) -> 5* k0(2,4,38) -> 5* k0(26,3,26) -> 5* k0(37,41,1) -> 5* k0(4,1,5) -> 5* k0(40,2,3) -> 5* k0(5,1,50) -> 5* k0(1,50,1) -> 5* k0(38,3,5) -> 5* k0(26,37,5) -> 5* k0(41,41,38) -> 5* k0(27,1,40) -> 5* k0(37,50,39) -> 5* k0(39,3,50) -> 5* k0(27,37,50) -> 5* k0(26,26,2) -> 5* k0(5,50,38) -> 5* k0(26,27,28) -> 5* k0(27,50,28) -> 5* k0(2,28,40) -> 5* k0(40,5,4) -> 5* k0(28,39,4) -> 5* k0(2,2,28) -> 5* k0(28,28,1) -> 5* k0(27,4,41) -> 5* k0(39,26,26) -> 5* k0(4,3,1) -> 5* k0(41,38,2) -> 5* k0(26,50,4) -> 5* k0(5,27,27) -> 5* k0(38,5,1) -> 5* k0(26,39,1) -> 5* k0(37,37,26) -> 5* k0(27,1,5) -> 5* k0(3,38,27) -> 5* k0(28,1,50) -> 5* k0(4,27,3) -> 5* k0(50,1,40) -> 5* k0(2,28,5) -> 5* k0(40,27,41) -> 5* k0(37,40,27) -> 5* k0(50,37,50) -> 5* k0(3,28,50) -> 5* k0(28,50,38) -> 5* k0(5,40,26) -> 5* k0(50,50,28) -> 5* k0(2,38,3) -> 5* k0(40,37,39) -> 5* k0(3,41,28) -> 5* k0(1,3,40) -> 5* k0(50,4,41) -> 5* k0(38,38,41) -> 5* k0(38,27,38) -> 5* k0(27,3,1) -> 5* k0(38,1,26) -> 5* k0(28,27,27) -> 5* k0(2,41,4) -> 5* k0(40,40,40) -> 5* k0(3,5,39) -> 5* k0(4,2,27) -> 5* k0(41,37,28) -> 5* k0(50,1,5) -> 5* k0(4,38,37) -> 5* k0(37,1,2) -> 5* k0(2,39,39) -> 5* k0(38,4,27) -> 5* k0(26,38,27) -> 5* k0(27,27,3) -> 5* k0(38,40,37) -> 5* k0(40,37,4) -> 5* k0(3,2,3) -> 5* k0(41,1,39) -> 5* k0(26,28,50) -> 5* k0(1,3,5) -> 5* k0(39,2,41) -> 5* k0(4,41,38) -> 5* k0(28,40,26) -> 5* k0(40,26,1) -> 5* k0(37,4,3) -> 5* k0(2,3,50) -> 5* k0(26,41,28) -> 5* k0(41,50,27) -> 5* k0(5,4,2) -> 5* k0(40,40,5) -> 5* k0(3,5,4) -> 5* k0(41,4,40) -> 5* k0(50,3,1) -> 5* k0(38,37,1) -> 5* k0(37,2,38) -> 5* k0(2,26,26) -> 5* k0(26,5,39) -> 5* k0(4,38,2) -> 5* k0(40,50,3) -> 5* k0(5,2,37) -> 5* k0(27,2,27) -> 5* k0(38,40,2) -> 5* k0(1,5,1) -> 5* k0(39,4,37) -> 5* k0(27,38,37) -> 5* k0(41,1,4) -> 5* k0(50,27,3) -> 5* k0(5,5,38) -> 5* k0(37,26,40) -> 5* k0(26,2,3) -> 5* k0(5,26,39) -> 5* k0(27,41,38) -> 5* k0(3,27,41) -> 5* k0(41,4,5) -> 5* k0(39,1,1) -> 5* k0(39,28,39) -> 5* k0(28,4,2) -> 5* k0(3,37,39) -> 5* k0(26,5,4) -> 5* k0(1,38,41) -> 5* k0(1,27,38) -> 5* k0(5,3,28) -> 5* k0(41,38,50) -> 5* k0(27,38,2) -> 5* k0(28,2,37) -> 5* k0(50,2,27) -> 5* k0(1,1,26) -> 5* k0(3,40,40) -> 5* k0(39,5,28) -> 5* k0(50,38,37) -> 5* k0(37,26,5) -> 5* k0(4,37,28) -> 5* k0(38,26,50) -> 5* k0(5,26,4) -> 5* k0(28,5,38) -> 5* k0(40,38,26) -> 5* k0(38,39,28) -> 5* k0(1,4,27) -> 5* k0(39,28,4) -> 5* k0(28,26,39) -> 5* k0(50,41,38) -> 5* k0(1,40,37) -> 5* k0(26,27,41) -> 5* k0(3,37,4) -> 5* k0(4,1,39) -> 5* k0(3,26,1) -> 5* k0(2,2,41) -> 5* k0(40,41,27) -> 5* k0(37,39,4) -> 5* k0(38,3,39) -> 5* k0(26,37,39) -> 5* k0(4,50,27) -> 5* k0(37,28,1) -> 5* k0(5,39,3) -> 5* k0(28,3,28) -> 5* k0(3,40,5) -> 5* k0(41,39,41) -> 5* k0(4,4,40) -> 5* k0(50,38,2) -> 5* k0(1,37,1) -> 5* k0(41,28,38) -> 5* k0(39,41,3) -> 5* k0(26,40,40) -> 5* k0(5,37,38) -> 5* k0(41,2,26) -> 5* k0(3,50,3) -> 5* k0(27,37,28) -> 5* k0(39,50,41) -> 5* k0(28,26,4) -> 5* k0(2,4,37) -> 5* k0(1,40,2) -> 5* k0(39,39,38) -> 5* k0(4,1,4) -> 5* k0(37,1,50) -> 5* k0(5,40,39) -> 5* k0(41,5,27) -> 5* k0(40,2,2) -> 5* k0(41,41,37) -> 5* k0(27,1,39) -> 5* k0(38,3,4) -> 5* k0(26,37,4) -> 5* k0(37,50,38) -> 5* k0(41,26,28) -> 5* k0(26,26,1) -> 5* k0(5,50,37) -> 5* k0(4,4,5) -> 5* k0(27,50,27) -> 5* k0(2,1,1) -> 5* k0(2,28,39) -> 5* k0(5,4,50) -> 5* k0(40,5,3) -> 5* k0(28,39,3) -> 5* k0(27,4,40) -> 5* k0(26,40,5) -> 5* k0(41,38,1) -> 5* k0(37,27,27) -> 5* k0(4,38,50) -> 5* k0(40,3,38) -> 5* k0(28,37,38) -> 5* k0(26,50,3) -> 5* k0(5,27,26) -> 5* k0(50,37,28) -> 5* k0(2,5,28) -> 5* k0(38,40,50) -> 5* k0(41,41,2) -> 5* k0(27,1,4) -> 5* k0(1,26,50) -> 5* k0(28,40,39) -> 5* k0(3,38,26) -> 5* k0(5,50,2) -> 5* k0(50,1,39) -> 5* k0(1,39,28) -> 5* k0(2,28,4) -> 5* k0(40,27,40) -> 5* k0(37,40,26) -> 5* k0(28,50,37) -> 5* k0(27,4,5) -> 5* k0(40,1,28) -> 5* k0(50,50,27) -> 5* k0(28,4,50) -> 5* k0(3,41,27) -> 5* k0(50,4,40) -> 5* k0(38,38,40) -> 5* k0(1,3,39) -> 5* k0(38,27,37) -> 5* k0(4,39,41) -> 5* k0(27,38,50) -> 5* k0(4,28,38) -> 5* k0(28,27,26) -> 5* k0(2,41,3) -> 5* k0(38,41,41) -> 5* k0(41,37,27) -> 5* k0(4,2,26) -> 5* k0(2,50,41) -> 5* k0(50,1,4) -> 5* k0(40,27,5) -> 5* k0(38,4,26) -> 5* k0(26,38,26) -> 5* k0(2,39,38) -> 5* k0(28,50,2) -> 5* k0(41,27,50) -> 5* k0(3,2,2) -> 5* k0(41,1,38) -> 5* k0(41,40,28) -> 5* k0(4,5,27) -> 5* k0(40,37,3) -> 5* k0(4,41,37) -> 5* k0(50,4,5) -> 5* k0(38,38,5) -> 5* k0(1,3,4) -> 5* k0(39,2,40) -> 5* k0(4,26,28) -> 5* k0(26,41,27) -> 5* k0(38,27,2) -> 5* k0(37,4,2) -> 5* k0(41,50,26) -> 5* k0(5,3,41) -> 5* k0(38,28,28) -> 5* k0(3,5,3) -> 5* k0(41,4,39) -> 5* k0(40,40,4) -> 5* k0(39,5,41) -> 5* k0(27,39,41) -> 5* k0(37,2,37) -> 5* k0(50,38,50) -> 5* k0(27,28,38) -> 5* k0(4,38,1) -> 5* k0(40,38,39) -> 5* k0(3,3,38) -> 5* k0(27,2,26) -> 5* k0(38,40,1) -> 5* k0(1,40,50) -> 5* k0(37,5,38) -> 5* k0(41,1,3) -> 5* k0(39,2,5) -> 5* k0(4,41,2) -> 5* k0(5,5,37) -> 5* k0(37,26,39) -> 5* k0(40,2,50) -> 5* k0(26,2,2) -> 5* k0(27,5,27) -> 5* k0(27,41,37) -> 5* k0(3,27,40) -> 5* k0(27,26,28) -> 5* k0(41,4,4) -> 5* k0(28,3,41) -> 5* k0(3,1,28) -> 5* k0(26,5,3) -> 5* k0(5,2,1) -> 5* k0(50,39,41) -> 5* k0(1,38,40) -> 5* k0(37,3,28) -> 5* k0(1,27,37) -> 5* k0(50,28,38) -> 5* k0(39,4,1) -> 5* k0(27,38,1) -> 5* k0(26,3,38) -> 5* k0(50,2,26) -> 5* k0(40,28,27) -> 5* k0(1,41,41) -> 5* k0(37,26,4) -> 5* k0(4,37,27) -> 5* k0(5,26,3) -> 5* k0(41,41,50) -> 5* k0(27,41,2) -> 5* k0(28,5,37) -> 5* k0(3,27,5) -> 5* k0(41,26,41) -> 5* k0(50,5,27) -> 5* k0(38,39,27) -> 5* k0(1,4,26) -> 5* k0(4,27,50) -> 5* k0(5,50,50) -> 5* k0(39,28,3) -> 5* k0(50,41,37) -> 5* k0(26,27,40) -> 5* k0(50,26,28) -> 5* k0(4,1,38) -> 5* k0(4,40,28) -> 5* k0(3,37,3) -> 5* k0(2,2,40) -> 5* k0(40,41,26) -> 5* k0(26,1,28) -> 5* k0(1,38,5) -> 5* k0(39,37,41) -> 5* k0(1,27,2) -> 5* k0(39,26,38) -> 5* k0(37,39,3) -> 5* k0(4,50,26) -> 5* k0(28,2,1) -> 5* k0(1,28,28) -> 5* k0(3,40,4) -> 5* k0(41,39,40) -> 5* k0(4,4,39) -> 5* k0(50,38,1) -> 5* k0(2,5,41) -> 5* k0(41,28,37) -> 5* k0(37,37,38) -> 5* k0(5,37,37) -> 5* k0(3,38,39) -> 5* k0(39,3,27) -> 5* k0(27,37,27) -> 5* k0(39,50,40) -> 5* k0(28,26,3) -> 5* k0(1,40,1) -> 5* k0(39,39,37) -> 5* k0(50,41,2) -> 5* k0(26,27,5) -> 5* k0(37,40,39) -> 5* k0(4,1,3) -> 5* k0(27,27,50) -> 5* k0(28,50,50) -> 5* k0(2,2,5) -> 5* k0(40,1,41) -> 5* k0(5,40,38) -> 5* k0(41,5,26) -> 5* k0(38,3,3) -> 5* k0(26,37,3) -> 5* k0(3,2,50) -> 5* k0(27,1,38) -> 5* k0(27,40,28) -> 5* k0(37,50,37) -> 5* k0(41,39,5) -> 5* k0(4,4,4) -> 5* k0(37,4,50) -> 5* k0(27,50,26) -> 5* k0(40,5,2) -> 5* k0(41,28,2) -> 5* k0(26,40,4) -> 5* k0(27,4,39) -> 5* k0(5,37,2) -> 5* k0(39,50,5) -> 5* k0(37,27,26) -> 5* k0(39,39,2) -> 5* k0(2,4,1) -> 5* k0(40,3,37) -> 5* k0(28,37,37) -> 5* k0(26,38,39) -> 5* k0(50,37,27) -> 5* k0(3,28,27) -> 5* k0(41,41,1) -> 5* k0(27,1,3) -> 5* k0(37,50,2) -> 5* k0(50,27,50) -> 5* k0(4,41,50) -> 5* k0(28,40,38) -> 5* k0(4,26,41) -> 5* k0(5,50,1) -> 5* k0(1,39,27) -> 5* k0(26,2,50) -> 5* k0(50,1,38) -> 5* k0(50,40,28) -> 5* k0(2,28,3) -> 5* k0(40,27,39) -> 5* k0(41,50,39) -> 5* k0(38,28,41) -> 5* k0(40,1,27) -> 5* k0(27,4,4) -> 5* k0(50,50,26) -> 5* k0(2,37,41) -> 5* k0(3,41,26) -> 5* k0(2,26,38) -> 5* k0(50,4,39) -> 5* k0(28,37,2) -> 5* k0(4,39,40) -> 5* k0(40,4,28) -> 5* k0(4,28,37) -> 5* k0(26,28,27) -> 5* k0(38,41,40) -> 5* k0(41,37,26) -> 5* k0(39,38,28) -> 5* k0(2,3,27) -> 5* k0(2,50,40) -> 5* k0(50,1,3) -> 5* k0(40,27,4) -> 5* k0(27,41,50) -> 5* k0(2,39,37) -> 5* k0(27,26,41) -> 5* k0(28,50,1) -> 5* k0(3,1,41) -> 5* k0(41,40,27) -> 5* k0(4,5,26) -> 5* k0(50,4,4) -> 5* k0(38,38,4) -> 5* k0(1,3,3) -> 5* k0(39,2,39) -> 5* k0(37,3,41) -> 5* k0(26,41,26) -> 5* k0(38,27,1) -> 5* k0(4,39,5) -> 5* k0(5,3,40) -> 5* k0(4,28,2) -> 5* k0(40,40,3) -> 5* k0(3,5,2) -> 5* k0(38,41,5) -> 5* k0(39,5,40) -> 5* k0(27,39,40) -> 5* k0(27,28,37) -> 5* k0(2,50,5) -> 5* k0(2,39,2) -> 5* k0(40,38,38) -> 5* k0(3,3,37) -> 5* k0(50,41,50) -> 5* k0(37,5,37) -> 5* k0(41,1,2) -> 5* k0(50,26,41) -> 5* k0(39,2,4) -> 5* k0(4,41,1) -> 5* k0(27,5,26) -> 5* k0(40,41,39) -> 5* k0(26,1,41) -> 5* k0(5,3,5) -> 5* k0(3,27,39) -> 5* k0(4,50,39) -> 5* k0(41,4,3) -> 5* k0(1,28,41) -> 5* k0(28,3,40) -> 5* k0(3,1,27) -> 5* k0(39,5,5) -> 5* k0(27,39,5) -> 5* k0(37,2,1) -> 5* k0(27,28,2) -> 5* k0(40,5,50) -> 5* k0(26,5,2) -> 5* k0(38,26,27) -> 5* k0(50,39,40) -> 5* k0(41,2,38) -> 5* k0(50,28,37) -> 5* k0(3,4,28) -> 5* k0(26,3,37) -> 5* k0(39,39,50) -> 5* k0(40,28,26) -> 5* k0(5,5,1) -> 5* k0(1,41,40) -> 5* k0(37,26,3) -> 5* k0(4,37,26) -> 5* k0(27,41,1) -> 5* k0(2,38,28) -> 5* k0(37,50,50) -> 5* k0(3,27,4) -> 5* k0(41,26,40) -> 5* k0(50,5,26) -> 5* k0(38,39,26) -> 5* k0(28,3,5) -> 5* k0(27,50,39) -> 5* k0(26,27,39) -> 5* k0(4,40,27) -> 5* k0(50,39,5) -> 5* k0(1,38,4) -> 5* k0(39,37,40) -> 5* k0(2,2,39) -> 5* k0(26,1,27) -> 5* k0(50,28,2) -> 5* k0(1,27,1) -> 5* k0(39,26,37) -> 5* k0(5,38,41) -> 5* k0(5,27,38) -> 5* k0(3,40,3) -> 5* k0(1,41,5) -> 5* k0(39,40,41) -> 5* k0(2,5,40) -> 5* k0(26,4,28) -> 5* k0(5,1,26) -> 5* k0(37,37,37) -> 5* k0(28,5,1) -> 5* k0(41,26,5) -> 5* k0(27,37,26) -> 5* k0(3,38,38) -> 5* k0(39,3,26) -> 5* k0(50,41,1) -> 5* k0(26,27,4) -> 5* k0(5,4,27) -> 5* k0(37,40,38) -> 5* k0(4,1,2) -> 5* k0(5,40,37) -> 5* k0(39,37,5) -> 5* k0(2,2,4) -> 5* k0(40,1,40) -> 5* k0(50,50,39) -> 5* k0(3,41,39) -> 5* k0(27,40,27) -> 5* k0(39,26,2) -> 5* k0(40,37,50) -> 5* k0(38,3,2) -> 5* k0(39,27,28) -> 5* k0(40,50,28) -> 5* k0(4,4,3) -> 5* k0(41,39,4) -> 5* k0(41,28,1) -> 5* k0(2,5,5) -> 5* k0(40,4,41) -> 5* k0(28,38,41) -> 5* k0(37,37,2) -> 5* k0(38,1,37) -> 5* k0(28,27,38) -> 5* k0(26,40,3) -> 5* k0(3,5,50) -> 5* k0(5,37,1) -> 5* k0(1,26,27) -> 5* k0(39,50,4) -> 5* k0(4,2,38) -> 5* k0(28,1,26) -> 5* k0(39,39,1) -> 5* k0(2,39,50) -> 5* k0(38,4,38) -> 5* k0(26,38,38) -> 5* k0(50,37,26) -> 5* k0(3,28,26) -> 5* k0(40,1,5) -> 5* k0(5,40,2) -> 5* k0(41,1,50) -> 5* k0(27,1,2) -> 5* k0(28,4,27) -> 5* k0(37,50,1) -> 5* k0(28,40,37) -> 5* k0(4,26,40) -> 5* k0(26,41,39) -> 5* k0(50,40,27) -> 5* k0(1,39,26) -> 5* k0(41,50,38) -> 5* k0(38,28,40) -> 5* k0(27,4,3) -> 5* k0(2,37,40) -> 5* k0(38,2,28) -> 5* k0(2,26,37) -> 5* k0(26,5,50) -> 5* k0(40,3,1) -> 5* k0(28,37,1) -> 5* k0(27,2,38) -> 5* k0(41,27,27) -> 5* k0(2,40,41) -> 5* k0(26,28,26) -> 5* k0(28,40,2) -> 5* k0(4,26,5) -> 5* k0(2,3,26) -> 5* k0(50,1,2) -> 5* k0(39,38,27) -> 5* k0(40,27,3) -> 5* k0(5,26,50) -> 5* k0(27,26,40) -> 5* k0(38,28,5) -> 5* k0(5,39,28) -> 5* k0(39,28,50) -> 5* k0(3,1,40) -> 5* k0(41,40,26) -> 5* k0(2,37,5) -> 5* k0(39,41,28) -> 5* k0(2,26,2) -> 5* k0(50,4,3) -> 5* k0(38,38,3) -> 5* k0(3,37,50) -> 5* k0(1,3,2) -> 5* k0(37,3,40) -> 5* k0(3,50,28) -> 5* k0(2,27,28) -> 5* k0(5,3,39) -> 5* k0(4,39,4) -> 5* k0(3,4,41) -> 5* k0(4,28,1) -> 5* k0(1,1,37) -> 5* k0(50,2,38) -> 5* k0(38,41,4) -> 5* k0(39,5,39) -> 5* k0(40,2,27) -> 5* k0(2,50,4) -> 5* k0(2,39,1) -> 5* k0(40,38,37) -> 5* k0(27,26,5) -> 5* k0(38,39,39) -> 5* k0(1,4,38) -> 5* k0(28,26,50) -> 5* k0(3,1,5) -> 5* k0(50,26,40) -> 5* k0(39,2,3) -> 5* k0(4,1,50) -> 5* k0(28,39,28) -> 5* k0(37,3,5) -> 5* k0(40,41,38) -> 5* k0(26,1,40) -> 5* k0(5,3,4) -> 5* k0(38,3,50) -> 5* k0(26,37,50) -> 5* k0(4,50,38) -> 5* k0(41,4,2) -> 5* k0(26,50,28) -> 5* k0(1,28,40) -> 5* k0(39,5,4) -> 5* k0(27,39,4) -> 5* k0(28,3,39) -> 5* k0(26,4,41) -> 5* k0(1,2,28) -> 5* k0(27,28,1) -> 5* k0(38,26,26) -> 5* k0(40,38,2) -> 5* k0(3,3,1) -> 5* k0(41,2,37) -> 5* k0(4,27,27) -> 5* k0(37,5,1) -> 5* k0(50,26,5) -> 5* k0(26,1,5) -> 5* k0(5,40,50) -> 5* k0(41,5,38) -> 5* k0(2,38,27) -> 5* k0(27,1,50) -> 5* k0(3,27,3) -> 5* k0(41,26,39) -> 5* k0(1,28,5) -> 5* k0(39,27,41) -> 5* k0(28,3,4) -> 5* k0(27,50,38) -> 5* k0(2,28,50) -> 5* k0(4,40,26) -> 5* k0(2,41,28) -> 5* k0(50,39,4) -> 5* k0(1,38,3) -> 5* k0(39,37,39) -> 5* k0(37,38,41) -> 5* k0(50,28,1) -> 5* k0(37,27,38) -> 5* k0(5,38,40) -> 5* k0(41,3,28) -> 5* k0(26,3,1) -> 5* k0(5,27,37) -> 5* k0(37,1,26) -> 5* k0(50,37,39) -> 5* k0(27,27,27) -> 5* k0(1,41,4) -> 5* k0(39,40,40) -> 5* k0(2,5,39) -> 5* k0(40,37,28) -> 5* k0(3,2,27) -> 5* k0(5,41,41) -> 5* k0(41,26,4) -> 5* k0(3,38,37) -> 5* k0(28,40,50) -> 5* k0(1,39,39) -> 5* k0(37,4,27) -> 5* k0(50,1,50) -> 5* k0(26,27,3) -> 5* k0(5,4,26) -> 5* k0(37,40,37) -> 5* k0(39,37,4) -> 5* k0(2,2,3) -> 5* k0(40,1,39) -> 5* k0(50,50,38) -> 5* k0(38,2,41) -> 5* k0(3,41,38) -> 5* k0(27,40,26) -> 5* k0(39,26,1) -> 5* k0(5,38,5) -> 5* k0(1,3,50) -> 5* k0(40,50,27) -> 5* k0(5,27,2) -> 5* k0(41,39,3) -> 5* k0(4,4,2) -> 5* k0(39,40,5) -> 5* k0(2,5,4) -> 5* k0(40,4,40) -> 5* k0(28,38,40) -> 5* k0(5,28,28) -> 5* k0(37,37,1) -> 5* k0(28,27,37) -> 5* k0(1,26,26) -> 5* k0(50,27,27) -> 5* k0(3,38,2) -> 5* k0(41,37,38) -> 5* k0(39,50,3) -> 5* k0(4,2,37) -> 5* k0(26,2,27) -> 5* k0(28,41,41) -> 5* k0(37,40,2) -> 5* k0(38,4,37) -> 5* k0(26,38,37) -> 5* k0(40,1,4) -> 5* k0(5,40,1) -> 5* k0(28,4,26) -> 5* k0(41,40,39) -> 5* k0(4,5,38) -> 5* k0(4,26,39) -> 5* k0(26,41,38) -> 5* k0(50,40,26) -> 5* k0(2,27,41) -> 5* k0(41,50,37) -> 5* k0(40,4,5) -> 5* k0(28,38,5) -> 5* k0(38,1,1) -> 5* k0(38,28,39) -> 5* k0(28,27,2) -> 5* k0(41,4,50) -> 5* k0(27,4,2) -> 5* k0(2,37,39) -> 5* k0(28,28,28) -> 5* k0(4,3,28) -> 5* k0(27,2,37) -> 5* k0(40,38,50) -> 5* k0(26,38,2) -> 5* k0(41,27,26) -> 5* k0(38,5,28) -> 5* k0(2,40,40) -> 5* k0(28,40,1) -> 5* k0(3,37,28) -> 5* k0(4,26,4) -> 5* k0(37,26,50) -> 5* k0(27,5,38) -> 5* k0(39,38,26) -> 5* k0(41,50,2) -> 5* k0(37,39,28) -> 5* k0(38,28,4) -> 5* k0(27,26,39) -> 5* k0(5,39,27) -> 5* k0(2,37,4) -> 5* k0(3,1,39) -> 5* k0(1,2,41) -> 5* k0(39,41,27) -> 5* k0(2,26,1) -> 5* k0(50,4,2) -> 5* k0(37,3,39) -> 5* k0(3,50,27) -> 5* k0(4,39,3) -> 5* k0(2,40,5) -> 5* k0(40,39,41) -> 5* k0(3,4,40) -> 5* k0(27,3,28) -> 5* k0(50,2,37) -> 5* k0(40,28,38) -> 5* k0(38,41,3) -> 5* k0(4,37,38) -> 5* k0(40,2,26) -> 5* k0(2,50,3) -> 5* k0(26,37,28) -> 5* k0(38,50,41) -> 5* k0(27,26,4) -> 5* k0(50,5,38) -> 5* k0(38,39,38) -> 5* k0(1,4,37) -> 5* k0(3,1,4) -> 5* k0(50,26,39) -> 5* k0(40,5,27) -> 5* k0(28,39,27) -> 5* k0(39,2,2) -> 5* k0(4,40,39) -> 5* k0(37,3,4) -> 5* k0(40,41,37) -> 5* k0(26,1,39) -> 5* k0(40,26,28) -> 5* k0(5,3,3) -> 5* k0(4,50,37) -> 5* k0(3,4,5) -> 5* k0(41,3,41) -> 5* k0(26,50,27) -> 5* k0(1,1,1) -> 5* k0(1,28,39) -> 5* k0(39,5,3) -> 5* k0(27,39,3) -> 5* k0(4,4,50) -> 5* k0(26,4,40) -> 5* k0(50,3,28) -> 5* k0(40,38,1) -> 5* k0(39,3,38) -> 5* k0(27,37,38) -> 5* k0(3,38,50) -> 5* k0(4,27,26) -> 5* k0(1,5,28) -> 5* k0(50,26,4) -> 5* k0(37,40,50) -> 5* k0(41,5,37) -> 5* k0(40,41,2) -> 5* k0(26,1,4) -> 5* k0(27,40,39) -> 5* k0(2,38,26) -> 5* k0(4,50,2) -> 5* k0(1,28,4) -> 5* k0(39,27,40) -> 5* k0(28,3,3) -> 5* k0(27,50,37) -> 5* k0(26,4,5) -> 5* k0(39,1,28) -> 5* k0(5,28,41) -> 5* k0(2,41,27) -> 5* k0(50,39,3) -> 5* k0(27,4,50) -> 5* k0(41,2,1) -> 5* k0(37,38,40) -> 5* k0(37,27,37) -> 5* k0(3,39,41) -> 5* k0(26,38,50) -> 5* k0(50,37,38) -> 5* k0(27,27,26) -> 5* k0(1,41,3) -> 5* k0(3,28,38) -> 5* k0(37,41,41) -> 5* k0(3,2,26) -> 5* k0(40,37,27) -> 5* k0(5,41,40) -> 5* k0(41,26,3) -> 5* k0(1,50,41) -> 5* k0(39,27,5) -> 5* k0(50,40,39) -> 5* k0(1,39,38) -> 5* k0(37,4,26) -> 5* k0(41,50,50) -> 5* k0(27,50,2) -> 5* k0(40,27,50) -> 5* k0(3,5,27) -> 5* k0(39,37,3) -> 5* k0(2,2,2) -> 5* k0(40,1,38) -> 5* k0(40,40,28) -> 5* k0(50,50,37) -> 5* k0(37,38,5) -> 5* k0(38,2,40) -> 5* k0(3,41,37) -> 5* k0(28,28,41) -> 5* k0(3,26,28) -> 5* k0(50,4,50) -> 5* k0(37,27,2) -> 5* k0(5,38,4) -> 5* k0(40,50,26) -> 5* k0(4,3,41) -> 5* k0(5,27,1) -> 5* k0(37,28,28) -> 5* k0(39,40,4) -> 5* k0(2,5,3) -> 5* k0(40,4,39) -> 5* k0(38,5,41) -> 5* k0(26,39,41) -> 5* k0(26,28,38) -> 5* k0(50,27,26) -> 5* k0(5,41,5) -> 5* k0(3,38,1) -> 5* k0(41,37,37) -> 5* k0(2,3,38) -> 5* k0(26,2,26) -> 5* k0(39,38,39) -> 5* k0(28,41,40) -> 5* k0(37,40,1) -> 5* k0(40,1,3) -> 5* k0(50,50,2) -> 5* k0(3,41,2) -> 5* k0(41,40,38) -> 5* k0(4,5,37) -> 5* k0(38,2,5) -> 5* k0(26,5,27) -> 5* k0(39,2,50) -> 5* k0(26,41,37) -> 5* k0(2,27,40) -> 5* k0(26,26,28) -> 5* k0(40,4,4) -> 5* k0(28,38,4) -> 5* k0(27,3,41) -> 5* k0(2,1,28) -> 5* k0(28,27,1) -> 5* k0(41,37,2) -> 5* k0(4,2,1) -> 5* k0(28,41,5) -> 5* k0(5,26,27) -> 5* k0(38,4,1) -> 5* k0(26,38,1) -> 5* k0(39,28,27) -> 5* k0(3,37,27) -> 5* k0(4,26,3) -> 5* k0(40,41,50) -> 5* k0(26,41,2) -> 5* k0(27,5,37) -> 5* k0(41,50,1) -> 5* k0(2,27,5) -> 5* k0(40,26,41) -> 5* k0(37,39,27) -> 5* k0(4,50,50) -> 5* k0(38,28,3) -> 5* k0(3,27,50) -> 5* k0(5,39,26) -> 5* k0(3,40,28) -> 5* k0(2,37,3) -> 5* k0(3,1,38) -> 5* k0(50,3,41) -> 5* k0(38,37,41) -> 5* k0(1,2,40) -> 5* k0(39,41,26) -> 5* k0(38,26,38) -> 5* k0(3,50,26) -> 5* k0(27,2,1) -> 5* k0(28,26,27) -> 5* k0(2,40,4) -> 5* k0(40,39,40) -> 5* k0(3,4,39) -> 5* k0(40,28,37) -> 5* k0(1,5,41) -> 5* k0(4,37,37) -> 5* k0(2,38,39) -> 5* k0(38,3,27) -> 5* k0(26,37,27) -> 5* k0(38,50,40) -> 5* k0(27,26,3) -> 5* k0(50,5,37) -> 5* k0(38,39,37) -> 5* k0(3,1,3) -> 5* k0(27,50,50) -> 5* k0(26,27,50) -> 5* k0(1,2,5) -> 5* k0(39,1,41) -> 5* k0(4,40,38) -> 5* k0(40,5,26) -> 5* k0(28,39,26) -> 5* k0(26,40,28) -> 5* k0(37,3,3) -> 5* k0(2,2,50) -> 5* k0(26,1,38) -> 5* k0(5,3,2) -> 5* k0(40,39,5) -> 5* k0(3,4,4) -> 5* k0(41,3,40) -> 5* k0(26,50,26) -> 5* k0(50,2,1) -> 5* k0(40,28,2) -> 5* k0(39,5,2) -> 5* k0(26,4,39) -> 5* k0(4,37,2) -> 5* k0(5,1,37) -> 5* k0(38,50,5) -> 5* k0(38,39,2) -> 5* k0(1,4,1) -> 5* k0(39,3,37) -> 5* k0(27,37,37) -> 5* k0(2,28,27) -> 5* k0(50,26,3) -> 5* k0(5,4,38) -> 5* k0(40,41,1) -> 5* k0(26,1,3) -> 5* k0(50,50,50) -> 5* k0(3,41,50) -> 5* k0(27,40,38) -> 5* k0(3,26,41) -> 5* k0(4,50,1) -> 5* k0(41,3,5) -> 5* k0(40,50,39) -> 5* k0(1,28,3) -> 5* k0(39,27,39) -> 5* k0(28,3,2) -> 5* k0(37,28,41) -> 5* k0(26,4,4) -> 5* k0(39,1,27) -> 5* k0(5,28,40) -> 5* k0(1,37,41) -> 5* k0(2,41,26) -> 5* k0(1,26,38) -> 5* k0(5,2,28) -> 5* k0(27,37,2) -> 5* k0(28,1,37) -> 5* k0(3,39,40) -> 5* k0(39,4,28) -> 5* k0(50,37,37) -> 5* k0(3,28,37) -> 5* k0(41,5,1) -> 5* k0(37,41,40) -> 5* k0(28,4,38) -> 5* k0(40,37,26) -> 5* k0(38,38,28) -> 5* k0(1,3,27) -> 5* k0(1,50,40) -> 5* k0(39,27,4) -> 5* k0(26,41,50) -> 5* k0(50,40,38) -> 5* k0(1,39,37) -> 5* k0(26,26,41) -> 5* k0(27,50,1) -> 5* k0(5,28,5) -> 5* k0(2,1,41) -> 5* k0(40,40,27) -> 5* k0(3,5,26) -> 5* k0(37,38,4) -> 5* k0(38,2,39) -> 5* k0(28,28,40) -> 5* k0(37,27,1) -> 5* k0(5,38,3) -> 5* k0(3,39,5) -> 5* k0(41,38,41) -> 5* k0(4,3,40) -> 5* k0(28,2,28) -> 5* k0(50,37,2) -> 5* k0(2,5,2) -> 5* k0(3,28,2) -> 5* k0(41,27,38) -> 5* k0(39,40,3) -> 5* k0(38,5,40) -> 5* k0(26,39,40) -> 5* k0(37,41,5) -> 5* k0(41,1,26) -> 5* k0(5,41,4) -> 5* k0(26,28,37) -> 5* k0(1,50,5) -> 5* k0(1,39,2) -> 5* k0(39,38,38) -> 5* k0(2,3,37) -> 5* k0(40,1,2) -> 5* k0(5,39,39) -> 5* k0(41,4,27) -> 5* k0(50,50,1) -> 5* k0(38,2,4) -> 5* k0(3,41,1) -> 5* k0(41,40,37) -> 5* k0(28,28,5) -> 5* k0(39,41,39) -> 5* k0(26,5,26) -> 5* k0(4,3,5) -> 5* k0(3,50,39) -> 5* k0(2,27,39) -> 5* k0(40,4,3) -> 5* k0(28,38,3) -> 5* k0(5,3,50) -> 5* k0(38,5,5) -> 5* k0(26,39,5) -> 5* k0(27,3,40) -> 5* k0(2,1,27) -> 5* k0(39,5,50) -> 5* k0(26,28,2) -> 5* k0(41,37,1) -> 5* k0(37,26,27) -> 5* k0(40,2,38) -> 5* k0(28,41,4) -> 5* k0(5,26,26) -> 5* k0(2,4,28) -> 5* k0(38,39,50) -> 5* k0(39,28,26) -> 5* k0(4,5,1) -> 5* k0(41,40,2) -> 5* k0(28,39,39) -> 5* k0(3,37,26) -> 5* k0(1,38,28) -> 5* k0(26,41,1) -> 5* k0(2,27,4) -> 5* k0(40,26,40) -> 5* k0(37,39,26) -> 5* k0(27,3,5) -> 5* k0(26,50,39) -> 5* k0(3,40,27) -> 5* k0(28,3,50) -> 5* k0(1,2,39) -> 5* k0(50,3,40) -> 5* k0(38,37,40) -> 5* k0(38,26,37) -> 5* k0(4,38,41) -> 5* k0(2,40,3) -> 5* k0(4,27,38) -> 5* k0(28,26,26) -> 5* k0(1,5,40) -> 5* k0(38,40,41) -> 5* k0(4,1,26) -> 5* k0(27,5,1) -> 5* k0(40,26,5) -> 5* k0(2,38,38) -> 5* k0(38,3,26) -> 5* k0(26,37,26) -> 5* k0(41,26,50) -> 5* k0(4,4,27) -> 5* k0(3,1,2) -> 5* k0(41,39,28) -> 5* k0(50,3,5) -> 5* k0(38,37,5) -> 5* k0(1,2,4) -> 5* k0(39,1,40) -> 5* k0(4,40,37) -> 5* k0(39,37,50) -> 5* k0(37,3,2) -> 5* k0(2,41,39) -> 5* k0(26,40,27) -> 5* k0(38,26,2) -> 5* k0(5,2,41) -> 5* k0(39,50,28) -> 5* k0(38,27,28) -> 5* k0(40,39,4) -> 5* k0(3,4,3) -> 5* k0(41,3,39) -> 5* k0(1,5,5) -> 5* k0(39,4,41) -> 5* k0(27,38,41) -> 5* k0(40,28,1) -> 5* k0(37,1,37) -> 5* k0(27,27,38) -> 5* k0(2,5,50) -> 5* k0(4,37,1) -> 5* k0(38,50,4) -> 5* k0(3,2,38) -> 5* k0(27,1,26) -> 5* k0(50,5,1) -> 5* k0(38,39,1) -> 5* k0(1,39,50) -> 5* k0(37,4,38) -> 5* k0(2,28,26) -> 5* k0(4,40,2) -> 5* k0(5,4,37) -> 5* k0(39,1,5) -> 5* k0(27,4,27) -> 5* k0(40,1,50) -> 5* k0(26,1,2) -> 5* k0(27,40,37) -> 5* k0(3,26,40) -> 5* k0(41,3,4) -> 5* k0(40,50,38) -> 5* k0(28,2,41) -> 5* k0(37,28,40) -> 5* k0(26,4,3) -> 5* k0(5,1,1) -> 5* k0(5,28,39) -> 5* k0(1,37,40) -> 5* k0(37,2,28) -> 5* k0(50,38,41) -> 5* k0(50,27,38) -> 5* k0(1,26,37) -> 5* k0(39,3,1) -> 5* k0(27,37,1) -> 5* k0(26,2,38) -> 5* k0(50,1,26) -> 5* k0(40,27,27) -> 5* k0(1,40,41) -> 5* k0(5,5,28) -> 5* k0(41,40,50) -> 5* k0(27,40,2) -> 5* k0(28,4,37) -> 5* k0(3,26,5) -> 5* k0(50,4,27) -> 5* k0(38,38,27) -> 5* k0(1,3,26) -> 5* k0(39,27,3) -> 5* k0(4,26,50) -> 5* k0(50,40,37) -> 5* k0(37,28,5) -> 5* k0(26,26,40) -> 5* k0(4,39,28) -> 5* k0(38,28,50) -> 5* k0(5,28,4) -> 5* k0(1,37,5) -> 5* k0(2,1,40) -> 5* k0(40,40,26) -> 5* k0(37,38,3) -> 5* k0(2,37,50) -> 5* k0(38,41,28) -> 5* k0(1,26,2) -> 5* k0(28,1,1) -> 5* k0(28,28,39) -> 5* k0(1,27,28) -> 5* k0(2,50,28) -> 5* k0(3,39,4) -> 5* k0(41,38,40) -> 5* k0(4,3,39) -> 5* k0(50,37,1) -> 5* k0(3,28,1) -> 5* k0(41,27,37) -> 5* k0(2,4,41) -> 5* k0(37,41,4) -> 5* k0(38,5,39) -> 5* k0(5,41,3) -> 5* k0(39,2,27) -> 5* k0(1,50,4) -> 5* k0(41,41,41) -> 5* k0(28,5,28) -> 5* k0(50,40,2) -> 5* k0(1,39,1) -> 5* k0(39,38,37) -> 5* k0(26,26,5) -> 5* k0(37,39,39) -> 5* k0(5,50,41) -> 5* k0(27,26,50) -> 5* k0(5,39,38) -> 5* k0(41,4,26) -> 5* k0(2,1,5) -> 5* k0(27,39,28) -> 5* k0(38,2,3) -> 5* k0(3,1,50) -> 5* k0(28,28,4) -> 5* k0(39,41,38) -> 5* k0(4,3,4) -> 5* k0(37,3,50) -> 5* k0(41,38,5) -> 5* k0(3,50,38) -> 5* k0(41,27,2) -> 5* k0(40,4,2) -> 5* k0(27,3,39) -> 5* k0(38,5,4) -> 5* k0(26,39,4) -> 5* k0(41,28,28) -> 5* k0(26,28,1) -> 5* k0(37,26,26) -> 5* k0(39,38,2) -> 5* k0(2,3,1) -> 5* k0(40,2,37) -> 5* k0(28,41,3) -> 5* k0(3,27,27) -> 5* k0(41,40,1) -> 5* k0(28,50,41) -> 5* k0(50,26,50) -> 5* k0(4,40,50) -> 5* k0(40,5,38) -> 5* k0(28,39,38) -> 5* k0(26,1,50) -> 5* k0(50,39,28) -> 5* k0(1,38,27) -> 5* k0(2,27,3) -> 5* k0(40,26,39) -> 5* k0(38,27,41) -> 5* k0(27,3,4) -> 5* k0(26,50,38) -> 5* k0(1,28,50) -> 5* k0(3,40,26) -> 5* k0(50,3,39) -> 5* k0(38,37,39) -> 5* k0(1,41,28) -> 5* k0(4,38,40) -> 5* k0(40,3,28) -> 5* k0(4,27,37) -> 5* k0(26,27,27) -> 5* k0(38,40,40) -> 5* k0(1,5,39) -> 5* k0(39,37,28) -> 5* k0(2,2,27) -> 5* k0(4,41,41) -> 5* k0(40,26,4) -> 5* k0(27,40,50) -> 5* k0(2,38,37) -> 5* k0(41,39,27) -> 5* k0(4,4,26) -> 5* k0(50,3,4) -> 5* k0(38,37,4) -> 5* k0(1,2,3) -> 5* k0(39,1,39) -> 5* k0(26,40,26) -> 5* k0(38,26,1) -> 5* k0(37,2,41) -> 5* k0(2,41,38) -> 5* k0(4,38,5) -> 5* k0(5,2,40) -> 5* k0(39,50,27) -> 5* k0(4,27,2) -> 5* k0(40,39,3) -> 5* k0(3,4,2) -> 5* k0(38,40,5) -> 5* k0(1,5,4) -> 5* k0(39,4,40) -> 5* k0(27,38,40) -> 5* k0(4,28,28) -> 5* k0(27,27,37) -> 5* k0(5,5,41) -> 5* k0(2,38,2) -> 5* k0(40,37,38) -> 5* k0(38,50,3) -> 5* k0(3,2,37) -> 5* k0(27,41,41) -> 5* k0(37,4,37) -> 5* k0(50,40,50) -> 5* k0(39,1,4) -> 5* k0(4,40,1) -> 5* k0(40,40,39) -> 5* k0(3,5,38) -> 5* k0(27,4,26) -> 5* k0(5,2,5) -> 5* k0(3,26,39) -> 5* k0(41,3,3) -> 5* k0(40,50,37) -> 5* k0(1,27,41) -> 5* k0(39,4,5) -> 5* k0(27,38,5) -> 5* k0(28,2,40) -> 5* k0(37,1,1) -> 5* k0(37,28,39) -> 5* k0(40,4,50) -> 5* k0(26,4,2) -> 5* k0(27,27,2) -> 5* k0(50,38,40) -> 5* k0(1,37,39) -> 5* k0(27,28,28) -> 5* k0(50,27,37) -> 5* k0(28,5,41) -> 5* k0(3,3,28) -> 5* k0(39,38,50) -> 5* k0(26,2,37) -> 5* k0(40,27,26) -> 5* k0(5,4,1) -> 5* k0(50,41,41) -> 5* k0(1,40,40) -> 5* k0(37,5,28) -> 5* k0(2,37,28) -> 5* k0(27,40,1) -> 5* k0(3,26,4) -> 5* k0(26,5,38) -> 5* k0(50,4,26) -> 5* k0(38,38,26) -> 5* k0(40,50,2) -> 5* k0(28,2,5) -> 5* k0(37,28,4) -> 5* k0(26,26,39) -> 5* k0(4,39,27) -> 5* k0(5,28,3) -> 5* k0(50,38,5) -> 5* k0(1,37,4) -> 5* k0(2,1,39) -> 5* k0(41,28,41) -> 5* k0(38,41,27) -> 5* k0(50,27,2) -> 5* k0(1,26,1) -> 5* k0(5,37,41) -> 5* k0(2,50,27) -> 5* k0(50,28,28) -> 5* k0(5,26,38) -> 5* k0(3,39,3) -> 5* k0(2,4,40) -> 5* k0(26,3,28) -> 5* k0(1,40,5) -> 5* k0(39,39,41) -> 5* k0(39,28,38) -> 5* k0(37,41,3) -> 5* k0(28,4,1) -> 5* k0(3,37,38) -> 5* k0(39,2,26) -> 5* k0(1,50,3) -> 5* k0(41,41,40) -> 5* k0(37,50,41) -> 5* k0(50,40,1) -> 5* k0(26,26,4) -> 5* k0(5,3,27) -> 5* k0(37,39,38) -> 5* k0(5,50,40) -> 5* k0(5,39,37) -> 5* k0(2,1,4) -> 5* k0(27,39,27) -> 5* k0(39,5,27) -> 5* k0(3,40,39) -> 5* k0(38,2,2) -> 5* k0(28,28,3) -> 5* k0(39,41,37) -> 5* k0(39,26,28) -> 5* k0(4,3,3) -> 5* k0(41,38,4) -> 5* k0(3,50,37) -> 5* k0(41,27,1) -> 5* k0(28,37,41) -> 5* k0(40,3,41) -> 5* k0(2,4,5) -> 5* k0(28,26,38) -> 5* k0(26,39,3) -> 5* k0(38,5,3) -> 5* k0(3,4,50) -> 5* k0(41,41,5) -> 5* k0(39,38,1) -> 5* k0(26,37,38) -> 5* k0(38,3,38) -> 5* k0(5,50,5) -> 5* k0(2,38,50) -> 5* k0(3,27,26) -> 5* k0(5,39,2) -> 5* k0(28,3,27) -> 5* k0(28,50,40) -> 5* k0(28,39,37) -> 5* k0(40,5,37) -> 5* k0(39,41,2) -> 5* k0(26,40,39) -> 5* k0(1,38,26) -> 5* k0(50,39,27) -> 5* k0(3,50,2) -> 5* k0(38,27,40) -> 5* k0(27,3,3) -> 5* k0(26,50,37) -> 5* k0(38,1,28) -> 5* k0(4,28,41) -> 5* k0(1,41,27) -> 5* k0(26,4,50) -> 5* k0(40,2,1) -> 5* k0(41,26,27) -> 5* k0(2,39,41) -> 5* k0(28,50,5) -> 5* k0(26,27,26) -> 5* k0(2,28,38) -> 5* k0(28,39,2) -> 5* k0(2,2,26) -> 5* k0(39,37,27) -> 5* k0(40,26,3) -> 5* k0(4,41,40) -> 5* k0(38,27,5) -> 5* k0(5,38,28) -> 5* k0(39,27,50) -> 5* k0(26,50,2) -> 5* k0(40,50,50) -> 5* k0(41,39,26) -> 5* k0(38,37,3) -> 5* k0(2,5,27) -> 5* k0(39,40,28) -> 5* k0(39,1,38) -> 5* k0(1,2,2) -> 5* k0(50,3,3) -> 5* k0(2,41,37) -> 5* k0(37,2,40) -> 5* k0(2,26,28) -> 5* k0(27,28,41) -> 5* k0(5,2,39) -> 5* k0(4,38,4) -> 5* k0(39,50,26) -> 5* k0(4,27,1) -> 5* k0(3,3,41) -> 5* k0(39,4,39) -> 5* k0(1,5,3) -> 5* k0(38,40,4) -> 5* k0(37,5,41) -> 5* k0(5,5,40) -> 5* k0(4,41,5) -> 5* k0(40,37,37) -> 5* k0(2,38,1) -> 5* k0(1,3,38) -> 5* k0(38,38,39) -> 5* k0(27,41,40) -> 5* k0(39,1,3) -> 5* k0(28,38,28) -> 5* k0(3,5,37) -> 5* k0(40,40,38) -> 5* k0(2,41,2) -> 5* k0(37,2,5) -> 5* k0(5,2,4) -> 5* k0(38,2,50) -> 5* k0(41,3,2) -> 5* k0(1,27,40) -> 5* k0(50,28,41) -> 5* k0(28,2,39) -> 5* k0(27,38,4) -> 5* k0(39,4,4) -> 5* k0(26,3,41) -> 5* k0(27,27,1) -> 5* k0(1,1,28) -> 5* k0(5,5,5) -> 5* k0(40,37,2) -> 5* k0(41,1,37) -> 5* k0(3,2,1) -> 5* k0(4,26,27) -> 5* k0(27,41,5) -> 5* k0(28,5,40) -> 5* k0(37,4,1) -> 5* k0(38,28,27) -> 5* k0(50,41,40) -> 5* k0(41,4,38) -> 5* k0(5,39,50) -> 5* k0(2,37,27) -> 5* k0(3,26,3) -> 5* k0(26,5,37) -> 5* k0(39,41,50) -> 5* k0(39,26,41) -> 5* k0(1,27,5) -> 5* k0(40,50,1) -> 5* k0(28,2,4) -> 5* k0(37,28,3) -> 5* k0(2,27,50) -> 5* k0(3,50,50) -> 5* k0(4,39,26) -> 5* k0(2,40,28) -> 5* k0(2,1,38) -> 5* k0(1,37,3) -> 5* k0(50,38,4) -> 5* k0(41,28,40) -> 5* k0(38,41,26) -> 5* k0(37,37,41) -> 5* k0(50,27,1) -> 5* k0(41,2,28) -> 5* k0(5,37,40) -> 5* k0(37,26,38) -> 5* k0(28,5,5) -> 5* k0(26,2,1) -> 5* k0(2,50,26) -> 5* k0(5,26,37) -> 5* k0(2,4,39) -> 5* k0(39,39,40) -> 5* k0(1,40,4) -> 5* k0(27,26,27) -> 5* k0(50,41,5) -> 5* k0(39,28,37) -> 5* k0(5,40,41) -> 5* k0(3,37,37) -> 5* k0(28,39,50) -> 5* k0(37,3,27) -> 5* k0(1,38,39) -> 5* k0(37,50,40) -> 5* k0(26,26,3) -> 5* k0(37,39,37) -> 5* k0(5,3,26) -> 5* k0(2,1,3) -> 5* k0(41,28,5) -> 5* k0(26,50,50) -> 5* k0(27,39,26) -> 5* k0(39,5,26) -> 5* k0(3,40,38) -> 5* k0(38,1,41) -> 5* k0(5,37,5) -> 5* k0(1,2,50) -> 5* k0(4,3,2) -> 5* k0(41,38,3) -> 5* k0(5,26,2) -> 5* k0(28,37,40) -> 5* k0(40,3,40) -> 5* k0(2,4,4) -> 5* k0(39,39,5) -> 5* k0(5,27,28) -> 5* k0(38,5,2) -> 5* k0(28,26,37) -> 5* k0(39,28,2) -> 5* k0(50,26,27) -> 5* k0(4,1,37) -> 5* k0(3,37,2) -> 5* k0(41,41,4) -> 5* k0(37,50,5) -> 5* k0(28,40,41) -> 5* k0(38,3,37) -> 5* k0(37,39,2) -> 5* k0(26,37,37) -> 5* k0(5,50,4) -> 5* k0(5,39,1) -> 5* k0(1,28,27) -> 5* k0(28,3,26) -> 5* k0(4,4,38) -> 5* k0(41,39,39) -> 5* k0(39,41,1) -> 5* k0(26,40,38) -> 5* k0(2,41,50) -> 5* k0(50,39,26) -> 5* k0(2,26,41) -> 5* k0(3,50,1) -> 5* k0(28,37,5) -> 5* k0(40,3,5) -> 5* k0(38,27,39) -> 5* k0(39,50,39) -> 5* k0(28,26,2) -> 5* k0(27,3,2) -> 5* k0(41,3,50) -> 5* k0(38,1,27) -> 5* k0(28,27,28) -> 5* k0(4,28,40) -> 5* k0(1,41,26) -> 5* k0(4,2,28) -> 5* k0(27,1,37) -> 5* k0(26,37,2) -> 5* k0(41,26,26) -> 5* k0(38,4,28) -> 5* k0(2,39,40) -> 5* k0(28,50,4) -> 5* k0(2,28,37) -> 5* k0(28,39,1) -> 5* k0(40,5,1) -> 5* k0(39,37,26) -> 5* k0(27,4,38) -> 5* k0(37,38,28) -> 5* k0(38,27,4) -> 5* k0(5,38,27) -> 5* k0(26,50,1) -> 5* k0(4,28,5) -> 5* k0(39,40,27) -> 5* k0(1,1,41) -> 5* k0(2,5,26) -> 5* k0(50,3,2) -> 5* k0(5,28,50) -> 5* k0(37,2,39) -> 5* k0(27,28,40) -> 5* k0(4,38,3) -> 5* k0(5,41,28) -> 5* k0(40,38,41) -> 5* k0(2,39,5) -> 5* k0(27,2,28) -> 5* k0(3,3,40) -> 5* k0(50,1,37) -> 5* k0(1,5,2) -> 5* k0(38,40,3) -> 5* k0(40,27,38) -> 5* k0(2,28,2) -> 5* k0(37,5,40) -> 5* k0(40,1,26) -> 5* k0(4,41,4) -> 5* k0(5,5,39) -> 5* k0(38,38,38) -> 5* k0(1,3,37) -> 5* k0(50,4,38) -> 5* k0(39,1,2) -> 5* k0(28,38,27) -> 5* k0(40,4,27) -> 5* k0(4,39,39) -> 5* k0(37,2,4) -> 5* k0(40,40,37) -> 5* k0(2,41,1) -> 5* k0(27,28,5) -> 5* k0(5,2,3) -> 5* k0(38,41,39) -> 5* k0(28,28,50) -> 5* k0(41,2,41) -> 5* k0(3,3,5) -> 5* k0(1,27,39) -> 5* k0(50,28,40) -> 5* k0(2,50,39) -> 5* k0(28,41,28) -> 5* k0(27,38,3) -> 5* k0(39,4,3) -> 5* k0(4,3,50) -> 5* k0(37,5,5) -> 5* k0(1,1,27) -> 5* k0(26,3,40) -> 5* k0(50,2,28) -> 5* k0(5,5,4) -> 5* k0(38,5,50) -> 5* k0(40,37,1) -> 5* k0(39,2,38) -> 5* k0(28,5,39) -> 5* k0(4,26,26) -> 5* k0(27,41,4) -> 5* k0(1,4,28) -> 5* k0(37,39,50) -> 5* k0(38,28,26) -> 5* k0(41,4,37) -> 5* k0(3,5,1) -> 5* k0(40,40,2) -> 5* k0(2,37,26) -> 5* k0(27,39,39) -> 5* k0(39,26,40) -> 5* k0(1,27,4) -> 5* k0(50,28,5) -> 5* k0(28,2,3) -> 5* k0(26,3,5) -> 5* k0(5,27,41) -> 5* k0(2,40,27) -> 5* k0(27,3,50) -> 5* k0(50,38,3) -> 5* k0(41,28,39) -> 5* k0(41,1,1) -> 5* k0(37,37,40) -> 5* k0(37,26,37) -> 5* k0(28,5,4) -> 5* k0(5,37,39) -> 5* k0(3,38,41) -> 5* k0(1,40,3) -> 5* k0(27,26,26) -> 5* k0(3,27,38) -> 5* k0(50,41,4) -> 5* k0(37,40,41) -> 5* k0(3,1,26) -> 5* k0(41,5,28) -> 5* k0(5,40,40) -> 5* k0(26,5,1) -> 5* k0(39,26,5) -> 5* k0(37,3,26) -> 5* k0(1,38,38) -> 5* k0(50,39,39) -> 5* k0(40,26,50) -> 5* k0(3,4,27) -> 5* k0(40,39,28) -> 5* k0(2,1,2) -> 5* k0(41,28,4) -> 5* k0(37,37,5) -> 5* k0(3,40,37) -> 5* k0(38,1,40) -> 5* k0(28,27,41) -> 5* k0(5,37,4) -> 5* k0(37,26,2) -> 5* k0(1,41,39) -> 5* k0(38,37,50) -> 5* k0(50,3,50) -> 5* k0(5,26,1) -> 5* k0(4,2,41) -> 5* k0(37,27,28) -> 5* k0(38,50,28) -> 5* k0(28,37,39) -> 5* k0(40,3,39) -> 5* k0(2,4,3) -> 5* k0(39,39,4) -> 5* k0(39,28,1) -> 5* k0(26,38,41) -> 5* k0(38,4,41) -> 5* k0(26,27,38) -> 5* k0(5,40,5) -> 5* k0(50,26,26) -> 5* k0(1,5,50) -> 5* k0(3,37,1) -> 5* k0(41,41,3) -> 5* k0(26,1,26) -> 5* k0(2,2,38) -> 5* k0(37,50,4) -> 5* k0(28,40,40) -> 5* k0(37,39,1) -> 5* k0(5,50,3) -> 5* k0(41,50,41) -> 5* k0(1,28,26) -> 5* k0(4,4,37) -> 5* k0(41,39,38) -> 5* k0(3,40,2) -> 5* k0(38,1,5) -> 5* k0(26,4,27) -> 5* k0(39,1,50) -> 5* k0(26,40,37) -> 5* k0(2,26,40) -> 5* k0(28,37,4) -> 5* k0(40,3,4) -> 5* k0(39,50,38) -> 5* k0(27,2,41) -> 5* k0(28,26,1) -> 5* k0(4,28,39) -> 5* k0(4,1,1) -> 5* k0(28,40,5) -> 5* k0(26,37,1) -> 5* k0(38,3,1) -> 5* k0(39,27,27) -> 5* k0(28,50,3) -> 5* k0(4,5,28) -> 5* k0(26,40,2) -> 5* k0(27,4,37) -> 5* k0(40,40,50) -> 5* k0(2,26,5) -> 5* k0(37,38,27) -> 5* k0(38,27,3) -> 5* k0(3,26,50) -> 5* k0(5,38,26) -> 5* k0(3,39,28) -> 5* k0(4,28,4) -> 5* k0(37,28,50) -> 5* k0(39,40,26) -> 5* k0(1,1,40) -> 5* k0(50,2,41) -> 5* k0(37,41,28) -> 5* k0(1,37,50) -> 5* k0(27,28,39) -> 5* k0(27,1,1) -> 5* k0(5,41,27) -> 5* k0(1,50,28) -> 5* k0(3,3,39) -> 5* k0(40,38,40) -> 5* k0(2,39,4) -> 5* k0(40,27,37) -> 5* k0(2,28,1) -> 5* k0(1,4,41) -> 5* k0(37,5,39) -> 5* k0(4,41,3) -> 5* k0(38,2,27) -> 5* k0(27,5,28) -> 5* k0(40,41,41) -> 5* k0(38,38,37) -> 5* k0(50,4,37) -> 5* k0(4,50,41) -> 5* k0(26,26,50) -> 5* k0(28,38,26) -> 5* k0(40,4,26) -> 5* k0(4,39,38) -> 5* k0(1,1,5) -> 5* k0(26,39,28) -> 5* k0(37,2,3) -> 5* k0(2,1,50) -> 5* k0(27,28,4) -> 5* k0(5,2,2) -> 5* k0(38,41,38) -> 5* k0(41,2,40) -> 5* k0(3,3,4) -> 5* k0(40,38,5) -> 5* k0(2,50,38) -> 5* k0(50,28,39) -> 5* k0(50,1,1) -> 5* k0(39,4,2) -> 5* k0(40,27,2) -> 5* k0(28,41,27) -> 5* k0(26,3,39) -> 5* k0(37,5,4) -> 5* k0(40,28,28) -> 5* k0(5,5,3) -> 5* k0(41,5,41) -> 5* k0(39,2,37) -> 5* k0(1,3,1) -> 5* k0(38,38,2) -> 5* k0(27,41,3) -> 5* k0(2,27,27) -> 5* k0(50,5,28) -> 5* k0(5,3,38) -> 5* k0(40,40,1) -> 5* k0(27,50,41) -> 5* k0(27,39,38) -> 5* k0(39,5,38) -> 5* k0(3,40,50) -> 5* k0(41,2,5) -> 5* k0(39,26,39) -> 5* k0(1,27,3) -> 5* k0(50,28,4) -> 5* k0(28,2,2) -> 5* k0(37,27,41) -> 5* k0(26,3,4) -> 5* k0(5,27,40) -> 5* k0(2,40,26) -> 5* k0(37,37,39) -> 5* k0(5,1,28) -> 5* k0(28,5,3) -> 5* k0(39,3,28) -> 5* k0(3,38,40) -> 5* k0(3,27,37) -> 5* k0(50,41,3) -> 5* k0(41,4,1) -> 5* k0(37,40,40) -> 5* k0(28,3,38) -> 5* k0(1,2,27) -> 5* k0(38,37,28) -> 5* k0(50,50,41) -> 5* k0(39,26,4) -> 5* k0(3,41,41) -> 5* k0(1,38,37) -> 5* k0(26,40,50) -> 5* k0(50,39,38) -> 5* k0(5,27,5) -> 5* k0(40,39,27) -> 5* k0(3,4,26) -> 5* k0(41,28,3) -> 5* k0(38,1,39) -> 5* k0(37,37,4) -> 5* k0(28,27,40) -> 5* k0(5,37,3) -> 5* k0(37,26,1) -> 5* k0(1,41,38) -> 5* k0(4,2,40) -> 5* k0(41,37,41) -> 5* k0(3,38,5) -> 5* k0(28,1,28) -> 5* k0(38,50,27) -> 5* k0(2,4,2) -> 5* k0(39,39,3) -> 5* k0(41,26,38) -> 5* k0(3,27,2) -> 5* k0(37,40,5) -> 5* k0(38,4,40) -> 5* k0(26,38,40) -> 5* k0(3,28,28) -> 5* k0(26,27,37) -> 5* k0(5,40,4) -> 5* k0(4,5,41) -> 5* k0(2,2,37) -> 5* k0(1,38,2) -> 5* k0(39,37,38) -> 5* k0(37,50,3) -> 5* k0(26,41,41) -> 5* k0(41,3,27) -> 5* k0(5,38,39) -> 5* k0(41,50,40) -> 5* k0(3,40,1) -> 5* k0(41,39,37) -> 5* k0(38,1,4) -> 5* k0(28,27,5) -> 5* k0(2,5,38) -> 5* k0(26,4,26) -> 5* k0(39,40,39) -> 5* k0(4,2,5) -> 5* k0(2,26,39) -> 5* k0(40,3,3) -> 5* k0(28,37,3) -> 5* k0(5,2,50) -> 5* k0(39,50,37) -> 5* k0(27,2,40) -> 5* k0(38,4,5) -> 5* k0(26,38,5) -> 5* k0(26,27,2) -> 5* k0(39,4,50) -> 5* k0(26,28,28) -> 5* k0(28,40,4) -> 5* k0(27,5,41) -> 5* k0(2,3,28) -> 5* k0(38,38,50) -> 5* k0(41,50,5) -> 5* k0(39,27,26) -> 5* k0(41,39,2) -> 5* k0(4,4,1) -> 5* k0(28,38,39) -> 5* k0(5,28,27) -> 5* k0(26,40,1) -> 5* k0(1,37,28) -> 5* k0(2,26,4) -> 5* k0(37,38,26) -> 5* k0(39,50,2) -> 5* k0(27,2,5) -> 5* k0(3,39,27) -> 5* k0(28,2,50) -> 5* k0(4,28,3) -> 5* k0(1,1,39) -> 5* k0(50,2,40) -> 5* k0(40,28,41) -> 5* k0(37,41,27) -> 5* k0(5,41,26) -> 5* k0(4,37,41) -> 5* k0(1,50,27) -> 5* k0(4,26,38) -> 5* k0(2,39,3) -> 5* k0(38,39,41) -> 5* k0(1,4,40) -> 5* k0(50,5,41) -> 5* k0(38,28,38) -> 5* k0(27,4,1) -> 5* k0(2,37,38) -> 5* k0(38,2,26) -> 5* k0(28,28,27) -> 5* k0(40,41,40) -> 5* k0(41,38,28) -> 5* k0(4,3,27) -> 5* k0(4,50,40) -> 5* k0(4,39,37) -> 5* k0(1,1,4) -> 5* k0(50,2,5) -> 5* k0(2,40,39) -> 5* k0(38,5,27) -> 5* k0(26,39,27) -> 5* k0(37,2,2) -> 5* k0(27,28,3) -> 5* k0(5,1,41) -> 5* k0(38,41,37) -> 5* k0(38,26,28) -> 5* k0(3,3,3) -> 5* k0(41,2,39) -> 5* k0(40,38,4) -> 5* k0(2,50,37) -> 5* k0(39,3,41) -> 5* k0(1,4,5) -> 5* k0(27,37,41) -> 5* k0(28,41,26) -> 5* k0(40,27,1) -> 5* k0(27,26,38) -> 5* k0(37,5,3) -> 5* k0(2,4,50) -> 5* k0(5,5,2) -> 5* k0(40,41,5) -> 5* k0(41,5,40) -> 5* k0(38,38,1) -> 5* k0(50,4,1) -> 5* k0(37,3,38) -> 5* k0(4,50,5) -> 5* k0(1,38,50) -> 5* k0(2,27,26) -> 5* k0(4,39,2) -> 5* k0(5,3,37) -> 5* k0(27,3,27) -> 5* k0(27,50,40) -> 5* k0(38,41,2) -> 5* k0(39,5,37) -> 5* k0(27,39,37) -> 5* k0(41,2,4) -> 5* k0(50,28,3) -> 5* k0(2,50,2) -> 5* k0(28,1,41) -> 5* k0(37,27,40) -> 5* k0(26,3,3) -> 5* k0(5,27,39) -> 5* k0(37,1,28) -> 5* k0(50,37,41) -> 5* k0(3,28,41) -> 5* k0(41,5,5) -> 5* k0(5,1,27) -> 5* k0(50,26,38) -> 5* k0(39,2,1) -> 5* k0(28,5,2) -> 5* k0(40,26,27) -> 5* k0(1,39,41) -> 5* k0(27,50,5) -> 5* k0(1,28,38) -> 5* k0(5,4,28) -> 5* k0(27,39,2) -> 5* k0(28,3,37) -> 5* k0(41,39,50) -> 5* k0(38,37,27) -> 5* k0(1,2,26) -> 5* k0(50,50,40) -> 5* k0(50,3,27) -> 5* k0(3,41,40) -> 5* k0(39,26,3) -> 5* k0(50,39,37) -> 5* k0(37,27,5) -> 5* k0(4,38,28) -> 5* k0(5,27,4) -> 5* k0(38,27,50) -> 5* k0(39,50,50) -> 5* k0(40,39,26) -> 5* k0(38,40,28) -> 5* k0(1,5,27) -> 5* k0(37,37,3) -> 5* k0(38,1,38) -> 5* k0(28,27,39) -> 5* k0(1,41,37) -> 5* k0(26,28,41) -> 5* k0(1,26,28) -> 5* k0(3,38,4) -> 5* k0(41,37,40) -> 5* k0(4,2,39) -> 5* k0(28,1,27) -> 5* k0(38,50,26) -> 5* k0(2,3,41) -> 5* k0(3,27,1) -> 5* k0(41,26,37) -> 5* k0(37,40,4) -> 5* k0(38,4,39) -> 5* k0(5,40,3) -> 5* k0(50,50,5) -> 5* k0(3,41,5) -> 5* k0(41,40,41) -> 5* k0(4,5,40) -> 5* k0(28,4,28) -> 5* k0(1,38,1) -> 5* k0(39,37,37) -> 5* k0(50,39,2) -> 5* k0(37,38,39) -> 5* k0(26,41,40) -> 5* k0(5,38,38) -> 5* k0(41,3,26) -> 5* k0(38,1,3) -> 5* k0(27,38,28) -> 5* k0(28,27,4) -> 5* k0(1,41,2) -> 5* k0(39,40,38) -> 5* k0(2,5,37) -> 5* k0(41,37,5) -> 5* k0(4,2,4) -> 5* k0(37,2,50) -> 5* k0(40,3,2) -> 5* k0(5,41,39) -> 5* k0(41,26,2) -> 5* k0(38,4,4) -> 5* k0(26,38,4) -> 5* k0(27,2,39) -> 5* k0(41,27,28) -> 5* k0(26,27,1) -> 5* k0(4,5,5) -> 5* k0(39,37,2) -> 5* k0(2,2,1) -> 5* k0(40,1,37) -> 5* k0(28,40,3) -> 5* k0(5,5,50) -> 5* k0(26,41,5) -> 5* k0(3,26,27) -> 5* k0(27,5,40) -> 5* k0(41,50,4) -> 5* k0(41,39,1) -> 5* k0(37,28,27) -> 5* k0(40,4,38) -> 5* k0(28,38,38) -> 5* k0(4,39,50) -> 5* k0(5,28,26) -> 5* k0(1,37,27) -> 5* k0(50,38,28) -> 5* k0(2,26,3) -> 5* k0(38,41,50) -> 5* k0(38,26,41) -> 5* k0(39,50,1) -> 5* k0(27,2,4) -> 5* k0(1,27,50) -> 5* k0(2,50,50) -> 5* k0(28,41,39) -> 5* k0(3,39,26) -> 5* k0(1,40,28) -> 5* k0(1,1,38) -> 5* k0(50,2,39) -> 5* k0(40,28,40) -> 5* k0(37,41,26) -> 5* k0(4,37,40) -> 5* k0(40,2,28) -> 5* k0(27,5,5) -> 5* k0(1,50,26) -> 5* k0(4,26,37) -> 5* k0(28,5,50) -> 5* k0(1,4,39) -> 5* k0(26,26,27) -> 5* k0(38,39,40) -> 5* k0(50,5,40) -> 5* k0(38,28,37) -> 5* k0(4,40,41) -> 5* k0(2,37,37) -> 5* k0(27,39,50) -> 5* k0(28,28,26) -> 5* f1(50) -> 5,26* f1(40) -> 26* f1(5) -> 26*,5,2 f1(37) -> 26* f1(27) -> 26* f1(2) -> 26*,5,2 f1(39) -> 5,26* f1(41) -> 26* f1(26) -> 5,26* f1(1) -> 26*,5,2 f1(38) -> 5,26* f1(28) -> 26* f1(3) -> 26*,5,2 h1(50) -> 27* h1(40) -> 5,27* h1(5) -> 27*,4,5 h1(37) -> 5,27* h1(27) -> 5,27* h1(2) -> 27*,5,4 h1(39) -> 27* h1(4) -> 27*,4,5 h1(41) -> 5,27* h1(26) -> 5,27* h1(1) -> 27*,4,5 h1(38) -> 27* h1(28) -> 5,27* h1(3) -> 27*,5,4 g1(40) -> 37* g1(37) -> 1,37* g1(27) -> 28,27,37*,1 g1(4) -> 28,27,37*,1,4,2 g1(41) -> 37* g1(28) -> 28,37*,1 h{#,1}(50) -> 6* h{#,1}(37) -> 6* h{#,1}(2) -> 6* h{#,1}(26) -> 6* h{#,1}(38) -> 6* h{#,1}(28) -> 6* g2(40) -> 26,37*,1 g2(32) -> 27* g2(41) -> 27,37*,1 g2(31) -> 26* h2(50) -> 27,5,41*,32 h2(30) -> 31* h2(39) -> 27,5,40*,31 h2(29) -> 32* h2(38) -> 27,5,41*,32 f2(40) -> 26,5,38* f2(37) -> 26,5,38* f2(32) -> 50*,2,29 f2(27) -> 26,38*,5,29 f2(4) -> 26,38*,2,5,29 f2(41) -> 26,5,38* f2(31) -> 50*,2,29 f2(28) -> 26,38*,5,29 a2() -> 39*,3,30 h{#,2}(50) -> 6* h{#,2}(29) -> 6* h{#,2}(38) -> 6* problem: DPs: TRS: f(a()) -> g(h(a())) h(g(x)) -> g(h(f(x))) k(x,h(x),a()) -> h(x) k(f(x),y,x) -> f(x) Qed