Dekker1/on-restart-benchmarks
Archived
1
0
Fork 0
Code
This repository has been archived on 2025-03-06. You can view files and clone it, but cannot push or open issues or pull requests.
on-restart-benchmarks/output/chuffed/gbac/original/UD4-gbac.sol
Jip J. Dekker ac89bcb3da
Add solver output
2021-06-23 13:46:35 +10:00

239 lines
25 KiB
Solidity
Raw Blame History

% init_area = 83030480;
objective = 14378;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 1, 1, 1, 1, 3, 4, 3, 5, 1, 3, 2, 2, 2, 5, 2, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.18 s
----------
objective = 14306;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 1, 1, 1, 1, 3, 4, 3, 5, 1, 3, 2, 2, 2, 5, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.19 s
----------
objective = 14234;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 1, 1, 1, 1, 3, 4, 3, 5, 1, 3, 2, 2, 2, 5, 5, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.19 s
----------
objective = 14090;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 1, 1, 1, 1, 3, 4, 3, 5, 2, 3, 2, 2, 2, 5, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.20 s
----------
objective = 14018;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 1, 1, 1, 1, 3, 4, 3, 5, 2, 3, 2, 2, 2, 5, 5, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.21 s
----------
objective = 13946;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 1, 1, 1, 1, 3, 4, 3, 5, 3, 3, 2, 2, 2, 5, 5, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.21 s
----------
objective = 13874;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 1, 1, 1, 1, 3, 4, 3, 5, 5, 3, 2, 2, 2, 5, 6, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.22 s
----------
objective = 13802;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 1, 1, 1, 1, 3, 4, 5, 3, 1, 3, 2, 2, 2, 5, 2, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.23 s
----------
objective = 13658;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 1, 1, 1, 1, 3, 4, 5, 3, 1, 3, 2, 2, 2, 5, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.24 s
----------
objective = 13442;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 1, 1, 1, 1, 3, 4, 5, 3, 2, 3, 2, 2, 2, 5, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.25 s
----------
objective = 13370;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 1, 1, 1, 1, 3, 4, 5, 3, 3, 3, 2, 2, 2, 5, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.25 s
----------
objective = 13298;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 1, 1, 1, 1, 3, 4, 5, 3, 3, 3, 2, 2, 2, 5, 6, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.26 s
----------
objective = 12867;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 1, 4, 5, 3, 1, 3, 2, 2, 2, 5, 2, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.29 s
----------
objective = 12795;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 1, 4, 5, 3, 1, 3, 2, 2, 2, 5, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.30 s
----------
objective = 12723;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 1, 4, 5, 3, 1, 3, 2, 2, 2, 5, 6, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.31 s
----------
objective = 12651;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 1, 4, 5, 3, 2, 3, 2, 2, 2, 5, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.32 s
----------
objective = 12579;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 1, 4, 5, 3, 2, 3, 2, 2, 2, 5, 6, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.33 s
----------
objective = 12507;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 1, 4, 5, 3, 3, 3, 2, 2, 2, 5, 6, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.34 s
----------
objective = 12147;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 2, 4, 5, 3, 1, 3, 2, 2, 2, 5, 1, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.35 s
----------
objective = 12075;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 2, 4, 5, 3, 1, 3, 2, 2, 2, 5, 2, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.36 s
----------
objective = 11931;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 2, 4, 5, 3, 1, 3, 2, 2, 2, 5, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.37 s
----------
objective = 11859;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 2, 4, 5, 3, 1, 3, 2, 2, 2, 5, 6, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.38 s
----------
objective = 11787;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 2, 4, 5, 3, 3, 3, 2, 2, 2, 5, 5, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.39 s
----------
objective = 11715;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 2, 4, 5, 3, 3, 3, 2, 2, 2, 5, 6, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.40 s
----------
objective = 11644;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 3, 4, 5, 4, 3, 3, 2, 2, 2, 5, 6, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.42 s
----------
objective = 11643;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 3, 4, 5, 5, 1, 3, 2, 2, 2, 6, 2, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.44 s
----------
objective = 11571;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 3, 4, 5, 5, 1, 3, 2, 2, 2, 6, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.45 s
----------
objective = 11499;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 3, 4, 5, 5, 2, 3, 2, 2, 2, 6, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.46 s
----------
objective = 11427;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 3, 1, 1, 1, 3, 4, 5, 5, 3, 3, 2, 2, 2, 6, 5, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 0.48 s
----------
objective = 11426;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 4, 1, 1, 1, 3, 4, 5, 3, 3, 3, 2, 2, 2, 5, 6, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 1.07 s
----------
objective = 11355;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 1, 4, 6, 3, 3, 3, 2, 2, 2, 3, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 1.12 s
----------
objective = 11283;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 2, 4, 3, 3, 1, 3, 2, 2, 2, 5, 6, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 1.14 s
----------
objective = 11211;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 2, 4, 3, 3, 3, 3, 2, 2, 2, 5, 5, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 1.15 s
----------
objective = 11139;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 2, 4, 3, 3, 3, 3, 2, 2, 2, 5, 6, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 1.16 s
----------
objective = 10995;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 2, 4, 5, 3, 1, 3, 2, 2, 2, 3, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 1.17 s
----------
objective = 10851;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 2, 4, 5, 3, 3, 3, 2, 2, 2, 3, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 1.18 s
----------
objective = 10779;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 2, 4, 5, 3, 3, 3, 2, 2, 2, 3, 6, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 1.19 s
----------
objective = 10707;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 2, 4, 6, 3, 1, 3, 2, 2, 2, 3, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 1.21 s
----------
objective = 10563;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 2, 4, 6, 3, 3, 3, 2, 2, 2, 3, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 1.22 s
----------
objective = 10491;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 3, 4, 5, 3, 3, 3, 2, 2, 2, 6, 3, 3, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 6, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 1.28 s
----------
objective = 10347;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 2, 4, 6, 3, 1, 3, 2, 2, 2, 3, 3, 5, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 2.68 s
----------
objective = 10203;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 2, 4, 6, 3, 3, 3, 2, 2, 2, 3, 3, 5, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 2.70 s
----------
objective = 10131;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 3, 4, 6, 3, 3, 3, 2, 2, 2, 4, 3, 5, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 2.85 s
----------
objective = 10059;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 3, 4, 6, 3, 3, 5, 2, 2, 2, 4, 3, 5, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 6.94 s
----------
objective = 9987;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 2, 4, 6, 3, 3, 5, 2, 2, 2, 3, 3, 6, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 8.60 s
----------
objective = 9915;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 1, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 3, 4, 6, 3, 3, 5, 2, 2, 2, 4, 3, 6, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 8.80 s
----------
objective = 9843;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 3, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 2, 4, 6, 3, 3, 5, 2, 2, 2, 3, 3, 6, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 12.96 s
----------
objective = 9771;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 3, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 3, 4, 6, 3, 3, 5, 2, 2, 2, 4, 3, 6, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 14.52 s
----------
objective = 9699;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 5, 3, 4, 3, 3, 4, 3, 3, 3, 5, 1, 1, 1, 3, 4, 6, 3, 3, 5, 2, 2, 2, 4, 3, 6, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 23.34 s
----------
% Pruned 49996 learnt clauses
% Pruned 49996 learnt clauses
objective = 9627;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 3, 3, 4, 3, 3, 5, 3, 3, 3, 5, 1, 1, 1, 2, 4, 6, 3, 3, 5, 2, 2, 2, 3, 3, 6, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 41.67 s
----------
objective = 9555;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 3, 3, 4, 3, 3, 5, 3, 3, 3, 5, 1, 1, 1, 3, 4, 6, 3, 3, 5, 2, 2, 2, 4, 3, 6, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 42.85 s
----------
objective = 9483;
period_of = [1, 1, 2, 2, 2, 2, 2, 1, 1, 2, 1, 3, 3, 3, 1, 3, 3, 3, 4, 3, 4, 1, 1, 3, 3, 1, 2, 3, 3, 3, 4, 4, 4, 4, 4, 4, 1, 1, 1, 1, 1, 1, 2, 2, 2, 3, 3, 2, 2, 2, 2, 3, 3, 4, 5, 3, 4, 5, 6, 2, 2, 2, 1, 2, 1, 2, 2, 2, 2, 2, 1, 3, 1, 1, 1, 3, 3, 3, 4, 5, 3, 4, 3, 3, 5, 3, 3, 3, 5, 1, 1, 1, 3, 4, 6, 3, 3, 5, 2, 2, 2, 4, 3, 6, 1, 3, 4, 1, 4, 2, 4, 5, 5, 3, 5, 5, 5, 5, 6, 4, 5, 5, 5, 1, 6, 1, 6, 6, 3, 6, 1, 6, 6, 3, 6, 6, 6, 6, 2];
% time elapsed: 48.62 s
----------
% Pruned 49995 learnt clauses
% Pruned 49995 learnt clauses
% Pruned 49996 learnt clauses
% Pruned 49993 learnt clauses
% Pruned 49995 learnt clauses
% Pruned 49993 learnt clauses
% Time limit exceeded!
%%%mzn-stat: nodes=493842
%%%mzn-stat: failures=477325
%%%mzn-stat: restarts=52
%%%mzn-stat: variables=236730
%%%mzn-stat: intVars=1456
%%%mzn-stat: boolVariables=235272
%%%mzn-stat: propagators=1183
%%%mzn-stat: propagations=156277561
%%%mzn-stat: peakDepth=114
%%%mzn-stat: nogoods=477325
%%%mzn-stat: backjumps=10504
%%%mzn-stat: peakMem=0.00
%%%mzn-stat: time=120.164
%%%mzn-stat: initTime=0.163
%%%mzn-stat: solveTime=120.001
%%%mzn-stat: objective=9483
%%%mzn-stat: optTime=48.455
%%%mzn-stat: baseMem=0.00
%%%mzn-stat: trailMem=0.42
%%%mzn-stat: randomSeed=1624263065
View Git Blame Copy Permalink