Termination of Cycle Rewriting of Selected Problems

Explanations:

  • Cell entries:

    YEStermination proved
    NOtermination disproved
    TIMEOUTtimeout limit reached, no result
    MAYBEtool answers 'maybe', no result


  • Note that available outputs (e.g. proofs) are linked with the entries.
  • Note that the columns AProVE and TTT2 prove SRS termination NOT termination of cycle rewriting!

Timeout:

For all tests a timeout of 900 sec. was used. In detail:
  • 900 sec. for torpacyc 2014, torpacyc 2015, and AProVE and TTT2 (for the SRS and all three encodings SPLIT, ROTATE, and SHIFT)
  • Combination, variant 1: 450 sec. for torpacyc and 450 sec. for AProVE/TTT2, where SPLIT is applied to the (perhaps simplified) SRS which results from the run of torpacyc
  • Combination, variant 2: 225 sec. for AProVE/TTT2 on the SRS (only NO finishes the proof), 225 sec. for torpacyc, 450 sec. for AProVE/TTT2 where SPLIT is applied to the result of the torpacyc-result

Results:

String termination Cycle termination
Folder Problem SRS AProVE TTT2 torpacyc SPLIT ROTATE SHIFT Combination
(XML) (TXT) 2014 2015 (TXT) AProVE TTT2 (TXT) AProVE TTT2 (TXT) AProVE TTT2 Variant 1 Variant 2
AProVE TTT2 AProVE TTT2
Summary
Sum YES 11 10 3 9 8 9 1 1 1 2 10 9 9 9
Sum NO 0 0 0 0 1 1 1 0 1 1 1 1 0 1
Sum MAYBE\|TIMEOUT\|CRASHED\|EMPTYRHS 0 1 8 2 2 1 9 10 9 8 0 1 2 1
collection aa-aba .xml .srs YES YES YES YES .srs YES YES .srs TIMEOUT TIMEOUT .srs TIMEOUT YES YES YES YES YES
collection ab-baPhi .xml .srs YES YES TIMEOUT YES .srs YES YES .srs TIMEOUT TIMEOUT .srs TIMEOUT TIMEOUT YES YES YES YES
collection ab-ba .xml .srs YES YES MAYBE MAYBE .srs NO NO .srs NO TIMEOUT .srs NO NO NO NO TIMEOUT NO
collection a-bPhi .xml .srs YES YES YES YES .srs YES YES .srs TIMEOUT TIMEOUT .srs TIMEOUT TIMEOUT YES YES YES YES
collection a-b .xml .srs YES YES YES YES .srs YES YES .srs YES YES .srs YES YES YES YES YES YES
collection bincount4 .xml .srs YES YES TIMEOUT YES .srs YES YES .srs TIMEOUT TIMEOUT .srs TIMEOUT TIMEOUT YES YES YES YES
collection bincountremove .xml .srs YES YES TIMEOUT YES .srs YES YES .srs TIMEOUT TIMEOUT .srs TIMEOUT TIMEOUT YES YES YES YES
collection bincount .xml .srs YES YES TIMEOUT YES .srs TIMEOUT YES .srs TIMEOUT TIMEOUT .srs TIMEOUT TIMEOUT YES YES YES YES
collection doubly-expPhi .xml .srs YES YES TIMEOUT YES .srs TIMEOUT YES .srs TIMEOUT TIMEOUT .srs TIMEOUT TIMEOUT YES YES YES YES
collection lata10 .xml .srs YES YES TIMEOUT YES .srs YES YES .srs TIMEOUT TIMEOUT .srs TIMEOUT TIMEOUT YES YES YES YES
collection towerPhi .xml .srs YES TIMEOUT TIMEOUT TIMEOUT .srs YES TIMEOUT .srs TIMEOUT TIMEOUT .srs TIMEOUT TIMEOUT YES MAYBE TIMEOUT MAYBE
Navigation [+/-]