Termination w.r.t. Q of the given QTRS could be disproven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(a(a(x1))) → b(b(c(a(a(x1)))))
b(b(x1)) → c(a(b(x1)))
c(x1) → x1

Q is empty.

(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

a(a(a(x))) → a(a(c(b(b(x)))))
b(b(x)) → b(a(c(x)))
c(x) → x

Q is empty.

(3) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.

Found the self-embedding DerivationStructure:

(b)^k+3 → b a a (b)^2k

(b)^k+3 → b a a (b)^2k
by Overlapping Derivationstructures

(b)^k+3 → b (a)^k+2
by Overlap u with m (ol1)

(b)^k+2 b → b (a c)^k+2
by Operation lift

(b)^k+1 b → b (a c)^k+1
by Operation lift

(b)^k b → b (a c)^k
by Selfoverlapping OC am1

b b → b a c
by original rule (OC 1)

c →
by original rule (OC 1)

(a)^k+2 → a a (b)^2k
by Overlap u with m (ol1)

(a)^k a a → a a (c b b)^k
by Selfoverlapping OC am1

a a a → a a c b b
by original rule (OC 1)

c →
by original rule (OC 1)

(4) NO