Input TRS:
    1: c(c(c(b(x)))) -> a(1(),b(c(x)))
    2: b(c(b(c(x)))) -> a(0(),a(1(),x))
    3: a(0(),x) -> c(c(x))
    4: a(1(),x) -> c(b(x))
Number of Rules: 4
Direct QKBOS(Sum) ... failed.