0.00/0.06	MAYBE
0.00/0.06	(ignored inputs)COMMENT doi:10.1007/978-1-4757-3661-8 [18] Example 7.1.5 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.06	Conditional Rewrite Rules:
0.00/0.06	   [ lt(?x,0) -> false,
0.00/0.06	     lt(0,s(?x)) -> true,
0.00/0.06	     lt(s(?x),s(?y)) -> lt(?x,?y),
0.00/0.06	     m(0,s(?y)) -> 0,
0.00/0.06	     m(?x,0) -> ?x,
0.00/0.06	     m(s(?x),s(?y)) -> m(?x,?y),
0.00/0.06	     gcd(?x,?x) -> ?x,
0.00/0.06	     gcd(s(?x),0) -> s(?x),
0.00/0.06	     gcd(0,s(?y)) -> s(?y),
0.00/0.06	     gcd(s(?x),s(?y)) -> gcd(m(?x,?y),s(?y)) | lt(?y,?x) == true,
0.00/0.06	     gcd(s(?x),s(?y)) -> gcd(s(?x),m(?y,?x)) | lt(?x,?y) == true ]
0.00/0.06	Check whether all rules are type 3
0.00/0.06	OK
0.00/0.06	Check whether the input is deterministic
0.00/0.06	OK
0.00/0.06	Result of unraveling:
0.00/0.06	   [ lt(?x,0) -> false,
0.00/0.06	     lt(0,s(?x)) -> true,
0.00/0.06	     lt(s(?x),s(?y)) -> lt(?x,?y),
0.00/0.06	     m(0,s(?y)) -> 0,
0.00/0.06	     m(?x,0) -> ?x,
0.00/0.06	     m(s(?x),s(?y)) -> m(?x,?y),
0.00/0.06	     gcd(?x,?x) -> ?x,
0.00/0.06	     gcd(s(?x),0) -> s(?x),
0.00/0.06	     gcd(0,s(?y)) -> s(?y),
0.00/0.06	     gcd(s(?x),s(?y)) -> U1(lt(?y,?x),?x,?y),
0.00/0.06	     U1(true,?x,?y) -> gcd(m(?x,?y),s(?y)),
0.00/0.06	     gcd(s(?x),s(?y)) -> U1(lt(?x,?y),?x,?y),
0.00/0.06	     U1(true,?x,?y) -> gcd(s(?x),m(?y,?x)) ]
0.00/0.06	Check whether U(R) is terminating
0.00/0.06	OK
0.00/0.06	Check whether the input is weakly left-linear
0.00/0.06	not weakly left-linear
0.00/0.06	Check whether U(R) is confluent
0.00/0.06	U(R) is not confluent
0.00/0.06	Conditional critical pairs (CCPs):
0.00/0.06	   [ gcd(m(?y_9,?y_9),s(?y_9)) = s(?y_9) | lt(?y_9,?y_9) == true,
0.00/0.06	     gcd(s(?y_10),m(?y_10,?y_10)) = s(?y_10) | lt(?y_10,?y_10) == true,
0.00/0.06	     s(?x_9) = gcd(m(?x_9,?x_9),s(?x_9)) | lt(?x_9,?x_9) == true,
0.00/0.06	     gcd(s(?x_10),m(?y_10,?x_10)) = gcd(m(?x_10,?y_10),s(?y_10)) | lt(?x_10,?y_10) == true,lt(?y_10,?x_10) == true,
0.00/0.06	     s(?x_10) = gcd(s(?x_10),m(?x_10,?x_10)) | lt(?x_10,?x_10) == true,
0.00/0.06	     gcd(m(?x_9,?y_9),s(?y_9)) = gcd(s(?x_9),m(?y_9,?x_9)) | lt(?y_9,?x_9) == true,lt(?x_9,?y_9) == true ]
0.00/0.06	Check whether the input is almost orthogonale
0.00/0.06	not almost orthogonal
0.00/0.06	not weakly left-linear
0.00/0.06	Check whether the input is absolutely irreducible
0.00/0.06	OK
0.00/0.06	Check whether all CCPs are joinable
0.00/0.06	Some ccp may be feasible but not joinable
0.00/0.06	   [ gcd(m(?y_9,?y_9),s(?y_9)) = s(?y_9) | lt(?y_9,?y_9) == true,
0.00/0.06	     gcd(s(?y_10),m(?y_10,?y_10)) = s(?y_10) | lt(?y_10,?y_10) == true,
0.00/0.06	     s(?x_9) = gcd(m(?x_9,?x_9),s(?x_9)) | lt(?x_9,?x_9) == true,
0.00/0.06	     gcd(s(?x_10),m(?y_10,?x_10)) = gcd(m(?x_10,?y_10),s(?y_10)) | lt(?x_10,?y_10) == true,lt(?y_10,?x_10) == true,
0.00/0.06	     s(?x_10) = gcd(s(?x_10),m(?x_10,?x_10)) | lt(?x_10,?x_10) == true,
0.00/0.06	     gcd(m(?x_9,?y_9),s(?y_9)) = gcd(s(?x_9),m(?y_9,?x_9)) | lt(?y_9,?x_9) == true,lt(?x_9,?y_9) == true ]
0.00/0.06	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.06	(21 msec.)
0.00/0.06	EOF