/bin/sh: line 1: 60088 Quit (core dumped) z3 -T:4.75 -smt2 /tmp/SMTP59968-44 > /tmp/SMTS59968-45 /bin/sh: line 1: 60094 Quit (core dumped) z3 -T:2.8499999999999996 -smt2 /tmp/SMTP59968-30 > /tmp/SMTS59968-31 /bin/sh: line 1: 60131 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP59968-16 > /tmp/SMTS59968-17 /bin/sh: line 1: 60100 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP59968-92 > /tmp/SMTS59968-93 /bin/sh: line 1: 60123 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP59968-64 > /tmp/SMTS59968-65 /bin/sh: line 1: 60119 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP59968-34 > /tmp/SMTS59968-35 WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: f(.(.(x,y),z)) -> f(.(x,.(y,z))) f(.(nil(),y)) -> .(nil(),f(y)) f(nil()) -> nil() g(.(x,.(y,z))) -> g(.(.(x,y),z)) g(.(x,nil())) -> .(g(x),nil()) g(nil()) -> nil() - Signature: {f/1,g/1} / {./2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {.,nil} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: f(.(.(x,y),z)) -> f(.(x,.(y,z))) f(.(nil(),y)) -> .(nil(),f(y)) f(nil()) -> nil() g(.(x,.(y,z))) -> g(.(.(x,y),z)) g(.(x,nil())) -> .(g(x),nil()) g(nil()) -> nil() - Signature: {f/1,g/1} / {./2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {.,nil} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: f(.(.(x,y),z)) -> f(.(x,.(y,z))) f(.(nil(),y)) -> .(nil(),f(y)) f(nil()) -> nil() g(.(x,.(y,z))) -> g(.(.(x,y),z)) g(.(x,nil())) -> .(g(x),nil()) g(nil()) -> nil() - Signature: {f/1,g/1} / {./2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {.,nil} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: f(.(x,z)){x -> .(x,y)} = f(.(.(x,y),z)) ->^+ f(.(x,.(y,z))) = C[f(.(x,.(y,z))) = f(.(x,z)){z -> .(y,z)}] ** Step 1.b:1: Bounds. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(.(.(x,y),z)) -> f(.(x,.(y,z))) f(.(nil(),y)) -> .(nil(),f(y)) f(nil()) -> nil() g(.(x,.(y,z))) -> g(.(.(x,y),z)) g(.(x,nil())) -> .(g(x),nil()) g(nil()) -> nil() - Signature: {f/1,g/1} / {./2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {.,nil} + 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) -> 2 ._1(2,2) -> 4 ._1(2,3) -> 3 ._1(2,4) -> 3 ._1(4,2) -> 7 ._1(5,6) -> 1 ._1(5,6) -> 5 ._1(6,6) -> 6 ._1(7,2) -> 7 f_0(2) -> 1 f_1(2) -> 6 f_1(3) -> 1 f_1(3) -> 6 f_1(4) -> 6 g_0(2) -> 1 g_1(2) -> 5 g_1(4) -> 5 g_1(7) -> 1 g_1(7) -> 5 nil_0() -> 2 nil_1() -> 1 nil_1() -> 5 nil_1() -> 6 ** Step 1.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: f(.(.(x,y),z)) -> f(.(x,.(y,z))) f(.(nil(),y)) -> .(nil(),f(y)) f(nil()) -> nil() g(.(x,.(y,z))) -> g(.(.(x,y),z)) g(.(x,nil())) -> .(g(x),nil()) g(nil()) -> nil() - Signature: {f/1,g/1} / {./2,nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g} and constructors {.,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))