0.00/0.03	MAYBE
0.00/0.03	(ignored inputs)COMMENT doi:10.1007/3-540-58216-9_40 [45] Example 4.1.a submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.03	Conditional Rewrite Rules:
0.00/0.03	   [ plus(0,?y) -> ?y,
0.00/0.03	     plus(s(?x),?y) -> plus(?x,s(?y)),
0.00/0.03	     f(?x,?y) -> ?z | plus(?x,?y) == plus(?z,?z') ]
0.00/0.03	Check whether all rules are type 3
0.00/0.03	OK
0.00/0.03	Check whether the input is deterministic
0.00/0.03	OK
0.00/0.03	Result of unraveling:
0.00/0.03	   [ plus(0,?y) -> ?y,
0.00/0.03	     plus(s(?x),?y) -> plus(?x,s(?y)),
0.00/0.03	     f(?x,?y) -> U0(plus(?x,?y),?x,?y),
0.00/0.03	     U0(plus(?z,?z'),?x,?y) -> ?z ]
0.00/0.03	Check whether U(R) is terminating
0.00/0.03	OK
0.00/0.03	Check whether the input is weakly left-linear
0.00/0.03	OK
0.00/0.03	Check whether U(R) is confluent
0.00/0.03	U(R) is not confluent
0.00/0.03	Conditional critical pairs (CCPs):
0.00/0.03	   [  ]
0.00/0.03	Check whether the input is almost orthogonale
0.00/0.03	OK
0.00/0.03	Check whether the input is properly oriented
0.00/0.03	OK
0.00/0.03	Check whether the input is right-stable
0.00/0.03	not right-stable
0.00/0.03	OK
0.00/0.03	Check whether the input is absolutely irreducible
0.00/0.03	not absolutely irreducible
0.00/0.03	/export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.03	(5 msec.)
0.00/0.03	EOF