0.00/0.13 MAYBE 0.00/0.13 (ignored inputs)COMMENT [63] TRS R_29 , p. 139 http://www.sakabe.nuie.nagoya-u.ac.jp/~nishida/DB/pdf/nishida04phdthesis.pdf submitted by: Thomas Sternagel and Aart Middeldorp 0.00/0.13 Conditional Rewrite Rules: 0.00/0.13 [ gcd(?z,?y) -> gcd(?x,?y) | iadd(?z) == tp2(?x,?y), 0.00/0.13 gcd(?y,?z) -> gcd(?x,?y) | iadd(?z) == tp2(?x,?y), 0.00/0.13 gcd(?x,0) -> ?x, 0.00/0.13 gcd(0,?x) -> ?x, 0.00/0.13 iadd(?y) -> tp2(0,?y), 0.00/0.13 iadd(s(?z)) -> u1(iadd(?z)), 0.00/0.13 u1(tp2(?x,?y)) -> tp2(s(?x),?y), 0.00/0.13 iadd(add(?x,?y)) -> tp2(?x,?y) ] 0.00/0.13 Check whether all rules are type 3 0.00/0.13 OK 0.00/0.13 Check whether the input is deterministic 0.00/0.13 OK 0.00/0.13 Result of unraveling: 0.00/0.13 [ gcd(?z,?y) -> U0(iadd(?z),?y,?z), 0.00/0.13 U0(tp2(?x,?y),?y,?z) -> gcd(?x,?y), 0.00/0.13 gcd(?y,?z) -> U1(iadd(?z),?y,?z), 0.00/0.13 U1(tp2(?x,?y),?y,?z) -> gcd(?x,?y), 0.00/0.13 gcd(?x,0) -> ?x, 0.00/0.13 gcd(0,?x) -> ?x, 0.00/0.13 iadd(?y) -> tp2(0,?y), 0.00/0.13 iadd(s(?z)) -> u1(iadd(?z)), 0.00/0.13 u1(tp2(?x,?y)) -> tp2(s(?x),?y), 0.00/0.13 iadd(add(?x,?y)) -> tp2(?x,?y) ] 0.00/0.13 Check whether U(R) is terminating 0.00/0.13 failed to show termination 0.00/0.13 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 u1(iadd(?z_5)) = tp2(0,s(?z_5)), 0.00/0.14 tp2(?x_7,?y_7) = tp2(0,add(?x_7,?y_7)), 0.00/0.14 tp2(0,s(?z_5)) = u1(iadd(?z_5)), 0.00/0.14 tp2(0,add(?x_7,?y_7)) = tp2(?x_7,?y_7) ] 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 (95 msec.) 0.00/0.14 EOF