/bin/sh: line 1: 12111 Quit (core dumped) z3 -T:7.6 -smt2 /tmp/SMTP12085-21 > /tmp/SMTS12085-24 /bin/sh: line 1: 12135 Quit (core dumped) z3 -T:2.8499999999999996 -smt2 /tmp/SMTP12085-34 > /tmp/SMTS12085-36 /bin/sh: line 1: 12151 Killed z3 -T:4.75 -smt2 /tmp/SMTP12085-26 > /tmp/SMTS12085-28 WORST_CASE(?,O(1)) * Step 1: Sum. WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: gcd(x,0()) -> x gcd(0(),y) -> y gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y))) - Signature: {gcd/2} / {-/2,0/0, x gcd(0(),y) -> y gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y))) - Signature: {gcd/2} / {-/2,0/0, c_1() gcd#(0(),y) -> c_2() gcd#(s(x),s(y)) -> c_3(gcd#(s(x),-(y,x)),gcd#(-(x,y),s(y))) Weak DPs and mark the set of starting terms. * Step 3: PredecessorEstimation. WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: gcd#(x,0()) -> c_1() gcd#(0(),y) -> c_2() gcd#(s(x),s(y)) -> c_3(gcd#(s(x),-(y,x)),gcd#(-(x,y),s(y))) - Weak TRS: gcd(x,0()) -> x gcd(0(),y) -> y gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y))) - Signature: {gcd/2,gcd#/2} / {-/2,0/0, c_1() 2: gcd#(0(),y) -> c_2() 3: gcd#(s(x),s(y)) -> c_3(gcd#(s(x),-(y,x)),gcd#(-(x,y),s(y))) * Step 4: RemoveWeakSuffixes. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: gcd#(x,0()) -> c_1() gcd#(0(),y) -> c_2() gcd#(s(x),s(y)) -> c_3(gcd#(s(x),-(y,x)),gcd#(-(x,y),s(y))) - Weak TRS: gcd(x,0()) -> x gcd(0(),y) -> y gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y))) - Signature: {gcd/2,gcd#/2} / {-/2,0/0, c_1() 2:W:gcd#(0(),y) -> c_2() 3:W:gcd#(s(x),s(y)) -> c_3(gcd#(s(x),-(y,x)),gcd#(-(x,y),s(y))) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: gcd#(s(x),s(y)) -> c_3(gcd#(s(x),-(y,x)),gcd#(-(x,y),s(y))) 2: gcd#(0(),y) -> c_2() 1: gcd#(x,0()) -> c_1() * Step 5: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: gcd(x,0()) -> x gcd(0(),y) -> y gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y))) - Signature: {gcd/2,gcd#/2} / {-/2,0/0,