[Termtools] jambox?

[Peter Schneider-Kamp]

Hi,

ist there something wrong with jambox? It performs a bit poorer
on SRSs than I expected (still much better than AProVE), but
on TRSs it cannot even prove termination of the (in)famous
quot-minus example of Arts & Giesl:

(VAR x y)
(RULES
minus(x,0)  -> x
minus(s(x),s(y)) -> minus(x,y)
quot(0,s(y)) -> 0
quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
)

This points to something being wrong with either jambox or
the way it is run.

Regards,
Peter
-- 
Peter Schneider-Kamp   mailto:psk at informatik.rwth-aachen.de
LuFG Informatik II     http://www-i2.informatik.rwth-aachen.de/~nowonder
RWTH Aachen            phone: ++49 241 80-21211