YES
(ignored inputs)COMMENT full experiments for [35] submitted by: Takahito Aoto and Yoshihito Toyama
Input:
   [ and3(?x,?y,F) -> F,
     and3(T,T,T) -> T,
     and3(?x,?y,?z) -> and3(?y,?z,?x) ]

Make it flat:
   [ and3(?x,?y,F) -> F,
     and3(T,T,T) -> T,
     and3(?x,?y,?z) -> and3(?y,?z,?x) ]
Time: 0.000 [s]

Make it Complete (R^):
   [ and3(?x,?y,F) = and3(?x_1,?y_1,F),
     F = and3(F,?x,?y),
     and3(?y,F,?x) = and3(?x_1,?y_1,F),
     and3(F,?x_1,?y_1) = and3(?x,?y,F),
     and3(F,?x_1,?y_1) = and3(F,?x,?y),
     and3(?y,F,?x) = and3(F,?x_1,?y_1),
     and3(?y,F,?x) = and3(?y_1,F,?x_1),
     F = and3(?y,F,?x),
     and3(?x,?y,F) = F,
     and3(T,T,T) = T,
     and3(?x,?y,?z) = and3(?y,?z,?x) ]
Time: 0.005 [s]

CPNF:
   [ F … F,
     T … T ]
Time: 0.000 [s]

Now checking all the pairs in CW...

Time to check pairs: 0.000 [s]

The TRS has Uniqueness of Normal Forms.
Total Time: 0.005 [s]

problems/130.trs: Success(UNC)
real 0.02
user 0.01
sys 0.01