0.10/0.13 YES 0.10/0.13 (ignored inputs)COMMENT [17] Example 4 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama 0.10/0.13 input TRS: 0.10/0.13 [ h(f,a,a) -> h(g,a,a), 0.10/0.13 h(g,a,a) -> h(f,a,a), 0.10/0.13 a -> a', 0.10/0.13 h(?x,a',?y) -> h(?x,?y,?y), 0.10/0.13 h(?x,?y,a') -> h(?x,?y,?y) ] 0.10/0.13 Try persistent and layer-preserving decomposition... 0.10/0.13 Sort Assignment: 0.10/0.13 a : =>15 0.10/0.13 f : =>8 0.10/0.13 g : =>8 0.10/0.13 h : 8*15*15=>13 0.10/0.13 a' : =>15 0.10/0.13 maximal types: {8,13,15} 0.10/0.13 ...decomposition failed. 0.10/0.13 TRS: 0.10/0.13 [ h(f,a,a) -> h(g,a,a), 0.10/0.13 h(g,a,a) -> h(f,a,a), 0.10/0.13 a -> a', 0.10/0.13 h(?x,a',?y) -> h(?x,?y,?y), 0.10/0.13 h(?x,?y,a') -> h(?x,?y,?y) ] 0.10/0.13 Input: 0.10/0.13 [ h(f,a,a) -> h(g,a,a), 0.10/0.13 h(g,a,a) -> h(f,a,a), 0.10/0.13 a -> a', 0.10/0.13 h(?x,a',?y) -> h(?x,?y,?y), 0.10/0.13 h(?x,?y,a') -> h(?x,?y,?y) ] 0.10/0.13 0.10/0.13 Make it flat: 0.10/0.13 [ h(f,a,a) -> h(g,a,a), 0.10/0.13 h(g,a,a) -> h(f,a,a), 0.10/0.13 a -> a', 0.10/0.13 h(?x,a',?y) -> h(?x,?y,?y), 0.10/0.13 h(?x,?y,a') -> h(?x,?y,?y) ] 0.10/0.13 Time: 0.000 [s] 0.10/0.13 0.10/0.13 Make it Complete (R^): 0.10/0.13 [ h(g,a,a') = h(f,a,a), 0.10/0.13 h(g,a',a) = h(f,a,a), 0.10/0.13 h(f,a,a') = h(g,a,a), 0.10/0.13 h(f,a',a) = h(g,a,a), 0.10/0.13 h(f,a,a) = h(g,a',a'), 0.10/0.13 h(g,a,a') = h(f,a',a'), 0.10/0.13 h(g,a',a) = h(f,a',a'), 0.10/0.13 h(f,a',a) = h(g,a',a'), 0.10/0.13 h(g,a',a) = h(f,a,a'), 0.10/0.13 h(f,a',a) = h(g,a',a), 0.10/0.13 h(g,a,a') = h(f,a',a), 0.10/0.13 h(g,a,a') = h(f,a,a'), 0.10/0.13 h(f,a,a') = h(g,a',a'), 0.10/0.13 h(g,a,a') = h(g,a',a'), 0.10/0.13 h(g,a',a) = h(g,a',a'), 0.10/0.13 h(g,a',a) = h(g,a,a), 0.10/0.13 h(g,a',a) = h(g,a,a'), 0.10/0.13 h(g,a,a') = h(g,a,a), 0.10/0.13 h(g,a',a') = h(g,a,a), 0.10/0.13 h(f,a',a') = h(g,a',a'), 0.10/0.13 h(f,a,a') = h(f,a',a'), 0.10/0.13 h(f,a',a) = h(f,a',a'), 0.10/0.13 h(f,a',a) = h(f,a,a), 0.10/0.13 h(f,a',a) = h(f,a,a'), 0.10/0.13 h(f,a,a') = h(f,a,a), 0.10/0.13 h(f,a',a') = h(f,a,a), 0.10/0.13 h(g,a,a) = h(f,a',a'), 0.10/0.13 h(f,a,a) = h(g,a,a), 0.10/0.13 h(?x,?y,a) = h(?x,?y,?y), 0.10/0.13 h(?x,a,?y) = h(?x,?y,?y), 0.10/0.13 h(?x,?y,a) = h(?x,a',?y), 0.10/0.13 h(?x,?y,a) = h(?x,?y,a'), 0.10/0.13 h(?x,?y,a) = h(?x,a,?y), 0.10/0.13 h(?x,a,a') = h(?x,a',a'), 0.10/0.13 h(?x,a,?y) = h(?x,a',?y), 0.10/0.13 h(?x,a,a) = h(?x,a',a'), 0.10/0.13 h(?x,a,a) = h(?x,a,a'), 0.10/0.13 h(?x,a,a) = h(?x,a',a), 0.10/0.13 h(?x,a,a') = h(?x,a',a), 0.10/0.13 h(?x,a',a') = h(?x,a',a), 0.10/0.13 h(?x,a,?y) = h(?x,?y,a'), 0.10/0.13 a = a', 0.10/0.13 h(?x,a',?y) = h(?x,?y,a'), 0.10/0.13 h(?x,a',?y) = h(?x,?y,?y), 0.10/0.13 h(?x,?y,a') = h(?x,?y,?y) ] 0.10/0.13 Time: 0.086 [s] 0.10/0.13 0.10/0.13 CPNF: 0.10/0.13 [ g … g, 0.10/0.13 f … f, 0.10/0.13 a … a' ] 0.10/0.13 Time: 0.000 [s] 0.10/0.13 0.10/0.13 Now checking all the pairs in CW... 0.10/0.13 0.10/0.13 Time to check pairs: 0.000 [s] 0.10/0.13 0.10/0.13 The TRS has Uniqueness of Normal Forms. 0.10/0.13 /export/starexec/sandbox/benchmark/theBenchmark.trs: Success(UNC) 0.10/0.13 (85 msec.) 0.10/0.13 EOF