NO Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema_04/z090-rotate.srs

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

0 QTRS
↳1 NonTerminationProof (⇒, 3699 ms)
↳2 NO

(0) Obligation:

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

begin(end(x)) → rewrite(end(x))
begin(s(x)) → rotate(cut(Cs(guess(x))))
begin(b(x)) → rotate(cut(Cb(guess(x))))
begin(t(x)) → rotate(cut(Ct(guess(x))))
begin(u(x)) → rotate(cut(Cu(guess(x))))
guess(s(x)) → Cs(guess(x))
guess(b(x)) → Cb(guess(x))
guess(t(x)) → Ct(guess(x))
guess(u(x)) → Cu(guess(x))
guess(s(x)) → moveleft(Bs(wait(x)))
guess(b(x)) → moveleft(Bb(wait(x)))
guess(t(x)) → moveleft(Bt(wait(x)))
guess(u(x)) → moveleft(Bu(wait(x)))
guess(end(x)) → finish(end(x))
Cs(moveleft(Bs(x))) → moveleft(Bs(As(x)))
Cb(moveleft(Bs(x))) → moveleft(Bs(Ab(x)))
Ct(moveleft(Bs(x))) → moveleft(Bs(At(x)))
Cu(moveleft(Bs(x))) → moveleft(Bs(Au(x)))
Cs(moveleft(Bb(x))) → moveleft(Bb(As(x)))
Cb(moveleft(Bb(x))) → moveleft(Bb(Ab(x)))
Ct(moveleft(Bb(x))) → moveleft(Bb(At(x)))
Cu(moveleft(Bb(x))) → moveleft(Bb(Au(x)))
Cs(moveleft(Bt(x))) → moveleft(Bt(As(x)))
Cb(moveleft(Bt(x))) → moveleft(Bt(Ab(x)))
Ct(moveleft(Bt(x))) → moveleft(Bt(At(x)))
Cu(moveleft(Bt(x))) → moveleft(Bt(Au(x)))
Cs(moveleft(Bu(x))) → moveleft(Bu(As(x)))
Cb(moveleft(Bu(x))) → moveleft(Bu(Ab(x)))
Ct(moveleft(Bu(x))) → moveleft(Bu(At(x)))
Cu(moveleft(Bu(x))) → moveleft(Bu(Au(x)))
cut(moveleft(Bs(x))) → Ds(cut(goright(x)))
cut(moveleft(Bb(x))) → Db(cut(goright(x)))
cut(moveleft(Bt(x))) → Dt(cut(goright(x)))
cut(moveleft(Bu(x))) → Du(cut(goright(x)))
goright(As(x)) → Cs(goright(x))
goright(Ab(x)) → Cb(goright(x))
goright(At(x)) → Ct(goright(x))
goright(Au(x)) → Cu(goright(x))
goright(wait(s(x))) → moveleft(Bs(wait(x)))
goright(wait(b(x))) → moveleft(Bb(wait(x)))
goright(wait(t(x))) → moveleft(Bt(wait(x)))
goright(wait(u(x))) → moveleft(Bu(wait(x)))
goright(wait(end(x))) → finish(end(x))
Cs(finish(x)) → finish(s(x))
Cb(finish(x)) → finish(b(x))
Ct(finish(x)) → finish(t(x))
Cu(finish(x)) → finish(u(x))
cut(finish(x)) → finish2(x)
Ds(finish2(x)) → finish2(s(x))
Db(finish2(x)) → finish2(b(x))
Dt(finish2(x)) → finish2(t(x))
Du(finish2(x)) → finish2(u(x))
rotate(finish2(x)) → rewrite(x)
rewrite(s(b(x))) → begin(b(s(s(s(x)))))
rewrite(s(b(s(x)))) → begin(b(t(x)))
rewrite(t(b(x))) → begin(b(s(x)))
rewrite(t(b(s(x)))) → begin(u(t(b(x))))
rewrite(b(u(x))) → begin(b(s(x)))
rewrite(t(s(x))) → begin(t(t(x)))
rewrite(t(u(x))) → begin(u(t(x)))
rewrite(s(u(x))) → begin(s(s(x)))

Q is empty.

(1) NonTerminationProof (COMPLETE transformation)

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

Found the self-embedding DerivationStructure:
rewrite t u end → rewrite t u end

rewrite t u end → rewrite t u end
by OverlapClosure OC 3
rewrite t u end → rotate finish2 t u end
by OverlapClosure OC 3
rewrite t u end → rotate Dt finish2 u end
by OverlapClosure OC 3
rewrite t u end → rotate Dt cut finish u end
by OverlapClosure OC 3
rewrite t u end → rotate Dt cut Cu finish end
by OverlapClosure OC 2
rewrite t u → rotate Dt cut Cu goright wait
by OverlapClosure OC 3
rewrite t u → rotate Dt cut goright Au wait
by OverlapClosure OC 3
rewrite t u → rotate cut moveleft Bt Au wait
by OverlapClosure OC 3
rewrite t u → rotate cut Cu moveleft Bt wait
by OverlapClosure OC 2
rewrite t u → rotate cut Cu guess t
by OverlapClosure OC 3
rewrite t u → begin u t
by original rule (OC 1)
begin u → rotate cut Cu guess
by original rule (OC 1)
guess t → moveleft Bt wait
by original rule (OC 1)
Cu moveleft Bt → moveleft Bt Au
by original rule (OC 1)
cut moveleft Bt → Dt cut goright
by original rule (OC 1)
goright Au → Cu goright
by original rule (OC 1)
goright wait end → finish end
by original rule (OC 1)
Cu finish → finish u
by original rule (OC 1)
cut finish → finish2
by original rule (OC 1)
Dt finish2 → finish2 t
by original rule (OC 1)
rotate finish2 → rewrite
by original rule (OC 1)

(2) NO