Problem Transformed outermost 08 f4

Tool Bounds

Execution Time	60.03802ms
Answer	TIMEOUT
Input	Transformed outermost 08 f4

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  f_1(f_1(f_1(f_1(x)))) -> c_0()
     , f_1(f_1(f_1(f_0(x)))) -> c_0()
     , f_1(f_0(f_0(f_0(x)))) -> c_0()
     , f_1(f_1(f_0(f_0(x)))) -> c_0()
     , f_0(f_0(f_0(a_1()))) -> f_1(f_0(f_0(f_0(a_1()))))
     , *top*_0(f_0(f_0(a_1()))) -> *top*_0(f_0(f_0(f_0(a_1()))))
     , *top*_0(f_0(a_1())) -> *top*_0(f_0(f_0(a_1())))
     , *top*_0(a_1()) -> *top*_0(f_0(a_1()))}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool CDI

Execution Time	60.045002ms
Answer	TIMEOUT
Input	Transformed outermost 08 f4

stdout:

TIMEOUT

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

Tool EDA

Execution Time	60.041016ms
Answer	TIMEOUT
Input	Transformed outermost 08 f4

stdout:

Tool IDA

Execution Time	60.053764ms
Answer	TIMEOUT
Input	Transformed outermost 08 f4

stdout:

Tool TRI

Execution Time	60.035263ms
Answer	TIMEOUT
Input	Transformed outermost 08 f4

stdout:

Tool TRI2

Execution Time	0.57362413ms
Answer	MAYBE
Input	Transformed outermost 08 f4

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  f_1(f_1(f_1(f_1(x)))) -> c_0()
     , f_1(f_1(f_1(f_0(x)))) -> c_0()
     , f_1(f_0(f_0(f_0(x)))) -> c_0()
     , f_1(f_1(f_0(f_0(x)))) -> c_0()
     , f_0(f_0(f_0(a_1()))) -> f_1(f_0(f_0(f_0(a_1()))))
     , *top*_0(f_0(f_0(a_1()))) -> *top*_0(f_0(f_0(f_0(a_1()))))
     , *top*_0(f_0(a_1())) -> *top*_0(f_0(f_0(a_1())))
     , *top*_0(a_1()) -> *top*_0(f_0(a_1()))}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..