/bin/sh: line 1: 4340 Quit (core dumped) z3 -T:2.8499999999999996 -smt2 /tmp/SMTP4240-51 > /tmp/SMTS4240-52 /bin/sh: line 1: 4348 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP4240-38 > /tmp/SMTS4240-39 /bin/sh: line 1: 4335 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP4240-19 > /tmp/SMTS4240-21 /bin/sh: line 1: 4342 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP4240-74 > /tmp/SMTS4240-77 /bin/sh: line 1: 4363 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP4240-60 > /tmp/SMTS4240-61 /bin/sh: line 1: 4353 Quit (core dumped) z3 -T:4.75 -smt2 /tmp/SMTP4240-18 > /tmp/SMTS4240-20 WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: merge(x,nil()) -> x merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v()))) merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v())) merge(nil(),y) -> y - Signature: {merge/2} / {++/2,nil/0,u/0,v/0} - Obligation: innermost runtime complexity wrt. defined symbols {merge} and constructors {++,nil,u,v} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: merge(x,nil()) -> x merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v()))) merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v())) merge(nil(),y) -> y - Signature: {merge/2} / {++/2,nil/0,u/0,v/0} - Obligation: innermost runtime complexity wrt. defined symbols {merge} and constructors {++,nil,u,v} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: merge(x,nil()) -> x merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v()))) merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v())) merge(nil(),y) -> y - Signature: {merge/2} / {++/2,nil/0,u/0,v/0} - Obligation: innermost runtime complexity wrt. defined symbols {merge} and constructors {++,nil,u,v} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: merge(y,++(u(),v())){y -> ++(x,y)} = merge(++(x,y),++(u(),v())) ->^+ ++(x,merge(y,++(u(),v()))) = C[merge(y,++(u(),v())) = merge(y,++(u(),v())){}] ** Step 1.b:1: Bounds. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: merge(x,nil()) -> x merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v()))) merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v())) merge(nil(),y) -> y - Signature: {merge/2} / {++/2,nil/0,u/0,v/0} - Obligation: innermost runtime complexity wrt. defined symbols {merge} and constructors {++,nil,u,v} + Applied Processor: Bounds {initialAutomaton = minimal, enrichment = match} + Details: The problem is match-bounded by 1. The enriched problem is compatible with follwoing automaton. ++_0(2,2) -> 1 ++_0(2,2) -> 2 ++_1(2,2) -> 8 ++_1(2,3) -> 1 ++_1(2,3) -> 3 ++_1(5,6) -> 3 ++_1(5,6) -> 4 ++_1(5,7) -> 1 ++_1(5,7) -> 3 merge_0(2,2) -> 1 merge_1(2,4) -> 3 merge_1(8,6) -> 7 nil_0() -> 1 nil_0() -> 2 u_0() -> 1 u_0() -> 2 u_1() -> 5 v_0() -> 1 v_0() -> 2 v_1() -> 6 2 -> 1 4 -> 3 ** Step 1.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: merge(x,nil()) -> x merge(++(x,y),++(u(),v())) -> ++(x,merge(y,++(u(),v()))) merge(++(x,y),++(u(),v())) -> ++(u(),merge(++(x,y),v())) merge(nil(),y) -> y - Signature: {merge/2} / {++/2,nil/0,u/0,v/0} - Obligation: innermost runtime complexity wrt. defined symbols {merge} and constructors {++,nil,u,v} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))