0.00/0.14	MAYBE
0.00/0.14	(ignored inputs)COMMENT [63] TRS R_28 , p. 138 http://www.sakabe.nuie.nagoya-u.ac.jp/~nishida/DB/pdf/nishida04phdthesis.pdf submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.14	Conditional Rewrite Rules:
0.00/0.14	   [ gcd(?z,?y) -> gcd(?x,?y) | iadd(?z) == tp2(?x,?y),
0.00/0.14	     gcd(?y,?z) -> gcd(?x,?y) | iadd(?z) == tp2(?x,?y),
0.00/0.14	     gcd(?x,0) -> ?x,
0.00/0.14	     gcd(0,?x) -> ?x,
0.00/0.14	     iadd(?y) -> tp2(0,?y),
0.00/0.14	     iadd(s(?z)) -> tp2(s(?x),?y) | iadd(?z) == tp2(?x,?y),
0.00/0.14	     iadd(add(?x,?y)) -> tp2(?x,?y) ]
0.00/0.14	Check whether all rules are type 3
0.00/0.14	OK
0.00/0.14	Check whether the input is deterministic
0.00/0.14	OK
0.00/0.14	Result of unraveling:
0.00/0.14	   [ gcd(?z,?y) -> U0(iadd(?z),?y,?z),
0.00/0.14	     U0(tp2(?x,?y),?y,?z) -> gcd(?x,?y),
0.00/0.14	     gcd(?y,?z) -> U1(iadd(?z),?y,?z),
0.00/0.14	     U1(tp2(?x,?y),?y,?z) -> gcd(?x,?y),
0.00/0.14	     gcd(?x,0) -> ?x,
0.00/0.14	     gcd(0,?x) -> ?x,
0.00/0.14	     iadd(?y) -> tp2(0,?y),
0.00/0.14	     iadd(s(?z)) -> U2(iadd(?z),?z),
0.00/0.14	     U2(tp2(?x,?y),?z) -> tp2(s(?x),?y),
0.00/0.14	     iadd(add(?x,?y)) -> tp2(?x,?y) ]
0.00/0.14	Check whether U(R) is terminating
0.00/0.14	failed to show termination
0.00/0.14	Check whether the input is weakly left-linear
0.00/0.14	not weakly left-linear
0.00/0.14	Conditional critical pairs (CCPs):
0.00/0.14	   [ gcd(?x_1,?y_1) = gcd(?x,?z_1) | iadd(?z_1) == tp2(?x_1,?y_1),iadd(?y_1) == tp2(?x,?z_1),
0.00/0.14	     ?x_2 = gcd(?x,0) | iadd(?x_2) == tp2(?x,0),
0.00/0.14	     ?x_3 = gcd(?x,?x_3) | iadd(0) == tp2(?x,?x_3),
0.00/0.14	     gcd(?x,?y) = gcd(?x_1,?z) | iadd(?z) == tp2(?x,?y),iadd(?y) == tp2(?x_1,?z),
0.00/0.14	     ?x_2 = gcd(?x_1,?x_2) | iadd(0) == tp2(?x_1,?x_2),
0.00/0.14	     ?x_3 = gcd(?x_1,0) | iadd(?x_3) == tp2(?x_1,0),
0.00/0.14	     gcd(?x,0) = ?z | iadd(?z) == tp2(?x,0),
0.00/0.14	     gcd(?x_1,?y_1) = ?y_1 | iadd(0) == tp2(?x_1,?y_1),
0.00/0.14	     0 = 0,
0.00/0.14	     gcd(?x,?y) = ?y | iadd(0) == tp2(?x,?y),
0.00/0.14	     gcd(?x_1,0) = ?z_1 | iadd(?z_1) == tp2(?x_1,0),
0.00/0.14	     0 = 0,
0.00/0.14	     tp2(s(?x_5),?y_5) = tp2(0,s(?z_5)) | iadd(?z_5) == tp2(?x_5,?y_5),
0.00/0.14	     tp2(?x_6,?y_6) = tp2(0,add(?x_6,?y_6)),
0.00/0.14	     tp2(0,s(?z_5)) = tp2(s(?x_5),?y_5) | iadd(?z_5) == tp2(?x_5,?y_5),
0.00/0.14	     tp2(0,add(?x_6,?y_6)) = tp2(?x_6,?y_6) ]
0.00/0.14	Check whether the input is almost orthogonale
0.00/0.14	not almost orthogonal
0.00/0.14	not weakly left-linear
0.00/0.14	/export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.14	(109 msec.)
0.00/0.14	EOF