YES

> read an ari file for LCTRSs
(FUN  cnt : (_ BitVec 4) -> (_ BitVec 4) )
(FUN  u1 : (_ BitVec 4) * (_ BitVec 4) * (_ BitVec 4) -> (_ BitVec 4) )
(FUN  cnt# : (_ BitVec 4) -> (_ BitVec 4) )
(FUN  u1# : (_ BitVec 4) * (_ BitVec 4) * (_ BitVec 4) -> (_ BitVec 4) )
(RULES
    1 : cnt(x) -> u1(x,#x0,#x0)
    2 : u1(x,i,z) -> u1(x,bvadd(i,#x1),bvadd(z,#x1)) WHEN (bvult i x)
    3 : u1(x,i,z) -> z WHEN (not (bvult i x))
)

(EQUATIONS
)

> Check left-linearity
Yes
> Compute critical pairs
( u1(x_8,#x0,#x0), u1(x_8,#x0,#x0) [ true ]
( u1(x_7,#x0,#x0), u1(x_7,#x0,#x0) [ true ]
( u1(x_4,bvadd(i_4,#x1),bvadd(z_4,#x1)), u1(x_4,bvadd(i_4,#x1),bvadd(z_4,#x1)) [ (and (bvult i_4 x_4) (bvult i_4 x_4)) ]
( u1(x_3,bvadd(i_3,#x1),bvadd(z_3,#x1)), u1(x_3,bvadd(i_3,#x1),bvadd(z_3,#x1)) [ (and (bvult i_3 x_3) (bvult i_3 x_3)) ]
( z_2, z_2 [ (and (not (bvult i_2 x_2)) (not (bvult i_2 x_2))) ]
( z_1, z_1 [ (and (not (bvult i_1 x_1)) (not (bvult i_1 x_1))) ]
> Check whether all CPs are trivial
Yes

YES