YES
  TPA v.1.0

Result: TRS is terminating

Default interpretations for symbols are not printed. For polynomial interpretations
and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary
symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans)
defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols.

[1]  TRS loaded from input file:
(1) f(f(x,a),y) -> f(f(a,y),f(a,x))

[2]  Label this TRS using following interpretation that is a model:
[f(x,y)] = 1
rest default

  thus obtaining new TRS:
(1a) f$11(f$10(x,a),y) -> f$11(f$01(a,y),f$01(a,x))
(1b) f$11(f$00(x,a),y) -> f$11(f$01(a,y),f$00(a,x))
(1c) f$10(f$10(x,a),y) -> f$11(f$00(a,y),f$01(a,x))
(1d) f$10(f$00(x,a),y) -> f$11(f$00(a,y),f$00(a,x))

[3]  Use following polynomial interpretation:
[f$10(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1a), (1c)-(1d)

[4]  Label this TRS using following interpretation that is a model:
[f$01(x,y)] = 1
[f$11(x,y)] = 0
rest default

  thus obtaining new TRS:
(1ba) f$1111(f$0010(x,a),y) -> f$1111(f$0101(a,y),f$0001(a,x))
(1bb) f$1101(f$0000(x,a),y) -> f$1110(f$0101(a,y),f$0000(a,x))
(1bc) f$1110(f$0010(x,a),y) -> f$1111(f$0100(a,y),f$0001(a,x))
(1bd) f$1100(f$0000(x,a),y) -> f$1110(f$0100(a,y),f$0000(a,x))

[5]  Use following polynomial interpretation:
[f$1100(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1bd)

[6]  Use following polynomial interpretation:
[f$1101(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1bb)

[7]  Use following polynomial interpretation:
[f$1110(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1bc)

[8]  Use following polynomial interpretation:
[f$0010(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1ba)

[9]  Since there are no remaining rules, termination is proved!

../tpdb/secret2005/matchbox2.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory