Problem Mixed SRS s6

Tool Bounds

Execution Time	60.06883ms
Answer	TIMEOUT
Input	Mixed SRS s6

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  a34(a56(x1)) -> a56(a34(x1))
     , a23(a56(x1)) -> a56(a23(x1))
     , a23(a45(x1)) -> a45(a23(x1))
     , a12(a56(x1)) -> a56(a12(x1))
     , a12(a45(x1)) -> a45(a12(x1))
     , a12(a34(x1)) -> a34(a12(x1))
     , a45(a56(a45(a56(a45(a56(x1)))))) -> x1
     , a34(a45(a34(a45(a34(a45(x1)))))) -> x1
     , a23(a34(a23(a34(a23(a34(x1)))))) -> x1
     , a12(a23(a12(a23(a12(a23(x1)))))) -> x1
     , a46(x1) -> a45(a56(a45(x1)))
     , a36(x1) -> a34(a45(a56(a45(a34(x1)))))
     , a35(x1) -> a34(a45(a34(x1)))
     , a26(x1) -> a23(a34(a45(a56(a45(a34(a23(x1)))))))
     , a25(x1) -> a23(a34(a45(a34(a23(x1)))))
     , a24(x1) -> a23(a34(a23(x1)))
     , a16(x1) -> a12(a23(a34(a45(a56(a45(a34(a23(a12(x1)))))))))
     , a15(x1) -> a12(a23(a34(a45(a34(a23(a12(x1)))))))
     , a14(x1) -> a12(a23(a34(a23(a12(x1)))))
     , a13(x1) -> a12(a23(a12(x1)))
     , a56(a56(x1)) -> x1
     , a46(a46(x1)) -> x1
     , a45(a45(x1)) -> x1
     , a36(a36(x1)) -> x1
     , a35(a35(x1)) -> x1
     , a34(a34(x1)) -> x1
     , a26(a26(x1)) -> x1
     , a25(a25(x1)) -> x1
     , a24(a24(x1)) -> x1
     , a23(a23(x1)) -> x1
     , a16(a16(x1)) -> x1
     , a15(a15(x1)) -> x1
     , a14(a14(x1)) -> x1
     , a13(a13(x1)) -> x1
     , 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.044636ms
Answer	TIMEOUT
Input	Mixed SRS s6

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.079205ms
Answer	TIMEOUT
Input	Mixed SRS s6

stdout:

Tool IDA

Execution Time	60.07182ms
Answer	TIMEOUT
Input	Mixed SRS s6

stdout:

Tool TRI

Execution Time	60.055252ms
Answer	TIMEOUT
Input	Mixed SRS s6

stdout:

Tool TRI2

Execution Time	2.398774ms
Answer	MAYBE
Input	Mixed SRS s6

stdout:

MAYBE

We consider the following Problem:

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

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..