warning: Ignored call to evalwcet2stop/2 in equation evalwcet2returnin/2 
Inferred cost of evalwcet2bb2in(A,B,C,D,E): 
evalwcet2bb2in(A,B,C,D,E):[21]: 1
  with precondition: [B=0,C=0,E=0,A=D,2>=A] 

evalwcet2bb2in(A,B,C,D,E):[22]: 0
  with precondition: [B=0,C=1,E=0,A=D,4>=A,A>=3] 

evalwcet2bb2in(A,B,C,D,E):[24]: 0
  with precondition: [B=0,C=1,E=0,A=D,4>=A] 

evalwcet2bb2in(A,B,C,D,E):[[20],22]: 0+it1*(2)
  Such that:it1=<10,it1=<1*E,it1=<-1*B+10,it1=<1*E+ -1*B
  with precondition: [C=1,A=D,4>=A,10>=E,A>=3,B>=0,E>=B+1] 

evalwcet2bb2in(A,B,C,D,E):[[20],23]: 1+it1*(2)
  Such that:it1=<10,it1=<-1*B+10
  with precondition: [C=0,E=10,A=D,4>=A,9>=B,A>=3,B>=0] 

evalwcet2bb2in(A,B,C,D,E):[[20],24]: 0+it1*(2)
  Such that:it1=<9,it1=<10,it1=<1*E,it1=<-1*B+10,it1=<1*E+ -1*B
  with precondition: [C=1,A=D,4>=A,9>=E,A>=3,B>=0,E>=B+1] 

Inferred cost of evalwcet2bb5in(A,B,C,D,E): 
evalwcet2bb5in(A,B,C,D,E):[28]: 1
  with precondition: [C=1,4>=A,A>=3] 

evalwcet2bb5in(A,B,C,D,E):[29]: 1
  with precondition: [C=1,4>=A] 

evalwcet2bb5in(A,B,C,D,E):[30]: 1+it1*(2)
  Such that:it1=<10
  with precondition: [C=1,4>=A,A>=3] 

evalwcet2bb5in(A,B,C,D,E):[31]: 1+it1*(2)
  Such that:it1=<9,it1=<10
  with precondition: [C=1,4>=A,A>=3] 

evalwcet2bb5in(A,B,C,D,E):[32]: 1
  with precondition: [C=0,E=B,A=D,A>=5] 

evalwcet2bb5in(A,B,C,D,E):[[26],[27],28]: 1+it1*(3+it2*(2))+it3*(3)
  Such that:it1=<1,it1=<2,it3=<-1*A+3
            it2=<10
  with precondition: [C=1,2>=A] 

evalwcet2bb5in(A,B,C,D,E):[[26],[27],29]: 1+it1*(3+it2*(2))+it3*(3)
  Such that:it1=<1,it1=<2,it3=<-1*A+3
            it2=<10
  with precondition: [C=1,2>=A] 

evalwcet2bb5in(A,B,C,D,E):[[26],[27],30]: 1+it1*(2)+it2*(3+it3*(2))+it4*(3)
  Such that:it1=<10,it2=<1,it2=<2,it4=<-1*A+3
            it3=<10
  with precondition: [C=1,2>=A] 

evalwcet2bb5in(A,B,C,D,E):[[26],[27],31]: 1+it1*(2)+it2*(3+it3*(2))+it4*(3)
  Such that:it1=<9,it1=<10,it2=<1,it2=<2,it4=<-1*A+3
            it3=<10
  with precondition: [C=1,2>=A] 

evalwcet2bb5in(A,B,C,D,E):[[26],[27],32]: 1+it1*(3+it2*(2))+it3*(3)
  Such that:it1=<2,it3=<-1*A+3
            it2=<10
  with precondition: [C=0,D=5,E=10,2>=A] 

evalwcet2bb5in(A,B,C,D,E):[[26],28]: 1+it1*(3)
  Such that:it1=<-1*A+3
  with precondition: [C=1,2>=A] 

evalwcet2bb5in(A,B,C,D,E):[[26],29]: 1+it1*(3)
  Such that:it1=<-1*A+3
  with precondition: [C=1,2>=A] 

evalwcet2bb5in(A,B,C,D,E):[[26],30]: 1+it1*(2)+it2*(3)
  Such that:it1=<10,it2=<-1*A+3
  with precondition: [C=1,2>=A] 

evalwcet2bb5in(A,B,C,D,E):[[26],31]: 1+it1*(2)+it2*(3)
  Such that:it1=<9,it1=<10,it2=<-1*A+3
  with precondition: [C=1,2>=A] 

evalwcet2bb5in(A,B,C,D,E):[[27],28]: 1+it1*(3+it2*(2))
  Such that:it1=<1,it1=<2
            it2=<10
  with precondition: [A=3,C=1] 

evalwcet2bb5in(A,B,C,D,E):[[27],29]: 1+it1*(3+it2*(2))
  Such that:it1=<1,it1=<2
            it2=<10
  with precondition: [A=3,C=1] 

evalwcet2bb5in(A,B,C,D,E):[[27],30]: 1+it1*(2)+it2*(3+it3*(2))
  Such that:it1=<10,it2=<1,it2=<2
            it3=<10
  with precondition: [A=3,C=1] 

evalwcet2bb5in(A,B,C,D,E):[[27],31]: 1+it1*(2)+it2*(3+it3*(2))
  Such that:it1=<9,it1=<10,it2=<1,it2=<2
            it3=<10
  with precondition: [A=3,C=1] 

evalwcet2bb5in(A,B,C,D,E):[[27],32]: 1+it1*(3+it2*(2))
  Such that:it1=<2,it1=<-1*A+5
            it2=<10
  with precondition: [C=0,D=5,E=10,4>=A,A>=3] 

Inferred cost of evalwcet2returnin(A,B): 
evalwcet2returnin(A,B):[34]: 1
  with precondition: [] 

Inferred cost of loop_cont_evalwcet2bb5in(A,B): 
loop_cont_evalwcet2bb5in(A,B):[36]: 1
  with precondition: [] 

Inferred cost of evalwcet2entryin(A,B): 
evalwcet2entryin(A,B):[38]: 3
  with precondition: [A>=5] 

evalwcet2entryin(A,B):[39]: 3+it1*(3+it2*(2))+it3*(3)
  Such that:it1=<2,it3=<-1*A+3
            it2=<10
  with precondition: [2>=A] 

evalwcet2entryin(A,B):[40]: 3+it1*(3+it2*(2))
  Such that:it1=<2,it1=<-1*A+5
            it2=<10
  with precondition: [4>=A,A>=3] 

evalwcet2entryin(A,B):[41]: 2
  with precondition: [4>=A,A>=3] 

evalwcet2entryin(A,B):[42]: 2
  with precondition: [4>=A] 

evalwcet2entryin(A,B):[43]: 2+it1*(2)
  Such that:it1=<10
  with precondition: [4>=A,A>=3] 

evalwcet2entryin(A,B):[44]: 2+it1*(2)
  Such that:it1=<9,it1=<10
  with precondition: [4>=A,A>=3] 

evalwcet2entryin(A,B):[45]: 2+it1*(3+it2*(2))+it3*(3)
  Such that:it1=<1,it1=<2,it3=<-1*A+3
            it2=<10
  with precondition: [2>=A] 

evalwcet2entryin(A,B):[46]: 2+it1*(3+it2*(2))+it3*(3)
  Such that:it1=<1,it1=<2,it3=<-1*A+3
            it2=<10
  with precondition: [2>=A] 

evalwcet2entryin(A,B):[47]: 2+it1*(2)+it2*(3+it3*(2))+it4*(3)
  Such that:it1=<10,it2=<1,it2=<2,it4=<-1*A+3
            it3=<10
  with precondition: [2>=A] 

evalwcet2entryin(A,B):[48]: 2+it1*(2)+it2*(3+it3*(2))+it4*(3)
  Such that:it1=<9,it1=<10,it2=<1,it2=<2,it4=<-1*A+3
            it3=<10
  with precondition: [2>=A] 

evalwcet2entryin(A,B):[49]: 2+it1*(3)
  Such that:it1=<-1*A+3
  with precondition: [2>=A] 

evalwcet2entryin(A,B):[50]: 2+it1*(3)
  Such that:it1=<-1*A+3
  with precondition: [2>=A] 

evalwcet2entryin(A,B):[51]: 2+it1*(2)+it2*(3)
  Such that:it1=<10,it2=<-1*A+3
  with precondition: [2>=A] 

evalwcet2entryin(A,B):[52]: 2+it1*(2)+it2*(3)
  Such that:it1=<9,it1=<10,it2=<-1*A+3
  with precondition: [2>=A] 

evalwcet2entryin(A,B):[53]: 2+it1*(3+it2*(2))
  Such that:it1=<1,it1=<2
            it2=<10
  with precondition: [A=3] 

evalwcet2entryin(A,B):[54]: 2+it1*(3+it2*(2))
  Such that:it1=<1,it1=<2
            it2=<10
  with precondition: [A=3] 

evalwcet2entryin(A,B):[55]: 2+it1*(2)+it2*(3+it3*(2))
  Such that:it1=<10,it2=<1,it2=<2
            it3=<10
  with precondition: [A=3] 

evalwcet2entryin(A,B):[56]: 2+it1*(2)+it2*(3+it3*(2))
  Such that:it1=<9,it1=<10,it2=<1,it2=<2
            it3=<10
  with precondition: [A=3] 

Inferred cost of evalwcet2start(A,B): 
evalwcet2start(A,B):[58]: 4
  with precondition: [A>=5] 

evalwcet2start(A,B):[59]: 4+it1*(3+it2*(2))+it3*(3)
  Such that:it1=<2,it3=<-1*A+3
            it2=<10
  with precondition: [2>=A] 

evalwcet2start(A,B):[60]: 4+it1*(3+it2*(2))
  Such that:it1=<2,it1=<-1*A+5
            it2=<10
  with precondition: [4>=A,A>=3] 

evalwcet2start(A,B):[61]: 3
  with precondition: [4>=A,A>=3] 

evalwcet2start(A,B):[62]: 3
  with precondition: [4>=A] 

evalwcet2start(A,B):[63]: 3+it1*(2)
  Such that:it1=<10
  with precondition: [4>=A,A>=3] 

evalwcet2start(A,B):[64]: 3+it1*(2)
  Such that:it1=<9,it1=<10
  with precondition: [4>=A,A>=3] 

evalwcet2start(A,B):[65]: 3+it1*(3+it2*(2))+it3*(3)
  Such that:it1=<1,it1=<2,it3=<-1*A+3
            it2=<10
  with precondition: [2>=A] 

evalwcet2start(A,B):[66]: 3+it1*(3+it2*(2))+it3*(3)
  Such that:it1=<1,it1=<2,it3=<-1*A+3
            it2=<10
  with precondition: [2>=A] 

evalwcet2start(A,B):[67]: 3+it1*(2)+it2*(3+it3*(2))+it4*(3)
  Such that:it1=<10,it2=<1,it2=<2,it4=<-1*A+3
            it3=<10
  with precondition: [2>=A] 

evalwcet2start(A,B):[68]: 3+it1*(2)+it2*(3+it3*(2))+it4*(3)
  Such that:it1=<9,it1=<10,it2=<1,it2=<2,it4=<-1*A+3
            it3=<10
  with precondition: [2>=A] 

evalwcet2start(A,B):[69]: 3+it1*(3)
  Such that:it1=<-1*A+3
  with precondition: [2>=A] 

evalwcet2start(A,B):[70]: 3+it1*(3)
  Such that:it1=<-1*A+3
  with precondition: [2>=A] 

evalwcet2start(A,B):[71]: 3+it1*(2)+it2*(3)
  Such that:it1=<10,it2=<-1*A+3
  with precondition: [2>=A] 

evalwcet2start(A,B):[72]: 3+it1*(2)+it2*(3)
  Such that:it1=<9,it1=<10,it2=<-1*A+3
  with precondition: [2>=A] 

evalwcet2start(A,B):[73]: 3+it1*(3+it2*(2))
  Such that:it1=<1,it1=<2
            it2=<10
  with precondition: [A=3] 

evalwcet2start(A,B):[74]: 3+it1*(3+it2*(2))
  Such that:it1=<1,it1=<2
            it2=<10
  with precondition: [A=3] 

evalwcet2start(A,B):[75]: 3+it1*(2)+it2*(3+it3*(2))
  Such that:it1=<10,it2=<1,it2=<2
            it3=<10
  with precondition: [A=3] 

evalwcet2start(A,B):[76]: 3+it1*(2)+it2*(3+it3*(2))
  Such that:it1=<9,it1=<10,it2=<1,it2=<2
            it3=<10
  with precondition: [A=3] 

Solved cost expressions of evalwcet2start(A,B): 
evalwcet2start(A,B):[58]: 4  with precondition: [A>=5] 
evalwcet2start(A,B):[59]: -3*A+59  with precondition: [2>=A] 
evalwcet2start(A,B):[60]: -23*A+119  with precondition: [4>=A,A>=3] 
evalwcet2start(A,B):[61]: 3  with precondition: [4>=A,A>=3] 
evalwcet2start(A,B):[62]: 3  with precondition: [4>=A] 
evalwcet2start(A,B):[63]: 23  with precondition: [4>=A,A>=3] 
evalwcet2start(A,B):[64]: 21  with precondition: [4>=A,A>=3] 
evalwcet2start(A,B):[65]: -3*A+35  with precondition: [2>=A] 
evalwcet2start(A,B):[66]: -3*A+35  with precondition: [2>=A] 
evalwcet2start(A,B):[67]: -3*A+55  with precondition: [2>=A] 
evalwcet2start(A,B):[68]: -3*A+53  with precondition: [2>=A] 
evalwcet2start(A,B):[69]: -3*A+12  with precondition: [2>=A] 
evalwcet2start(A,B):[70]: -3*A+12  with precondition: [2>=A] 
evalwcet2start(A,B):[71]: -3*A+32  with precondition: [2>=A] 
evalwcet2start(A,B):[72]: -3*A+30  with precondition: [2>=A] 
evalwcet2start(A,B):[73]: 26  with precondition: [A=3] 
evalwcet2start(A,B):[74]: 26  with precondition: [A=3] 
evalwcet2start(A,B):[75]: 46  with precondition: [A=3] 
evalwcet2start(A,B):[76]: 44  with precondition: [A=3] 
Maximum cost of evalwcet2start(A,B): max([-3*A+59,46,-23*A+119]) 
Asymptotic class: n 
Time statistics: 
Partial evaluation computed in 7 ms.
Invariants computed in 77 ms.
----Backward Invariants 51 ms.
----Transitive Invariants 3 ms.
Refinement performed in 41 ms.
Termination proved in 6 ms.
Upper bounds computed in 122 ms.
----Phase cost structures 30 ms.
--------Equation cost structures 28 ms.
--------Inductive compression(1) 0 ms.
--------Inductive compression(2) 0 ms.
--------Black Cost 0 ms.
----Chain cost structures 74 ms.
----Solving cost expressions 4 ms.

Compressed phase information: 27 
Compressed Chains: 0 
Compressed invariants: 0 
Total analysis performed in 268 ms.