MAYBE


Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR z x y)
    (RULES
      lte(x,z) -> true | lte(x,y) == true, lte(y,z) == true
      lte(x,x) -> true
      max(x,y) -> y | lte(x,y) == true
      max(x,y) -> x | lte(x,y) == false
      lte(x,max(x,y)) -> true
      lte(y,max(x,y)) -> true
    )

No "->="-rules.

Decomposed conditions if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR z x y)
    (RULES
      lte(x,z) -> true | lte(x,y) == true, lte(y,z) == true
      lte(x,x) -> true
      max(x,y) -> y | lte(x,y) == true
      max(x,y) -> x | lte(x,y) == false
      lte(x,max(x,y)) -> true
      lte(y,max(x,y)) -> true
    )

Removed infeasible rules as much as possible.
    (CONDITIONTYPE ORIENTED)
    (VAR z x y)
    (RULES
      max(x,y) -> y | lte(x,y) == true
      lte(x,z) -> true | lte(x,y) == true, lte(y,z) == true
      lte(x,x) -> true
      lte(x,max(x,y)) -> true
      lte(y,max(x,y)) -> true
    )

Try to disprove confluence of the following (C)TRS:
    (CONDITIONTYPE ORIENTED)
    (VAR z x y)
    (RULES
      max(x,y) -> y | lte(x,y) == true
      lte(x,z) -> true | lte(x,y) == true, lte(y,z) == true
      lte(x,x) -> true
      lte(x,max(x,y)) -> true
      lte(y,max(x,y)) -> true
    )

Failed either to apply SR and U for normal 1CTRSs to the above CTRS or to prove confluence of any converted TRSs.

Try to apply SR and U for 3DCTRSs to the above CTRS.