0.00/0.02 MAYBE 0.00/0.02 (ignored inputs)COMMENT doi:10.1016/j.tcs.2012.09.005 [72] Example 4 submitted by: Thomas Sternagel and Aart Middeldorp 0.00/0.02 Conditional Rewrite Rules: 0.00/0.02 [ div(?z,?y) -> ?x | mul(?x,?y) == ?z,gt(?y,0) == tt, 0.00/0.02 mul(?x,0) -> 0, 0.00/0.02 mul(0,?y) -> 0, 0.00/0.02 mul(s(?x),s(?y)) -> s(?z) | mul(?x,s(?y)) == ?w,add(?w,?y) == ?z, 0.00/0.02 gt(0,?y) -> ff, 0.00/0.02 gt(s(?x),0) -> tt, 0.00/0.02 gt(s(?x),s(?y)) -> ?z | gt(?x,?y) == ?z ] 0.00/0.02 Check whether all rules are type 3 0.00/0.02 OK 0.00/0.02 Check whether the input is deterministic 0.00/0.02 No. non-deterministic rule: div(?z,?y) -> ?x | mul(?x,?y) == ?z,gt(?y,0) == tt 0.00/0.02 Conditional critical pairs (CCPs): 0.00/0.02 [ 0 = 0, 0.00/0.02 0 = 0 ] 0.00/0.02 Check whether the input is almost orthogonale 0.00/0.02 OK 0.00/0.02 Check whether the input is properly oriented 0.00/0.02 not properly oriented 0.00/0.02 /export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR) 0.00/0.02 (0 msec.) 0.00/0.03 EOF