NO Input: [ g(?y) -> f(?x,?y) ] Make it flat: [ g(?y) -> f(?x,?y) ] Time: 0.000 [s] Make it Complete (R^): [ f(?x,?y) = f(?x_1,?y), g(?y) = f(?x,?y) ] Time: 0.000 [s] The number of normal forms that must be checked: 6 Time: 0.000 [s] Now checking all the pairs... Time to check pairs: 0.000 [s] The TRS doesn't have Uniqueness of Normal Forms. Counter Example: f(?!cx_1,?!cx) <->* f(?!cx,?!cx) proof: f(?!cx_1,?!cx) ->R^ f(?!,?!cx) f(?!cx,?!cx) ->R^ f(?!,?!cx) Total Time: 0.001 [s] problems/r3.trs: Success(not UNC) real 0.02 user 0.00 sys 0.01