Incidentally, Jambox and TPA are the only tools that produced proof attempts for secret-jambox1. So this is now an open problem: (RULES a c -> a , a c b c -> c b c c , c -> b a a ) -- -- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 -- ---- http://www.imn.htwk-leipzig.de/~waldmann/ -------