MAYBE 1185.55/297.32 MAYBE 1185.55/297.32 1185.55/297.32 We are left with following problem, upon which TcT provides the 1185.55/297.32 certificate MAYBE. 1185.55/297.32 1185.55/297.32 Strict Trs: 1185.55/297.32 { a(a(a(a(x1)))) -> A(A(A(x1))) 1185.55/297.32 , a(b(x1)) -> C(x1) 1185.55/297.32 , a(A(x1)) -> x1 1185.55/297.32 , b(b(b(b(x1)))) -> B(B(B(x1))) 1185.55/297.32 , b(c(x1)) -> A(x1) 1185.55/297.32 , b(B(x1)) -> x1 1185.55/297.32 , C(b(b(b(x1)))) -> a(B(B(B(x1)))) 1185.55/297.32 , C(C(C(a(x1)))) -> c(c(c(B(x1)))) 1185.55/297.32 , C(C(C(C(x1)))) -> c(c(c(x1))) 1185.55/297.32 , C(c(x1)) -> x1 1185.55/297.32 , C(B(x1)) -> a(x1) 1185.55/297.32 , c(a(x1)) -> B(x1) 1185.55/297.32 , c(C(x1)) -> x1 1185.55/297.32 , c(c(c(c(x1)))) -> C(C(C(x1))) 1185.55/297.32 , A(a(x1)) -> x1 1185.55/297.32 , A(C(x1)) -> b(x1) 1185.55/297.32 , A(c(c(c(x1)))) -> b(C(C(C(x1)))) 1185.55/297.32 , A(A(A(b(x1)))) -> a(a(a(C(x1)))) 1185.55/297.32 , A(A(A(A(x1)))) -> a(a(a(x1))) 1185.55/297.32 , B(a(a(a(x1)))) -> c(A(A(A(x1)))) 1185.55/297.32 , B(b(x1)) -> x1 1185.55/297.32 , B(A(x1)) -> c(x1) 1185.55/297.32 , B(B(B(c(x1)))) -> b(b(b(A(x1)))) 1185.55/297.32 , B(B(B(B(x1)))) -> b(b(b(x1))) } 1185.55/297.32 Obligation: 1185.55/297.32 derivational complexity 1185.55/297.32 Answer: 1185.55/297.32 MAYBE 1185.55/297.32 1185.55/297.32 None of the processors succeeded. 1185.55/297.32 1185.55/297.32 Details of failed attempt(s): 1185.55/297.32 ----------------------------- 1185.55/297.32 1) 'Inspecting Problem... (timeout of 297 seconds)' failed due to 1185.55/297.32 the following reason: 1185.55/297.32 1185.55/297.32 Computation stopped due to timeout after 297.0 seconds. 1185.55/297.32 1185.55/297.32 2) 'iteProgress (timeout of 297 seconds)' failed due to the 1185.55/297.32 following reason: 1185.55/297.32 1185.55/297.32 Computation stopped due to timeout after 297.0 seconds. 1185.55/297.32 1185.55/297.32 3) 'bsearch-matrix (timeout of 297 seconds)' failed due to the 1185.55/297.32 following reason: 1185.55/297.32 1185.55/297.32 The input cannot be shown compatible 1185.55/297.32 1185.55/297.32 4) 'Fastest (timeout of 60 seconds)' failed due to the following 1185.55/297.32 reason: 1185.55/297.32 1185.55/297.32 Computation stopped due to timeout after 60.0 seconds. 1185.55/297.32 1185.55/297.32 1185.55/297.32 Arrrr.. 1186.00/297.50 EOF