YES

> read an ari file for LCTRSs
(FUN  sum : Int -> Int )
(FUN  sum# : Int -> Int )
(RULES
    1 : sum(x) -> 0 WHEN (>= 0 x)
    2 : sum(x) -> +(x,sum(+(x,-1))) WHEN (not (>= 0 x))
)

(EQUATIONS
)

> Check left-linearity
Yes
> Compute critical pairs
( 0, 0 [ (and (>= 0 x_4) (>= 0 x_4)) ]
( 0, 0 [ (and (>= 0 x_3) (>= 0 x_3)) ]
( +(x_2,sum(+(x_2,-1))), +(x_2,sum(+(x_2,-1))) [ (and (not (>= 0 x_2)) (not (>= 0 x_2))) ]
( +(x_1,sum(+(x_1,-1))), +(x_1,sum(+(x_1,-1))) [ (and (not (>= 0 x_1)) (not (>= 0 x_1))) ]
> Check whether all CPs are trivial
Yes

YES