WORST_CASE(Omega(n^1),O(n^1))
proof of input_Ohid4FwRvN.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^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) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
    (24) CpxRNTS
    (25) CompleteCoflocoProof [FINISHED, 389 ms]
    (26) BOUNDS(1, n^1)
(27) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(28) CdtProblem
    (29) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (30) CpxRelTRS
    (31) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (32) CpxRelTRS
    (33) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (34) typed CpxTrs
    (35) OrderProof [LOWER BOUND(ID), 0 ms]
    (36) typed CpxTrs
    (37) RewriteLemmaProof [LOWER BOUND(ID), 1525 ms]
    (38) typed CpxTrs
    (39) RewriteLemmaProof [LOWER BOUND(ID), 1094 ms]
    (40) BEST
        (41) proven lower bound
            (42) LowerBoundPropagationProof [FINISHED, 0 ms]
            (43) BOUNDS(n^1, INF)
        (44) typed CpxTrs
            (45) RewriteLemmaProof [LOWER BOUND(ID), 106 ms]
            (46) typed CpxTrs
            (47) RewriteLemmaProof [LOWER BOUND(ID), 2031 ms]
            (48) typed CpxTrs
            (49) RewriteLemmaProof [LOWER BOUND(ID), 306 ms]
            (50) BOUNDS(1, INF)


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

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^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:
   IF(true, z0, z1) -> c
   VERIFY(nil) -> c17
   CHOICE(cons(z0, z1)) -> c12
   EQ(1(z0), 0(z1)) -> c8
   MEMBER(z0, nil) -> c2
   IF(false, z0, z1) -> c1
   GUESS(nil) -> c14
   NEGATE(1(z0)) -> c11
   NEGATE(0(z0)) -> c10
   EQ(nil, nil) -> c5
   EQ(0(z0), 1(z1)) -> c7

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

(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 TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   SATCK(v0, v1) -> null_SATCK [0]
   SAT(v0) -> null_SAT [0]
   negate(v0) -> null_negate [0]
   guess(v0) -> null_guess [0]
   choice(v0) -> null_choice [0]
   EQ(v0, v1) -> null_EQ [0]
   CHOICE(v0) -> null_CHOICE [0]
   GUESS(v0) -> null_GUESS [0]
   MEMBER(v0, v1) -> null_MEMBER [0]
   VERIFY(v0) -> null_VERIFY [0]

And the following fresh constants:    null_SATCK, null_SAT, null_negate, null_guess, null_choice, null_EQ, null_CHOICE, null_GUESS, null_MEMBER, null_VERIFY

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

(22)
Obligation:
Runtime Complexity Weighted TRS where all 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) -> null_SATCK [0]
   SAT(v0) -> null_SAT [0]
   negate(v0) -> null_negate [0]
   guess(v0) -> null_guess [0]
   choice(v0) -> null_choice [0]
   EQ(v0, v1) -> null_EQ [0]
   CHOICE(v0) -> null_CHOICE [0]
   GUESS(v0) -> null_GUESS [0]
   MEMBER(v0, v1) -> null_MEMBER [0]
   VERIFY(v0) -> null_VERIFY [0]

The TRS has the following type information:
EQ :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> O:0:1:cons:nil:null_negate:null_guess:null_choice -> c6:c9:null_EQ
O :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> O:0:1:cons:nil:null_negate:null_guess:null_choice
0 :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> O:0:1:cons:nil:null_negate:null_guess:null_choice
c6 :: c6:c9:null_EQ -> c6:c9:null_EQ
1 :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> O:0:1:cons:nil:null_negate:null_guess:null_choice
c9 :: c6:c9:null_EQ -> c6:c9:null_EQ
CHOICE :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> c13:null_CHOICE
cons :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> O:0:1:cons:nil:null_negate:null_guess:null_choice -> O:0:1:cons:nil:null_negate:null_guess:null_choice
c13 :: c13:null_CHOICE -> c13:null_CHOICE
GUESS :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> c15:c16:null_GUESS
c15 :: c13:null_CHOICE -> c15:c16:null_GUESS
c16 :: c15:c16:null_GUESS -> c15:c16:null_GUESS
MEMBER :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> O:0:1:cons:nil:null_negate:null_guess:null_choice -> c3:c4:null_MEMBER
c3 :: c6:c9:null_EQ -> c3:c4:null_MEMBER
c4 :: c3:c4:null_MEMBER -> c3:c4:null_MEMBER
VERIFY :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> c18:c19:null_VERIFY
c18 :: c3:c4:null_MEMBER -> c18:c19:null_VERIFY
negate :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> O:0:1:cons:nil:null_negate:null_guess:null_choice
c19 :: c18:c19:null_VERIFY -> c18:c19:null_VERIFY
SATCK :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> O:0:1:cons:nil:null_negate:null_guess:null_choice -> c21:null_SATCK
c21 :: c18:c19:null_VERIFY -> c21:null_SATCK
SAT :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> c:null_SAT
c :: c21:null_SATCK -> c:null_SAT
guess :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> O:0:1:cons:nil:null_negate:null_guess:null_choice
nil :: O:0:1:cons:nil:null_negate:null_guess:null_choice
choice :: O:0:1:cons:nil:null_negate:null_guess:null_choice -> O:0:1:cons:nil:null_negate:null_guess:null_choice
null_SATCK :: c21:null_SATCK
null_SAT :: c:null_SAT
null_negate :: O:0:1:cons:nil:null_negate:null_guess:null_choice
null_guess :: O:0:1:cons:nil:null_negate:null_guess:null_choice
null_choice :: O:0:1:cons:nil:null_negate:null_guess:null_choice
null_EQ :: c6:c9:null_EQ
null_CHOICE :: c13:null_CHOICE
null_GUESS :: c15:c16:null_GUESS
null_MEMBER :: c3:c4:null_MEMBER
null_VERIFY :: c18:c19:null_VERIFY

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

(23) 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
   null_SATCK => 0
   null_SAT => 0
   null_negate => 0
   null_guess => 0
   null_choice => 0
   null_EQ => 0
   null_CHOICE => 0
   null_GUESS => 0
   null_MEMBER => 0
   null_VERIFY => 0

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

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

   CHOICE(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   CHOICE(z) -{ 1 }-> 1 + CHOICE(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   EQ(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   EQ(z, z') -{ 1 }-> 1 + EQ(z0, z1) :|: z1 >= 0, z = 1 + z0, z0 >= 0, z' = 1 + z1
   GUESS(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   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') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   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, guess(z0)) :|: z = z0, z0 >= 0
   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) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   VERIFY(z) -{ 1 }-> 1 + VERIFY(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   VERIFY(z) -{ 1 }-> 1 + MEMBER(negate(z0), z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1
   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

Only complete derivations are relevant for the runtime complexity.

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

(25) CompleteCoflocoProof (FINISHED)
Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V1, V),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun1(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun2(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun3(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun4(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[fun5(V1, V, Out)],[V1 >= 0,V >= 0]).
eq(start(V1, V),0,[fun6(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[negate(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[guess(V1, Out)],[V1 >= 0]).
eq(start(V1, V),0,[choice(V1, Out)],[V1 >= 0]).
eq(fun(V1, V, Out),1,[fun(V3, V2, Ret1)],[Out = 1 + Ret1,V2 >= 0,V1 = 1 + V3,V3 >= 0,V = 1 + V2]).
eq(fun1(V1, Out),1,[fun1(V4, Ret11)],[Out = 1 + Ret11,V4 >= 0,V5 >= 0,V1 = 1 + V4 + V5]).
eq(fun2(V1, Out),1,[fun1(V7, Ret12)],[Out = 1 + Ret12,V6 >= 0,V7 >= 0,V1 = 1 + V6 + V7]).
eq(fun2(V1, Out),1,[fun2(V9, Ret13)],[Out = 1 + Ret13,V9 >= 0,V8 >= 0,V1 = 1 + V8 + V9]).
eq(fun3(V1, V, Out),1,[fun(V11, V10, Ret14)],[Out = 1 + Ret14,V1 = V11,V10 >= 0,V = 1 + V10 + V12,V11 >= 0,V12 >= 0]).
eq(fun3(V1, V, Out),1,[fun3(V14, V15, Ret15)],[Out = 1 + Ret15,V1 = V14,V13 >= 0,V = 1 + V13 + V15,V14 >= 0,V15 >= 0]).
eq(fun4(V1, Out),1,[negate(V17, Ret10),fun3(Ret10, V16, Ret16)],[Out = 1 + Ret16,V16 >= 0,V17 >= 0,V1 = 1 + V16 + V17]).
eq(fun4(V1, Out),1,[fun4(V18, Ret17)],[Out = 1 + Ret17,V18 >= 0,V19 >= 0,V1 = 1 + V18 + V19]).
eq(fun5(V1, V, Out),0,[fun4(V20, Ret18)],[Out = 1 + Ret18,V1 = V21,V20 >= 0,V = V20,V21 >= 0]).
eq(fun6(V1, Out),0,[guess(V22, Ret111),fun5(V22, Ret111, Ret19)],[Out = 1 + Ret19,V1 = V22,V22 >= 0]).
eq(negate(V1, Out),0,[],[Out = 1 + V23,V1 = 1 + V23,V23 >= 0]).
eq(guess(V1, Out),0,[],[Out = 0,V1 = 0]).
eq(guess(V1, Out),0,[choice(V25, Ret01),guess(V24, Ret110)],[Out = 1 + Ret01 + Ret110,V24 >= 0,V25 >= 0,V1 = 1 + V24 + V25]).
eq(choice(V1, Out),0,[],[Out = V26,V27 >= 0,V26 >= 0,V1 = 1 + V26 + V27]).
eq(choice(V1, Out),0,[choice(V28, Ret)],[Out = Ret,V28 >= 0,V29 >= 0,V1 = 1 + V28 + V29]).
eq(fun5(V1, V, Out),0,[],[Out = 0,V31 >= 0,V30 >= 0,V1 = V31,V = V30]).
eq(fun6(V1, Out),0,[],[Out = 0,V32 >= 0,V1 = V32]).
eq(negate(V1, Out),0,[],[Out = 0,V33 >= 0,V1 = V33]).
eq(guess(V1, Out),0,[],[Out = 0,V34 >= 0,V1 = V34]).
eq(choice(V1, Out),0,[],[Out = 0,V35 >= 0,V1 = V35]).
eq(fun(V1, V, Out),0,[],[Out = 0,V36 >= 0,V37 >= 0,V1 = V36,V = V37]).
eq(fun1(V1, Out),0,[],[Out = 0,V38 >= 0,V1 = V38]).
eq(fun2(V1, Out),0,[],[Out = 0,V39 >= 0,V1 = V39]).
eq(fun3(V1, V, Out),0,[],[Out = 0,V40 >= 0,V41 >= 0,V1 = V40,V = V41]).
eq(fun4(V1, Out),0,[],[Out = 0,V42 >= 0,V1 = V42]).
input_output_vars(fun(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun1(V1,Out),[V1],[Out]).
input_output_vars(fun2(V1,Out),[V1],[Out]).
input_output_vars(fun3(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun4(V1,Out),[V1],[Out]).
input_output_vars(fun5(V1,V,Out),[V1,V],[Out]).
input_output_vars(fun6(V1,Out),[V1],[Out]).
input_output_vars(negate(V1,Out),[V1],[Out]).
input_output_vars(guess(V1,Out),[V1],[Out]).
input_output_vars(choice(V1,Out),[V1],[Out]).


CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. recursive  : [choice/2]
1. recursive  : [fun/3]
2. recursive  : [fun1/2]
3. recursive  : [fun2/2]
4. recursive  : [fun3/3]
5. non_recursive  : [negate/2]
6. recursive  : [fun4/2]
7. non_recursive  : [fun5/3]
8. recursive  : [guess/2]
9. non_recursive  : [fun6/2]
10. non_recursive  : [start/2]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into choice/2
1. SCC is partially evaluated into fun/3
2. SCC is partially evaluated into fun1/2
3. SCC is partially evaluated into fun2/2
4. SCC is partially evaluated into fun3/3
5. SCC is partially evaluated into negate/2
6. SCC is partially evaluated into fun4/2
7. SCC is partially evaluated into fun5/3
8. SCC is partially evaluated into guess/2
9. SCC is partially evaluated into fun6/2
10. SCC is partially evaluated into start/2

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations choice/2 
* CE 32 is refined into CE [35] 
* CE 34 is refined into CE [36] 
* CE 33 is refined into CE [37] 


### Cost equations --> "Loop" of choice/2 
* CEs [37] --> Loop 24 
* CEs [35] --> Loop 25 
* CEs [36] --> Loop 26 

### Ranking functions of CR choice(V1,Out) 
* RF of phase [24]: [V1]

#### Partial ranking functions of CR choice(V1,Out) 
* Partial RF of phase [24]:
  - RF of loop [24:1]:
    V1


### Specialization of cost equations fun/3 
* CE 12 is refined into CE [38] 
* CE 11 is refined into CE [39] 


### Cost equations --> "Loop" of fun/3 
* CEs [39] --> Loop 27 
* CEs [38] --> Loop 28 

### Ranking functions of CR fun(V1,V,Out) 
* RF of phase [27]: [V,V1]

#### Partial ranking functions of CR fun(V1,V,Out) 
* Partial RF of phase [27]:
  - RF of loop [27:1]:
    V
    V1


### Specialization of cost equations fun1/2 
* CE 14 is refined into CE [40] 
* CE 13 is refined into CE [41] 


### Cost equations --> "Loop" of fun1/2 
* CEs [41] --> Loop 29 
* CEs [40] --> Loop 30 

### Ranking functions of CR fun1(V1,Out) 
* RF of phase [29]: [V1]

#### Partial ranking functions of CR fun1(V1,Out) 
* Partial RF of phase [29]:
  - RF of loop [29:1]:
    V1


### Specialization of cost equations fun2/2 
* CE 15 is refined into CE [42,43] 
* CE 17 is refined into CE [44] 
* CE 16 is refined into CE [45] 


### Cost equations --> "Loop" of fun2/2 
* CEs [45] --> Loop 31 
* CEs [43] --> Loop 32 
* CEs [42] --> Loop 33 
* CEs [44] --> Loop 34 

### Ranking functions of CR fun2(V1,Out) 
* RF of phase [31]: [V1]

#### Partial ranking functions of CR fun2(V1,Out) 
* Partial RF of phase [31]:
  - RF of loop [31:1]:
    V1


### Specialization of cost equations fun3/3 
* CE 18 is refined into CE [46,47] 
* CE 20 is refined into CE [48] 
* CE 19 is refined into CE [49] 


### Cost equations --> "Loop" of fun3/3 
* CEs [49] --> Loop 35 
* CEs [47] --> Loop 36 
* CEs [46] --> Loop 37 
* CEs [48] --> Loop 38 

### Ranking functions of CR fun3(V1,V,Out) 
* RF of phase [35]: [V]

#### Partial ranking functions of CR fun3(V1,V,Out) 
* Partial RF of phase [35]:
  - RF of loop [35:1]:
    V


### Specialization of cost equations negate/2 
* CE 28 is refined into CE [50] 
* CE 29 is refined into CE [51] 


### Cost equations --> "Loop" of negate/2 
* CEs [50] --> Loop 39 
* CEs [51] --> Loop 40 

### Ranking functions of CR negate(V1,Out) 

#### Partial ranking functions of CR negate(V1,Out) 


### Specialization of cost equations fun4/2 
* CE 21 is refined into CE [52,53,54,55] 
* CE 23 is refined into CE [56] 
* CE 22 is refined into CE [57] 


### Cost equations --> "Loop" of fun4/2 
* CEs [57] --> Loop 41 
* CEs [53,55] --> Loop 42 
* CEs [52,54] --> Loop 43 
* CEs [56] --> Loop 44 

### Ranking functions of CR fun4(V1,Out) 
* RF of phase [41]: [V1]

#### Partial ranking functions of CR fun4(V1,Out) 
* Partial RF of phase [41]:
  - RF of loop [41:1]:
    V1


### Specialization of cost equations fun5/3 
* CE 24 is refined into CE [58,59] 
* CE 25 is refined into CE [60] 


### Cost equations --> "Loop" of fun5/3 
* CEs [59] --> Loop 45 
* CEs [58] --> Loop 46 
* CEs [60] --> Loop 47 

### Ranking functions of CR fun5(V1,V,Out) 

#### Partial ranking functions of CR fun5(V1,V,Out) 


### Specialization of cost equations guess/2 
* CE 30 is refined into CE [61] 
* CE 31 is refined into CE [62,63] 


### Cost equations --> "Loop" of guess/2 
* CEs [63] --> Loop 48 
* CEs [62] --> Loop 49 
* CEs [61] --> Loop 50 

### Ranking functions of CR guess(V1,Out) 
* RF of phase [48,49]: [V1]

#### Partial ranking functions of CR guess(V1,Out) 
* Partial RF of phase [48,49]:
  - RF of loop [48:1]:
    V1-1
  - RF of loop [49:1]:
    V1


### Specialization of cost equations fun6/2 
* CE 26 is refined into CE [64,65,66,67,68] 
* CE 27 is refined into CE [69] 


### Cost equations --> "Loop" of fun6/2 
* CEs [68] --> Loop 51 
* CEs [65,67] --> Loop 52 
* CEs [64,66] --> Loop 53 
* CEs [69] --> Loop 54 

### Ranking functions of CR fun6(V1,Out) 

#### Partial ranking functions of CR fun6(V1,Out) 


### Specialization of cost equations start/2 
* CE 1 is refined into CE [70,71] 
* CE 2 is refined into CE [72,73] 
* CE 3 is refined into CE [74,75] 
* CE 4 is refined into CE [76,77] 
* CE 5 is refined into CE [78,79] 
* CE 6 is refined into CE [80,81,82] 
* CE 7 is refined into CE [83,84,85,86] 
* CE 8 is refined into CE [87,88] 
* CE 9 is refined into CE [89,90] 
* CE 10 is refined into CE [91,92] 


### Cost equations --> "Loop" of start/2 
* CEs [70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92] --> Loop 55 

### Ranking functions of CR start(V1,V) 

#### Partial ranking functions of CR start(V1,V) 


Computing Bounds
=====================================

#### Cost of chains of choice(V1,Out):
* Chain [[24],26]: 0
  with precondition: [Out=0,V1>=1] 

* Chain [[24],25]: 0
  with precondition: [Out>=0,V1>=Out+2] 

* Chain [26]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [25]: 0
  with precondition: [Out>=0,V1>=Out+1] 


#### Cost of chains of fun(V1,V,Out):
* Chain [[27],28]: 1*it(27)+0
  Such that:it(27) =< Out

  with precondition: [Out>=1,V1>=Out,V>=Out] 

* Chain [28]: 0
  with precondition: [Out=0,V1>=0,V>=0] 


#### Cost of chains of fun1(V1,Out):
* Chain [[29],30]: 1*it(29)+0
  Such that:it(29) =< V1

  with precondition: [Out>=1,V1>=Out] 

* Chain [30]: 0
  with precondition: [Out=0,V1>=0] 


#### Cost of chains of fun2(V1,Out):
* Chain [[31],34]: 1*it(31)+0
  Such that:it(31) =< V1

  with precondition: [Out>=1,V1>=Out] 

* Chain [[31],33]: 1*it(31)+1
  Such that:it(31) =< V1

  with precondition: [Out>=2,V1>=Out] 

* Chain [[31],32]: 2*it(31)+1
  Such that:aux(1) =< V1
it(31) =< aux(1)

  with precondition: [Out>=3,V1>=Out] 

* Chain [34]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [33]: 1
  with precondition: [Out=1,V1>=1] 

* Chain [32]: 1*s(1)+1
  Such that:s(1) =< V1

  with precondition: [Out>=2,V1>=Out] 


#### Cost of chains of fun3(V1,V,Out):
* Chain [[35],38]: 1*it(35)+0
  Such that:it(35) =< V

  with precondition: [V1>=0,Out>=1,V>=Out] 

* Chain [[35],37]: 1*it(35)+1
  Such that:it(35) =< V

  with precondition: [V1>=0,Out>=2,V>=Out] 

* Chain [[35],36]: 2*it(35)+1
  Such that:aux(3) =< V
it(35) =< aux(3)

  with precondition: [V1>=1,Out>=3,V>=Out] 

* Chain [38]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [37]: 1
  with precondition: [Out=1,V1>=0,V>=1] 

* Chain [36]: 1*s(7)+1
  Such that:s(7) =< V

  with precondition: [Out>=2,V1+1>=Out,V>=Out] 


#### Cost of chains of negate(V1,Out):
* Chain [40]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [39]: 0
  with precondition: [V1=Out,V1>=1] 


#### Cost of chains of fun4(V1,Out):
* Chain [[41],44]: 1*it(41)+0
  Such that:it(41) =< V1

  with precondition: [Out>=1,V1>=Out] 

* Chain [[41],43]: 1*it(41)+1
  Such that:it(41) =< V1

  with precondition: [Out>=2,V1>=Out] 

* Chain [[41],42]: 11*it(41)+2
  Such that:aux(6) =< V1
it(41) =< aux(6)

  with precondition: [Out>=3,V1>=Out] 

* Chain [44]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [43]: 1
  with precondition: [Out=1,V1>=1] 

* Chain [42]: 10*s(14)+2
  Such that:aux(5) =< V1
s(14) =< aux(5)

  with precondition: [Out>=2,V1>=Out] 


#### Cost of chains of fun5(V1,V,Out):
* Chain [47]: 0
  with precondition: [Out=0,V1>=0,V>=0] 

* Chain [46]: 0
  with precondition: [Out=1,V1>=0,V>=0] 

* Chain [45]: 23*s(24)+2
  Such that:s(23) =< V
s(24) =< s(23)

  with precondition: [V1>=0,Out>=2,V+1>=Out] 


#### Cost of chains of guess(V1,Out):
* Chain [[48,49],50]: 0
  with precondition: [Out>=1,V1>=Out] 

* Chain [50]: 0
  with precondition: [Out=0,V1>=0] 


#### Cost of chains of fun6(V1,Out):
* Chain [54]: 0
  with precondition: [Out=0,V1>=0] 

* Chain [53]: 0
  with precondition: [Out=1,V1>=0] 

* Chain [52]: 0
  with precondition: [Out=2,V1>=0] 

* Chain [51]: 23*s(26)+2
  Such that:s(25) =< V1
s(26) =< s(25)

  with precondition: [Out>=3,V1+2>=Out] 


#### Cost of chains of start(V1,V):
* Chain [55]: 29*s(27)+52*s(28)+2
  Such that:aux(10) =< V1
aux(11) =< V
s(28) =< aux(10)
s(27) =< aux(11)

  with precondition: [V1>=0] 


Closed-form bounds of start(V1,V): 
-------------------------------------
* Chain [55] with precondition: [V1>=0] 
    - Upper bound: 52*V1+2+nat(V)*29 
    - Complexity: n 

### Maximum cost of start(V1,V): 52*V1+2+nat(V)*29 
Asymptotic class: n 
* Total analysis performed in 347 ms.


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

(26)
BOUNDS(1, n^1)

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

(27) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(28)
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


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

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

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


The TRS R consists of the following rules:

   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))

The (relative) TRS S consists of the following 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)

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

(31) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

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


The TRS R consists of the following rules:

   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))

The (relative) TRS S consists of the following 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)

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

(33) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(34)
Obligation:
Innermost TRS:
Rules:
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))
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)

Types:
IF :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c:c1
true :: true:false:nil:cons:O:0:1:unsat
c :: c:c1
false :: true:false:nil:cons:O:0:1:unsat
c1 :: c:c1
MEMBER :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c2:c3:c4
nil :: true:false:nil:cons:O:0:1:unsat
c2 :: c2:c3:c4
cons :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c3 :: c:c1 -> c5:c6:c7:c8:c9 -> c2:c3:c4
eq :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
EQ :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c5:c6:c7:c8:c9
c4 :: c:c1 -> c2:c3:c4 -> c2:c3:c4
c5 :: c5:c6:c7:c8:c9
O :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c6 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
1 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c7 :: c5:c6:c7:c8:c9
c8 :: c5:c6:c7:c8:c9
c9 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
NEGATE :: true:false:nil:cons:O:0:1:unsat -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
CHOICE :: true:false:nil:cons:O:0:1:unsat -> c12:c13
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
GUESS :: true:false:nil:cons:O:0:1:unsat -> c14:c15:c16
c14 :: c14:c15:c16
c15 :: c12:c13 -> c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
VERIFY :: true:false:nil:cons:O:0:1:unsat -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c:c1 -> c2:c3:c4 -> c10:c11 -> c17:c18:c19
negate :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c19 :: c:c1 -> c17:c18:c19 -> c17:c18:c19
SAT :: true:false:nil:cons:O:0:1:unsat -> c20
c20 :: c21 -> c14:c15:c16 -> c20
SATCK :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c21
guess :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c21 :: c:c1 -> c17:c18:c19 -> c21
unsat :: true:false:nil:cons:O:0:1:unsat
if :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
hole_c:c11_22 :: c:c1
hole_true:false:nil:cons:O:0:1:unsat2_22 :: true:false:nil:cons:O:0:1:unsat
hole_c2:c3:c43_22 :: c2:c3:c4
hole_c5:c6:c7:c8:c94_22 :: c5:c6:c7:c8:c9
hole_c10:c115_22 :: c10:c11
hole_c12:c136_22 :: c12:c13
hole_c14:c15:c167_22 :: c14:c15:c16
hole_c17:c18:c198_22 :: c17:c18:c19
hole_c209_22 :: c20
hole_c2110_22 :: c21
gen_true:false:nil:cons:O:0:1:unsat11_22 :: Nat -> true:false:nil:cons:O:0:1:unsat
gen_c2:c3:c412_22 :: Nat -> c2:c3:c4
gen_c5:c6:c7:c8:c913_22 :: Nat -> c5:c6:c7:c8:c9
gen_c12:c1314_22 :: Nat -> c12:c13
gen_c14:c15:c1615_22 :: Nat -> c14:c15:c16
gen_c17:c18:c1916_22 :: Nat -> c17:c18:c19

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

(35) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
MEMBER, eq, member, EQ, CHOICE, GUESS, VERIFY, verify, guess, choice

They will be analysed ascendingly in the following order:
eq < MEMBER
member < MEMBER
EQ < MEMBER
MEMBER < VERIFY
eq < member
member < VERIFY
member < verify
CHOICE < GUESS
verify < VERIFY
choice < guess

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

(36)
Obligation:
Innermost TRS:
Rules:
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))
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)

Types:
IF :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c:c1
true :: true:false:nil:cons:O:0:1:unsat
c :: c:c1
false :: true:false:nil:cons:O:0:1:unsat
c1 :: c:c1
MEMBER :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c2:c3:c4
nil :: true:false:nil:cons:O:0:1:unsat
c2 :: c2:c3:c4
cons :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c3 :: c:c1 -> c5:c6:c7:c8:c9 -> c2:c3:c4
eq :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
EQ :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c5:c6:c7:c8:c9
c4 :: c:c1 -> c2:c3:c4 -> c2:c3:c4
c5 :: c5:c6:c7:c8:c9
O :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c6 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
1 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c7 :: c5:c6:c7:c8:c9
c8 :: c5:c6:c7:c8:c9
c9 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
NEGATE :: true:false:nil:cons:O:0:1:unsat -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
CHOICE :: true:false:nil:cons:O:0:1:unsat -> c12:c13
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
GUESS :: true:false:nil:cons:O:0:1:unsat -> c14:c15:c16
c14 :: c14:c15:c16
c15 :: c12:c13 -> c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
VERIFY :: true:false:nil:cons:O:0:1:unsat -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c:c1 -> c2:c3:c4 -> c10:c11 -> c17:c18:c19
negate :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c19 :: c:c1 -> c17:c18:c19 -> c17:c18:c19
SAT :: true:false:nil:cons:O:0:1:unsat -> c20
c20 :: c21 -> c14:c15:c16 -> c20
SATCK :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c21
guess :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c21 :: c:c1 -> c17:c18:c19 -> c21
unsat :: true:false:nil:cons:O:0:1:unsat
if :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
hole_c:c11_22 :: c:c1
hole_true:false:nil:cons:O:0:1:unsat2_22 :: true:false:nil:cons:O:0:1:unsat
hole_c2:c3:c43_22 :: c2:c3:c4
hole_c5:c6:c7:c8:c94_22 :: c5:c6:c7:c8:c9
hole_c10:c115_22 :: c10:c11
hole_c12:c136_22 :: c12:c13
hole_c14:c15:c167_22 :: c14:c15:c16
hole_c17:c18:c198_22 :: c17:c18:c19
hole_c209_22 :: c20
hole_c2110_22 :: c21
gen_true:false:nil:cons:O:0:1:unsat11_22 :: Nat -> true:false:nil:cons:O:0:1:unsat
gen_c2:c3:c412_22 :: Nat -> c2:c3:c4
gen_c5:c6:c7:c8:c913_22 :: Nat -> c5:c6:c7:c8:c9
gen_c12:c1314_22 :: Nat -> c12:c13
gen_c14:c15:c1615_22 :: Nat -> c14:c15:c16
gen_c17:c18:c1916_22 :: Nat -> c17:c18:c19


Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat11_22(0) <=> true
gen_true:false:nil:cons:O:0:1:unsat11_22(+(x, 1)) <=> cons(true, gen_true:false:nil:cons:O:0:1:unsat11_22(x))
gen_c2:c3:c412_22(0) <=> c2
gen_c2:c3:c412_22(+(x, 1)) <=> c4(c, gen_c2:c3:c412_22(x))
gen_c5:c6:c7:c8:c913_22(0) <=> c5
gen_c5:c6:c7:c8:c913_22(+(x, 1)) <=> c6(gen_c5:c6:c7:c8:c913_22(x))
gen_c12:c1314_22(0) <=> c12
gen_c12:c1314_22(+(x, 1)) <=> c13(gen_c12:c1314_22(x))
gen_c14:c15:c1615_22(0) <=> c14
gen_c14:c15:c1615_22(+(x, 1)) <=> c16(gen_c14:c15:c1615_22(x))
gen_c17:c18:c1916_22(0) <=> c17
gen_c17:c18:c1916_22(+(x, 1)) <=> c19(c, gen_c17:c18:c1916_22(x))


The following defined symbols remain to be analysed:
eq, MEMBER, member, EQ, CHOICE, GUESS, VERIFY, verify, guess, choice

They will be analysed ascendingly in the following order:
eq < MEMBER
member < MEMBER
EQ < MEMBER
MEMBER < VERIFY
eq < member
member < VERIFY
member < verify
CHOICE < GUESS
verify < VERIFY
choice < guess

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

(37) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
member(gen_true:false:nil:cons:O:0:1:unsat11_22(a), gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n131_22))) -> *17_22, rt in Omega(0)

Induction Base:
member(gen_true:false:nil:cons:O:0:1:unsat11_22(a), gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, 0)))

Induction Step:
member(gen_true:false:nil:cons:O:0:1:unsat11_22(a), gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, +(n131_22, 1)))) ->_R^Omega(0)
if(eq(gen_true:false:nil:cons:O:0:1:unsat11_22(a), true), true, member(gen_true:false:nil:cons:O:0:1:unsat11_22(a), gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n131_22)))) ->_IH
if(eq(gen_true:false:nil:cons:O:0:1:unsat11_22(a), true), true, *17_22)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(38)
Obligation:
Innermost TRS:
Rules:
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))
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)

Types:
IF :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c:c1
true :: true:false:nil:cons:O:0:1:unsat
c :: c:c1
false :: true:false:nil:cons:O:0:1:unsat
c1 :: c:c1
MEMBER :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c2:c3:c4
nil :: true:false:nil:cons:O:0:1:unsat
c2 :: c2:c3:c4
cons :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c3 :: c:c1 -> c5:c6:c7:c8:c9 -> c2:c3:c4
eq :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
EQ :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c5:c6:c7:c8:c9
c4 :: c:c1 -> c2:c3:c4 -> c2:c3:c4
c5 :: c5:c6:c7:c8:c9
O :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c6 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
1 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c7 :: c5:c6:c7:c8:c9
c8 :: c5:c6:c7:c8:c9
c9 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
NEGATE :: true:false:nil:cons:O:0:1:unsat -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
CHOICE :: true:false:nil:cons:O:0:1:unsat -> c12:c13
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
GUESS :: true:false:nil:cons:O:0:1:unsat -> c14:c15:c16
c14 :: c14:c15:c16
c15 :: c12:c13 -> c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
VERIFY :: true:false:nil:cons:O:0:1:unsat -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c:c1 -> c2:c3:c4 -> c10:c11 -> c17:c18:c19
negate :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c19 :: c:c1 -> c17:c18:c19 -> c17:c18:c19
SAT :: true:false:nil:cons:O:0:1:unsat -> c20
c20 :: c21 -> c14:c15:c16 -> c20
SATCK :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c21
guess :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c21 :: c:c1 -> c17:c18:c19 -> c21
unsat :: true:false:nil:cons:O:0:1:unsat
if :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
hole_c:c11_22 :: c:c1
hole_true:false:nil:cons:O:0:1:unsat2_22 :: true:false:nil:cons:O:0:1:unsat
hole_c2:c3:c43_22 :: c2:c3:c4
hole_c5:c6:c7:c8:c94_22 :: c5:c6:c7:c8:c9
hole_c10:c115_22 :: c10:c11
hole_c12:c136_22 :: c12:c13
hole_c14:c15:c167_22 :: c14:c15:c16
hole_c17:c18:c198_22 :: c17:c18:c19
hole_c209_22 :: c20
hole_c2110_22 :: c21
gen_true:false:nil:cons:O:0:1:unsat11_22 :: Nat -> true:false:nil:cons:O:0:1:unsat
gen_c2:c3:c412_22 :: Nat -> c2:c3:c4
gen_c5:c6:c7:c8:c913_22 :: Nat -> c5:c6:c7:c8:c9
gen_c12:c1314_22 :: Nat -> c12:c13
gen_c14:c15:c1615_22 :: Nat -> c14:c15:c16
gen_c17:c18:c1916_22 :: Nat -> c17:c18:c19


Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat11_22(a), gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n131_22))) -> *17_22, rt in Omega(0)


Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat11_22(0) <=> true
gen_true:false:nil:cons:O:0:1:unsat11_22(+(x, 1)) <=> cons(true, gen_true:false:nil:cons:O:0:1:unsat11_22(x))
gen_c2:c3:c412_22(0) <=> c2
gen_c2:c3:c412_22(+(x, 1)) <=> c4(c, gen_c2:c3:c412_22(x))
gen_c5:c6:c7:c8:c913_22(0) <=> c5
gen_c5:c6:c7:c8:c913_22(+(x, 1)) <=> c6(gen_c5:c6:c7:c8:c913_22(x))
gen_c12:c1314_22(0) <=> c12
gen_c12:c1314_22(+(x, 1)) <=> c13(gen_c12:c1314_22(x))
gen_c14:c15:c1615_22(0) <=> c14
gen_c14:c15:c1615_22(+(x, 1)) <=> c16(gen_c14:c15:c1615_22(x))
gen_c17:c18:c1916_22(0) <=> c17
gen_c17:c18:c1916_22(+(x, 1)) <=> c19(c, gen_c17:c18:c1916_22(x))


The following defined symbols remain to be analysed:
EQ, MEMBER, CHOICE, GUESS, VERIFY, verify, guess, choice

They will be analysed ascendingly in the following order:
EQ < MEMBER
MEMBER < VERIFY
CHOICE < GUESS
verify < VERIFY
choice < guess

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

(39) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
CHOICE(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n263902_22))) -> *17_22, rt in Omega(n263902_22)

Induction Base:
CHOICE(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, 0)))

Induction Step:
CHOICE(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, +(n263902_22, 1)))) ->_R^Omega(1)
c13(CHOICE(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n263902_22)))) ->_IH
c13(*17_22)

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(40)
Complex Obligation (BEST)

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

(41)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
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))
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)

Types:
IF :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c:c1
true :: true:false:nil:cons:O:0:1:unsat
c :: c:c1
false :: true:false:nil:cons:O:0:1:unsat
c1 :: c:c1
MEMBER :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c2:c3:c4
nil :: true:false:nil:cons:O:0:1:unsat
c2 :: c2:c3:c4
cons :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c3 :: c:c1 -> c5:c6:c7:c8:c9 -> c2:c3:c4
eq :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
EQ :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c5:c6:c7:c8:c9
c4 :: c:c1 -> c2:c3:c4 -> c2:c3:c4
c5 :: c5:c6:c7:c8:c9
O :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c6 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
1 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c7 :: c5:c6:c7:c8:c9
c8 :: c5:c6:c7:c8:c9
c9 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
NEGATE :: true:false:nil:cons:O:0:1:unsat -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
CHOICE :: true:false:nil:cons:O:0:1:unsat -> c12:c13
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
GUESS :: true:false:nil:cons:O:0:1:unsat -> c14:c15:c16
c14 :: c14:c15:c16
c15 :: c12:c13 -> c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
VERIFY :: true:false:nil:cons:O:0:1:unsat -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c:c1 -> c2:c3:c4 -> c10:c11 -> c17:c18:c19
negate :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c19 :: c:c1 -> c17:c18:c19 -> c17:c18:c19
SAT :: true:false:nil:cons:O:0:1:unsat -> c20
c20 :: c21 -> c14:c15:c16 -> c20
SATCK :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c21
guess :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c21 :: c:c1 -> c17:c18:c19 -> c21
unsat :: true:false:nil:cons:O:0:1:unsat
if :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
hole_c:c11_22 :: c:c1
hole_true:false:nil:cons:O:0:1:unsat2_22 :: true:false:nil:cons:O:0:1:unsat
hole_c2:c3:c43_22 :: c2:c3:c4
hole_c5:c6:c7:c8:c94_22 :: c5:c6:c7:c8:c9
hole_c10:c115_22 :: c10:c11
hole_c12:c136_22 :: c12:c13
hole_c14:c15:c167_22 :: c14:c15:c16
hole_c17:c18:c198_22 :: c17:c18:c19
hole_c209_22 :: c20
hole_c2110_22 :: c21
gen_true:false:nil:cons:O:0:1:unsat11_22 :: Nat -> true:false:nil:cons:O:0:1:unsat
gen_c2:c3:c412_22 :: Nat -> c2:c3:c4
gen_c5:c6:c7:c8:c913_22 :: Nat -> c5:c6:c7:c8:c9
gen_c12:c1314_22 :: Nat -> c12:c13
gen_c14:c15:c1615_22 :: Nat -> c14:c15:c16
gen_c17:c18:c1916_22 :: Nat -> c17:c18:c19


Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat11_22(a), gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n131_22))) -> *17_22, rt in Omega(0)


Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat11_22(0) <=> true
gen_true:false:nil:cons:O:0:1:unsat11_22(+(x, 1)) <=> cons(true, gen_true:false:nil:cons:O:0:1:unsat11_22(x))
gen_c2:c3:c412_22(0) <=> c2
gen_c2:c3:c412_22(+(x, 1)) <=> c4(c, gen_c2:c3:c412_22(x))
gen_c5:c6:c7:c8:c913_22(0) <=> c5
gen_c5:c6:c7:c8:c913_22(+(x, 1)) <=> c6(gen_c5:c6:c7:c8:c913_22(x))
gen_c12:c1314_22(0) <=> c12
gen_c12:c1314_22(+(x, 1)) <=> c13(gen_c12:c1314_22(x))
gen_c14:c15:c1615_22(0) <=> c14
gen_c14:c15:c1615_22(+(x, 1)) <=> c16(gen_c14:c15:c1615_22(x))
gen_c17:c18:c1916_22(0) <=> c17
gen_c17:c18:c1916_22(+(x, 1)) <=> c19(c, gen_c17:c18:c1916_22(x))


The following defined symbols remain to be analysed:
CHOICE, GUESS, VERIFY, verify, guess, choice

They will be analysed ascendingly in the following order:
CHOICE < GUESS
verify < VERIFY
choice < guess

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

(42) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(43)
BOUNDS(n^1, INF)

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

(44)
Obligation:
Innermost TRS:
Rules:
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))
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)

Types:
IF :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c:c1
true :: true:false:nil:cons:O:0:1:unsat
c :: c:c1
false :: true:false:nil:cons:O:0:1:unsat
c1 :: c:c1
MEMBER :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c2:c3:c4
nil :: true:false:nil:cons:O:0:1:unsat
c2 :: c2:c3:c4
cons :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c3 :: c:c1 -> c5:c6:c7:c8:c9 -> c2:c3:c4
eq :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
EQ :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c5:c6:c7:c8:c9
c4 :: c:c1 -> c2:c3:c4 -> c2:c3:c4
c5 :: c5:c6:c7:c8:c9
O :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c6 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
1 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c7 :: c5:c6:c7:c8:c9
c8 :: c5:c6:c7:c8:c9
c9 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
NEGATE :: true:false:nil:cons:O:0:1:unsat -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
CHOICE :: true:false:nil:cons:O:0:1:unsat -> c12:c13
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
GUESS :: true:false:nil:cons:O:0:1:unsat -> c14:c15:c16
c14 :: c14:c15:c16
c15 :: c12:c13 -> c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
VERIFY :: true:false:nil:cons:O:0:1:unsat -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c:c1 -> c2:c3:c4 -> c10:c11 -> c17:c18:c19
negate :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c19 :: c:c1 -> c17:c18:c19 -> c17:c18:c19
SAT :: true:false:nil:cons:O:0:1:unsat -> c20
c20 :: c21 -> c14:c15:c16 -> c20
SATCK :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c21
guess :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c21 :: c:c1 -> c17:c18:c19 -> c21
unsat :: true:false:nil:cons:O:0:1:unsat
if :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
hole_c:c11_22 :: c:c1
hole_true:false:nil:cons:O:0:1:unsat2_22 :: true:false:nil:cons:O:0:1:unsat
hole_c2:c3:c43_22 :: c2:c3:c4
hole_c5:c6:c7:c8:c94_22 :: c5:c6:c7:c8:c9
hole_c10:c115_22 :: c10:c11
hole_c12:c136_22 :: c12:c13
hole_c14:c15:c167_22 :: c14:c15:c16
hole_c17:c18:c198_22 :: c17:c18:c19
hole_c209_22 :: c20
hole_c2110_22 :: c21
gen_true:false:nil:cons:O:0:1:unsat11_22 :: Nat -> true:false:nil:cons:O:0:1:unsat
gen_c2:c3:c412_22 :: Nat -> c2:c3:c4
gen_c5:c6:c7:c8:c913_22 :: Nat -> c5:c6:c7:c8:c9
gen_c12:c1314_22 :: Nat -> c12:c13
gen_c14:c15:c1615_22 :: Nat -> c14:c15:c16
gen_c17:c18:c1916_22 :: Nat -> c17:c18:c19


Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat11_22(a), gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n131_22))) -> *17_22, rt in Omega(0)
CHOICE(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n263902_22))) -> *17_22, rt in Omega(n263902_22)


Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat11_22(0) <=> true
gen_true:false:nil:cons:O:0:1:unsat11_22(+(x, 1)) <=> cons(true, gen_true:false:nil:cons:O:0:1:unsat11_22(x))
gen_c2:c3:c412_22(0) <=> c2
gen_c2:c3:c412_22(+(x, 1)) <=> c4(c, gen_c2:c3:c412_22(x))
gen_c5:c6:c7:c8:c913_22(0) <=> c5
gen_c5:c6:c7:c8:c913_22(+(x, 1)) <=> c6(gen_c5:c6:c7:c8:c913_22(x))
gen_c12:c1314_22(0) <=> c12
gen_c12:c1314_22(+(x, 1)) <=> c13(gen_c12:c1314_22(x))
gen_c14:c15:c1615_22(0) <=> c14
gen_c14:c15:c1615_22(+(x, 1)) <=> c16(gen_c14:c15:c1615_22(x))
gen_c17:c18:c1916_22(0) <=> c17
gen_c17:c18:c1916_22(+(x, 1)) <=> c19(c, gen_c17:c18:c1916_22(x))


The following defined symbols remain to be analysed:
GUESS, VERIFY, verify, guess, choice

They will be analysed ascendingly in the following order:
verify < VERIFY
choice < guess

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

(45) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
GUESS(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n264551_22))) -> *17_22, rt in Omega(n264551_22)

Induction Base:
GUESS(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, 0)))

Induction Step:
GUESS(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, +(n264551_22, 1)))) ->_R^Omega(1)
c16(GUESS(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n264551_22)))) ->_IH
c16(*17_22)

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(46)
Obligation:
Innermost TRS:
Rules:
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))
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)

Types:
IF :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c:c1
true :: true:false:nil:cons:O:0:1:unsat
c :: c:c1
false :: true:false:nil:cons:O:0:1:unsat
c1 :: c:c1
MEMBER :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c2:c3:c4
nil :: true:false:nil:cons:O:0:1:unsat
c2 :: c2:c3:c4
cons :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c3 :: c:c1 -> c5:c6:c7:c8:c9 -> c2:c3:c4
eq :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
EQ :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c5:c6:c7:c8:c9
c4 :: c:c1 -> c2:c3:c4 -> c2:c3:c4
c5 :: c5:c6:c7:c8:c9
O :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c6 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
1 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c7 :: c5:c6:c7:c8:c9
c8 :: c5:c6:c7:c8:c9
c9 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
NEGATE :: true:false:nil:cons:O:0:1:unsat -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
CHOICE :: true:false:nil:cons:O:0:1:unsat -> c12:c13
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
GUESS :: true:false:nil:cons:O:0:1:unsat -> c14:c15:c16
c14 :: c14:c15:c16
c15 :: c12:c13 -> c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
VERIFY :: true:false:nil:cons:O:0:1:unsat -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c:c1 -> c2:c3:c4 -> c10:c11 -> c17:c18:c19
negate :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c19 :: c:c1 -> c17:c18:c19 -> c17:c18:c19
SAT :: true:false:nil:cons:O:0:1:unsat -> c20
c20 :: c21 -> c14:c15:c16 -> c20
SATCK :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c21
guess :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c21 :: c:c1 -> c17:c18:c19 -> c21
unsat :: true:false:nil:cons:O:0:1:unsat
if :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
hole_c:c11_22 :: c:c1
hole_true:false:nil:cons:O:0:1:unsat2_22 :: true:false:nil:cons:O:0:1:unsat
hole_c2:c3:c43_22 :: c2:c3:c4
hole_c5:c6:c7:c8:c94_22 :: c5:c6:c7:c8:c9
hole_c10:c115_22 :: c10:c11
hole_c12:c136_22 :: c12:c13
hole_c14:c15:c167_22 :: c14:c15:c16
hole_c17:c18:c198_22 :: c17:c18:c19
hole_c209_22 :: c20
hole_c2110_22 :: c21
gen_true:false:nil:cons:O:0:1:unsat11_22 :: Nat -> true:false:nil:cons:O:0:1:unsat
gen_c2:c3:c412_22 :: Nat -> c2:c3:c4
gen_c5:c6:c7:c8:c913_22 :: Nat -> c5:c6:c7:c8:c9
gen_c12:c1314_22 :: Nat -> c12:c13
gen_c14:c15:c1615_22 :: Nat -> c14:c15:c16
gen_c17:c18:c1916_22 :: Nat -> c17:c18:c19


Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat11_22(a), gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n131_22))) -> *17_22, rt in Omega(0)
CHOICE(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n263902_22))) -> *17_22, rt in Omega(n263902_22)
GUESS(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n264551_22))) -> *17_22, rt in Omega(n264551_22)


Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat11_22(0) <=> true
gen_true:false:nil:cons:O:0:1:unsat11_22(+(x, 1)) <=> cons(true, gen_true:false:nil:cons:O:0:1:unsat11_22(x))
gen_c2:c3:c412_22(0) <=> c2
gen_c2:c3:c412_22(+(x, 1)) <=> c4(c, gen_c2:c3:c412_22(x))
gen_c5:c6:c7:c8:c913_22(0) <=> c5
gen_c5:c6:c7:c8:c913_22(+(x, 1)) <=> c6(gen_c5:c6:c7:c8:c913_22(x))
gen_c12:c1314_22(0) <=> c12
gen_c12:c1314_22(+(x, 1)) <=> c13(gen_c12:c1314_22(x))
gen_c14:c15:c1615_22(0) <=> c14
gen_c14:c15:c1615_22(+(x, 1)) <=> c16(gen_c14:c15:c1615_22(x))
gen_c17:c18:c1916_22(0) <=> c17
gen_c17:c18:c1916_22(+(x, 1)) <=> c19(c, gen_c17:c18:c1916_22(x))


The following defined symbols remain to be analysed:
verify, VERIFY, guess, choice

They will be analysed ascendingly in the following order:
verify < VERIFY
choice < guess

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

(47) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
choice(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n559978_22))) -> *17_22, rt in Omega(0)

Induction Base:
choice(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, 0)))

Induction Step:
choice(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, +(n559978_22, 1)))) ->_R^Omega(0)
choice(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n559978_22))) ->_IH
*17_22

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(48)
Obligation:
Innermost TRS:
Rules:
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))
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)

Types:
IF :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c:c1
true :: true:false:nil:cons:O:0:1:unsat
c :: c:c1
false :: true:false:nil:cons:O:0:1:unsat
c1 :: c:c1
MEMBER :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c2:c3:c4
nil :: true:false:nil:cons:O:0:1:unsat
c2 :: c2:c3:c4
cons :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c3 :: c:c1 -> c5:c6:c7:c8:c9 -> c2:c3:c4
eq :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
member :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
EQ :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c5:c6:c7:c8:c9
c4 :: c:c1 -> c2:c3:c4 -> c2:c3:c4
c5 :: c5:c6:c7:c8:c9
O :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
0 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c6 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
1 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c7 :: c5:c6:c7:c8:c9
c8 :: c5:c6:c7:c8:c9
c9 :: c5:c6:c7:c8:c9 -> c5:c6:c7:c8:c9
NEGATE :: true:false:nil:cons:O:0:1:unsat -> c10:c11
c10 :: c10:c11
c11 :: c10:c11
CHOICE :: true:false:nil:cons:O:0:1:unsat -> c12:c13
c12 :: c12:c13
c13 :: c12:c13 -> c12:c13
GUESS :: true:false:nil:cons:O:0:1:unsat -> c14:c15:c16
c14 :: c14:c15:c16
c15 :: c12:c13 -> c14:c15:c16
c16 :: c14:c15:c16 -> c14:c15:c16
VERIFY :: true:false:nil:cons:O:0:1:unsat -> c17:c18:c19
c17 :: c17:c18:c19
c18 :: c:c1 -> c2:c3:c4 -> c10:c11 -> c17:c18:c19
negate :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
verify :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c19 :: c:c1 -> c17:c18:c19 -> c17:c18:c19
SAT :: true:false:nil:cons:O:0:1:unsat -> c20
c20 :: c21 -> c14:c15:c16 -> c20
SATCK :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> c21
guess :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
c21 :: c:c1 -> c17:c18:c19 -> c21
unsat :: true:false:nil:cons:O:0:1:unsat
if :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
choice :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
sat :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
satck :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
hole_c:c11_22 :: c:c1
hole_true:false:nil:cons:O:0:1:unsat2_22 :: true:false:nil:cons:O:0:1:unsat
hole_c2:c3:c43_22 :: c2:c3:c4
hole_c5:c6:c7:c8:c94_22 :: c5:c6:c7:c8:c9
hole_c10:c115_22 :: c10:c11
hole_c12:c136_22 :: c12:c13
hole_c14:c15:c167_22 :: c14:c15:c16
hole_c17:c18:c198_22 :: c17:c18:c19
hole_c209_22 :: c20
hole_c2110_22 :: c21
gen_true:false:nil:cons:O:0:1:unsat11_22 :: Nat -> true:false:nil:cons:O:0:1:unsat
gen_c2:c3:c412_22 :: Nat -> c2:c3:c4
gen_c5:c6:c7:c8:c913_22 :: Nat -> c5:c6:c7:c8:c9
gen_c12:c1314_22 :: Nat -> c12:c13
gen_c14:c15:c1615_22 :: Nat -> c14:c15:c16
gen_c17:c18:c1916_22 :: Nat -> c17:c18:c19


Lemmas:
member(gen_true:false:nil:cons:O:0:1:unsat11_22(a), gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n131_22))) -> *17_22, rt in Omega(0)
CHOICE(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n263902_22))) -> *17_22, rt in Omega(n263902_22)
GUESS(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n264551_22))) -> *17_22, rt in Omega(n264551_22)
choice(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n559978_22))) -> *17_22, rt in Omega(0)


Generator Equations:
gen_true:false:nil:cons:O:0:1:unsat11_22(0) <=> true
gen_true:false:nil:cons:O:0:1:unsat11_22(+(x, 1)) <=> cons(true, gen_true:false:nil:cons:O:0:1:unsat11_22(x))
gen_c2:c3:c412_22(0) <=> c2
gen_c2:c3:c412_22(+(x, 1)) <=> c4(c, gen_c2:c3:c412_22(x))
gen_c5:c6:c7:c8:c913_22(0) <=> c5
gen_c5:c6:c7:c8:c913_22(+(x, 1)) <=> c6(gen_c5:c6:c7:c8:c913_22(x))
gen_c12:c1314_22(0) <=> c12
gen_c12:c1314_22(+(x, 1)) <=> c13(gen_c12:c1314_22(x))
gen_c14:c15:c1615_22(0) <=> c14
gen_c14:c15:c1615_22(+(x, 1)) <=> c16(gen_c14:c15:c1615_22(x))
gen_c17:c18:c1916_22(0) <=> c17
gen_c17:c18:c1916_22(+(x, 1)) <=> c19(c, gen_c17:c18:c1916_22(x))


The following defined symbols remain to be analysed:
guess
----------------------------------------

(49) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
guess(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n560816_22))) -> *17_22, rt in Omega(0)

Induction Base:
guess(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, 0)))

Induction Step:
guess(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, +(n560816_22, 1)))) ->_R^Omega(0)
cons(choice(true), guess(gen_true:false:nil:cons:O:0:1:unsat11_22(+(1, n560816_22)))) ->_IH
cons(choice(true), *17_22)

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(50)
BOUNDS(1, INF)