warning: Ignored call to f24/3 in equation f17/3 warning: Ignored call to f24/3 in equation f17/3 warning: Ignored call to f24/3 in equation f17/3 Inferred cost of f6(A,B,C,D,E,F,G): f6(A,B,C,D,E,F,G):[25]: 2 with precondition: [C=0,D=0,F=0,G=1,A=E,0>=A+1] f6(A,B,C,D,E,F,G):[26]: 1 with precondition: [C=0,D=1,G=0,A=E,0>=A+1] f6(A,B,C,D,E,F,G):[27]: 2 with precondition: [C=0,D=0,F=0,G=1,A=E,A>=1] f6(A,B,C,D,E,F,G):[28]: 1 with precondition: [C=0,D=1,G=0,A=E,A>=1] f6(A,B,C,D,E,F,G):[29]: 1 with precondition: [A=0,C=0,D=0,E=0,G=0,F=B] f6(A,B,C,D,E,F,G):[30]: 0 with precondition: [C=0,D=1,G=0,E=A,F=B] f6(A,B,C,D,E,F,G):[[21,22,23,24],25]: inf with precondition: [C=0,D=0,F=0,G=1,0>=E+1] f6(A,B,C,D,E,F,G):[[21,22,23,24],26]: inf with precondition: [C=0,D=1,G=0,0>=E+1] f6(A,B,C,D,E,F,G):[[21,22,23,24],27]: inf with precondition: [C=0,D=0,F=0,G=1,E>=1] f6(A,B,C,D,E,F,G):[[21,22,23,24],28]: inf with precondition: [C=0,D=1,G=0,E>=1] f6(A,B,C,D,E,F,G):[[21,22,23,24],29]: inf with precondition: [C=0,D=0,E=0,G=0] f6(A,B,C,D,E,F,G):[[21,22,23,24],30]: inf with precondition: [C=0,D=1,G=0] f6(A,B,C,D,E,F,G):[[21,22,23,24],31]...: inf with precondition: [C=0,1>=D,D>=0] Inferred cost of f17(A,B,C): f17(A,B,C):[32]: 1 with precondition: [0>=C] f17(A,B,C):[33]: 1 with precondition: [C>=2] f17(A,B,C):[34]: 1 with precondition: [C=1] Inferred cost of loop_cont_f6(A,B,C): loop_cont_f6(A,B,C):[36]: 1 with precondition: [0>=C] loop_cont_f6(A,B,C):[37]: 1 with precondition: [C>=2] loop_cont_f6(A,B,C):[38]: 1 with precondition: [C=1] Inferred cost of f0(A,B,C): f0(A,B,C):[40]: 4 with precondition: [] f0(A,B,C):[41]: 4 with precondition: [] f0(A,B,C):[42]: 3 with precondition: [] f0(A,B,C):[43]: inf with precondition: [] f0(A,B,C):[44]: inf with precondition: [] f0(A,B,C):[45]: inf with precondition: [] f0(A,B,C):[46]: 2 with precondition: [] f0(A,B,C):[47]: 2 with precondition: [] f0(A,B,C):[48]: 1 with precondition: [] f0(A,B,C):[49]: inf with precondition: [] f0(A,B,C):[50]: inf with precondition: [] f0(A,B,C):[51]: inf with precondition: [] f0(A,B,C):[52]...: inf with precondition: [] f0(A,B,C):[53]...: inf with precondition: [] Solved cost expressions of f0(A,B,C): f0(A,B,C):[40]: 4 with precondition: [] f0(A,B,C):[41]: 4 with precondition: [] f0(A,B,C):[42]: 3 with precondition: [] f0(A,B,C):[43]: inf with precondition: [] f0(A,B,C):[44]: inf with precondition: [] f0(A,B,C):[45]: inf with precondition: [] f0(A,B,C):[46]: 2 with precondition: [] f0(A,B,C):[47]: 2 with precondition: [] f0(A,B,C):[48]: 1 with precondition: [] f0(A,B,C):[49]: inf with precondition: [] f0(A,B,C):[50]: inf with precondition: [] f0(A,B,C):[51]: inf with precondition: [] f0(A,B,C):[52]...: inf with precondition: [] f0(A,B,C):[53]...: inf with precondition: [] Maximum cost of f0(A,B,C): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 13 ms. Invariants computed in 39 ms. ----Backward Invariants 27 ms. ----Transitive Invariants 2 ms. Refinement performed in 34 ms. Termination proved in 4 ms. Upper bounds computed in 27 ms. ----Phase cost structures 8 ms. --------Equation cost structures 5 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 15 ms. ----Solving cost expressions 0 ms. Compressed phase information: 12 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 132 ms.