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) b(x) ->= b(b(x))
(2) a(b(a(x))) -> a(b(b(a(x))))

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

  thus obtaining new TRS:
(1a) b$1(x) ->= b$0(b$1(x))
(1b) b$0(x) ->= b$0(b$0(x))
(2a) a$0(b$1(a$1(x))) -> a$0(b$0(b$1(a$1(x))))
(2b) a$0(b$1(a$0(x))) -> a$0(b$0(b$1(a$0(x))))

[3]  Reverse every lhs and rhs of the rule to obtain the following TRS:
(1a) b$1(x) ->= b$1(b$0(x))
(1b) b$0(x) ->= b$0(b$0(x))
(2a) a$1(b$1(a$0(x))) -> a$1(b$1(b$0(a$0(x))))
(2b) a$0(b$1(a$0(x))) -> a$0(b$1(b$0(a$0(x))))

[4]  Label this TRS using following interpretation over N\{0,1}:
[b$0(x)] = 2
[b$1(x)] = 2
[a$0(x)] = x + 1
[a$1(x)] = 2
rest default

  This interpretation is a model and yields following TRS:
(1a) b$1{j}(x) ->= b$1{2}(b$0{j}(x))
(1b) b$0{j}(x) ->= b$0{2}(b$0{j}(x))
(2a) a$1{2}(b$1{j + 1}(a$0{j}(x))) -> a$1{2}(b$1{2}(b$0{j + 1}(a$0{j}(x))))
(2b) a$0{2}(b$1{j + 1}(a$0{j}(x))) -> a$0{2}(b$1{2}(b$0{j + 1}(a$0{j}(x))))

[5]  Use following polynomial interpretation:
[b$0_{i}(x)] = x
[b$1_{i}(x)] = x + i
[a$0_{i}(x)] = x
[a$1_{i}(x)] = x
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(2a)-(2b)

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

../qualif/zr05.srs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory