Problem Trafo 06 dup01

Tool Bounds

Execution Time	60.06126ms
Answer	TIMEOUT
Input	Trafo 06 dup01

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1))))
     , a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1))))
     , a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1))))
     , a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1))))
     , a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1))))
     , a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1))))
     , a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) ->
       x1
     , a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) ->
       x1
     , a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) ->
       x1
     , a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) ->
       x1
     , a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1))))))
     , a36(a36(x1)) ->
       a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1))))))))))
     , a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1))))))
     , a26(a26(x1)) ->
       a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))))
     , a25(a25(x1)) ->
       a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))))
     , a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1))))))
     , a16(a16(x1)) ->
       a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))))
     , a15(a15(x1)) ->
       a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))
     , a14(a14(x1)) ->
       a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))))
     , a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1))))))
     , a56(a56(a56(a56(x1)))) -> x1
     , a46(a46(a46(a46(x1)))) -> x1
     , a45(a45(a45(a45(x1)))) -> x1
     , a36(a36(a36(a36(x1)))) -> x1
     , a35(a35(a35(a35(x1)))) -> x1
     , a34(a34(a34(a34(x1)))) -> x1
     , a26(a26(a26(a26(x1)))) -> x1
     , a25(a25(a25(a25(x1)))) -> x1
     , a24(a24(a24(a24(x1)))) -> x1
     , a23(a23(a23(a23(x1)))) -> x1
     , a16(a16(a16(a16(x1)))) -> x1
     , a15(a15(a15(a15(x1)))) -> x1
     , a14(a14(a14(a14(x1)))) -> x1
     , a13(a13(a13(a13(x1)))) -> x1
     , a12(a12(a12(a12(x1)))) -> x1}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool CDI

Execution Time	60.045433ms
Answer	TIMEOUT
Input	Trafo 06 dup01

stdout:

TIMEOUT

Statistics:
Number of monomials: 0
Last formula building started for bound 0
Last SAT solving started for bound 0

Tool EDA

Execution Time	60.08104ms
Answer	TIMEOUT
Input	Trafo 06 dup01

stdout:

Tool IDA

Execution Time	60.108414ms
Answer	TIMEOUT
Input	Trafo 06 dup01

stdout:

Tool TRI

Execution Time	60.077312ms
Answer	TIMEOUT
Input	Trafo 06 dup01

stdout:

Tool TRI2

Execution Time	17.114624ms
Answer	MAYBE
Input	Trafo 06 dup01

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  a34(a34(a56(a56(x1)))) -> a56(a56(a34(a34(x1))))
     , a23(a23(a56(a56(x1)))) -> a56(a56(a23(a23(x1))))
     , a23(a23(a45(a45(x1)))) -> a45(a45(a23(a23(x1))))
     , a12(a12(a56(a56(x1)))) -> a56(a56(a12(a12(x1))))
     , a12(a12(a45(a45(x1)))) -> a45(a45(a12(a12(x1))))
     , a12(a12(a34(a34(x1)))) -> a34(a34(a12(a12(x1))))
     , a45(a45(a56(a56(a45(a45(a56(a56(a45(a45(a56(a56(x1)))))))))))) ->
       x1
     , a34(a34(a45(a45(a34(a34(a45(a45(a34(a34(a45(a45(x1)))))))))))) ->
       x1
     , a23(a23(a34(a34(a23(a23(a34(a34(a23(a23(a34(a34(x1)))))))))))) ->
       x1
     , a12(a12(a23(a23(a12(a12(a23(a23(a12(a12(a23(a23(x1)))))))))))) ->
       x1
     , a46(a46(x1)) -> a45(a45(a56(a56(a45(a45(x1))))))
     , a36(a36(x1)) ->
       a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(x1))))))))))
     , a35(a35(x1)) -> a34(a34(a45(a45(a34(a34(x1))))))
     , a26(a26(x1)) ->
       a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(x1))))))))))))))
     , a25(a25(x1)) ->
       a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(x1))))))))))
     , a24(a24(x1)) -> a23(a23(a34(a34(a23(a23(x1))))))
     , a16(a16(x1)) ->
       a12(a12(a23(a23(a34(a34(a45(a45(a56(a56(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))))))
     , a15(a15(x1)) ->
       a12(a12(a23(a23(a34(a34(a45(a45(a34(a34(a23(a23(a12(a12(x1))))))))))))))
     , a14(a14(x1)) ->
       a12(a12(a23(a23(a34(a34(a23(a23(a12(a12(x1))))))))))
     , a13(a13(x1)) -> a12(a12(a23(a23(a12(a12(x1))))))
     , a56(a56(a56(a56(x1)))) -> x1
     , a46(a46(a46(a46(x1)))) -> x1
     , a45(a45(a45(a45(x1)))) -> x1
     , a36(a36(a36(a36(x1)))) -> x1
     , a35(a35(a35(a35(x1)))) -> x1
     , a34(a34(a34(a34(x1)))) -> x1
     , a26(a26(a26(a26(x1)))) -> x1
     , a25(a25(a25(a25(x1)))) -> x1
     , a24(a24(a24(a24(x1)))) -> x1
     , a23(a23(a23(a23(x1)))) -> x1
     , a16(a16(a16(a16(x1)))) -> x1
     , a15(a15(a15(a15(x1)))) -> x1
     , a14(a14(a14(a14(x1)))) -> x1
     , a13(a13(a13(a13(x1)))) -> x1
     , a12(a12(a12(a12(x1)))) -> x1}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..