WORST_CASE(?,O(n^2))
proof of input_o3a9YGu4n1.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxTRS
(1) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms]
(2) CpxWeightedTrs
(3) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxTypedWeightedTrs
(5) CompletionProof [UPPER BOUND(ID), 0 ms]
(6) CpxTypedWeightedCompleteTrs
(7) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
(8) CpxRNTS
(9) CompleteCoflocoProof [FINISHED, 921 ms]
(10) BOUNDS(1, n^2)


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

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


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) RelTrsToWeightedTrsProof (UPPER BOUND(ID))
Transformed relative TRS to weighted TRS
----------------------------------------

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


The TRS R consists of the following rules:

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

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

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

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

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

The TRS has the following type information:
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
true :: true:false:nil:cons:O:0:1:unsat
false :: 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
nil :: true:false:nil:cons:O:0:1:unsat
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
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
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
1 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat
negate :: 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
guess :: 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
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
unsat :: true:false:nil:cons:O:0:1:unsat

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

(5) 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:

   if(v0, v1, v2) -> null_if [0]
   member(v0, v1) -> null_member [0]
   eq(v0, v1) -> null_eq [0]
   negate(v0) -> null_negate [0]
   choice(v0) -> null_choice [0]
   guess(v0) -> null_guess [0]
   verify(v0) -> null_verify [0]

And the following fresh constants:    null_if, null_member, null_eq, null_negate, null_choice, null_guess, null_verify

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

(6)
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:

   if(true, t, e) -> t [1]
   if(false, t, e) -> e [1]
   member(x, nil) -> false [1]
   member(x, cons(y, ys)) -> if(eq(x, y), true, member(x, ys)) [1]
   eq(nil, nil) -> true [1]
   eq(O(x), 0(y)) -> eq(x, y) [1]
   eq(0(x), 1(y)) -> false [1]
   eq(1(x), 0(y)) -> false [1]
   eq(1(x), 1(y)) -> eq(x, y) [1]
   negate(0(x)) -> 1(x) [1]
   negate(1(x)) -> 0(x) [1]
   choice(cons(x, xs)) -> x [1]
   choice(cons(x, xs)) -> choice(xs) [1]
   guess(nil) -> nil [1]
   guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) [1]
   verify(nil) -> true [1]
   verify(cons(l, ls)) -> if(member(negate(l), ls), false, verify(ls)) [1]
   sat(cnf) -> satck(cnf, guess(cnf)) [1]
   satck(cnf, assign) -> if(verify(assign), assign, unsat) [1]
   if(v0, v1, v2) -> null_if [0]
   member(v0, v1) -> null_member [0]
   eq(v0, v1) -> null_eq [0]
   negate(v0) -> null_negate [0]
   choice(v0) -> null_choice [0]
   guess(v0) -> null_guess [0]
   verify(v0) -> null_verify [0]

The TRS has the following type information:
if :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
true :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
false :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
member :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
nil :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
cons :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
eq :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
O :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
0 :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
1 :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
negate :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
choice :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
guess :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
verify :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
sat :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
satck :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
unsat :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
null_if :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
null_member :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
null_eq :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
null_negate :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
null_choice :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
null_guess :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify
null_verify :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify

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

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

   true => 2
   false => 0
   nil => 1
   unsat => 3
   null_if => 0
   null_member => 0
   null_eq => 0
   null_negate => 0
   null_choice => 0
   null_guess => 0
   null_verify => 0

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

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

   choice(z) -{ 1 }-> x :|: z = 1 + x + xs, xs >= 0, x >= 0
   choice(z) -{ 1 }-> choice(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0
   choice(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   eq(z, z') -{ 1 }-> eq(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
   eq(z, z') -{ 1 }-> 2 :|: z = 1, z' = 1
   eq(z, z') -{ 1 }-> 0 :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
   eq(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   guess(z) -{ 1 }-> 1 :|: z = 1
   guess(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   guess(z) -{ 1 }-> 1 + choice(clause) + guess(cnf) :|: cnf >= 0, z = 1 + clause + cnf, clause >= 0
   if(z, z', z'') -{ 1 }-> e :|: z' = t, t >= 0, e >= 0, z = 0, z'' = e
   if(z, z', z'') -{ 1 }-> t :|: z = 2, z' = t, t >= 0, e >= 0, z'' = e
   if(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   member(z, z') -{ 1 }-> if(eq(x, y), 2, member(x, ys)) :|: ys >= 0, x >= 0, y >= 0, z = x, z' = 1 + y + ys
   member(z, z') -{ 1 }-> 0 :|: x >= 0, z' = 1, z = x
   member(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   negate(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   negate(z) -{ 1 }-> 1 + x :|: x >= 0, z = 1 + x
   sat(z) -{ 1 }-> satck(cnf, guess(cnf)) :|: cnf >= 0, z = cnf
   satck(z, z') -{ 1 }-> if(verify(assign), assign, 3) :|: cnf >= 0, z' = assign, z = cnf, assign >= 0
   verify(z) -{ 1 }-> if(member(negate(l), ls), 0, verify(ls)) :|: l >= 0, ls >= 0, z = 1 + l + ls
   verify(z) -{ 1 }-> 2 :|: z = 1
   verify(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

Only complete derivations are relevant for the runtime complexity.

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

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

eq(start(V3, V1, V4),0,[if(V3, V1, V4, Out)],[V3 >= 0,V1 >= 0,V4 >= 0]).
eq(start(V3, V1, V4),0,[member(V3, V1, Out)],[V3 >= 0,V1 >= 0]).
eq(start(V3, V1, V4),0,[eq(V3, V1, Out)],[V3 >= 0,V1 >= 0]).
eq(start(V3, V1, V4),0,[negate(V3, Out)],[V3 >= 0]).
eq(start(V3, V1, V4),0,[choice(V3, Out)],[V3 >= 0]).
eq(start(V3, V1, V4),0,[guess(V3, Out)],[V3 >= 0]).
eq(start(V3, V1, V4),0,[verify(V3, Out)],[V3 >= 0]).
eq(start(V3, V1, V4),0,[sat(V3, Out)],[V3 >= 0]).
eq(start(V3, V1, V4),0,[satck(V3, V1, Out)],[V3 >= 0,V1 >= 0]).
eq(if(V3, V1, V4, Out),1,[],[Out = V2,V3 = 2,V1 = V2,V2 >= 0,V >= 0,V4 = V]).
eq(if(V3, V1, V4, Out),1,[],[Out = V5,V1 = V6,V6 >= 0,V5 >= 0,V3 = 0,V4 = V5]).
eq(member(V3, V1, Out),1,[],[Out = 0,V7 >= 0,V1 = 1,V3 = V7]).
eq(member(V3, V1, Out),1,[eq(V8, V10, Ret0),member(V8, V9, Ret2),if(Ret0, 2, Ret2, Ret)],[Out = Ret,V9 >= 0,V8 >= 0,V10 >= 0,V3 = V8,V1 = 1 + V10 + V9]).
eq(eq(V3, V1, Out),1,[],[Out = 2,V3 = 1,V1 = 1]).
eq(eq(V3, V1, Out),1,[eq(V11, V12, Ret1)],[Out = Ret1,V1 = 1 + V12,V11 >= 0,V12 >= 0,V3 = 1 + V11]).
eq(eq(V3, V1, Out),1,[],[Out = 0,V1 = 1 + V14,V13 >= 0,V14 >= 0,V3 = 1 + V13]).
eq(negate(V3, Out),1,[],[Out = 1 + V15,V15 >= 0,V3 = 1 + V15]).
eq(choice(V3, Out),1,[],[Out = V16,V3 = 1 + V16 + V17,V17 >= 0,V16 >= 0]).
eq(choice(V3, Out),1,[choice(V19, Ret3)],[Out = Ret3,V3 = 1 + V18 + V19,V19 >= 0,V18 >= 0]).
eq(guess(V3, Out),1,[],[Out = 1,V3 = 1]).
eq(guess(V3, Out),1,[choice(V20, Ret01),guess(V21, Ret11)],[Out = 1 + Ret01 + Ret11,V21 >= 0,V3 = 1 + V20 + V21,V20 >= 0]).
eq(verify(V3, Out),1,[],[Out = 2,V3 = 1]).
eq(verify(V3, Out),1,[negate(V23, Ret00),member(Ret00, V22, Ret02),verify(V22, Ret21),if(Ret02, 0, Ret21, Ret4)],[Out = Ret4,V23 >= 0,V22 >= 0,V3 = 1 + V22 + V23]).
eq(sat(V3, Out),1,[guess(V24, Ret12),satck(V24, Ret12, Ret5)],[Out = Ret5,V24 >= 0,V3 = V24]).
eq(satck(V3, V1, Out),1,[verify(V25, Ret03),if(Ret03, V25, 3, Ret6)],[Out = Ret6,V26 >= 0,V1 = V25,V3 = V26,V25 >= 0]).
eq(if(V3, V1, V4, Out),0,[],[Out = 0,V28 >= 0,V4 = V29,V27 >= 0,V3 = V28,V1 = V27,V29 >= 0]).
eq(member(V3, V1, Out),0,[],[Out = 0,V31 >= 0,V30 >= 0,V3 = V31,V1 = V30]).
eq(eq(V3, V1, Out),0,[],[Out = 0,V33 >= 0,V32 >= 0,V3 = V33,V1 = V32]).
eq(negate(V3, Out),0,[],[Out = 0,V34 >= 0,V3 = V34]).
eq(choice(V3, Out),0,[],[Out = 0,V35 >= 0,V3 = V35]).
eq(guess(V3, Out),0,[],[Out = 0,V36 >= 0,V3 = V36]).
eq(verify(V3, Out),0,[],[Out = 0,V37 >= 0,V3 = V37]).
input_output_vars(if(V3,V1,V4,Out),[V3,V1,V4],[Out]).
input_output_vars(member(V3,V1,Out),[V3,V1],[Out]).
input_output_vars(eq(V3,V1,Out),[V3,V1],[Out]).
input_output_vars(negate(V3,Out),[V3],[Out]).
input_output_vars(choice(V3,Out),[V3],[Out]).
input_output_vars(guess(V3,Out),[V3],[Out]).
input_output_vars(verify(V3,Out),[V3],[Out]).
input_output_vars(sat(V3,Out),[V3],[Out]).
input_output_vars(satck(V3,V1,Out),[V3,V1],[Out]).


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

#### Computed strongly connected components 
0. recursive  : [choice/2]
1. recursive  : [eq/3]
2. recursive  : [guess/2]
3. non_recursive  : [if/4]
4. recursive [non_tail] : [member/3]
5. non_recursive  : [negate/2]
6. recursive [non_tail] : [verify/2]
7. non_recursive  : [satck/3]
8. non_recursive  : [sat/2]
9. non_recursive  : [start/3]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into choice/2
1. SCC is partially evaluated into eq/3
2. SCC is partially evaluated into guess/2
3. SCC is partially evaluated into if/4
4. SCC is partially evaluated into member/3
5. SCC is partially evaluated into negate/2
6. SCC is partially evaluated into verify/2
7. SCC is partially evaluated into satck/3
8. SCC is partially evaluated into sat/2
9. SCC is partially evaluated into start/3

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

### Specialization of cost equations choice/2 
* CE 22 is refined into CE [33] 
* CE 24 is refined into CE [34] 
* CE 23 is refined into CE [35] 


### Cost equations --> "Loop" of choice/2 
* CEs [35] --> Loop 23 
* CEs [33] --> Loop 24 
* CEs [34] --> Loop 25 

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

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


### Specialization of cost equations eq/3 
* CE 18 is refined into CE [36] 
* CE 19 is refined into CE [37] 
* CE 16 is refined into CE [38] 
* CE 17 is refined into CE [39] 


### Cost equations --> "Loop" of eq/3 
* CEs [39] --> Loop 26 
* CEs [36,37] --> Loop 27 
* CEs [38] --> Loop 28 

### Ranking functions of CR eq(V3,V1,Out) 
* RF of phase [26]: [V1,V3]

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


### Specialization of cost equations guess/2 
* CE 27 is refined into CE [40] 
* CE 25 is refined into CE [41] 
* CE 26 is refined into CE [42,43] 


### Cost equations --> "Loop" of guess/2 
* CEs [43] --> Loop 29 
* CEs [42] --> Loop 30 
* CEs [40] --> Loop 31 
* CEs [41] --> Loop 32 

### Ranking functions of CR guess(V3,Out) 
* RF of phase [29,30]: [V3]

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


### Specialization of cost equations if/4 
* CE 12 is refined into CE [44] 
* CE 10 is refined into CE [45] 
* CE 11 is refined into CE [46] 


### Cost equations --> "Loop" of if/4 
* CEs [44] --> Loop 33 
* CEs [45] --> Loop 34 
* CEs [46] --> Loop 35 

### Ranking functions of CR if(V3,V1,V4,Out) 

#### Partial ranking functions of CR if(V3,V1,V4,Out) 


### Specialization of cost equations member/3 
* CE 13 is refined into CE [47] 
* CE 15 is refined into CE [48] 
* CE 14 is refined into CE [49,50,51,52,53,54] 


### Cost equations --> "Loop" of member/3 
* CEs [51] --> Loop 36 
* CEs [53] --> Loop 37 
* CEs [54] --> Loop 38 
* CEs [49] --> Loop 39 
* CEs [50,52] --> Loop 40 
* CEs [47,48] --> Loop 41 

### Ranking functions of CR member(V3,V1,Out) 
* RF of phase [36,37,38,39,40]: [V1]

#### Partial ranking functions of CR member(V3,V1,Out) 
* Partial RF of phase [36,37,38,39,40]:
  - RF of loop [36:1,40:1]:
    V1
  - RF of loop [37:1,38:1]:
    V1/3-2/3
    -V3/3+V1/3
  - RF of loop [39:1]:
    V1/2-1/2


### Specialization of cost equations negate/2 
* CE 20 is refined into CE [55] 
* CE 21 is refined into CE [56] 


### Cost equations --> "Loop" of negate/2 
* CEs [55] --> Loop 42 
* CEs [56] --> Loop 43 

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

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


### Specialization of cost equations verify/2 
* CE 30 is refined into CE [57] 
* CE 28 is refined into CE [58] 
* CE 29 is refined into CE [59,60,61,62,63,64,65,66,67] 


### Cost equations --> "Loop" of verify/2 
* CEs [59,61,63,65] --> Loop 44 
* CEs [60,62,64,66,67] --> Loop 45 
* CEs [57] --> Loop 46 
* CEs [58] --> Loop 47 

### Ranking functions of CR verify(V3,Out) 
* RF of phase [44,45]: [V3]

#### Partial ranking functions of CR verify(V3,Out) 
* Partial RF of phase [44,45]:
  - RF of loop [44:1,45:1]:
    V3


### Specialization of cost equations satck/3 
* CE 32 is refined into CE [68,69,70,71,72,73,74] 


### Cost equations --> "Loop" of satck/3 
* CEs [73] --> Loop 48 
* CEs [70,72] --> Loop 49 
* CEs [68] --> Loop 50 
* CEs [69,71,74] --> Loop 51 

### Ranking functions of CR satck(V3,V1,Out) 

#### Partial ranking functions of CR satck(V3,V1,Out) 


### Specialization of cost equations sat/2 
* CE 31 is refined into CE [75,76,77,78,79,80] 


### Cost equations --> "Loop" of sat/2 
* CEs [78] --> Loop 52 
* CEs [77,80] --> Loop 53 
* CEs [75] --> Loop 54 
* CEs [76,79] --> Loop 55 

### Ranking functions of CR sat(V3,Out) 

#### Partial ranking functions of CR sat(V3,Out) 


### Specialization of cost equations start/3 
* CE 1 is refined into CE [81,82,83] 
* CE 2 is refined into CE [84,85] 
* CE 3 is refined into CE [86,87,88] 
* CE 4 is refined into CE [89,90] 
* CE 5 is refined into CE [91,92] 
* CE 6 is refined into CE [93,94] 
* CE 7 is refined into CE [95,96,97] 
* CE 8 is refined into CE [98,99,100,101] 
* CE 9 is refined into CE [102,103,104,105] 


### Cost equations --> "Loop" of start/3 
* CEs [88] --> Loop 56 
* CEs [102] --> Loop 57 
* CEs [82] --> Loop 58 
* CEs [86,95] --> Loop 59 
* CEs [81,83,84,85,87,89,90,91,92,93,94,96,97,98,99,100,101,103,104,105] --> Loop 60 

### Ranking functions of CR start(V3,V1,V4) 

#### Partial ranking functions of CR start(V3,V1,V4) 


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

#### Cost of chains of choice(V3,Out):
* Chain [[23],25]: 1*it(23)+0
  Such that:it(23) =< V3

  with precondition: [Out=0,V3>=1] 

* Chain [[23],24]: 1*it(23)+1
  Such that:it(23) =< V3-Out

  with precondition: [Out>=0,V3>=Out+2] 

* Chain [25]: 0
  with precondition: [Out=0,V3>=0] 

* Chain [24]: 1
  with precondition: [Out>=0,V3>=Out+1] 


#### Cost of chains of eq(V3,V1,Out):
* Chain [[26],28]: 1*it(26)+1
  Such that:it(26) =< V3

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

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

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

* Chain [28]: 1
  with precondition: [V3=1,V1=1,Out=2] 

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


#### Cost of chains of guess(V3,Out):
* Chain [[29,30],32]: 5*it(29)+1
  Such that:aux(3) =< V3
it(29) =< aux(3)

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

* Chain [[29,30],31]: 5*it(29)+0
  Such that:aux(4) =< V3
it(29) =< aux(4)

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

* Chain [32]: 1
  with precondition: [V3=1,Out=1] 

* Chain [31]: 0
  with precondition: [Out=0,V3>=0] 


#### Cost of chains of if(V3,V1,V4,Out):
* Chain [35]: 1
  with precondition: [V3=0,V4=Out,V1>=0,V4>=0] 

* Chain [34]: 1
  with precondition: [V3=2,V1=Out,V1>=0,V4>=0] 

* Chain [33]: 0
  with precondition: [Out=0,V3>=0,V1>=0,V4>=0] 


#### Cost of chains of member(V3,V1,Out):
* Chain [[36,37,38,39,40],41]: 9*it(36)+5*it(37)+3*it(39)+1
  Such that:aux(6) =< -V3/3+V1/3
it(39) =< V1/2
aux(12) =< V1
aux(13) =< V1/3
it(37) =< aux(6)
it(37) =< aux(13)
it(36) =< aux(12)
it(37) =< aux(12)
it(39) =< aux(12)

  with precondition: [2>=Out,Out>=0,2*V3>=Out,2*V1>=Out+2] 

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


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

* Chain [42]: 1
  with precondition: [V3=Out,V3>=1] 


#### Cost of chains of verify(V3,Out):
* Chain [[44,45],47]: 8*it(44)+15*s(72)+10*s(73)+45*s(74)+5*s(75)+10*s(83)+1
  Such that:aux(23) =< V3/3
aux(33) =< V3
it(44) =< aux(33)
aux(24) =< aux(23)*3
aux(27) =< aux(23)
s(78) =< it(44)*aux(23)
aux(25) =< it(44)*aux(24)
s(86) =< it(44)*aux(27)
s(77) =< aux(25)*(1/3)
s(79) =< aux(25)*(1/2)
s(72) =< s(79)
s(83) =< s(86)
s(83) =< s(77)
s(74) =< aux(25)
s(83) =< aux(25)
s(72) =< aux(25)
s(73) =< s(77)
s(73) =< aux(25)
s(75) =< s(78)
s(75) =< s(77)
s(75) =< aux(25)

  with precondition: [2>=Out,V3>=2,Out>=0] 

* Chain [[44,45],46]: 8*it(44)+15*s(72)+10*s(73)+45*s(74)+5*s(75)+10*s(83)+0
  Such that:aux(23) =< V3/3
aux(34) =< V3
it(44) =< aux(34)
aux(24) =< aux(23)*3
aux(27) =< aux(23)
s(78) =< it(44)*aux(23)
aux(25) =< it(44)*aux(24)
s(86) =< it(44)*aux(27)
s(77) =< aux(25)*(1/3)
s(79) =< aux(25)*(1/2)
s(72) =< s(79)
s(83) =< s(86)
s(83) =< s(77)
s(74) =< aux(25)
s(83) =< aux(25)
s(72) =< aux(25)
s(73) =< s(77)
s(73) =< aux(25)
s(75) =< s(78)
s(75) =< s(77)
s(75) =< aux(25)

  with precondition: [Out=0,V3>=1] 

* Chain [47]: 1
  with precondition: [V3=1,Out=2] 

* Chain [46]: 0
  with precondition: [Out=0,V3>=0] 


#### Cost of chains of satck(V3,V1,Out):
* Chain [51]: 16*s(105)+30*s(113)+20*s(114)+90*s(115)+20*s(116)+10*s(117)+2
  Such that:aux(35) =< V1
aux(36) =< V1/3
s(105) =< aux(35)
s(106) =< aux(36)*3
s(107) =< aux(36)
s(108) =< s(105)*aux(36)
s(109) =< s(105)*s(106)
s(110) =< s(105)*s(107)
s(111) =< s(109)*(1/3)
s(112) =< s(109)*(1/2)
s(113) =< s(112)
s(114) =< s(110)
s(114) =< s(111)
s(115) =< s(109)
s(114) =< s(109)
s(113) =< s(109)
s(116) =< s(111)
s(116) =< s(109)
s(117) =< s(108)
s(117) =< s(111)
s(117) =< s(109)

  with precondition: [Out=0,V3>=0,V1>=0] 

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

* Chain [49]: 16*s(135)+30*s(143)+20*s(144)+90*s(145)+20*s(146)+10*s(147)+3
  Such that:aux(37) =< V1
aux(38) =< V1/3
s(135) =< aux(37)
s(136) =< aux(38)*3
s(137) =< aux(38)
s(138) =< s(135)*aux(38)
s(139) =< s(135)*s(136)
s(140) =< s(135)*s(137)
s(141) =< s(139)*(1/3)
s(142) =< s(139)*(1/2)
s(143) =< s(142)
s(144) =< s(140)
s(144) =< s(141)
s(145) =< s(139)
s(144) =< s(139)
s(143) =< s(139)
s(146) =< s(141)
s(146) =< s(139)
s(147) =< s(138)
s(147) =< s(141)
s(147) =< s(139)

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

* Chain [48]: 8*s(165)+15*s(173)+10*s(174)+45*s(175)+10*s(176)+5*s(177)+3
  Such that:s(164) =< V1
s(163) =< V1/3
s(165) =< s(164)
s(166) =< s(163)*3
s(167) =< s(163)
s(168) =< s(165)*s(163)
s(169) =< s(165)*s(166)
s(170) =< s(165)*s(167)
s(171) =< s(169)*(1/3)
s(172) =< s(169)*(1/2)
s(173) =< s(172)
s(174) =< s(170)
s(174) =< s(171)
s(175) =< s(169)
s(174) =< s(169)
s(173) =< s(169)
s(176) =< s(171)
s(176) =< s(169)
s(177) =< s(168)
s(177) =< s(171)
s(177) =< s(169)

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


#### Cost of chains of sat(V3,Out):
* Chain [55]: 26*s(179)+30*s(190)+20*s(191)+90*s(192)+20*s(193)+10*s(194)+4
  Such that:aux(39) =< V3
s(181) =< V3/3
s(179) =< aux(39)
s(183) =< s(181)*3
s(184) =< s(181)
s(185) =< s(179)*s(181)
s(186) =< s(179)*s(183)
s(187) =< s(179)*s(184)
s(188) =< s(186)*(1/3)
s(189) =< s(186)*(1/2)
s(190) =< s(189)
s(191) =< s(187)
s(191) =< s(188)
s(192) =< s(186)
s(191) =< s(186)
s(190) =< s(186)
s(193) =< s(188)
s(193) =< s(186)
s(194) =< s(185)
s(194) =< s(188)
s(194) =< s(186)

  with precondition: [Out=0,V3>=0] 

* Chain [54]: 10*s(211)+5
  Such that:s(210) =< V3
s(211) =< s(210)

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

* Chain [53]: 26*s(213)+30*s(224)+20*s(225)+90*s(226)+20*s(227)+10*s(228)+5
  Such that:aux(41) =< V3
s(215) =< V3/3
s(213) =< aux(41)
s(217) =< s(215)*3
s(218) =< s(215)
s(219) =< s(213)*s(215)
s(220) =< s(213)*s(217)
s(221) =< s(213)*s(218)
s(222) =< s(220)*(1/3)
s(223) =< s(220)*(1/2)
s(224) =< s(223)
s(225) =< s(221)
s(225) =< s(222)
s(226) =< s(220)
s(225) =< s(220)
s(224) =< s(220)
s(227) =< s(222)
s(227) =< s(220)
s(228) =< s(219)
s(228) =< s(222)
s(228) =< s(220)

  with precondition: [Out=3,V3>=0] 

* Chain [52]: 18*s(245)+15*s(256)+10*s(257)+45*s(258)+10*s(259)+5*s(260)+5
  Such that:s(247) =< V3/3
aux(43) =< V3
s(245) =< aux(43)
s(249) =< s(247)*3
s(250) =< s(247)
s(251) =< s(245)*s(247)
s(252) =< s(245)*s(249)
s(253) =< s(245)*s(250)
s(254) =< s(252)*(1/3)
s(255) =< s(252)*(1/2)
s(256) =< s(255)
s(257) =< s(253)
s(257) =< s(254)
s(258) =< s(252)
s(257) =< s(252)
s(256) =< s(252)
s(259) =< s(254)
s(259) =< s(252)
s(260) =< s(251)
s(260) =< s(254)
s(260) =< s(252)

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


#### Cost of chains of start(V3,V1,V4):
* Chain [60]: 3*s(262)+5*s(265)+50*s(266)+108*s(268)+105*s(282)+70*s(283)+315*s(284)+70*s(285)+35*s(286)+75*s(359)+50*s(360)+225*s(361)+50*s(362)+25*s(363)+5
  Such that:s(261) =< -V3/3+V1/3
s(262) =< V1/2
aux(44) =< V3
aux(45) =< V3/3
aux(46) =< V1
aux(47) =< V1/3
s(268) =< aux(44)
s(266) =< aux(46)
s(275) =< aux(45)*3
s(276) =< aux(45)
s(277) =< s(268)*aux(45)
s(278) =< s(268)*s(275)
s(279) =< s(268)*s(276)
s(280) =< s(278)*(1/3)
s(281) =< s(278)*(1/2)
s(282) =< s(281)
s(283) =< s(279)
s(283) =< s(280)
s(284) =< s(278)
s(283) =< s(278)
s(282) =< s(278)
s(285) =< s(280)
s(285) =< s(278)
s(286) =< s(277)
s(286) =< s(280)
s(286) =< s(278)
s(265) =< s(261)
s(265) =< aux(47)
s(265) =< aux(46)
s(262) =< aux(46)
s(352) =< aux(47)*3
s(353) =< aux(47)
s(354) =< s(266)*aux(47)
s(355) =< s(266)*s(352)
s(356) =< s(266)*s(353)
s(357) =< s(355)*(1/3)
s(358) =< s(355)*(1/2)
s(359) =< s(358)
s(360) =< s(356)
s(360) =< s(357)
s(361) =< s(355)
s(360) =< s(355)
s(359) =< s(355)
s(362) =< s(357)
s(362) =< s(355)
s(363) =< s(354)
s(363) =< s(357)
s(363) =< s(355)

  with precondition: [V3>=0] 

* Chain [59]: 1
  with precondition: [V3=1] 

* Chain [58]: 1
  with precondition: [V3=2,V1>=0,V4>=0] 

* Chain [57]: 3
  with precondition: [V1=1,V3>=0] 

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

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


Closed-form bounds of start(V3,V1,V4): 
-------------------------------------
* Chain [60] with precondition: [V3>=0] 
    - Upper bound: 108*V3+5+V3/3*(2555/2*V3)+nat(V1)*50+1825/2*nat(V1)*nat(V1/3)+nat(-V3/3+V1/3)*5+nat(V1/2)*3 
    - Complexity: n^2 
* Chain [59] with precondition: [V3=1] 
    - Upper bound: 1 
    - Complexity: constant 
* Chain [58] with precondition: [V3=2,V1>=0,V4>=0] 
    - Upper bound: 1 
    - Complexity: constant 
* Chain [57] with precondition: [V1=1,V3>=0] 
    - Upper bound: 3 
    - Complexity: constant 
* Chain [56] with precondition: [V3=V1,V3>=2] 
    - Upper bound: V1+1 
    - Complexity: n 

### Maximum cost of start(V3,V1,V4): max([2,108*V3+4+V3/3*(2555/2*V3)+nat(V1)*49+1825/2*nat(V1)*nat(V1/3)+nat(-V3/3+V1/3)*5+nat(V1/2)*3+nat(V1)])+1 
Asymptotic class: n^2 
* Total analysis performed in 732 ms.


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

(10)
BOUNDS(1, n^2)