warning: Ignored call to f300/4 in equation f1/4 warning: Ignored call to f300/4 in equation f1/4 warning: Ignored call to f300/4 in equation f1/4 warning: Ignored call to loop_cont_f2/4 in equation f1/4 Inferred cost of f2(A,B,C,D,E,F,G,H,I): f2(A,B,C,D,E,F,G,H,I):[11]: 0 with precondition: [E=1,A=B,A=C,I=D,A=F,A=G,A=H] f2(A,B,C,D,E,F,G,H,I):[[10],11]: inf with precondition: [E=1,A=B,G=F,D=I,A+C=G+H,G>=A+1,A>=C] f2(A,B,C,D,E,F,G,H,I):[[10],12]...: inf with precondition: [A=B,1>=E,E>=0,A>=C] Inferred cost of f1(A,B,C,D): f1(A,B,C,D):[13]: 1 with precondition: [B>=A,C>=A+1,C>=B] f1(A,B,C,D):[14]: 1 with precondition: [B>=A,B>=C+1] f1(A,B,C,D):[15]: 1 with precondition: [A>=B+1] f1(A,B,C,D):[16]: 1 with precondition: [A=B,A=C] f1(A,B,C,D):[17]: inf with precondition: [A=B,A=C] f1(A,B,C,D):[18]...: inf with precondition: [A=B,A=C] f1(A,B,C,D):[19]...: inf with precondition: [A=B,A=C] Solved cost expressions of f1(A,B,C,D): f1(A,B,C,D):[13]: 1 with precondition: [B>=A,C>=A+1,C>=B] f1(A,B,C,D):[14]: 1 with precondition: [B>=A,B>=C+1] f1(A,B,C,D):[15]: 1 with precondition: [A>=B+1] f1(A,B,C,D):[16]: 1 with precondition: [A=B,A=C] f1(A,B,C,D):[17]: inf with precondition: [A=B,A=C] f1(A,B,C,D):[18]...: inf with precondition: [A=B,A=C] f1(A,B,C,D):[19]...: inf with precondition: [A=B,A=C] Maximum cost of f1(A,B,C,D): inf Asymptotic class: infinity Time statistics: Partial evaluation computed in 4 ms. Invariants computed in 16 ms. ----Backward Invariants 9 ms. ----Transitive Invariants 1 ms. Refinement performed in 11 ms. Termination proved in 3 ms. Upper bounds computed in 14 ms. ----Phase cost structures 4 ms. --------Equation cost structures 4 ms. --------Inductive compression(1) 0 ms. --------Inductive compression(2) 0 ms. --------Black Cost 0 ms. ----Chain cost structures 7 ms. ----Solving cost expressions 0 ms. Compressed phase information: 1 Compressed Chains: 0 Compressed invariants: 0 Total analysis performed in 58 ms.