0.00/0.08	MAYBE
0.00/0.08	(ignored inputs)COMMENT doi:10.1007/3-540-54317-1_79 [55] CL-pc^L of Table 2.3 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.08	Conditional Rewrite Rules:
0.00/0.08	   [ App(App(App(S,?x),?y),?z) -> App(App(?x,?z),App(?y,?z)),
0.00/0.08	     App(App(K,?x),?y) -> ?x,
0.00/0.08	     App(I,?x) -> ?x,
0.00/0.08	     App(App(App(C,T),?x),?y) -> ?x,
0.00/0.08	     App(App(App(C,F),?x),?y) -> ?y,
0.00/0.08	     App(App(App(C,?z),?x),?y) -> ?x | ?x == ?y,
0.00/0.08	     App(App(App(C,?z),?x),?y) -> ?y | ?x == ?y ]
0.00/0.08	Check whether all rules are type 3
0.00/0.08	OK
0.00/0.08	Check whether the input is deterministic
0.00/0.08	OK
0.00/0.08	Result of unraveling:
0.00/0.08	   [ App(App(App(S,?x),?y),?z) -> App(App(?x,?z),App(?y,?z)),
0.00/0.08	     App(App(K,?x),?y) -> ?x,
0.00/0.08	     App(I,?x) -> ?x,
0.00/0.08	     App(App(App(C,T),?x),?y) -> ?x,
0.00/0.08	     App(App(App(C,F),?x),?y) -> ?y,
0.00/0.08	     App(App(App(C,?z),?x),?y) -> U1(?x,?x,?y,?z),
0.00/0.08	     U1(?y,?x,?y,?z) -> ?x,
0.00/0.08	     U1(?y,?x,?y,?z) -> ?y ]
0.00/0.08	Check whether U(R) is terminating
0.00/0.08	failed to show termination
0.00/0.08	Check whether the input is weakly left-linear
0.00/0.08	not weakly left-linear
0.00/0.08	Conditional critical pairs (CCPs):
0.00/0.08	   [ ?x_5 = ?x_5 | ?x_5 == ?y_5,
0.00/0.08	     ?y_6 = ?x_6 | ?x_6 == ?y_6,
0.00/0.08	     ?x_5 = ?y_5 | ?x_5 == ?y_5,
0.00/0.08	     ?y_6 = ?y_6 | ?x_6 == ?y_6,
0.00/0.08	     ?x_3 = ?x_3 | ?x_3 == ?y_3,
0.00/0.08	     ?y_4 = ?x_4 | ?x_4 == ?y_4,
0.00/0.08	     ?y_6 = ?x_6 | ?x_6 == ?y_6,?x_6 == ?y_6,
0.00/0.08	     ?x_3 = ?y_3 | ?x_3 == ?y_3,
0.00/0.08	     ?y_4 = ?y_4 | ?x_4 == ?y_4,
0.00/0.08	     ?x_5 = ?y_5 | ?x_5 == ?y_5,?x_5 == ?y_5 ]
0.00/0.08	Check whether the input is almost orthogonale
0.00/0.08	not almost orthogonal
0.00/0.08	not weakly left-linear
0.00/0.08	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.08	(43 msec.)
0.00/0.08	EOF