[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?
>
We have fixed the bug. The new version of MU-TERM is not
able to prove termination of this system (see below).

Thanks,

Salvador.

Dependency Pairs and Strongly Connected Components
-----------------------------------------------------------------------------------------
-> Dependency pairs:
nF_f(x,a(a(b(b(y))))) -> nF_f(a(a(a(b(b(b(x)))))),y)
nF_f(a(x),y) -> nF_f(x,a(y))
nF_f(b(x),y) -> nF_f(x,b(y))

-> -> Dependency pairs in cycle:
-> -> Dependency pairs in cycle:
nF_f(x,a(a(b(b(y))))) -> nF_f(a(a(a(b(b(b(x)))))),y)
nF_f(a(x),y) -> nF_f(x,a(y))
nF_f(b(x),y) -> nF_f(x,b(y))

-> Proof of termination for ExZ12:
No proof was found.
SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 2
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: Rationals and integers
Delta: automatic

Total elapsed time: 00h 00m 21s 46cent

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