0.00/0.34	MAYBE
0.00/0.34	(ignored inputs)COMMENT doi:10.1007/3-540-60381-6_19 [71] Example 4 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.34	Conditional Rewrite Rules:
0.00/0.34	   [ f(?x',?x'') -> h(?x,f(?x,b)) | ?x' == ?x,?x'' == ?x,
0.00/0.34	     f(g(?y'),?y'') -> h(?y,f(g(?y),a)) | ?y' == ?y,?y'' == ?y,
0.00/0.34	     a -> b ]
0.00/0.34	Check whether all rules are type 3
0.00/0.34	OK
0.00/0.34	Check whether the input is deterministic
0.00/0.34	OK
0.00/0.34	Result of unraveling:
0.00/0.34	   [ f(?x',?x'') -> U0(?x',?x',?x''),
0.00/0.34	     U0(?x,?x',?x'') -> U1(?x'',?x',?x'',?x),
0.00/0.34	     U1(?x,?x',?x'',?x) -> h(?x,f(?x,b)),
0.00/0.34	     f(g(?y'),?y'') -> U2(?y',?y',?y''),
0.00/0.34	     U2(?y,?y',?y'') -> U3(?y'',?y',?y'',?y),
0.00/0.34	     U3(?y,?y',?y'',?y) -> h(?y,f(g(?y),a)),
0.00/0.34	     a -> b ]
0.00/0.34	Check whether U(R) is terminating
0.00/0.34	failed to show termination
0.00/0.34	Check whether the input is weakly left-linear
0.00/0.34	not weakly left-linear
0.00/0.34	Conditional critical pairs (CCPs):
0.00/0.34	   [ h(?y_1,f(g(?y_1),a)) = h(?x,f(?x,b)) | ?y'_1 == ?y_1,?y''_1 == ?y_1,g(?y'_1) == ?x,?y''_1 == ?x,
0.00/0.34	     h(?x,f(?x,b)) = h(?y_1,f(g(?y_1),a)) | g(?y'_1) == ?x,?x'' == ?x,?y'_1 == ?y_1,?x'' == ?y_1 ]
0.00/0.34	Check whether the input is almost orthogonale
0.00/0.34	not almost orthogonal
0.00/0.34	not weakly left-linear
0.00/0.34	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.34	(353 msec.)
0.00/0.34	EOF