/bin/sh: line 1: 64137 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP63957-64 > /tmp/SMTS63957-65 /bin/sh: line 1: 64141 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP63957-19 > /tmp/SMTS63957-20 /bin/sh: line 1: 64155 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP63957-68 > /tmp/SMTS63957-69 /bin/sh: line 1: 64162 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP63957-60 > /tmp/SMTS63957-61 /bin/sh: line 1: 64132 Quit (core dumped) z3 -T:14.25 -smt2 /tmp/SMTP63957-62 > /tmp/SMTS63957-63 WORST_CASE(?,O(n^1)) * Step 1: Sum. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: p(m,n,s(r)) -> p(m,r,n) p(m,0(),0()) -> m p(m,s(n),0()) -> p(0(),n,m) - Signature: {p/3} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {p} and constructors {0,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. MAYBE + Considered Problem: - Strict TRS: p(m,n,s(r)) -> p(m,r,n) p(m,0(),0()) -> m p(m,s(n),0()) -> p(0(),n,m) - Signature: {p/3} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {p} and constructors {0,s} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: Ara. MAYBE + Considered Problem: - Strict TRS: p(m,n,s(r)) -> p(m,r,n) p(m,0(),0()) -> m p(m,s(n),0()) -> p(0(),n,m) - Signature: {p/3} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {p} and constructors {0,s} + Applied Processor: Ara {minDegree = 1, maxDegree = 3, araTimeout = 15, araRuleShifting = Just 1, isBestCase = True, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "0") :: [] -(0)-> "A"(1) F (TrsFun "0") :: [] -(0)-> "A"(0) F (TrsFun "main") :: ["A"(0) x "A"(1) x "A"(1)] -(1)-> "A"(0) F (TrsFun "p") :: ["A"(0) x "A"(1) x "A"(1)] -(1)-> "A"(0) F (TrsFun "s") :: ["A"(1)] -(1)-> "A"(1) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: p(m,n,s(r)) -> p(m,r,n) p(m,0(),0()) -> m p(m,s(n),0()) -> p(0(),n,m) main(x1,x2,x3) -> p(x1,x2,x3) 2. Weak: ** Step 1.b:1: Ara. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: p(m,n,s(r)) -> p(m,r,n) p(m,0(),0()) -> m p(m,s(n),0()) -> p(0(),n,m) - Signature: {p/3} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {p} and constructors {0,s} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "0") :: [] -(0)-> "A"(1) F (TrsFun "p") :: ["A"(1) x "A"(1) x "A"(1)] -(1)-> "A"(0) F (TrsFun "s") :: ["A"(1)] -(1)-> "A"(1) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: p(m,n,s(r)) -> p(m,r,n) p(m,0(),0()) -> m p(m,s(n),0()) -> p(0(),n,m) 2. Weak: WORST_CASE(?,O(n^1))