0.00/0.05 NO 0.00/0.05 (ignored inputs)COMMENT [63] TRS R_27 , 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.05 Conditional Rewrite Rules: 0.00/0.05 [ gcd(add(?x,?y),?y) -> gcd(?x,?y), 0.00/0.05 gcd(?y,add(?x,?y)) -> gcd(?x,?y), 0.00/0.05 gcd(?x,0) -> ?x, 0.00/0.05 gcd(0,?x) -> ?x, 0.00/0.05 gcd(?x,?y) -> gcd(?y,?x) | leq(?y,?x) == false, 0.00/0.05 add(0,?y) -> ?y, 0.00/0.05 add(s(?x),?y) -> s(add(?x,?y)) ] 0.00/0.05 Check whether all rules are type 3 0.00/0.05 OK 0.00/0.05 Check whether the input is deterministic 0.00/0.05 OK 0.00/0.05 Result of unraveling: 0.00/0.05 [ gcd(add(?x,?y),?y) -> gcd(?x,?y), 0.00/0.05 gcd(?y,add(?x,?y)) -> gcd(?x,?y), 0.00/0.05 gcd(?x,0) -> ?x, 0.00/0.05 gcd(0,?x) -> ?x, 0.00/0.05 gcd(?x,?y) -> U0(leq(?y,?x),?x,?y), 0.00/0.05 U0(false,?x,?y) -> gcd(?y,?x), 0.00/0.05 add(0,?y) -> ?y, 0.00/0.05 add(s(?x),?y) -> s(add(?x,?y)) ] 0.00/0.05 Check whether U(R) is terminating 0.00/0.05 OK 0.00/0.05 Check whether the input is weakly left-linear 0.00/0.05 not weakly left-linear 0.00/0.05 Check whether U(R) is confluent 0.00/0.05 U(R) is not confluent 0.00/0.05 Conditional critical pairs (CCPs): 0.00/0.05 [ add(?x,0) = gcd(?x,0), 0.00/0.05 gcd(?y_4,add(?x,?y_4)) = gcd(?x,?y_4) | leq(?y_4,add(?x,?y_4)) == false, 0.00/0.05 gcd(?y_5,?y_5) = gcd(0,?y_5), 0.00/0.05 gcd(s(add(?x_6,?y_6)),?y_6) = gcd(s(?x_6),?y_6), 0.00/0.05 add(?x_1,0) = gcd(?x_1,0), 0.00/0.05 gcd(add(?x_1,?x_4),?x_4) = gcd(?x_1,?x_4) | leq(add(?x_1,?x_4),?x_4) == false, 0.00/0.05 gcd(?y_5,?y_5) = gcd(0,?y_5), 0.00/0.05 gcd(?y_6,s(add(?x_6,?y_6))) = gcd(s(?x_6),?y_6), 0.00/0.05 gcd(?x,0) = add(?x,0), 0.00/0.05 0 = 0, 0.00/0.05 gcd(0,?x_4) = ?x_4 | leq(0,?x_4) == false, 0.00/0.05 gcd(?x_1,0) = add(?x_1,0), 0.00/0.05 0 = 0, 0.00/0.05 gcd(?y_4,0) = ?y_4 | leq(?y_4,0) == false, 0.00/0.05 gcd(?x,?y) = gcd(?y,add(?x,?y)) | leq(?y,add(?x,?y)) == false, 0.00/0.05 gcd(?x_1,?y_1) = gcd(add(?x_1,?y_1),?y_1) | leq(add(?x_1,?y_1),?y_1) == false, 0.00/0.05 ?x_2 = gcd(0,?x_2) | leq(0,?x_2) == false, 0.00/0.05 ?x_3 = gcd(?x_3,0) | leq(?x_3,0) == false ] 0.00/0.05 Check whether the input is almost orthogonale 0.00/0.05 not almost orthogonal 0.00/0.05 not weakly left-linear 0.00/0.05 Check whether the input is absolutely irreducible 0.00/0.05 OK 0.00/0.05 Check whether all CCPs are joinable 0.00/0.05 Some ccp may be feasible but not joinable 0.00/0.05 [ add(?x,0) = gcd(?x,0), 0.00/0.05 gcd(?y_5,?y_5) = gcd(0,?y_5), 0.00/0.05 gcd(s(add(?x_6,?y_6)),?y_6) = gcd(s(?x_6),?y_6), 0.00/0.05 add(?x_1,0) = gcd(?x_1,0), 0.00/0.05 gcd(?y_5,?y_5) = gcd(0,?y_5), 0.00/0.05 gcd(?y_6,s(add(?x_6,?y_6))) = gcd(s(?x_6),?y_6), 0.00/0.05 gcd(?x,0) = add(?x,0), 0.00/0.05 gcd(?x_1,0) = add(?x_1,0) ] 0.00/0.05 A feasible but not joinable CCP: add(?x,0) = gcd(?x,0) 0.00/0.05 /export/starexec/sandbox2/benchmark/theBenchmark.trs: Success(not CR) 0.00/0.05 (12 msec.) 0.00/0.05 EOF