0.49/0.53	YES
0.49/0.53	(ignored inputs)COMMENT doi:10.1016/0022-0000 ( 86 ) 90033-4 [47] Example 2.3.ii submitted by: Thomas Sternagel and Aart Middeldorp
0.49/0.53	Conditional Rewrite Rules:
0.49/0.53	   [ App(App(App(S,?a),?b),?c) -> App(App(?a,?c),App(?b,?c)) | ?a == I,?b == I,?c == I,
0.49/0.53	     App(App(K,?a),?b) -> ?a | ?a == I,?b == I,
0.49/0.53	     App(I,?a) -> ?a | ?a == I ]
0.49/0.53	Check whether all rules are type 3
0.49/0.53	OK
0.49/0.53	Check whether the input is deterministic
0.49/0.53	OK
0.49/0.53	Result of unraveling:
0.49/0.53	   [ App(App(App(S,?a),?b),?c) -> U0(?a,?a,?b,?c),
0.49/0.53	     U0(I,?a,?b,?c) -> U1(?b,?a,?b,?c),
0.49/0.53	     U1(I,?a,?b,?c) -> U2(?c,?a,?b,?c),
0.49/0.53	     U2(I,?a,?b,?c) -> App(App(?a,?c),App(?b,?c)),
0.49/0.53	     App(App(K,?a),?b) -> U3(?a,?a,?b),
0.49/0.53	     U3(I,?a,?b) -> U4(?b,?a,?b),
0.49/0.53	     U4(I,?a,?b) -> ?a,
0.49/0.53	     App(I,?a) -> U5(?a,?a),
0.49/0.53	     U5(I,?a) -> ?a ]
0.49/0.53	Check whether U(R) is terminating
0.49/0.53	failed to show termination
0.49/0.53	Check whether the input is weakly left-linear
0.49/0.53	OK
0.49/0.53	Conditional critical pairs (CCPs):
0.49/0.53	   [  ]
0.49/0.53	Check whether the input is almost orthogonale
0.49/0.53	OK
0.49/0.53	Check whether the input is properly oriented
0.49/0.53	OK
0.49/0.53	Check whether the input is right-stable
0.49/0.53	OK
0.49/0.53	R is almost orthogonal, properly oriented, right stable
0.49/0.53	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR)
0.49/0.53	(526 msec.)
0.49/0.53	EOF