Tool Bounds
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ 1(0(1(0(0(1(0(0(0(1(1(0(0(1(0(1(0(0(1(0(0(1(0(1(1(1(1(0(1(1(1(0(0(1(1(0(1(1(0(0(0(1(1(0(1(0(1(0(0(0(1(1(1(1(1(1(1(0(0(1(1(0(0(1(0(1(0(0(1(1(1(1(0(0(0(0(1(0(1(1(0(0(0(1(1(0(0(0(0(0(0(1(0(0(0(1(0(0(0(1(0(0(0(0(0(0(0(1(0(1(1(0(1(0(1(1(0(0(1(1(1(0(1(1(1(1(0(0(1(1(0(0(0(0(0(0(0(0(1(1(1(1(1(1(1(0(1(1(0(1(1(0(1(1(1(0(0(1(1(0(1(1(1(0(0(0(1(1(1(0(1(1(0(1(0(1(1(0(1(0(1(0(1(1(1(0(0(0(0(0(1(1(0(0(0(1(0(0(0(0(1(0(0(1(0(1(1(1(1(0(1(1(1(1(1(1(1(0(1(0(1(0(0(0(1(1(0(1(0(1(0(1(1(0(0(0(0(0(1(1(1(0(1(1(0(1(0(0(1(1(0(1(1(1(1(1(1(0(0(1(0(0(1(0(1(0(1(0(0(0(0(1(0(0(0(0(0(1(1(1(0(0(1(1(1(0(1(0(1(0(0(0(1(1(0(0(0(1(1(1(1(0(0(1(1(1(1(1(0(0(1(0(0(0(1(1(1(1(0(0(0(1(0(0(1(0(0(1(1(1(1(1(0(1(1(0(0(0(1(0(0(0(0(1(0(1(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
0(1(0(1(0(0(1(1(1(0(1(0(1(1(1(0(0(1(0(0(1(0(1(1(0(0(1(0(1(1(1(1(1(0(0(0(1(1(1(0(1(1(0(0(1(1(1(0(1(0(1(0(0(0(1(1(0(0(0(0(1(1(1(0(0(1(1(0(1(0(1(0(1(1(1(0(1(1(1(1(1(1(0(1(1(1(1(0(1(0(1(0(1(1(0(1(1(1(0(0(0(1(0(0(0(0(0(0(1(0(0(1(0(0(0(1(1(0(0(0(0(0(0(0(1(0(1(0(1(1(0(0(0(1(1(0(0(0(1(1(1(1(1(0(0(1(1(0(1(1(0(0(0(1(0(0(0(1(1(0(1(0(1(1(0(0(1(0(1(1(1(0(1(0(0(1(0(1(1(0(1(1(1(0(1(1(0(1(1(1(1(1(1(0(1(1(1(0(0(0(0(1(1(1(0(1(1(0(0(1(1(0(1(1(0(1(1(0(0(0(1(0(1(0(0(0(1(1(1(1(0(1(1(0(0(0(1(0(0(0(1(0(0(0(0(1(1(0(1(1(1(0(0(0(0(0(1(1(1(1(0(0(1(1(0(0(1(1(1(1(1(1(0(0(0(1(0(0(0(1(0(1(1(1(1(0(1(0(1(0(0(0(0(1(0(1(1(1(1(1(0(0(0(0(0(0(0(0(0(1(0(0(0(1(0(1(0(1(1(0(0(0(1(0(0(0(1(0(1(0(0(0(0(1(1(1(1(0(0(0(0(1(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 3(4(5(x1))) -> 4(3(5(x1)))
, 0(0(x1)) -> 0(x1)
, 0(x1) -> 1(x1)}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..Tool CDI
stdout:
TIMEOUT
Statistics:
Number of monomials: 0
Last formula building started for bound 0
Last SAT solving started for bound 0Tool EDA
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ 1(0(1(0(0(1(0(0(0(1(1(0(0(1(0(1(0(0(1(0(0(1(0(1(1(1(1(0(1(1(1(0(0(1(1(0(1(1(0(0(0(1(1(0(1(0(1(0(0(0(1(1(1(1(1(1(1(0(0(1(1(0(0(1(0(1(0(0(1(1(1(1(0(0(0(0(1(0(1(1(0(0(0(1(1(0(0(0(0(0(0(1(0(0(0(1(0(0(0(1(0(0(0(0(0(0(0(1(0(1(1(0(1(0(1(1(0(0(1(1(1(0(1(1(1(1(0(0(1(1(0(0(0(0(0(0(0(0(1(1(1(1(1(1(1(0(1(1(0(1(1(0(1(1(1(0(0(1(1(0(1(1(1(0(0(0(1(1(1(0(1(1(0(1(0(1(1(0(1(0(1(0(1(1(1(0(0(0(0(0(1(1(0(0(0(1(0(0(0(0(1(0(0(1(0(1(1(1(1(0(1(1(1(1(1(1(1(0(1(0(1(0(0(0(1(1(0(1(0(1(0(1(1(0(0(0(0(0(1(1(1(0(1(1(0(1(0(0(1(1(0(1(1(1(1(1(1(0(0(1(0(0(1(0(1(0(1(0(0(0(0(1(0(0(0(0(0(1(1(1(0(0(1(1(1(0(1(0(1(0(0(0(1(1(0(0(0(1(1(1(1(0(0(1(1(1(1(1(0(0(1(0(0(0(1(1(1(1(0(0(0(1(0(0(1(0(0(1(1(1(1(1(0(1(1(0(0(0(1(0(0(0(0(1(0(1(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
0(1(0(1(0(0(1(1(1(0(1(0(1(1(1(0(0(1(0(0(1(0(1(1(0(0(1(0(1(1(1(1(1(0(0(0(1(1(1(0(1(1(0(0(1(1(1(0(1(0(1(0(0(0(1(1(0(0(0(0(1(1(1(0(0(1(1(0(1(0(1(0(1(1(1(0(1(1(1(1(1(1(0(1(1(1(1(0(1(0(1(0(1(1(0(1(1(1(0(0(0(1(0(0(0(0(0(0(1(0(0(1(0(0(0(1(1(0(0(0(0(0(0(0(1(0(1(0(1(1(0(0(0(1(1(0(0(0(1(1(1(1(1(0(0(1(1(0(1(1(0(0(0(1(0(0(0(1(1(0(1(0(1(1(0(0(1(0(1(1(1(0(1(0(0(1(0(1(1(0(1(1(1(0(1(1(0(1(1(1(1(1(1(0(1(1(1(0(0(0(0(1(1(1(0(1(1(0(0(1(1(0(1(1(0(1(1(0(0(0(1(0(1(0(0(0(1(1(1(1(0(1(1(0(0(0(1(0(0(0(1(0(0(0(0(1(1(0(1(1(1(0(0(0(0(0(1(1(1(1(0(0(1(1(0(0(1(1(1(1(1(1(0(0(0(1(0(0(0(1(0(1(1(1(1(0(1(0(1(0(0(0(0(1(0(1(1(1(1(1(0(0(0(0(0(0(0(0(0(1(0(0(0(1(0(1(0(1(1(0(0(0(1(0(0(0(1(0(1(0(0(0(0(1(1(1(1(0(0(0(0(1(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 3(4(5(x1))) -> 4(3(5(x1)))
, 0(0(x1)) -> 0(x1)
, 0(x1) -> 1(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:
{ 1(0(1(0(0(1(0(0(0(1(1(0(0(1(0(1(0(0(1(0(0(1(0(1(1(1(1(0(1(1(1(0(0(1(1(0(1(1(0(0(0(1(1(0(1(0(1(0(0(0(1(1(1(1(1(1(1(0(0(1(1(0(0(1(0(1(0(0(1(1(1(1(0(0(0(0(1(0(1(1(0(0(0(1(1(0(0(0(0(0(0(1(0(0(0(1(0(0(0(1(0(0(0(0(0(0(0(1(0(1(1(0(1(0(1(1(0(0(1(1(1(0(1(1(1(1(0(0(1(1(0(0(0(0(0(0(0(0(1(1(1(1(1(1(1(0(1(1(0(1(1(0(1(1(1(0(0(1(1(0(1(1(1(0(0(0(1(1(1(0(1(1(0(1(0(1(1(0(1(0(1(0(1(1(1(0(0(0(0(0(1(1(0(0(0(1(0(0(0(0(1(0(0(1(0(1(1(1(1(0(1(1(1(1(1(1(1(0(1(0(1(0(0(0(1(1(0(1(0(1(0(1(1(0(0(0(0(0(1(1(1(0(1(1(0(1(0(0(1(1(0(1(1(1(1(1(1(0(0(1(0(0(1(0(1(0(1(0(0(0(0(1(0(0(0(0(0(1(1(1(0(0(1(1(1(0(1(0(1(0(0(0(1(1(0(0(0(1(1(1(1(0(0(1(1(1(1(1(0(0(1(0(0(0(1(1(1(1(0(0(0(1(0(0(1(0(0(1(1(1(1(1(0(1(1(0(0(0(1(0(0(0(0(1(0(1(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
0(1(0(1(0(0(1(1(1(0(1(0(1(1(1(0(0(1(0(0(1(0(1(1(0(0(1(0(1(1(1(1(1(0(0(0(1(1(1(0(1(1(0(0(1(1(1(0(1(0(1(0(0(0(1(1(0(0(0(0(1(1(1(0(0(1(1(0(1(0(1(0(1(1(1(0(1(1(1(1(1(1(0(1(1(1(1(0(1(0(1(0(1(1(0(1(1(1(0(0(0(1(0(0(0(0(0(0(1(0(0(1(0(0(0(1(1(0(0(0(0(0(0(0(1(0(1(0(1(1(0(0(0(1(1(0(0(0(1(1(1(1(1(0(0(1(1(0(1(1(0(0(0(1(0(0(0(1(1(0(1(0(1(1(0(0(1(0(1(1(1(0(1(0(0(1(0(1(1(0(1(1(1(0(1(1(0(1(1(1(1(1(1(0(1(1(1(0(0(0(0(1(1(1(0(1(1(0(0(1(1(0(1(1(0(1(1(0(0(0(1(0(1(0(0(0(1(1(1(1(0(1(1(0(0(0(1(0(0(0(1(0(0(0(0(1(1(0(1(1(1(0(0(0(0(0(1(1(1(1(0(0(1(1(0(0(1(1(1(1(1(1(0(0(0(1(0(0(0(1(0(1(1(1(1(0(1(0(1(0(0(0(0(1(0(1(1(1(1(1(0(0(0(0(0(0(0(0(0(1(0(0(0(1(0(1(0(1(1(0(0(0(1(0(0(0(1(0(1(0(0(0(0(1(1(1(1(0(0(0(0(1(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 3(4(5(x1))) -> 4(3(5(x1)))
, 0(0(x1)) -> 0(x1)
, 0(x1) -> 1(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:
{ 1(0(1(0(0(1(0(0(0(1(1(0(0(1(0(1(0(0(1(0(0(1(0(1(1(1(1(0(1(1(1(0(0(1(1(0(1(1(0(0(0(1(1(0(1(0(1(0(0(0(1(1(1(1(1(1(1(0(0(1(1(0(0(1(0(1(0(0(1(1(1(1(0(0(0(0(1(0(1(1(0(0(0(1(1(0(0(0(0(0(0(1(0(0(0(1(0(0(0(1(0(0(0(0(0(0(0(1(0(1(1(0(1(0(1(1(0(0(1(1(1(0(1(1(1(1(0(0(1(1(0(0(0(0(0(0(0(0(1(1(1(1(1(1(1(0(1(1(0(1(1(0(1(1(1(0(0(1(1(0(1(1(1(0(0(0(1(1(1(0(1(1(0(1(0(1(1(0(1(0(1(0(1(1(1(0(0(0(0(0(1(1(0(0(0(1(0(0(0(0(1(0(0(1(0(1(1(1(1(0(1(1(1(1(1(1(1(0(1(0(1(0(0(0(1(1(0(1(0(1(0(1(1(0(0(0(0(0(1(1(1(0(1(1(0(1(0(0(1(1(0(1(1(1(1(1(1(0(0(1(0(0(1(0(1(0(1(0(0(0(0(1(0(0(0(0(0(1(1(1(0(0(1(1(1(0(1(0(1(0(0(0(1(1(0(0(0(1(1(1(1(0(0(1(1(1(1(1(0(0(1(0(0(0(1(1(1(1(0(0(0(1(0(0(1(0(0(1(1(1(1(1(0(1(1(0(0(0(1(0(0(0(0(1(0(1(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
0(1(0(1(0(0(1(1(1(0(1(0(1(1(1(0(0(1(0(0(1(0(1(1(0(0(1(0(1(1(1(1(1(0(0(0(1(1(1(0(1(1(0(0(1(1(1(0(1(0(1(0(0(0(1(1(0(0(0(0(1(1(1(0(0(1(1(0(1(0(1(0(1(1(1(0(1(1(1(1(1(1(0(1(1(1(1(0(1(0(1(0(1(1(0(1(1(1(0(0(0(1(0(0(0(0(0(0(1(0(0(1(0(0(0(1(1(0(0(0(0(0(0(0(1(0(1(0(1(1(0(0(0(1(1(0(0(0(1(1(1(1(1(0(0(1(1(0(1(1(0(0(0(1(0(0(0(1(1(0(1(0(1(1(0(0(1(0(1(1(1(0(1(0(0(1(0(1(1(0(1(1(1(0(1(1(0(1(1(1(1(1(1(0(1(1(1(0(0(0(0(1(1(1(0(1(1(0(0(1(1(0(1(1(0(1(1(0(0(0(1(0(1(0(0(0(1(1(1(1(0(1(1(0(0(0(1(0(0(0(1(0(0(0(0(1(1(0(1(1(1(0(0(0(0(0(1(1(1(1(0(0(1(1(0(0(1(1(1(1(1(1(0(0(0(1(0(0(0(1(0(1(1(1(1(0(1(0(1(0(0(0(0(1(0(1(1(1(1(1(0(0(0(0(0(0(0(0(0(1(0(0(0(1(0(1(0(1(1(0(0(0(1(0(0(0(1(0(1(0(0(0(0(1(1(1(1(0(0(0(0(1(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 3(4(5(x1))) -> 4(3(5(x1)))
, 0(0(x1)) -> 0(x1)
, 0(x1) -> 1(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:
{ 1(0(1(0(0(1(0(0(0(1(1(0(0(1(0(1(0(0(1(0(0(1(0(1(1(1(1(0(1(1(1(0(0(1(1(0(1(1(0(0(0(1(1(0(1(0(1(0(0(0(1(1(1(1(1(1(1(0(0(1(1(0(0(1(0(1(0(0(1(1(1(1(0(0(0(0(1(0(1(1(0(0(0(1(1(0(0(0(0(0(0(1(0(0(0(1(0(0(0(1(0(0(0(0(0(0(0(1(0(1(1(0(1(0(1(1(0(0(1(1(1(0(1(1(1(1(0(0(1(1(0(0(0(0(0(0(0(0(1(1(1(1(1(1(1(0(1(1(0(1(1(0(1(1(1(0(0(1(1(0(1(1(1(0(0(0(1(1(1(0(1(1(0(1(0(1(1(0(1(0(1(0(1(1(1(0(0(0(0(0(1(1(0(0(0(1(0(0(0(0(1(0(0(1(0(1(1(1(1(0(1(1(1(1(1(1(1(0(1(0(1(0(0(0(1(1(0(1(0(1(0(1(1(0(0(0(0(0(1(1(1(0(1(1(0(1(0(0(1(1(0(1(1(1(1(1(1(0(0(1(0(0(1(0(1(0(1(0(0(0(0(1(0(0(0(0(0(1(1(1(0(0(1(1(1(0(1(0(1(0(0(0(1(1(0(0(0(1(1(1(1(0(0(1(1(1(1(1(0(0(1(0(0(0(1(1(1(1(0(0(0(1(0(0(1(0(0(1(1(1(1(1(0(1(1(0(0(0(1(0(0(0(0(1(0(1(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
0(1(0(1(0(0(1(1(1(0(1(0(1(1(1(0(0(1(0(0(1(0(1(1(0(0(1(0(1(1(1(1(1(0(0(0(1(1(1(0(1(1(0(0(1(1(1(0(1(0(1(0(0(0(1(1(0(0(0(0(1(1(1(0(0(1(1(0(1(0(1(0(1(1(1(0(1(1(1(1(1(1(0(1(1(1(1(0(1(0(1(0(1(1(0(1(1(1(0(0(0(1(0(0(0(0(0(0(1(0(0(1(0(0(0(1(1(0(0(0(0(0(0(0(1(0(1(0(1(1(0(0(0(1(1(0(0(0(1(1(1(1(1(0(0(1(1(0(1(1(0(0(0(1(0(0(0(1(1(0(1(0(1(1(0(0(1(0(1(1(1(0(1(0(0(1(0(1(1(0(1(1(1(0(1(1(0(1(1(1(1(1(1(0(1(1(1(0(0(0(0(1(1(1(0(1(1(0(0(1(1(0(1(1(0(1(1(0(0(0(1(0(1(0(0(0(1(1(1(1(0(1(1(0(0(0(1(0(0(0(1(0(0(0(0(1(1(0(1(1(1(0(0(0(0(0(1(1(1(1(0(0(1(1(0(0(1(1(1(1(1(1(0(0(0(1(0(0(0(1(0(1(1(1(1(0(1(0(1(0(0(0(0(1(0(1(1(1(1(1(0(0(0(0(0(0(0(0(0(1(0(0(0(1(0(1(0(1(1(0(0(0(1(0(0(0(1(0(1(0(0(0(0(1(1(1(1(0(0(0(0(1(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
, 3(4(5(x1))) -> 4(3(5(x1)))
, 0(0(x1)) -> 0(x1)
, 0(x1) -> 1(x1)}
StartTerms: all
Strategy: none
Certificate: TIMEOUT
Proof:
Computation stopped due to timeout after 60.0 seconds.
Arrrr..