YES

Problem:
 f(s(X),X) -> f(X,a(X))
 f(X,c(X)) -> f(s(X),X)
 f(X,X) -> c(X)

Proof:
 Bounds Processor:
  bound: 4
  enrichment: top
  automaton:
   final states: {43,40,39,38,37,36,35,34,19,18,15,14,9,8,5}
   transitions:
    f0(36,39) -> 5*
    f0(36,43) -> 5*
    f0(43,5) -> 5*
    f0(38,5) -> 5*
    f0(43,9) -> 5*
    f0(38,9) -> 5*
    f0(18,5) -> 5*
    f0(8,5) -> 5*
    f0(18,9) -> 5*
    f0(43,15) -> 5*
    f0(37,34) -> 5*
    f0(38,15) -> 5*
    f0(8,9) -> 5*
    f0(37,36) -> 5*
    f0(43,19) -> 5*
    f0(37,38) -> 5*
    f0(18,15) -> 5*
    f0(38,19) -> 5*
    f0(37,40) -> 5*
    f0(8,15) -> 5*
    f0(18,19) -> 5*
    f0(8,19) -> 5*
    f0(39,8) -> 5*
    f0(34,8) -> 5*
    f0(19,8) -> 5*
    f0(14,8) -> 5*
    f0(9,8) -> 5*
    f0(39,14) -> 5*
    f0(43,35) -> 5*
    f0(34,14) -> 5*
    f0(38,35) -> 5*
    f0(43,37) -> 5*
    f0(38,37) -> 5*
    f0(39,18) -> 5*
    f0(19,14) -> 5*
    f0(43,39) -> 5*
    f0(34,18) -> 5*
    f0(14,14) -> 5*
    f0(38,39) -> 5*
    f0(18,35) -> 5*
    f0(9,14) -> 5*
    f0(18,37) -> 5*
    f0(8,35) -> 5*
    f0(19,18) -> 5*
    f0(43,43) -> 5*
    f0(14,18) -> 5*
    f0(38,43) -> 5*
    f0(18,39) -> 5*
    f0(8,37) -> 5*
    f0(9,18) -> 5*
    f0(40,5) -> 5*
    f0(8,39) -> 5*
    f0(35,5) -> 5*
    f0(18,43) -> 5*
    f0(40,9) -> 5*
    f0(8,43) -> 5*
    f0(35,9) -> 5*
    f0(15,5) -> 5*
    f0(5,5) -> 5*
    f0(15,9) -> 5*
    f0(39,34) -> 5*
    f0(40,15) -> 5*
    f0(34,34) -> 5*
    f0(35,15) -> 5*
    f0(5,9) -> 5*
    f0(39,36) -> 5*
    f0(34,36) -> 5*
    f0(39,38) -> 5*
    f0(19,34) -> 5*
    f0(40,19) -> 5*
    f0(14,34) -> 5*
    f0(34,38) -> 5*
    f0(15,15) -> 5*
    f0(35,19) -> 5*
    f0(39,40) -> 5*
    f0(19,36) -> 5*
    f0(9,34) -> 5*
    f0(14,36) -> 5*
    f0(34,40) -> 5*
    f0(5,15) -> 5*
    f0(19,38) -> 5*
    f0(9,36) -> 5*
    f0(14,38) -> 5*
    f0(15,19) -> 5*
    f0(19,40) -> 5*
    f0(9,38) -> 5*
    f0(14,40) -> 5*
    f0(5,19) -> 5*
    f0(9,40) -> 5*
    f0(36,8) -> 5*
    f0(36,14) -> 5*
    f0(40,35) -> 5*
    f0(35,35) -> 5*
    f0(40,37) -> 5*
    f0(35,37) -> 5*
    f0(36,18) -> 5*
    f0(40,39) -> 5*
    f0(35,39) -> 5*
    f0(15,35) -> 5*
    f0(15,37) -> 5*
    f0(5,35) -> 5*
    f0(40,43) -> 5*
    f0(35,43) -> 5*
    f0(15,39) -> 5*
    f0(5,37) -> 5*
    f0(37,5) -> 5*
    f0(5,39) -> 5*
    f0(15,43) -> 5*
    f0(37,9) -> 5*
    f0(5,43) -> 5*
    f0(36,34) -> 5*
    f0(37,15) -> 5*
    f0(36,36) -> 5*
    f0(36,38) -> 5*
    f0(37,19) -> 5*
    f0(36,40) -> 5*
    f0(43,8) -> 5*
    f0(38,8) -> 5*
    f0(18,8) -> 5*
    f0(43,14) -> 5*
    f0(8,8) -> 5*
    f0(38,14) -> 5*
    f0(37,35) -> 5*
    f0(43,18) -> 5*
    f0(37,37) -> 5*
    f0(38,18) -> 5*
    f0(18,14) -> 5*
    f0(37,39) -> 5*
    f0(8,14) -> 5*
    f0(18,18) -> 5*
    f0(37,43) -> 5*
    f0(8,18) -> 5*
    f0(39,5) -> 5*
    f0(34,5) -> 5*
    f0(39,9) -> 5*
    f0(19,5) -> 5*
    f0(14,5) -> 5*
    f0(34,9) -> 5*
    f0(9,5) -> 5*
    f0(19,9) -> 5*
    f0(43,34) -> 5*
    f0(14,9) -> 5*
    f0(38,34) -> 5*
    f0(39,15) -> 5*
    f0(9,9) -> 5*
    f0(43,36) -> 5*
    f0(34,15) -> 5*
    f0(38,36) -> 5*
    f0(43,38) -> 5*
    f0(38,38) -> 5*
    f0(18,34) -> 5*
    f0(39,19) -> 5*
    f0(19,15) -> 5*
    f0(43,40) -> 5*
    f0(14,15) -> 5*
    f0(34,19) -> 5*
    f0(38,40) -> 5*
    f0(18,36) -> 5*
    f0(8,34) -> 5*
    f0(9,15) -> 5*
    f0(18,38) -> 5*
    f0(8,36) -> 5*
    f0(19,19) -> 5*
    f0(14,19) -> 5*
    f0(18,40) -> 5*
    f0(8,38) -> 5*
    f0(9,19) -> 5*
    f0(8,40) -> 5*
    f0(40,8) -> 5*
    f0(35,8) -> 5*
    f0(15,8) -> 5*
    f0(40,14) -> 5*
    f0(5,8) -> 5*
    f0(35,14) -> 5*
    f0(39,35) -> 5*
    f0(34,35) -> 5*
    f0(39,37) -> 5*
    f0(40,18) -> 5*
    f0(34,37) -> 5*
    f0(35,18) -> 5*
    f0(15,14) -> 5*
    f0(39,39) -> 5*
    f0(19,35) -> 5*
    f0(14,35) -> 5*
    f0(34,39) -> 5*
    f0(5,14) -> 5*
    f0(19,37) -> 5*
    f0(9,35) -> 5*
    f0(14,37) -> 5*
    f0(15,18) -> 5*
    f0(39,43) -> 5*
    f0(19,39) -> 5*
    f0(9,37) -> 5*
    f0(14,39) -> 5*
    f0(34,43) -> 5*
    f0(5,18) -> 5*
    f0(9,39) -> 5*
    f0(36,5) -> 5*
    f0(19,43) -> 5*
    f0(14,43) -> 5*
    f0(9,43) -> 5*
    f0(36,9) -> 5*
    f0(40,34) -> 5*
    f0(35,34) -> 5*
    f0(36,15) -> 5*
    f0(40,36) -> 5*
    f0(35,36) -> 5*
    f0(40,38) -> 5*
    f0(35,38) -> 5*
    f0(15,34) -> 5*
    f0(36,19) -> 5*
    f0(40,40) -> 5*
    f0(35,40) -> 5*
    f0(15,36) -> 5*
    f0(5,34) -> 5*
    f0(15,38) -> 5*
    f0(5,36) -> 5*
    f0(15,40) -> 5*
    f0(5,38) -> 5*
    f0(5,40) -> 5*
    f0(37,8) -> 5*
    f0(37,14) -> 5*
    f0(36,35) -> 5*
    f0(36,37) -> 5*
    f0(37,18) -> 5*
    c1(40) -> 5*
    c1(35) -> 5*
    c1(15) -> 5*
    c1(5) -> 5*
    c1(37) -> 5*
    c1(39) -> 5*
    c1(34) -> 5*
    c1(19) -> 5*
    c1(14) -> 5*
    c1(9) -> 5*
    c1(36) -> 5*
    c1(43) -> 5*
    c1(38) -> 5*
    c1(18) -> 5*
    c1(8) -> 5*
    f1(36,39) -> 5*
    f1(7,14) -> 5*
    f1(36,43) -> 5*
    f1(7,18) -> 5*
    f1(43,9) -> 5*
    f1(38,9) -> 5*
    f1(8,5) -> 5*
    f1(18,9) -> 5*
    f1(43,15) -> 5*
    f1(37,34) -> 5*
    f1(38,15) -> 5*
    f1(8,9) -> 5*
    f1(37,36) -> 5*
    f1(43,19) -> 5*
    f1(37,38) -> 5*
    f1(18,15) -> 5*
    f1(38,19) -> 5*
    f1(37,40) -> 5*
    f1(7,34) -> 5*
    f1(8,15) -> 5*
    f1(7,36) -> 5*
    f1(18,19) -> 5*
    f1(7,38) -> 5*
    f1(8,19) -> 5*
    f1(39,6) -> 5*
    f1(7,40) -> 5*
    f1(34,6) -> 5*
    f1(19,6) -> 5*
    f1(14,6) -> 5*
    f1(9,6) -> 5*
    f1(14,8) -> 5*
    f1(43,35) -> 5*
    f1(38,35) -> 5*
    f1(43,37) -> 5*
    f1(38,37) -> 5*
    f1(39,18) -> 5*
    f1(43,39) -> 5*
    f1(14,14) -> 5*
    f1(34,18) -> 5*
    f1(38,39) -> 5*
    f1(18,35) -> 5*
    f1(18,37) -> 5*
    f1(8,35) -> 5*
    f1(19,18) -> 5*
    f1(43,43) -> 5*
    f1(14,18) -> 5*
    f1(38,43) -> 5*
    f1(18,39) -> 5*
    f1(8,37) -> 5*
    f1(9,18) -> 5*
    f1(8,39) -> 5*
    f1(18,43) -> 5*
    f1(40,9) -> 5*
    f1(8,43) -> 5*
    f1(35,9) -> 5*
    f1(15,9) -> 5*
    f1(39,34) -> 5*
    f1(40,15) -> 5*
    f1(34,34) -> 5*
    f1(35,15) -> 5*
    f1(5,9) -> 5*
    f1(39,36) -> 5*
    f1(34,36) -> 5*
    f1(39,38) -> 5*
    f1(19,34) -> 5*
    f1(40,19) -> 5*
    f1(34,38) -> 5*
    f1(14,34) -> 5*
    f1(15,15) -> 5*
    f1(35,19) -> 5*
    f1(39,40) -> 5*
    f1(19,36) -> 5*
    f1(9,34) -> 5*
    f1(34,40) -> 5*
    f1(14,36) -> 5*
    f1(5,15) -> 5*
    f1(19,38) -> 5*
    f1(9,36) -> 5*
    f1(14,38) -> 5*
    f1(15,19) -> 5*
    f1(19,40) -> 5*
    f1(9,38) -> 5*
    f1(14,40) -> 5*
    f1(5,19) -> 5*
    f1(9,40) -> 5*
    f1(36,6) -> 5*
    f1(40,35) -> 5*
    f1(35,35) -> 5*
    f1(40,37) -> 5*
    f1(35,37) -> 5*
    f1(36,18) -> 5*
    f1(40,39) -> 5*
    f1(35,39) -> 5*
    f1(15,35) -> 5*
    f1(15,37) -> 5*
    f1(5,35) -> 5*
    f1(40,43) -> 5*
    f1(35,43) -> 5*
    f1(15,39) -> 5*
    f1(5,37) -> 5*
    f1(5,39) -> 5*
    f1(15,43) -> 5*
    f1(37,9) -> 5*
    f1(5,43) -> 5*
    f1(7,5) -> 5*
    f1(36,34) -> 5*
    f1(37,15) -> 5*
    f1(7,9) -> 5*
    f1(36,36) -> 5*
    f1(36,38) -> 5*
    f1(37,19) -> 5*
    f1(36,40) -> 5*
    f1(7,15) -> 5*
    f1(43,6) -> 5*
    f1(7,19) -> 5*
    f1(38,6) -> 5*
    f1(18,6) -> 5*
    f1(8,6) -> 5*
    f1(8,8) -> 5*
    f1(37,35) -> 5*
    f1(43,18) -> 5*
    f1(37,37) -> 5*
    f1(38,18) -> 5*
    f1(37,39) -> 5*
    f1(8,14) -> 5*
    f1(7,35) -> 5*
    f1(18,18) -> 5*
    f1(37,43) -> 5*
    f1(7,37) -> 5*
    f1(8,18) -> 5*
    f1(7,39) -> 5*
    f1(39,9) -> 5*
    f1(7,43) -> 5*
    f1(14,5) -> 5*
    f1(34,9) -> 5*
    f1(19,9) -> 5*
    f1(43,34) -> 5*
    f1(14,9) -> 5*
    f1(38,34) -> 5*
    f1(39,15) -> 5*
    f1(9,9) -> 5*
    f1(43,36) -> 5*
    f1(34,15) -> 5*
    f1(38,36) -> 5*
    f1(43,38) -> 5*
    f1(38,38) -> 5*
    f1(18,34) -> 5*
    f1(19,15) -> 5*
    f1(39,19) -> 5*
    f1(43,40) -> 5*
    f1(14,15) -> 5*
    f1(34,19) -> 5*
    f1(38,40) -> 5*
    f1(18,36) -> 5*
    f1(8,34) -> 5*
    f1(9,15) -> 5*
    f1(18,38) -> 5*
    f1(8,36) -> 5*
    f1(19,19) -> 5*
    f1(14,19) -> 5*
    f1(18,40) -> 5*
    f1(8,38) -> 5*
    f1(9,19) -> 5*
    f1(40,6) -> 5*
    f1(8,40) -> 5*
    f1(35,6) -> 5*
    f1(15,6) -> 5*
    f1(5,6) -> 5*
    f1(39,35) -> 5*
    f1(34,35) -> 5*
    f1(39,37) -> 5*
    f1(40,18) -> 5*
    f1(34,37) -> 5*
    f1(35,18) -> 5*
    f1(39,39) -> 5*
    f1(19,35) -> 5*
    f1(34,39) -> 5*
    f1(14,35) -> 5*
    f1(19,37) -> 5*
    f1(9,35) -> 5*
    f1(14,37) -> 5*
    f1(15,18) -> 5*
    f1(39,43) -> 5*
    f1(19,39) -> 5*
    f1(9,37) -> 5*
    f1(34,43) -> 5*
    f1(14,39) -> 5*
    f1(5,18) -> 5*
    f1(9,39) -> 5*
    f1(19,43) -> 5*
    f1(14,43) -> 5*
    f1(9,43) -> 5*
    f1(36,9) -> 5*
    f1(40,34) -> 5*
    f1(35,34) -> 5*
    f1(36,15) -> 5*
    f1(40,36) -> 5*
    f1(35,36) -> 5*
    f1(40,38) -> 5*
    f1(35,38) -> 5*
    f1(15,34) -> 5*
    f1(36,19) -> 5*
    f1(40,40) -> 5*
    f1(35,40) -> 5*
    f1(15,36) -> 5*
    f1(5,34) -> 5*
    f1(15,38) -> 5*
    f1(5,36) -> 5*
    f1(15,40) -> 5*
    f1(5,38) -> 5*
    f1(37,6) -> 5*
    f1(5,40) -> 5*
    f1(7,8) -> 5*
    f1(36,35) -> 5*
    f1(36,37) -> 5*
    f1(37,18) -> 5*
    s1(40) -> 8*
    s1(35) -> 8*
    s1(15) -> 8*
    s1(5) -> 8*,5,7
    s1(37) -> 8*
    s1(39) -> 8*
    s1(34) -> 8*
    s1(19) -> 8*
    s1(14) -> 8*
    s1(9) -> 8*
    s1(36) -> 8*
    s1(43) -> 8*
    s1(38) -> 8*
    s1(18) -> 8*
    s1(8) -> 8*
    c2(9) -> 5*
    c2(8) -> 5*
    f2(37,18) -> 5*
    f2(36,39) -> 5*
    f2(36,43) -> 5*
    f2(43,11) -> 5*
    f2(38,11) -> 5*
    f2(43,15) -> 5*
    f2(37,34) -> 5*
    f2(18,11) -> 5*
    f2(38,15) -> 5*
    f2(37,36) -> 5*
    f2(43,19) -> 5*
    f2(37,38) -> 5*
    f2(18,15) -> 5*
    f2(38,19) -> 5*
    f2(37,40) -> 5*
    f2(8,15) -> 5*
    f2(18,19) -> 5*
    f2(8,19) -> 5*
    f2(39,12) -> 5*
    f2(14,8) -> 5*
    f2(34,12) -> 5*
    f2(43,35) -> 5*
    f2(14,10) -> 5*
    f2(38,35) -> 5*
    f2(19,12) -> 5*
    f2(43,37) -> 5*
    f2(14,12) -> 5*
    f2(38,37) -> 5*
    f2(9,12) -> 5*
    f2(39,18) -> 5*
    f2(43,39) -> 5*
    f2(14,14) -> 5*
    f2(34,18) -> 5*
    f2(38,39) -> 5*
    f2(18,35) -> 5*
    f2(18,37) -> 5*
    f2(8,35) -> 5*
    f2(19,18) -> 5*
    f2(43,43) -> 5*
    f2(14,18) -> 5*
    f2(38,43) -> 5*
    f2(18,39) -> 5*
    f2(8,37) -> 5*
    f2(9,18) -> 5*
    f2(8,39) -> 5*
    f2(18,43) -> 5*
    f2(8,43) -> 5*
    f2(40,11) -> 5*
    f2(35,11) -> 5*
    f2(39,34) -> 5*
    f2(40,15) -> 5*
    f2(34,34) -> 5*
    f2(15,11) -> 5*
    f2(35,15) -> 5*
    f2(39,36) -> 5*
    f2(34,36) -> 5*
    f2(19,34) -> 5*
    f2(39,38) -> 5*
    f2(40,19) -> 5*
    f2(14,34) -> 5*
    f2(34,38) -> 5*
    f2(15,15) -> 5*
    f2(35,19) -> 5*
    f2(39,40) -> 5*
    f2(9,34) -> 5*
    f2(19,36) -> 5*
    f2(14,36) -> 5*
    f2(34,40) -> 5*
    f2(5,15) -> 5*
    f2(9,36) -> 5*
    f2(19,38) -> 5*
    f2(14,38) -> 5*
    f2(15,19) -> 5*
    f2(19,40) -> 5*
    f2(9,38) -> 5*
    f2(14,40) -> 5*
    f2(5,19) -> 5*
    f2(9,40) -> 5*
    f2(36,12) -> 5*
    f2(40,35) -> 5*
    f2(35,35) -> 5*
    f2(40,37) -> 5*
    f2(35,37) -> 5*
    f2(36,18) -> 5*
    f2(40,39) -> 5*
    f2(35,39) -> 5*
    f2(15,35) -> 5*
    f2(5,35) -> 5*
    f2(15,37) -> 5*
    f2(40,43) -> 5*
    f2(35,43) -> 5*
    f2(15,39) -> 5*
    f2(5,37) -> 5*
    f2(5,39) -> 5*
    f2(15,43) -> 5*
    f2(5,43) -> 5*
    f2(37,11) -> 5*
    f2(36,34) -> 5*
    f2(37,15) -> 5*
    f2(36,36) -> 5*
    f2(36,38) -> 5*
    f2(37,19) -> 5*
    f2(36,40) -> 5*
    f2(43,12) -> 5*
    f2(38,12) -> 5*
    f2(13,8) -> 5*
    f2(37,35) -> 5*
    f2(18,12) -> 5*
    f2(8,10) -> 5*
    f2(43,18) -> 5*
    f2(37,37) -> 5*
    f2(8,12) -> 5*
    f2(38,18) -> 5*
    f2(13,14) -> 5*
    f2(37,39) -> 5*
    f2(18,18) -> 5*
    f2(37,43) -> 5*
    f2(8,18) -> 5*
    f2(39,11) -> 5*
    f2(34,11) -> 5*
    f2(43,34) -> 5*
    f2(38,34) -> 5*
    f2(19,11) -> 5*
    f2(39,15) -> 5*
    f2(43,36) -> 5*
    f2(34,15) -> 5*
    f2(38,36) -> 5*
    f2(9,11) -> 5*
    f2(43,38) -> 5*
    f2(18,34) -> 5*
    f2(38,38) -> 5*
    f2(19,15) -> 5*
    f2(39,19) -> 5*
    f2(43,40) -> 5*
    f2(14,15) -> 5*
    f2(34,19) -> 5*
    f2(38,40) -> 5*
    f2(8,34) -> 5*
    f2(18,36) -> 5*
    f2(9,15) -> 5*
    f2(8,36) -> 5*
    f2(18,38) -> 5*
    f2(19,19) -> 5*
    f2(14,19) -> 5*
    f2(8,38) -> 5*
    f2(18,40) -> 5*
    f2(9,19) -> 5*
    f2(8,40) -> 5*
    f2(40,12) -> 5*
    f2(35,12) -> 5*
    f2(39,35) -> 5*
    f2(34,35) -> 5*
    f2(15,12) -> 5*
    f2(39,37) -> 5*
    f2(40,18) -> 5*
    f2(34,37) -> 5*
    f2(5,12) -> 5*
    f2(35,18) -> 5*
    f2(39,39) -> 5*
    f2(19,35) -> 5*
    f2(34,39) -> 5*
    f2(14,35) -> 5*
    f2(9,35) -> 5*
    f2(19,37) -> 5*
    f2(14,37) -> 5*
    f2(15,18) -> 5*
    f2(39,43) -> 5*
    f2(9,37) -> 5*
    f2(19,39) -> 5*
    f2(34,43) -> 5*
    f2(14,39) -> 5*
    f2(5,18) -> 5*
    f2(9,39) -> 5*
    f2(19,43) -> 5*
    f2(14,43) -> 5*
    f2(9,43) -> 5*
    f2(36,11) -> 5*
    f2(40,34) -> 5*
    f2(35,34) -> 5*
    f2(36,15) -> 5*
    f2(40,36) -> 5*
    f2(35,36) -> 5*
    f2(40,38) -> 5*
    f2(15,34) -> 5*
    f2(35,38) -> 5*
    f2(36,19) -> 5*
    f2(40,40) -> 5*
    f2(35,40) -> 5*
    f2(5,34) -> 5*
    f2(15,36) -> 5*
    f2(5,36) -> 5*
    f2(15,38) -> 5*
    f2(15,40) -> 5*
    f2(5,38) -> 5*
    f2(5,40) -> 5*
    f2(37,12) -> 5*
    f2(36,35) -> 5*
    f2(36,37) -> 5*
    s2(14) -> 8,14*
    s2(8) -> 8,14*,13
    a2(40) -> 15*
    a2(35) -> 15*
    a2(15) -> 15*
    a2(5) -> 9,15*,6,5,12
    a2(37) -> 15*
    a2(39) -> 15*
    a2(34) -> 15*
    a2(19) -> 15*
    a2(14) -> 15*
    a2(9) -> 9,18*,11
    a2(36) -> 15*
    a2(43) -> 15*
    a2(38) -> 15*
    a2(18) -> 15*
    a2(8) -> 15*
    c3(35) -> 5*
    c3(15) -> 5*
    c3(19) -> 5*
    c3(14) -> 5*
    c3(36) -> 5*
    c3(38) -> 5*
    c3(18) -> 5*
    f3(36,39) -> 5*
    f3(37,20) -> 5*
    f3(36,43) -> 5*
    f3(37,34) -> 5*
    f3(37,40) -> 5*
    f3(43,27) -> 5*
    f3(38,27) -> 5*
    f3(8,21) -> 5*
    f3(18,27) -> 5*
    f3(38,35) -> 5*
    f3(43,37) -> 5*
    f3(43,39) -> 5*
    f3(38,39) -> 5*
    f3(39,20) -> 5*
    f3(34,20) -> 5*
    f3(18,37) -> 5*
    f3(43,43) -> 5*
    f3(38,43) -> 5*
    f3(18,39) -> 5*
    f3(14,22) -> 5*
    f3(18,43) -> 5*
    f3(19,26) -> 5*
    f3(39,34) -> 5*
    f3(34,34) -> 5*
    f3(39,40) -> 5*
    f3(34,40) -> 5*
    f3(14,36) -> 5*
    f3(19,40) -> 5*
    f3(40,27) -> 5*
    f3(35,27) -> 5*
    f3(15,27) -> 5*
    f3(40,37) -> 5*
    f3(35,37) -> 5*
    f3(40,39) -> 5*
    f3(35,39) -> 5*
    f3(40,43) -> 5*
    f3(15,39) -> 5*
    f3(35,43) -> 5*
    f3(36,26) -> 5*
    f3(15,43) -> 5*
    f3(36,34) -> 5*
    f3(36,40) -> 5*
    f3(37,27) -> 5*
    f3(37,37) -> 5*
    f3(43,20) -> 5*
    f3(37,39) -> 5*
    f3(37,43) -> 5*
    f3(18,20) -> 5*
    f3(38,26) -> 5*
    f3(43,34) -> 5*
    f3(38,34) -> 5*
    f3(18,34) -> 5*
    f3(43,40) -> 5*
    f3(38,40) -> 5*
    f3(18,40) -> 5*
    f3(8,38) -> 5*
    f3(39,27) -> 5*
    f3(34,27) -> 5*
    f3(39,37) -> 5*
    f3(34,37) -> 5*
    f3(19,35) -> 5*
    f3(39,39) -> 5*
    f3(40,20) -> 5*
    f3(34,39) -> 5*
    f3(35,20) -> 5*
    f3(39,43) -> 5*
    f3(34,43) -> 5*
    f3(19,43) -> 5*
    f3(40,34) -> 5*
    f3(35,34) -> 5*
    f3(15,34) -> 5*
    f3(40,40) -> 5*
    f3(35,40) -> 5*
    f3(15,40) -> 5*
    f3(36,27) -> 5*
    f3(36,35) -> 5*
    a3(40) -> 15,39*
    a3(35) -> 37,15,39*
    a3(15) -> 18,15,34*,27
    a3(37) -> 37,15,39*
    a3(39) -> 37,15,39*
    a3(34) -> 37,15,39*
    a3(19) -> 18,15,35*,26
    a3(14) -> 19,15,36*,22
    a3(36) -> 35,15,40*
    a3(43) -> 15,39*
    a3(18) -> 18,15,39*,20
    a3(8) -> 19,9,15,38*,10,21
    c4(40) -> 5*
    c4(37) -> 5*
    c4(39) -> 5*
    c4(34) -> 5*
    c4(43) -> 5*
    f4(38,41) -> 5*
    f4(38,43) -> 5*
    a4(38) -> 18,35,15,40,43*,41
  problem:
   
  Qed