Problem:
g(x,x,x) -> g(c(),d(),e())
g(x,y,x) -> g(c(),d(),e())
s(f(x,y)) -> f(y,f(s(s(x)),a()))
h(h(x,a()),y) -> h(h(a(),y),h(a(),x))
f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b())))
f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b()))
h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a())))
f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y))
s(y) -> b()
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {14,9,8,7,6}
transitions:
g0(14,1,17) -> 6*
g0(14,16,15) -> 6*
g0(4,14,15) -> 6*
g0(17,1,5) -> 6*
g0(15,16,4) -> 6*
g0(5,14,4) -> 6*
g0(5,4,1) -> 6*
g0(3,4,2) -> 6*
g0(16,3,16) -> 6*
g0(4,1,17) -> 6*
g0(14,3,17) -> 6*
g0(17,3,5) -> 6*
g0(4,16,15) -> 6*
g0(5,16,4) -> 6*
g0(2,1,5) -> 6*
g0(16,5,16) -> 6*
g0(14,14,3) -> 6*
g0(4,3,17) -> 6*
g0(14,5,17) -> 6*
g0(17,5,5) -> 6*
g0(1,3,16) -> 6*
g0(15,1,15) -> 6*
g0(2,3,5) -> 6*
g0(16,1,4) -> 6*
g0(3,14,14) -> 6*
g0(14,16,3) -> 6*
g0(4,14,3) -> 6*
g0(4,5,17) -> 6*
g0(1,5,16) -> 6*
g0(5,1,15) -> 6*
g0(15,3,15) -> 6*
g0(2,5,5) -> 6*
g0(3,1,16) -> 6*
g0(16,3,4) -> 6*
g0(3,16,14) -> 6*
g0(4,16,3) -> 6*
g0(1,1,4) -> 6*
g0(15,14,1) -> 6*
g0(5,3,15) -> 6*
g0(15,5,15) -> 6*
g0(16,5,4) -> 6*
g0(14,1,14) -> 6*
g0(1,3,4) -> 6*
g0(15,1,3) -> 6*
g0(15,16,1) -> 6*
g0(5,14,1) -> 6*
g0(3,14,2) -> 6*
g0(5,5,15) -> 6*
g0(14,3,14) -> 6*
g0(4,1,14) -> 6*
g0(1,5,4) -> 6*
g0(5,1,3) -> 6*
g0(15,3,3) -> 6*
g0(5,16,1) -> 6*
g0(3,16,2) -> 6*
g0(16,15,16) -> 6*
g0(14,15,17) -> 6*
g0(14,5,14) -> 6*
g0(17,15,5) -> 6*
g0(4,3,14) -> 6*
g0(5,3,3) -> 6*
g0(15,5,3) -> 6*
g0(16,1,1) -> 6*
g0(16,17,16) -> 6*
g0(14,1,2) -> 6*
g0(4,15,17) -> 6*
g0(14,17,17) -> 6*
g0(17,17,5) -> 6*
g0(4,5,14) -> 6*
g0(5,5,3) -> 6*
g0(1,15,16) -> 6*
g0(2,15,5) -> 6*
g0(16,3,1) -> 6*
g0(4,1,2) -> 6*
g0(14,3,2) -> 6*
g0(4,17,17) -> 6*
g0(1,1,1) -> 6*
g0(1,17,16) -> 6*
g0(15,15,15) -> 6*
g0(2,17,5) -> 6*
g0(16,15,4) -> 6*
g0(16,5,1) -> 6*
g0(4,3,2) -> 6*
g0(14,5,2) -> 6*
g0(1,3,1) -> 6*
g0(17,2,16) -> 6*
g0(15,2,17) -> 6*
g0(5,15,15) -> 6*
g0(15,17,15) -> 6*
g0(16,17,4) -> 6*
g0(4,5,2) -> 6*
g0(1,15,4) -> 6*
g0(1,5,1) -> 6*
g0(17,4,16) -> 6*
g0(5,2,17) -> 6*
g0(15,4,17) -> 6*
g0(5,17,15) -> 6*
g0(2,2,16) -> 6*
g0(3,2,5) -> 6*
g0(14,15,14) -> 6*
g0(1,17,4) -> 6*
g0(15,15,3) -> 6*
g0(5,4,17) -> 6*
g0(2,4,16) -> 6*
g0(16,2,15) -> 6*
g0(3,4,5) -> 6*
g0(14,17,14) -> 6*
g0(17,2,4) -> 6*
g0(4,15,14) -> 6*
g0(15,17,3) -> 6*
g0(5,15,3) -> 6*
g0(16,4,15) -> 6*
g0(17,4,4) -> 6*
g0(4,17,14) -> 6*
g0(5,17,3) -> 6*
g0(1,2,15) -> 6*
g0(2,2,4) -> 6*
g0(16,15,1) -> 6*
g0(14,15,2) -> 6*
g0(1,4,15) -> 6*
g0(15,2,14) -> 6*
g0(2,4,4) -> 6*
g0(16,2,3) -> 6*
g0(16,17,1) -> 6*
g0(14,17,2) -> 6*
g0(4,15,2) -> 6*
g0(17,14,16) -> 6*
g0(1,15,1) -> 6*
g0(15,14,17) -> 6*
g0(15,4,14) -> 6*
g0(5,2,14) -> 6*
g0(16,4,3) -> 6*
g0(4,17,2) -> 6*
g0(1,2,3) -> 6*
g0(17,16,16) -> 6*
g0(1,17,1) -> 6*
g0(15,16,17) -> 6*
g0(5,14,17) -> 6*
g0(5,4,14) -> 6*
g0(2,14,16) -> 6*
g0(3,14,5) -> 6*
g0(1,4,3) -> 6*
g0(17,2,1) -> 6*
g0(15,2,2) -> 6*
g0(5,16,17) -> 6*
g0(2,16,16) -> 6*
g0(16,14,15) -> 6*
g0(3,16,5) -> 6*
g0(17,14,4) -> 6*
g0(17,4,1) -> 6*
g0(5,2,2) -> 6*
g0(15,4,2) -> 6*
g0(2,2,1) -> 6*
g0(16,1,17) -> 6*
g0(16,16,15) -> 6*
g0(17,16,4) -> 6*
g0(5,4,2) -> 6*
g0(14,1,5) -> 6*
g0(1,14,15) -> 6*
g0(2,14,4) -> 6*
g0(2,4,1) -> 6*
g0(16,3,17) -> 6*
g0(1,1,17) -> 6*
g0(4,1,5) -> 6*
g0(14,3,5) -> 6*
g0(1,16,15) -> 6*
g0(15,14,14) -> 6*
g0(2,16,4) -> 6*
g0(16,14,3) -> 6*
g0(16,5,17) -> 6*
g0(3,3,16) -> 6*
g0(1,3,17) -> 6*
g0(17,1,15) -> 6*
g0(4,3,5) -> 6*
g0(14,5,5) -> 6*
g0(15,16,14) -> 6*
g0(5,14,14) -> 6*
g0(16,16,3) -> 6*
g0(1,14,3) -> 6*
g0(3,5,16) -> 6*
g0(1,5,17) -> 6*
g0(17,3,15) -> 6*
g0(4,5,5) -> 6*
g0(5,16,14) -> 6*
g0(2,1,15) -> 6*
g0(3,1,4) -> 6*
g0(17,14,1) -> 6*
g0(1,16,3) -> 6*
g0(15,14,2) -> 6*
g0(17,5,15) -> 6*
g0(2,3,15) -> 6*
g0(16,1,14) -> 6*
g0(3,3,4) -> 6*
g0(17,1,3) -> 6*
g0(17,16,1) -> 6*
g0(15,16,2) -> 6*
g0(5,14,2) -> 6*
g0(2,14,1) -> 6*
g0(2,5,15) -> 6*
g0(16,3,14) -> 6*
g0(3,5,4) -> 6*
g0(17,3,3) -> 6*
g0(5,16,2) -> 6*
g0(1,1,14) -> 6*
g0(2,1,3) -> 6*
g0(2,16,1) -> 6*
g0(16,15,17) -> 6*
g0(16,5,14) -> 6*
g0(17,5,3) -> 6*
g0(14,15,5) -> 6*
g0(1,3,14) -> 6*
g0(2,3,3) -> 6*
g0(16,1,2) -> 6*
g0(16,17,17) -> 6*
g0(3,15,16) -> 6*
g0(1,15,17) -> 6*
g0(14,17,5) -> 6*
g0(1,5,14) -> 6*
g0(4,15,5) -> 6*
g0(2,5,3) -> 6*
g0(16,3,2) -> 6*
g0(3,1,1) -> 6*
g0(1,1,2) -> 6*
g0(3,17,16) -> 6*
g0(1,17,17) -> 6*
g0(17,15,15) -> 6*
g0(4,17,5) -> 6*
g0(16,5,2) -> 6*
g0(3,3,1) -> 6*
g0(1,3,2) -> 6*
g0(17,2,17) -> 6*
g0(17,17,15) -> 6*
g0(14,2,16) -> 6*
g0(15,2,5) -> 6*
g0(2,15,15) -> 6*
g0(3,15,4) -> 6*
g0(3,5,1) -> 6*
g0(1,5,2) -> 6*
g0(17,4,17) -> 6*
g0(4,2,16) -> 6*
g0(14,4,16) -> 6*
g0(2,2,17) -> 6*
g0(5,2,5) -> 6*
g0(15,4,5) -> 6*
g0(2,17,15) -> 6*
g0(16,15,14) -> 6*
g0(3,17,4) -> 6*
g0(17,15,3) -> 6*
g0(4,4,16) -> 6*
g0(2,4,17) -> 6*
g0(5,4,5) -> 6*
g0(16,17,14) -> 6*
g0(17,17,3) -> 6*
g0(14,2,4) -> 6*
g0(1,15,14) -> 6*
g0(2,15,3) -> 6*
g0(3,2,15) -> 6*
g0(4,2,4) -> 6*
g0(14,4,4) -> 6*
g0(1,17,14) -> 6*
g0(2,17,3) -> 6*
g0(16,15,2) -> 6*
g0(3,4,15) -> 6*
g0(17,2,14) -> 6*
g0(4,4,4) -> 6*
g0(16,17,2) -> 6*
g0(3,15,1) -> 6*
g0(17,14,17) -> 6*
g0(1,15,2) -> 6*
g0(17,4,14) -> 6*
g0(14,14,16) -> 6*
g0(2,2,14) -> 6*
g0(15,14,5) -> 6*
g0(3,2,3) -> 6*
g0(3,17,1) -> 6*
g0(17,16,17) -> 6*
g0(1,17,2) -> 6*
g0(14,16,16) -> 6*
g0(4,14,16) -> 6*
g0(2,14,17) -> 6*
g0(15,16,5) -> 6*
g0(5,14,5) -> 6*
g0(2,4,14) -> 6*
g0(3,4,3) -> 6*
g0(17,2,2) -> 6*
g0(14,2,1) -> 6*
g0(4,16,16) -> 6*
g0(2,16,17) -> 6*
g0(5,16,5) -> 6*
g0(17,4,2) -> 6*
g0(14,14,4) -> 6*
g0(4,2,1) -> 6*
g0(14,4,1) -> 6*
g0(2,2,2) -> 6*
g0(15,1,16) -> 6*
g0(3,14,15) -> 6*
g0(16,1,5) -> 6*
g0(14,16,4) -> 6*
g0(4,14,4) -> 6*
g0(4,4,1) -> 6*
g0(2,4,2) -> 6*
g0(5,1,16) -> 6*
g0(15,3,16) -> 6*
g0(3,1,17) -> 6*
g0(3,16,15) -> 6*
g0(16,3,5) -> 6*
g0(17,14,14) -> 6*
g0(4,16,4) -> 6*
g0(1,1,5) -> 6*
g0(5,3,16) -> 6*
g0(15,5,16) -> 6*
g0(3,3,17) -> 6*
g0(16,5,5) -> 6*
g0(17,16,14) -> 6*
g0(14,1,15) -> 6*
g0(1,3,5) -> 6*
g0(15,1,4) -> 6*
g0(2,14,14) -> 6*
g0(3,14,3) -> 6*
g0(5,5,16) -> 6*
g0(3,5,17) -> 6*
g0(4,1,15) -> 6*
g0(14,3,15) -> 6*
g0(1,5,5) -> 6*
g0(2,1,16) -> 6*
g0(5,1,4) -> 6*
g0(2,16,14) -> 6*
g0(15,3,4) -> 6*
g0(3,16,3) -> 6*
g0(17,14,2) -> 6*
g0(14,14,1) -> 6*
g0(4,3,15) -> 6*
g0(14,5,15) -> 6*
g0(5,3,4) -> 6*
g0(15,5,4) -> 6*
g0(17,16,2) -> 6*
g0(14,1,3) -> 6*
g0(14,16,1) -> 6*
g0(4,14,1) -> 6*
g0(2,14,2) -> 6*
g0(4,5,15) -> 6*
g0(5,5,4) -> 6*
g0(3,1,14) -> 6*
g0(4,1,3) -> 6*
g0(14,3,3) -> 6*
g0(4,16,1) -> 6*
g0(2,16,2) -> 6*
g0(15,15,16) -> 6*
g0(3,3,14) -> 6*
g0(16,15,5) -> 6*
g0(4,3,3) -> 6*
g0(14,5,3) -> 6*
g0(15,1,1) -> 6*
g0(5,15,16) -> 6*
g0(15,17,16) -> 6*
g0(3,15,17) -> 6*
g0(3,5,14) -> 6*
g0(16,17,5) -> 6*
g0(4,5,3) -> 6*
g0(1,15,5) -> 6*
g0(5,1,1) -> 6*
g0(15,3,1) -> 6*
g0(3,1,2) -> 6*
g0(5,17,16) -> 6*
g0(3,17,17) -> 6*
g0(14,15,15) -> 6*
g0(1,17,5) -> 6*
g0(15,15,4) -> 6*
g0(5,3,1) -> 6*
g0(15,5,1) -> 6*
g0(3,3,2) -> 6*
g0(16,2,16) -> 6*
g0(14,2,17) -> 6*
g0(4,15,15) -> 6*
g0(14,17,15) -> 6*
g0(17,2,5) -> 6*
g0(5,15,4) -> 6*
g0(15,17,4) -> 6*
g0(5,5,1) -> 6*
g0(3,5,2) -> 6*
g0(16,4,16) -> 6*
g0(4,2,17) -> 6*
g0(14,4,17) -> 6*
g0(4,17,15) -> 6*
g0(17,4,5) -> 6*
g0(5,17,4) -> 6*
g0(1,2,16) -> 6*
g0(2,2,5) -> 6*
g0(14,15,3) -> 6*
g0(4,4,17) -> 6*
g0(1,4,16) -> 6*
g0(15,2,15) -> 6*
g0(2,4,5) -> 6*
g0(3,15,14) -> 6*
g0(16,2,4) -> 6*
g0(4,15,3) -> 6*
g0(14,17,3) -> 6*
g0(5,2,15) -> 6*
g0(15,4,15) -> 6*
g0(3,17,14) -> 6*
g0(16,4,4) -> 6*
g0(4,17,3) -> 6*
g0(1,2,4) -> 6*
g0(15,15,1) -> 6*
g0(5,4,15) -> 6*
g0(14,2,14) -> 6*
g0(1,4,4) -> 6*
g0(15,2,3) -> 6*
g0(5,15,1) -> 6*
g0(15,17,1) -> 6*
g0(3,15,2) -> 6*
g0(16,14,16) -> 6*
g0(14,14,17) -> 6*
g0(4,2,14) -> 6*
g0(17,14,5) -> 6*
g0(14,4,14) -> 6*
g0(5,2,3) -> 6*
g0(15,4,3) -> 6*
g0(5,17,1) -> 6*
g0(3,17,2) -> 6*
g0(16,16,16) -> 6*
g0(14,16,17) -> 6*
g0(4,14,17) -> 6*
g0(4,4,14) -> 6*
g0(17,16,5) -> 6*
g0(5,4,3) -> 6*
g0(1,14,16) -> 6*
g0(2,14,5) -> 6*
g0(16,2,1) -> 6*
g0(14,2,2) -> 6*
g0(4,16,17) -> 6*
g0(1,16,16) -> 6*
g0(15,14,15) -> 6*
g0(2,16,5) -> 6*
g0(16,14,4) -> 6*
g0(16,4,1) -> 6*
g0(4,2,2) -> 6*
g0(14,4,2) -> 6*
g0(1,2,1) -> 6*
g0(17,1,16) -> 6*
g0(15,1,17) -> 6*
g0(15,16,15) -> 6*
g0(5,14,15) -> 6*
g0(16,16,4) -> 6*
g0(4,4,2) -> 6*
g0(1,14,4) -> 6*
g0(1,4,1) -> 6*
g0(17,3,16) -> 6*
g0(15,3,17) -> 6*
g0(5,1,17) -> 6*
g0(5,16,15) -> 6*
g0(3,1,5) -> 6*
g0(14,14,14) -> 6*
g0(1,16,4) -> 6*
g0(15,14,3) -> 6*
g0(17,5,16) -> 6*
g0(15,5,17) -> 6*
g0(5,3,17) -> 6*
g0(2,3,16) -> 6*
g0(16,1,15) -> 6*
g0(3,3,5) -> 6*
g0(14,16,14) -> 6*
g0(17,1,4) -> 6*
g0(4,14,14) -> 6*
g0(15,16,3) -> 6*
g0(5,14,3) -> 6*
g0(5,5,17) -> 6*
g0(2,5,16) -> 6*
g0(16,3,15) -> 6*
g0(3,5,5) -> 6*
g0(4,16,14) -> 6*
g0(17,3,4) -> 6*
g0(5,16,3) -> 6*
g0(1,1,15) -> 6*
g0(2,1,4) -> 6*
g0(16,14,1) -> 6*
g0(16,5,15) -> 6*
g0(14,14,2) -> 6*
g0(17,5,4) -> 6*
g0(1,3,15) -> 6*
g0(15,1,14) -> 6*
g0(2,3,4) -> 6*
g0(16,1,3) -> 6*
g0(16,16,1) -> 6*
g0(14,16,2) -> 6*
g0(4,14,2) -> 6*
g0(1,14,1) -> 6*
g0(1,5,15) -> 6*
g0(5,1,14) -> 6*
g0(15,3,14) -> 6*
g0(2,5,4) -> 6*
g0(16,3,3) -> 6*
g0(4,16,2) -> 6*
g0(1,1,3) -> 6*
g0(1,16,1) -> 6*
g0(17,15,16) -> 6*
g0(15,15,17) -> 6*
g0(5,3,14) -> 6*
g0(15,5,14) -> 6*
g0(16,5,3) -> 6*
g0(1,3,3) -> 6*
g0(17,1,1) -> 6*
g0(17,17,16) -> 6*
g0(15,1,2) -> 6*
g0(15,17,17) -> 6*
g0(5,15,17) -> 6*
g0(5,5,14) -> 6*
g0(2,15,16) -> 6*
g0(3,15,5) -> 6*
g0(1,5,3) -> 6*
g0(17,3,1) -> 6*
g0(5,1,2) -> 6*
g0(15,3,2) -> 6*
g0(5,17,17) -> 6*
g0(2,1,1) -> 6*
g0(2,17,16) -> 6*
g0(16,15,15) -> 6*
g0(3,17,5) -> 6*
g0(17,15,4) -> 6*
g0(17,5,1) -> 6*
g0(5,3,2) -> 6*
g0(15,5,2) -> 6*
g0(2,3,1) -> 6*
g0(16,2,17) -> 6*
g0(16,17,15) -> 6*
g0(17,17,4) -> 6*
g0(5,5,2) -> 6*
g0(14,2,5) -> 6*
g0(1,15,15) -> 6*
g0(2,15,4) -> 6*
g0(2,5,1) -> 6*
g0(16,4,17) -> 6*
g0(3,2,16) -> 6*
g0(1,2,17) -> 6*
g0(4,2,5) -> 6*
g0(14,4,5) -> 6*
g0(1,17,15) -> 6*
g0(15,15,14) -> 6*
g0(2,17,4) -> 6*
g0(16,15,3) -> 6*
g0(3,4,16) -> 6*
g0(17,2,15) -> 6*
g0(1,4,17) -> 6*
g0(4,4,5) -> 6*
g0(5,15,14) -> 6*
g0(15,17,14) -> 6*
g0(16,17,3) -> 6*
g0(1,15,3) -> 6*
g0(17,4,15) -> 6*
g0(5,17,14) -> 6*
g0(2,2,15) -> 6*
g0(3,2,4) -> 6*
g0(1,17,3) -> 6*
g0(17,15,1) -> 6*
g0(15,15,2) -> 6*
g0(2,4,15) -> 6*
g0(16,2,14) -> 6*
g0(3,4,4) -> 6*
g0(17,2,3) -> 6*
g0(17,17,1) -> 6*
g0(5,15,2) -> 6*
g0(15,17,2) -> 6*
g0(2,15,1) -> 6*
g0(16,14,17) -> 6*
g0(16,4,14) -> 6*
g0(17,4,3) -> 6*
g0(5,17,2) -> 6*
g0(1,2,14) -> 6*
g0(14,14,5) -> 6*
g0(2,2,3) -> 6*
g0(2,17,1) -> 6*
g0(16,16,17) -> 6*
g0(3,14,16) -> 6*
g0(1,14,17) -> 6*
g0(1,4,14) -> 6*
g0(14,16,5) -> 6*
g0(4,14,5) -> 6*
g0(2,4,3) -> 6*
g0(16,2,2) -> 6*
g0(3,16,16) -> 6*
g0(17,14,15) -> 6*
g0(1,16,17) -> 6*
g0(4,16,5) -> 6*
g0(16,4,2) -> 6*
g0(3,2,1) -> 6*
g0(1,2,2) -> 6*
g0(17,1,17) -> 6*
g0(17,16,15) -> 6*
g0(14,1,16) -> 6*
g0(2,14,15) -> 6*
g0(15,1,5) -> 6*
g0(3,14,4) -> 6*
g0(3,4,1) -> 6*
g0(1,4,2) -> 6*
g0(17,3,17) -> 6*
g0(14,3,16) -> 6*
g0(4,1,16) -> 6*
g0(2,1,17) -> 6*
g0(5,1,5) -> 6*
g0(15,3,5) -> 6*
g0(2,16,15) -> 6*
g0(16,14,14) -> 6*
g0(3,16,4) -> 6*
g0(17,14,3) -> 6*
g0(17,5,17) -> 6*
g0(14,5,16) -> 6*
g0(4,3,16) -> 6*
g0(2,3,17) -> 6*
g0(5,3,5) -> 6*
g0(15,5,5) -> 6*
g0(16,16,14) -> 6*
g0(17,16,3) -> 6*
g0(14,1,4) -> 6*
g0(1,14,14) -> 6*
g0(2,14,3) -> 6*
g0(4,5,16) -> 6*
g0(2,5,17) -> 6*
g0(5,5,5) -> 6*
g0(3,1,15) -> 6*
g0(1,1,16) -> 6*
g0(4,1,4) -> 6*
g0(1,16,14) -> 6*
g0(14,3,4) -> 6*
g0(2,16,3) -> 6*
g0(16,14,2) -> 6*
g0(3,3,15) -> 6*
g0(17,1,14) -> 6*
g0(4,3,4) -> 6*
g0(14,5,4) -> 6*
g0(16,16,2) -> 6*
g0(3,14,1) -> 6*
g0(1,14,2) -> 6*
g0(3,5,15) -> 6*
g0(17,3,14) -> 6*
g0(4,5,4) -> 6*
g0(2,1,14) -> 6*
g0(3,1,3) -> 6*
g0(3,16,1) -> 6*
g0(17,15,17) -> 6*
g0(1,16,2) -> 6*
g0(17,5,14) -> 6*
g0(14,15,16) -> 6*
g0(15,15,5) -> 6*
g0(2,3,14) -> 6*
g0(3,3,3) -> 6*
g0(17,1,2) -> 6*
g0(17,17,17) -> 6*
g0(14,1,1) -> 6*
g0(14,17,16) -> 6*
g0(4,15,16) -> 6*
g0(2,15,17) -> 6*
g0(5,15,5) -> 6*
g0(15,17,5) -> 6*
g0(2,5,14) -> 6*
g0(3,5,3) -> 6*
g0(17,3,2) -> 6*
g0(4,1,1) -> 6*
g0(14,3,1) -> 6*
g0(2,1,2) -> 6*
g0(4,17,16) -> 6*
g0(2,17,17) -> 6*
g0(5,17,5) -> 6*
g0(17,5,2) -> 6*
g0(14,15,4) -> 6*
g0(4,3,1) -> 6*
g0(14,5,1) -> 6*
g0(2,3,2) -> 6*
g0(15,2,16) -> 6*
g0(16,2,5) -> 6*
g0(3,15,15) -> 6*
g0(4,15,4) -> 6*
g0(14,17,4) -> 6*
g0(4,5,1) -> 6*
g0(2,5,2) -> 6*
g0(15,4,16) -> 6*
g0(5,2,16) -> 6*
g0(3,2,17) -> 6*
g0(16,4,5) -> 6*
g0(3,17,15) -> 6*
g0(17,15,14) -> 6*
g0(4,17,4) -> 6*
g0(1,2,5) -> 6*
g0(5,4,16) -> 6*
g0(3,4,17) -> 6*
g0(17,17,14) -> 6*
g0(14,2,15) -> 6*
g0(1,4,5) -> 6*
g0(15,2,4) -> 6*
g0(2,15,14) -> 6*
g0(3,15,3) -> 6*
g0(4,2,15) -> 6*
g0(14,4,15) -> 6*
g0(5,2,4) -> 6*
g0(15,4,4) -> 6*
g0(2,17,14) -> 6*
g0(3,17,3) -> 6*
g0(17,15,2) -> 6*
g0(14,15,1) -> 6*
g0(4,4,15) -> 6*
g0(5,4,4) -> 6*
g0(17,17,2) -> 6*
g0(14,2,3) -> 6*
g0(4,15,1) -> 6*
g0(14,17,1) -> 6*
g0(2,15,2) -> 6*
g0(15,14,16) -> 6*
g0(3,2,14) -> 6*
g0(16,14,5) -> 6*
g0(4,2,3) -> 6*
g0(14,4,3) -> 6*
g0(4,17,1) -> 6*
g0(2,17,2) -> 6*
g0(15,16,16) -> 6*
g0(5,14,16) -> 6*
g0(3,14,17) -> 6*
g0(16,16,5) -> 6*
g0(3,4,14) -> 6*
g0(4,4,3) -> 6*
g0(1,14,5) -> 6*
g0(15,2,1) -> 6*
g0(5,16,16) -> 6*
g0(3,16,17) -> 6*
g0(14,14,15) -> 6*
g0(1,16,5) -> 6*
g0(15,14,4) -> 6*
g0(5,2,1) -> 6*
g0(15,4,1) -> 6*
g0(3,2,2) -> 6*
g0(16,1,16) -> 6*
c0() -> 1*
d0() -> 2*
e0() -> 3*
s0(15) -> 7*
s0(5) -> 7*
s0(17) -> 7*
s0(2) -> 7*
s0(14) -> 7*
s0(4) -> 7*
s0(16) -> 7*
s0(1) -> 7*
s0(3) -> 7*
f0(17,14) -> 9*
f0(17,16) -> 9*
f0(2,14) -> 9*
f0(2,16) -> 9*
f0(3,1) -> 9*
f0(3,3) -> 9*
f0(3,5) -> 9*
f0(3,15) -> 9*
f0(3,17) -> 9*
f0(14,2) -> 9*
f0(4,2) -> 9*
f0(14,4) -> 9*
f0(4,4) -> 9*
f0(14,14) -> 9*
f0(14,16) -> 9*
f0(4,14) -> 9*
f0(4,16) -> 9*
f0(15,1) -> 9*
f0(5,1) -> 9*
f0(15,3) -> 9*
f0(5,3) -> 9*
f0(15,5) -> 9*
f0(5,5) -> 9*
f0(15,15) -> 9*
f0(15,17) -> 9*
f0(5,15) -> 9*
f0(5,17) -> 9*
f0(16,2) -> 9*
f0(16,4) -> 9*
f0(1,2) -> 9*
f0(1,4) -> 9*
f0(16,14) -> 9*
f0(16,16) -> 9*
f0(1,14) -> 9*
f0(1,16) -> 9*
f0(17,1) -> 9*
f0(17,3) -> 9*
f0(2,1) -> 9*
f0(17,5) -> 9*
f0(2,3) -> 9*
f0(2,5) -> 9*
f0(17,15) -> 9*
f0(17,17) -> 9*
f0(2,15) -> 9*
f0(2,17) -> 9*
f0(3,2) -> 9*
f0(3,4) -> 9*
f0(3,14) -> 9*
f0(3,16) -> 9*
f0(14,1) -> 9*
f0(4,1) -> 9*
f0(14,3) -> 9*
f0(4,3) -> 9*
f0(14,5) -> 9*
f0(4,5) -> 9*
f0(14,15) -> 9*
f0(4,15) -> 9*
f0(14,17) -> 9*
f0(4,17) -> 9*
f0(15,2) -> 9*
f0(5,2) -> 9*
f0(15,4) -> 9*
f0(5,4) -> 9*
f0(15,14) -> 9*
f0(15,16) -> 9*
f0(5,14) -> 9*
f0(5,16) -> 9*
f0(16,1) -> 9*
f0(16,3) -> 9*
f0(1,1) -> 9*
f0(16,5) -> 9*
f0(1,3) -> 9*
f0(1,5) -> 9*
f0(16,15) -> 9*
f0(16,17) -> 9*
f0(1,15) -> 9*
f0(1,17) -> 9*
f0(17,2) -> 9*
f0(17,4) -> 9*
f0(2,2) -> 9*
f0(2,4) -> 9*
a0() -> 4*
h0(17,14) -> 8*
h0(17,16) -> 8*
h0(2,14) -> 8*
h0(2,16) -> 8*
h0(3,1) -> 8*
h0(3,3) -> 8*
h0(3,5) -> 8*
h0(3,15) -> 8*
h0(3,17) -> 8*
h0(14,2) -> 8*
h0(4,2) -> 8*
h0(14,4) -> 8*
h0(4,4) -> 8*
h0(14,14) -> 8*
h0(14,16) -> 8*
h0(4,14) -> 8*
h0(4,16) -> 8*
h0(15,1) -> 8*
h0(5,1) -> 8*
h0(15,3) -> 8*
h0(5,3) -> 8*
h0(15,5) -> 8*
h0(5,5) -> 8*
h0(15,15) -> 8*
h0(15,17) -> 8*
h0(5,15) -> 8*
h0(5,17) -> 8*
h0(16,2) -> 8*
h0(16,4) -> 8*
h0(1,2) -> 8*
h0(1,4) -> 8*
h0(16,14) -> 8*
h0(16,16) -> 8*
h0(1,14) -> 8*
h0(1,16) -> 8*
h0(17,1) -> 8*
h0(17,3) -> 8*
h0(2,1) -> 8*
h0(17,5) -> 8*
h0(2,3) -> 8*
h0(2,5) -> 8*
h0(17,15) -> 8*
h0(17,17) -> 8*
h0(2,15) -> 8*
h0(2,17) -> 8*
h0(3,2) -> 8*
h0(3,4) -> 8*
h0(3,14) -> 8*
h0(3,16) -> 8*
h0(14,1) -> 8*
h0(4,1) -> 8*
h0(14,3) -> 8*
h0(4,3) -> 8*
h0(14,5) -> 8*
h0(4,5) -> 8*
h0(14,15) -> 8*
h0(4,15) -> 8*
h0(14,17) -> 8*
h0(4,17) -> 8*
h0(15,2) -> 8*
h0(5,2) -> 8*
h0(15,4) -> 8*
h0(5,4) -> 8*
h0(15,14) -> 8*
h0(15,16) -> 8*
h0(5,14) -> 8*
h0(5,16) -> 8*
h0(16,1) -> 8*
h0(16,3) -> 8*
h0(1,1) -> 8*
h0(16,5) -> 8*
h0(1,3) -> 8*
h0(1,5) -> 8*
h0(16,15) -> 8*
h0(16,17) -> 8*
h0(1,15) -> 8*
h0(1,17) -> 8*
h0(17,2) -> 8*
h0(17,4) -> 8*
h0(2,2) -> 8*
h0(2,4) -> 8*
b0() -> 5*
b1() -> 14*,5,7
g1(12,16,10) -> 6*
g1(15,16,17) -> 6*
g1(15,11,10) -> 6*
g1(12,16,17) -> 6*
g1(12,11,10) -> 6*
g1(15,11,17) -> 6*
g1(12,11,17) -> 6*
g1(15,16,10) -> 6*
c1() -> 15*,1,12
d1() -> 16*,2,11
e1() -> 17*,3,10
problem:
Qed