WORST_CASE(?,O(n^1))
proof of input_NTbBonChVO.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
(3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CdtProblem
(5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CdtProblem
(9) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
(10) CdtProblem
(11) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms]
(12) CdtProblem
(13) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CdtProblem
(15) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(16) CpxRelTRS
(17) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(18) CpxWeightedTrs
(19) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(20) CpxTypedWeightedTrs
(21) CompletionProof [UPPER BOUND(ID), 0 ms]
(22) CpxTypedWeightedCompleteTrs
(23) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
(24) CpxTypedWeightedCompleteTrs
(25) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
(26) CpxRNTS
(27) SimplificationProof [BOTH BOUNDS(ID, ID), 1 ms]
(28) CpxRNTS
(29) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
(30) CpxRNTS
(31) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(32) CpxRNTS
(33) IntTrsBoundProof [UPPER BOUND(ID), 261 ms]
(34) CpxRNTS
(35) IntTrsBoundProof [UPPER BOUND(ID), 15 ms]
(36) CpxRNTS
(37) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(38) CpxRNTS
(39) IntTrsBoundProof [UPPER BOUND(ID), 120 ms]
(40) CpxRNTS
(41) IntTrsBoundProof [UPPER BOUND(ID), 105 ms]
(42) CpxRNTS
(43) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(44) CpxRNTS
(45) IntTrsBoundProof [UPPER BOUND(ID), 58 ms]
(46) CpxRNTS
(47) IntTrsBoundProof [UPPER BOUND(ID), 14 ms]
(48) CpxRNTS
(49) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(50) CpxRNTS
(51) IntTrsBoundProof [UPPER BOUND(ID), 106 ms]
(52) CpxRNTS
(53) IntTrsBoundProof [UPPER BOUND(ID), 4 ms]
(54) CpxRNTS
(55) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(56) CpxRNTS
(57) IntTrsBoundProof [UPPER BOUND(ID), 240 ms]
(58) CpxRNTS
(59) IntTrsBoundProof [UPPER BOUND(ID), 53 ms]
(60) CpxRNTS
(61) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(62) CpxRNTS
(63) IntTrsBoundProof [UPPER BOUND(ID), 309 ms]
(64) CpxRNTS
(65) IntTrsBoundProof [UPPER BOUND(ID), 104 ms]
(66) CpxRNTS
(67) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(68) CpxRNTS
(69) IntTrsBoundProof [UPPER BOUND(ID), 218 ms]
(70) CpxRNTS
(71) IntTrsBoundProof [UPPER BOUND(ID), 115 ms]
(72) CpxRNTS
(73) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(74) CpxRNTS
(75) IntTrsBoundProof [UPPER BOUND(ID), 421 ms]
(76) CpxRNTS
(77) IntTrsBoundProof [UPPER BOUND(ID), 156 ms]
(78) CpxRNTS
(79) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(80) CpxRNTS
(81) IntTrsBoundProof [UPPER BOUND(ID), 197 ms]
(82) CpxRNTS
(83) IntTrsBoundProof [UPPER BOUND(ID), 62 ms]
(84) CpxRNTS
(85) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(86) CpxRNTS
(87) IntTrsBoundProof [UPPER BOUND(ID), 218 ms]
(88) CpxRNTS
(89) IntTrsBoundProof [UPPER BOUND(ID), 95 ms]
(90) CpxRNTS
(91) FinalProof [FINISHED, 0 ms]
(92) BOUNDS(1, n^1)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

   if(true, t, e) -> t
   if(false, t, e) -> e
   member(x, nil) -> false
   member(x, cons(y, ys)) -> if(eq(x, y), true, member(x, ys))
   eq(nil, nil) -> true
   eq(O(x), 0(y)) -> eq(x, y)
   eq(0(x), 1(y)) -> false
   eq(1(x), 0(y)) -> false
   eq(1(x), 1(y)) -> eq(x, y)
   negate(0(x)) -> 1(x)
   negate(1(x)) -> 0(x)
   choice(cons(x, xs)) -> x
   choice(cons(x, xs)) -> choice(xs)
   guess(nil) -> nil
   guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf))
   verify(nil) -> true
   verify(cons(l, ls)) -> if(member(negate(l), ls), false, verify(ls))
   sat(cnf) -> satck(cnf, guess(cnf))
   satck(cnf, assign) -> if(verify(assign), assign, unsat)

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   member(z0, nil) -> false
   member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2))
   eq(nil, nil) -> true
   eq(O(z0), 0(z1)) -> eq(z0, z1)
   eq(0(z0), 1(z1)) -> false
   eq(1(z0), 0(z1)) -> false
   eq(1(z0), 1(z1)) -> eq(z0, z1)
   negate(0(z0)) -> 1(z0)
   negate(1(z0)) -> 0(z0)
   choice(cons(z0, z1)) -> z0
   choice(cons(z0, z1)) -> choice(z1)
   guess(nil) -> nil
   guess(cons(z0, z1)) -> cons(choice(z0), guess(z1))
   verify(nil) -> true
   verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1))
   sat(z0) -> satck(z0, guess(z0))
   satck(z0, z1) -> if(verify(z1), z1, unsat)
Tuples:
   IF(true, z0, z1) -> c
   IF(false, z0, z1) -> c1
   MEMBER(z0, nil) -> c2
   MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2))
   EQ(nil, nil) -> c5
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(0(z0), 1(z1)) -> c7
   EQ(1(z0), 0(z1)) -> c8
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   NEGATE(0(z0)) -> c10
   NEGATE(1(z0)) -> c11
   CHOICE(cons(z0, z1)) -> c12
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(nil) -> c14
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   VERIFY(nil) -> c17
   VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0))
   VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1))
   SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0))
   SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1))
S tuples:
   IF(true, z0, z1) -> c
   IF(false, z0, z1) -> c1
   MEMBER(z0, nil) -> c2
   MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2))
   EQ(nil, nil) -> c5
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(0(z0), 1(z1)) -> c7
   EQ(1(z0), 0(z1)) -> c8
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   NEGATE(0(z0)) -> c10
   NEGATE(1(z0)) -> c11
   CHOICE(cons(z0, z1)) -> c12
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(nil) -> c14
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   VERIFY(nil) -> c17
   VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0))
   VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1))
   SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0))
   SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1))
K tuples:none
Defined Rule Symbols:   if_3, member_2, eq_2, negate_1, choice_1, guess_1, verify_1, sat_1, satck_2

Defined Pair Symbols:   IF_3, MEMBER_2, EQ_2, NEGATE_1, CHOICE_1, GUESS_1, VERIFY_1, SAT_1, SATCK_2

Compound Symbols:   c, c1, c2, c3_2, c4_2, c5, c6_1, c7, c8, c9_1, c10, c11, c12, c13_1, c14, c15_1, c16_1, c17, c18_3, c19_2, c20_2, c21_2


----------------------------------------

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
Removed 11 trailing nodes:
   CHOICE(cons(z0, z1)) -> c12
   IF(true, z0, z1) -> c
   VERIFY(nil) -> c17
   EQ(0(z0), 1(z1)) -> c7
   MEMBER(z0, nil) -> c2
   EQ(1(z0), 0(z1)) -> c8
   EQ(nil, nil) -> c5
   IF(false, z0, z1) -> c1
   GUESS(nil) -> c14
   NEGATE(0(z0)) -> c10
   NEGATE(1(z0)) -> c11

----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   member(z0, nil) -> false
   member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2))
   eq(nil, nil) -> true
   eq(O(z0), 0(z1)) -> eq(z0, z1)
   eq(0(z0), 1(z1)) -> false
   eq(1(z0), 0(z1)) -> false
   eq(1(z0), 1(z1)) -> eq(z0, z1)
   negate(0(z0)) -> 1(z0)
   negate(1(z0)) -> 0(z0)
   choice(cons(z0, z1)) -> z0
   choice(cons(z0, z1)) -> choice(z1)
   guess(nil) -> nil
   guess(cons(z0, z1)) -> cons(choice(z0), guess(z1))
   verify(nil) -> true
   verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1))
   sat(z0) -> satck(z0, guess(z0))
   satck(z0, z1) -> if(verify(z1), z1, unsat)
Tuples:
   MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2))
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0))
   VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1))
   SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0))
   SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1))
S tuples:
   MEMBER(z0, cons(z1, z2)) -> c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(IF(eq(z0, z1), true, member(z0, z2)), MEMBER(z0, z2))
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   VERIFY(cons(z0, z1)) -> c18(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0))
   VERIFY(cons(z0, z1)) -> c19(IF(member(negate(z0), z1), false, verify(z1)), VERIFY(z1))
   SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0))
   SATCK(z0, z1) -> c21(IF(verify(z1), z1, unsat), VERIFY(z1))
K tuples:none
Defined Rule Symbols:   if_3, member_2, eq_2, negate_1, choice_1, guess_1, verify_1, sat_1, satck_2

Defined Pair Symbols:   MEMBER_2, EQ_2, CHOICE_1, GUESS_1, VERIFY_1, SAT_1, SATCK_2

Compound Symbols:   c3_2, c4_2, c6_1, c9_1, c13_1, c15_1, c16_1, c18_3, c19_2, c20_2, c21_2


----------------------------------------

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 6 trailing tuple parts
----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   member(z0, nil) -> false
   member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2))
   eq(nil, nil) -> true
   eq(O(z0), 0(z1)) -> eq(z0, z1)
   eq(0(z0), 1(z1)) -> false
   eq(1(z0), 0(z1)) -> false
   eq(1(z0), 1(z1)) -> eq(z0, z1)
   negate(0(z0)) -> 1(z0)
   negate(1(z0)) -> 0(z0)
   choice(cons(z0, z1)) -> z0
   choice(cons(z0, z1)) -> choice(z1)
   guess(nil) -> nil
   guess(cons(z0, z1)) -> cons(choice(z0), guess(z1))
   verify(nil) -> true
   verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1))
   sat(z0) -> satck(z0, guess(z0))
   satck(z0, z1) -> if(verify(z1), z1, unsat)
Tuples:
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0))
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2))
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1))
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1))
   SATCK(z0, z1) -> c21(VERIFY(z1))
S tuples:
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   SAT(z0) -> c20(SATCK(z0, guess(z0)), GUESS(z0))
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2))
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1))
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1))
   SATCK(z0, z1) -> c21(VERIFY(z1))
K tuples:none
Defined Rule Symbols:   if_3, member_2, eq_2, negate_1, choice_1, guess_1, verify_1, sat_1, satck_2

Defined Pair Symbols:   EQ_2, CHOICE_1, GUESS_1, SAT_1, MEMBER_2, VERIFY_1, SATCK_2

Compound Symbols:   c6_1, c9_1, c13_1, c15_1, c16_1, c20_2, c3_1, c4_1, c18_1, c19_1, c21_1


----------------------------------------

(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
Split RHS of tuples not part of any SCC
----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   member(z0, nil) -> false
   member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2))
   eq(nil, nil) -> true
   eq(O(z0), 0(z1)) -> eq(z0, z1)
   eq(0(z0), 1(z1)) -> false
   eq(1(z0), 0(z1)) -> false
   eq(1(z0), 1(z1)) -> eq(z0, z1)
   negate(0(z0)) -> 1(z0)
   negate(1(z0)) -> 0(z0)
   choice(cons(z0, z1)) -> z0
   choice(cons(z0, z1)) -> choice(z1)
   guess(nil) -> nil
   guess(cons(z0, z1)) -> cons(choice(z0), guess(z1))
   verify(nil) -> true
   verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1))
   sat(z0) -> satck(z0, guess(z0))
   satck(z0, z1) -> if(verify(z1), z1, unsat)
Tuples:
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2))
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1))
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1))
   SATCK(z0, z1) -> c21(VERIFY(z1))
   SAT(z0) -> c(SATCK(z0, guess(z0)))
   SAT(z0) -> c(GUESS(z0))
S tuples:
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2))
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1))
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1))
   SATCK(z0, z1) -> c21(VERIFY(z1))
   SAT(z0) -> c(SATCK(z0, guess(z0)))
   SAT(z0) -> c(GUESS(z0))
K tuples:none
Defined Rule Symbols:   if_3, member_2, eq_2, negate_1, choice_1, guess_1, verify_1, sat_1, satck_2

Defined Pair Symbols:   EQ_2, CHOICE_1, GUESS_1, MEMBER_2, VERIFY_1, SATCK_2, SAT_1

Compound Symbols:   c6_1, c9_1, c13_1, c15_1, c16_1, c3_1, c4_1, c18_1, c19_1, c21_1, c_1


----------------------------------------

(9) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   SAT(z0) -> c(GUESS(z0))

----------------------------------------

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   member(z0, nil) -> false
   member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2))
   eq(nil, nil) -> true
   eq(O(z0), 0(z1)) -> eq(z0, z1)
   eq(0(z0), 1(z1)) -> false
   eq(1(z0), 0(z1)) -> false
   eq(1(z0), 1(z1)) -> eq(z0, z1)
   negate(0(z0)) -> 1(z0)
   negate(1(z0)) -> 0(z0)
   choice(cons(z0, z1)) -> z0
   choice(cons(z0, z1)) -> choice(z1)
   guess(nil) -> nil
   guess(cons(z0, z1)) -> cons(choice(z0), guess(z1))
   verify(nil) -> true
   verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1))
   sat(z0) -> satck(z0, guess(z0))
   satck(z0, z1) -> if(verify(z1), z1, unsat)
Tuples:
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2))
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1))
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1))
   SATCK(z0, z1) -> c21(VERIFY(z1))
   SAT(z0) -> c(SATCK(z0, guess(z0)))
S tuples:
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2))
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1))
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1))
   SATCK(z0, z1) -> c21(VERIFY(z1))
   SAT(z0) -> c(SATCK(z0, guess(z0)))
K tuples:none
Defined Rule Symbols:   if_3, member_2, eq_2, negate_1, choice_1, guess_1, verify_1, sat_1, satck_2

Defined Pair Symbols:   EQ_2, CHOICE_1, GUESS_1, MEMBER_2, VERIFY_1, SATCK_2, SAT_1

Compound Symbols:   c6_1, c9_1, c13_1, c15_1, c16_1, c3_1, c4_1, c18_1, c19_1, c21_1, c_1


----------------------------------------

(11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
The following tuples could be moved from S to K by knowledge propagation:
   SAT(z0) -> c(SATCK(z0, guess(z0)))
   SATCK(z0, z1) -> c21(VERIFY(z1))

----------------------------------------

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   member(z0, nil) -> false
   member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2))
   eq(nil, nil) -> true
   eq(O(z0), 0(z1)) -> eq(z0, z1)
   eq(0(z0), 1(z1)) -> false
   eq(1(z0), 0(z1)) -> false
   eq(1(z0), 1(z1)) -> eq(z0, z1)
   negate(0(z0)) -> 1(z0)
   negate(1(z0)) -> 0(z0)
   choice(cons(z0, z1)) -> z0
   choice(cons(z0, z1)) -> choice(z1)
   guess(nil) -> nil
   guess(cons(z0, z1)) -> cons(choice(z0), guess(z1))
   verify(nil) -> true
   verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1))
   sat(z0) -> satck(z0, guess(z0))
   satck(z0, z1) -> if(verify(z1), z1, unsat)
Tuples:
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2))
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1))
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1))
   SATCK(z0, z1) -> c21(VERIFY(z1))
   SAT(z0) -> c(SATCK(z0, guess(z0)))
S tuples:
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2))
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1))
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1))
K tuples:
   SAT(z0) -> c(SATCK(z0, guess(z0)))
   SATCK(z0, z1) -> c21(VERIFY(z1))
Defined Rule Symbols:   if_3, member_2, eq_2, negate_1, choice_1, guess_1, verify_1, sat_1, satck_2

Defined Pair Symbols:   EQ_2, CHOICE_1, GUESS_1, MEMBER_2, VERIFY_1, SATCK_2, SAT_1

Compound Symbols:   c6_1, c9_1, c13_1, c15_1, c16_1, c3_1, c4_1, c18_1, c19_1, c21_1, c_1


----------------------------------------

(13) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   if(true, z0, z1) -> z0
   if(false, z0, z1) -> z1
   member(z0, nil) -> false
   member(z0, cons(z1, z2)) -> if(eq(z0, z1), true, member(z0, z2))
   eq(nil, nil) -> true
   eq(O(z0), 0(z1)) -> eq(z0, z1)
   eq(0(z0), 1(z1)) -> false
   eq(1(z0), 0(z1)) -> false
   eq(1(z0), 1(z1)) -> eq(z0, z1)
   verify(nil) -> true
   verify(cons(z0, z1)) -> if(member(negate(z0), z1), false, verify(z1))
   sat(z0) -> satck(z0, guess(z0))
   satck(z0, z1) -> if(verify(z1), z1, unsat)

----------------------------------------

(14)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   negate(0(z0)) -> 1(z0)
   negate(1(z0)) -> 0(z0)
   guess(nil) -> nil
   guess(cons(z0, z1)) -> cons(choice(z0), guess(z1))
   choice(cons(z0, z1)) -> z0
   choice(cons(z0, z1)) -> choice(z1)
Tuples:
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2))
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1))
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1))
   SATCK(z0, z1) -> c21(VERIFY(z1))
   SAT(z0) -> c(SATCK(z0, guess(z0)))
S tuples:
   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2))
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1))
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1))
K tuples:
   SAT(z0) -> c(SATCK(z0, guess(z0)))
   SATCK(z0, z1) -> c21(VERIFY(z1))
Defined Rule Symbols:   negate_1, guess_1, choice_1

Defined Pair Symbols:   EQ_2, CHOICE_1, GUESS_1, MEMBER_2, VERIFY_1, SATCK_2, SAT_1

Compound Symbols:   c6_1, c9_1, c13_1, c15_1, c16_1, c3_1, c4_1, c18_1, c19_1, c21_1, c_1


----------------------------------------

(15) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(16)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1))
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1))
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1))
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0))
   GUESS(cons(z0, z1)) -> c16(GUESS(z1))
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1))
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2))
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1))
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1))

The (relative) TRS S consists of the following rules:

   SATCK(z0, z1) -> c21(VERIFY(z1))
   SAT(z0) -> c(SATCK(z0, guess(z0)))
   negate(0(z0)) -> 1(z0)
   negate(1(z0)) -> 0(z0)
   guess(nil) -> nil
   guess(cons(z0, z1)) -> cons(choice(z0), guess(z1))
   choice(cons(z0, z1)) -> z0
   choice(cons(z0, z1)) -> choice(z1)

Rewrite Strategy: INNERMOST
----------------------------------------

(17) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

(18)
Obligation:
The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) [1]
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) [1]
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) [1]
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) [1]
   GUESS(cons(z0, z1)) -> c16(GUESS(z1)) [1]
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1)) [1]
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2)) [1]
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1)) [1]
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1)) [1]
   SATCK(z0, z1) -> c21(VERIFY(z1)) [0]
   SAT(z0) -> c(SATCK(z0, guess(z0))) [0]
   negate(0(z0)) -> 1(z0) [0]
   negate(1(z0)) -> 0(z0) [0]
   guess(nil) -> nil [0]
   guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) [0]
   choice(cons(z0, z1)) -> z0 [0]
   choice(cons(z0, z1)) -> choice(z1) [0]

Rewrite Strategy: INNERMOST
----------------------------------------

(19) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(20)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) [1]
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) [1]
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) [1]
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) [1]
   GUESS(cons(z0, z1)) -> c16(GUESS(z1)) [1]
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1)) [1]
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2)) [1]
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1)) [1]
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1)) [1]
   SATCK(z0, z1) -> c21(VERIFY(z1)) [0]
   SAT(z0) -> c(SATCK(z0, guess(z0))) [0]
   negate(0(z0)) -> 1(z0) [0]
   negate(1(z0)) -> 0(z0) [0]
   guess(nil) -> nil [0]
   guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) [0]
   choice(cons(z0, z1)) -> z0 [0]
   choice(cons(z0, z1)) -> choice(z1) [0]

The TRS has the following type information:
EQ :: O:0:1:cons:nil -> O:0:1:cons:nil -> c6:c9
O :: O:0:1:cons:nil -> O:0:1:cons:nil
0 :: O:0:1:cons:nil -> O:0:1:cons:nil
c6 :: c6:c9 -> c6:c9
1 :: O:0:1:cons:nil -> O:0:1:cons:nil
c9 :: c6:c9 -> c6:c9
CHOICE :: O:0:1:cons:nil -> c13
cons :: O:0:1:cons:nil -> O:0:1:cons:nil -> O:0:1:cons:nil
c13 :: c13 -> c13
GUESS :: O:0:1:cons:nil -> c15:c16
c15 :: c13 -> c15:c16
c16 :: c15:c16 -> c15:c16
MEMBER :: O:0:1:cons:nil -> O:0:1:cons:nil -> c3:c4
c3 :: c6:c9 -> c3:c4
c4 :: c3:c4 -> c3:c4
VERIFY :: O:0:1:cons:nil -> c18:c19
c18 :: c3:c4 -> c18:c19
negate :: O:0:1:cons:nil -> O:0:1:cons:nil
c19 :: c18:c19 -> c18:c19
SATCK :: O:0:1:cons:nil -> O:0:1:cons:nil -> c21
c21 :: c18:c19 -> c21
SAT :: O:0:1:cons:nil -> c
c :: c21 -> c
guess :: O:0:1:cons:nil -> O:0:1:cons:nil
nil :: O:0:1:cons:nil
choice :: O:0:1:cons:nil -> O:0:1:cons:nil

Rewrite Strategy: INNERMOST
----------------------------------------

(21) CompletionProof (UPPER BOUND(ID))
The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

   EQ_2
   CHOICE_1
   GUESS_1
   MEMBER_2
   VERIFY_1

(c) The following functions are completely defined:

   SATCK_2
   SAT_1
   negate_1
   guess_1
   choice_1

Due to the following rules being added:

   SATCK(v0, v1) -> const5 [0]
   SAT(v0) -> const6 [0]
   negate(v0) -> nil [0]
   guess(v0) -> nil [0]
   choice(v0) -> nil [0]

And the following fresh constants:    const5, const6, const, const1, const2, const3, const4

----------------------------------------

(22)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) [1]
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) [1]
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) [1]
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) [1]
   GUESS(cons(z0, z1)) -> c16(GUESS(z1)) [1]
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1)) [1]
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2)) [1]
   VERIFY(cons(z0, z1)) -> c18(MEMBER(negate(z0), z1)) [1]
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1)) [1]
   SATCK(z0, z1) -> c21(VERIFY(z1)) [0]
   SAT(z0) -> c(SATCK(z0, guess(z0))) [0]
   negate(0(z0)) -> 1(z0) [0]
   negate(1(z0)) -> 0(z0) [0]
   guess(nil) -> nil [0]
   guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) [0]
   choice(cons(z0, z1)) -> z0 [0]
   choice(cons(z0, z1)) -> choice(z1) [0]
   SATCK(v0, v1) -> const5 [0]
   SAT(v0) -> const6 [0]
   negate(v0) -> nil [0]
   guess(v0) -> nil [0]
   choice(v0) -> nil [0]

The TRS has the following type information:
EQ :: O:0:1:cons:nil -> O:0:1:cons:nil -> c6:c9
O :: O:0:1:cons:nil -> O:0:1:cons:nil
0 :: O:0:1:cons:nil -> O:0:1:cons:nil
c6 :: c6:c9 -> c6:c9
1 :: O:0:1:cons:nil -> O:0:1:cons:nil
c9 :: c6:c9 -> c6:c9
CHOICE :: O:0:1:cons:nil -> c13
cons :: O:0:1:cons:nil -> O:0:1:cons:nil -> O:0:1:cons:nil
c13 :: c13 -> c13
GUESS :: O:0:1:cons:nil -> c15:c16
c15 :: c13 -> c15:c16
c16 :: c15:c16 -> c15:c16
MEMBER :: O:0:1:cons:nil -> O:0:1:cons:nil -> c3:c4
c3 :: c6:c9 -> c3:c4
c4 :: c3:c4 -> c3:c4
VERIFY :: O:0:1:cons:nil -> c18:c19
c18 :: c3:c4 -> c18:c19
negate :: O:0:1:cons:nil -> O:0:1:cons:nil
c19 :: c18:c19 -> c18:c19
SATCK :: O:0:1:cons:nil -> O:0:1:cons:nil -> c21:const5
c21 :: c18:c19 -> c21:const5
SAT :: O:0:1:cons:nil -> c:const6
c :: c21:const5 -> c:const6
guess :: O:0:1:cons:nil -> O:0:1:cons:nil
nil :: O:0:1:cons:nil
choice :: O:0:1:cons:nil -> O:0:1:cons:nil
const5 :: c21:const5
const6 :: c:const6
const :: c6:c9
const1 :: c13
const2 :: c15:c16
const3 :: c3:c4
const4 :: c18:c19

Rewrite Strategy: INNERMOST
----------------------------------------

(23) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

(24)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   EQ(O(z0), 0(z1)) -> c6(EQ(z0, z1)) [1]
   EQ(1(z0), 1(z1)) -> c9(EQ(z0, z1)) [1]
   CHOICE(cons(z0, z1)) -> c13(CHOICE(z1)) [1]
   GUESS(cons(z0, z1)) -> c15(CHOICE(z0)) [1]
   GUESS(cons(z0, z1)) -> c16(GUESS(z1)) [1]
   MEMBER(z0, cons(z1, z2)) -> c3(EQ(z0, z1)) [1]
   MEMBER(z0, cons(z1, z2)) -> c4(MEMBER(z0, z2)) [1]
   VERIFY(cons(0(z0'), z1)) -> c18(MEMBER(1(z0'), z1)) [1]
   VERIFY(cons(1(z0''), z1)) -> c18(MEMBER(0(z0''), z1)) [1]
   VERIFY(cons(z0, z1)) -> c18(MEMBER(nil, z1)) [1]
   VERIFY(cons(z0, z1)) -> c19(VERIFY(z1)) [1]
   SATCK(z0, z1) -> c21(VERIFY(z1)) [0]
   SAT(nil) -> c(SATCK(nil, nil)) [0]
   SAT(cons(z01, z1')) -> c(SATCK(cons(z01, z1'), cons(choice(z01), guess(z1')))) [0]
   SAT(z0) -> c(SATCK(z0, nil)) [0]
   negate(0(z0)) -> 1(z0) [0]
   negate(1(z0)) -> 0(z0) [0]
   guess(nil) -> nil [0]
   guess(cons(z0, z1)) -> cons(choice(z0), guess(z1)) [0]
   choice(cons(z0, z1)) -> z0 [0]
   choice(cons(z0, z1)) -> choice(z1) [0]
   SATCK(v0, v1) -> const5 [0]
   SAT(v0) -> const6 [0]
   negate(v0) -> nil [0]
   guess(v0) -> nil [0]
   choice(v0) -> nil [0]

The TRS has the following type information:
EQ :: O:0:1:cons:nil -> O:0:1:cons:nil -> c6:c9
O :: O:0:1:cons:nil -> O:0:1:cons:nil
0 :: O:0:1:cons:nil -> O:0:1:cons:nil
c6 :: c6:c9 -> c6:c9
1 :: O:0:1:cons:nil -> O:0:1:cons:nil
c9 :: c6:c9 -> c6:c9
CHOICE :: O:0:1:cons:nil -> c13
cons :: O:0:1:cons:nil -> O:0:1:cons:nil -> O:0:1:cons:nil
c13 :: c13 -> c13
GUESS :: O:0:1:cons:nil -> c15:c16
c15 :: c13 -> c15:c16
c16 :: c15:c16 -> c15:c16
MEMBER :: O:0:1:cons:nil -> O:0:1:cons:nil -> c3:c4
c3 :: c6:c9 -> c3:c4
c4 :: c3:c4 -> c3:c4
VERIFY :: O:0:1:cons:nil -> c18:c19
c18 :: c3:c4 -> c18:c19
negate :: O:0:1:cons:nil -> O:0:1:cons:nil
c19 :: c18:c19 -> c18:c19
SATCK :: O:0:1:cons:nil -> O:0:1:cons:nil -> c21:const5
c21 :: c18:c19 -> c21:const5
SAT :: O:0:1:cons:nil -> c:const6
c :: c21:const5 -> c:const6
guess :: O:0:1:cons:nil -> O:0:1:cons:nil
nil :: O:0:1:cons:nil
choice :: O:0:1:cons:nil -> O:0:1:cons:nil
const5 :: c21:const5
const6 :: c:const6
const :: c6:c9
const1 :: c13
const2 :: c15:c16
const3 :: c3:c4
const4 :: c18:c19

Rewrite Strategy: INNERMOST
----------------------------------------

(25) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   nil => 0
   const5 => 0
   const6 => 0
   const => 0
   const1 => 0
   const2 => 0
   const3 => 0
   const4 => 0

----------------------------------------

(26)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ 1 }-> 1 + EQ(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + CHOICE(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z0, z2) :|: z = z0, z1 >= 0, z' = 1 + z1 + z2, z0 >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + EQ(z0, z1) :|: z = z0, z1 >= 0, z' = 1 + z1 + z2, z0 >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   SAT(z) -{ 0 }-> 1 + SATCK(z0, 0) :|: z = z0, z0 >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + choice(z01) + guess(z1')) :|: z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> choice(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   guess(z) -{ 0 }-> 1 + choice(z0) + guess(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   negate(z) -{ 0 }-> 1 + z0 :|: z = 1 + z0, z0 >= 0


----------------------------------------

(27) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

(28)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ 1 }-> 1 + EQ(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + CHOICE(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + EQ(z, z1) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + choice(z01) + guess(z1')) :|: z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> choice(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + choice(z0) + guess(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0


----------------------------------------

(29) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID))
Found the following analysis order by SCC decomposition:

   { choice }
   { EQ }
   { CHOICE }
   { negate }
   { guess }
   { MEMBER }
   { GUESS }
   { VERIFY }
   { SATCK }
   { SAT }

----------------------------------------

(30)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ 1 }-> 1 + EQ(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + CHOICE(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + EQ(z, z1) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + choice(z01) + guess(z1')) :|: z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> choice(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + choice(z0) + guess(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {choice}, {EQ}, {CHOICE}, {negate}, {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}

----------------------------------------

(31) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(32)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ 1 }-> 1 + EQ(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + CHOICE(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + EQ(z, z1) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + choice(z01) + guess(z1')) :|: z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> choice(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + choice(z0) + guess(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {choice}, {EQ}, {CHOICE}, {negate}, {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}

----------------------------------------

(33) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: choice
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z

----------------------------------------

(34)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ 1 }-> 1 + EQ(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + CHOICE(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + EQ(z, z1) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + choice(z01) + guess(z1')) :|: z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> choice(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + choice(z0) + guess(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {choice}, {EQ}, {CHOICE}, {negate}, {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: ?, size: O(n^1) [z]

----------------------------------------

(35) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: choice
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

----------------------------------------

(36)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ 1 }-> 1 + EQ(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + CHOICE(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + EQ(z, z1) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + choice(z01) + guess(z1')) :|: z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> choice(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + choice(z0) + guess(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {EQ}, {CHOICE}, {negate}, {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]

----------------------------------------

(37) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(38)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ 1 }-> 1 + EQ(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + CHOICE(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + EQ(z, z1) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + guess(z1')) :|: s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + guess(z1) :|: s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {EQ}, {CHOICE}, {negate}, {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]

----------------------------------------

(39) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: EQ
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

----------------------------------------

(40)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ 1 }-> 1 + EQ(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + CHOICE(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + EQ(z, z1) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + guess(z1')) :|: s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + guess(z1) :|: s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {EQ}, {CHOICE}, {negate}, {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: ?, size: O(1) [0]

----------------------------------------

(41) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: EQ
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z'

----------------------------------------

(42)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ 1 }-> 1 + EQ(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + CHOICE(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + EQ(z, z1) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + guess(z1')) :|: s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + guess(z1) :|: s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {CHOICE}, {negate}, {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]

----------------------------------------

(43) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(44)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + CHOICE(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + guess(z1')) :|: s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + guess(z1) :|: s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {CHOICE}, {negate}, {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]

----------------------------------------

(45) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: CHOICE
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

----------------------------------------

(46)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + CHOICE(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + guess(z1')) :|: s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + guess(z1) :|: s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {CHOICE}, {negate}, {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: ?, size: O(1) [0]

----------------------------------------

(47) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: CHOICE
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z

----------------------------------------

(48)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + CHOICE(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + guess(z1')) :|: s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + guess(z1) :|: s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {negate}, {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]

----------------------------------------

(49) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(50)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + guess(z1')) :|: s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + guess(z1) :|: s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {negate}, {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]

----------------------------------------

(51) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: negate
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z

----------------------------------------

(52)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + guess(z1')) :|: s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + guess(z1) :|: s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {negate}, {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: ?, size: O(n^1) [z]

----------------------------------------

(53) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: negate
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

----------------------------------------

(54)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + guess(z1')) :|: s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + guess(z1) :|: s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]

----------------------------------------

(55) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(56)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + guess(z1')) :|: s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + guess(z1) :|: s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]

----------------------------------------

(57) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: guess
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z

----------------------------------------

(58)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + guess(z1')) :|: s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + guess(z1) :|: s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {guess}, {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: ?, size: O(n^1) [z]

----------------------------------------

(59) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: guess
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

----------------------------------------

(60)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + guess(z1')) :|: s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + guess(z1) :|: s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]

----------------------------------------

(61) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(62)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + s5) :|: s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]

----------------------------------------

(63) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: MEMBER
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z'

----------------------------------------

(64)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + s5) :|: s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {MEMBER}, {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: ?, size: O(n^1) [z']

----------------------------------------

(65) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: MEMBER
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z'

----------------------------------------

(66)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 }-> 1 + MEMBER(z, z2) :|: z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + s5) :|: s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(0, z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0', z1) :|: z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(1 + z0'', z1) :|: z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']

----------------------------------------

(67) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(68)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 + z2 }-> 1 + s7 :|: s7 >= 0, s7 <= z2, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + s5) :|: s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 + z1 }-> 1 + s10 :|: s10 >= 0, s10 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s8 :|: s8 >= 0, s8 <= z1, z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s9 :|: s9 >= 0, s9 <= z1, z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']

----------------------------------------

(69) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: GUESS
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z

----------------------------------------

(70)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 + z2 }-> 1 + s7 :|: s7 >= 0, s7 <= z2, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + s5) :|: s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 + z1 }-> 1 + s10 :|: s10 >= 0, s10 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s8 :|: s8 >= 0, s8 <= z1, z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s9 :|: s9 >= 0, s9 <= z1, z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {GUESS}, {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']
  GUESS: runtime: ?, size: O(n^1) [z]

----------------------------------------

(71) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: GUESS
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z

----------------------------------------

(72)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 }-> 1 + GUESS(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 + z2 }-> 1 + s7 :|: s7 >= 0, s7 <= z2, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + s5) :|: s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 + z1 }-> 1 + s10 :|: s10 >= 0, s10 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s8 :|: s8 >= 0, s8 <= z1, z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s9 :|: s9 >= 0, s9 <= z1, z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']
  GUESS: runtime: O(n^1) [z], size: O(n^1) [z]

----------------------------------------

(73) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(74)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z1 }-> 1 + s11 :|: s11 >= 0, s11 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 + z2 }-> 1 + s7 :|: s7 >= 0, s7 <= z2, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + s5) :|: s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 + z1 }-> 1 + s10 :|: s10 >= 0, s10 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s8 :|: s8 >= 0, s8 <= z1, z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s9 :|: s9 >= 0, s9 <= z1, z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']
  GUESS: runtime: O(n^1) [z], size: O(n^1) [z]

----------------------------------------

(75) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: VERIFY
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: z

----------------------------------------

(76)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z1 }-> 1 + s11 :|: s11 >= 0, s11 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 + z2 }-> 1 + s7 :|: s7 >= 0, s7 <= z2, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + s5) :|: s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 + z1 }-> 1 + s10 :|: s10 >= 0, s10 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s8 :|: s8 >= 0, s8 <= z1, z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s9 :|: s9 >= 0, s9 <= z1, z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {VERIFY}, {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']
  GUESS: runtime: O(n^1) [z], size: O(n^1) [z]
  VERIFY: runtime: ?, size: O(n^1) [z]

----------------------------------------

(77) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: VERIFY
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + z

----------------------------------------

(78)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z1 }-> 1 + s11 :|: s11 >= 0, s11 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 + z2 }-> 1 + s7 :|: s7 >= 0, s7 <= z2, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + s5) :|: s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 0 }-> 1 + VERIFY(z') :|: z' >= 0, z >= 0
   VERIFY(z) -{ 1 + z1 }-> 1 + s10 :|: s10 >= 0, s10 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s8 :|: s8 >= 0, s8 <= z1, z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s9 :|: s9 >= 0, s9 <= z1, z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']
  GUESS: runtime: O(n^1) [z], size: O(n^1) [z]
  VERIFY: runtime: O(n^1) [1 + z], size: O(n^1) [z]

----------------------------------------

(79) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(80)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z1 }-> 1 + s11 :|: s11 >= 0, s11 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 + z2 }-> 1 + s7 :|: s7 >= 0, s7 <= z2, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + s5) :|: s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 1 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z', z' >= 0, z >= 0
   VERIFY(z) -{ 1 + z1 }-> 1 + s10 :|: s10 >= 0, s10 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 2 + z1 }-> 1 + s12 :|: s12 >= 0, s12 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s8 :|: s8 >= 0, s8 <= z1, z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s9 :|: s9 >= 0, s9 <= z1, z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']
  GUESS: runtime: O(n^1) [z], size: O(n^1) [z]
  VERIFY: runtime: O(n^1) [1 + z], size: O(n^1) [z]

----------------------------------------

(81) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: SATCK
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + z'

----------------------------------------

(82)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z1 }-> 1 + s11 :|: s11 >= 0, s11 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 + z2 }-> 1 + s7 :|: s7 >= 0, s7 <= z2, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + s5) :|: s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 1 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z', z' >= 0, z >= 0
   VERIFY(z) -{ 1 + z1 }-> 1 + s10 :|: s10 >= 0, s10 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 2 + z1 }-> 1 + s12 :|: s12 >= 0, s12 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s8 :|: s8 >= 0, s8 <= z1, z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s9 :|: s9 >= 0, s9 <= z1, z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {SATCK}, {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']
  GUESS: runtime: O(n^1) [z], size: O(n^1) [z]
  VERIFY: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  SATCK: runtime: ?, size: O(n^1) [1 + z']

----------------------------------------

(83) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: SATCK
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + z'

----------------------------------------

(84)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z1 }-> 1 + s11 :|: s11 >= 0, s11 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 + z2 }-> 1 + s7 :|: s7 >= 0, s7 <= z2, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(z, 0) :|: z >= 0
   SAT(z) -{ 0 }-> 1 + SATCK(0, 0) :|: z = 0
   SAT(z) -{ 0 }-> 1 + SATCK(1 + z01 + z1', 1 + s + s5) :|: s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 1 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z', z' >= 0, z >= 0
   VERIFY(z) -{ 1 + z1 }-> 1 + s10 :|: s10 >= 0, s10 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 2 + z1 }-> 1 + s12 :|: s12 >= 0, s12 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s8 :|: s8 >= 0, s8 <= z1, z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s9 :|: s9 >= 0, s9 <= z1, z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']
  GUESS: runtime: O(n^1) [z], size: O(n^1) [z]
  VERIFY: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  SATCK: runtime: O(n^1) [1 + z'], size: O(n^1) [1 + z']

----------------------------------------

(85) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(86)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z1 }-> 1 + s11 :|: s11 >= 0, s11 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 + z2 }-> 1 + s7 :|: s7 >= 0, s7 <= z2, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 1 }-> 1 + s14 :|: s14 >= 0, s14 <= 0 + 1, z = 0
   SAT(z) -{ 2 + s + s5 }-> 1 + s15 :|: s15 >= 0, s15 <= 1 + s + s5 + 1, s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SAT(z) -{ 1 }-> 1 + s16 :|: s16 >= 0, s16 <= 0 + 1, z >= 0
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 1 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z', z' >= 0, z >= 0
   VERIFY(z) -{ 1 + z1 }-> 1 + s10 :|: s10 >= 0, s10 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 2 + z1 }-> 1 + s12 :|: s12 >= 0, s12 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s8 :|: s8 >= 0, s8 <= z1, z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s9 :|: s9 >= 0, s9 <= z1, z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']
  GUESS: runtime: O(n^1) [z], size: O(n^1) [z]
  VERIFY: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  SATCK: runtime: O(n^1) [1 + z'], size: O(n^1) [1 + z']

----------------------------------------

(87) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: SAT
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 2 + z

----------------------------------------

(88)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z1 }-> 1 + s11 :|: s11 >= 0, s11 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 + z2 }-> 1 + s7 :|: s7 >= 0, s7 <= z2, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 1 }-> 1 + s14 :|: s14 >= 0, s14 <= 0 + 1, z = 0
   SAT(z) -{ 2 + s + s5 }-> 1 + s15 :|: s15 >= 0, s15 <= 1 + s + s5 + 1, s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SAT(z) -{ 1 }-> 1 + s16 :|: s16 >= 0, s16 <= 0 + 1, z >= 0
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 1 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z', z' >= 0, z >= 0
   VERIFY(z) -{ 1 + z1 }-> 1 + s10 :|: s10 >= 0, s10 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 2 + z1 }-> 1 + s12 :|: s12 >= 0, s12 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s8 :|: s8 >= 0, s8 <= z1, z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s9 :|: s9 >= 0, s9 <= z1, z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: {SAT}
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']
  GUESS: runtime: O(n^1) [z], size: O(n^1) [z]
  VERIFY: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  SATCK: runtime: O(n^1) [1 + z'], size: O(n^1) [1 + z']
  SAT: runtime: ?, size: O(n^1) [2 + z]

----------------------------------------

(89) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: SAT
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + z

----------------------------------------

(90)
Obligation:
Complexity RNTS consisting of the following rules:

   CHOICE(z) -{ 1 + z1 }-> 1 + s3 :|: s3 >= 0, s3 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ z' }-> 1 + s1 :|: s1 >= 0, s1 <= 0, z' - 1 >= 0, z - 1 >= 0
   GUESS(z) -{ 1 + z1 }-> 1 + s11 :|: s11 >= 0, s11 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   GUESS(z) -{ 1 + z0 }-> 1 + s4 :|: s4 >= 0, s4 <= 0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   MEMBER(z, z') -{ 1 + z1 }-> 1 + s2 :|: s2 >= 0, s2 <= 0, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   MEMBER(z, z') -{ 1 + z2 }-> 1 + s7 :|: s7 >= 0, s7 <= z2, z1 >= 0, z' = 1 + z1 + z2, z >= 0, z2 >= 0
   SAT(z) -{ 0 }-> 0 :|: z >= 0
   SAT(z) -{ 1 }-> 1 + s14 :|: s14 >= 0, s14 <= 0 + 1, z = 0
   SAT(z) -{ 2 + s + s5 }-> 1 + s15 :|: s15 >= 0, s15 <= 1 + s + s5 + 1, s5 >= 0, s5 <= z1', s >= 0, s <= z01, z01 >= 0, z1' >= 0, z = 1 + z01 + z1'
   SAT(z) -{ 1 }-> 1 + s16 :|: s16 >= 0, s16 <= 0 + 1, z >= 0
   SATCK(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   SATCK(z, z') -{ 1 + z' }-> 1 + s13 :|: s13 >= 0, s13 <= z', z' >= 0, z >= 0
   VERIFY(z) -{ 1 + z1 }-> 1 + s10 :|: s10 >= 0, s10 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 2 + z1 }-> 1 + s12 :|: s12 >= 0, s12 <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s8 :|: s8 >= 0, s8 <= z1, z1 >= 0, z0' >= 0, z = 1 + (1 + z0') + z1
   VERIFY(z) -{ 1 + z1 }-> 1 + s9 :|: s9 >= 0, s9 <= z1, z1 >= 0, z = 1 + (1 + z0'') + z1, z0'' >= 0
   choice(z) -{ 0 }-> s'' :|: s'' >= 0, s'' <= z1, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> z0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   choice(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 0 :|: z = 0
   guess(z) -{ 0 }-> 0 :|: z >= 0
   guess(z) -{ 0 }-> 1 + s' + s6 :|: s6 >= 0, s6 <= z1, s' >= 0, s' <= z0, z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   negate(z) -{ 0 }-> 0 :|: z >= 0
   negate(z) -{ 0 }-> 1 + (z - 1) :|: z - 1 >= 0

Function symbols to be analyzed: 
Previous analysis results are:
  choice: runtime: O(1) [0], size: O(n^1) [z]
  EQ: runtime: O(n^1) [z'], size: O(1) [0]
  CHOICE: runtime: O(n^1) [z], size: O(1) [0]
  negate: runtime: O(1) [0], size: O(n^1) [z]
  guess: runtime: O(1) [0], size: O(n^1) [z]
  MEMBER: runtime: O(n^1) [z'], size: O(n^1) [z']
  GUESS: runtime: O(n^1) [z], size: O(n^1) [z]
  VERIFY: runtime: O(n^1) [1 + z], size: O(n^1) [z]
  SATCK: runtime: O(n^1) [1 + z'], size: O(n^1) [1 + z']
  SAT: runtime: O(n^1) [1 + z], size: O(n^1) [2 + z]

----------------------------------------

(91) FinalProof (FINISHED)
Computed overall runtime complexity
----------------------------------------

(92)
BOUNDS(1, n^1)