Dear all, I find this astonishing: http://www.lri.fr/%7Emarche/termination-competition/2007/webform.cgi?command=viewres&file=srs-standard.db&tool=ttt2&prob=SRS.Zantema.z090.srs to my knowledge, this would be the first automatic proof for an SRS with non-prim-rec complexity. I'm not saying it's impossible. Best regards, Johannes.