[Termtools] competition

[Salvador Lucas]

Zantema, H. wrote:

>In the mean time Cime produced two YES answers where other tools
>produced NO:
>TRSCS_Ex_4_4_Luc96B_FR and TRSCS_Ex_4_4_Luc96B_Z.
>
>Since the NO is correct, unfortunately now Cime is disqualified
>according the rules.
>
>I expect that the MU-Term proof of Zantema-z12 is not correct. Salvador
>(or any other having MUTerm running): can you check the system 
>
>(VAR x y )
>(RULES
>f(x,a(b(y))) -> f(a(a(b(b(x)))),y)
>f(a(x),y) -> f(x,a(y))
>f(b(x),y) -> f(x,b(y))
>)
>
>and tell me the outcome?
>
The 'proof' reported by MU-TERM is not correct. There must
be a bug in the computation of the dependency graph...

Best regards,

Salvador.

_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools