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

(0) Obligation:

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

and(not(not(x)), y, not(z)) → and(y, band(x, z), x)

Q is empty.