(*************************************************************)
(*      This file is distributed under the terms of the      *)
(*      GNU Lesser General Public License Version 2.1        *)
(*************************************************************)
(*    Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr      *)
(*************************************************************)

Require Import Lucas.

Eval vm_compute in 2.

Time Eval vm_compute in lucas 2.

Eval vm_compute in 3.

Time Eval vm_compute in lucas 3.

Eval vm_compute in 5.

Time Eval vm_compute in lucas 5.

Eval vm_compute in 7.

Time Eval vm_compute in lucas 7.

Eval vm_compute in 13.

Time Eval vm_compute in lucas 13.

Eval vm_compute in 17.

Time Eval vm_compute in lucas 17.

Eval vm_compute in 19.

Time Eval vm_compute in lucas 19.

Eval vm_compute in 31.

Time Eval vm_compute in lucas 31.

Eval vm_compute in 61.

Time Eval vm_compute in lucas 61.

Eval vm_compute in 89.

Time Eval vm_compute in lucas 89.

Eval vm_compute in 107.

Time Eval vm_compute in lucas 107.

Eval vm_compute in 127.

Time Eval vm_compute in lucas 127.

Eval vm_compute in 521.

Time Eval vm_compute in lucas 521.

Eval vm_compute in 607.

Time Eval vm_compute in lucas 607.

Eval vm_compute in 1279.

Time Eval vm_compute in lucas 1279.

Eval vm_compute in 2203.

Time Eval vm_compute in lucas 2203.

Eval vm_compute in 2281.

Time Eval vm_compute in lucas 2281.

Eval vm_compute in 3217.

Time Eval vm_compute in lucas 3217.

Eval vm_compute in 4253.

Time Eval vm_compute in lucas 4253.

Eval vm_compute in 4423.

Time Eval vm_compute in lucas 4423.

(*
     = 3
     = 0
Finished transaction in 0. secs (0.01u,0.s)
     = 5
     = 0
Finished transaction in 0. secs (0.u,0.s)
     = 7
     = 0
Finished transaction in 0. secs (0.u,0.s)
     = 13
     = 0
Finished transaction in 0. secs (0.u,0.s)
     = 17
     = 0
Finished transaction in 0. secs (0.u,0.s)
     = 19
     = 0
Finished transaction in 0. secs (0.u,0.s)
     = 31
     = 0
Finished transaction in 0. secs (0.u,0.s)
     = 61
     = 0
Finished transaction in 0. secs (0.01u,0.s)
     = 89
     = 0
Finished transaction in 0. secs (0.02u,0.s)
     = 107
     = 0
Finished transaction in 0. secs (0.02u,0.s)
     = 127
     = 0
Finished transaction in 0. secs (0.04u,0.s)
     = 521
     = 0
Finished transaction in 2. secs (1.85u,0.01s)
     = 607
     = 0
Finished transaction in 3. secs (2.78u,0.07s)
     = 1279
     = 0
Finished transaction in 21. secs (20.21u,0.26s)
     = 2203
     = 0
Finished transaction in 94. secs (89.1u,1.05s)
     = 2281
     = 0
Finished transaction in 102. secs (97.59u,1.1s)
     = 3217
     = 0
Finished transaction in 244. secs (237.65u,2.39s)
     = 4253
     = 0
Finished transaction in 506. secs (494.09u,4.65s)
     = 4423
     = 0
Finished transaction in 572. secs (563.27u,5.45s)


*)