[Termtools] strange proof

[Claude Marché]

When runnning torpa directly on that problem, I get a full proof. So
the problem from the engine running tools. But I do not know where,
never seen that before.  I managed to get torpa running again on that
particular. 

If someone sees a similar problem, please tell me. I do not see any
other way to do apart from running the tool again on the problem.

- Claude

>>>>> "Zantema," == Zantema, H <h.zantema at TUE.nl> writes:

    >> Jörg Endrullis notes that this proof is at least incomplete:
    Zantema,> http://www.lri.fr/~marche/termination-competition/2007/webform.cgi?command=viewres&file=srs-standard.db&tool=torpa&prob=SRS.Gebhardt.02.srs


    Zantema,> This is strange, on my computer the output is correct, see below. It is always found in at most 20 seconds, and sometimes an alternative proof is found using nested labelling. This latter proof is found in a fraction of a second.

    Zantema,>             Best regards, Hans Zantema.

    Zantema,> _________________________________________________________
    Zantema,> Dr Hans Zantema            
    Zantema,> Technische Universiteit Eindhoven, Department of Computer Science 
    Zantema,> P.O. Box 513, 5600 MB Eindhoven, The Netherlands 
    Zantema,> e-mail: H.Zantema at tue.nl, homepage: www.win.tue.nl/~hzantema
    Zantema,> office: Hoofdgebouw room 6.73, tel: (040)2472749




    Zantema,> YES
    Zantema,> TORPA version 1.7 is applied to
    Zantema,> 0 0 0 0  -> 0 0 0 1 ,
    Zantema,> 1 0 0 1  -> 0 1 0 0 ,
    Zantema,> [CG] Reversed dependency pair transformation:
    Zantema,>   0 0 0 0  ->= 1 0 0 0 
    Zantema,>   1 0 0 1  ->= 0 0 1 0 
    Zantema,>   #0 0 0 0  -> #1 0 0 0 
    Zantema,>   #0 0 0 0  -> #0 0 0 
    Zantema,>   #0 0 0 0  -> #0 0 
    Zantema,>   #0 0 0 0  -> #0 
    Zantema,>   #1 0 0 1  -> #0 0 1 0 
    Zantema,>   #1 0 0 1  -> #0 1 0 
    Zantema,>   #1 0 0 1  -> #1 0 
    Zantema,>   #1 0 0 1  -> #0 
    Zantema,> [A] Choose polynomial interpretation   0 1 #0 #1: lambda x.x+1
    Zantema,> remove: #0 0 0 0  -> #0 0 0 
    Zantema,> remove: #0 0 0 0  -> #0 0 
    Zantema,> remove: #0 0 0 0  -> #0 
    Zantema,> remove: #1 0 0 1  -> #0 1 0 
    Zantema,> remove: #1 0 0 1  -> #1 0 
    Zantema,> remove: #1 0 0 1  -> #0 
    Zantema,> Remaining rules:
    Zantema,>     0 0 0 0  ->= 1 0 0 0 
    Zantema,>     1 0 0 1  ->= 0 0 1 0 
    Zantema,>     #0 0 0 0  -> #1 0 0 0 
    Zantema,>     #1 0 0 1  -> #0 0 1 0 
    Zantema,> [A] Choose quasi-periodic interpretation:
    Zantema,> [0](0) = 4
    Zantema,> [0](1) = 5
    Zantema,> [0](2) = 8
    Zantema,> [0](3) = 8
    Zantema,> [0](4) = 8
    Zantema,> [0](x+5) = [0](x)+5
    Zantema,> [1](0) = 6
    Zantema,> [1](1) = 6
    Zantema,> [1](2) = 6
    Zantema,> [1](3) = 6
    Zantema,> [1](4) = 9
    Zantema,> [1](x+5) = [1](x)+5
    Zantema,> [#0](0) = 0
    Zantema,> [#0](1) = 1
    Zantema,> [#0](2) = 1
    Zantema,> [#0](3) = 1
    Zantema,> [#0](4) = 1
    Zantema,> [#0](x+5) = [#0](x)+5
    Zantema,> [#1](0) = 1
    Zantema,> [#1](1) = 1
    Zantema,> [#1](2) = 1
    Zantema,> [#1](3) = 1
    Zantema,> [#1](4) = 6
    Zantema,> [#1](x+5) = [#1](x)+5
    Zantema,> remove: #1 0 0 1  -> #0 0 1 0 
    Zantema,> remaining rules:
    Zantema,> 0 0 0 0  ->= 1 0 0 0 
    Zantema,> 1 0 0 1  ->= 0 0 1 0 
    Zantema,> #0 0 0 0  -> #1 0 0 0 
    Zantema,> [A] Choose polynomial interpretation   #0: lambda x.x+1,  rest identity
    Zantema,> remove: #0 0 0 0  -> #1 0 0 0 
    Zantema,> Relatively terminating since no strict rules remain.


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

-- 
Claude Marché                          | tel: +33 1 72 92 59 69           
INRIA Futurs - ProVal                  | mobile: +33 6 33 14 57 93 
Parc Orsay Université - ZAC des Vignes | fax: +33 1 74 85 42 29   
3, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |