125 lines
23 KiB
Solidity
125 lines
23 KiB
Solidity
% init_area = 473782338;
|
|
objective = 23362;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 1, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 6, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 5, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 5, 5, 6, 3];
|
|
% time elapsed: 0.39 s
|
|
----------
|
|
objective = 23104;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 1, 6, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 5, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 5, 5, 6, 3];
|
|
% time elapsed: 0.41 s
|
|
----------
|
|
objective = 23103;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 1, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 5, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 5, 5, 6, 3];
|
|
% time elapsed: 0.42 s
|
|
----------
|
|
objective = 22102;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 1, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 6, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 5, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 0.44 s
|
|
----------
|
|
objective = 21844;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 1, 6, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 5, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 0.46 s
|
|
----------
|
|
objective = 21843;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 1, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 5, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 0.48 s
|
|
----------
|
|
objective = 21676;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 1, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 6, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 5, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 6, 6, 6, 3];
|
|
% time elapsed: 0.50 s
|
|
----------
|
|
objective = 21418;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 1, 6, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 5, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 6, 6, 6, 3];
|
|
% time elapsed: 0.51 s
|
|
----------
|
|
objective = 21417;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 1, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 5, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 6, 6, 6, 3];
|
|
% time elapsed: 0.53 s
|
|
----------
|
|
objective = 21377;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 1, 6, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 6, 5, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 6, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 0.56 s
|
|
----------
|
|
objective = 21376;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 1, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 6, 5, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 6, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 0.58 s
|
|
----------
|
|
objective = 21371;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 1, 6, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 0.60 s
|
|
----------
|
|
objective = 21370;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 1, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 0.62 s
|
|
----------
|
|
objective = 21346;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 5, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 1, 6, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 4, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 1.07 s
|
|
----------
|
|
objective = 21345;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 4, 5, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 1, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 4, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 1.09 s
|
|
----------
|
|
objective = 21339;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 5, 5, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 1, 6, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 4, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 4.70 s
|
|
----------
|
|
objective = 21338;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 5, 5, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 1, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 4, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 4.73 s
|
|
----------
|
|
objective = 21331;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 5, 5, 3, 3, 3, 6, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 1, 6, 4, 4, 5, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 6, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 4, 6, 6, 6, 6, 5, 5, 6, 3];
|
|
% time elapsed: 5.92 s
|
|
----------
|
|
objective = 21330;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 5, 5, 3, 3, 3, 6, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 1, 4, 4, 5, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 6, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 4, 6, 6, 6, 6, 5, 5, 6, 3];
|
|
% time elapsed: 5.95 s
|
|
----------
|
|
objective = 21329;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 4, 3, 2, 2, 3, 4, 1, 1, 6, 5, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 1, 4, 4, 6, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 5, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 4, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 10.33 s
|
|
----------
|
|
% Pruned 49997 learnt clauses
|
|
objective = 21328;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 5, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 1, 4, 4, 4, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 6, 6, 5, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 6, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 81.63 s
|
|
----------
|
|
objective = 21299;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 5, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 1, 6, 4, 4, 4, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 6, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 81.76 s
|
|
----------
|
|
objective = 21298;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 5, 3, 2, 2, 3, 4, 1, 1, 4, 4, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 1, 4, 4, 4, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 6, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 5, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 81.79 s
|
|
----------
|
|
objective = 21251;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 5, 3, 2, 2, 3, 4, 1, 1, 4, 5, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 1, 6, 4, 4, 4, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 6, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 4, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 84.69 s
|
|
----------
|
|
objective = 21250;
|
|
period_of = [1, 2, 2, 2, 2, 2, 2, 2, 3, 3, 1, 3, 3, 3, 4, 1, 4, 1, 3, 3, 3, 2, 1, 2, 3, 2, 3, 1, 2, 1, 1, 1, 3, 3, 3, 2, 5, 5, 4, 4, 3, 5, 4, 3, 4, 2, 3, 4, 3, 1, 2, 2, 4, 2, 2, 2, 2, 1, 4, 2, 3, 4, 3, 3, 3, 3, 4, 5, 1, 1, 5, 3, 1, 2, 2, 1, 1, 2, 2, 2, 2, 2, 4, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 2, 3, 3, 3, 3, 4, 4, 1, 1, 5, 6, 1, 5, 1, 5, 2, 3, 2, 2, 3, 2, 5, 2, 2, 4, 3, 3, 3, 1, 1, 3, 3, 4, 4, 4, 3, 3, 1, 1, 2, 4, 2, 2, 2, 2, 1, 1, 4, 5, 3, 2, 2, 3, 4, 1, 1, 4, 5, 3, 3, 3, 5, 3, 2, 4, 2, 4, 5, 6, 5, 5, 1, 2, 2, 3, 3, 3, 4, 4, 3, 4, 3, 3, 5, 3, 3, 3, 3, 3, 4, 4, 3, 1, 2, 4, 4, 3, 4, 3, 1, 6, 1, 4, 4, 4, 4, 3, 4, 3, 3, 3, 1, 4, 4, 5, 5, 5, 3, 3, 3, 3, 4, 5, 5, 1, 6, 5, 6, 6, 6, 6, 1, 6, 4, 6, 6, 1, 5, 6, 1, 1, 6, 4, 6, 1, 5, 6, 6, 6, 5, 5, 5, 5, 6, 6, 6, 1, 3, 1, 4, 5, 4, 5, 1, 4, 5, 5, 1, 5, 5, 2, 3, 3, 6, 3, 3, 1, 1, 5, 4, 4, 6, 6, 6, 6, 5, 6, 6, 3];
|
|
% time elapsed: 84.78 s
|
|
----------
|
|
% Pruned 49998 learnt clauses
|
|
% Time limit exceeded!
|
|
%%%mzn-stat: nodes=196810
|
|
%%%mzn-stat: failures=190539
|
|
%%%mzn-stat: restarts=25
|
|
%%%mzn-stat: variables=349725
|
|
%%%mzn-stat: intVars=2907
|
|
%%%mzn-stat: boolVariables=346816
|
|
%%%mzn-stat: propagators=2298
|
|
%%%mzn-stat: propagations=124288063
|
|
%%%mzn-stat: peakDepth=234
|
|
%%%mzn-stat: nogoods=190539
|
|
%%%mzn-stat: backjumps=233
|
|
%%%mzn-stat: peakMem=0.00
|
|
%%%mzn-stat: time=120.354
|
|
%%%mzn-stat: initTime=0.354
|
|
%%%mzn-stat: solveTime=120.000
|
|
%%%mzn-stat: objective=21250
|
|
%%%mzn-stat: optTime=84.428
|
|
%%%mzn-stat: baseMem=0.00
|
|
%%%mzn-stat: trailMem=0.63
|
|
%%%mzn-stat: randomSeed=1624263186
|