PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/een/normalized-mod008.opb
MD5SUM	18b325bb9311c83b0604c703bacc9a29
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	87
Optimality of the best value was proved	NO
Number of terms in the objective function	319
Biggest coefficient in the objective function	87
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	23554
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	7499
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	758444
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.283956
Number of variables	319
Total number of constraints	6
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	186
Maximum length of a constraint	231
Trace number 7042

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-14 21:14:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5148 boxname=wulflinc30 idbench=396 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  18b325bb9311c83b0604c703bacc9a29  /oldhome/oroussel/tmp/wulflinc30/normalized-mod008.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc30/normalized-mod008.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mod008.opb
IDLAUNCH: 5148
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        714104 kB
Buffers:         38584 kB
Cached:         241372 kB
SwapCached:          0 kB
Active:          85408 kB
Inactive:       197372 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        713852 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32188 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:19:59 (client local time) WITH STATUS 30 IN 313.55 SECONDS
stats: 5148 0 313.55 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss.ss
c ---[   4]---> BDD-cost:  105
c ---[   3]---> BDD-cost:  168
c ---[   2]---> BDD-cost:  223
c ---[   1]---> Sorter-cost:  663     Base: 3
c ---[   0]---> Sorter-cost:  354     Base: 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4796    13664 |    1598       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 2576[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:61666     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        56 |  172842   406835 |   57614      56      206     3.7 |  0.000 % |
c |       157 |  172842   406835 |   63375     157     6349    40.4 |  0.011 % |
c |       307 |  172842   406835 |   69712     307     9285    30.2 |  0.011 % |
c |       532 |  172842   406835 |   76684     532    12735    23.9 |  0.011 % |
c |       869 |  172842   406835 |   84352     869    17720    20.4 |  0.011 % |
c |      1375 |  172842   406835 |   92787    1375    44364    32.3 |  0.011 % |
c |      2134 |  172842   406835 |  102066    2134    72301    33.9 |  0.011 % |
c |      3273 |  172842   406835 |  112273    3273   108788    33.2 |  0.011 % |
c |      4981 |  172835   406820 |  123500    4976   173136    34.8 |  0.014 % |
c |      7544 |  172835   406820 |  135850    7539   227153    30.1 |  0.014 % |
c |     11388 |  172835   406820 |  149435   11383   310090    27.2 |  0.014 % |
c ==============================================================================
c [1mFound solution: 2574[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11878 |  174301   410490 |   58100   11873   319051    26.9 |  0.014 % |
c |     11978 |  174301   410490 |   63910   11973   320046    26.7 |  0.017 % |
c ==============================================================================
c [1mFound solution: 1534[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12125 |  174459   410873 |   58153   12120   322201    26.6 |  0.017 % |
c |     12225 |  174459   410873 |   63968   12220   324109    26.5 |  0.019 % |
c |     12375 |  174459   410873 |   70365   12370   325485    26.3 |  0.019 % |
c |     12602 |  174459   410873 |   77401   12597   327897    26.0 |  0.019 % |
c |     12941 |  174459   410873 |   85141   12936   330873    25.6 |  0.019 % |
c |     13448 |  174459   410873 |   93655   13443   337210    25.1 |  0.019 % |
c |     14208 |  174396   410732 |  103021   13974   341489    24.4 |  0.049 % |
c |     15347 |  174396   410732 |  113323   15113   385765    25.5 |  0.049 % |
c |     17055 |  174396   410732 |  124656   16821   410578    24.4 |  0.049 % |
c ==============================================================================
c [1mFound solution: 1524[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18129 |  174525   411107 |   58175   17895   428822    24.0 |  0.049 % |
c |     18231 |  174525   411107 |   63992   17997   433039    24.1 |  0.050 % |
c |     18381 |  174525   411107 |   70391   18147   436771    24.1 |  0.050 % |
c |     18606 |  174525   411107 |   77430   18372   439629    23.9 |  0.050 % |
c |     18943 |  174525   411107 |   85174   18709   442373    23.6 |  0.050 % |
c |     19449 |  174525   411107 |   93691   19215   446389    23.2 |  0.050 % |
c |     20210 |  174525   411107 |  103060   19976   478173    23.9 |  0.050 % |
c |     21349 |  174525   411107 |  113366   21115   511060    24.2 |  0.050 % |
c |     23060 |  174525   411107 |  124703   22826   570421    25.0 |  0.050 % |
c |     25622 |  174525   411107 |  137173   25388   626000    24.7 |  0.050 % |
c ==============================================================================
c [1mFound solution: 1468[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26221 |  175828   414288 |   58609   25987   660533    25.4 |  0.050 % |
c |     26321 |  175828   414288 |   64469   26087   662241    25.4 |  0.052 % |
c |     26471 |  175828   414288 |   70916   26237   663318    25.3 |  0.052 % |
c |     26697 |  175828   414288 |   78008   26463   664759    25.1 |  0.052 % |
c |     27034 |  175828   414288 |   85809   26800   668656    24.9 |  0.052 % |
c |     27540 |  175828   414288 |   94390   27306   677381    24.8 |  0.052 % |
c |     28301 |  175828   414288 |  103829   28067   702790    25.0 |  0.052 % |
c |     29440 |  175828   414288 |  114212   29206   722713    24.7 |  0.052 % |
c |     31149 |  175828   414288 |  125633   30915   748640    24.2 |  0.052 % |
c |     33711 |  175828   414288 |  138196   33477   819467    24.5 |  0.052 % |
c ==============================================================================
c [1mFound solution: 1462[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34038 |  176768   416584 |   58922   33804   824949    24.4 |  0.052 % |
c |     34139 |  176768   416584 |   64814   33905   830018    24.5 |  0.053 % |
c |     34289 |  176768   416584 |   71295   34055   832685    24.5 |  0.053 % |
c |     34514 |  176768   416584 |   78425   34280   837460    24.4 |  0.053 % |
c |     34851 |  176768   416584 |   86267   34617   844832    24.4 |  0.053 % |
c |     35357 |  176768   416584 |   94894   35123   852707    24.3 |  0.053 % |
c ==============================================================================
c [1mFound solution: 1234[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35451 |  176829   416731 |   58943   35217   854333    24.3 |  0.053 % |
c ==============================================================================
c [1mFound solution: 654[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35527 |  176920   416952 |   58973   35293   854865    24.2 |  0.053 % |
c |     35628 |  176920   416952 |   64870   35394   858240    24.2 |  0.057 % |
c |     35780 |  176920   416952 |   71357   35546   865453    24.3 |  0.057 % |
c |     36005 |  176920   416952 |   78493   35771   868880    24.3 |  0.057 % |
c |     36343 |  176711   416481 |   86342   35938   871334    24.2 |  0.151 % |
c |     36849 |  176525   416061 |   94976   36360   888114    24.4 |  0.239 % |
c |     37609 |  176490   415983 |  104474   37113   920534    24.8 |  0.255 % |
c |     38751 |  176490   415983 |  114921   38255   975259    25.5 |  0.255 % |
c |     40459 |  176490   415983 |  126413   39963  1077284    27.0 |  0.255 % |
c ==============================================================================
c [1mFound solution: 634[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41306 |  176505   416020 |   58835   40810  1101263    27.0 |  0.255 % |
c |     41406 |  176505   416020 |   64718   40910  1102153    26.9 |  0.256 % |
c ==============================================================================
c [1mFound solution: 621[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41417 |  176518   416051 |   58839   40921  1102835    27.0 |  0.256 % |
c |     41517 |  176518   416051 |   64722   41021  1108224    27.0 |  0.258 % |
c |     41667 |  176518   416051 |   71195   41171  1114182    27.1 |  0.258 % |
c |     41892 |  176518   416051 |   78314   41396  1122207    27.1 |  0.258 % |
c |     42229 |  176518   416051 |   86146   41733  1147926    27.5 |  0.258 % |
c ==============================================================================
c [1mFound solution: 394[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42475 |  176088   415074 |   58696   41791  1144500    27.4 |  0.258 % |
c ==============================================================================
c [1mFound solution: 351[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42561 |  176096   415094 |   58698   41877  1151047    27.5 |  0.258 % |
c |     42661 |  175982   414833 |   64567   41934  1155007    27.5 |  0.548 % |
c ==============================================================================
c [1mFound solution: 309[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42783 |  176114   415211 |   58704   42056  1158826    27.6 |  0.548 % |
c ==============================================================================
c [1mFound solution: 306[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42798 |  176134   415259 |   58711   42071  1158998    27.5 |  0.548 % |
c |     42898 |  176134   415259 |   64582   42171  1161711    27.5 |  0.552 % |
c |     43048 |  176134   415259 |   71040   42321  1163369    27.5 |  0.552 % |
c ==============================================================================
c [1mFound solution: 293[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43108 |  176143   415282 |   58714   42381  1167500    27.5 |  0.552 % |
c |     43210 |  176143   415282 |   64585   42483  1177918    27.7 |  0.553 % |
c |     43361 |  176143   415282 |   71043   42634  1182448    27.7 |  0.553 % |
c |     43587 |  175661   414178 |   78148   42696  1188854    27.8 |  0.785 % |
c |     43929 |  175661   414178 |   85963   43038  1216283    28.3 |  0.785 % |
c |     44437 |  175271   413283 |   94559   43482  1270859    29.2 |  0.983 % |
c ==============================================================================
c [1mFound solution: 286[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45135 |  174923   412493 |   58307   44058  1366946    31.0 |  0.983 % |
c |     45236 |  174736   412054 |   64137   43968  1370773    31.2 |  1.260 % |
c |     45386 |  174736   412054 |   70551   44118  1381228    31.3 |  1.260 % |
c |     45612 |  174672   411909 |   77606   44335  1399158    31.6 |  1.287 % |
c |     45949 |  174672   411909 |   85367   44672  1420291    31.8 |  1.287 % |
c ==============================================================================
c [1mFound solution: 263[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46059 |  174126   410665 |   58042   44545  1417178    31.8 |  1.287 % |
c ==============================================================================
c [1mFound solution: 261[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46063 |  174130   410675 |   58043   44549  1418128    31.8 |  1.287 % |
c ==============================================================================
c [1mFound solution: 260[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46070 |  174140   410699 |   58046   44556  1422686    31.9 |  1.287 % |
c ==============================================================================
c [1mFound solution: 258[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46136 |  174150   410723 |   58050   44622  1430066    32.0 |  1.287 % |
c |     46236 |  174047   410491 |   63855   44707  1450664    32.4 |  1.615 % |
c |     46386 |  174047   410491 |   70240   44857  1482568    33.1 |  1.615 % |
c |     46611 |  174047   410491 |   77264   45082  1507319    33.4 |  1.615 % |
c ==============================================================================
c [1mFound solution: 209[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46696 |  174060   410523 |   58020   45167  1513379    33.5 |  1.615 % |
c ==============================================================================
c [1mFound solution: 203[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46720 |  173566   409397 |   57855   44863  1505841    33.6 |  1.615 % |
c ==============================================================================
c [1mFound solution: 155[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost: 1444
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46746 |  178104   422379 |   59368   44889  1507566    33.6 |  1.615 % |
c |     46854 |  178104   422379 |   65304   44997  1527861    34.0 |  1.842 % |
c ==============================================================================
c [1mFound solution: 147[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost: 1601
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46982 |  180930   430533 |   60310   45125  1552519    34.4 |  1.842 % |
c ==============================================================================
c [1mFound solution: 145[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:  721
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47055 |  183897   439263 |   61299   45174  1562619    34.6 |  1.842 % |
c |     47155 |  183897   439263 |   67428   45274  1569474    34.7 |  1.944 % |
c |     47306 |  182606   436302 |   74171   44313  1534834    34.6 |  2.579 % |
c |     47534 |  182606   436302 |   81588   44541  1553752    34.9 |  2.579 % |
c ==============================================================================
c [1mFound solution: 139[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:  775
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47837 |  185580   444828 |   61860   44844  1598126    35.6 |  2.579 % |
c |     47939 |  185580   444828 |   68046   44946  1613711    35.9 |  2.564 % |
c |     48102 |  185580   444828 |   74850   45109  1642516    36.4 |  2.564 % |
c ==============================================================================
c [1mFound solution: 137[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:  199
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48240 |  188272   452638 |   62757   45247  1650993    36.5 |  2.564 % |
c |     48340 |  188272   452638 |   69032   45347  1663044    36.7 |  2.551 % |
c ==============================================================================
c [1mFound solution: 124[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:  296
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48446 |  190602   459362 |   63534   45453  1682051    37.0 |  2.551 % |
c |     48547 |  190602   459362 |   69887   45554  1694218    37.2 |  2.535 % |
c |     48712 |  190602   459362 |   76876   45719  1715968    37.5 |  2.535 % |
c ==============================================================================
c [1mFound solution: 87[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:  127
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48915 |  183753   443673 |   61251   42719  1633556    38.2 |  2.535 % |
c |     49015 |  183753   443673 |   67376   42819  1642281    38.4 |  6.206 % |
c ==============================================================================
c [1mOptimal solution: 87[0m
s OPTIMUM FOUND
v -x0 -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 x318
c _______________________________________________________________________________
c 
c restarts              : 110
c conflicts             : 49065          (157 /sec)
c decisions             : 157998         (504 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 313.198 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.90 2/54 23207
Raw data (stat): 23207 (runsolver) R 23206 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487748517 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.98 0.90 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 5180 0 0 0 987 12 0 0 25 0 1 0 487748517 23109632 4952 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5642 4952 603 41 0 5601 0
vsize: 22568
[startup+20.0015 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 5255 0 0 0 1986 12 0 0 25 0 1 0 487748517 23433216 5027 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5721 5027 603 41 0 5680 0
vsize: 22884
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 5345 0 0 0 2986 12 0 0 25 0 1 0 487748517 23830528 5117 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5818 5117 603 41 0 5777 0
vsize: 23272
[startup+40.0022 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 5405 0 0 0 3985 12 0 0 25 0 1 0 487748517 24121344 5177 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5889 5177 603 41 0 5848 0
vsize: 23556
[startup+50.003 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 5761 0 0 0 4984 14 0 0 25 0 1 0 487748517 26009600 5449 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6350 5449 603 41 0 6309 0
vsize: 25400
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 5774 0 0 0 5984 14 0 0 25 0 1 0 487748517 26009600 5462 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6350 5462 603 41 0 6309 0
vsize: 25400
[startup+70.0039 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 5831 0 0 0 6983 14 0 0 25 0 1 0 487748517 26365952 5519 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6437 5519 603 41 0 6396 0
vsize: 25748
[startup+80.0047 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 5948 0 0 0 7982 15 0 0 25 0 1 0 487748517 26710016 5615 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6521 5615 603 41 0 6480 0
vsize: 26084
[startup+90.0041 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 6089 0 0 0 8981 16 0 0 25 0 1 0 487748517 27246592 5756 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6652 5756 603 41 0 6611 0
vsize: 26608
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 6267 0 0 0 9980 17 0 0 25 0 1 0 487748517 27721728 5850 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6768 5850 603 41 0 6727 0
vsize: 27072
[startup+110.006 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 6348 0 0 0 10979 18 0 0 25 0 1 0 487748517 27992064 5931 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6834 5931 603 41 0 6793 0
vsize: 27336
[startup+120.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 6415 0 0 0 11978 19 0 0 25 0 1 0 487748517 28258304 5998 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6899 5998 603 41 0 6858 0
vsize: 27596
[startup+130.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 6597 0 0 0 12978 19 0 0 25 0 1 0 487748517 28672000 6091 4294967295 134512640 134672761 3221224576 3221223760 134558831 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7000 6091 603 41 0 6959 0
vsize: 28000
[startup+140.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 6748 0 0 0 13977 20 0 0 25 0 1 0 487748517 28889088 6145 4294967295 134512640 134672761 3221224576 3221223744 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7053 6145 603 41 0 7012 0
vsize: 28212
[startup+150.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 6757 0 0 0 14976 21 0 0 25 0 1 0 487748517 29024256 6154 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7086 6154 603 41 0 7045 0
vsize: 28344
[startup+160.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 6815 0 0 0 15976 21 0 0 25 0 1 0 487748517 29245440 6212 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7140 6212 603 41 0 7099 0
vsize: 28560
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 6874 0 0 0 16976 22 0 0 25 0 1 0 487748517 29511680 6271 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7205 6271 603 41 0 7164 0
vsize: 28820
[startup+180.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 6944 0 0 0 17975 22 0 0 25 0 1 0 487748517 29773824 6341 4294967295 134512640 134672761 3221224576 3221223716 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7269 6341 603 41 0 7228 0
vsize: 29076
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 7018 0 0 0 18974 23 0 0 25 0 1 0 487748517 30044160 6415 4294967295 134512640 134672761 3221224576 3221223700 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7335 6415 603 41 0 7294 0
vsize: 29340
[startup+200.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 7177 0 0 0 19973 24 0 0 25 0 1 0 487748517 30253056 6473 4294967295 134512640 134672761 3221224576 3221223712 134560625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7386 6473 603 41 0 7345 0
vsize: 29544
[startup+210.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 7402 0 0 0 20973 25 0 0 25 0 1 0 487748517 30425088 6528 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7428 6528 603 41 0 7387 0
vsize: 29712
[startup+220.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 7435 0 0 0 21972 25 0 0 25 0 1 0 487748517 30556160 6561 4294967295 134512640 134672761 3221224576 3221223712 134560645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7460 6561 603 41 0 7419 0
vsize: 29840
[startup+230.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 7484 0 0 0 22972 26 0 0 25 0 1 0 487748517 30818304 6610 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7524 6610 603 41 0 7483 0
vsize: 30096
[startup+240.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 7646 0 0 0 23971 26 0 0 25 0 1 0 487748517 31653888 6772 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7728 6772 603 41 0 7687 0
vsize: 30912
[startup+250.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 7924 0 0 0 24970 27 0 0 25 0 1 0 487748517 31666176 6809 4294967295 134512640 134672761 3221224576 3221223876 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7731 6809 603 41 0 7690 0
vsize: 30924
[startup+260.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 8122 0 0 0 25969 28 0 0 25 0 1 0 487748517 32030720 6899 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7820 6899 603 41 0 7779 0
vsize: 31280
[startup+270.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 8385 0 0 0 26969 29 0 0 25 0 1 0 487748517 32841728 7110 4294967295 134512640 134672761 3221224576 3221223712 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8018 7110 603 41 0 7977 0
vsize: 32072
[startup+280.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 8463 0 0 0 27969 29 0 0 25 0 1 0 487748517 33116160 7188 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8085 7188 603 41 0 8044 0
vsize: 32340
[startup+290.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 8557 0 0 0 28968 30 0 0 25 0 1 0 487748517 33394688 7282 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8153 7282 603 41 0 8112 0
vsize: 32612
[startup+300.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 8698 0 0 0 29967 30 0 0 25 0 1 0 487748517 33943552 7423 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8287 7423 603 41 0 8246 0
vsize: 33148
[startup+310.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 8755 0 0 0 30967 31 0 0 25 0 1 0 487748517 34193408 7480 4294967295 134512640 134672761 3221224576 3221223680 134555096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8348 7480 603 41 0 8307 0
vsize: 33392
[startup+313.582 s]
Raw data (loadavg): 0.99 0.98 0.91 1/53 23207
Raw data (stat): 23207 (minisat+) R 23206 11931 11930 0 -1 0 8755 0 0 0 30967 31 0 0 25 0 1 0 487748517 34193408 7480 4294967295 134512640 134672761 3221224576 3221223680 134555096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8348 7480 603 41 0 8307 0
vsize: 0

Child status: 30
Real time (s): 313.581
CPU time (s): 313.55
CPU user time (s): 313.219
CPU system time (s): 0.330949
CPU usage (%): 99.9902
Max. virtual memory (Kb): 33392
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	87
#### END VERIFIER DATA ####