Tool Bounds
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ 2(2(2(0(0(1(0(0(2(0(0(2(1(1(2(1(0(1(2(2(2(1(0(x1)))))))))))))))))))))))
->
1(2(2(2(2(0(1(2(1(2(0(1(2(1(2(1(0(1(0(1(0(1(1(2(2(1(0(x1)))))))))))))))))))))))))))
, 2(2(1(2(2(0(0(2(1(1(0(2(2(0(2(2(0(2(2(1(2(0(2(x1)))))))))))))))))))))))
->
1(2(1(1(1(2(2(2(1(2(1(0(2(1(1(1(1(2(2(0(0(1(1(0(2(1(2(x1)))))))))))))))))))))))))))
, 2(2(1(2(1(2(2(2(0(1(2(1(2(2(2(2(1(1(0(1(0(1(0(x1)))))))))))))))))))))))
->
1(2(1(2(1(2(0(1(2(2(0(1(1(1(2(2(1(1(1(2(2(0(1(0(1(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(2(2(1(2(1(1(1(0(0(2(1(1(0(2(0(0(1(1(2(x1)))))))))))))))))))))))
->
2(1(1(1(2(2(2(1(1(0(2(2(1(0(1(0(2(2(1(2(0(0(0(1(2(1(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(2(0(0(2(2(2(2(1(1(1(1(1(2(1(2(0(0(1(1(x1)))))))))))))))))))))))
->
2(2(1(1(2(2(1(2(1(2(2(0(0(0(2(1(0(2(2(1(2(2(0(1(1(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(1(2(0(1(1(2(2(0(1(1(1(1(1(2(2(2(0(2(1(x1)))))))))))))))))))))))
->
1(2(1(2(2(1(1(1(1(2(2(2(1(2(0(0(0(1(2(0(0(1(2(2(2(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(1(0(0(2(1(0(2(1(2(0(0(2(1(0(1(1(2(2(1(x1)))))))))))))))))))))))
->
2(1(2(2(0(1(2(1(1(0(1(2(1(0(0(1(2(2(1(2(1(0(2(1(2(2(1(x1)))))))))))))))))))))))))))
, 2(2(0(1(2(2(2(0(2(2(2(0(2(2(2(2(1(0(1(0(0(1(0(x1)))))))))))))))))))))))
->
2(2(0(1(1(2(2(2(1(1(2(1(0(0(1(2(2(1(2(1(0(2(2(0(0(2(0(x1)))))))))))))))))))))))))))
, 2(2(0(1(1(0(0(1(2(1(0(2(1(2(2(2(1(0(0(2(2(2(0(x1)))))))))))))))))))))))
->
2(2(1(0(0(0(0(2(2(1(1(2(2(1(0(2(1(2(1(2(2(1(2(2(2(0(0(x1)))))))))))))))))))))))))))
, 2(2(0(0(2(1(2(0(1(2(0(2(1(0(1(1(2(2(1(0(1(0(2(x1)))))))))))))))))))))))
->
2(2(2(2(1(2(1(2(0(2(2(2(2(2(0(1(2(0(2(1(0(0(0(2(0(2(2(x1)))))))))))))))))))))))))))
, 2(2(0(0(1(2(1(1(2(1(0(0(0(0(0(2(1(2(1(1(2(0(2(x1)))))))))))))))))))))))
->
2(1(1(2(2(2(2(1(2(1(0(0(2(1(0(2(2(0(1(1(0(2(0(0(0(0(2(x1)))))))))))))))))))))))))))
, 2(2(0(0(1(0(1(2(2(2(1(1(0(0(1(2(2(1(2(0(1(2(1(x1)))))))))))))))))))))))
->
2(2(2(2(0(2(0(2(2(1(2(1(0(1(1(2(2(0(0(2(1(2(1(2(1(2(0(x1)))))))))))))))))))))))))))
, 2(1(2(1(0(2(1(2(0(0(0(0(2(0(0(0(2(2(0(0(0(0(1(x1)))))))))))))))))))))))
->
2(1(2(1(2(0(0(2(1(0(0(2(2(0(1(0(2(1(2(1(2(2(1(2(1(1(2(x1)))))))))))))))))))))))))))
, 2(1(1(0(2(2(2(0(1(2(1(1(0(1(2(0(0(1(1(1(1(2(2(x1)))))))))))))))))))))))
->
2(0(0(2(1(0(0(0(0(0(1(2(1(1(2(1(1(2(1(2(2(0(1(1(1(2(2(x1)))))))))))))))))))))))))))
, 2(1(0(1(1(2(0(0(2(1(0(0(0(1(2(1(1(2(0(2(1(2(1(x1)))))))))))))))))))))))
->
2(0(2(2(0(0(2(2(1(1(1(2(0(1(0(1(2(2(2(2(2(0(0(0(2(2(1(x1)))))))))))))))))))))))))))
, 2(1(0(1(0(0(2(2(2(0(1(0(0(2(0(0(1(2(0(2(2(2(0(x1)))))))))))))))))))))))
->
2(1(1(2(0(1(2(0(0(2(0(1(2(2(1(1(1(2(2(2(0(0(1(1(0(2(0(x1)))))))))))))))))))))))))))
, 2(0(2(0(1(2(2(0(0(2(2(2(1(1(1(2(1(0(2(0(2(2(0(x1)))))))))))))))))))))))
->
2(1(1(1(2(2(0(0(0(2(1(0(0(0(1(1(0(2(2(0(2(2(2(2(2(2(0(x1)))))))))))))))))))))))))))
, 2(0(2(0(1(0(1(1(2(0(1(1(2(2(1(0(2(0(2(0(2(2(2(x1)))))))))))))))))))))))
->
2(0(0(1(1(2(0(2(2(1(1(2(2(0(1(2(2(2(0(0(2(0(2(2(2(0(2(x1)))))))))))))))))))))))))))
, 2(0(1(0(0(0(1(0(0(0(0(0(0(0(1(0(2(0(0(2(2(2(2(x1)))))))))))))))))))))))
->
2(2(2(1(1(2(1(2(0(1(1(2(1(0(2(1(0(0(1(0(1(1(2(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(2(2(2(1(1(0(0(2(2(2(0(0(0(2(1(2(2(0(2(0(2(0(x1)))))))))))))))))))))))
->
1(2(1(2(0(0(1(1(1(2(2(2(2(1(2(2(2(0(2(0(1(2(2(2(2(0(0(x1)))))))))))))))))))))))))))
, 1(2(0(2(1(2(2(1(2(2(2(0(1(1(1(1(0(1(0(0(2(0(1(x1)))))))))))))))))))))))
->
1(2(1(2(1(2(2(2(2(2(2(0(0(2(0(0(2(2(0(1(1(1(1(0(0(2(1(x1)))))))))))))))))))))))))))
, 1(2(0(0(2(0(1(2(2(0(2(1(2(1(2(0(1(0(1(2(0(2(1(x1)))))))))))))))))))))))
->
1(2(2(0(2(1(2(2(0(1(0(2(1(0(1(2(1(2(2(2(2(0(2(2(0(2(0(x1)))))))))))))))))))))))))))
, 1(1(2(2(1(0(2(0(1(1(2(2(2(1(0(1(0(0(2(1(1(0(2(x1)))))))))))))))))))))))
->
2(2(2(1(1(2(2(2(1(2(2(0(0(2(0(0(1(2(0(2(2(1(2(2(2(0(2(x1)))))))))))))))))))))))))))
, 1(1(1(0(2(2(1(1(1(2(2(0(2(0(2(1(1(2(1(2(1(2(2(x1)))))))))))))))))))))))
->
1(2(1(2(1(1(1(1(2(1(1(1(2(2(0(1(0(2(2(1(2(2(2(1(0(1(2(x1)))))))))))))))))))))))))))
, 1(1(0(2(1(2(2(2(2(1(0(1(2(0(1(2(1(1(0(2(1(2(0(x1)))))))))))))))))))))))
->
2(2(1(2(1(2(2(1(0(1(2(2(2(1(0(2(1(1(2(1(0(1(1(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(2(1(0(2(0(1(2(0(2(0(0(2(1(0(1(0(1(2(1(2(x1)))))))))))))))))))))))
->
2(0(2(2(1(1(1(2(2(0(1(2(0(2(1(1(2(1(0(0(2(0(1(2(2(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(1(2(2(2(2(1(0(2(1(2(0(0(0(1(0(2(1(1(1(2(x1)))))))))))))))))))))))
->
2(1(2(1(2(2(2(2(2(0(0(0(0(2(1(2(2(2(2(1(2(2(2(0(0(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(0(1(1(1(2(2(2(1(2(1(0(0(0(2(2(2(0(1(2(0(x1)))))))))))))))))))))))
->
2(1(2(1(2(2(2(1(2(2(0(2(2(1(0(2(1(2(2(0(1(0(1(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(0(1(0(2(2(2(2(1(0(0(2(0(2(1(2(1(2(1(1(2(0(2(x1)))))))))))))))))))))))
->
2(1(2(0(2(0(2(0(2(2(2(2(1(2(1(2(2(2(1(1(2(1(0(1(1(2(2(x1)))))))))))))))))))))))))))
, 1(0(0(1(0(1(1(0(2(1(1(2(1(2(1(2(0(1(2(2(1(2(1(x1)))))))))))))))))))))))
->
1(2(0(0(1(1(2(2(1(2(0(2(2(0(1(1(2(2(2(1(2(2(2(2(2(1(2(x1)))))))))))))))))))))))))))
, 0(1(2(1(1(2(2(2(1(1(0(0(1(0(2(0(2(2(1(0(2(1(1(x1)))))))))))))))))))))))
->
2(1(2(1(2(1(2(2(0(2(0(1(2(1(2(1(2(0(1(2(0(0(2(2(1(1(2(x1)))))))))))))))))))))))))))
, 0(1(1(1(2(2(1(0(0(2(2(2(2(0(2(0(0(0(0(1(0(0(2(x1)))))))))))))))))))))))
->
0(2(1(1(1(1(2(2(1(1(0(1(1(2(1(2(1(0(0(1(2(2(1(0(0(2(2(x1)))))))))))))))))))))))))))
, 0(1(1(1(1(2(1(1(2(2(0(1(0(1(1(0(2(0(0(2(0(1(0(x1)))))))))))))))))))))))
->
2(2(2(2(2(1(0(1(2(2(0(1(1(1(2(2(1(1(0(0(0(0(2(2(1(2(2(x1)))))))))))))))))))))))))))
, 0(1(1(0(1(1(1(2(2(0(2(0(1(2(2(2(0(1(2(0(1(0(2(x1)))))))))))))))))))))))
->
0(2(0(1(0(2(0(2(2(2(1(2(1(1(2(2(2(2(2(2(2(1(0(0(0(2(2(x1)))))))))))))))))))))))))))
, 0(1(0(0(1(2(2(1(0(1(2(1(2(0(1(0(2(2(0(1(2(1(0(x1)))))))))))))))))))))))
->
0(0(0(1(2(2(2(2(2(2(2(0(0(0(0(1(2(1(2(2(2(1(0(2(0(2(0(x1)))))))))))))))))))))))))))
, 0(0(2(0(2(2(1(2(1(1(2(1(1(2(1(0(0(0(0(1(1(2(1(x1)))))))))))))))))))))))
->
0(0(1(2(2(1(1(2(2(1(1(2(2(2(2(0(1(2(1(2(1(1(1(0(1(2(2(x1)))))))))))))))))))))))))))
, 0(0(1(2(0(1(0(0(2(0(1(1(0(1(2(1(1(2(2(1(1(0(2(x1)))))))))))))))))))))))
->
0(2(2(2(0(1(1(2(1(2(2(1(2(1(0(2(2(2(1(2(1(1(0(0(1(0(2(x1)))))))))))))))))))))))))))
, 0(0(1(0(2(2(1(2(0(0(1(2(0(2(2(2(1(1(2(0(0(2(1(x1)))))))))))))))))))))))
->
0(1(1(1(0(2(1(2(1(2(0(1(1(2(1(1(2(2(2(2(2(0(2(2(2(1(2(x1)))))))))))))))))))))))))))
, 0(0(0(2(2(0(2(2(2(1(1(0(2(2(1(2(1(0(2(0(0(0(1(x1)))))))))))))))))))))))
->
2(0(1(1(1(2(2(1(1(2(2(2(2(1(0(1(2(1(1(2(2(2(1(2(1(2(2(x1)))))))))))))))))))))))))))
, 0(0(0(0(1(0(0(2(2(1(0(2(0(2(1(1(2(1(2(2(0(1(1(x1)))))))))))))))))))))))
->
0(1(2(0(0(2(1(2(2(1(1(2(1(1(1(1(2(2(2(1(2(1(0(2(1(1(0(x1)))))))))))))))))))))))))))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool EDA
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ 2(2(2(0(0(1(0(0(2(0(0(2(1(1(2(1(0(1(2(2(2(1(0(x1)))))))))))))))))))))))
->
1(2(2(2(2(0(1(2(1(2(0(1(2(1(2(1(0(1(0(1(0(1(1(2(2(1(0(x1)))))))))))))))))))))))))))
, 2(2(1(2(2(0(0(2(1(1(0(2(2(0(2(2(0(2(2(1(2(0(2(x1)))))))))))))))))))))))
->
1(2(1(1(1(2(2(2(1(2(1(0(2(1(1(1(1(2(2(0(0(1(1(0(2(1(2(x1)))))))))))))))))))))))))))
, 2(2(1(2(1(2(2(2(0(1(2(1(2(2(2(2(1(1(0(1(0(1(0(x1)))))))))))))))))))))))
->
1(2(1(2(1(2(0(1(2(2(0(1(1(1(2(2(1(1(1(2(2(0(1(0(1(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(2(2(1(2(1(1(1(0(0(2(1(1(0(2(0(0(1(1(2(x1)))))))))))))))))))))))
->
2(1(1(1(2(2(2(1(1(0(2(2(1(0(1(0(2(2(1(2(0(0(0(1(2(1(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(2(0(0(2(2(2(2(1(1(1(1(1(2(1(2(0(0(1(1(x1)))))))))))))))))))))))
->
2(2(1(1(2(2(1(2(1(2(2(0(0(0(2(1(0(2(2(1(2(2(0(1(1(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(1(2(0(1(1(2(2(0(1(1(1(1(1(2(2(2(0(2(1(x1)))))))))))))))))))))))
->
1(2(1(2(2(1(1(1(1(2(2(2(1(2(0(0(0(1(2(0(0(1(2(2(2(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(1(0(0(2(1(0(2(1(2(0(0(2(1(0(1(1(2(2(1(x1)))))))))))))))))))))))
->
2(1(2(2(0(1(2(1(1(0(1(2(1(0(0(1(2(2(1(2(1(0(2(1(2(2(1(x1)))))))))))))))))))))))))))
, 2(2(0(1(2(2(2(0(2(2(2(0(2(2(2(2(1(0(1(0(0(1(0(x1)))))))))))))))))))))))
->
2(2(0(1(1(2(2(2(1(1(2(1(0(0(1(2(2(1(2(1(0(2(2(0(0(2(0(x1)))))))))))))))))))))))))))
, 2(2(0(1(1(0(0(1(2(1(0(2(1(2(2(2(1(0(0(2(2(2(0(x1)))))))))))))))))))))))
->
2(2(1(0(0(0(0(2(2(1(1(2(2(1(0(2(1(2(1(2(2(1(2(2(2(0(0(x1)))))))))))))))))))))))))))
, 2(2(0(0(2(1(2(0(1(2(0(2(1(0(1(1(2(2(1(0(1(0(2(x1)))))))))))))))))))))))
->
2(2(2(2(1(2(1(2(0(2(2(2(2(2(0(1(2(0(2(1(0(0(0(2(0(2(2(x1)))))))))))))))))))))))))))
, 2(2(0(0(1(2(1(1(2(1(0(0(0(0(0(2(1(2(1(1(2(0(2(x1)))))))))))))))))))))))
->
2(1(1(2(2(2(2(1(2(1(0(0(2(1(0(2(2(0(1(1(0(2(0(0(0(0(2(x1)))))))))))))))))))))))))))
, 2(2(0(0(1(0(1(2(2(2(1(1(0(0(1(2(2(1(2(0(1(2(1(x1)))))))))))))))))))))))
->
2(2(2(2(0(2(0(2(2(1(2(1(0(1(1(2(2(0(0(2(1(2(1(2(1(2(0(x1)))))))))))))))))))))))))))
, 2(1(2(1(0(2(1(2(0(0(0(0(2(0(0(0(2(2(0(0(0(0(1(x1)))))))))))))))))))))))
->
2(1(2(1(2(0(0(2(1(0(0(2(2(0(1(0(2(1(2(1(2(2(1(2(1(1(2(x1)))))))))))))))))))))))))))
, 2(1(1(0(2(2(2(0(1(2(1(1(0(1(2(0(0(1(1(1(1(2(2(x1)))))))))))))))))))))))
->
2(0(0(2(1(0(0(0(0(0(1(2(1(1(2(1(1(2(1(2(2(0(1(1(1(2(2(x1)))))))))))))))))))))))))))
, 2(1(0(1(1(2(0(0(2(1(0(0(0(1(2(1(1(2(0(2(1(2(1(x1)))))))))))))))))))))))
->
2(0(2(2(0(0(2(2(1(1(1(2(0(1(0(1(2(2(2(2(2(0(0(0(2(2(1(x1)))))))))))))))))))))))))))
, 2(1(0(1(0(0(2(2(2(0(1(0(0(2(0(0(1(2(0(2(2(2(0(x1)))))))))))))))))))))))
->
2(1(1(2(0(1(2(0(0(2(0(1(2(2(1(1(1(2(2(2(0(0(1(1(0(2(0(x1)))))))))))))))))))))))))))
, 2(0(2(0(1(2(2(0(0(2(2(2(1(1(1(2(1(0(2(0(2(2(0(x1)))))))))))))))))))))))
->
2(1(1(1(2(2(0(0(0(2(1(0(0(0(1(1(0(2(2(0(2(2(2(2(2(2(0(x1)))))))))))))))))))))))))))
, 2(0(2(0(1(0(1(1(2(0(1(1(2(2(1(0(2(0(2(0(2(2(2(x1)))))))))))))))))))))))
->
2(0(0(1(1(2(0(2(2(1(1(2(2(0(1(2(2(2(0(0(2(0(2(2(2(0(2(x1)))))))))))))))))))))))))))
, 2(0(1(0(0(0(1(0(0(0(0(0(0(0(1(0(2(0(0(2(2(2(2(x1)))))))))))))))))))))))
->
2(2(2(1(1(2(1(2(0(1(1(2(1(0(2(1(0(0(1(0(1(1(2(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(2(2(2(1(1(0(0(2(2(2(0(0(0(2(1(2(2(0(2(0(2(0(x1)))))))))))))))))))))))
->
1(2(1(2(0(0(1(1(1(2(2(2(2(1(2(2(2(0(2(0(1(2(2(2(2(0(0(x1)))))))))))))))))))))))))))
, 1(2(0(2(1(2(2(1(2(2(2(0(1(1(1(1(0(1(0(0(2(0(1(x1)))))))))))))))))))))))
->
1(2(1(2(1(2(2(2(2(2(2(0(0(2(0(0(2(2(0(1(1(1(1(0(0(2(1(x1)))))))))))))))))))))))))))
, 1(2(0(0(2(0(1(2(2(0(2(1(2(1(2(0(1(0(1(2(0(2(1(x1)))))))))))))))))))))))
->
1(2(2(0(2(1(2(2(0(1(0(2(1(0(1(2(1(2(2(2(2(0(2(2(0(2(0(x1)))))))))))))))))))))))))))
, 1(1(2(2(1(0(2(0(1(1(2(2(2(1(0(1(0(0(2(1(1(0(2(x1)))))))))))))))))))))))
->
2(2(2(1(1(2(2(2(1(2(2(0(0(2(0(0(1(2(0(2(2(1(2(2(2(0(2(x1)))))))))))))))))))))))))))
, 1(1(1(0(2(2(1(1(1(2(2(0(2(0(2(1(1(2(1(2(1(2(2(x1)))))))))))))))))))))))
->
1(2(1(2(1(1(1(1(2(1(1(1(2(2(0(1(0(2(2(1(2(2(2(1(0(1(2(x1)))))))))))))))))))))))))))
, 1(1(0(2(1(2(2(2(2(1(0(1(2(0(1(2(1(1(0(2(1(2(0(x1)))))))))))))))))))))))
->
2(2(1(2(1(2(2(1(0(1(2(2(2(1(0(2(1(1(2(1(0(1(1(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(2(1(0(2(0(1(2(0(2(0(0(2(1(0(1(0(1(2(1(2(x1)))))))))))))))))))))))
->
2(0(2(2(1(1(1(2(2(0(1(2(0(2(1(1(2(1(0(0(2(0(1(2(2(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(1(2(2(2(2(1(0(2(1(2(0(0(0(1(0(2(1(1(1(2(x1)))))))))))))))))))))))
->
2(1(2(1(2(2(2(2(2(0(0(0(0(2(1(2(2(2(2(1(2(2(2(0(0(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(0(1(1(1(2(2(2(1(2(1(0(0(0(2(2(2(0(1(2(0(x1)))))))))))))))))))))))
->
2(1(2(1(2(2(2(1(2(2(0(2(2(1(0(2(1(2(2(0(1(0(1(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(0(1(0(2(2(2(2(1(0(0(2(0(2(1(2(1(2(1(1(2(0(2(x1)))))))))))))))))))))))
->
2(1(2(0(2(0(2(0(2(2(2(2(1(2(1(2(2(2(1(1(2(1(0(1(1(2(2(x1)))))))))))))))))))))))))))
, 1(0(0(1(0(1(1(0(2(1(1(2(1(2(1(2(0(1(2(2(1(2(1(x1)))))))))))))))))))))))
->
1(2(0(0(1(1(2(2(1(2(0(2(2(0(1(1(2(2(2(1(2(2(2(2(2(1(2(x1)))))))))))))))))))))))))))
, 0(1(2(1(1(2(2(2(1(1(0(0(1(0(2(0(2(2(1(0(2(1(1(x1)))))))))))))))))))))))
->
2(1(2(1(2(1(2(2(0(2(0(1(2(1(2(1(2(0(1(2(0(0(2(2(1(1(2(x1)))))))))))))))))))))))))))
, 0(1(1(1(2(2(1(0(0(2(2(2(2(0(2(0(0(0(0(1(0(0(2(x1)))))))))))))))))))))))
->
0(2(1(1(1(1(2(2(1(1(0(1(1(2(1(2(1(0(0(1(2(2(1(0(0(2(2(x1)))))))))))))))))))))))))))
, 0(1(1(1(1(2(1(1(2(2(0(1(0(1(1(0(2(0(0(2(0(1(0(x1)))))))))))))))))))))))
->
2(2(2(2(2(1(0(1(2(2(0(1(1(1(2(2(1(1(0(0(0(0(2(2(1(2(2(x1)))))))))))))))))))))))))))
, 0(1(1(0(1(1(1(2(2(0(2(0(1(2(2(2(0(1(2(0(1(0(2(x1)))))))))))))))))))))))
->
0(2(0(1(0(2(0(2(2(2(1(2(1(1(2(2(2(2(2(2(2(1(0(0(0(2(2(x1)))))))))))))))))))))))))))
, 0(1(0(0(1(2(2(1(0(1(2(1(2(0(1(0(2(2(0(1(2(1(0(x1)))))))))))))))))))))))
->
0(0(0(1(2(2(2(2(2(2(2(0(0(0(0(1(2(1(2(2(2(1(0(2(0(2(0(x1)))))))))))))))))))))))))))
, 0(0(2(0(2(2(1(2(1(1(2(1(1(2(1(0(0(0(0(1(1(2(1(x1)))))))))))))))))))))))
->
0(0(1(2(2(1(1(2(2(1(1(2(2(2(2(0(1(2(1(2(1(1(1(0(1(2(2(x1)))))))))))))))))))))))))))
, 0(0(1(2(0(1(0(0(2(0(1(1(0(1(2(1(1(2(2(1(1(0(2(x1)))))))))))))))))))))))
->
0(2(2(2(0(1(1(2(1(2(2(1(2(1(0(2(2(2(1(2(1(1(0(0(1(0(2(x1)))))))))))))))))))))))))))
, 0(0(1(0(2(2(1(2(0(0(1(2(0(2(2(2(1(1(2(0(0(2(1(x1)))))))))))))))))))))))
->
0(1(1(1(0(2(1(2(1(2(0(1(1(2(1(1(2(2(2(2(2(0(2(2(2(1(2(x1)))))))))))))))))))))))))))
, 0(0(0(2(2(0(2(2(2(1(1(0(2(2(1(2(1(0(2(0(0(0(1(x1)))))))))))))))))))))))
->
2(0(1(1(1(2(2(1(1(2(2(2(2(1(0(1(2(1(1(2(2(2(1(2(1(2(2(x1)))))))))))))))))))))))))))
, 0(0(0(0(1(0(0(2(2(1(0(2(0(2(1(1(2(1(2(2(0(1(1(x1)))))))))))))))))))))))
->
0(1(2(0(0(2(1(2(2(1(1(2(1(1(1(1(2(2(2(1(2(1(0(2(1(1(0(x1)))))))))))))))))))))))))))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool IDA
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ 2(2(2(0(0(1(0(0(2(0(0(2(1(1(2(1(0(1(2(2(2(1(0(x1)))))))))))))))))))))))
->
1(2(2(2(2(0(1(2(1(2(0(1(2(1(2(1(0(1(0(1(0(1(1(2(2(1(0(x1)))))))))))))))))))))))))))
, 2(2(1(2(2(0(0(2(1(1(0(2(2(0(2(2(0(2(2(1(2(0(2(x1)))))))))))))))))))))))
->
1(2(1(1(1(2(2(2(1(2(1(0(2(1(1(1(1(2(2(0(0(1(1(0(2(1(2(x1)))))))))))))))))))))))))))
, 2(2(1(2(1(2(2(2(0(1(2(1(2(2(2(2(1(1(0(1(0(1(0(x1)))))))))))))))))))))))
->
1(2(1(2(1(2(0(1(2(2(0(1(1(1(2(2(1(1(1(2(2(0(1(0(1(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(2(2(1(2(1(1(1(0(0(2(1(1(0(2(0(0(1(1(2(x1)))))))))))))))))))))))
->
2(1(1(1(2(2(2(1(1(0(2(2(1(0(1(0(2(2(1(2(0(0(0(1(2(1(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(2(0(0(2(2(2(2(1(1(1(1(1(2(1(2(0(0(1(1(x1)))))))))))))))))))))))
->
2(2(1(1(2(2(1(2(1(2(2(0(0(0(2(1(0(2(2(1(2(2(0(1(1(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(1(2(0(1(1(2(2(0(1(1(1(1(1(2(2(2(0(2(1(x1)))))))))))))))))))))))
->
1(2(1(2(2(1(1(1(1(2(2(2(1(2(0(0(0(1(2(0(0(1(2(2(2(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(1(0(0(2(1(0(2(1(2(0(0(2(1(0(1(1(2(2(1(x1)))))))))))))))))))))))
->
2(1(2(2(0(1(2(1(1(0(1(2(1(0(0(1(2(2(1(2(1(0(2(1(2(2(1(x1)))))))))))))))))))))))))))
, 2(2(0(1(2(2(2(0(2(2(2(0(2(2(2(2(1(0(1(0(0(1(0(x1)))))))))))))))))))))))
->
2(2(0(1(1(2(2(2(1(1(2(1(0(0(1(2(2(1(2(1(0(2(2(0(0(2(0(x1)))))))))))))))))))))))))))
, 2(2(0(1(1(0(0(1(2(1(0(2(1(2(2(2(1(0(0(2(2(2(0(x1)))))))))))))))))))))))
->
2(2(1(0(0(0(0(2(2(1(1(2(2(1(0(2(1(2(1(2(2(1(2(2(2(0(0(x1)))))))))))))))))))))))))))
, 2(2(0(0(2(1(2(0(1(2(0(2(1(0(1(1(2(2(1(0(1(0(2(x1)))))))))))))))))))))))
->
2(2(2(2(1(2(1(2(0(2(2(2(2(2(0(1(2(0(2(1(0(0(0(2(0(2(2(x1)))))))))))))))))))))))))))
, 2(2(0(0(1(2(1(1(2(1(0(0(0(0(0(2(1(2(1(1(2(0(2(x1)))))))))))))))))))))))
->
2(1(1(2(2(2(2(1(2(1(0(0(2(1(0(2(2(0(1(1(0(2(0(0(0(0(2(x1)))))))))))))))))))))))))))
, 2(2(0(0(1(0(1(2(2(2(1(1(0(0(1(2(2(1(2(0(1(2(1(x1)))))))))))))))))))))))
->
2(2(2(2(0(2(0(2(2(1(2(1(0(1(1(2(2(0(0(2(1(2(1(2(1(2(0(x1)))))))))))))))))))))))))))
, 2(1(2(1(0(2(1(2(0(0(0(0(2(0(0(0(2(2(0(0(0(0(1(x1)))))))))))))))))))))))
->
2(1(2(1(2(0(0(2(1(0(0(2(2(0(1(0(2(1(2(1(2(2(1(2(1(1(2(x1)))))))))))))))))))))))))))
, 2(1(1(0(2(2(2(0(1(2(1(1(0(1(2(0(0(1(1(1(1(2(2(x1)))))))))))))))))))))))
->
2(0(0(2(1(0(0(0(0(0(1(2(1(1(2(1(1(2(1(2(2(0(1(1(1(2(2(x1)))))))))))))))))))))))))))
, 2(1(0(1(1(2(0(0(2(1(0(0(0(1(2(1(1(2(0(2(1(2(1(x1)))))))))))))))))))))))
->
2(0(2(2(0(0(2(2(1(1(1(2(0(1(0(1(2(2(2(2(2(0(0(0(2(2(1(x1)))))))))))))))))))))))))))
, 2(1(0(1(0(0(2(2(2(0(1(0(0(2(0(0(1(2(0(2(2(2(0(x1)))))))))))))))))))))))
->
2(1(1(2(0(1(2(0(0(2(0(1(2(2(1(1(1(2(2(2(0(0(1(1(0(2(0(x1)))))))))))))))))))))))))))
, 2(0(2(0(1(2(2(0(0(2(2(2(1(1(1(2(1(0(2(0(2(2(0(x1)))))))))))))))))))))))
->
2(1(1(1(2(2(0(0(0(2(1(0(0(0(1(1(0(2(2(0(2(2(2(2(2(2(0(x1)))))))))))))))))))))))))))
, 2(0(2(0(1(0(1(1(2(0(1(1(2(2(1(0(2(0(2(0(2(2(2(x1)))))))))))))))))))))))
->
2(0(0(1(1(2(0(2(2(1(1(2(2(0(1(2(2(2(0(0(2(0(2(2(2(0(2(x1)))))))))))))))))))))))))))
, 2(0(1(0(0(0(1(0(0(0(0(0(0(0(1(0(2(0(0(2(2(2(2(x1)))))))))))))))))))))))
->
2(2(2(1(1(2(1(2(0(1(1(2(1(0(2(1(0(0(1(0(1(1(2(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(2(2(2(1(1(0(0(2(2(2(0(0(0(2(1(2(2(0(2(0(2(0(x1)))))))))))))))))))))))
->
1(2(1(2(0(0(1(1(1(2(2(2(2(1(2(2(2(0(2(0(1(2(2(2(2(0(0(x1)))))))))))))))))))))))))))
, 1(2(0(2(1(2(2(1(2(2(2(0(1(1(1(1(0(1(0(0(2(0(1(x1)))))))))))))))))))))))
->
1(2(1(2(1(2(2(2(2(2(2(0(0(2(0(0(2(2(0(1(1(1(1(0(0(2(1(x1)))))))))))))))))))))))))))
, 1(2(0(0(2(0(1(2(2(0(2(1(2(1(2(0(1(0(1(2(0(2(1(x1)))))))))))))))))))))))
->
1(2(2(0(2(1(2(2(0(1(0(2(1(0(1(2(1(2(2(2(2(0(2(2(0(2(0(x1)))))))))))))))))))))))))))
, 1(1(2(2(1(0(2(0(1(1(2(2(2(1(0(1(0(0(2(1(1(0(2(x1)))))))))))))))))))))))
->
2(2(2(1(1(2(2(2(1(2(2(0(0(2(0(0(1(2(0(2(2(1(2(2(2(0(2(x1)))))))))))))))))))))))))))
, 1(1(1(0(2(2(1(1(1(2(2(0(2(0(2(1(1(2(1(2(1(2(2(x1)))))))))))))))))))))))
->
1(2(1(2(1(1(1(1(2(1(1(1(2(2(0(1(0(2(2(1(2(2(2(1(0(1(2(x1)))))))))))))))))))))))))))
, 1(1(0(2(1(2(2(2(2(1(0(1(2(0(1(2(1(1(0(2(1(2(0(x1)))))))))))))))))))))))
->
2(2(1(2(1(2(2(1(0(1(2(2(2(1(0(2(1(1(2(1(0(1(1(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(2(1(0(2(0(1(2(0(2(0(0(2(1(0(1(0(1(2(1(2(x1)))))))))))))))))))))))
->
2(0(2(2(1(1(1(2(2(0(1(2(0(2(1(1(2(1(0(0(2(0(1(2(2(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(1(2(2(2(2(1(0(2(1(2(0(0(0(1(0(2(1(1(1(2(x1)))))))))))))))))))))))
->
2(1(2(1(2(2(2(2(2(0(0(0(0(2(1(2(2(2(2(1(2(2(2(0(0(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(0(1(1(1(2(2(2(1(2(1(0(0(0(2(2(2(0(1(2(0(x1)))))))))))))))))))))))
->
2(1(2(1(2(2(2(1(2(2(0(2(2(1(0(2(1(2(2(0(1(0(1(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(0(1(0(2(2(2(2(1(0(0(2(0(2(1(2(1(2(1(1(2(0(2(x1)))))))))))))))))))))))
->
2(1(2(0(2(0(2(0(2(2(2(2(1(2(1(2(2(2(1(1(2(1(0(1(1(2(2(x1)))))))))))))))))))))))))))
, 1(0(0(1(0(1(1(0(2(1(1(2(1(2(1(2(0(1(2(2(1(2(1(x1)))))))))))))))))))))))
->
1(2(0(0(1(1(2(2(1(2(0(2(2(0(1(1(2(2(2(1(2(2(2(2(2(1(2(x1)))))))))))))))))))))))))))
, 0(1(2(1(1(2(2(2(1(1(0(0(1(0(2(0(2(2(1(0(2(1(1(x1)))))))))))))))))))))))
->
2(1(2(1(2(1(2(2(0(2(0(1(2(1(2(1(2(0(1(2(0(0(2(2(1(1(2(x1)))))))))))))))))))))))))))
, 0(1(1(1(2(2(1(0(0(2(2(2(2(0(2(0(0(0(0(1(0(0(2(x1)))))))))))))))))))))))
->
0(2(1(1(1(1(2(2(1(1(0(1(1(2(1(2(1(0(0(1(2(2(1(0(0(2(2(x1)))))))))))))))))))))))))))
, 0(1(1(1(1(2(1(1(2(2(0(1(0(1(1(0(2(0(0(2(0(1(0(x1)))))))))))))))))))))))
->
2(2(2(2(2(1(0(1(2(2(0(1(1(1(2(2(1(1(0(0(0(0(2(2(1(2(2(x1)))))))))))))))))))))))))))
, 0(1(1(0(1(1(1(2(2(0(2(0(1(2(2(2(0(1(2(0(1(0(2(x1)))))))))))))))))))))))
->
0(2(0(1(0(2(0(2(2(2(1(2(1(1(2(2(2(2(2(2(2(1(0(0(0(2(2(x1)))))))))))))))))))))))))))
, 0(1(0(0(1(2(2(1(0(1(2(1(2(0(1(0(2(2(0(1(2(1(0(x1)))))))))))))))))))))))
->
0(0(0(1(2(2(2(2(2(2(2(0(0(0(0(1(2(1(2(2(2(1(0(2(0(2(0(x1)))))))))))))))))))))))))))
, 0(0(2(0(2(2(1(2(1(1(2(1(1(2(1(0(0(0(0(1(1(2(1(x1)))))))))))))))))))))))
->
0(0(1(2(2(1(1(2(2(1(1(2(2(2(2(0(1(2(1(2(1(1(1(0(1(2(2(x1)))))))))))))))))))))))))))
, 0(0(1(2(0(1(0(0(2(0(1(1(0(1(2(1(1(2(2(1(1(0(2(x1)))))))))))))))))))))))
->
0(2(2(2(0(1(1(2(1(2(2(1(2(1(0(2(2(2(1(2(1(1(0(0(1(0(2(x1)))))))))))))))))))))))))))
, 0(0(1(0(2(2(1(2(0(0(1(2(0(2(2(2(1(1(2(0(0(2(1(x1)))))))))))))))))))))))
->
0(1(1(1(0(2(1(2(1(2(0(1(1(2(1(1(2(2(2(2(2(0(2(2(2(1(2(x1)))))))))))))))))))))))))))
, 0(0(0(2(2(0(2(2(2(1(1(0(2(2(1(2(1(0(2(0(0(0(1(x1)))))))))))))))))))))))
->
2(0(1(1(1(2(2(1(1(2(2(2(2(1(0(1(2(1(1(2(2(2(1(2(1(2(2(x1)))))))))))))))))))))))))))
, 0(0(0(0(1(0(0(2(2(1(0(2(0(2(1(1(2(1(2(2(0(1(1(x1)))))))))))))))))))))))
->
0(1(2(0(0(2(1(2(2(1(1(2(1(1(1(1(2(2(2(1(2(1(0(2(1(1(0(x1)))))))))))))))))))))))))))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool TRI
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ 2(2(2(0(0(1(0(0(2(0(0(2(1(1(2(1(0(1(2(2(2(1(0(x1)))))))))))))))))))))))
->
1(2(2(2(2(0(1(2(1(2(0(1(2(1(2(1(0(1(0(1(0(1(1(2(2(1(0(x1)))))))))))))))))))))))))))
, 2(2(1(2(2(0(0(2(1(1(0(2(2(0(2(2(0(2(2(1(2(0(2(x1)))))))))))))))))))))))
->
1(2(1(1(1(2(2(2(1(2(1(0(2(1(1(1(1(2(2(0(0(1(1(0(2(1(2(x1)))))))))))))))))))))))))))
, 2(2(1(2(1(2(2(2(0(1(2(1(2(2(2(2(1(1(0(1(0(1(0(x1)))))))))))))))))))))))
->
1(2(1(2(1(2(0(1(2(2(0(1(1(1(2(2(1(1(1(2(2(0(1(0(1(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(2(2(1(2(1(1(1(0(0(2(1(1(0(2(0(0(1(1(2(x1)))))))))))))))))))))))
->
2(1(1(1(2(2(2(1(1(0(2(2(1(0(1(0(2(2(1(2(0(0(0(1(2(1(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(2(0(0(2(2(2(2(1(1(1(1(1(2(1(2(0(0(1(1(x1)))))))))))))))))))))))
->
2(2(1(1(2(2(1(2(1(2(2(0(0(0(2(1(0(2(2(1(2(2(0(1(1(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(1(2(0(1(1(2(2(0(1(1(1(1(1(2(2(2(0(2(1(x1)))))))))))))))))))))))
->
1(2(1(2(2(1(1(1(1(2(2(2(1(2(0(0(0(1(2(0(0(1(2(2(2(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(1(0(0(2(1(0(2(1(2(0(0(2(1(0(1(1(2(2(1(x1)))))))))))))))))))))))
->
2(1(2(2(0(1(2(1(1(0(1(2(1(0(0(1(2(2(1(2(1(0(2(1(2(2(1(x1)))))))))))))))))))))))))))
, 2(2(0(1(2(2(2(0(2(2(2(0(2(2(2(2(1(0(1(0(0(1(0(x1)))))))))))))))))))))))
->
2(2(0(1(1(2(2(2(1(1(2(1(0(0(1(2(2(1(2(1(0(2(2(0(0(2(0(x1)))))))))))))))))))))))))))
, 2(2(0(1(1(0(0(1(2(1(0(2(1(2(2(2(1(0(0(2(2(2(0(x1)))))))))))))))))))))))
->
2(2(1(0(0(0(0(2(2(1(1(2(2(1(0(2(1(2(1(2(2(1(2(2(2(0(0(x1)))))))))))))))))))))))))))
, 2(2(0(0(2(1(2(0(1(2(0(2(1(0(1(1(2(2(1(0(1(0(2(x1)))))))))))))))))))))))
->
2(2(2(2(1(2(1(2(0(2(2(2(2(2(0(1(2(0(2(1(0(0(0(2(0(2(2(x1)))))))))))))))))))))))))))
, 2(2(0(0(1(2(1(1(2(1(0(0(0(0(0(2(1(2(1(1(2(0(2(x1)))))))))))))))))))))))
->
2(1(1(2(2(2(2(1(2(1(0(0(2(1(0(2(2(0(1(1(0(2(0(0(0(0(2(x1)))))))))))))))))))))))))))
, 2(2(0(0(1(0(1(2(2(2(1(1(0(0(1(2(2(1(2(0(1(2(1(x1)))))))))))))))))))))))
->
2(2(2(2(0(2(0(2(2(1(2(1(0(1(1(2(2(0(0(2(1(2(1(2(1(2(0(x1)))))))))))))))))))))))))))
, 2(1(2(1(0(2(1(2(0(0(0(0(2(0(0(0(2(2(0(0(0(0(1(x1)))))))))))))))))))))))
->
2(1(2(1(2(0(0(2(1(0(0(2(2(0(1(0(2(1(2(1(2(2(1(2(1(1(2(x1)))))))))))))))))))))))))))
, 2(1(1(0(2(2(2(0(1(2(1(1(0(1(2(0(0(1(1(1(1(2(2(x1)))))))))))))))))))))))
->
2(0(0(2(1(0(0(0(0(0(1(2(1(1(2(1(1(2(1(2(2(0(1(1(1(2(2(x1)))))))))))))))))))))))))))
, 2(1(0(1(1(2(0(0(2(1(0(0(0(1(2(1(1(2(0(2(1(2(1(x1)))))))))))))))))))))))
->
2(0(2(2(0(0(2(2(1(1(1(2(0(1(0(1(2(2(2(2(2(0(0(0(2(2(1(x1)))))))))))))))))))))))))))
, 2(1(0(1(0(0(2(2(2(0(1(0(0(2(0(0(1(2(0(2(2(2(0(x1)))))))))))))))))))))))
->
2(1(1(2(0(1(2(0(0(2(0(1(2(2(1(1(1(2(2(2(0(0(1(1(0(2(0(x1)))))))))))))))))))))))))))
, 2(0(2(0(1(2(2(0(0(2(2(2(1(1(1(2(1(0(2(0(2(2(0(x1)))))))))))))))))))))))
->
2(1(1(1(2(2(0(0(0(2(1(0(0(0(1(1(0(2(2(0(2(2(2(2(2(2(0(x1)))))))))))))))))))))))))))
, 2(0(2(0(1(0(1(1(2(0(1(1(2(2(1(0(2(0(2(0(2(2(2(x1)))))))))))))))))))))))
->
2(0(0(1(1(2(0(2(2(1(1(2(2(0(1(2(2(2(0(0(2(0(2(2(2(0(2(x1)))))))))))))))))))))))))))
, 2(0(1(0(0(0(1(0(0(0(0(0(0(0(1(0(2(0(0(2(2(2(2(x1)))))))))))))))))))))))
->
2(2(2(1(1(2(1(2(0(1(1(2(1(0(2(1(0(0(1(0(1(1(2(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(2(2(2(1(1(0(0(2(2(2(0(0(0(2(1(2(2(0(2(0(2(0(x1)))))))))))))))))))))))
->
1(2(1(2(0(0(1(1(1(2(2(2(2(1(2(2(2(0(2(0(1(2(2(2(2(0(0(x1)))))))))))))))))))))))))))
, 1(2(0(2(1(2(2(1(2(2(2(0(1(1(1(1(0(1(0(0(2(0(1(x1)))))))))))))))))))))))
->
1(2(1(2(1(2(2(2(2(2(2(0(0(2(0(0(2(2(0(1(1(1(1(0(0(2(1(x1)))))))))))))))))))))))))))
, 1(2(0(0(2(0(1(2(2(0(2(1(2(1(2(0(1(0(1(2(0(2(1(x1)))))))))))))))))))))))
->
1(2(2(0(2(1(2(2(0(1(0(2(1(0(1(2(1(2(2(2(2(0(2(2(0(2(0(x1)))))))))))))))))))))))))))
, 1(1(2(2(1(0(2(0(1(1(2(2(2(1(0(1(0(0(2(1(1(0(2(x1)))))))))))))))))))))))
->
2(2(2(1(1(2(2(2(1(2(2(0(0(2(0(0(1(2(0(2(2(1(2(2(2(0(2(x1)))))))))))))))))))))))))))
, 1(1(1(0(2(2(1(1(1(2(2(0(2(0(2(1(1(2(1(2(1(2(2(x1)))))))))))))))))))))))
->
1(2(1(2(1(1(1(1(2(1(1(1(2(2(0(1(0(2(2(1(2(2(2(1(0(1(2(x1)))))))))))))))))))))))))))
, 1(1(0(2(1(2(2(2(2(1(0(1(2(0(1(2(1(1(0(2(1(2(0(x1)))))))))))))))))))))))
->
2(2(1(2(1(2(2(1(0(1(2(2(2(1(0(2(1(1(2(1(0(1(1(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(2(1(0(2(0(1(2(0(2(0(0(2(1(0(1(0(1(2(1(2(x1)))))))))))))))))))))))
->
2(0(2(2(1(1(1(2(2(0(1(2(0(2(1(1(2(1(0(0(2(0(1(2(2(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(1(2(2(2(2(1(0(2(1(2(0(0(0(1(0(2(1(1(1(2(x1)))))))))))))))))))))))
->
2(1(2(1(2(2(2(2(2(0(0(0(0(2(1(2(2(2(2(1(2(2(2(0(0(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(0(1(1(1(2(2(2(1(2(1(0(0(0(2(2(2(0(1(2(0(x1)))))))))))))))))))))))
->
2(1(2(1(2(2(2(1(2(2(0(2(2(1(0(2(1(2(2(0(1(0(1(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(0(1(0(2(2(2(2(1(0(0(2(0(2(1(2(1(2(1(1(2(0(2(x1)))))))))))))))))))))))
->
2(1(2(0(2(0(2(0(2(2(2(2(1(2(1(2(2(2(1(1(2(1(0(1(1(2(2(x1)))))))))))))))))))))))))))
, 1(0(0(1(0(1(1(0(2(1(1(2(1(2(1(2(0(1(2(2(1(2(1(x1)))))))))))))))))))))))
->
1(2(0(0(1(1(2(2(1(2(0(2(2(0(1(1(2(2(2(1(2(2(2(2(2(1(2(x1)))))))))))))))))))))))))))
, 0(1(2(1(1(2(2(2(1(1(0(0(1(0(2(0(2(2(1(0(2(1(1(x1)))))))))))))))))))))))
->
2(1(2(1(2(1(2(2(0(2(0(1(2(1(2(1(2(0(1(2(0(0(2(2(1(1(2(x1)))))))))))))))))))))))))))
, 0(1(1(1(2(2(1(0(0(2(2(2(2(0(2(0(0(0(0(1(0(0(2(x1)))))))))))))))))))))))
->
0(2(1(1(1(1(2(2(1(1(0(1(1(2(1(2(1(0(0(1(2(2(1(0(0(2(2(x1)))))))))))))))))))))))))))
, 0(1(1(1(1(2(1(1(2(2(0(1(0(1(1(0(2(0(0(2(0(1(0(x1)))))))))))))))))))))))
->
2(2(2(2(2(1(0(1(2(2(0(1(1(1(2(2(1(1(0(0(0(0(2(2(1(2(2(x1)))))))))))))))))))))))))))
, 0(1(1(0(1(1(1(2(2(0(2(0(1(2(2(2(0(1(2(0(1(0(2(x1)))))))))))))))))))))))
->
0(2(0(1(0(2(0(2(2(2(1(2(1(1(2(2(2(2(2(2(2(1(0(0(0(2(2(x1)))))))))))))))))))))))))))
, 0(1(0(0(1(2(2(1(0(1(2(1(2(0(1(0(2(2(0(1(2(1(0(x1)))))))))))))))))))))))
->
0(0(0(1(2(2(2(2(2(2(2(0(0(0(0(1(2(1(2(2(2(1(0(2(0(2(0(x1)))))))))))))))))))))))))))
, 0(0(2(0(2(2(1(2(1(1(2(1(1(2(1(0(0(0(0(1(1(2(1(x1)))))))))))))))))))))))
->
0(0(1(2(2(1(1(2(2(1(1(2(2(2(2(0(1(2(1(2(1(1(1(0(1(2(2(x1)))))))))))))))))))))))))))
, 0(0(1(2(0(1(0(0(2(0(1(1(0(1(2(1(1(2(2(1(1(0(2(x1)))))))))))))))))))))))
->
0(2(2(2(0(1(1(2(1(2(2(1(2(1(0(2(2(2(1(2(1(1(0(0(1(0(2(x1)))))))))))))))))))))))))))
, 0(0(1(0(2(2(1(2(0(0(1(2(0(2(2(2(1(1(2(0(0(2(1(x1)))))))))))))))))))))))
->
0(1(1(1(0(2(1(2(1(2(0(1(1(2(1(1(2(2(2(2(2(0(2(2(2(1(2(x1)))))))))))))))))))))))))))
, 0(0(0(2(2(0(2(2(2(1(1(0(2(2(1(2(1(0(2(0(0(0(1(x1)))))))))))))))))))))))
->
2(0(1(1(1(2(2(1(1(2(2(2(2(1(0(1(2(1(1(2(2(2(1(2(1(2(2(x1)))))))))))))))))))))))))))
, 0(0(0(0(1(0(0(2(2(1(0(2(0(2(1(1(2(1(2(2(0(1(1(x1)))))))))))))))))))))))
->
0(1(2(0(0(2(1(2(2(1(1(2(1(1(1(1(2(2(2(1(2(1(0(2(1(1(0(x1)))))))))))))))))))))))))))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool TRI2
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ 2(2(2(0(0(1(0(0(2(0(0(2(1(1(2(1(0(1(2(2(2(1(0(x1)))))))))))))))))))))))
->
1(2(2(2(2(0(1(2(1(2(0(1(2(1(2(1(0(1(0(1(0(1(1(2(2(1(0(x1)))))))))))))))))))))))))))
, 2(2(1(2(2(0(0(2(1(1(0(2(2(0(2(2(0(2(2(1(2(0(2(x1)))))))))))))))))))))))
->
1(2(1(1(1(2(2(2(1(2(1(0(2(1(1(1(1(2(2(0(0(1(1(0(2(1(2(x1)))))))))))))))))))))))))))
, 2(2(1(2(1(2(2(2(0(1(2(1(2(2(2(2(1(1(0(1(0(1(0(x1)))))))))))))))))))))))
->
1(2(1(2(1(2(0(1(2(2(0(1(1(1(2(2(1(1(1(2(2(0(1(0(1(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(2(2(1(2(1(1(1(0(0(2(1(1(0(2(0(0(1(1(2(x1)))))))))))))))))))))))
->
2(1(1(1(2(2(2(1(1(0(2(2(1(0(1(0(2(2(1(2(0(0(0(1(2(1(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(2(0(0(2(2(2(2(1(1(1(1(1(2(1(2(0(0(1(1(x1)))))))))))))))))))))))
->
2(2(1(1(2(2(1(2(1(2(2(0(0(0(2(1(0(2(2(1(2(2(0(1(1(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(1(2(0(1(1(2(2(0(1(1(1(1(1(2(2(2(0(2(1(x1)))))))))))))))))))))))
->
1(2(1(2(2(1(1(1(1(2(2(2(1(2(0(0(0(1(2(0(0(1(2(2(2(2(2(x1)))))))))))))))))))))))))))
, 2(2(1(1(1(0(0(2(1(0(2(1(2(0(0(2(1(0(1(1(2(2(1(x1)))))))))))))))))))))))
->
2(1(2(2(0(1(2(1(1(0(1(2(1(0(0(1(2(2(1(2(1(0(2(1(2(2(1(x1)))))))))))))))))))))))))))
, 2(2(0(1(2(2(2(0(2(2(2(0(2(2(2(2(1(0(1(0(0(1(0(x1)))))))))))))))))))))))
->
2(2(0(1(1(2(2(2(1(1(2(1(0(0(1(2(2(1(2(1(0(2(2(0(0(2(0(x1)))))))))))))))))))))))))))
, 2(2(0(1(1(0(0(1(2(1(0(2(1(2(2(2(1(0(0(2(2(2(0(x1)))))))))))))))))))))))
->
2(2(1(0(0(0(0(2(2(1(1(2(2(1(0(2(1(2(1(2(2(1(2(2(2(0(0(x1)))))))))))))))))))))))))))
, 2(2(0(0(2(1(2(0(1(2(0(2(1(0(1(1(2(2(1(0(1(0(2(x1)))))))))))))))))))))))
->
2(2(2(2(1(2(1(2(0(2(2(2(2(2(0(1(2(0(2(1(0(0(0(2(0(2(2(x1)))))))))))))))))))))))))))
, 2(2(0(0(1(2(1(1(2(1(0(0(0(0(0(2(1(2(1(1(2(0(2(x1)))))))))))))))))))))))
->
2(1(1(2(2(2(2(1(2(1(0(0(2(1(0(2(2(0(1(1(0(2(0(0(0(0(2(x1)))))))))))))))))))))))))))
, 2(2(0(0(1(0(1(2(2(2(1(1(0(0(1(2(2(1(2(0(1(2(1(x1)))))))))))))))))))))))
->
2(2(2(2(0(2(0(2(2(1(2(1(0(1(1(2(2(0(0(2(1(2(1(2(1(2(0(x1)))))))))))))))))))))))))))
, 2(1(2(1(0(2(1(2(0(0(0(0(2(0(0(0(2(2(0(0(0(0(1(x1)))))))))))))))))))))))
->
2(1(2(1(2(0(0(2(1(0(0(2(2(0(1(0(2(1(2(1(2(2(1(2(1(1(2(x1)))))))))))))))))))))))))))
, 2(1(1(0(2(2(2(0(1(2(1(1(0(1(2(0(0(1(1(1(1(2(2(x1)))))))))))))))))))))))
->
2(0(0(2(1(0(0(0(0(0(1(2(1(1(2(1(1(2(1(2(2(0(1(1(1(2(2(x1)))))))))))))))))))))))))))
, 2(1(0(1(1(2(0(0(2(1(0(0(0(1(2(1(1(2(0(2(1(2(1(x1)))))))))))))))))))))))
->
2(0(2(2(0(0(2(2(1(1(1(2(0(1(0(1(2(2(2(2(2(0(0(0(2(2(1(x1)))))))))))))))))))))))))))
, 2(1(0(1(0(0(2(2(2(0(1(0(0(2(0(0(1(2(0(2(2(2(0(x1)))))))))))))))))))))))
->
2(1(1(2(0(1(2(0(0(2(0(1(2(2(1(1(1(2(2(2(0(0(1(1(0(2(0(x1)))))))))))))))))))))))))))
, 2(0(2(0(1(2(2(0(0(2(2(2(1(1(1(2(1(0(2(0(2(2(0(x1)))))))))))))))))))))))
->
2(1(1(1(2(2(0(0(0(2(1(0(0(0(1(1(0(2(2(0(2(2(2(2(2(2(0(x1)))))))))))))))))))))))))))
, 2(0(2(0(1(0(1(1(2(0(1(1(2(2(1(0(2(0(2(0(2(2(2(x1)))))))))))))))))))))))
->
2(0(0(1(1(2(0(2(2(1(1(2(2(0(1(2(2(2(0(0(2(0(2(2(2(0(2(x1)))))))))))))))))))))))))))
, 2(0(1(0(0(0(1(0(0(0(0(0(0(0(1(0(2(0(0(2(2(2(2(x1)))))))))))))))))))))))
->
2(2(2(1(1(2(1(2(0(1(1(2(1(0(2(1(0(0(1(0(1(1(2(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(2(2(2(1(1(0(0(2(2(2(0(0(0(2(1(2(2(0(2(0(2(0(x1)))))))))))))))))))))))
->
1(2(1(2(0(0(1(1(1(2(2(2(2(1(2(2(2(0(2(0(1(2(2(2(2(0(0(x1)))))))))))))))))))))))))))
, 1(2(0(2(1(2(2(1(2(2(2(0(1(1(1(1(0(1(0(0(2(0(1(x1)))))))))))))))))))))))
->
1(2(1(2(1(2(2(2(2(2(2(0(0(2(0(0(2(2(0(1(1(1(1(0(0(2(1(x1)))))))))))))))))))))))))))
, 1(2(0(0(2(0(1(2(2(0(2(1(2(1(2(0(1(0(1(2(0(2(1(x1)))))))))))))))))))))))
->
1(2(2(0(2(1(2(2(0(1(0(2(1(0(1(2(1(2(2(2(2(0(2(2(0(2(0(x1)))))))))))))))))))))))))))
, 1(1(2(2(1(0(2(0(1(1(2(2(2(1(0(1(0(0(2(1(1(0(2(x1)))))))))))))))))))))))
->
2(2(2(1(1(2(2(2(1(2(2(0(0(2(0(0(1(2(0(2(2(1(2(2(2(0(2(x1)))))))))))))))))))))))))))
, 1(1(1(0(2(2(1(1(1(2(2(0(2(0(2(1(1(2(1(2(1(2(2(x1)))))))))))))))))))))))
->
1(2(1(2(1(1(1(1(2(1(1(1(2(2(0(1(0(2(2(1(2(2(2(1(0(1(2(x1)))))))))))))))))))))))))))
, 1(1(0(2(1(2(2(2(2(1(0(1(2(0(1(2(1(1(0(2(1(2(0(x1)))))))))))))))))))))))
->
2(2(1(2(1(2(2(1(0(1(2(2(2(1(0(2(1(1(2(1(0(1(1(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(2(1(0(2(0(1(2(0(2(0(0(2(1(0(1(0(1(2(1(2(x1)))))))))))))))))))))))
->
2(0(2(2(1(1(1(2(2(0(1(2(0(2(1(1(2(1(0(0(2(0(1(2(2(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(1(2(2(2(2(1(0(2(1(2(0(0(0(1(0(2(1(1(1(2(x1)))))))))))))))))))))))
->
2(1(2(1(2(2(2(2(2(0(0(0(0(2(1(2(2(2(2(1(2(2(2(0(0(2(2(x1)))))))))))))))))))))))))))
, 1(1(0(0(1(1(1(2(2(2(1(2(1(0(0(0(2(2(2(0(1(2(0(x1)))))))))))))))))))))))
->
2(1(2(1(2(2(2(1(2(2(0(2(2(1(0(2(1(2(2(0(1(0(1(1(2(2(2(x1)))))))))))))))))))))))))))
, 1(0(1(0(2(2(2(2(1(0(0(2(0(2(1(2(1(2(1(1(2(0(2(x1)))))))))))))))))))))))
->
2(1(2(0(2(0(2(0(2(2(2(2(1(2(1(2(2(2(1(1(2(1(0(1(1(2(2(x1)))))))))))))))))))))))))))
, 1(0(0(1(0(1(1(0(2(1(1(2(1(2(1(2(0(1(2(2(1(2(1(x1)))))))))))))))))))))))
->
1(2(0(0(1(1(2(2(1(2(0(2(2(0(1(1(2(2(2(1(2(2(2(2(2(1(2(x1)))))))))))))))))))))))))))
, 0(1(2(1(1(2(2(2(1(1(0(0(1(0(2(0(2(2(1(0(2(1(1(x1)))))))))))))))))))))))
->
2(1(2(1(2(1(2(2(0(2(0(1(2(1(2(1(2(0(1(2(0(0(2(2(1(1(2(x1)))))))))))))))))))))))))))
, 0(1(1(1(2(2(1(0(0(2(2(2(2(0(2(0(0(0(0(1(0(0(2(x1)))))))))))))))))))))))
->
0(2(1(1(1(1(2(2(1(1(0(1(1(2(1(2(1(0(0(1(2(2(1(0(0(2(2(x1)))))))))))))))))))))))))))
, 0(1(1(1(1(2(1(1(2(2(0(1(0(1(1(0(2(0(0(2(0(1(0(x1)))))))))))))))))))))))
->
2(2(2(2(2(1(0(1(2(2(0(1(1(1(2(2(1(1(0(0(0(0(2(2(1(2(2(x1)))))))))))))))))))))))))))
, 0(1(1(0(1(1(1(2(2(0(2(0(1(2(2(2(0(1(2(0(1(0(2(x1)))))))))))))))))))))))
->
0(2(0(1(0(2(0(2(2(2(1(2(1(1(2(2(2(2(2(2(2(1(0(0(0(2(2(x1)))))))))))))))))))))))))))
, 0(1(0(0(1(2(2(1(0(1(2(1(2(0(1(0(2(2(0(1(2(1(0(x1)))))))))))))))))))))))
->
0(0(0(1(2(2(2(2(2(2(2(0(0(0(0(1(2(1(2(2(2(1(0(2(0(2(0(x1)))))))))))))))))))))))))))
, 0(0(2(0(2(2(1(2(1(1(2(1(1(2(1(0(0(0(0(1(1(2(1(x1)))))))))))))))))))))))
->
0(0(1(2(2(1(1(2(2(1(1(2(2(2(2(0(1(2(1(2(1(1(1(0(1(2(2(x1)))))))))))))))))))))))))))
, 0(0(1(2(0(1(0(0(2(0(1(1(0(1(2(1(1(2(2(1(1(0(2(x1)))))))))))))))))))))))
->
0(2(2(2(0(1(1(2(1(2(2(1(2(1(0(2(2(2(1(2(1(1(0(0(1(0(2(x1)))))))))))))))))))))))))))
, 0(0(1(0(2(2(1(2(0(0(1(2(0(2(2(2(1(1(2(0(0(2(1(x1)))))))))))))))))))))))
->
0(1(1(1(0(2(1(2(1(2(0(1(1(2(1(1(2(2(2(2(2(0(2(2(2(1(2(x1)))))))))))))))))))))))))))
, 0(0(0(2(2(0(2(2(2(1(1(0(2(2(1(2(1(0(2(0(0(0(1(x1)))))))))))))))))))))))
->
2(0(1(1(1(2(2(1(1(2(2(2(2(1(0(1(2(1(1(2(2(2(1(2(1(2(2(x1)))))))))))))))))))))))))))
, 0(0(0(0(1(0(0(2(2(1(0(2(0(2(1(1(2(1(2(2(0(1(1(x1)))))))))))))))))))))))
->
0(1(2(0(0(2(1(2(2(1(1(2(1(1(1(1(2(2(2(1(2(1(0(2(1(1(0(x1)))))))))))))))))))))))))))}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..