MAYBE 1115.45/297.03 MAYBE 1115.45/297.03 1115.45/297.03 We are left with following problem, upon which TcT provides the 1115.45/297.03 certificate MAYBE. 1115.45/297.03 1115.45/297.03 Strict Trs: 1115.45/297.03 { sq(0(x1)) -> 1115.45/297.03 p(s(p(s(p(p(p(p(s(s(s(s(0(p(s(p(s(x1))))))))))))))))) 1115.45/297.03 , sq(s(x1)) -> 1115.45/297.03 s(p(s(p(s(p(p(s(s(twice(p(s(p(s(p(p(p(s(s(s(sq(p(p(p(p(p(p(s(s(s(s(s(s(x1))))))))))))))))))))))))))))))))) 1115.45/297.03 , 0(x1) -> x1 1115.45/297.03 , p(0(x1)) -> 0(s(s(s(s(s(s(s(s(s(s(s(x1)))))))))))) 1115.45/297.03 , p(p(s(x1))) -> p(x1) 1115.45/297.03 , p(s(x1)) -> x1 1115.45/297.03 , twice(0(x1)) -> 1115.45/297.03 p(p(p(p(s(s(p(s(s(s(0(p(p(p(s(s(s(p(p(s(s(p(s(p(s(p(s(x1))))))))))))))))))))))))))) 1115.45/297.03 , twice(s(x1)) -> 1115.45/297.03 p(p(s(s(s(p(p(s(s(s(twice(p(s(p(s(x1))))))))))))))) } 1115.45/297.03 Obligation: 1115.45/297.03 derivational complexity 1115.45/297.03 Answer: 1115.45/297.03 MAYBE 1115.45/297.03 1115.45/297.03 None of the processors succeeded. 1115.45/297.03 1115.45/297.03 Details of failed attempt(s): 1115.45/297.03 ----------------------------- 1115.45/297.03 1) 'bsearch-matrix (timeout of 297 seconds)' failed due to the 1115.45/297.03 following reason: 1115.45/297.03 1115.45/297.03 Computation stopped due to timeout after 297.0 seconds. 1115.45/297.03 1115.45/297.03 2) 'Inspecting Problem... (timeout of 297 seconds)' failed due to 1115.45/297.03 the following reason: 1115.45/297.03 1115.45/297.03 Computation stopped due to timeout after 297.0 seconds. 1115.45/297.03 1115.45/297.03 3) 'iteProgress (timeout of 297 seconds)' failed due to the 1115.45/297.03 following reason: 1115.45/297.03 1115.45/297.03 Computation stopped due to timeout after 297.0 seconds. 1115.45/297.03 1115.45/297.03 4) 'Fastest (timeout of 60 seconds)' failed due to the following 1115.45/297.03 reason: 1115.45/297.03 1115.45/297.03 Computation stopped due to timeout after 60.0 seconds. 1115.45/297.03 1115.45/297.03 1115.45/297.03 Arrrr.. 1115.90/297.49 EOF