61.90/60.03 /export/starexec/sandbox/solver/bin/starexec_run_coco: line 4: 43803 Done java -jar "$DIR/txtr-0.jar" "$DIR/trs.xml.txtr" "$1" 61.90/60.03 43804 Alarm clock | NaTT.exe 2> "$2/stderr.txt" 61.90/60.03 Input TRS: 61.90/60.03 1: add(0(),x) -> x 61.90/60.03 2: add(s(x),y) -> s(add(x,y)) 61.90/60.03 3: mult(0(),y) -> 0() 61.90/60.03 4: mult(s(x),y) -> add(mult(x,y),y) 61.90/60.03 5: lte(0(),y) -> true() 61.90/60.03 6: lte(s(x),0()) -> false() 61.90/60.03 7: lte(s(x),s(y)) -> lte(x,y) 61.90/60.03 8: minus(0(),s(y)) -> 0() 61.90/60.03 9: minus(x,0()) -> x 61.90/60.03 10: minus(s(x),s(y)) -> minus(x,y) 61.90/60.03 11: mod(0(),y) -> 0() 61.90/60.03 12: mod(x,0()) -> x 61.90/60.03 13: mod(x,s(y)) -> mod(minus(x,s(y)),s(y)) | lte(s(y),x) --> true() 61.90/60.03 14: mod(x,s(y)) -> x | lte(s(y),x) --> false() 61.90/60.03 15: div(0(),s(x)) -> 0() 61.90/60.03 16: div(s(x),s(y)) -> 0() | lte(s(x),y) --> true() 61.90/60.03 17: div(s(x),s(y)) -> s(q) | lte(s(x),y) --> false() | div(minus(x,y),s(y)) --> q 61.90/60.03 18: power(x,0()) -> s(0()) 61.90/60.03 19: power(x,n) -> mult(mult(y,y),s(0())) | mod(n,s(s(0()))) --> 0() | power(x,div(n,s(s(0())))) --> y 61.90/60.03 20: power(x,n) -> mult(mult(y,y),x) | mod(n,s(s(0()))) --> s(z) | power(x,div(n,s(s(0())))) --> y 61.90/60.03 Infeasibility test: 61.90/60.03 mod(x3,s(s(0()))) --> 0() 61.90/60.03 power(x2,div(x3,s(s(0())))) --> y 61.90/60.03 mod(x3,s(s(0()))) --> s(x1) 61.90/60.03 power(x2,div(x3,s(s(0())))) --> x4 61.90/60.03 Co-Order(NegReal,≥,Sum) ...Co-QLPOpS ...Co-QWPOpS(PosReal,>,Sum) ...Co-Order(PosReal,≥,Sum-Sum; PosReal,≥,Sum-Sum) ... 61.90/60.03 EOF