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) top(ok(left(car(x,y),z))) -> top(check(right(y,z)))
(2) top(ok(right(x,car(y,z)))) -> top(check(left(x,z)))
(3) top(ok(left(bot,x))) -> top(check(right(bot,x)))
(4) top(ok(right(x,bot))) -> top(check(left(x,bot)))
(5) top(ok(left(car(x,y),z))) ->= top(check(left(y,z)))
(6) top(ok(right(x,car(y,z)))) ->= top(check(right(x,z)))
(7) bot ->= car(new,bot)
(8) check(old) ->= ok(old)
(9) check(car(x,y)) ->= car(check(x),y)
(10) check(car(x,y)) ->= car(x,check(y))
(11) check(left(x,y)) ->= left(check(x),y)
(12) check(left(x,y)) ->= left(x,check(y))
(13) check(right(x,y)) ->= right(check(x),y)
(14) check(right(x,y)) ->= right(x,check(y))
(15) car(ok(x),y) ->= ok(car(x,y))
(16) car(x,ok(y)) ->= ok(car(x,y))
(17) left(ok(x),y) ->= ok(left(x,y))
(18) left(x,ok(y)) ->= ok(left(x,y))
(19) right(ok(x),y) ->= ok(right(x,y))
(20) right(x,ok(y)) ->= ok(right(x,y))

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

  thus obtaining new TRS:
(1a) top$1(ok$1(left$11(car$11(x,y),z))) -> top$1(check$1(right$11(y,z)))
(1b) top$1(ok$1(left$10(car$11(x,y),z))) -> top$1(check$1(right$10(y,z)))
(1c) top$1(ok$1(left$11(car$10(x,y),z))) -> top$1(check$1(right$01(y,z)))
(1d) top$1(ok$1(left$10(car$10(x,y),z))) -> top$0(check$0(right$00(y,z)))
(1e) top$1(ok$1(left$11(car$01(x,y),z))) -> top$1(check$1(right$11(y,z)))
(1f) top$1(ok$1(left$10(car$01(x,y),z))) -> top$1(check$1(right$10(y,z)))
(1g) top$1(ok$1(left$01(car$00(x,y),z))) -> top$1(check$1(right$01(y,z)))
(1h) top$0(ok$0(left$00(car$00(x,y),z))) -> top$0(check$0(right$00(y,z)))
(2a) top$1(ok$1(right$11(x,car$11(y,z)))) -> top$1(check$1(left$11(x,z)))
(2b) top$1(ok$1(right$11(x,car$10(y,z)))) -> top$1(check$1(left$10(x,z)))
(2c) top$1(ok$1(right$01(x,car$11(y,z)))) -> top$1(check$1(left$01(x,z)))
(2d) top$1(ok$1(right$01(x,car$10(y,z)))) -> top$0(check$0(left$00(x,z)))
(2e) top$1(ok$1(right$11(x,car$01(y,z)))) -> top$1(check$1(left$11(x,z)))
(2f) top$1(ok$1(right$10(x,car$00(y,z)))) -> top$1(check$1(left$10(x,z)))
(2g) top$1(ok$1(right$01(x,car$01(y,z)))) -> top$1(check$1(left$01(x,z)))
(2h) top$0(ok$0(right$00(x,car$00(y,z)))) -> top$0(check$0(left$00(x,z)))
(3a) top$1(ok$1(left$01(bot,x))) -> top$1(check$1(right$01(bot,x)))
(3b) top$0(ok$0(left$00(bot,x))) -> top$0(check$0(right$00(bot,x)))
(4a) top$1(ok$1(right$10(x,bot))) -> top$1(check$1(left$10(x,bot)))
(4b) top$0(ok$0(right$00(x,bot))) -> top$0(check$0(left$00(x,bot)))
(5a) top$1(ok$1(left$11(car$11(x,y),z))) ->= top$1(check$1(left$11(y,z)))
(5b) top$1(ok$1(left$10(car$11(x,y),z))) ->= top$1(check$1(left$10(y,z)))
(5c) top$1(ok$1(left$11(car$10(x,y),z))) ->= top$1(check$1(left$01(y,z)))
(5d) top$1(ok$1(left$10(car$10(x,y),z))) ->= top$0(check$0(left$00(y,z)))
(5e) top$1(ok$1(left$11(car$01(x,y),z))) ->= top$1(check$1(left$11(y,z)))
(5f) top$1(ok$1(left$10(car$01(x,y),z))) ->= top$1(check$1(left$10(y,z)))
(5g) top$1(ok$1(left$01(car$00(x,y),z))) ->= top$1(check$1(left$01(y,z)))
(5h) top$0(ok$0(left$00(car$00(x,y),z))) ->= top$0(check$0(left$00(y,z)))
(6a) top$1(ok$1(right$11(x,car$11(y,z)))) ->= top$1(check$1(right$11(x,z)))
(6b) top$1(ok$1(right$11(x,car$10(y,z)))) ->= top$1(check$1(right$10(x,z)))
(6c) top$1(ok$1(right$01(x,car$11(y,z)))) ->= top$1(check$1(right$01(x,z)))
(6d) top$1(ok$1(right$01(x,car$10(y,z)))) ->= top$0(check$0(right$00(x,z)))
(6e) top$1(ok$1(right$11(x,car$01(y,z)))) ->= top$1(check$1(right$11(x,z)))
(6f) top$1(ok$1(right$10(x,car$00(y,z)))) ->= top$1(check$1(right$10(x,z)))
(6g) top$1(ok$1(right$01(x,car$01(y,z)))) ->= top$1(check$1(right$01(x,z)))
(6h) top$0(ok$0(right$00(x,car$00(y,z)))) ->= top$0(check$0(right$00(x,z)))
(7a) bot ->= car$00(new,bot)
(8a) check$1(old) ->= ok$1(old)
(9a) check$1(car$11(x,y)) ->= car$11(check$1(x),y)
(9b) check$1(car$10(x,y)) ->= car$10(check$1(x),y)
(9c) check$1(car$01(x,y)) ->= car$01(check$0(x),y)
(9d) check$0(car$00(x,y)) ->= car$00(check$0(x),y)
(10a) check$1(car$11(x,y)) ->= car$11(x,check$1(y))
(10b) check$1(car$10(x,y)) ->= car$10(x,check$0(y))
(10c) check$1(car$01(x,y)) ->= car$01(x,check$1(y))
(10d) check$0(car$00(x,y)) ->= car$00(x,check$0(y))
(11a) check$1(left$11(x,y)) ->= left$11(check$1(x),y)
(11b) check$1(left$10(x,y)) ->= left$10(check$1(x),y)
(11c) check$1(left$01(x,y)) ->= left$01(check$0(x),y)
(11d) check$0(left$00(x,y)) ->= left$00(check$0(x),y)
(12a) check$1(left$11(x,y)) ->= left$11(x,check$1(y))
(12b) check$1(left$10(x,y)) ->= left$10(x,check$0(y))
(12c) check$1(left$01(x,y)) ->= left$01(x,check$1(y))
(12d) check$0(left$00(x,y)) ->= left$00(x,check$0(y))
(13a) check$1(right$11(x,y)) ->= right$11(check$1(x),y)
(13b) check$1(right$10(x,y)) ->= right$10(check$1(x),y)
(13c) check$1(right$01(x,y)) ->= right$01(check$0(x),y)
(13d) check$0(right$00(x,y)) ->= right$00(check$0(x),y)
(14a) check$1(right$11(x,y)) ->= right$11(x,check$1(y))
(14b) check$1(right$10(x,y)) ->= right$10(x,check$0(y))
(14c) check$1(right$01(x,y)) ->= right$01(x,check$1(y))
(14d) check$0(right$00(x,y)) ->= right$00(x,check$0(y))
(15a) car$11(ok$1(x),y) ->= ok$1(car$11(x,y))
(15b) car$10(ok$1(x),y) ->= ok$1(car$10(x,y))
(15c) car$01(ok$0(x),y) ->= ok$1(car$01(x,y))
(15d) car$00(ok$0(x),y) ->= ok$0(car$00(x,y))
(16a) car$11(x,ok$1(y)) ->= ok$1(car$11(x,y))
(16b) car$10(x,ok$0(y)) ->= ok$1(car$10(x,y))
(16c) car$01(x,ok$1(y)) ->= ok$1(car$01(x,y))
(16d) car$00(x,ok$0(y)) ->= ok$0(car$00(x,y))
(17a) left$11(ok$1(x),y) ->= ok$1(left$11(x,y))
(17b) left$10(ok$1(x),y) ->= ok$1(left$10(x,y))
(17c) left$01(ok$0(x),y) ->= ok$1(left$01(x,y))
(17d) left$00(ok$0(x),y) ->= ok$0(left$00(x,y))
(18a) left$11(x,ok$1(y)) ->= ok$1(left$11(x,y))
(18b) left$10(x,ok$0(y)) ->= ok$1(left$10(x,y))
(18c) left$01(x,ok$1(y)) ->= ok$1(left$01(x,y))
(18d) left$00(x,ok$0(y)) ->= ok$0(left$00(x,y))
(19a) right$11(ok$1(x),y) ->= ok$1(right$11(x,y))
(19b) right$10(ok$1(x),y) ->= ok$1(right$10(x,y))
(19c) right$01(ok$0(x),y) ->= ok$1(right$01(x,y))
(19d) right$00(ok$0(x),y) ->= ok$0(right$00(x,y))
(20a) right$11(x,ok$1(y)) ->= ok$1(right$11(x,y))
(20b) right$10(x,ok$0(y)) ->= ok$1(right$10(x,y))
(20c) right$01(x,ok$1(y)) ->= ok$1(right$01(x,y))
(20d) right$00(x,ok$0(y)) ->= ok$0(right$00(x,y))

[3]  Use following polynomial interpretation:
[ok$0(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1h), (2h), (3b), (4b), (5h), (6h), (15c), (16b), (17c), (18b), (19c), (20b)

[4]  Use following polynomial interpretation:
[car$01(x,y)] = x + y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1e)-(1f), (2e), (2g), (5e)-(5f), (6e), (6g)

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

  Remove rules with left hand side strictly bigger than right hand side:
(1c)-(1d), (2b), (2d), (5c)-(5d), (6b), (6d)

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

  Remove rules with left hand side strictly bigger than right hand side:
(1a)-(1b), (2a), (2c), (5a)-(5b), (6a), (6c)

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

  Remove rules with left hand side strictly bigger than right hand side:
(2f), (4a)

[8]  Unlabel this TRS to obtain the one consisting of the rules:
(1), (3), (5)-(20)

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

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

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

../tpdb/TRS/relative/rtL-cbn5.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory