Problem Various 04 21

Tool Bounds

Execution Time	60.066277ms
Answer	TIMEOUT
Input	Various 04 21

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x))
     , +(p10(), p5()) -> +(p5(), p10())
     , +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x))
     , +(p10(), p2()) -> +(p2(), p10())
     , +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x))
     , +(p10(), p1()) -> +(p1(), p10())
     , +(p5(), +(p5(), x)) -> +(p10(), x)
     , +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x))
     , +(p5(), p2()) -> +(p2(), p5())
     , +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x))
     , +(p5(), p1()) -> +(p1(), p5())
     , +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x))
     , +(p2(), +(p2(), p2())) -> +(p1(), p5())
     , +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x))
     , +(p2(), p1()) -> +(p1(), p2())
     , +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x)
     , +(p1(), +(p1(), x)) -> +(p2(), x)
     , +(+(x, y), z) -> +(x, +(y, z))
     , +(p5(), p5()) -> p10()
     , +(p1(), +(p2(), p2())) -> p5()
     , +(p1(), p1()) -> p2()}
  StartTerms: all
  Strategy: none

Certificate: TIMEOUT

Proof:
  Computation stopped due to timeout after 60.0 seconds.

Arrrr..

Tool CDI

Execution Time	60.06073ms
Answer	TIMEOUT
Input	Various 04 21

stdout:

TIMEOUT

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

Tool EDA

Execution Time	60.318893ms
Answer	TIMEOUT
Input	Various 04 21

stdout:

Tool IDA

Execution Time	60.041573ms
Answer	TIMEOUT
Input	Various 04 21

stdout:

Tool TRI

Execution Time	60.041466ms
Answer	TIMEOUT
Input	Various 04 21

stdout:

Tool TRI2

Execution Time	1.2102201ms
Answer	MAYBE
Input	Various 04 21

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  +(p10(), +(p5(), x)) -> +(p5(), +(p10(), x))
     , +(p10(), p5()) -> +(p5(), p10())
     , +(p10(), +(p2(), x)) -> +(p2(), +(p10(), x))
     , +(p10(), p2()) -> +(p2(), p10())
     , +(p10(), +(p1(), x)) -> +(p1(), +(p10(), x))
     , +(p10(), p1()) -> +(p1(), p10())
     , +(p5(), +(p5(), x)) -> +(p10(), x)
     , +(p5(), +(p2(), x)) -> +(p2(), +(p5(), x))
     , +(p5(), p2()) -> +(p2(), p5())
     , +(p5(), +(p1(), x)) -> +(p1(), +(p5(), x))
     , +(p5(), p1()) -> +(p1(), p5())
     , +(p2(), +(p2(), +(p2(), x))) -> +(p1(), +(p5(), x))
     , +(p2(), +(p2(), p2())) -> +(p1(), p5())
     , +(p2(), +(p1(), x)) -> +(p1(), +(p2(), x))
     , +(p2(), p1()) -> +(p1(), p2())
     , +(p1(), +(p2(), +(p2(), x))) -> +(p5(), x)
     , +(p1(), +(p1(), x)) -> +(p2(), x)
     , +(+(x, y), z) -> +(x, +(y, z))
     , +(p5(), p5()) -> p10()
     , +(p1(), +(p2(), p2())) -> p5()
     , +(p1(), p1()) -> p2()}
  StartTerms: all
  Strategy: none

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..