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) app(app(lt,app(s,x)),app(s,y)) -> app(app(lt,x),y)
(2) app(app(lt,0),app(s,y)) -> true
(3) app(app(lt,y),0) -> false
(4) app(app(eq,x),x) -> true
(5) app(app(eq,app(s,x)),0) -> false
(6) app(app(eq,0),app(s,x)) -> false
(7) app(app(member,w),null) -> false
(8) app(app(member,w),app(app(app(fork,x),y),z)) -> app(app(app(if,app(app(lt,w),y)),app(app(member,w),x)),app(app(app(if,app(app(eq,w),y)),true),app(app(member,w),z)))

[2]  Apply uncurrying transformation with <app> as function application symbol to obtain the following TRS:
(1) lt(s(x),s(y)) -> lt(x,y)
(2) lt(0,s(y)) -> true
(3) lt(y,0) -> false
(4) eq(x,x) -> true
(5) eq(s(x),0) -> false
(6) eq(0,s(x)) -> false
(7) member(w,null) -> false
(8) member(w,fork`1(x,fork`2(y,z))) -> if`1(lt(w,y),if`2(member(w,x),if`1(eq(w,y),if`2(true,member(w,z)))))

[3]  Eliminate dummy symbol <if`2>, to obtain the following TRS:
(1) lt(s(x),s(y)) -> lt(x,y)
(2) lt(0,s(y)) -> true
(3) lt(y,0) -> false
(4) eq(x,x) -> true
(5) eq(s(x),0) -> false
(6) eq(0,s(x)) -> false
(7) member(w,null) -> false
(8a) member(w,fork`1(x,fork`2(y,z))) -> if`1(lt(w,y),#0)
(8b) member(w,fork`1(x,fork`2(y,z))) -> #2(member(w,x))
(8c) member(w,fork`1(x,fork`2(y,z))) -> #3(if`1(eq(w,y),#1))
(8d) member(w,fork`1(x,fork`2(y,z))) -> #4(true)
(8e) member(w,fork`1(x,fork`2(y,z))) -> #5(member(w,z))

[4]  Eliminate dummy symbol <if`1>, to obtain the following TRS:
(1) lt(s(x),s(y)) -> lt(x,y)
(2) lt(0,s(y)) -> true
(3) lt(y,0) -> false
(4) eq(x,x) -> true
(5) eq(s(x),0) -> false
(6) eq(0,s(x)) -> false
(7) member(w,null) -> false
(8aa) member(w,fork`1(x,fork`2(y,z))) -> #6
(8ab) member(w,fork`1(x,fork`2(y,z))) -> #7(lt(w,y))
(8ac) member(w,fork`1(x,fork`2(y,z))) -> #8(#0)
(8b) member(w,fork`1(x,fork`2(y,z))) -> #2(member(w,x))
(8ca) member(w,fork`1(x,fork`2(y,z))) -> #3(#9)
(8cb) member(w,fork`1(x,fork`2(y,z))) -> #10(eq(w,y))
(8cc) member(w,fork`1(x,fork`2(y,z))) -> #11(#1)
(8d) member(w,fork`1(x,fork`2(y,z))) -> #4(true)
(8e) member(w,fork`1(x,fork`2(y,z))) -> #5(member(w,z))

[5]  Use following polynomial interpretation:
[fork`1(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(8aa)-(8ac), (8b), (8ca)-(8cc), (8d)-(8e)

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

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

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

  Remove rules with left hand side strictly bigger than right hand side:
(4)-(6)

[8]  Use following polynomial interpretation:
[0] = 3
rest default

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

[9]  Use following polynomial interpretation:
[s(x)] = x + 1
rest default

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

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

../tpdb/TRS/higher-order/Bird/BTreeMember.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory