YES O(n) TRS: { h(g(x)) -> g(h(f(x))), f(a()) -> g(h(a())), k(x, h(x), a()) -> h(x), k(f(x), y, x) -> f(x) } DUP: We consider a non-duplicating system. Trs: { h(g(x)) -> g(h(f(x))), f(a()) -> g(h(a())), k(x, h(x), a()) -> h(x), k(f(x), y, x) -> f(x) } BOUND: Automaton: { k_0(47, 47, 47) -> 4, k_0(47, 47, 46) -> 4, k_0(47, 47, 45) -> 4, k_0(47, 47, 44) -> 4, k_0(47, 47, 43) -> 4, k_0(47, 47, 42) -> 4, k_0(47, 47, 41) -> 4, k_0(47, 47, 40) -> 4, k_0(47, 47, 39) -> 4, k_0(47, 47, 38) -> 4, k_0(47, 47, 4) -> 4, k_0(47, 47, 3) -> 4, k_0(47, 47, 2) -> 4, k_0(47, 47, 1) -> 4, k_0(47, 47, 0) -> 4, k_0(47, 46, 47) -> 4, k_0(47, 46, 46) -> 4, k_0(47, 46, 45) -> 4, k_0(47, 46, 44) -> 4, k_0(47, 46, 43) -> 4, k_0(47, 46, 42) -> 4, k_0(47, 46, 41) -> 4, k_0(47, 46, 40) -> 4, k_0(47, 46, 39) -> 4, k_0(47, 46, 38) -> 4, k_0(47, 46, 4) -> 4, k_0(47, 46, 3) -> 4, k_0(47, 46, 2) -> 4, k_0(47, 46, 1) -> 4, k_0(47, 46, 0) -> 4, k_0(47, 45, 47) -> 4, k_0(47, 45, 46) -> 4, k_0(47, 45, 45) -> 4, k_0(47, 45, 44) -> 4, k_0(47, 45, 43) -> 4, k_0(47, 45, 42) -> 4, k_0(47, 45, 41) -> 4, k_0(47, 45, 40) -> 4, k_0(47, 45, 39) -> 4, k_0(47, 45, 38) -> 4, k_0(47, 45, 4) -> 4, k_0(47, 45, 3) -> 4, k_0(47, 45, 2) -> 4, k_0(47, 45, 1) -> 4, k_0(47, 45, 0) -> 4, k_0(47, 44, 47) -> 4, k_0(47, 44, 46) -> 4, k_0(47, 44, 45) -> 4, k_0(47, 44, 44) -> 4, k_0(47, 44, 43) -> 4, k_0(47, 44, 42) -> 4, k_0(47, 44, 41) -> 4, k_0(47, 44, 40) -> 4, k_0(47, 44, 39) -> 4, k_0(47, 44, 38) -> 4, k_0(47, 44, 4) -> 4, k_0(47, 44, 3) -> 4, k_0(47, 44, 2) -> 4, k_0(47, 44, 1) -> 4, k_0(47, 44, 0) -> 4, k_0(47, 43, 47) -> 4, k_0(47, 43, 46) -> 4, k_0(47, 43, 45) -> 4, k_0(47, 43, 44) -> 4, k_0(47, 43, 43) -> 4, k_0(47, 43, 42) -> 4, k_0(47, 43, 41) -> 4, k_0(47, 43, 40) -> 4, k_0(47, 43, 39) -> 4, k_0(47, 43, 38) -> 4, k_0(47, 43, 4) -> 4, k_0(47, 43, 3) -> 4, k_0(47, 43, 2) -> 4, k_0(47, 43, 1) -> 4, k_0(47, 43, 0) -> 4, k_0(47, 42, 47) -> 4, k_0(47, 42, 46) -> 4, k_0(47, 42, 45) -> 4, k_0(47, 42, 44) -> 4, k_0(47, 42, 43) -> 4, k_0(47, 42, 42) -> 4, k_0(47, 42, 41) -> 4, k_0(47, 42, 40) -> 4, k_0(47, 42, 39) -> 4, k_0(47, 42, 38) -> 4, k_0(47, 42, 4) -> 4, k_0(47, 42, 3) -> 4, k_0(47, 42, 2) -> 4, k_0(47, 42, 1) -> 4, k_0(47, 42, 0) -> 4, k_0(47, 41, 47) -> 4, k_0(47, 41, 46) -> 4, k_0(47, 41, 45) -> 4, k_0(47, 41, 44) -> 4, k_0(47, 41, 43) -> 4, k_0(47, 41, 42) -> 4, k_0(47, 41, 41) -> 4, k_0(47, 41, 40) -> 4, k_0(47, 41, 39) -> 4, k_0(47, 41, 38) -> 4, k_0(47, 41, 4) -> 4, k_0(47, 41, 3) -> 4, k_0(47, 41, 2) -> 4, k_0(47, 41, 1) -> 4, k_0(47, 41, 0) -> 4, k_0(47, 40, 47) -> 4, k_0(47, 40, 46) -> 4, k_0(47, 40, 45) -> 4, k_0(47, 40, 44) -> 4, k_0(47, 40, 43) -> 4, k_0(47, 40, 42) -> 4, k_0(47, 40, 41) -> 4, k_0(47, 40, 40) -> 4, k_0(47, 40, 39) -> 4, k_0(47, 40, 38) -> 4, k_0(47, 40, 4) -> 4, k_0(47, 40, 3) -> 4, k_0(47, 40, 2) -> 4, k_0(47, 40, 1) -> 4, k_0(47, 40, 0) -> 4, k_0(47, 39, 47) -> 4, k_0(47, 39, 46) -> 4, k_0(47, 39, 45) -> 4, k_0(47, 39, 44) -> 4, k_0(47, 39, 43) -> 4, k_0(47, 39, 42) -> 4, k_0(47, 39, 41) -> 4, k_0(47, 39, 40) -> 4, k_0(47, 39, 39) -> 4, k_0(47, 39, 38) -> 4, k_0(47, 39, 4) -> 4, k_0(47, 39, 3) -> 4, k_0(47, 39, 2) -> 4, k_0(47, 39, 1) -> 4, k_0(47, 39, 0) -> 4, k_0(47, 38, 47) -> 4, k_0(47, 38, 46) -> 4, k_0(47, 38, 45) -> 4, k_0(47, 38, 44) -> 4, k_0(47, 38, 43) -> 4, k_0(47, 38, 42) -> 4, k_0(47, 38, 41) -> 4, k_0(47, 38, 40) -> 4, k_0(47, 38, 39) -> 4, k_0(47, 38, 38) -> 4, k_0(47, 38, 4) -> 4, k_0(47, 38, 3) -> 4, k_0(47, 38, 2) -> 4, k_0(47, 38, 1) -> 4, k_0(47, 38, 0) -> 4, k_0(47, 4, 47) -> 4, k_0(47, 4, 46) -> 4, k_0(47, 4, 45) -> 4, k_0(47, 4, 44) -> 4, k_0(47, 4, 43) -> 4, k_0(47, 4, 42) -> 4, k_0(47, 4, 41) -> 4, k_0(47, 4, 40) -> 4, k_0(47, 4, 39) -> 4, k_0(47, 4, 38) -> 4, k_0(47, 4, 4) -> 4, k_0(47, 4, 3) -> 4, k_0(47, 4, 2) -> 4, k_0(47, 4, 1) -> 4, k_0(47, 4, 0) -> 4, k_0(47, 3, 47) -> 4, k_0(47, 3, 46) -> 4, k_0(47, 3, 45) -> 4, k_0(47, 3, 44) -> 4, k_0(47, 3, 43) -> 4, k_0(47, 3, 42) -> 4, k_0(47, 3, 41) -> 4, k_0(47, 3, 40) -> 4, k_0(47, 3, 39) -> 4, k_0(47, 3, 38) -> 4, k_0(47, 3, 4) -> 4, k_0(47, 3, 3) -> 4, k_0(47, 3, 2) -> 4, k_0(47, 3, 1) -> 4, k_0(47, 3, 0) -> 4, k_0(47, 2, 47) -> 4, k_0(47, 2, 46) -> 4, k_0(47, 2, 45) -> 4, k_0(47, 2, 44) -> 4, k_0(47, 2, 43) -> 4, k_0(47, 2, 42) -> 4, k_0(47, 2, 41) -> 4, k_0(47, 2, 40) -> 4, k_0(47, 2, 39) -> 4, k_0(47, 2, 38) -> 4, k_0(47, 2, 4) -> 4, k_0(47, 2, 3) -> 4, k_0(47, 2, 2) -> 4, k_0(47, 2, 1) -> 4, k_0(47, 2, 0) -> 4, k_0(47, 1, 47) -> 4, k_0(47, 1, 46) -> 4, k_0(47, 1, 45) -> 4, k_0(47, 1, 44) -> 4, k_0(47, 1, 43) -> 4, k_0(47, 1, 42) -> 4, k_0(47, 1, 41) -> 4, k_0(47, 1, 40) -> 4, k_0(47, 1, 39) -> 4, k_0(47, 1, 38) -> 4, k_0(47, 1, 4) -> 4, k_0(47, 1, 3) -> 4, k_0(47, 1, 2) -> 4, k_0(47, 1, 1) -> 4, k_0(47, 1, 0) -> 4, k_0(47, 0, 47) -> 4, k_0(47, 0, 46) -> 4, k_0(47, 0, 45) -> 4, k_0(47, 0, 44) -> 4, k_0(47, 0, 43) -> 4, k_0(47, 0, 42) -> 4, k_0(47, 0, 41) -> 4, k_0(47, 0, 40) -> 4, k_0(47, 0, 39) -> 4, k_0(47, 0, 38) -> 4, k_0(47, 0, 4) -> 4, k_0(47, 0, 3) -> 4, k_0(47, 0, 2) -> 4, k_0(47, 0, 1) -> 4, k_0(47, 0, 0) -> 4, k_0(46, 47, 47) -> 4, k_0(46, 47, 46) -> 4, k_0(46, 47, 45) -> 4, k_0(46, 47, 44) -> 4, k_0(46, 47, 43) -> 4, k_0(46, 47, 42) -> 4, k_0(46, 47, 41) -> 4, k_0(46, 47, 40) -> 4, k_0(46, 47, 39) -> 4, k_0(46, 47, 38) -> 4, k_0(46, 47, 4) -> 4, k_0(46, 47, 3) -> 4, k_0(46, 47, 2) -> 4, k_0(46, 47, 1) -> 4, k_0(46, 47, 0) -> 4, k_0(46, 46, 47) -> 4, k_0(46, 46, 46) -> 4, k_0(46, 46, 45) -> 4, k_0(46, 46, 44) -> 4, k_0(46, 46, 43) -> 4, k_0(46, 46, 42) -> 4, k_0(46, 46, 41) -> 4, k_0(46, 46, 40) -> 4, k_0(46, 46, 39) -> 4, k_0(46, 46, 38) -> 4, k_0(46, 46, 4) -> 4, k_0(46, 46, 3) -> 4, k_0(46, 46, 2) -> 4, k_0(46, 46, 1) -> 4, k_0(46, 46, 0) -> 4, k_0(46, 45, 47) -> 4, k_0(46, 45, 46) -> 4, k_0(46, 45, 45) -> 4, k_0(46, 45, 44) -> 4, k_0(46, 45, 43) -> 4, k_0(46, 45, 42) -> 4, k_0(46, 45, 41) -> 4, k_0(46, 45, 40) -> 4, k_0(46, 45, 39) -> 4, k_0(46, 45, 38) -> 4, k_0(46, 45, 4) -> 4, k_0(46, 45, 3) -> 4, k_0(46, 45, 2) -> 4, k_0(46, 45, 1) -> 4, k_0(46, 45, 0) -> 4, k_0(46, 44, 47) -> 4, k_0(46, 44, 46) -> 4, k_0(46, 44, 45) -> 4, k_0(46, 44, 44) -> 4, k_0(46, 44, 43) -> 4, k_0(46, 44, 42) -> 4, k_0(46, 44, 41) -> 4, k_0(46, 44, 40) -> 4, k_0(46, 44, 39) -> 4, k_0(46, 44, 38) -> 4, k_0(46, 44, 4) -> 4, k_0(46, 44, 3) -> 4, k_0(46, 44, 2) -> 4, k_0(46, 44, 1) -> 4, k_0(46, 44, 0) -> 4, k_0(46, 43, 47) -> 4, k_0(46, 43, 46) -> 4, k_0(46, 43, 45) -> 4, k_0(46, 43, 44) -> 4, k_0(46, 43, 43) -> 4, k_0(46, 43, 42) -> 4, k_0(46, 43, 41) -> 4, k_0(46, 43, 40) -> 4, k_0(46, 43, 39) -> 4, k_0(46, 43, 38) -> 4, k_0(46, 43, 4) -> 4, k_0(46, 43, 3) -> 4, k_0(46, 43, 2) -> 4, k_0(46, 43, 1) -> 4, k_0(46, 43, 0) -> 4, k_0(46, 42, 47) -> 4, k_0(46, 42, 46) -> 4, k_0(46, 42, 45) -> 4, k_0(46, 42, 44) -> 4, k_0(46, 42, 43) -> 4, k_0(46, 42, 42) -> 4, k_0(46, 42, 41) -> 4, k_0(46, 42, 40) -> 4, k_0(46, 42, 39) -> 4, k_0(46, 42, 38) -> 4, k_0(46, 42, 4) -> 4, k_0(46, 42, 3) -> 4, k_0(46, 42, 2) -> 4, k_0(46, 42, 1) -> 4, k_0(46, 42, 0) -> 4, k_0(46, 41, 47) -> 4, k_0(46, 41, 46) -> 4, k_0(46, 41, 45) -> 4, k_0(46, 41, 44) -> 4, k_0(46, 41, 43) -> 4, k_0(46, 41, 42) -> 4, k_0(46, 41, 41) -> 4, k_0(46, 41, 40) -> 4, k_0(46, 41, 39) -> 4, k_0(46, 41, 38) -> 4, k_0(46, 41, 4) -> 4, k_0(46, 41, 3) -> 4, k_0(46, 41, 2) -> 4, k_0(46, 41, 1) -> 4, k_0(46, 41, 0) -> 4, k_0(46, 40, 47) -> 4, k_0(46, 40, 46) -> 4, k_0(46, 40, 45) -> 4, k_0(46, 40, 44) -> 4, k_0(46, 40, 43) -> 4, k_0(46, 40, 42) -> 4, k_0(46, 40, 41) -> 4, k_0(46, 40, 40) -> 4, k_0(46, 40, 39) -> 4, k_0(46, 40, 38) -> 4, k_0(46, 40, 4) -> 4, k_0(46, 40, 3) -> 4, k_0(46, 40, 2) -> 4, k_0(46, 40, 1) -> 4, k_0(46, 40, 0) -> 4, k_0(46, 39, 47) -> 4, k_0(46, 39, 46) -> 4, k_0(46, 39, 45) -> 4, k_0(46, 39, 44) -> 4, k_0(46, 39, 43) -> 4, k_0(46, 39, 42) -> 4, k_0(46, 39, 41) -> 4, k_0(46, 39, 40) -> 4, k_0(46, 39, 39) -> 4, k_0(46, 39, 38) -> 4, k_0(46, 39, 4) -> 4, k_0(46, 39, 3) -> 4, k_0(46, 39, 2) -> 4, k_0(46, 39, 1) -> 4, k_0(46, 39, 0) -> 4, k_0(46, 38, 47) -> 4, k_0(46, 38, 46) -> 4, k_0(46, 38, 45) -> 4, k_0(46, 38, 44) -> 4, k_0(46, 38, 43) -> 4, k_0(46, 38, 42) -> 4, k_0(46, 38, 41) -> 4, k_0(46, 38, 40) -> 4, k_0(46, 38, 39) -> 4, k_0(46, 38, 38) -> 4, k_0(46, 38, 4) -> 4, k_0(46, 38, 3) -> 4, k_0(46, 38, 2) -> 4, k_0(46, 38, 1) -> 4, k_0(46, 38, 0) -> 4, k_0(46, 4, 47) -> 4, k_0(46, 4, 46) -> 4, k_0(46, 4, 45) -> 4, k_0(46, 4, 44) -> 4, k_0(46, 4, 43) -> 4, k_0(46, 4, 42) -> 4, k_0(46, 4, 41) -> 4, k_0(46, 4, 40) -> 4, k_0(46, 4, 39) -> 4, k_0(46, 4, 38) -> 4, k_0(46, 4, 4) -> 4, k_0(46, 4, 3) -> 4, k_0(46, 4, 2) -> 4, k_0(46, 4, 1) -> 4, k_0(46, 4, 0) -> 4, k_0(46, 3, 47) -> 4, k_0(46, 3, 46) -> 4, k_0(46, 3, 45) -> 4, k_0(46, 3, 44) -> 4, k_0(46, 3, 43) -> 4, k_0(46, 3, 42) -> 4, k_0(46, 3, 41) -> 4, k_0(46, 3, 40) -> 4, k_0(46, 3, 39) -> 4, k_0(46, 3, 38) -> 4, k_0(46, 3, 4) -> 4, k_0(46, 3, 3) -> 4, k_0(46, 3, 2) -> 4, k_0(46, 3, 1) -> 4, k_0(46, 3, 0) -> 4, k_0(46, 2, 47) -> 4, k_0(46, 2, 46) -> 4, k_0(46, 2, 45) -> 4, k_0(46, 2, 44) -> 4, k_0(46, 2, 43) -> 4, k_0(46, 2, 42) -> 4, k_0(46, 2, 41) -> 4, k_0(46, 2, 40) -> 4, k_0(46, 2, 39) -> 4, k_0(46, 2, 38) -> 4, k_0(46, 2, 4) -> 4, k_0(46, 2, 3) -> 4, k_0(46, 2, 2) -> 4, k_0(46, 2, 1) -> 4, k_0(46, 2, 0) -> 4, k_0(46, 1, 47) -> 4, k_0(46, 1, 46) -> 4, k_0(46, 1, 45) -> 4, k_0(46, 1, 44) -> 4, k_0(46, 1, 43) -> 4, k_0(46, 1, 42) -> 4, k_0(46, 1, 41) -> 4, k_0(46, 1, 40) -> 4, k_0(46, 1, 39) -> 4, k_0(46, 1, 38) -> 4, k_0(46, 1, 4) -> 4, k_0(46, 1, 3) -> 4, k_0(46, 1, 2) -> 4, k_0(46, 1, 1) -> 4, k_0(46, 1, 0) -> 4, k_0(46, 0, 47) -> 4, k_0(46, 0, 46) -> 4, k_0(46, 0, 45) -> 4, k_0(46, 0, 44) -> 4, k_0(46, 0, 43) -> 4, k_0(46, 0, 42) -> 4, k_0(46, 0, 41) -> 4, k_0(46, 0, 40) -> 4, k_0(46, 0, 39) -> 4, k_0(46, 0, 38) -> 4, k_0(46, 0, 4) -> 4, k_0(46, 0, 3) -> 4, k_0(46, 0, 2) -> 4, k_0(46, 0, 1) -> 4, k_0(46, 0, 0) -> 4, k_0(45, 47, 47) -> 4, k_0(45, 47, 46) -> 4, k_0(45, 47, 45) -> 4, k_0(45, 47, 44) -> 4, k_0(45, 47, 43) -> 4, k_0(45, 47, 42) -> 4, k_0(45, 47, 41) -> 4, k_0(45, 47, 40) -> 4, k_0(45, 47, 39) -> 4, k_0(45, 47, 38) -> 4, k_0(45, 47, 4) -> 4, k_0(45, 47, 3) -> 4, k_0(45, 47, 2) -> 4, k_0(45, 47, 1) -> 4, k_0(45, 47, 0) -> 4, k_0(45, 46, 47) -> 4, k_0(45, 46, 46) -> 4, k_0(45, 46, 45) -> 4, k_0(45, 46, 44) -> 4, k_0(45, 46, 43) -> 4, k_0(45, 46, 42) -> 4, k_0(45, 46, 41) -> 4, k_0(45, 46, 40) -> 4, k_0(45, 46, 39) -> 4, k_0(45, 46, 38) -> 4, k_0(45, 46, 4) -> 4, k_0(45, 46, 3) -> 4, k_0(45, 46, 2) -> 4, k_0(45, 46, 1) -> 4, k_0(45, 46, 0) -> 4, k_0(45, 45, 47) -> 4, k_0(45, 45, 46) -> 4, k_0(45, 45, 45) -> 4, k_0(45, 45, 44) -> 4, k_0(45, 45, 43) -> 4, k_0(45, 45, 42) -> 4, k_0(45, 45, 41) -> 4, k_0(45, 45, 40) -> 4, k_0(45, 45, 39) -> 4, k_0(45, 45, 38) -> 4, k_0(45, 45, 4) -> 4, k_0(45, 45, 3) -> 4, k_0(45, 45, 2) -> 4, k_0(45, 45, 1) -> 4, k_0(45, 45, 0) -> 4, k_0(45, 44, 47) -> 4, k_0(45, 44, 46) -> 4, k_0(45, 44, 45) -> 4, k_0(45, 44, 44) -> 4, k_0(45, 44, 43) -> 4, k_0(45, 44, 42) -> 4, k_0(45, 44, 41) -> 4, k_0(45, 44, 40) -> 4, k_0(45, 44, 39) -> 4, k_0(45, 44, 38) -> 4, k_0(45, 44, 4) -> 4, k_0(45, 44, 3) -> 4, k_0(45, 44, 2) -> 4, k_0(45, 44, 1) -> 4, k_0(45, 44, 0) -> 4, k_0(45, 43, 47) -> 4, k_0(45, 43, 46) -> 4, k_0(45, 43, 45) -> 4, k_0(45, 43, 44) -> 4, k_0(45, 43, 43) -> 4, k_0(45, 43, 42) -> 4, k_0(45, 43, 41) -> 4, k_0(45, 43, 40) -> 4, k_0(45, 43, 39) -> 4, k_0(45, 43, 38) -> 4, k_0(45, 43, 4) -> 4, k_0(45, 43, 3) -> 4, k_0(45, 43, 2) -> 4, k_0(45, 43, 1) -> 4, k_0(45, 43, 0) -> 4, k_0(45, 42, 47) -> 4, k_0(45, 42, 46) -> 4, k_0(45, 42, 45) -> 4, k_0(45, 42, 44) -> 4, k_0(45, 42, 43) -> 4, k_0(45, 42, 42) -> 4, k_0(45, 42, 41) -> 4, k_0(45, 42, 40) -> 4, k_0(45, 42, 39) -> 4, k_0(45, 42, 38) -> 4, k_0(45, 42, 4) -> 4, k_0(45, 42, 3) -> 4, k_0(45, 42, 2) -> 4, k_0(45, 42, 1) -> 4, k_0(45, 42, 0) -> 4, k_0(45, 41, 47) -> 4, k_0(45, 41, 46) -> 4, k_0(45, 41, 45) -> 4, k_0(45, 41, 44) -> 4, k_0(45, 41, 43) -> 4, k_0(45, 41, 42) -> 4, k_0(45, 41, 41) -> 4, k_0(45, 41, 40) -> 4, k_0(45, 41, 39) -> 4, k_0(45, 41, 38) -> 4, k_0(45, 41, 4) -> 4, k_0(45, 41, 3) -> 4, k_0(45, 41, 2) -> 4, k_0(45, 41, 1) -> 4, k_0(45, 41, 0) -> 4, k_0(45, 40, 47) -> 4, k_0(45, 40, 46) -> 4, k_0(45, 40, 45) -> 4, k_0(45, 40, 44) -> 4, k_0(45, 40, 43) -> 4, k_0(45, 40, 42) -> 4, k_0(45, 40, 41) -> 4, k_0(45, 40, 40) -> 4, k_0(45, 40, 39) -> 4, k_0(45, 40, 38) -> 4, k_0(45, 40, 4) -> 4, k_0(45, 40, 3) -> 4, k_0(45, 40, 2) -> 4, k_0(45, 40, 1) -> 4, k_0(45, 40, 0) -> 4, k_0(45, 39, 47) -> 4, k_0(45, 39, 46) -> 4, k_0(45, 39, 45) -> 4, k_0(45, 39, 44) -> 4, k_0(45, 39, 43) -> 4, k_0(45, 39, 42) -> 4, k_0(45, 39, 41) -> 4, k_0(45, 39, 40) -> 4, k_0(45, 39, 39) -> 4, k_0(45, 39, 38) -> 4, k_0(45, 39, 4) -> 4, k_0(45, 39, 3) -> 4, k_0(45, 39, 2) -> 4, k_0(45, 39, 1) -> 4, k_0(45, 39, 0) -> 4, k_0(45, 38, 47) -> 4, k_0(45, 38, 46) -> 4, k_0(45, 38, 45) -> 4, k_0(45, 38, 44) -> 4, k_0(45, 38, 43) -> 4, k_0(45, 38, 42) -> 4, k_0(45, 38, 41) -> 4, k_0(45, 38, 40) -> 4, k_0(45, 38, 39) -> 4, k_0(45, 38, 38) -> 4, k_0(45, 38, 4) -> 4, k_0(45, 38, 3) -> 4, k_0(45, 38, 2) -> 4, k_0(45, 38, 1) -> 4, k_0(45, 38, 0) -> 4, k_0(45, 4, 47) -> 4, k_0(45, 4, 46) -> 4, k_0(45, 4, 45) -> 4, k_0(45, 4, 44) -> 4, k_0(45, 4, 43) -> 4, k_0(45, 4, 42) -> 4, k_0(45, 4, 41) -> 4, k_0(45, 4, 40) -> 4, k_0(45, 4, 39) -> 4, k_0(45, 4, 38) -> 4, k_0(45, 4, 4) -> 4, k_0(45, 4, 3) -> 4, k_0(45, 4, 2) -> 4, k_0(45, 4, 1) -> 4, k_0(45, 4, 0) -> 4, k_0(45, 3, 47) -> 4, k_0(45, 3, 46) -> 4, k_0(45, 3, 45) -> 4, k_0(45, 3, 44) -> 4, k_0(45, 3, 43) -> 4, k_0(45, 3, 42) -> 4, k_0(45, 3, 41) -> 4, k_0(45, 3, 40) -> 4, k_0(45, 3, 39) -> 4, k_0(45, 3, 38) -> 4, k_0(45, 3, 4) -> 4, k_0(45, 3, 3) -> 4, k_0(45, 3, 2) -> 4, k_0(45, 3, 1) -> 4, k_0(45, 3, 0) -> 4, k_0(45, 2, 47) -> 4, k_0(45, 2, 46) -> 4, k_0(45, 2, 45) -> 4, k_0(45, 2, 44) -> 4, k_0(45, 2, 43) -> 4, k_0(45, 2, 42) -> 4, k_0(45, 2, 41) -> 4, k_0(45, 2, 40) -> 4, k_0(45, 2, 39) -> 4, k_0(45, 2, 38) -> 4, k_0(45, 2, 4) -> 4, k_0(45, 2, 3) -> 4, k_0(45, 2, 2) -> 4, k_0(45, 2, 1) -> 4, k_0(45, 2, 0) -> 4, k_0(45, 1, 47) -> 4, k_0(45, 1, 46) -> 4, k_0(45, 1, 45) -> 4, k_0(45, 1, 44) -> 4, k_0(45, 1, 43) -> 4, k_0(45, 1, 42) -> 4, k_0(45, 1, 41) -> 4, k_0(45, 1, 40) -> 4, k_0(45, 1, 39) -> 4, k_0(45, 1, 38) -> 4, k_0(45, 1, 4) -> 4, k_0(45, 1, 3) -> 4, k_0(45, 1, 2) -> 4, k_0(45, 1, 1) -> 4, k_0(45, 1, 0) -> 4, k_0(45, 0, 47) -> 4, k_0(45, 0, 46) -> 4, k_0(45, 0, 45) -> 4, k_0(45, 0, 44) -> 4, k_0(45, 0, 43) -> 4, k_0(45, 0, 42) -> 4, k_0(45, 0, 41) -> 4, k_0(45, 0, 40) -> 4, k_0(45, 0, 39) -> 4, k_0(45, 0, 38) -> 4, k_0(45, 0, 4) -> 4, k_0(45, 0, 3) -> 4, k_0(45, 0, 2) -> 4, k_0(45, 0, 1) -> 4, k_0(45, 0, 0) -> 4, k_0(44, 47, 47) -> 4, k_0(44, 47, 46) -> 4, k_0(44, 47, 45) -> 4, k_0(44, 47, 44) -> 4, k_0(44, 47, 43) -> 4, k_0(44, 47, 42) -> 4, k_0(44, 47, 41) -> 4, k_0(44, 47, 40) -> 4, k_0(44, 47, 39) -> 4, k_0(44, 47, 38) -> 4, k_0(44, 47, 4) -> 4, k_0(44, 47, 3) -> 4, k_0(44, 47, 2) -> 4, k_0(44, 47, 1) -> 4, k_0(44, 47, 0) -> 4, k_0(44, 46, 47) -> 4, k_0(44, 46, 46) -> 4, k_0(44, 46, 45) -> 4, k_0(44, 46, 44) -> 4, k_0(44, 46, 43) -> 4, k_0(44, 46, 42) -> 4, k_0(44, 46, 41) -> 4, k_0(44, 46, 40) -> 4, k_0(44, 46, 39) -> 4, k_0(44, 46, 38) -> 4, k_0(44, 46, 4) -> 4, k_0(44, 46, 3) -> 4, k_0(44, 46, 2) -> 4, k_0(44, 46, 1) -> 4, k_0(44, 46, 0) -> 4, k_0(44, 45, 47) -> 4, k_0(44, 45, 46) -> 4, k_0(44, 45, 45) -> 4, k_0(44, 45, 44) -> 4, k_0(44, 45, 43) -> 4, k_0(44, 45, 42) -> 4, k_0(44, 45, 41) -> 4, k_0(44, 45, 40) -> 4, k_0(44, 45, 39) -> 4, k_0(44, 45, 38) -> 4, k_0(44, 45, 4) -> 4, k_0(44, 45, 3) -> 4, k_0(44, 45, 2) -> 4, k_0(44, 45, 1) -> 4, k_0(44, 45, 0) -> 4, k_0(44, 44, 47) -> 4, k_0(44, 44, 46) -> 4, k_0(44, 44, 45) -> 4, k_0(44, 44, 44) -> 4, k_0(44, 44, 43) -> 4, k_0(44, 44, 42) -> 4, k_0(44, 44, 41) -> 4, k_0(44, 44, 40) -> 4, k_0(44, 44, 39) -> 4, k_0(44, 44, 38) -> 4, k_0(44, 44, 4) -> 4, k_0(44, 44, 3) -> 4, k_0(44, 44, 2) -> 4, k_0(44, 44, 1) -> 4, k_0(44, 44, 0) -> 4, k_0(44, 43, 47) -> 4, k_0(44, 43, 46) -> 4, k_0(44, 43, 45) -> 4, k_0(44, 43, 44) -> 4, k_0(44, 43, 43) -> 4, k_0(44, 43, 42) -> 4, k_0(44, 43, 41) -> 4, k_0(44, 43, 40) -> 4, k_0(44, 43, 39) -> 4, k_0(44, 43, 38) -> 4, k_0(44, 43, 4) -> 4, k_0(44, 43, 3) -> 4, k_0(44, 43, 2) -> 4, k_0(44, 43, 1) -> 4, k_0(44, 43, 0) -> 4, k_0(44, 42, 47) -> 4, k_0(44, 42, 46) -> 4, k_0(44, 42, 45) -> 4, k_0(44, 42, 44) -> 4, k_0(44, 42, 43) -> 4, k_0(44, 42, 42) -> 4, k_0(44, 42, 41) -> 4, k_0(44, 42, 40) -> 4, k_0(44, 42, 39) -> 4, k_0(44, 42, 38) -> 4, k_0(44, 42, 4) -> 4, k_0(44, 42, 3) -> 4, k_0(44, 42, 2) -> 4, k_0(44, 42, 1) -> 4, k_0(44, 42, 0) -> 4, k_0(44, 41, 47) -> 4, k_0(44, 41, 46) -> 4, k_0(44, 41, 45) -> 4, k_0(44, 41, 44) -> 4, k_0(44, 41, 43) -> 4, k_0(44, 41, 42) -> 4, k_0(44, 41, 41) -> 4, k_0(44, 41, 40) -> 4, k_0(44, 41, 39) -> 4, k_0(44, 41, 38) -> 4, k_0(44, 41, 4) -> 4, k_0(44, 41, 3) -> 4, k_0(44, 41, 2) -> 4, k_0(44, 41, 1) -> 4, k_0(44, 41, 0) -> 4, k_0(44, 40, 47) -> 4, k_0(44, 40, 46) -> 4, k_0(44, 40, 45) -> 4, k_0(44, 40, 44) -> 4, k_0(44, 40, 43) -> 4, k_0(44, 40, 42) -> 4, k_0(44, 40, 41) -> 4, k_0(44, 40, 40) -> 4, k_0(44, 40, 39) -> 4, k_0(44, 40, 38) -> 4, k_0(44, 40, 4) -> 4, k_0(44, 40, 3) -> 4, k_0(44, 40, 2) -> 4, k_0(44, 40, 1) -> 4, k_0(44, 40, 0) -> 4, k_0(44, 39, 47) -> 4, k_0(44, 39, 46) -> 4, k_0(44, 39, 45) -> 4, k_0(44, 39, 44) -> 4, k_0(44, 39, 43) -> 4, k_0(44, 39, 42) -> 4, k_0(44, 39, 41) -> 4, k_0(44, 39, 40) -> 4, k_0(44, 39, 39) -> 4, k_0(44, 39, 38) -> 4, k_0(44, 39, 4) -> 4, k_0(44, 39, 3) -> 4, k_0(44, 39, 2) -> 4, k_0(44, 39, 1) -> 4, k_0(44, 39, 0) -> 4, k_0(44, 38, 47) -> 4, k_0(44, 38, 46) -> 4, k_0(44, 38, 45) -> 4, k_0(44, 38, 44) -> 4, k_0(44, 38, 43) -> 4, k_0(44, 38, 42) -> 4, k_0(44, 38, 41) -> 4, k_0(44, 38, 40) -> 4, k_0(44, 38, 39) -> 4, k_0(44, 38, 38) -> 4, k_0(44, 38, 4) -> 4, k_0(44, 38, 3) -> 4, k_0(44, 38, 2) -> 4, k_0(44, 38, 1) -> 4, k_0(44, 38, 0) -> 4, k_0(44, 4, 47) -> 4, k_0(44, 4, 46) -> 4, k_0(44, 4, 45) -> 4, k_0(44, 4, 44) -> 4, k_0(44, 4, 43) -> 4, k_0(44, 4, 42) -> 4, k_0(44, 4, 41) -> 4, k_0(44, 4, 40) -> 4, k_0(44, 4, 39) -> 4, k_0(44, 4, 38) -> 4, k_0(44, 4, 4) -> 4, k_0(44, 4, 3) -> 4, k_0(44, 4, 2) -> 4, k_0(44, 4, 1) -> 4, k_0(44, 4, 0) -> 4, k_0(44, 3, 47) -> 4, k_0(44, 3, 46) -> 4, k_0(44, 3, 45) -> 4, k_0(44, 3, 44) -> 4, k_0(44, 3, 43) -> 4, k_0(44, 3, 42) -> 4, k_0(44, 3, 41) -> 4, k_0(44, 3, 40) -> 4, k_0(44, 3, 39) -> 4, k_0(44, 3, 38) -> 4, k_0(44, 3, 4) -> 4, k_0(44, 3, 3) -> 4, k_0(44, 3, 2) -> 4, k_0(44, 3, 1) -> 4, k_0(44, 3, 0) -> 4, k_0(44, 2, 47) -> 4, k_0(44, 2, 46) -> 4, k_0(44, 2, 45) -> 4, k_0(44, 2, 44) -> 4, k_0(44, 2, 43) -> 4, k_0(44, 2, 42) -> 4, k_0(44, 2, 41) -> 4, k_0(44, 2, 40) -> 4, k_0(44, 2, 39) -> 4, k_0(44, 2, 38) -> 4, k_0(44, 2, 4) -> 4, k_0(44, 2, 3) -> 4, k_0(44, 2, 2) -> 4, k_0(44, 2, 1) -> 4, k_0(44, 2, 0) -> 4, k_0(44, 1, 47) -> 4, k_0(44, 1, 46) -> 4, k_0(44, 1, 45) -> 4, k_0(44, 1, 44) -> 4, k_0(44, 1, 43) -> 4, k_0(44, 1, 42) -> 4, k_0(44, 1, 41) -> 4, k_0(44, 1, 40) -> 4, k_0(44, 1, 39) -> 4, k_0(44, 1, 38) -> 4, k_0(44, 1, 4) -> 4, k_0(44, 1, 3) -> 4, k_0(44, 1, 2) -> 4, k_0(44, 1, 1) -> 4, k_0(44, 1, 0) -> 4, k_0(44, 0, 47) -> 4, k_0(44, 0, 46) -> 4, k_0(44, 0, 45) -> 4, k_0(44, 0, 44) -> 4, k_0(44, 0, 43) -> 4, k_0(44, 0, 42) -> 4, k_0(44, 0, 41) -> 4, k_0(44, 0, 40) -> 4, k_0(44, 0, 39) -> 4, k_0(44, 0, 38) -> 4, k_0(44, 0, 4) -> 4, k_0(44, 0, 3) -> 4, k_0(44, 0, 2) -> 4, k_0(44, 0, 1) -> 4, k_0(44, 0, 0) -> 4, k_0(43, 47, 47) -> 4, k_0(43, 47, 46) -> 4, k_0(43, 47, 45) -> 4, k_0(43, 47, 44) -> 4, k_0(43, 47, 43) -> 4, k_0(43, 47, 42) -> 4, k_0(43, 47, 41) -> 4, k_0(43, 47, 40) -> 4, k_0(43, 47, 39) -> 4, k_0(43, 47, 38) -> 4, k_0(43, 47, 4) -> 4, k_0(43, 47, 3) -> 4, k_0(43, 47, 2) -> 4, k_0(43, 47, 1) -> 4, k_0(43, 47, 0) -> 4, k_0(43, 46, 47) -> 4, k_0(43, 46, 46) -> 4, k_0(43, 46, 45) -> 4, k_0(43, 46, 44) -> 4, k_0(43, 46, 43) -> 4, k_0(43, 46, 42) -> 4, k_0(43, 46, 41) -> 4, k_0(43, 46, 40) -> 4, k_0(43, 46, 39) -> 4, k_0(43, 46, 38) -> 4, k_0(43, 46, 4) -> 4, k_0(43, 46, 3) -> 4, k_0(43, 46, 2) -> 4, k_0(43, 46, 1) -> 4, k_0(43, 46, 0) -> 4, k_0(43, 45, 47) -> 4, k_0(43, 45, 46) -> 4, k_0(43, 45, 45) -> 4, k_0(43, 45, 44) -> 4, k_0(43, 45, 43) -> 4, k_0(43, 45, 42) -> 4, k_0(43, 45, 41) -> 4, k_0(43, 45, 40) -> 4, k_0(43, 45, 39) -> 4, k_0(43, 45, 38) -> 4, k_0(43, 45, 4) -> 4, k_0(43, 45, 3) -> 4, k_0(43, 45, 2) -> 4, k_0(43, 45, 1) -> 4, k_0(43, 45, 0) -> 4, k_0(43, 44, 47) -> 4, k_0(43, 44, 46) -> 4, k_0(43, 44, 45) -> 4, k_0(43, 44, 44) -> 4, k_0(43, 44, 43) -> 4, k_0(43, 44, 42) -> 4, k_0(43, 44, 41) -> 4, k_0(43, 44, 40) -> 4, k_0(43, 44, 39) -> 4, k_0(43, 44, 38) -> 4, k_0(43, 44, 4) -> 4, k_0(43, 44, 3) -> 4, k_0(43, 44, 2) -> 4, k_0(43, 44, 1) -> 4, k_0(43, 44, 0) -> 4, k_0(43, 43, 47) -> 4, k_0(43, 43, 46) -> 4, k_0(43, 43, 45) -> 4, k_0(43, 43, 44) -> 4, k_0(43, 43, 43) -> 4, k_0(43, 43, 42) -> 4, k_0(43, 43, 41) -> 4, k_0(43, 43, 40) -> 4, k_0(43, 43, 39) -> 4, k_0(43, 43, 38) -> 4, k_0(43, 43, 4) -> 4, k_0(43, 43, 3) -> 4, k_0(43, 43, 2) -> 4, k_0(43, 43, 1) -> 4, k_0(43, 43, 0) -> 4, k_0(43, 42, 47) -> 4, k_0(43, 42, 46) -> 4, k_0(43, 42, 45) -> 4, k_0(43, 42, 44) -> 4, k_0(43, 42, 43) -> 4, k_0(43, 42, 42) -> 4, k_0(43, 42, 41) -> 4, k_0(43, 42, 40) -> 4, k_0(43, 42, 39) -> 4, k_0(43, 42, 38) -> 4, k_0(43, 42, 4) -> 4, k_0(43, 42, 3) -> 4, k_0(43, 42, 2) -> 4, k_0(43, 42, 1) -> 4, k_0(43, 42, 0) -> 4, k_0(43, 41, 47) -> 4, k_0(43, 41, 46) -> 4, k_0(43, 41, 45) -> 4, k_0(43, 41, 44) -> 4, k_0(43, 41, 43) -> 4, k_0(43, 41, 42) -> 4, k_0(43, 41, 41) -> 4, k_0(43, 41, 40) -> 4, k_0(43, 41, 39) -> 4, k_0(43, 41, 38) -> 4, k_0(43, 41, 4) -> 4, k_0(43, 41, 3) -> 4, k_0(43, 41, 2) -> 4, k_0(43, 41, 1) -> 4, k_0(43, 41, 0) -> 4, k_0(43, 40, 47) -> 4, k_0(43, 40, 46) -> 4, k_0(43, 40, 45) -> 4, k_0(43, 40, 44) -> 4, k_0(43, 40, 43) -> 4, k_0(43, 40, 42) -> 4, k_0(43, 40, 41) -> 4, k_0(43, 40, 40) -> 4, k_0(43, 40, 39) -> 4, k_0(43, 40, 38) -> 4, k_0(43, 40, 4) -> 4, k_0(43, 40, 3) -> 4, k_0(43, 40, 2) -> 4, k_0(43, 40, 1) -> 4, k_0(43, 40, 0) -> 4, k_0(43, 39, 47) -> 4, k_0(43, 39, 46) -> 4, k_0(43, 39, 45) -> 4, k_0(43, 39, 44) -> 4, k_0(43, 39, 43) -> 4, k_0(43, 39, 42) -> 4, k_0(43, 39, 41) -> 4, k_0(43, 39, 40) -> 4, k_0(43, 39, 39) -> 4, k_0(43, 39, 38) -> 4, k_0(43, 39, 4) -> 4, k_0(43, 39, 3) -> 4, k_0(43, 39, 2) -> 4, k_0(43, 39, 1) -> 4, k_0(43, 39, 0) -> 4, k_0(43, 38, 47) -> 4, k_0(43, 38, 46) -> 4, k_0(43, 38, 45) -> 4, k_0(43, 38, 44) -> 4, k_0(43, 38, 43) -> 4, k_0(43, 38, 42) -> 4, k_0(43, 38, 41) -> 4, k_0(43, 38, 40) -> 4, k_0(43, 38, 39) -> 4, k_0(43, 38, 38) -> 4, k_0(43, 38, 4) -> 4, k_0(43, 38, 3) -> 4, k_0(43, 38, 2) -> 4, k_0(43, 38, 1) -> 4, k_0(43, 38, 0) -> 4, k_0(43, 4, 47) -> 4, k_0(43, 4, 46) -> 4, k_0(43, 4, 45) -> 4, k_0(43, 4, 44) -> 4, k_0(43, 4, 43) -> 4, k_0(43, 4, 42) -> 4, k_0(43, 4, 41) -> 4, k_0(43, 4, 40) -> 4, k_0(43, 4, 39) -> 4, k_0(43, 4, 38) -> 4, k_0(43, 4, 4) -> 4, k_0(43, 4, 3) -> 4, k_0(43, 4, 2) -> 4, k_0(43, 4, 1) -> 4, k_0(43, 4, 0) -> 4, k_0(43, 3, 47) -> 4, k_0(43, 3, 46) -> 4, k_0(43, 3, 45) -> 4, k_0(43, 3, 44) -> 4, k_0(43, 3, 43) -> 4, k_0(43, 3, 42) -> 4, k_0(43, 3, 41) -> 4, k_0(43, 3, 40) -> 4, k_0(43, 3, 39) -> 4, k_0(43, 3, 38) -> 4, k_0(43, 3, 4) -> 4, k_0(43, 3, 3) -> 4, k_0(43, 3, 2) -> 4, k_0(43, 3, 1) -> 4, k_0(43, 3, 0) -> 4, k_0(43, 2, 47) -> 4, k_0(43, 2, 46) -> 4, k_0(43, 2, 45) -> 4, k_0(43, 2, 44) -> 4, k_0(43, 2, 43) -> 4, k_0(43, 2, 42) -> 4, k_0(43, 2, 41) -> 4, k_0(43, 2, 40) -> 4, k_0(43, 2, 39) -> 4, k_0(43, 2, 38) -> 4, k_0(43, 2, 4) -> 4, k_0(43, 2, 3) -> 4, k_0(43, 2, 2) -> 4, k_0(43, 2, 1) -> 4, k_0(43, 2, 0) -> 4, k_0(43, 1, 47) -> 4, k_0(43, 1, 46) -> 4, k_0(43, 1, 45) -> 4, k_0(43, 1, 44) -> 4, k_0(43, 1, 43) -> 4, k_0(43, 1, 42) -> 4, k_0(43, 1, 41) -> 4, k_0(43, 1, 40) -> 4, k_0(43, 1, 39) -> 4, k_0(43, 1, 38) -> 4, k_0(43, 1, 4) -> 4, k_0(43, 1, 3) -> 4, k_0(43, 1, 2) -> 4, k_0(43, 1, 1) -> 4, k_0(43, 1, 0) -> 4, k_0(43, 0, 47) -> 4, k_0(43, 0, 46) -> 4, k_0(43, 0, 45) -> 4, k_0(43, 0, 44) -> 4, k_0(43, 0, 43) -> 4, k_0(43, 0, 42) -> 4, k_0(43, 0, 41) -> 4, k_0(43, 0, 40) -> 4, k_0(43, 0, 39) -> 4, k_0(43, 0, 38) -> 4, k_0(43, 0, 4) -> 4, k_0(43, 0, 3) -> 4, k_0(43, 0, 2) -> 4, k_0(43, 0, 1) -> 4, k_0(43, 0, 0) -> 4, k_0(42, 47, 47) -> 4, k_0(42, 47, 46) -> 4, k_0(42, 47, 45) -> 4, k_0(42, 47, 44) -> 4, k_0(42, 47, 43) -> 4, k_0(42, 47, 42) -> 4, k_0(42, 47, 41) -> 4, k_0(42, 47, 40) -> 4, k_0(42, 47, 39) -> 4, k_0(42, 47, 38) -> 4, k_0(42, 47, 4) -> 4, k_0(42, 47, 3) -> 4, k_0(42, 47, 2) -> 4, k_0(42, 47, 1) -> 4, k_0(42, 47, 0) -> 4, k_0(42, 46, 47) -> 4, k_0(42, 46, 46) -> 4, k_0(42, 46, 45) -> 4, k_0(42, 46, 44) -> 4, k_0(42, 46, 43) -> 4, k_0(42, 46, 42) -> 4, k_0(42, 46, 41) -> 4, k_0(42, 46, 40) -> 4, k_0(42, 46, 39) -> 4, k_0(42, 46, 38) -> 4, k_0(42, 46, 4) -> 4, k_0(42, 46, 3) -> 4, k_0(42, 46, 2) -> 4, k_0(42, 46, 1) -> 4, k_0(42, 46, 0) -> 4, k_0(42, 45, 47) -> 4, k_0(42, 45, 46) -> 4, k_0(42, 45, 45) -> 4, k_0(42, 45, 44) -> 4, k_0(42, 45, 43) -> 4, k_0(42, 45, 42) -> 4, k_0(42, 45, 41) -> 4, k_0(42, 45, 40) -> 4, k_0(42, 45, 39) -> 4, k_0(42, 45, 38) -> 4, k_0(42, 45, 4) -> 4, k_0(42, 45, 3) -> 4, k_0(42, 45, 2) -> 4, k_0(42, 45, 1) -> 4, k_0(42, 45, 0) -> 4, k_0(42, 44, 47) -> 4, k_0(42, 44, 46) -> 4, k_0(42, 44, 45) -> 4, k_0(42, 44, 44) -> 4, k_0(42, 44, 43) -> 4, k_0(42, 44, 42) -> 4, k_0(42, 44, 41) -> 4, k_0(42, 44, 40) -> 4, k_0(42, 44, 39) -> 4, k_0(42, 44, 38) -> 4, k_0(42, 44, 4) -> 4, k_0(42, 44, 3) -> 4, k_0(42, 44, 2) -> 4, k_0(42, 44, 1) -> 4, k_0(42, 44, 0) -> 4, k_0(42, 43, 47) -> 4, k_0(42, 43, 46) -> 4, k_0(42, 43, 45) -> 4, k_0(42, 43, 44) -> 4, k_0(42, 43, 43) -> 4, k_0(42, 43, 42) -> 4, k_0(42, 43, 41) -> 4, k_0(42, 43, 40) -> 4, k_0(42, 43, 39) -> 4, k_0(42, 43, 38) -> 4, k_0(42, 43, 4) -> 4, k_0(42, 43, 3) -> 4, k_0(42, 43, 2) -> 4, k_0(42, 43, 1) -> 4, k_0(42, 43, 0) -> 4, k_0(42, 42, 47) -> 4, k_0(42, 42, 46) -> 4, k_0(42, 42, 45) -> 4, k_0(42, 42, 44) -> 4, k_0(42, 42, 43) -> 4, k_0(42, 42, 42) -> 4, k_0(42, 42, 41) -> 4, k_0(42, 42, 40) -> 4, k_0(42, 42, 39) -> 4, k_0(42, 42, 38) -> 4, k_0(42, 42, 4) -> 4, k_0(42, 42, 3) -> 4, k_0(42, 42, 2) -> 4, k_0(42, 42, 1) -> 4, k_0(42, 42, 0) -> 4, k_0(42, 41, 47) -> 4, k_0(42, 41, 46) -> 4, k_0(42, 41, 45) -> 4, k_0(42, 41, 44) -> 4, k_0(42, 41, 43) -> 4, k_0(42, 41, 42) -> 4, k_0(42, 41, 41) -> 4, k_0(42, 41, 40) -> 4, k_0(42, 41, 39) -> 4, k_0(42, 41, 38) -> 4, k_0(42, 41, 4) -> 4, k_0(42, 41, 3) -> 4, k_0(42, 41, 2) -> 4, k_0(42, 41, 1) -> 4, k_0(42, 41, 0) -> 4, k_0(42, 40, 47) -> 4, k_0(42, 40, 46) -> 4, k_0(42, 40, 45) -> 4, k_0(42, 40, 44) -> 4, k_0(42, 40, 43) -> 4, k_0(42, 40, 42) -> 4, k_0(42, 40, 41) -> 4, k_0(42, 40, 40) -> 4, k_0(42, 40, 39) -> 4, k_0(42, 40, 38) -> 4, k_0(42, 40, 4) -> 4, k_0(42, 40, 3) -> 4, k_0(42, 40, 2) -> 4, k_0(42, 40, 1) -> 4, k_0(42, 40, 0) -> 4, k_0(42, 39, 47) -> 4, k_0(42, 39, 46) -> 4, k_0(42, 39, 45) -> 4, k_0(42, 39, 44) -> 4, k_0(42, 39, 43) -> 4, k_0(42, 39, 42) -> 4, k_0(42, 39, 41) -> 4, k_0(42, 39, 40) -> 4, k_0(42, 39, 39) -> 4, k_0(42, 39, 38) -> 4, k_0(42, 39, 4) -> 4, k_0(42, 39, 3) -> 4, k_0(42, 39, 2) -> 4, k_0(42, 39, 1) -> 4, k_0(42, 39, 0) -> 4, k_0(42, 38, 47) -> 4, k_0(42, 38, 46) -> 4, k_0(42, 38, 45) -> 4, k_0(42, 38, 44) -> 4, k_0(42, 38, 43) -> 4, k_0(42, 38, 42) -> 4, k_0(42, 38, 41) -> 4, k_0(42, 38, 40) -> 4, k_0(42, 38, 39) -> 4, k_0(42, 38, 38) -> 4, k_0(42, 38, 4) -> 4, k_0(42, 38, 3) -> 4, k_0(42, 38, 2) -> 4, k_0(42, 38, 1) -> 4, k_0(42, 38, 0) -> 4, k_0(42, 4, 47) -> 4, k_0(42, 4, 46) -> 4, k_0(42, 4, 45) -> 4, k_0(42, 4, 44) -> 4, k_0(42, 4, 43) -> 4, k_0(42, 4, 42) -> 4, k_0(42, 4, 41) -> 4, k_0(42, 4, 40) -> 4, k_0(42, 4, 39) -> 4, k_0(42, 4, 38) -> 4, k_0(42, 4, 4) -> 4, k_0(42, 4, 3) -> 4, k_0(42, 4, 2) -> 4, k_0(42, 4, 1) -> 4, k_0(42, 4, 0) -> 4, k_0(42, 3, 47) -> 4, k_0(42, 3, 46) -> 4, k_0(42, 3, 45) -> 4, k_0(42, 3, 44) -> 4, k_0(42, 3, 43) -> 4, k_0(42, 3, 42) -> 4, k_0(42, 3, 41) -> 4, k_0(42, 3, 40) -> 4, k_0(42, 3, 39) -> 4, k_0(42, 3, 38) -> 4, k_0(42, 3, 4) -> 4, k_0(42, 3, 3) -> 4, k_0(42, 3, 2) -> 4, k_0(42, 3, 1) -> 4, k_0(42, 3, 0) -> 4, k_0(42, 2, 47) -> 4, k_0(42, 2, 46) -> 4, k_0(42, 2, 45) -> 4, k_0(42, 2, 44) -> 4, k_0(42, 2, 43) -> 4, k_0(42, 2, 42) -> 4, k_0(42, 2, 41) -> 4, k_0(42, 2, 40) -> 4, k_0(42, 2, 39) -> 4, k_0(42, 2, 38) -> 4, k_0(42, 2, 4) -> 4, k_0(42, 2, 3) -> 4, k_0(42, 2, 2) -> 4, k_0(42, 2, 1) -> 4, k_0(42, 2, 0) -> 4, k_0(42, 1, 47) -> 4, k_0(42, 1, 46) -> 4, k_0(42, 1, 45) -> 4, k_0(42, 1, 44) -> 4, k_0(42, 1, 43) -> 4, k_0(42, 1, 42) -> 4, k_0(42, 1, 41) -> 4, k_0(42, 1, 40) -> 4, k_0(42, 1, 39) -> 4, k_0(42, 1, 38) -> 4, k_0(42, 1, 4) -> 4, k_0(42, 1, 3) -> 4, k_0(42, 1, 2) -> 4, k_0(42, 1, 1) -> 4, k_0(42, 1, 0) -> 4, k_0(42, 0, 47) -> 4, k_0(42, 0, 46) -> 4, k_0(42, 0, 45) -> 4, k_0(42, 0, 44) -> 4, k_0(42, 0, 43) -> 4, k_0(42, 0, 42) -> 4, k_0(42, 0, 41) -> 4, k_0(42, 0, 40) -> 4, k_0(42, 0, 39) -> 4, k_0(42, 0, 38) -> 4, k_0(42, 0, 4) -> 4, k_0(42, 0, 3) -> 4, k_0(42, 0, 2) -> 4, k_0(42, 0, 1) -> 4, k_0(42, 0, 0) -> 4, k_0(41, 47, 47) -> 4, k_0(41, 47, 46) -> 4, k_0(41, 47, 45) -> 4, k_0(41, 47, 44) -> 4, k_0(41, 47, 43) -> 4, k_0(41, 47, 42) -> 4, k_0(41, 47, 41) -> 4, k_0(41, 47, 40) -> 4, k_0(41, 47, 39) -> 4, k_0(41, 47, 38) -> 4, k_0(41, 47, 4) -> 4, k_0(41, 47, 3) -> 4, k_0(41, 47, 2) -> 4, k_0(41, 47, 1) -> 4, k_0(41, 47, 0) -> 4, k_0(41, 46, 47) -> 4, k_0(41, 46, 46) -> 4, k_0(41, 46, 45) -> 4, k_0(41, 46, 44) -> 4, k_0(41, 46, 43) -> 4, k_0(41, 46, 42) -> 4, k_0(41, 46, 41) -> 4, k_0(41, 46, 40) -> 4, k_0(41, 46, 39) -> 4, k_0(41, 46, 38) -> 4, k_0(41, 46, 4) -> 4, k_0(41, 46, 3) -> 4, k_0(41, 46, 2) -> 4, k_0(41, 46, 1) -> 4, k_0(41, 46, 0) -> 4, k_0(41, 45, 47) -> 4, k_0(41, 45, 46) -> 4, k_0(41, 45, 45) -> 4, k_0(41, 45, 44) -> 4, k_0(41, 45, 43) -> 4, k_0(41, 45, 42) -> 4, k_0(41, 45, 41) -> 4, k_0(41, 45, 40) -> 4, k_0(41, 45, 39) -> 4, k_0(41, 45, 38) -> 4, k_0(41, 45, 4) -> 4, k_0(41, 45, 3) -> 4, k_0(41, 45, 2) -> 4, k_0(41, 45, 1) -> 4, k_0(41, 45, 0) -> 4, k_0(41, 44, 47) -> 4, k_0(41, 44, 46) -> 4, k_0(41, 44, 45) -> 4, k_0(41, 44, 44) -> 4, k_0(41, 44, 43) -> 4, k_0(41, 44, 42) -> 4, k_0(41, 44, 41) -> 4, k_0(41, 44, 40) -> 4, k_0(41, 44, 39) -> 4, k_0(41, 44, 38) -> 4, k_0(41, 44, 4) -> 4, k_0(41, 44, 3) -> 4, k_0(41, 44, 2) -> 4, k_0(41, 44, 1) -> 4, k_0(41, 44, 0) -> 4, k_0(41, 43, 47) -> 4, k_0(41, 43, 46) -> 4, k_0(41, 43, 45) -> 4, k_0(41, 43, 44) -> 4, k_0(41, 43, 43) -> 4, k_0(41, 43, 42) -> 4, k_0(41, 43, 41) -> 4, k_0(41, 43, 40) -> 4, k_0(41, 43, 39) -> 4, k_0(41, 43, 38) -> 4, k_0(41, 43, 4) -> 4, k_0(41, 43, 3) -> 4, k_0(41, 43, 2) -> 4, k_0(41, 43, 1) -> 4, k_0(41, 43, 0) -> 4, k_0(41, 42, 47) -> 4, k_0(41, 42, 46) -> 4, k_0(41, 42, 45) -> 4, k_0(41, 42, 44) -> 4, k_0(41, 42, 43) -> 4, k_0(41, 42, 42) -> 4, k_0(41, 42, 41) -> 4, k_0(41, 42, 40) -> 4, k_0(41, 42, 39) -> 4, k_0(41, 42, 38) -> 4, k_0(41, 42, 4) -> 4, k_0(41, 42, 3) -> 4, k_0(41, 42, 2) -> 4, k_0(41, 42, 1) -> 4, k_0(41, 42, 0) -> 4, k_0(41, 41, 47) -> 4, k_0(41, 41, 46) -> 4, k_0(41, 41, 45) -> 4, k_0(41, 41, 44) -> 4, k_0(41, 41, 43) -> 4, k_0(41, 41, 42) -> 4, k_0(41, 41, 41) -> 4, k_0(41, 41, 40) -> 4, k_0(41, 41, 39) -> 4, k_0(41, 41, 38) -> 4, k_0(41, 41, 4) -> 4, k_0(41, 41, 3) -> 4, k_0(41, 41, 2) -> 4, k_0(41, 41, 1) -> 4, k_0(41, 41, 0) -> 4, k_0(41, 40, 47) -> 4, k_0(41, 40, 46) -> 4, k_0(41, 40, 45) -> 4, k_0(41, 40, 44) -> 4, k_0(41, 40, 43) -> 4, k_0(41, 40, 42) -> 4, k_0(41, 40, 41) -> 4, k_0(41, 40, 40) -> 4, k_0(41, 40, 39) -> 4, k_0(41, 40, 38) -> 4, k_0(41, 40, 4) -> 4, k_0(41, 40, 3) -> 4, k_0(41, 40, 2) -> 4, k_0(41, 40, 1) -> 4, k_0(41, 40, 0) -> 4, k_0(41, 39, 47) -> 4, k_0(41, 39, 46) -> 4, k_0(41, 39, 45) -> 4, k_0(41, 39, 44) -> 4, k_0(41, 39, 43) -> 4, k_0(41, 39, 42) -> 4, k_0(41, 39, 41) -> 4, k_0(41, 39, 40) -> 4, k_0(41, 39, 39) -> 4, k_0(41, 39, 38) -> 4, k_0(41, 39, 4) -> 4, k_0(41, 39, 3) -> 4, k_0(41, 39, 2) -> 4, k_0(41, 39, 1) -> 4, k_0(41, 39, 0) -> 4, k_0(41, 38, 47) -> 4, k_0(41, 38, 46) -> 4, k_0(41, 38, 45) -> 4, k_0(41, 38, 44) -> 4, k_0(41, 38, 43) -> 4, k_0(41, 38, 42) -> 4, k_0(41, 38, 41) -> 4, k_0(41, 38, 40) -> 4, k_0(41, 38, 39) -> 4, k_0(41, 38, 38) -> 4, k_0(41, 38, 4) -> 4, k_0(41, 38, 3) -> 4, k_0(41, 38, 2) -> 4, k_0(41, 38, 1) -> 4, k_0(41, 38, 0) -> 4, k_0(41, 4, 47) -> 4, k_0(41, 4, 46) -> 4, k_0(41, 4, 45) -> 4, k_0(41, 4, 44) -> 4, k_0(41, 4, 43) -> 4, k_0(41, 4, 42) -> 4, k_0(41, 4, 41) -> 4, k_0(41, 4, 40) -> 4, k_0(41, 4, 39) -> 4, k_0(41, 4, 38) -> 4, k_0(41, 4, 4) -> 4, k_0(41, 4, 3) -> 4, k_0(41, 4, 2) -> 4, k_0(41, 4, 1) -> 4, k_0(41, 4, 0) -> 4, k_0(41, 3, 47) -> 4, k_0(41, 3, 46) -> 4, k_0(41, 3, 45) -> 4, k_0(41, 3, 44) -> 4, k_0(41, 3, 43) -> 4, k_0(41, 3, 42) -> 4, k_0(41, 3, 41) -> 4, k_0(41, 3, 40) -> 4, k_0(41, 3, 39) -> 4, k_0(41, 3, 38) -> 4, k_0(41, 3, 4) -> 4, k_0(41, 3, 3) -> 4, k_0(41, 3, 2) -> 4, k_0(41, 3, 1) -> 4, k_0(41, 3, 0) -> 4, k_0(41, 2, 47) -> 4, k_0(41, 2, 46) -> 4, k_0(41, 2, 45) -> 4, k_0(41, 2, 44) -> 4, k_0(41, 2, 43) -> 4, k_0(41, 2, 42) -> 4, k_0(41, 2, 41) -> 4, k_0(41, 2, 40) -> 4, k_0(41, 2, 39) -> 4, k_0(41, 2, 38) -> 4, k_0(41, 2, 4) -> 4, k_0(41, 2, 3) -> 4, k_0(41, 2, 2) -> 4, k_0(41, 2, 1) -> 4, k_0(41, 2, 0) -> 4, k_0(41, 1, 47) -> 4, k_0(41, 1, 46) -> 4, k_0(41, 1, 45) -> 4, k_0(41, 1, 44) -> 4, k_0(41, 1, 43) -> 4, k_0(41, 1, 42) -> 4, k_0(41, 1, 41) -> 4, k_0(41, 1, 40) -> 4, k_0(41, 1, 39) -> 4, k_0(41, 1, 38) -> 4, k_0(41, 1, 4) -> 4, k_0(41, 1, 3) -> 4, k_0(41, 1, 2) -> 4, k_0(41, 1, 1) -> 4, k_0(41, 1, 0) -> 4, k_0(41, 0, 47) -> 4, k_0(41, 0, 46) -> 4, k_0(41, 0, 45) -> 4, k_0(41, 0, 44) -> 4, k_0(41, 0, 43) -> 4, k_0(41, 0, 42) -> 4, k_0(41, 0, 41) -> 4, k_0(41, 0, 40) -> 4, k_0(41, 0, 39) -> 4, k_0(41, 0, 38) -> 4, k_0(41, 0, 4) -> 4, k_0(41, 0, 3) -> 4, k_0(41, 0, 2) -> 4, k_0(41, 0, 1) -> 4, k_0(41, 0, 0) -> 4, k_0(40, 47, 47) -> 4, k_0(40, 47, 46) -> 4, k_0(40, 47, 45) -> 4, k_0(40, 47, 44) -> 4, k_0(40, 47, 43) -> 4, k_0(40, 47, 42) -> 4, k_0(40, 47, 41) -> 4, k_0(40, 47, 40) -> 4, k_0(40, 47, 39) -> 4, k_0(40, 47, 38) -> 4, k_0(40, 47, 4) -> 4, k_0(40, 47, 3) -> 4, k_0(40, 47, 2) -> 4, k_0(40, 47, 1) -> 4, k_0(40, 47, 0) -> 4, k_0(40, 46, 47) -> 4, k_0(40, 46, 46) -> 4, k_0(40, 46, 45) -> 4, k_0(40, 46, 44) -> 4, k_0(40, 46, 43) -> 4, k_0(40, 46, 42) -> 4, k_0(40, 46, 41) -> 4, k_0(40, 46, 40) -> 4, k_0(40, 46, 39) -> 4, k_0(40, 46, 38) -> 4, k_0(40, 46, 4) -> 4, k_0(40, 46, 3) -> 4, k_0(40, 46, 2) -> 4, k_0(40, 46, 1) -> 4, k_0(40, 46, 0) -> 4, k_0(40, 45, 47) -> 4, k_0(40, 45, 46) -> 4, k_0(40, 45, 45) -> 4, k_0(40, 45, 44) -> 4, k_0(40, 45, 43) -> 4, k_0(40, 45, 42) -> 4, k_0(40, 45, 41) -> 4, k_0(40, 45, 40) -> 4, k_0(40, 45, 39) -> 4, k_0(40, 45, 38) -> 4, k_0(40, 45, 4) -> 4, k_0(40, 45, 3) -> 4, k_0(40, 45, 2) -> 4, k_0(40, 45, 1) -> 4, k_0(40, 45, 0) -> 4, k_0(40, 44, 47) -> 4, k_0(40, 44, 46) -> 4, k_0(40, 44, 45) -> 4, k_0(40, 44, 44) -> 4, k_0(40, 44, 43) -> 4, k_0(40, 44, 42) -> 4, k_0(40, 44, 41) -> 4, k_0(40, 44, 40) -> 4, k_0(40, 44, 39) -> 4, k_0(40, 44, 38) -> 4, k_0(40, 44, 4) -> 4, k_0(40, 44, 3) -> 4, k_0(40, 44, 2) -> 4, k_0(40, 44, 1) -> 4, k_0(40, 44, 0) -> 4, k_0(40, 43, 47) -> 4, k_0(40, 43, 46) -> 4, k_0(40, 43, 45) -> 4, k_0(40, 43, 44) -> 4, k_0(40, 43, 43) -> 4, k_0(40, 43, 42) -> 4, k_0(40, 43, 41) -> 4, k_0(40, 43, 40) -> 4, k_0(40, 43, 39) -> 4, k_0(40, 43, 38) -> 4, k_0(40, 43, 4) -> 4, k_0(40, 43, 3) -> 4, k_0(40, 43, 2) -> 4, k_0(40, 43, 1) -> 4, k_0(40, 43, 0) -> 4, k_0(40, 42, 47) -> 4, k_0(40, 42, 46) -> 4, k_0(40, 42, 45) -> 4, k_0(40, 42, 44) -> 4, k_0(40, 42, 43) -> 4, k_0(40, 42, 42) -> 4, k_0(40, 42, 41) -> 4, k_0(40, 42, 40) -> 4, k_0(40, 42, 39) -> 4, k_0(40, 42, 38) -> 4, k_0(40, 42, 4) -> 4, k_0(40, 42, 3) -> 4, k_0(40, 42, 2) -> 4, k_0(40, 42, 1) -> 4, k_0(40, 42, 0) -> 4, k_0(40, 41, 47) -> 4, k_0(40, 41, 46) -> 4, k_0(40, 41, 45) -> 4, k_0(40, 41, 44) -> 4, k_0(40, 41, 43) -> 4, k_0(40, 41, 42) -> 4, k_0(40, 41, 41) -> 4, k_0(40, 41, 40) -> 4, k_0(40, 41, 39) -> 4, k_0(40, 41, 38) -> 4, k_0(40, 41, 4) -> 4, k_0(40, 41, 3) -> 4, k_0(40, 41, 2) -> 4, k_0(40, 41, 1) -> 4, k_0(40, 41, 0) -> 4, k_0(40, 40, 47) -> 4, k_0(40, 40, 46) -> 4, k_0(40, 40, 45) -> 4, k_0(40, 40, 44) -> 4, k_0(40, 40, 43) -> 4, k_0(40, 40, 42) -> 4, k_0(40, 40, 41) -> 4, k_0(40, 40, 40) -> 4, k_0(40, 40, 39) -> 4, k_0(40, 40, 38) -> 4, k_0(40, 40, 4) -> 4, k_0(40, 40, 3) -> 4, k_0(40, 40, 2) -> 4, k_0(40, 40, 1) -> 4, k_0(40, 40, 0) -> 4, k_0(40, 39, 47) -> 4, k_0(40, 39, 46) -> 4, k_0(40, 39, 45) -> 4, k_0(40, 39, 44) -> 4, k_0(40, 39, 43) -> 4, k_0(40, 39, 42) -> 4, k_0(40, 39, 41) -> 4, k_0(40, 39, 40) -> 4, k_0(40, 39, 39) -> 4, k_0(40, 39, 38) -> 4, k_0(40, 39, 4) -> 4, k_0(40, 39, 3) -> 4, k_0(40, 39, 2) -> 4, k_0(40, 39, 1) -> 4, k_0(40, 39, 0) -> 4, k_0(40, 38, 47) -> 4, k_0(40, 38, 46) -> 4, k_0(40, 38, 45) -> 4, k_0(40, 38, 44) -> 4, k_0(40, 38, 43) -> 4, k_0(40, 38, 42) -> 4, k_0(40, 38, 41) -> 4, k_0(40, 38, 40) -> 4, k_0(40, 38, 39) -> 4, k_0(40, 38, 38) -> 4, k_0(40, 38, 4) -> 4, k_0(40, 38, 3) -> 4, k_0(40, 38, 2) -> 4, k_0(40, 38, 1) -> 4, k_0(40, 38, 0) -> 4, k_0(40, 4, 47) -> 4, k_0(40, 4, 46) -> 4, k_0(40, 4, 45) -> 4, k_0(40, 4, 44) -> 4, k_0(40, 4, 43) -> 4, k_0(40, 4, 42) -> 4, k_0(40, 4, 41) -> 4, k_0(40, 4, 40) -> 4, k_0(40, 4, 39) -> 4, k_0(40, 4, 38) -> 4, k_0(40, 4, 4) -> 4, k_0(40, 4, 3) -> 4, k_0(40, 4, 2) -> 4, k_0(40, 4, 1) -> 4, k_0(40, 4, 0) -> 4, k_0(40, 3, 47) -> 4, k_0(40, 3, 46) -> 4, k_0(40, 3, 45) -> 4, k_0(40, 3, 44) -> 4, k_0(40, 3, 43) -> 4, k_0(40, 3, 42) -> 4, k_0(40, 3, 41) -> 4, k_0(40, 3, 40) -> 4, k_0(40, 3, 39) -> 4, k_0(40, 3, 38) -> 4, k_0(40, 3, 4) -> 4, k_0(40, 3, 3) -> 4, k_0(40, 3, 2) -> 4, k_0(40, 3, 1) -> 4, k_0(40, 3, 0) -> 4, k_0(40, 2, 47) -> 4, k_0(40, 2, 46) -> 4, k_0(40, 2, 45) -> 4, k_0(40, 2, 44) -> 4, k_0(40, 2, 43) -> 4, k_0(40, 2, 42) -> 4, k_0(40, 2, 41) -> 4, k_0(40, 2, 40) -> 4, k_0(40, 2, 39) -> 4, k_0(40, 2, 38) -> 4, k_0(40, 2, 4) -> 4, k_0(40, 2, 3) -> 4, k_0(40, 2, 2) -> 4, k_0(40, 2, 1) -> 4, k_0(40, 2, 0) -> 4, k_0(40, 1, 47) -> 4, k_0(40, 1, 46) -> 4, k_0(40, 1, 45) -> 4, k_0(40, 1, 44) -> 4, k_0(40, 1, 43) -> 4, k_0(40, 1, 42) -> 4, k_0(40, 1, 41) -> 4, k_0(40, 1, 40) -> 4, k_0(40, 1, 39) -> 4, k_0(40, 1, 38) -> 4, k_0(40, 1, 4) -> 4, k_0(40, 1, 3) -> 4, k_0(40, 1, 2) -> 4, k_0(40, 1, 1) -> 4, k_0(40, 1, 0) -> 4, k_0(40, 0, 47) -> 4, k_0(40, 0, 46) -> 4, k_0(40, 0, 45) -> 4, k_0(40, 0, 44) -> 4, k_0(40, 0, 43) -> 4, k_0(40, 0, 42) -> 4, k_0(40, 0, 41) -> 4, k_0(40, 0, 40) -> 4, k_0(40, 0, 39) -> 4, k_0(40, 0, 38) -> 4, k_0(40, 0, 4) -> 4, k_0(40, 0, 3) -> 4, k_0(40, 0, 2) -> 4, k_0(40, 0, 1) -> 4, k_0(40, 0, 0) -> 4, k_0(39, 47, 47) -> 4, k_0(39, 47, 46) -> 4, k_0(39, 47, 45) -> 4, k_0(39, 47, 44) -> 4, k_0(39, 47, 43) -> 4, k_0(39, 47, 42) -> 4, k_0(39, 47, 41) -> 4, k_0(39, 47, 40) -> 4, k_0(39, 47, 39) -> 4, k_0(39, 47, 38) -> 4, k_0(39, 47, 4) -> 4, k_0(39, 47, 3) -> 4, k_0(39, 47, 2) -> 4, k_0(39, 47, 1) -> 4, k_0(39, 47, 0) -> 4, k_0(39, 46, 47) -> 4, k_0(39, 46, 46) -> 4, k_0(39, 46, 45) -> 4, k_0(39, 46, 44) -> 4, k_0(39, 46, 43) -> 4, k_0(39, 46, 42) -> 4, k_0(39, 46, 41) -> 4, k_0(39, 46, 40) -> 4, k_0(39, 46, 39) -> 4, k_0(39, 46, 38) -> 4, k_0(39, 46, 4) -> 4, k_0(39, 46, 3) -> 4, k_0(39, 46, 2) -> 4, k_0(39, 46, 1) -> 4, k_0(39, 46, 0) -> 4, k_0(39, 45, 47) -> 4, k_0(39, 45, 46) -> 4, k_0(39, 45, 45) -> 4, k_0(39, 45, 44) -> 4, k_0(39, 45, 43) -> 4, k_0(39, 45, 42) -> 4, k_0(39, 45, 41) -> 4, k_0(39, 45, 40) -> 4, k_0(39, 45, 39) -> 4, k_0(39, 45, 38) -> 4, k_0(39, 45, 4) -> 4, k_0(39, 45, 3) -> 4, k_0(39, 45, 2) -> 4, k_0(39, 45, 1) -> 4, k_0(39, 45, 0) -> 4, k_0(39, 44, 47) -> 4, k_0(39, 44, 46) -> 4, k_0(39, 44, 45) -> 4, k_0(39, 44, 44) -> 4, k_0(39, 44, 43) -> 4, k_0(39, 44, 42) -> 4, k_0(39, 44, 41) -> 4, k_0(39, 44, 40) -> 4, k_0(39, 44, 39) -> 4, k_0(39, 44, 38) -> 4, k_0(39, 44, 4) -> 4, k_0(39, 44, 3) -> 4, k_0(39, 44, 2) -> 4, k_0(39, 44, 1) -> 4, k_0(39, 44, 0) -> 4, k_0(39, 43, 47) -> 4, k_0(39, 43, 46) -> 4, k_0(39, 43, 45) -> 4, k_0(39, 43, 44) -> 4, k_0(39, 43, 43) -> 4, k_0(39, 43, 42) -> 4, k_0(39, 43, 41) -> 4, k_0(39, 43, 40) -> 4, k_0(39, 43, 39) -> 4, k_0(39, 43, 38) -> 4, k_0(39, 43, 4) -> 4, k_0(39, 43, 3) -> 4, k_0(39, 43, 2) -> 4, k_0(39, 43, 1) -> 4, k_0(39, 43, 0) -> 4, k_0(39, 42, 47) -> 4, k_0(39, 42, 46) -> 4, k_0(39, 42, 45) -> 4, k_0(39, 42, 44) -> 4, k_0(39, 42, 43) -> 4, k_0(39, 42, 42) -> 4, k_0(39, 42, 41) -> 4, k_0(39, 42, 40) -> 4, k_0(39, 42, 39) -> 4, k_0(39, 42, 38) -> 4, k_0(39, 42, 4) -> 4, k_0(39, 42, 3) -> 4, k_0(39, 42, 2) -> 4, k_0(39, 42, 1) -> 4, k_0(39, 42, 0) -> 4, k_0(39, 41, 47) -> 4, k_0(39, 41, 46) -> 4, k_0(39, 41, 45) -> 4, k_0(39, 41, 44) -> 4, k_0(39, 41, 43) -> 4, k_0(39, 41, 42) -> 4, k_0(39, 41, 41) -> 4, k_0(39, 41, 40) -> 4, k_0(39, 41, 39) -> 4, k_0(39, 41, 38) -> 4, k_0(39, 41, 4) -> 4, k_0(39, 41, 3) -> 4, k_0(39, 41, 2) -> 4, k_0(39, 41, 1) -> 4, k_0(39, 41, 0) -> 4, k_0(39, 40, 47) -> 4, k_0(39, 40, 46) -> 4, k_0(39, 40, 45) -> 4, k_0(39, 40, 44) -> 4, k_0(39, 40, 43) -> 4, k_0(39, 40, 42) -> 4, k_0(39, 40, 41) -> 4, k_0(39, 40, 40) -> 4, k_0(39, 40, 39) -> 4, k_0(39, 40, 38) -> 4, k_0(39, 40, 4) -> 4, k_0(39, 40, 3) -> 4, k_0(39, 40, 2) -> 4, k_0(39, 40, 1) -> 4, k_0(39, 40, 0) -> 4, k_0(39, 39, 47) -> 4, k_0(39, 39, 46) -> 4, k_0(39, 39, 45) -> 4, k_0(39, 39, 44) -> 4, k_0(39, 39, 43) -> 4, k_0(39, 39, 42) -> 4, k_0(39, 39, 41) -> 4, k_0(39, 39, 40) -> 4, k_0(39, 39, 39) -> 4, k_0(39, 39, 38) -> 4, k_0(39, 39, 4) -> 4, k_0(39, 39, 3) -> 4, k_0(39, 39, 2) -> 4, k_0(39, 39, 1) -> 4, k_0(39, 39, 0) -> 4, k_0(39, 38, 47) -> 4, k_0(39, 38, 46) -> 4, k_0(39, 38, 45) -> 4, k_0(39, 38, 44) -> 4, k_0(39, 38, 43) -> 4, k_0(39, 38, 42) -> 4, k_0(39, 38, 41) -> 4, k_0(39, 38, 40) -> 4, k_0(39, 38, 39) -> 4, k_0(39, 38, 38) -> 4, k_0(39, 38, 4) -> 4, k_0(39, 38, 3) -> 4, k_0(39, 38, 2) -> 4, k_0(39, 38, 1) -> 4, k_0(39, 38, 0) -> 4, k_0(39, 4, 47) -> 4, k_0(39, 4, 46) -> 4, k_0(39, 4, 45) -> 4, k_0(39, 4, 44) -> 4, k_0(39, 4, 43) -> 4, k_0(39, 4, 42) -> 4, k_0(39, 4, 41) -> 4, k_0(39, 4, 40) -> 4, k_0(39, 4, 39) -> 4, k_0(39, 4, 38) -> 4, k_0(39, 4, 4) -> 4, k_0(39, 4, 3) -> 4, k_0(39, 4, 2) -> 4, k_0(39, 4, 1) -> 4, k_0(39, 4, 0) -> 4, k_0(39, 3, 47) -> 4, k_0(39, 3, 46) -> 4, k_0(39, 3, 45) -> 4, k_0(39, 3, 44) -> 4, k_0(39, 3, 43) -> 4, k_0(39, 3, 42) -> 4, k_0(39, 3, 41) -> 4, k_0(39, 3, 40) -> 4, k_0(39, 3, 39) -> 4, k_0(39, 3, 38) -> 4, k_0(39, 3, 4) -> 4, k_0(39, 3, 3) -> 4, k_0(39, 3, 2) -> 4, k_0(39, 3, 1) -> 4, k_0(39, 3, 0) -> 4, k_0(39, 2, 47) -> 4, k_0(39, 2, 46) -> 4, k_0(39, 2, 45) -> 4, k_0(39, 2, 44) -> 4, k_0(39, 2, 43) -> 4, k_0(39, 2, 42) -> 4, k_0(39, 2, 41) -> 4, k_0(39, 2, 40) -> 4, k_0(39, 2, 39) -> 4, k_0(39, 2, 38) -> 4, k_0(39, 2, 4) -> 4, k_0(39, 2, 3) -> 4, k_0(39, 2, 2) -> 4, k_0(39, 2, 1) -> 4, k_0(39, 2, 0) -> 4, k_0(39, 1, 47) -> 4, k_0(39, 1, 46) -> 4, k_0(39, 1, 45) -> 4, k_0(39, 1, 44) -> 4, k_0(39, 1, 43) -> 4, k_0(39, 1, 42) -> 4, k_0(39, 1, 41) -> 4, k_0(39, 1, 40) -> 4, k_0(39, 1, 39) -> 4, k_0(39, 1, 38) -> 4, k_0(39, 1, 4) -> 4, k_0(39, 1, 3) -> 4, k_0(39, 1, 2) -> 4, k_0(39, 1, 1) -> 4, k_0(39, 1, 0) -> 4, k_0(39, 0, 47) -> 4, k_0(39, 0, 46) -> 4, k_0(39, 0, 45) -> 4, k_0(39, 0, 44) -> 4, k_0(39, 0, 43) -> 4, k_0(39, 0, 42) -> 4, k_0(39, 0, 41) -> 4, k_0(39, 0, 40) -> 4, k_0(39, 0, 39) -> 4, k_0(39, 0, 38) -> 4, k_0(39, 0, 4) -> 4, k_0(39, 0, 3) -> 4, k_0(39, 0, 2) -> 4, k_0(39, 0, 1) -> 4, k_0(39, 0, 0) -> 4, k_0(38, 47, 47) -> 4, k_0(38, 47, 46) -> 4, k_0(38, 47, 45) -> 4, k_0(38, 47, 44) -> 4, k_0(38, 47, 43) -> 4, k_0(38, 47, 42) -> 4, k_0(38, 47, 41) -> 4, k_0(38, 47, 40) -> 4, k_0(38, 47, 39) -> 4, k_0(38, 47, 38) -> 4, k_0(38, 47, 4) -> 4, k_0(38, 47, 3) -> 4, k_0(38, 47, 2) -> 4, k_0(38, 47, 1) -> 4, k_0(38, 47, 0) -> 4, k_0(38, 46, 47) -> 4, k_0(38, 46, 46) -> 4, k_0(38, 46, 45) -> 4, k_0(38, 46, 44) -> 4, k_0(38, 46, 43) -> 4, k_0(38, 46, 42) -> 4, k_0(38, 46, 41) -> 4, k_0(38, 46, 40) -> 4, k_0(38, 46, 39) -> 4, k_0(38, 46, 38) -> 4, k_0(38, 46, 4) -> 4, k_0(38, 46, 3) -> 4, k_0(38, 46, 2) -> 4, k_0(38, 46, 1) -> 4, k_0(38, 46, 0) -> 4, k_0(38, 45, 47) -> 4, k_0(38, 45, 46) -> 4, k_0(38, 45, 45) -> 4, k_0(38, 45, 44) -> 4, k_0(38, 45, 43) -> 4, k_0(38, 45, 42) -> 4, k_0(38, 45, 41) -> 4, k_0(38, 45, 40) -> 4, k_0(38, 45, 39) -> 4, k_0(38, 45, 38) -> 4, k_0(38, 45, 4) -> 4, k_0(38, 45, 3) -> 4, k_0(38, 45, 2) -> 4, k_0(38, 45, 1) -> 4, k_0(38, 45, 0) -> 4, k_0(38, 44, 47) -> 4, k_0(38, 44, 46) -> 4, k_0(38, 44, 45) -> 4, k_0(38, 44, 44) -> 4, k_0(38, 44, 43) -> 4, k_0(38, 44, 42) -> 4, k_0(38, 44, 41) -> 4, k_0(38, 44, 40) -> 4, k_0(38, 44, 39) -> 4, k_0(38, 44, 38) -> 4, k_0(38, 44, 4) -> 4, k_0(38, 44, 3) -> 4, k_0(38, 44, 2) -> 4, k_0(38, 44, 1) -> 4, k_0(38, 44, 0) -> 4, k_0(38, 43, 47) -> 4, k_0(38, 43, 46) -> 4, k_0(38, 43, 45) -> 4, k_0(38, 43, 44) -> 4, k_0(38, 43, 43) -> 4, k_0(38, 43, 42) -> 4, k_0(38, 43, 41) -> 4, k_0(38, 43, 40) -> 4, k_0(38, 43, 39) -> 4, k_0(38, 43, 38) -> 4, k_0(38, 43, 4) -> 4, k_0(38, 43, 3) -> 4, k_0(38, 43, 2) -> 4, k_0(38, 43, 1) -> 4, k_0(38, 43, 0) -> 4, k_0(38, 42, 47) -> 4, k_0(38, 42, 46) -> 4, k_0(38, 42, 45) -> 4, k_0(38, 42, 44) -> 4, k_0(38, 42, 43) -> 4, k_0(38, 42, 42) -> 4, k_0(38, 42, 41) -> 4, k_0(38, 42, 40) -> 4, k_0(38, 42, 39) -> 4, k_0(38, 42, 38) -> 4, k_0(38, 42, 4) -> 4, k_0(38, 42, 3) -> 4, k_0(38, 42, 2) -> 4, k_0(38, 42, 1) -> 4, k_0(38, 42, 0) -> 4, k_0(38, 41, 47) -> 4, k_0(38, 41, 46) -> 4, k_0(38, 41, 45) -> 4, k_0(38, 41, 44) -> 4, k_0(38, 41, 43) -> 4, k_0(38, 41, 42) -> 4, k_0(38, 41, 41) -> 4, k_0(38, 41, 40) -> 4, k_0(38, 41, 39) -> 4, k_0(38, 41, 38) -> 4, k_0(38, 41, 4) -> 4, k_0(38, 41, 3) -> 4, k_0(38, 41, 2) -> 4, k_0(38, 41, 1) -> 4, k_0(38, 41, 0) -> 4, k_0(38, 40, 47) -> 4, k_0(38, 40, 46) -> 4, k_0(38, 40, 45) -> 4, k_0(38, 40, 44) -> 4, k_0(38, 40, 43) -> 4, k_0(38, 40, 42) -> 4, k_0(38, 40, 41) -> 4, k_0(38, 40, 40) -> 4, k_0(38, 40, 39) -> 4, k_0(38, 40, 38) -> 4, k_0(38, 40, 4) -> 4, k_0(38, 40, 3) -> 4, k_0(38, 40, 2) -> 4, k_0(38, 40, 1) -> 4, k_0(38, 40, 0) -> 4, k_0(38, 39, 47) -> 4, k_0(38, 39, 46) -> 4, k_0(38, 39, 45) -> 4, k_0(38, 39, 44) -> 4, k_0(38, 39, 43) -> 4, k_0(38, 39, 42) -> 4, k_0(38, 39, 41) -> 4, k_0(38, 39, 40) -> 4, k_0(38, 39, 39) -> 4, k_0(38, 39, 38) -> 4, k_0(38, 39, 4) -> 4, k_0(38, 39, 3) -> 4, k_0(38, 39, 2) -> 4, k_0(38, 39, 1) -> 4, k_0(38, 39, 0) -> 4, k_0(38, 38, 47) -> 4, k_0(38, 38, 46) -> 4, k_0(38, 38, 45) -> 4, k_0(38, 38, 44) -> 4, k_0(38, 38, 43) -> 4, k_0(38, 38, 42) -> 4, k_0(38, 38, 41) -> 4, k_0(38, 38, 40) -> 4, k_0(38, 38, 39) -> 4, k_0(38, 38, 38) -> 4, k_0(38, 38, 4) -> 4, k_0(38, 38, 3) -> 4, k_0(38, 38, 2) -> 4, k_0(38, 38, 1) -> 4, k_0(38, 38, 0) -> 4, k_0(38, 4, 47) -> 4, k_0(38, 4, 46) -> 4, k_0(38, 4, 45) -> 4, k_0(38, 4, 44) -> 4, k_0(38, 4, 43) -> 4, k_0(38, 4, 42) -> 4, k_0(38, 4, 41) -> 4, k_0(38, 4, 40) -> 4, k_0(38, 4, 39) -> 4, k_0(38, 4, 38) -> 4, k_0(38, 4, 4) -> 4, k_0(38, 4, 3) -> 4, k_0(38, 4, 2) -> 4, k_0(38, 4, 1) -> 4, k_0(38, 4, 0) -> 4, k_0(38, 3, 47) -> 4, k_0(38, 3, 46) -> 4, k_0(38, 3, 45) -> 4, k_0(38, 3, 44) -> 4, k_0(38, 3, 43) -> 4, k_0(38, 3, 42) -> 4, k_0(38, 3, 41) -> 4, k_0(38, 3, 40) -> 4, k_0(38, 3, 39) -> 4, k_0(38, 3, 38) -> 4, k_0(38, 3, 4) -> 4, k_0(38, 3, 3) -> 4, k_0(38, 3, 2) -> 4, k_0(38, 3, 1) -> 4, k_0(38, 3, 0) -> 4, k_0(38, 2, 47) -> 4, k_0(38, 2, 46) -> 4, k_0(38, 2, 45) -> 4, k_0(38, 2, 44) -> 4, k_0(38, 2, 43) -> 4, k_0(38, 2, 42) -> 4, k_0(38, 2, 41) -> 4, k_0(38, 2, 40) -> 4, k_0(38, 2, 39) -> 4, k_0(38, 2, 38) -> 4, k_0(38, 2, 4) -> 4, k_0(38, 2, 3) -> 4, k_0(38, 2, 2) -> 4, k_0(38, 2, 1) -> 4, k_0(38, 2, 0) -> 4, k_0(38, 1, 47) -> 4, k_0(38, 1, 46) -> 4, k_0(38, 1, 45) -> 4, k_0(38, 1, 44) -> 4, k_0(38, 1, 43) -> 4, k_0(38, 1, 42) -> 4, k_0(38, 1, 41) -> 4, k_0(38, 1, 40) -> 4, k_0(38, 1, 39) -> 4, k_0(38, 1, 38) -> 4, k_0(38, 1, 4) -> 4, k_0(38, 1, 3) -> 4, k_0(38, 1, 2) -> 4, k_0(38, 1, 1) -> 4, k_0(38, 1, 0) -> 4, k_0(38, 0, 47) -> 4, k_0(38, 0, 46) -> 4, k_0(38, 0, 45) -> 4, k_0(38, 0, 44) -> 4, k_0(38, 0, 43) -> 4, k_0(38, 0, 42) -> 4, k_0(38, 0, 41) -> 4, k_0(38, 0, 40) -> 4, k_0(38, 0, 39) -> 4, k_0(38, 0, 38) -> 4, k_0(38, 0, 4) -> 4, k_0(38, 0, 3) -> 4, k_0(38, 0, 2) -> 4, k_0(38, 0, 1) -> 4, k_0(38, 0, 0) -> 4, k_0(4, 47, 47) -> 4, k_0(4, 47, 46) -> 4, k_0(4, 47, 45) -> 4, k_0(4, 47, 44) -> 4, k_0(4, 47, 43) -> 4, k_0(4, 47, 42) -> 4, k_0(4, 47, 41) -> 4, k_0(4, 47, 40) -> 4, k_0(4, 47, 39) -> 4, k_0(4, 47, 38) -> 4, k_0(4, 47, 4) -> 4, k_0(4, 47, 3) -> 4, k_0(4, 47, 2) -> 4, k_0(4, 47, 1) -> 4, k_0(4, 47, 0) -> 4, k_0(4, 46, 47) -> 4, k_0(4, 46, 46) -> 4, k_0(4, 46, 45) -> 4, k_0(4, 46, 44) -> 4, k_0(4, 46, 43) -> 4, k_0(4, 46, 42) -> 4, k_0(4, 46, 41) -> 4, k_0(4, 46, 40) -> 4, k_0(4, 46, 39) -> 4, k_0(4, 46, 38) -> 4, k_0(4, 46, 4) -> 4, k_0(4, 46, 3) -> 4, k_0(4, 46, 2) -> 4, k_0(4, 46, 1) -> 4, k_0(4, 46, 0) -> 4, k_0(4, 45, 47) -> 4, k_0(4, 45, 46) -> 4, k_0(4, 45, 45) -> 4, k_0(4, 45, 44) -> 4, k_0(4, 45, 43) -> 4, k_0(4, 45, 42) -> 4, k_0(4, 45, 41) -> 4, k_0(4, 45, 40) -> 4, k_0(4, 45, 39) -> 4, k_0(4, 45, 38) -> 4, k_0(4, 45, 4) -> 4, k_0(4, 45, 3) -> 4, k_0(4, 45, 2) -> 4, k_0(4, 45, 1) -> 4, k_0(4, 45, 0) -> 4, k_0(4, 44, 47) -> 4, k_0(4, 44, 46) -> 4, k_0(4, 44, 45) -> 4, k_0(4, 44, 44) -> 4, k_0(4, 44, 43) -> 4, k_0(4, 44, 42) -> 4, k_0(4, 44, 41) -> 4, k_0(4, 44, 40) -> 4, k_0(4, 44, 39) -> 4, k_0(4, 44, 38) -> 4, k_0(4, 44, 4) -> 4, k_0(4, 44, 3) -> 4, k_0(4, 44, 2) -> 4, k_0(4, 44, 1) -> 4, k_0(4, 44, 0) -> 4, k_0(4, 43, 47) -> 4, k_0(4, 43, 46) -> 4, k_0(4, 43, 45) -> 4, k_0(4, 43, 44) -> 4, k_0(4, 43, 43) -> 4, k_0(4, 43, 42) -> 4, k_0(4, 43, 41) -> 4, k_0(4, 43, 40) -> 4, k_0(4, 43, 39) -> 4, k_0(4, 43, 38) -> 4, k_0(4, 43, 4) -> 4, k_0(4, 43, 3) -> 4, k_0(4, 43, 2) -> 4, k_0(4, 43, 1) -> 4, k_0(4, 43, 0) -> 4, k_0(4, 42, 47) -> 4, k_0(4, 42, 46) -> 4, k_0(4, 42, 45) -> 4, k_0(4, 42, 44) -> 4, k_0(4, 42, 43) -> 4, k_0(4, 42, 42) -> 4, k_0(4, 42, 41) -> 4, k_0(4, 42, 40) -> 4, k_0(4, 42, 39) -> 4, k_0(4, 42, 38) -> 4, k_0(4, 42, 4) -> 4, k_0(4, 42, 3) -> 4, k_0(4, 42, 2) -> 4, k_0(4, 42, 1) -> 4, k_0(4, 42, 0) -> 4, k_0(4, 41, 47) -> 4, k_0(4, 41, 46) -> 4, k_0(4, 41, 45) -> 4, k_0(4, 41, 44) -> 4, k_0(4, 41, 43) -> 4, k_0(4, 41, 42) -> 4, k_0(4, 41, 41) -> 4, k_0(4, 41, 40) -> 4, k_0(4, 41, 39) -> 4, k_0(4, 41, 38) -> 4, k_0(4, 41, 4) -> 4, k_0(4, 41, 3) -> 4, k_0(4, 41, 2) -> 4, k_0(4, 41, 1) -> 4, k_0(4, 41, 0) -> 4, k_0(4, 40, 47) -> 4, k_0(4, 40, 46) -> 4, k_0(4, 40, 45) -> 4, k_0(4, 40, 44) -> 4, k_0(4, 40, 43) -> 4, k_0(4, 40, 42) -> 4, k_0(4, 40, 41) -> 4, k_0(4, 40, 40) -> 4, k_0(4, 40, 39) -> 4, k_0(4, 40, 38) -> 4, k_0(4, 40, 4) -> 4, k_0(4, 40, 3) -> 4, k_0(4, 40, 2) -> 4, k_0(4, 40, 1) -> 4, k_0(4, 40, 0) -> 4, k_0(4, 39, 47) -> 4, k_0(4, 39, 46) -> 4, k_0(4, 39, 45) -> 4, k_0(4, 39, 44) -> 4, k_0(4, 39, 43) -> 4, k_0(4, 39, 42) -> 4, k_0(4, 39, 41) -> 4, k_0(4, 39, 40) -> 4, k_0(4, 39, 39) -> 4, k_0(4, 39, 38) -> 4, k_0(4, 39, 4) -> 4, k_0(4, 39, 3) -> 4, k_0(4, 39, 2) -> 4, k_0(4, 39, 1) -> 4, k_0(4, 39, 0) -> 4, k_0(4, 38, 47) -> 4, k_0(4, 38, 46) -> 4, k_0(4, 38, 45) -> 4, k_0(4, 38, 44) -> 4, k_0(4, 38, 43) -> 4, k_0(4, 38, 42) -> 4, k_0(4, 38, 41) -> 4, k_0(4, 38, 40) -> 4, k_0(4, 38, 39) -> 4, k_0(4, 38, 38) -> 4, k_0(4, 38, 4) -> 4, k_0(4, 38, 3) -> 4, k_0(4, 38, 2) -> 4, k_0(4, 38, 1) -> 4, k_0(4, 38, 0) -> 4, k_0(4, 4, 47) -> 4, k_0(4, 4, 46) -> 4, k_0(4, 4, 45) -> 4, k_0(4, 4, 44) -> 4, k_0(4, 4, 43) -> 4, k_0(4, 4, 42) -> 4, k_0(4, 4, 41) -> 4, k_0(4, 4, 40) -> 4, k_0(4, 4, 39) -> 4, k_0(4, 4, 38) -> 4, k_0(4, 4, 4) -> 4, k_0(4, 4, 3) -> 4, k_0(4, 4, 2) -> 4, k_0(4, 4, 1) -> 4, k_0(4, 4, 0) -> 4, k_0(4, 3, 47) -> 4, k_0(4, 3, 46) -> 4, k_0(4, 3, 45) -> 4, k_0(4, 3, 44) -> 4, k_0(4, 3, 43) -> 4, k_0(4, 3, 42) -> 4, k_0(4, 3, 41) -> 4, k_0(4, 3, 40) -> 4, k_0(4, 3, 39) -> 4, k_0(4, 3, 38) -> 4, k_0(4, 3, 4) -> 4, k_0(4, 3, 3) -> 4, k_0(4, 3, 2) -> 4, k_0(4, 3, 1) -> 4, k_0(4, 3, 0) -> 4, k_0(4, 2, 47) -> 4, k_0(4, 2, 46) -> 4, k_0(4, 2, 45) -> 4, k_0(4, 2, 44) -> 4, k_0(4, 2, 43) -> 4, k_0(4, 2, 42) -> 4, k_0(4, 2, 41) -> 4, k_0(4, 2, 40) -> 4, k_0(4, 2, 39) -> 4, k_0(4, 2, 38) -> 4, k_0(4, 2, 4) -> 4, k_0(4, 2, 3) -> 4, k_0(4, 2, 2) -> 4, k_0(4, 2, 1) -> 4, k_0(4, 2, 0) -> 4, k_0(4, 1, 47) -> 4, k_0(4, 1, 46) -> 4, k_0(4, 1, 45) -> 4, k_0(4, 1, 44) -> 4, k_0(4, 1, 43) -> 4, k_0(4, 1, 42) -> 4, k_0(4, 1, 41) -> 4, k_0(4, 1, 40) -> 4, k_0(4, 1, 39) -> 4, k_0(4, 1, 38) -> 4, k_0(4, 1, 4) -> 4, k_0(4, 1, 3) -> 4, k_0(4, 1, 2) -> 4, k_0(4, 1, 1) -> 4, k_0(4, 1, 0) -> 4, k_0(4, 0, 47) -> 4, k_0(4, 0, 46) -> 4, k_0(4, 0, 45) -> 4, k_0(4, 0, 44) -> 4, k_0(4, 0, 43) -> 4, k_0(4, 0, 42) -> 4, k_0(4, 0, 41) -> 4, k_0(4, 0, 40) -> 4, k_0(4, 0, 39) -> 4, k_0(4, 0, 38) -> 4, k_0(4, 0, 4) -> 4, k_0(4, 0, 3) -> 4, k_0(4, 0, 2) -> 4, k_0(4, 0, 1) -> 4, k_0(4, 0, 0) -> 4, k_0(3, 47, 47) -> 4, k_0(3, 47, 46) -> 4, k_0(3, 47, 45) -> 4, k_0(3, 47, 44) -> 4, k_0(3, 47, 43) -> 4, k_0(3, 47, 42) -> 4, k_0(3, 47, 41) -> 4, k_0(3, 47, 40) -> 4, k_0(3, 47, 39) -> 4, k_0(3, 47, 38) -> 4, k_0(3, 47, 4) -> 4, k_0(3, 47, 3) -> 4, k_0(3, 47, 2) -> 4, k_0(3, 47, 1) -> 4, k_0(3, 47, 0) -> 4, k_0(3, 46, 47) -> 4, k_0(3, 46, 46) -> 4, k_0(3, 46, 45) -> 4, k_0(3, 46, 44) -> 4, k_0(3, 46, 43) -> 4, k_0(3, 46, 42) -> 4, k_0(3, 46, 41) -> 4, k_0(3, 46, 40) -> 4, k_0(3, 46, 39) -> 4, k_0(3, 46, 38) -> 4, k_0(3, 46, 4) -> 4, k_0(3, 46, 3) -> 4, k_0(3, 46, 2) -> 4, k_0(3, 46, 1) -> 4, k_0(3, 46, 0) -> 4, k_0(3, 45, 47) -> 4, k_0(3, 45, 46) -> 4, k_0(3, 45, 45) -> 4, k_0(3, 45, 44) -> 4, k_0(3, 45, 43) -> 4, k_0(3, 45, 42) -> 4, k_0(3, 45, 41) -> 4, k_0(3, 45, 40) -> 4, k_0(3, 45, 39) -> 4, k_0(3, 45, 38) -> 4, k_0(3, 45, 4) -> 4, k_0(3, 45, 3) -> 4, k_0(3, 45, 2) -> 4, k_0(3, 45, 1) -> 4, k_0(3, 45, 0) -> 4, k_0(3, 44, 47) -> 4, k_0(3, 44, 46) -> 4, k_0(3, 44, 45) -> 4, k_0(3, 44, 44) -> 4, k_0(3, 44, 43) -> 4, k_0(3, 44, 42) -> 4, k_0(3, 44, 41) -> 4, k_0(3, 44, 40) -> 4, k_0(3, 44, 39) -> 4, k_0(3, 44, 38) -> 4, k_0(3, 44, 4) -> 4, k_0(3, 44, 3) -> 4, k_0(3, 44, 2) -> 4, k_0(3, 44, 1) -> 4, k_0(3, 44, 0) -> 4, k_0(3, 43, 47) -> 4, k_0(3, 43, 46) -> 4, k_0(3, 43, 45) -> 4, k_0(3, 43, 44) -> 4, k_0(3, 43, 43) -> 4, k_0(3, 43, 42) -> 4, k_0(3, 43, 41) -> 4, k_0(3, 43, 40) -> 4, k_0(3, 43, 39) -> 4, k_0(3, 43, 38) -> 4, k_0(3, 43, 4) -> 4, k_0(3, 43, 3) -> 4, k_0(3, 43, 2) -> 4, k_0(3, 43, 1) -> 4, k_0(3, 43, 0) -> 4, k_0(3, 42, 47) -> 4, k_0(3, 42, 46) -> 4, k_0(3, 42, 45) -> 4, k_0(3, 42, 44) -> 4, k_0(3, 42, 43) -> 4, k_0(3, 42, 42) -> 4, k_0(3, 42, 41) -> 4, k_0(3, 42, 40) -> 4, k_0(3, 42, 39) -> 4, k_0(3, 42, 38) -> 4, k_0(3, 42, 4) -> 4, k_0(3, 42, 3) -> 4, k_0(3, 42, 2) -> 4, k_0(3, 42, 1) -> 4, k_0(3, 42, 0) -> 4, k_0(3, 41, 47) -> 4, k_0(3, 41, 46) -> 4, k_0(3, 41, 45) -> 4, k_0(3, 41, 44) -> 4, k_0(3, 41, 43) -> 4, k_0(3, 41, 42) -> 4, k_0(3, 41, 41) -> 4, k_0(3, 41, 40) -> 4, k_0(3, 41, 39) -> 4, k_0(3, 41, 38) -> 4, k_0(3, 41, 4) -> 4, k_0(3, 41, 3) -> 4, k_0(3, 41, 2) -> 4, k_0(3, 41, 1) -> 4, k_0(3, 41, 0) -> 4, k_0(3, 40, 47) -> 4, k_0(3, 40, 46) -> 4, k_0(3, 40, 45) -> 4, k_0(3, 40, 44) -> 4, k_0(3, 40, 43) -> 4, k_0(3, 40, 42) -> 4, k_0(3, 40, 41) -> 4, k_0(3, 40, 40) -> 4, k_0(3, 40, 39) -> 4, k_0(3, 40, 38) -> 4, k_0(3, 40, 4) -> 4, k_0(3, 40, 3) -> 4, k_0(3, 40, 2) -> 4, k_0(3, 40, 1) -> 4, k_0(3, 40, 0) -> 4, k_0(3, 39, 47) -> 4, k_0(3, 39, 46) -> 4, k_0(3, 39, 45) -> 4, k_0(3, 39, 44) -> 4, k_0(3, 39, 43) -> 4, k_0(3, 39, 42) -> 4, k_0(3, 39, 41) -> 4, k_0(3, 39, 40) -> 4, k_0(3, 39, 39) -> 4, k_0(3, 39, 38) -> 4, k_0(3, 39, 4) -> 4, k_0(3, 39, 3) -> 4, k_0(3, 39, 2) -> 4, k_0(3, 39, 1) -> 4, k_0(3, 39, 0) -> 4, k_0(3, 38, 47) -> 4, k_0(3, 38, 46) -> 4, k_0(3, 38, 45) -> 4, k_0(3, 38, 44) -> 4, k_0(3, 38, 43) -> 4, k_0(3, 38, 42) -> 4, k_0(3, 38, 41) -> 4, k_0(3, 38, 40) -> 4, k_0(3, 38, 39) -> 4, k_0(3, 38, 38) -> 4, k_0(3, 38, 4) -> 4, k_0(3, 38, 3) -> 4, k_0(3, 38, 2) -> 4, k_0(3, 38, 1) -> 4, k_0(3, 38, 0) -> 4, k_0(3, 4, 47) -> 4, k_0(3, 4, 46) -> 4, k_0(3, 4, 45) -> 4, k_0(3, 4, 44) -> 4, k_0(3, 4, 43) -> 4, k_0(3, 4, 42) -> 4, k_0(3, 4, 41) -> 4, k_0(3, 4, 40) -> 4, k_0(3, 4, 39) -> 4, k_0(3, 4, 38) -> 4, k_0(3, 4, 4) -> 4, k_0(3, 4, 3) -> 4, k_0(3, 4, 2) -> 4, k_0(3, 4, 1) -> 4, k_0(3, 4, 0) -> 4, k_0(3, 3, 47) -> 4, k_0(3, 3, 46) -> 4, k_0(3, 3, 45) -> 4, k_0(3, 3, 44) -> 4, k_0(3, 3, 43) -> 4, k_0(3, 3, 42) -> 4, k_0(3, 3, 41) -> 4, k_0(3, 3, 40) -> 4, k_0(3, 3, 39) -> 4, k_0(3, 3, 38) -> 4, k_0(3, 3, 4) -> 4, k_0(3, 3, 3) -> 4, k_0(3, 3, 2) -> 4, k_0(3, 3, 1) -> 4, k_0(3, 3, 0) -> 4, k_0(3, 2, 47) -> 4, k_0(3, 2, 46) -> 4, k_0(3, 2, 45) -> 4, k_0(3, 2, 44) -> 4, k_0(3, 2, 43) -> 4, k_0(3, 2, 42) -> 4, k_0(3, 2, 41) -> 4, k_0(3, 2, 40) -> 4, k_0(3, 2, 39) -> 4, k_0(3, 2, 38) -> 4, k_0(3, 2, 4) -> 4, k_0(3, 2, 3) -> 4, k_0(3, 2, 2) -> 4, k_0(3, 2, 1) -> 4, k_0(3, 2, 0) -> 4, k_0(3, 1, 47) -> 4, k_0(3, 1, 46) -> 4, k_0(3, 1, 45) -> 4, k_0(3, 1, 44) -> 4, k_0(3, 1, 43) -> 4, k_0(3, 1, 42) -> 4, k_0(3, 1, 41) -> 4, k_0(3, 1, 40) -> 4, k_0(3, 1, 39) -> 4, k_0(3, 1, 38) -> 4, k_0(3, 1, 4) -> 4, k_0(3, 1, 3) -> 4, k_0(3, 1, 2) -> 4, k_0(3, 1, 1) -> 4, k_0(3, 1, 0) -> 4, k_0(3, 0, 47) -> 4, k_0(3, 0, 46) -> 4, k_0(3, 0, 45) -> 4, k_0(3, 0, 44) -> 4, k_0(3, 0, 43) -> 4, k_0(3, 0, 42) -> 4, k_0(3, 0, 41) -> 4, k_0(3, 0, 40) -> 4, k_0(3, 0, 39) -> 4, k_0(3, 0, 38) -> 4, k_0(3, 0, 4) -> 4, k_0(3, 0, 3) -> 4, k_0(3, 0, 2) -> 4, k_0(3, 0, 1) -> 4, k_0(3, 0, 0) -> 4, k_0(2, 47, 47) -> 4, k_0(2, 47, 46) -> 4, k_0(2, 47, 45) -> 4, k_0(2, 47, 44) -> 4, k_0(2, 47, 43) -> 4, k_0(2, 47, 42) -> 4, k_0(2, 47, 41) -> 4, k_0(2, 47, 40) -> 4, k_0(2, 47, 39) -> 4, k_0(2, 47, 38) -> 4, k_0(2, 47, 4) -> 4, k_0(2, 47, 3) -> 4, k_0(2, 47, 2) -> 4, k_0(2, 47, 1) -> 4, k_0(2, 47, 0) -> 4, k_0(2, 46, 47) -> 4, k_0(2, 46, 46) -> 4, k_0(2, 46, 45) -> 4, k_0(2, 46, 44) -> 4, k_0(2, 46, 43) -> 4, k_0(2, 46, 42) -> 4, k_0(2, 46, 41) -> 4, k_0(2, 46, 40) -> 4, k_0(2, 46, 39) -> 4, k_0(2, 46, 38) -> 4, k_0(2, 46, 4) -> 4, k_0(2, 46, 3) -> 4, k_0(2, 46, 2) -> 4, k_0(2, 46, 1) -> 4, k_0(2, 46, 0) -> 4, k_0(2, 45, 47) -> 4, k_0(2, 45, 46) -> 4, k_0(2, 45, 45) -> 4, k_0(2, 45, 44) -> 4, k_0(2, 45, 43) -> 4, k_0(2, 45, 42) -> 4, k_0(2, 45, 41) -> 4, k_0(2, 45, 40) -> 4, k_0(2, 45, 39) -> 4, k_0(2, 45, 38) -> 4, k_0(2, 45, 4) -> 4, k_0(2, 45, 3) -> 4, k_0(2, 45, 2) -> 4, k_0(2, 45, 1) -> 4, k_0(2, 45, 0) -> 4, k_0(2, 44, 47) -> 4, k_0(2, 44, 46) -> 4, k_0(2, 44, 45) -> 4, k_0(2, 44, 44) -> 4, k_0(2, 44, 43) -> 4, k_0(2, 44, 42) -> 4, k_0(2, 44, 41) -> 4, k_0(2, 44, 40) -> 4, k_0(2, 44, 39) -> 4, k_0(2, 44, 38) -> 4, k_0(2, 44, 4) -> 4, k_0(2, 44, 3) -> 4, k_0(2, 44, 2) -> 4, k_0(2, 44, 1) -> 4, k_0(2, 44, 0) -> 4, k_0(2, 43, 47) -> 4, k_0(2, 43, 46) -> 4, k_0(2, 43, 45) -> 4, k_0(2, 43, 44) -> 4, k_0(2, 43, 43) -> 4, k_0(2, 43, 42) -> 4, k_0(2, 43, 41) -> 4, k_0(2, 43, 40) -> 4, k_0(2, 43, 39) -> 4, k_0(2, 43, 38) -> 4, k_0(2, 43, 4) -> 4, k_0(2, 43, 3) -> 4, k_0(2, 43, 2) -> 4, k_0(2, 43, 1) -> 4, k_0(2, 43, 0) -> 4, k_0(2, 42, 47) -> 4, k_0(2, 42, 46) -> 4, k_0(2, 42, 45) -> 4, k_0(2, 42, 44) -> 4, k_0(2, 42, 43) -> 4, k_0(2, 42, 42) -> 4, k_0(2, 42, 41) -> 4, k_0(2, 42, 40) -> 4, k_0(2, 42, 39) -> 4, k_0(2, 42, 38) -> 4, k_0(2, 42, 4) -> 4, k_0(2, 42, 3) -> 4, k_0(2, 42, 2) -> 4, k_0(2, 42, 1) -> 4, k_0(2, 42, 0) -> 4, k_0(2, 41, 47) -> 4, k_0(2, 41, 46) -> 4, k_0(2, 41, 45) -> 4, k_0(2, 41, 44) -> 4, k_0(2, 41, 43) -> 4, k_0(2, 41, 42) -> 4, k_0(2, 41, 41) -> 4, k_0(2, 41, 40) -> 4, k_0(2, 41, 39) -> 4, k_0(2, 41, 38) -> 4, k_0(2, 41, 4) -> 4, k_0(2, 41, 3) -> 4, k_0(2, 41, 2) -> 4, k_0(2, 41, 1) -> 4, k_0(2, 41, 0) -> 4, k_0(2, 40, 47) -> 4, k_0(2, 40, 46) -> 4, k_0(2, 40, 45) -> 4, k_0(2, 40, 44) -> 4, k_0(2, 40, 43) -> 4, k_0(2, 40, 42) -> 4, k_0(2, 40, 41) -> 4, k_0(2, 40, 40) -> 4, k_0(2, 40, 39) -> 4, k_0(2, 40, 38) -> 4, k_0(2, 40, 4) -> 4, k_0(2, 40, 3) -> 4, k_0(2, 40, 2) -> 4, k_0(2, 40, 1) -> 4, k_0(2, 40, 0) -> 4, k_0(2, 39, 47) -> 4, k_0(2, 39, 46) -> 4, k_0(2, 39, 45) -> 4, k_0(2, 39, 44) -> 4, k_0(2, 39, 43) -> 4, k_0(2, 39, 42) -> 4, k_0(2, 39, 41) -> 4, k_0(2, 39, 40) -> 4, k_0(2, 39, 39) -> 4, k_0(2, 39, 38) -> 4, k_0(2, 39, 4) -> 4, k_0(2, 39, 3) -> 4, k_0(2, 39, 2) -> 4, k_0(2, 39, 1) -> 4, k_0(2, 39, 0) -> 4, k_0(2, 38, 47) -> 4, k_0(2, 38, 46) -> 4, k_0(2, 38, 45) -> 4, k_0(2, 38, 44) -> 4, k_0(2, 38, 43) -> 4, k_0(2, 38, 42) -> 4, k_0(2, 38, 41) -> 4, k_0(2, 38, 40) -> 4, k_0(2, 38, 39) -> 4, k_0(2, 38, 38) -> 4, k_0(2, 38, 4) -> 4, k_0(2, 38, 3) -> 4, k_0(2, 38, 2) -> 4, k_0(2, 38, 1) -> 4, k_0(2, 38, 0) -> 4, k_0(2, 4, 47) -> 4, k_0(2, 4, 46) -> 4, k_0(2, 4, 45) -> 4, k_0(2, 4, 44) -> 4, k_0(2, 4, 43) -> 4, k_0(2, 4, 42) -> 4, k_0(2, 4, 41) -> 4, k_0(2, 4, 40) -> 4, k_0(2, 4, 39) -> 4, k_0(2, 4, 38) -> 4, k_0(2, 4, 4) -> 4, k_0(2, 4, 3) -> 4, k_0(2, 4, 2) -> 4, k_0(2, 4, 1) -> 4, k_0(2, 4, 0) -> 4, k_0(2, 3, 47) -> 4, k_0(2, 3, 46) -> 4, k_0(2, 3, 45) -> 4, k_0(2, 3, 44) -> 4, k_0(2, 3, 43) -> 4, k_0(2, 3, 42) -> 4, k_0(2, 3, 41) -> 4, k_0(2, 3, 40) -> 4, k_0(2, 3, 39) -> 4, k_0(2, 3, 38) -> 4, k_0(2, 3, 4) -> 4, k_0(2, 3, 3) -> 4, k_0(2, 3, 2) -> 4, k_0(2, 3, 1) -> 4, k_0(2, 3, 0) -> 4, k_0(2, 2, 47) -> 4, k_0(2, 2, 46) -> 4, k_0(2, 2, 45) -> 4, k_0(2, 2, 44) -> 4, k_0(2, 2, 43) -> 4, k_0(2, 2, 42) -> 4, k_0(2, 2, 41) -> 4, k_0(2, 2, 40) -> 4, k_0(2, 2, 39) -> 4, k_0(2, 2, 38) -> 4, k_0(2, 2, 4) -> 4, k_0(2, 2, 3) -> 4, k_0(2, 2, 2) -> 4, k_0(2, 2, 1) -> 4, k_0(2, 2, 0) -> 4, k_0(2, 1, 47) -> 4, k_0(2, 1, 46) -> 4, k_0(2, 1, 45) -> 4, k_0(2, 1, 44) -> 4, k_0(2, 1, 43) -> 4, k_0(2, 1, 42) -> 4, k_0(2, 1, 41) -> 4, k_0(2, 1, 40) -> 4, k_0(2, 1, 39) -> 4, k_0(2, 1, 38) -> 4, k_0(2, 1, 4) -> 4, k_0(2, 1, 3) -> 4, k_0(2, 1, 2) -> 4, k_0(2, 1, 1) -> 4, k_0(2, 1, 0) -> 4, k_0(2, 0, 47) -> 4, k_0(2, 0, 46) -> 4, k_0(2, 0, 45) -> 4, k_0(2, 0, 44) -> 4, k_0(2, 0, 43) -> 4, k_0(2, 0, 42) -> 4, k_0(2, 0, 41) -> 4, k_0(2, 0, 40) -> 4, k_0(2, 0, 39) -> 4, k_0(2, 0, 38) -> 4, k_0(2, 0, 4) -> 4, k_0(2, 0, 3) -> 4, k_0(2, 0, 2) -> 4, k_0(2, 0, 1) -> 4, k_0(2, 0, 0) -> 4, k_0(1, 47, 47) -> 4, k_0(1, 47, 46) -> 4, k_0(1, 47, 45) -> 4, k_0(1, 47, 44) -> 4, k_0(1, 47, 43) -> 4, k_0(1, 47, 42) -> 4, k_0(1, 47, 41) -> 4, k_0(1, 47, 40) -> 4, k_0(1, 47, 39) -> 4, k_0(1, 47, 38) -> 4, k_0(1, 47, 4) -> 4, k_0(1, 47, 3) -> 4, k_0(1, 47, 2) -> 4, k_0(1, 47, 1) -> 4, k_0(1, 47, 0) -> 4, k_0(1, 46, 47) -> 4, k_0(1, 46, 46) -> 4, k_0(1, 46, 45) -> 4, k_0(1, 46, 44) -> 4, k_0(1, 46, 43) -> 4, k_0(1, 46, 42) -> 4, k_0(1, 46, 41) -> 4, k_0(1, 46, 40) -> 4, k_0(1, 46, 39) -> 4, k_0(1, 46, 38) -> 4, k_0(1, 46, 4) -> 4, k_0(1, 46, 3) -> 4, k_0(1, 46, 2) -> 4, k_0(1, 46, 1) -> 4, k_0(1, 46, 0) -> 4, k_0(1, 45, 47) -> 4, k_0(1, 45, 46) -> 4, k_0(1, 45, 45) -> 4, k_0(1, 45, 44) -> 4, k_0(1, 45, 43) -> 4, k_0(1, 45, 42) -> 4, k_0(1, 45, 41) -> 4, k_0(1, 45, 40) -> 4, k_0(1, 45, 39) -> 4, k_0(1, 45, 38) -> 4, k_0(1, 45, 4) -> 4, k_0(1, 45, 3) -> 4, k_0(1, 45, 2) -> 4, k_0(1, 45, 1) -> 4, k_0(1, 45, 0) -> 4, k_0(1, 44, 47) -> 4, k_0(1, 44, 46) -> 4, k_0(1, 44, 45) -> 4, k_0(1, 44, 44) -> 4, k_0(1, 44, 43) -> 4, k_0(1, 44, 42) -> 4, k_0(1, 44, 41) -> 4, k_0(1, 44, 40) -> 4, k_0(1, 44, 39) -> 4, k_0(1, 44, 38) -> 4, k_0(1, 44, 4) -> 4, k_0(1, 44, 3) -> 4, k_0(1, 44, 2) -> 4, k_0(1, 44, 1) -> 4, k_0(1, 44, 0) -> 4, k_0(1, 43, 47) -> 4, k_0(1, 43, 46) -> 4, k_0(1, 43, 45) -> 4, k_0(1, 43, 44) -> 4, k_0(1, 43, 43) -> 4, k_0(1, 43, 42) -> 4, k_0(1, 43, 41) -> 4, k_0(1, 43, 40) -> 4, k_0(1, 43, 39) -> 4, k_0(1, 43, 38) -> 4, k_0(1, 43, 4) -> 4, k_0(1, 43, 3) -> 4, k_0(1, 43, 2) -> 4, k_0(1, 43, 1) -> 4, k_0(1, 43, 0) -> 4, k_0(1, 42, 47) -> 4, k_0(1, 42, 46) -> 4, k_0(1, 42, 45) -> 4, k_0(1, 42, 44) -> 4, k_0(1, 42, 43) -> 4, k_0(1, 42, 42) -> 4, k_0(1, 42, 41) -> 4, k_0(1, 42, 40) -> 4, k_0(1, 42, 39) -> 4, k_0(1, 42, 38) -> 4, k_0(1, 42, 4) -> 4, k_0(1, 42, 3) -> 4, k_0(1, 42, 2) -> 4, k_0(1, 42, 1) -> 4, k_0(1, 42, 0) -> 4, k_0(1, 41, 47) -> 4, k_0(1, 41, 46) -> 4, k_0(1, 41, 45) -> 4, k_0(1, 41, 44) -> 4, k_0(1, 41, 43) -> 4, k_0(1, 41, 42) -> 4, k_0(1, 41, 41) -> 4, k_0(1, 41, 40) -> 4, k_0(1, 41, 39) -> 4, k_0(1, 41, 38) -> 4, k_0(1, 41, 4) -> 4, k_0(1, 41, 3) -> 4, k_0(1, 41, 2) -> 4, k_0(1, 41, 1) -> 4, k_0(1, 41, 0) -> 4, k_0(1, 40, 47) -> 4, k_0(1, 40, 46) -> 4, k_0(1, 40, 45) -> 4, k_0(1, 40, 44) -> 4, k_0(1, 40, 43) -> 4, k_0(1, 40, 42) -> 4, k_0(1, 40, 41) -> 4, k_0(1, 40, 40) -> 4, k_0(1, 40, 39) -> 4, k_0(1, 40, 38) -> 4, k_0(1, 40, 4) -> 4, k_0(1, 40, 3) -> 4, k_0(1, 40, 2) -> 4, k_0(1, 40, 1) -> 4, k_0(1, 40, 0) -> 4, k_0(1, 39, 47) -> 4, k_0(1, 39, 46) -> 4, k_0(1, 39, 45) -> 4, k_0(1, 39, 44) -> 4, k_0(1, 39, 43) -> 4, k_0(1, 39, 42) -> 4, k_0(1, 39, 41) -> 4, k_0(1, 39, 40) -> 4, k_0(1, 39, 39) -> 4, k_0(1, 39, 38) -> 4, k_0(1, 39, 4) -> 4, k_0(1, 39, 3) -> 4, k_0(1, 39, 2) -> 4, k_0(1, 39, 1) -> 4, k_0(1, 39, 0) -> 4, k_0(1, 38, 47) -> 4, k_0(1, 38, 46) -> 4, k_0(1, 38, 45) -> 4, k_0(1, 38, 44) -> 4, k_0(1, 38, 43) -> 4, k_0(1, 38, 42) -> 4, k_0(1, 38, 41) -> 4, k_0(1, 38, 40) -> 4, k_0(1, 38, 39) -> 4, k_0(1, 38, 38) -> 4, k_0(1, 38, 4) -> 4, k_0(1, 38, 3) -> 4, k_0(1, 38, 2) -> 4, k_0(1, 38, 1) -> 4, k_0(1, 38, 0) -> 4, k_0(1, 4, 47) -> 4, k_0(1, 4, 46) -> 4, k_0(1, 4, 45) -> 4, k_0(1, 4, 44) -> 4, k_0(1, 4, 43) -> 4, k_0(1, 4, 42) -> 4, k_0(1, 4, 41) -> 4, k_0(1, 4, 40) -> 4, k_0(1, 4, 39) -> 4, k_0(1, 4, 38) -> 4, k_0(1, 4, 4) -> 4, k_0(1, 4, 3) -> 4, k_0(1, 4, 2) -> 4, k_0(1, 4, 1) -> 4, k_0(1, 4, 0) -> 4, k_0(1, 3, 47) -> 4, k_0(1, 3, 46) -> 4, k_0(1, 3, 45) -> 4, k_0(1, 3, 44) -> 4, k_0(1, 3, 43) -> 4, k_0(1, 3, 42) -> 4, k_0(1, 3, 41) -> 4, k_0(1, 3, 40) -> 4, k_0(1, 3, 39) -> 4, k_0(1, 3, 38) -> 4, k_0(1, 3, 4) -> 4, k_0(1, 3, 3) -> 4, k_0(1, 3, 2) -> 4, k_0(1, 3, 1) -> 4, k_0(1, 3, 0) -> 4, k_0(1, 2, 47) -> 4, k_0(1, 2, 46) -> 4, k_0(1, 2, 45) -> 4, k_0(1, 2, 44) -> 4, k_0(1, 2, 43) -> 4, k_0(1, 2, 42) -> 4, k_0(1, 2, 41) -> 4, k_0(1, 2, 40) -> 4, k_0(1, 2, 39) -> 4, k_0(1, 2, 38) -> 4, k_0(1, 2, 4) -> 4, k_0(1, 2, 3) -> 4, k_0(1, 2, 2) -> 4, k_0(1, 2, 1) -> 4, k_0(1, 2, 0) -> 4, k_0(1, 1, 47) -> 4, k_0(1, 1, 46) -> 4, k_0(1, 1, 45) -> 4, k_0(1, 1, 44) -> 4, k_0(1, 1, 43) -> 4, k_0(1, 1, 42) -> 4, k_0(1, 1, 41) -> 4, k_0(1, 1, 40) -> 4, k_0(1, 1, 39) -> 4, k_0(1, 1, 38) -> 4, k_0(1, 1, 4) -> 4, k_0(1, 1, 3) -> 4, k_0(1, 1, 2) -> 4, k_0(1, 1, 1) -> 4, k_0(1, 1, 0) -> 4, k_0(1, 0, 47) -> 4, k_0(1, 0, 46) -> 4, k_0(1, 0, 45) -> 4, k_0(1, 0, 44) -> 4, k_0(1, 0, 43) -> 4, k_0(1, 0, 42) -> 4, k_0(1, 0, 41) -> 4, k_0(1, 0, 40) -> 4, k_0(1, 0, 39) -> 4, k_0(1, 0, 38) -> 4, k_0(1, 0, 4) -> 4, k_0(1, 0, 3) -> 4, k_0(1, 0, 2) -> 4, k_0(1, 0, 1) -> 4, k_0(1, 0, 0) -> 4, k_0(0, 47, 47) -> 4, k_0(0, 47, 46) -> 4, k_0(0, 47, 45) -> 4, k_0(0, 47, 44) -> 4, k_0(0, 47, 43) -> 4, k_0(0, 47, 42) -> 4, k_0(0, 47, 41) -> 4, k_0(0, 47, 40) -> 4, k_0(0, 47, 39) -> 4, k_0(0, 47, 38) -> 4, k_0(0, 47, 4) -> 4, k_0(0, 47, 3) -> 4, k_0(0, 47, 2) -> 4, k_0(0, 47, 1) -> 4, k_0(0, 47, 0) -> 4, k_0(0, 46, 47) -> 4, k_0(0, 46, 46) -> 4, k_0(0, 46, 45) -> 4, k_0(0, 46, 44) -> 4, k_0(0, 46, 43) -> 4, k_0(0, 46, 42) -> 4, k_0(0, 46, 41) -> 4, k_0(0, 46, 40) -> 4, k_0(0, 46, 39) -> 4, k_0(0, 46, 38) -> 4, k_0(0, 46, 4) -> 4, k_0(0, 46, 3) -> 4, k_0(0, 46, 2) -> 4, k_0(0, 46, 1) -> 4, k_0(0, 46, 0) -> 4, k_0(0, 45, 47) -> 4, k_0(0, 45, 46) -> 4, k_0(0, 45, 45) -> 4, k_0(0, 45, 44) -> 4, k_0(0, 45, 43) -> 4, k_0(0, 45, 42) -> 4, k_0(0, 45, 41) -> 4, k_0(0, 45, 40) -> 4, k_0(0, 45, 39) -> 4, k_0(0, 45, 38) -> 4, k_0(0, 45, 4) -> 4, k_0(0, 45, 3) -> 4, k_0(0, 45, 2) -> 4, k_0(0, 45, 1) -> 4, k_0(0, 45, 0) -> 4, k_0(0, 44, 47) -> 4, k_0(0, 44, 46) -> 4, k_0(0, 44, 45) -> 4, k_0(0, 44, 44) -> 4, k_0(0, 44, 43) -> 4, k_0(0, 44, 42) -> 4, k_0(0, 44, 41) -> 4, k_0(0, 44, 40) -> 4, k_0(0, 44, 39) -> 4, k_0(0, 44, 38) -> 4, k_0(0, 44, 4) -> 4, k_0(0, 44, 3) -> 4, k_0(0, 44, 2) -> 4, k_0(0, 44, 1) -> 4, k_0(0, 44, 0) -> 4, k_0(0, 43, 47) -> 4, k_0(0, 43, 46) -> 4, k_0(0, 43, 45) -> 4, k_0(0, 43, 44) -> 4, k_0(0, 43, 43) -> 4, k_0(0, 43, 42) -> 4, k_0(0, 43, 41) -> 4, k_0(0, 43, 40) -> 4, k_0(0, 43, 39) -> 4, k_0(0, 43, 38) -> 4, k_0(0, 43, 4) -> 4, k_0(0, 43, 3) -> 4, k_0(0, 43, 2) -> 4, k_0(0, 43, 1) -> 4, k_0(0, 43, 0) -> 4, k_0(0, 42, 47) -> 4, k_0(0, 42, 46) -> 4, k_0(0, 42, 45) -> 4, k_0(0, 42, 44) -> 4, k_0(0, 42, 43) -> 4, k_0(0, 42, 42) -> 4, k_0(0, 42, 41) -> 4, k_0(0, 42, 40) -> 4, k_0(0, 42, 39) -> 4, k_0(0, 42, 38) -> 4, k_0(0, 42, 4) -> 4, k_0(0, 42, 3) -> 4, k_0(0, 42, 2) -> 4, k_0(0, 42, 1) -> 4, k_0(0, 42, 0) -> 4, k_0(0, 41, 47) -> 4, k_0(0, 41, 46) -> 4, k_0(0, 41, 45) -> 4, k_0(0, 41, 44) -> 4, k_0(0, 41, 43) -> 4, k_0(0, 41, 42) -> 4, k_0(0, 41, 41) -> 4, k_0(0, 41, 40) -> 4, k_0(0, 41, 39) -> 4, k_0(0, 41, 38) -> 4, k_0(0, 41, 4) -> 4, k_0(0, 41, 3) -> 4, k_0(0, 41, 2) -> 4, k_0(0, 41, 1) -> 4, k_0(0, 41, 0) -> 4, k_0(0, 40, 47) -> 4, k_0(0, 40, 46) -> 4, k_0(0, 40, 45) -> 4, k_0(0, 40, 44) -> 4, k_0(0, 40, 43) -> 4, k_0(0, 40, 42) -> 4, k_0(0, 40, 41) -> 4, k_0(0, 40, 40) -> 4, k_0(0, 40, 39) -> 4, k_0(0, 40, 38) -> 4, k_0(0, 40, 4) -> 4, k_0(0, 40, 3) -> 4, k_0(0, 40, 2) -> 4, k_0(0, 40, 1) -> 4, k_0(0, 40, 0) -> 4, k_0(0, 39, 47) -> 4, k_0(0, 39, 46) -> 4, k_0(0, 39, 45) -> 4, k_0(0, 39, 44) -> 4, k_0(0, 39, 43) -> 4, k_0(0, 39, 42) -> 4, k_0(0, 39, 41) -> 4, k_0(0, 39, 40) -> 4, k_0(0, 39, 39) -> 4, k_0(0, 39, 38) -> 4, k_0(0, 39, 4) -> 4, k_0(0, 39, 3) -> 4, k_0(0, 39, 2) -> 4, k_0(0, 39, 1) -> 4, k_0(0, 39, 0) -> 4, k_0(0, 38, 47) -> 4, k_0(0, 38, 46) -> 4, k_0(0, 38, 45) -> 4, k_0(0, 38, 44) -> 4, k_0(0, 38, 43) -> 4, k_0(0, 38, 42) -> 4, k_0(0, 38, 41) -> 4, k_0(0, 38, 40) -> 4, k_0(0, 38, 39) -> 4, k_0(0, 38, 38) -> 4, k_0(0, 38, 4) -> 4, k_0(0, 38, 3) -> 4, k_0(0, 38, 2) -> 4, k_0(0, 38, 1) -> 4, k_0(0, 38, 0) -> 4, k_0(0, 4, 47) -> 4, k_0(0, 4, 46) -> 4, k_0(0, 4, 45) -> 4, k_0(0, 4, 44) -> 4, k_0(0, 4, 43) -> 4, k_0(0, 4, 42) -> 4, k_0(0, 4, 41) -> 4, k_0(0, 4, 40) -> 4, k_0(0, 4, 39) -> 4, k_0(0, 4, 38) -> 4, k_0(0, 4, 4) -> 4, k_0(0, 4, 3) -> 4, k_0(0, 4, 2) -> 4, k_0(0, 4, 1) -> 4, k_0(0, 4, 0) -> 4, k_0(0, 3, 47) -> 4, k_0(0, 3, 46) -> 4, k_0(0, 3, 45) -> 4, k_0(0, 3, 44) -> 4, k_0(0, 3, 43) -> 4, k_0(0, 3, 42) -> 4, k_0(0, 3, 41) -> 4, k_0(0, 3, 40) -> 4, k_0(0, 3, 39) -> 4, k_0(0, 3, 38) -> 4, k_0(0, 3, 4) -> 4, k_0(0, 3, 3) -> 4, k_0(0, 3, 2) -> 4, k_0(0, 3, 1) -> 4, k_0(0, 3, 0) -> 4, k_0(0, 2, 47) -> 4, k_0(0, 2, 46) -> 4, k_0(0, 2, 45) -> 4, k_0(0, 2, 44) -> 4, k_0(0, 2, 43) -> 4, k_0(0, 2, 42) -> 4, k_0(0, 2, 41) -> 4, k_0(0, 2, 40) -> 4, k_0(0, 2, 39) -> 4, k_0(0, 2, 38) -> 4, k_0(0, 2, 4) -> 4, k_0(0, 2, 3) -> 4, k_0(0, 2, 2) -> 4, k_0(0, 2, 1) -> 4, k_0(0, 2, 0) -> 4, k_0(0, 1, 47) -> 4, k_0(0, 1, 46) -> 4, k_0(0, 1, 45) -> 4, k_0(0, 1, 44) -> 4, k_0(0, 1, 43) -> 4, k_0(0, 1, 42) -> 4, k_0(0, 1, 41) -> 4, k_0(0, 1, 40) -> 4, k_0(0, 1, 39) -> 4, k_0(0, 1, 38) -> 4, k_0(0, 1, 4) -> 4, k_0(0, 1, 3) -> 4, k_0(0, 1, 2) -> 4, k_0(0, 1, 1) -> 4, k_0(0, 1, 0) -> 4, k_0(0, 0, 47) -> 4, k_0(0, 0, 46) -> 4, k_0(0, 0, 45) -> 4, k_0(0, 0, 44) -> 4, k_0(0, 0, 43) -> 4, k_0(0, 0, 42) -> 4, k_0(0, 0, 41) -> 4, k_0(0, 0, 40) -> 4, k_0(0, 0, 39) -> 4, k_0(0, 0, 38) -> 4, k_0(0, 0, 4) -> 4, k_0(0, 0, 3) -> 4, k_0(0, 0, 2) -> 4, k_0(0, 0, 1) -> 4, k_0(0, 0, 0) -> 4, f_2(47) -> 46 | 41 | 4 | 3 | 2, f_2(46) -> 46 | 41 | 4 | 3 | 2, f_2(45) -> 46 | 41 | 4 | 3 | 2, f_2(44) -> 46 | 41 | 4 | 3 | 2, f_2(43) -> 46 | 41 | 4 | 3 | 2, f_2(42) -> 46 | 41 | 4 | 3 | 2, f_2(41) -> 46 | 41 | 4 | 3 | 2, f_2(40) -> 46 | 41 | 4 | 3 | 2, f_2(38) -> 46 | 41 | 4 | 3 | 2, f_2(4) -> 46 | 41 | 4 | 3 | 2, f_2(1) -> 46 | 41 | 4 | 3 | 2, f_1(47) -> 41 | 4 | 3, f_1(46) -> 41 | 4 | 3, f_1(45) -> 41 | 4 | 3, f_1(44) -> 41 | 4 | 3, f_1(43) -> 41 | 4 | 3, f_1(42) -> 41 | 4 | 3, f_1(41) -> 41 | 4 | 3, f_1(40) -> 41 | 4 | 3, f_1(39) -> 41 | 4 | 3, f_1(38) -> 41 | 4 | 3, f_1(4) -> 41 | 4 | 3, f_1(3) -> 41 | 4 | 3, f_1(2) -> 41 | 4 | 3, f_1(1) -> 41 | 4 | 3, f_1(0) -> 41 | 4 | 3, f_0(47) -> 3, f_0(46) -> 3, f_0(45) -> 3, f_0(44) -> 3, f_0(43) -> 3, f_0(42) -> 3, f_0(41) -> 3, f_0(40) -> 3, f_0(39) -> 3, f_0(38) -> 3, f_0(4) -> 3, f_0(3) -> 3, f_0(2) -> 3, f_0(1) -> 3, f_0(0) -> 3, a_2() -> 2, a_1() -> 2, a_0() -> 2, h_2(46) -> 45 | 40 | 4 | 1, h_2(2) -> 45 | 40 | 4 | 1, h_1(47) -> 40 | 4 | 1, h_1(46) -> 40 | 4 | 1, h_1(45) -> 40 | 4 | 1, h_1(44) -> 40 | 4 | 1, h_1(43) -> 40 | 4 | 1, h_1(42) -> 40 | 4 | 1, h_1(41) -> 40 | 4 | 1, h_1(40) -> 40 | 4 | 1, h_1(39) -> 40 | 4 | 1, h_1(38) -> 40 | 4 | 1, h_1(4) -> 40 | 4 | 1, h_1(3) -> 40 | 4 | 1, h_1(2) -> 40 | 4 | 1, h_1(1) -> 40 | 4 | 1, h_1(0) -> 40 | 4 | 1, h_0(47) -> 1, h_0(46) -> 1, h_0(45) -> 1, h_0(44) -> 1, h_0(43) -> 1, h_0(42) -> 1, h_0(41) -> 1, h_0(40) -> 1, h_0(39) -> 1, h_0(38) -> 1, h_0(4) -> 1, h_0(3) -> 1, h_0(2) -> 1, h_0(1) -> 1, h_0(0) -> 1, g_2(47) -> 47 | 44 | 43 | 42 | 41 | 40 | 39 | 38 | 3 | 1 | 0, g_2(45) -> 47 | 44 | 43 | 42 | 41 | 40 | 39 | 38 | 3 | 1 | 0, g_2(44) -> 47 | 44 | 43 | 42 | 41 | 40 | 39 | 38 | 3 | 1 | 0, g_2(43) -> 47 | 44 | 43 | 42 | 41 | 40 | 39 | 38 | 3 | 1 | 0, g_2(40) -> 47 | 44 | 43 | 42 | 41 | 40 | 39 | 38 | 3 | 1 | 0, g_1(47) -> 47 | 44 | 43 | 42 | 41 | 40 | 39 | 38 | 3 | 1 | 0, g_1(46) -> 39 | 3 | 0, g_1(45) -> 47 | 44 | 43 | 42 | 41 | 40 | 39 | 38 | 3 | 1 | 0, g_1(44) -> 47 | 44 | 43 | 42 | 41 | 40 | 39 | 38 | 3 | 1 | 0, g_1(43) -> 47 | 44 | 43 | 42 | 41 | 40 | 39 | 38 | 3 | 1 | 0, g_1(42) -> 43 | 41 | 40 | 38 | 1 | 0, g_1(41) -> 39 | 3 | 0, g_1(40) -> 47 | 44 | 43 | 42 | 41 | 40 | 39 | 38 | 3 | 1 | 0, g_1(38) -> 43 | 41 | 40 | 38 | 1 | 0, g_1(4) -> 39 | 3 | 0, g_1(1) -> 43 | 41 | 40 | 38 | 1 | 0, g_0(47) -> 0, g_0(46) -> 0, g_0(45) -> 0, g_0(44) -> 0, g_0(43) -> 0, g_0(42) -> 0, g_0(41) -> 0, g_0(40) -> 0, g_0(39) -> 0, g_0(38) -> 0, g_0(4) -> 0, g_0(3) -> 0, g_0(2) -> 0, g_0(1) -> 0, g_0(0) -> 0 } Strict: {} Qed