Problem Zantema 04 z070

Tool Bounds

Execution Time	60.046562ms
Answer	TIMEOUT
Input	Zantema 04 z070

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(c(B(x1)))))
     , A(c(c(c(c(x1))))) -> b(C(C(C(x1))))
     , B(B(B(c(x1)))) -> b(b(b(b(A(x1)))))
     , C(b(b(b(b(x1))))) -> a(B(B(B(x1))))
     , A(A(A(b(x1)))) -> a(a(a(a(C(x1)))))
     , B(a(a(a(a(x1))))) -> c(A(A(A(x1))))
     , C(C(C(C(x1)))) -> c(c(c(c(x1))))
     , c(c(c(c(c(x1))))) -> C(C(C(x1)))
     , B(B(B(B(x1)))) -> b(b(b(b(x1))))
     , b(b(b(b(b(x1))))) -> B(B(B(x1)))
     , A(A(A(A(x1)))) -> a(a(a(a(x1))))
     , a(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.04345ms
Answer	TIMEOUT
Input	Zantema 04 z070

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.048157ms
Answer	TIMEOUT
Input	Zantema 04 z070

stdout:

Tool IDA

Execution Time	60.049458ms
Answer	TIMEOUT
Input	Zantema 04 z070

stdout:

Tool TRI

Execution Time	60.043217ms
Answer	TIMEOUT
Input	Zantema 04 z070

stdout:

Tool TRI2

Execution Time	2.154056ms
Answer	MAYBE
Input	Zantema 04 z070

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(c(B(x1)))))
     , A(c(c(c(c(x1))))) -> b(C(C(C(x1))))
     , B(B(B(c(x1)))) -> b(b(b(b(A(x1)))))
     , C(b(b(b(b(x1))))) -> a(B(B(B(x1))))
     , A(A(A(b(x1)))) -> a(a(a(a(C(x1)))))
     , B(a(a(a(a(x1))))) -> c(A(A(A(x1))))
     , C(C(C(C(x1)))) -> c(c(c(c(x1))))
     , c(c(c(c(c(x1))))) -> C(C(C(x1)))
     , B(B(B(B(x1)))) -> b(b(b(b(x1))))
     , b(b(b(b(b(x1))))) -> B(B(B(x1)))
     , A(A(A(A(x1)))) -> a(a(a(a(x1))))
     , a(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..