Problem Zantema 04 z069

Tool Bounds

Execution Time	60.046623ms
Answer	TIMEOUT
Input	Zantema 04 z069

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  C(c(x1)) -> x1
     , c(C(x1)) -> x1
     , B(b(x1)) -> x1
     , b(B(x1)) -> x1
     , A(a(x1)) -> x1
     , a(A(x1)) -> x1
     , C(C(C(a(x1)))) -> c(c(c(B(x1))))
     , A(c(c(c(x1)))) -> b(C(C(C(x1))))
     , B(B(B(c(x1)))) -> b(b(b(A(x1))))
     , C(b(b(b(x1)))) -> a(B(B(B(x1))))
     , A(A(A(b(x1)))) -> a(a(a(C(x1))))
     , B(a(a(a(x1)))) -> c(A(A(A(x1))))
     , C(C(C(C(x1)))) -> c(c(c(x1)))
     , c(c(c(c(x1)))) -> C(C(C(x1)))
     , B(B(B(B(x1)))) -> b(b(b(x1)))
     , b(b(b(b(x1)))) -> B(B(B(x1)))
     , A(A(A(A(x1)))) -> a(a(a(x1)))
     , a(a(a(a(x1)))) -> A(A(A(x1)))
     , B(A(x1)) -> c(x1)
     , C(B(x1)) -> a(x1)
     , A(C(x1)) -> b(x1)
     , c(a(x1)) -> B(x1)
     , b(c(x1)) -> A(x1)
     , a(b(x1)) -> C(x1)}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool CDI

Execution Time	60.043976ms
Answer	TIMEOUT
Input	Zantema 04 z069

stdout:

TIMEOUT

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

Tool EDA

Execution Time	60.044548ms
Answer	TIMEOUT
Input	Zantema 04 z069

stdout:

Tool IDA

Execution Time	60.067596ms
Answer	TIMEOUT
Input	Zantema 04 z069

stdout:

Tool TRI

Execution Time	61.70396ms
Answer	TIMEOUT
Input	Zantema 04 z069

stdout:

Tool TRI2

Execution Time	2.09022ms
Answer	MAYBE
Input	Zantema 04 z069

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  C(c(x1)) -> x1
     , c(C(x1)) -> x1
     , B(b(x1)) -> x1
     , b(B(x1)) -> x1
     , A(a(x1)) -> x1
     , a(A(x1)) -> x1
     , C(C(C(a(x1)))) -> c(c(c(B(x1))))
     , A(c(c(c(x1)))) -> b(C(C(C(x1))))
     , B(B(B(c(x1)))) -> b(b(b(A(x1))))
     , C(b(b(b(x1)))) -> a(B(B(B(x1))))
     , A(A(A(b(x1)))) -> a(a(a(C(x1))))
     , B(a(a(a(x1)))) -> c(A(A(A(x1))))
     , C(C(C(C(x1)))) -> c(c(c(x1)))
     , c(c(c(c(x1)))) -> C(C(C(x1)))
     , B(B(B(B(x1)))) -> b(b(b(x1)))
     , b(b(b(b(x1)))) -> B(B(B(x1)))
     , A(A(A(A(x1)))) -> a(a(a(x1)))
     , a(a(a(a(x1)))) -> A(A(A(x1)))
     , B(A(x1)) -> c(x1)
     , C(B(x1)) -> a(x1)
     , A(C(x1)) -> b(x1)
     , c(a(x1)) -> B(x1)
     , b(c(x1)) -> A(x1)
     , a(b(x1)) -> C(x1)}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..