289 lines
12 KiB
Solidity
289 lines
12 KiB
Solidity
% init_area = 5256656;
|
|
objective = 15791;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 1, 2, 1, 1, 2, 1, 1, 2, 2, 2, 2];
|
|
% time elapsed: 0.05 s
|
|
----------
|
|
objective = 15360;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 1, 2, 1, 1, 2, 1, 1, 2, 2, 3, 2];
|
|
% time elapsed: 0.06 s
|
|
----------
|
|
objective = 15359;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 1, 2, 1, 1, 2, 1, 1, 2, 2, 4, 2];
|
|
% time elapsed: 0.06 s
|
|
----------
|
|
objective = 15000;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 1, 2, 1, 1, 2, 1, 1, 2, 3, 4, 2];
|
|
% time elapsed: 0.07 s
|
|
----------
|
|
objective = 14999;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 1, 2, 1, 1, 2, 1, 1, 2, 4, 4, 2];
|
|
% time elapsed: 0.07 s
|
|
----------
|
|
objective = 14206;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 4, 4, 2];
|
|
% time elapsed: 0.07 s
|
|
----------
|
|
objective = 13990;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 1, 2, 2, 2, 2, 1, 1, 2, 4, 4, 2];
|
|
% time elapsed: 0.08 s
|
|
----------
|
|
objective = 13919;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 1, 2, 2, 3, 2, 1, 1, 2, 2, 3, 2];
|
|
% time elapsed: 0.08 s
|
|
----------
|
|
objective = 12982;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 2, 2, 2, 3, 2, 1, 1, 2, 2, 3, 2];
|
|
% time elapsed: 0.08 s
|
|
----------
|
|
objective = 12693;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 2, 2, 2, 3, 2, 1, 1, 2, 2, 4, 2];
|
|
% time elapsed: 0.09 s
|
|
----------
|
|
objective = 12406;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 2, 2, 2, 2, 3, 2, 1, 1, 2, 2, 4, 2];
|
|
% time elapsed: 0.09 s
|
|
----------
|
|
objective = 12263;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 2, 2, 3, 4, 2, 1, 1, 2, 2, 5, 2];
|
|
% time elapsed: 0.10 s
|
|
----------
|
|
objective = 11975;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 3, 2, 3, 4, 2, 1, 1, 2, 2, 5, 2];
|
|
% time elapsed: 0.10 s
|
|
----------
|
|
objective = 11616;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 1, 3, 2, 3, 4, 2, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 0.11 s
|
|
----------
|
|
objective = 11542;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 2, 3, 2, 2, 3, 2, 1, 1, 2, 2, 4, 2];
|
|
% time elapsed: 0.11 s
|
|
----------
|
|
objective = 11399;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 2, 3, 2, 3, 3, 2, 1, 1, 2, 2, 4, 2];
|
|
% time elapsed: 0.12 s
|
|
----------
|
|
objective = 10967;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 3, 3, 2, 3, 3, 2, 1, 1, 2, 2, 4, 2];
|
|
% time elapsed: 0.12 s
|
|
----------
|
|
objective = 10606;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 3, 3, 2, 3, 3, 2, 1, 1, 2, 2, 4, 2];
|
|
% time elapsed: 0.13 s
|
|
----------
|
|
objective = 10175;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 3, 1, 2, 3, 3, 2, 3, 3, 2, 1, 1, 2, 2, 4, 2];
|
|
% time elapsed: 0.13 s
|
|
----------
|
|
objective = 10030;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 3, 2, 2, 3, 5, 2, 1, 1, 2, 2, 4, 2];
|
|
% time elapsed: 0.14 s
|
|
----------
|
|
objective = 9599;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 3, 1, 2, 3, 2, 2, 3, 5, 2, 1, 1, 2, 2, 4, 2];
|
|
% time elapsed: 0.14 s
|
|
----------
|
|
objective = 9529;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 3, 1, 1, 3, 4, 2, 3, 5, 2, 1, 1, 2, 2, 4, 2];
|
|
% time elapsed: 0.15 s
|
|
----------
|
|
objective = 9528;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 4, 1, 1, 3, 4, 2, 3, 5, 2, 1, 1, 2, 2, 4, 2];
|
|
% time elapsed: 0.15 s
|
|
----------
|
|
objective = 9527;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 1, 3, 5, 3, 4, 3, 2, 1, 1, 2, 2, 5, 2];
|
|
% time elapsed: 0.18 s
|
|
----------
|
|
objective = 8806;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 1, 2, 3, 5, 3, 4, 3, 2, 1, 1, 2, 2, 5, 2];
|
|
% time elapsed: 0.18 s
|
|
----------
|
|
objective = 8519;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 3, 1, 2, 3, 5, 3, 4, 3, 2, 1, 1, 2, 2, 5, 2];
|
|
% time elapsed: 0.18 s
|
|
----------
|
|
objective = 8231;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 3, 2, 3, 1, 2, 3, 5, 3, 4, 3, 2, 1, 1, 2, 2, 5, 2];
|
|
% time elapsed: 0.21 s
|
|
----------
|
|
objective = 7512;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 3, 2, 3, 1, 4, 3, 5, 3, 4, 3, 2, 1, 1, 2, 2, 5, 2];
|
|
% time elapsed: 0.22 s
|
|
----------
|
|
objective = 6936;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 4, 3, 2, 3, 1, 4, 3, 5, 3, 4, 3, 2, 1, 1, 2, 2, 5, 2];
|
|
% time elapsed: 0.22 s
|
|
----------
|
|
objective = 6862;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 4, 1, 2, 1, 1, 4, 3, 5, 5, 4, 3, 2, 1, 1, 2, 2, 5, 2];
|
|
% time elapsed: 0.23 s
|
|
----------
|
|
objective = 6575;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 4, 1, 2, 3, 1, 4, 3, 5, 5, 4, 3, 2, 1, 1, 2, 2, 5, 2];
|
|
% time elapsed: 0.24 s
|
|
----------
|
|
objective = 6216;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 4, 1, 2, 3, 1, 4, 3, 5, 5, 4, 3, 2, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 0.25 s
|
|
----------
|
|
objective = 5928;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 4, 3, 2, 3, 1, 4, 3, 5, 5, 4, 3, 2, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 0.26 s
|
|
----------
|
|
objective = 5927;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 1, 2, 2, 4, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 0.27 s
|
|
----------
|
|
objective = 5711;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 4, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 0.27 s
|
|
----------
|
|
objective = 5496;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 3, 2, 2, 4, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 0.28 s
|
|
----------
|
|
objective = 5495;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 0.28 s
|
|
----------
|
|
objective = 5136;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 1, 2, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 4, 3, 5, 2];
|
|
% time elapsed: 0.29 s
|
|
----------
|
|
objective = 4705;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 2, 2, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 4, 3, 5, 2];
|
|
% time elapsed: 0.31 s
|
|
----------
|
|
objective = 4418;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 2, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 4, 3, 5, 2];
|
|
% time elapsed: 0.32 s
|
|
----------
|
|
objective = 4201;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 1, 4, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 4, 3, 5, 2];
|
|
% time elapsed: 0.32 s
|
|
----------
|
|
objective = 3625;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 1, 2, 4, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 4, 3, 5, 2];
|
|
% time elapsed: 0.67 s
|
|
----------
|
|
objective = 3337;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 1, 2, 2, 4, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 4, 3, 5, 2];
|
|
% time elapsed: 0.83 s
|
|
----------
|
|
objective = 3049;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 4, 2, 2, 4, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 4, 3, 5, 2];
|
|
% time elapsed: 0.83 s
|
|
----------
|
|
objective = 2905;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 4, 1, 2, 4, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 4, 3, 5, 2];
|
|
% time elapsed: 1.00 s
|
|
----------
|
|
objective = 2762;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 4, 1, 2, 5, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 4, 3, 5, 2];
|
|
% time elapsed: 1.01 s
|
|
----------
|
|
objective = 2330;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 4, 4, 2, 5, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 5, 4, 3, 2, 1, 1, 4, 3, 5, 2];
|
|
% time elapsed: 1.43 s
|
|
----------
|
|
objective = 2329;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 4, 4, 2, 6, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 4, 4, 3, 2, 1, 1, 4, 3, 5, 2];
|
|
% time elapsed: 1.64 s
|
|
----------
|
|
objective = 2257;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 4, 5, 2, 6, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 4, 3, 3, 2, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 1.77 s
|
|
----------
|
|
objective = 2113;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 4, 5, 4, 6, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 4, 3, 3, 2, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 1.82 s
|
|
----------
|
|
objective = 1968;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 1, 1, 1, 4, 5, 4, 6, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 4, 3, 3, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 1.98 s
|
|
----------
|
|
objective = 1608;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 4, 5, 4, 6, 3, 3, 2, 2, 6, 3, 2, 3, 1, 5, 3, 5, 4, 3, 3, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 1.98 s
|
|
----------
|
|
objective = 1537;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 4, 5, 4, 6, 3, 3, 6, 2, 6, 3, 2, 3, 1, 5, 3, 5, 4, 3, 3, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 2.01 s
|
|
----------
|
|
objective = 1534;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 4, 5, 4, 6, 1, 2, 6, 2, 6, 3, 2, 1, 1, 5, 3, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 2.14 s
|
|
----------
|
|
objective = 1463;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 4, 5, 4, 6, 1, 3, 6, 2, 6, 3, 2, 1, 1, 5, 3, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 2.16 s
|
|
----------
|
|
objective = 1462;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 4, 5, 4, 6, 1, 3, 6, 2, 6, 3, 2, 1, 1, 5, 4, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 2.30 s
|
|
----------
|
|
objective = 1246;
|
|
period_of = [1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 4, 5, 4, 6, 2, 3, 6, 2, 6, 3, 2, 1, 1, 5, 4, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 2.70 s
|
|
----------
|
|
objective = 1175;
|
|
period_of = [1, 1, 1, 1, 2, 2, 2, 2, 1, 1, 4, 5, 4, 6, 2, 3, 6, 2, 6, 3, 2, 1, 1, 5, 4, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 2.75 s
|
|
----------
|
|
objective = 1174;
|
|
period_of = [1, 1, 1, 1, 2, 3, 2, 2, 1, 1, 4, 5, 4, 6, 2, 3, 6, 2, 6, 3, 2, 1, 1, 5, 4, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 2.96 s
|
|
----------
|
|
objective = 1173;
|
|
period_of = [1, 1, 1, 2, 2, 3, 2, 2, 1, 1, 4, 5, 4, 6, 2, 3, 6, 2, 6, 3, 2, 1, 1, 5, 4, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 3.04 s
|
|
----------
|
|
objective = 1102;
|
|
period_of = [1, 1, 3, 2, 2, 3, 2, 2, 1, 1, 4, 5, 4, 6, 2, 3, 6, 2, 6, 3, 2, 1, 1, 5, 4, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 3.08 s
|
|
----------
|
|
objective = 1031;
|
|
period_of = [1, 1, 3, 1, 2, 3, 2, 2, 1, 1, 4, 5, 4, 6, 2, 3, 6, 2, 6, 3, 2, 1, 1, 5, 4, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 3.13 s
|
|
----------
|
|
objective = 1030;
|
|
period_of = [1, 1, 2, 1, 2, 3, 2, 2, 1, 1, 4, 5, 4, 6, 2, 3, 6, 2, 6, 3, 2, 1, 1, 5, 4, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 3.16 s
|
|
----------
|
|
objective = 1029;
|
|
period_of = [1, 1, 2, 3, 2, 3, 2, 2, 1, 1, 4, 5, 4, 6, 2, 3, 6, 2, 6, 3, 2, 1, 1, 5, 4, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 3.30 s
|
|
----------
|
|
objective = 957;
|
|
period_of = [1, 1, 2, 3, 2, 1, 2, 2, 1, 1, 4, 5, 4, 6, 2, 3, 6, 2, 6, 3, 2, 1, 1, 5, 4, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 4.39 s
|
|
----------
|
|
objective = 956;
|
|
period_of = [1, 1, 2, 3, 4, 1, 2, 2, 1, 1, 4, 5, 4, 6, 2, 3, 6, 2, 6, 3, 2, 1, 1, 5, 4, 5, 4, 3, 6, 4, 1, 1, 2, 3, 5, 2];
|
|
% time elapsed: 5.06 s
|
|
----------
|
|
% Pruned 49996 learnt clauses
|
|
% Pruned 49990 learnt clauses
|
|
% Time limit exceeded!
|
|
%%%mzn-stat: nodes=484528
|
|
%%%mzn-stat: failures=186752
|
|
%%%mzn-stat: restarts=813
|
|
%%%mzn-stat: variables=98352
|
|
%%%mzn-stat: intVars=780
|
|
%%%mzn-stat: boolVariables=97570
|
|
%%%mzn-stat: propagators=1243
|
|
%%%mzn-stat: propagations=212047937
|
|
%%%mzn-stat: peakDepth=75
|
|
%%%mzn-stat: nogoods=186752
|
|
%%%mzn-stat: backjumps=4686
|
|
%%%mzn-stat: peakMem=0.00
|
|
%%%mzn-stat: time=120.067
|
|
%%%mzn-stat: initTime=0.050
|
|
%%%mzn-stat: solveTime=120.017
|
|
%%%mzn-stat: objective=956
|
|
%%%mzn-stat: optTime=5.009
|
|
%%%mzn-stat: baseMem=0.00
|
|
%%%mzn-stat: trailMem=0.19
|
|
%%%mzn-stat: randomSeed=6
|