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: {35,33,32,31,30,29,28,27,19,18,15,14,9,8,5}
   transitions:
    f0(27,18) -> 5*
    f0(33,5) -> 5*
    f0(28,5) -> 5*
    f0(18,5) -> 5*
    f0(32,28) -> 5*
    f0(33,9) -> 5*
    f0(27,28) -> 5*
    f0(8,5) -> 5*
    f0(28,9) -> 5*
    f0(32,30) -> 5*
    f0(27,30) -> 5*
    f0(18,9) -> 5*
    f0(32,32) -> 5*
    f0(27,32) -> 5*
    f0(8,9) -> 5*
    f0(33,15) -> 5*
    f0(28,15) -> 5*
    f0(18,15) -> 5*
    f0(33,19) -> 5*
    f0(8,15) -> 5*
    f0(28,19) -> 5*
    f0(18,19) -> 5*
    f0(8,19) -> 5*
    f0(33,27) -> 5*
    f0(28,27) -> 5*
    f0(29,8) -> 5*
    f0(33,29) -> 5*
    f0(18,27) -> 5*
    f0(28,29) -> 5*
    f0(19,8) -> 5*
    f0(33,31) -> 5*
    f0(14,8) -> 5*
    f0(8,27) -> 5*
    f0(28,31) -> 5*
    f0(18,29) -> 5*
    f0(9,8) -> 5*
    f0(33,33) -> 5*
    f0(8,29) -> 5*
    f0(18,31) -> 5*
    f0(28,33) -> 5*
    f0(29,14) -> 5*
    f0(33,35) -> 5*
    f0(28,35) -> 5*
    f0(8,31) -> 5*
    f0(18,33) -> 5*
    f0(19,14) -> 5*
    f0(14,14) -> 5*
    f0(18,35) -> 5*
    f0(8,33) -> 5*
    f0(9,14) -> 5*
    f0(29,18) -> 5*
    f0(8,35) -> 5*
    f0(19,18) -> 5*
    f0(14,18) -> 5*
    f0(9,18) -> 5*
    f0(35,5) -> 5*
    f0(30,5) -> 5*
    f0(35,9) -> 5*
    f0(15,5) -> 5*
    f0(29,28) -> 5*
    f0(30,9) -> 5*
    f0(5,5) -> 5*
    f0(19,28) -> 5*
    f0(29,30) -> 5*
    f0(14,28) -> 5*
    f0(15,9) -> 5*
    f0(9,28) -> 5*
    f0(19,30) -> 5*
    f0(29,32) -> 5*
    f0(14,30) -> 5*
    f0(35,15) -> 5*
    f0(5,9) -> 5*
    f0(9,30) -> 5*
    f0(19,32) -> 5*
    f0(30,15) -> 5*
    f0(14,32) -> 5*
    f0(9,32) -> 5*
    f0(35,19) -> 5*
    f0(15,15) -> 5*
    f0(30,19) -> 5*
    f0(5,15) -> 5*
    f0(15,19) -> 5*
    f0(5,19) -> 5*
    f0(35,27) -> 5*
    f0(30,27) -> 5*
    f0(31,8) -> 5*
    f0(35,29) -> 5*
    f0(30,29) -> 5*
    f0(35,31) -> 5*
    f0(15,27) -> 5*
    f0(30,31) -> 5*
    f0(35,33) -> 5*
    f0(5,27) -> 5*
    f0(15,29) -> 5*
    f0(30,33) -> 5*
    f0(31,14) -> 5*
    f0(35,35) -> 5*
    f0(5,29) -> 5*
    f0(15,31) -> 5*
    f0(30,35) -> 5*
    f0(5,31) -> 5*
    f0(15,33) -> 5*
    f0(31,18) -> 5*
    f0(15,35) -> 5*
    f0(5,33) -> 5*
    f0(5,35) -> 5*
    f0(32,5) -> 5*
    f0(27,5) -> 5*
    f0(31,28) -> 5*
    f0(32,9) -> 5*
    f0(27,9) -> 5*
    f0(31,30) -> 5*
    f0(31,32) -> 5*
    f0(32,15) -> 5*
    f0(27,15) -> 5*
    f0(32,19) -> 5*
    f0(27,19) -> 5*
    f0(32,27) -> 5*
    f0(33,8) -> 5*
    f0(27,27) -> 5*
    f0(28,8) -> 5*
    f0(32,29) -> 5*
    f0(27,29) -> 5*
    f0(18,8) -> 5*
    f0(32,31) -> 5*
    f0(27,31) -> 5*
    f0(8,8) -> 5*
    f0(32,33) -> 5*
    f0(33,14) -> 5*
    f0(27,33) -> 5*
    f0(28,14) -> 5*
    f0(32,35) -> 5*
    f0(27,35) -> 5*
    f0(18,14) -> 5*
    f0(33,18) -> 5*
    f0(8,14) -> 5*
    f0(28,18) -> 5*
    f0(18,18) -> 5*
    f0(8,18) -> 5*
    f0(29,5) -> 5*
    f0(19,5) -> 5*
    f0(33,28) -> 5*
    f0(14,5) -> 5*
    f0(28,28) -> 5*
    f0(9,5) -> 5*
    f0(29,9) -> 5*
    f0(33,30) -> 5*
    f0(18,28) -> 5*
    f0(28,30) -> 5*
    f0(19,9) -> 5*
    f0(33,32) -> 5*
    f0(14,9) -> 5*
    f0(8,28) -> 5*
    f0(18,30) -> 5*
    f0(28,32) -> 5*
    f0(9,9) -> 5*
    f0(8,30) -> 5*
    f0(18,32) -> 5*
    f0(29,15) -> 5*
    f0(8,32) -> 5*
    f0(19,15) -> 5*
    f0(14,15) -> 5*
    f0(9,15) -> 5*
    f0(29,19) -> 5*
    f0(19,19) -> 5*
    f0(14,19) -> 5*
    f0(9,19) -> 5*
    f0(35,8) -> 5*
    f0(29,27) -> 5*
    f0(30,8) -> 5*
    f0(19,27) -> 5*
    f0(29,29) -> 5*
    f0(14,27) -> 5*
    f0(15,8) -> 5*
    f0(9,27) -> 5*
    f0(29,31) -> 5*
    f0(19,29) -> 5*
    f0(14,29) -> 5*
    f0(35,14) -> 5*
    f0(5,8) -> 5*
    f0(9,29) -> 5*
    f0(19,31) -> 5*
    f0(29,33) -> 5*
    f0(30,14) -> 5*
    f0(14,31) -> 5*
    f0(29,35) -> 5*
    f0(9,31) -> 5*
    f0(19,33) -> 5*
    f0(14,33) -> 5*
    f0(35,18) -> 5*
    f0(15,14) -> 5*
    f0(19,35) -> 5*
    f0(9,33) -> 5*
    f0(30,18) -> 5*
    f0(14,35) -> 5*
    f0(5,14) -> 5*
    f0(9,35) -> 5*
    f0(15,18) -> 5*
    f0(5,18) -> 5*
    f0(31,5) -> 5*
    f0(35,28) -> 5*
    f0(30,28) -> 5*
    f0(31,9) -> 5*
    f0(35,30) -> 5*
    f0(30,30) -> 5*
    f0(35,32) -> 5*
    f0(15,28) -> 5*
    f0(30,32) -> 5*
    f0(5,28) -> 5*
    f0(15,30) -> 5*
    f0(31,15) -> 5*
    f0(5,30) -> 5*
    f0(15,32) -> 5*
    f0(5,32) -> 5*
    f0(31,19) -> 5*
    f0(31,27) -> 5*
    f0(32,8) -> 5*
    f0(27,8) -> 5*
    f0(31,29) -> 5*
    f0(31,31) -> 5*
    f0(31,33) -> 5*
    f0(32,14) -> 5*
    f0(27,14) -> 5*
    f0(31,35) -> 5*
    f0(32,18) -> 5*
    s0(35) -> 5*
    s0(30) -> 5*
    s0(15) -> 5*
    s0(5) -> 5*
    s0(32) -> 5*
    s0(27) -> 5*
    s0(29) -> 5*
    s0(19) -> 5*
    s0(14) -> 5*
    s0(9) -> 5*
    s0(31) -> 5*
    s0(33) -> 5*
    s0(28) -> 5*
    s0(18) -> 5*
    s0(8) -> 5*
    a0(35) -> 5*
    a0(30) -> 5*
    a0(15) -> 5*
    a0(5) -> 5*
    a0(32) -> 5*
    a0(27) -> 5*
    a0(29) -> 5*
    a0(19) -> 5*
    a0(14) -> 5*
    a0(9) -> 5*
    a0(31) -> 5*
    a0(33) -> 5*
    a0(28) -> 5*
    a0(18) -> 5*
    a0(8) -> 5*
    c0(35) -> 5*
    c0(30) -> 5*
    c0(15) -> 5*
    c0(5) -> 5*
    c0(32) -> 5*
    c0(27) -> 5*
    c0(29) -> 5*
    c0(19) -> 5*
    c0(14) -> 5*
    c0(9) -> 5*
    c0(31) -> 5*
    c0(33) -> 5*
    c0(28) -> 5*
    c0(18) -> 5*
    c0(8) -> 5*
    c1(35) -> 5*
    c1(30) -> 5*
    c1(15) -> 5*
    c1(5) -> 5*
    c1(32) -> 5*
    c1(27) -> 5*
    c1(29) -> 5*
    c1(19) -> 5*
    c1(14) -> 5*
    c1(9) -> 5*
    c1(31) -> 5*
    c1(33) -> 5*
    c1(28) -> 5*
    c1(18) -> 5*
    c1(8) -> 5*
    f1(32,18) -> 5*
    f1(7,14) -> 5*
    f1(27,18) -> 5*
    f1(7,18) -> 5*
    f1(32,28) -> 5*
    f1(33,9) -> 5*
    f1(27,28) -> 5*
    f1(8,5) -> 5*
    f1(28,9) -> 5*
    f1(32,30) -> 5*
    f1(27,30) -> 5*
    f1(18,9) -> 5*
    f1(32,32) -> 5*
    f1(7,28) -> 5*
    f1(27,32) -> 5*
    f1(8,9) -> 5*
    f1(33,15) -> 5*
    f1(7,30) -> 5*
    f1(28,15) -> 5*
    f1(7,32) -> 5*
    f1(18,15) -> 5*
    f1(33,19) -> 5*
    f1(8,15) -> 5*
    f1(28,19) -> 5*
    f1(18,19) -> 5*
    f1(8,19) -> 5*
    f1(29,6) -> 5*
    f1(33,27) -> 5*
    f1(28,27) -> 5*
    f1(19,6) -> 5*
    f1(33,29) -> 5*
    f1(14,6) -> 5*
    f1(18,27) -> 5*
    f1(28,29) -> 5*
    f1(9,6) -> 5*
    f1(33,31) -> 5*
    f1(14,8) -> 5*
    f1(8,27) -> 5*
    f1(18,29) -> 5*
    f1(28,31) -> 5*
    f1(33,33) -> 5*
    f1(8,29) -> 5*
    f1(18,31) -> 5*
    f1(28,33) -> 5*
    f1(33,35) -> 5*
    f1(28,35) -> 5*
    f1(8,31) -> 5*
    f1(18,33) -> 5*
    f1(14,14) -> 5*
    f1(18,35) -> 5*
    f1(8,33) -> 5*
    f1(29,18) -> 5*
    f1(8,35) -> 5*
    f1(19,18) -> 5*
    f1(14,18) -> 5*
    f1(9,18) -> 5*
    f1(35,9) -> 5*
    f1(29,28) -> 5*
    f1(30,9) -> 5*
    f1(19,28) -> 5*
    f1(29,30) -> 5*
    f1(14,28) -> 5*
    f1(15,9) -> 5*
    f1(9,28) -> 5*
    f1(19,30) -> 5*
    f1(29,32) -> 5*
    f1(14,30) -> 5*
    f1(35,15) -> 5*
    f1(5,9) -> 5*
    f1(9,30) -> 5*
    f1(19,32) -> 5*
    f1(30,15) -> 5*
    f1(14,32) -> 5*
    f1(9,32) -> 5*
    f1(35,19) -> 5*
    f1(15,15) -> 5*
    f1(30,19) -> 5*
    f1(5,15) -> 5*
    f1(15,19) -> 5*
    f1(5,19) -> 5*
    f1(31,6) -> 5*
    f1(35,27) -> 5*
    f1(30,27) -> 5*
    f1(35,29) -> 5*
    f1(30,29) -> 5*
    f1(35,31) -> 5*
    f1(15,27) -> 5*
    f1(30,31) -> 5*
    f1(35,33) -> 5*
    f1(5,27) -> 5*
    f1(15,29) -> 5*
    f1(30,33) -> 5*
    f1(35,35) -> 5*
    f1(5,29) -> 5*
    f1(15,31) -> 5*
    f1(30,35) -> 5*
    f1(5,31) -> 5*
    f1(15,33) -> 5*
    f1(31,18) -> 5*
    f1(15,35) -> 5*
    f1(5,33) -> 5*
    f1(5,35) -> 5*
    f1(31,28) -> 5*
    f1(32,9) -> 5*
    f1(7,5) -> 5*
    f1(27,9) -> 5*
    f1(31,30) -> 5*
    f1(31,32) -> 5*
    f1(7,9) -> 5*
    f1(32,15) -> 5*
    f1(27,15) -> 5*
    f1(32,19) -> 5*
    f1(7,15) -> 5*
    f1(27,19) -> 5*
    f1(7,19) -> 5*
    f1(33,6) -> 5*
    f1(28,6) -> 5*
    f1(32,27) -> 5*
    f1(27,27) -> 5*
    f1(18,6) -> 5*
    f1(32,29) -> 5*
    f1(27,29) -> 5*
    f1(8,6) -> 5*
    f1(32,31) -> 5*
    f1(27,31) -> 5*
    f1(7,27) -> 5*
    f1(8,8) -> 5*
    f1(32,33) -> 5*
    f1(7,29) -> 5*
    f1(27,33) -> 5*
    f1(32,35) -> 5*
    f1(27,35) -> 5*
    f1(7,31) -> 5*
    f1(33,18) -> 5*
    f1(7,33) -> 5*
    f1(8,14) -> 5*
    f1(28,18) -> 5*
    f1(7,35) -> 5*
    f1(18,18) -> 5*
    f1(8,18) -> 5*
    f1(33,28) -> 5*
    f1(14,5) -> 5*
    f1(28,28) -> 5*
    f1(29,9) -> 5*
    f1(33,30) -> 5*
    f1(18,28) -> 5*
    f1(28,30) -> 5*
    f1(19,9) -> 5*
    f1(33,32) -> 5*
    f1(14,9) -> 5*
    f1(8,28) -> 5*
    f1(18,30) -> 5*
    f1(28,32) -> 5*
    f1(9,9) -> 5*
    f1(8,30) -> 5*
    f1(18,32) -> 5*
    f1(29,15) -> 5*
    f1(8,32) -> 5*
    f1(19,15) -> 5*
    f1(14,15) -> 5*
    f1(9,15) -> 5*
    f1(29,19) -> 5*
    f1(19,19) -> 5*
    f1(14,19) -> 5*
    f1(9,19) -> 5*
    f1(35,6) -> 5*
    f1(30,6) -> 5*
    f1(29,27) -> 5*
    f1(15,6) -> 5*
    f1(19,27) -> 5*
    f1(29,29) -> 5*
    f1(14,27) -> 5*
    f1(5,6) -> 5*
    f1(9,27) -> 5*
    f1(19,29) -> 5*
    f1(29,31) -> 5*
    f1(14,29) -> 5*
    f1(9,29) -> 5*
    f1(19,31) -> 5*
    f1(29,33) -> 5*
    f1(14,31) -> 5*
    f1(29,35) -> 5*
    f1(9,31) -> 5*
    f1(19,33) -> 5*
    f1(14,33) -> 5*
    f1(35,18) -> 5*
    f1(19,35) -> 5*
    f1(9,33) -> 5*
    f1(30,18) -> 5*
    f1(14,35) -> 5*
    f1(9,35) -> 5*
    f1(15,18) -> 5*
    f1(5,18) -> 5*
    f1(35,28) -> 5*
    f1(30,28) -> 5*
    f1(31,9) -> 5*
    f1(35,30) -> 5*
    f1(30,30) -> 5*
    f1(35,32) -> 5*
    f1(15,28) -> 5*
    f1(30,32) -> 5*
    f1(5,28) -> 5*
    f1(15,30) -> 5*
    f1(31,15) -> 5*
    f1(5,30) -> 5*
    f1(15,32) -> 5*
    f1(5,32) -> 5*
    f1(31,19) -> 5*
    f1(32,6) -> 5*
    f1(27,6) -> 5*
    f1(31,27) -> 5*
    f1(31,29) -> 5*
    f1(31,31) -> 5*
    f1(7,8) -> 5*
    f1(31,33) -> 5*
    f1(31,35) -> 5*
    s1(35) -> 5,8*
    s1(30) -> 5,8*
    s1(15) -> 5,8*
    s1(5) -> 8*,5,7
    s1(32) -> 5,8*
    s1(27) -> 5,8*
    s1(29) -> 5,8*
    s1(19) -> 5,8*
    s1(14) -> 5,8*
    s1(9) -> 5,8*
    s1(31) -> 5,8*
    s1(33) -> 5,8*
    s1(28) -> 5,8*
    s1(18) -> 5,8*
    s1(8) -> 5,8*
    a1(35) -> 5,9*
    a1(30) -> 5,9*
    a1(15) -> 5,9*
    a1(5) -> 9*,5,6
    a1(32) -> 5,9*
    a1(27) -> 5,9*
    a1(29) -> 5,9*
    a1(19) -> 5,9*
    a1(14) -> 5,9*
    a1(9) -> 5,9*
    a1(31) -> 5,9*
    a1(33) -> 5,9*
    a1(28) -> 5,9*
    a1(18) -> 5,9*
    a1(8) -> 5,9*
    c2(35) -> 5*
    c2(30) -> 5*
    c2(15) -> 5*
    c2(32) -> 5*
    c2(27) -> 5*
    c2(29) -> 5*
    c2(19) -> 5*
    c2(14) -> 5*
    c2(9) -> 5*
    c2(31) -> 5*
    c2(33) -> 5*
    c2(28) -> 5*
    c2(18) -> 5*
    c2(8) -> 5*
    f2(32,18) -> 5*
    f2(27,18) -> 5*
    f2(32,28) -> 5*
    f2(27,28) -> 5*
    f2(32,30) -> 5*
    f2(33,11) -> 5*
    f2(27,30) -> 5*
    f2(28,11) -> 5*
    f2(32,32) -> 5*
    f2(27,32) -> 5*
    f2(18,11) -> 5*
    f2(33,15) -> 5*
    f2(28,15) -> 5*
    f2(18,15) -> 5*
    f2(33,19) -> 5*
    f2(8,15) -> 5*
    f2(28,19) -> 5*
    f2(18,19) -> 5*
    f2(8,19) -> 5*
    f2(33,27) -> 5*
    f2(28,27) -> 5*
    f2(33,29) -> 5*
    f2(18,27) -> 5*
    f2(28,29) -> 5*
    f2(33,31) -> 5*
    f2(14,8) -> 5*
    f2(8,27) -> 5*
    f2(18,29) -> 5*
    f2(28,31) -> 5*
    f2(29,12) -> 5*
    f2(33,33) -> 5*
    f2(14,10) -> 5*
    f2(8,29) -> 5*
    f2(18,31) -> 5*
    f2(28,33) -> 5*
    f2(19,12) -> 5*
    f2(33,35) -> 5*
    f2(14,12) -> 5*
    f2(28,35) -> 5*
    f2(8,31) -> 5*
    f2(18,33) -> 5*
    f2(9,12) -> 5*
    f2(14,14) -> 5*
    f2(18,35) -> 5*
    f2(8,33) -> 5*
    f2(29,18) -> 5*
    f2(8,35) -> 5*
    f2(19,18) -> 5*
    f2(14,18) -> 5*
    f2(9,18) -> 5*
    f2(29,28) -> 5*
    f2(35,11) -> 5*
    f2(19,28) -> 5*
    f2(29,30) -> 5*
    f2(30,11) -> 5*
    f2(14,28) -> 5*
    f2(9,28) -> 5*
    f2(19,30) -> 5*
    f2(29,32) -> 5*
    f2(14,30) -> 5*
    f2(35,15) -> 5*
    f2(15,11) -> 5*
    f2(9,30) -> 5*
    f2(19,32) -> 5*
    f2(30,15) -> 5*
    f2(14,32) -> 5*
    f2(9,32) -> 5*
    f2(35,19) -> 5*
    f2(15,15) -> 5*
    f2(30,19) -> 5*
    f2(5,15) -> 5*
    f2(15,19) -> 5*
    f2(5,19) -> 5*
    f2(35,27) -> 5*
    f2(30,27) -> 5*
    f2(35,29) -> 5*
    f2(30,29) -> 5*
    f2(35,31) -> 5*
    f2(15,27) -> 5*
    f2(30,31) -> 5*
    f2(31,12) -> 5*
    f2(35,33) -> 5*
    f2(5,27) -> 5*
    f2(15,29) -> 5*
    f2(30,33) -> 5*
    f2(35,35) -> 5*
    f2(5,29) -> 5*
    f2(15,31) -> 5*
    f2(30,35) -> 5*
    f2(5,31) -> 5*
    f2(15,33) -> 5*
    f2(31,18) -> 5*
    f2(15,35) -> 5*
    f2(5,33) -> 5*
    f2(5,35) -> 5*
    f2(31,28) -> 5*
    f2(31,30) -> 5*
    f2(32,11) -> 5*
    f2(27,11) -> 5*
    f2(31,32) -> 5*
    f2(32,15) -> 5*
    f2(27,15) -> 5*
    f2(32,19) -> 5*
    f2(27,19) -> 5*
    f2(32,27) -> 5*
    f2(27,27) -> 5*
    f2(32,29) -> 5*
    f2(27,29) -> 5*
    f2(32,31) -> 5*
    f2(13,8) -> 5*
    f2(33,12) -> 5*
    f2(27,31) -> 5*
    f2(28,12) -> 5*
    f2(32,33) -> 5*
    f2(27,33) -> 5*
    f2(18,12) -> 5*
    f2(8,10) -> 5*
    f2(32,35) -> 5*
    f2(27,35) -> 5*
    f2(8,12) -> 5*
    f2(13,14) -> 5*
    f2(33,18) -> 5*
    f2(28,18) -> 5*
    f2(18,18) -> 5*
    f2(8,18) -> 5*
    f2(33,28) -> 5*
    f2(28,28) -> 5*
    f2(33,30) -> 5*
    f2(18,28) -> 5*
    f2(28,30) -> 5*
    f2(29,11) -> 5*
    f2(33,32) -> 5*
    f2(8,28) -> 5*
    f2(18,30) -> 5*
    f2(28,32) -> 5*
    f2(19,11) -> 5*
    f2(8,30) -> 5*
    f2(18,32) -> 5*
    f2(9,11) -> 5*
    f2(29,15) -> 5*
    f2(8,32) -> 5*
    f2(19,15) -> 5*
    f2(14,15) -> 5*
    f2(9,15) -> 5*
    f2(29,19) -> 5*
    f2(19,19) -> 5*
    f2(14,19) -> 5*
    f2(9,19) -> 5*
    f2(29,27) -> 5*
    f2(19,27) -> 5*
    f2(29,29) -> 5*
    f2(14,27) -> 5*
    f2(35,12) -> 5*
    f2(9,27) -> 5*
    f2(19,29) -> 5*
    f2(29,31) -> 5*
    f2(30,12) -> 5*
    f2(14,29) -> 5*
    f2(9,29) -> 5*
    f2(19,31) -> 5*
    f2(29,33) -> 5*
    f2(14,31) -> 5*
    f2(15,12) -> 5*
    f2(29,35) -> 5*
    f2(9,31) -> 5*
    f2(19,33) -> 5*
    f2(14,33) -> 5*
    f2(35,18) -> 5*
    f2(5,12) -> 5*
    f2(19,35) -> 5*
    f2(9,33) -> 5*
    f2(30,18) -> 5*
    f2(14,35) -> 5*
    f2(9,35) -> 5*
    f2(15,18) -> 5*
    f2(5,18) -> 5*
    f2(35,28) -> 5*
    f2(30,28) -> 5*
    f2(35,30) -> 5*
    f2(30,30) -> 5*
    f2(31,11) -> 5*
    f2(35,32) -> 5*
    f2(15,28) -> 5*
    f2(30,32) -> 5*
    f2(5,28) -> 5*
    f2(15,30) -> 5*
    f2(31,15) -> 5*
    f2(5,30) -> 5*
    f2(15,32) -> 5*
    f2(5,32) -> 5*
    f2(31,19) -> 5*
    f2(31,27) -> 5*
    f2(31,29) -> 5*
    f2(31,31) -> 5*
    f2(32,12) -> 5*
    f2(27,12) -> 5*
    f2(31,33) -> 5*
    f2(31,35) -> 5*
    s2(14) -> 8,5,14*
    s2(8) -> 8,14*,5,13
    a2(35) -> 9,5,18*
    a2(30) -> 9,5,18*
    a2(15) -> 9,5,18*
    a2(5) -> 9,15*,6,5,12
    a2(32) -> 9,5,18*
    a2(27) -> 9,5,18*
    a2(29) -> 9,5,18*
    a2(19) -> 9,5,18*
    a2(14) -> 9,5,19*
    a2(9) -> 9,18*,5,11
    a2(31) -> 9,5,18*
    a2(33) -> 9,5,18*
    a2(28) -> 9,5,18*
    a2(18) -> 9,5,18*
    a2(8) -> 9,19*,5,10
    c3(35) -> 5*
    c3(30) -> 5*
    c3(15) -> 5*
    c3(32) -> 5*
    c3(27) -> 5*
    c3(29) -> 5*
    c3(19) -> 5*
    c3(14) -> 5*
    c3(31) -> 5*
    c3(33) -> 5*
    c3(28) -> 5*
    c3(18) -> 5*
    f3(32,20) -> 5*
    f3(27,20) -> 5*
    f3(32,30) -> 5*
    f3(27,30) -> 5*
    f3(33,25) -> 5*
    f3(28,25) -> 5*
    f3(8,21) -> 5*
    f3(33,27) -> 5*
    f3(28,27) -> 5*
    f3(18,25) -> 5*
    f3(18,27) -> 5*
    f3(33,33) -> 5*
    f3(28,33) -> 5*
    f3(8,31) -> 5*
    f3(18,33) -> 5*
    f3(29,22) -> 5*
    f3(19,22) -> 5*
    f3(29,28) -> 5*
    f3(14,26) -> 5*
    f3(19,28) -> 5*
    f3(29,32) -> 5*
    f3(19,32) -> 5*
    f3(35,25) -> 5*
    f3(30,25) -> 5*
    f3(35,27) -> 5*
    f3(30,27) -> 5*
    f3(15,25) -> 5*
    f3(15,27) -> 5*
    f3(35,33) -> 5*
    f3(30,33) -> 5*
    f3(15,33) -> 5*
    f3(31,22) -> 5*
    f3(31,28) -> 5*
    f3(31,32) -> 5*
    f3(32,33) -> 5*
    f3(27,33) -> 5*
    f3(33,20) -> 5*
    f3(28,20) -> 5*
    f3(18,20) -> 5*
    f3(33,30) -> 5*
    f3(28,30) -> 5*
    f3(33,32) -> 5*
    f3(28,32) -> 5*
    f3(18,30) -> 5*
    f3(18,32) -> 5*
    f3(19,25) -> 5*
    f3(19,27) -> 5*
    f3(14,29) -> 5*
    f3(29,35) -> 5*
    f3(19,33) -> 5*
    f3(19,35) -> 5*
    f3(35,20) -> 5*
    f3(30,20) -> 5*
    f3(35,30) -> 5*
    f3(30,30) -> 5*
    f3(35,32) -> 5*
    f3(30,32) -> 5*
    f3(15,32) -> 5*
    f3(31,35) -> 5*
    a3(35) -> 9,18,5,33*
    a3(30) -> 30,9,18,33*,5
    a3(15) -> 9,18,27*,5,25
    a3(32) -> 9,18,5,30*
    a3(27) -> 9,18,5,30*
    a3(29) -> 9,18,5,28*
    a3(19) -> 18,9,32*,5,22
    a3(14) -> 9,19,29*,5,26
    a3(31) -> 9,18,5,28*
    a3(33) -> 30,9,18,33*,5
    a3(28) -> 30,9,18,33*,5
    a3(18) -> 18,9,33*,5,20
    a3(8) -> 9,19,31*,10,5,21
    c4(30) -> 5*
    c4(33) -> 5*
    f4(31,35) -> 5*
    f4(31,34) -> 5*
    a4(31) -> 9,18,28,35*,5,34
  problem:
   
  Qed