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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb30-15-opb/normalized-frb30-15-2.opb
MD5SUM	25130921f4384cc034832ca1cd52ec48
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
Optimality of the best value was proved	NO
Number of terms in the objective function	450
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	450
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	450
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05584
Number of variables	450
Total number of constraints	17874
Number of constraints which are clauses	17874
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 6345

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-14 04:33:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4827 boxname=wulflinc29 idbench=315 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  25130921f4384cc034832ca1cd52ec48  /oldhome/oroussel/tmp/wulflinc29/normalized-frb30-15-2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc29/normalized-frb30-15-2.opb /oldhome/oroussel/tmp/wulflinc29/normalized-frb30-15-2.opb
IDLAUNCH: 4827
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        814352 kB
Buffers:         36848 kB
Cached:         145584 kB
SwapCached:         12 kB
Active:          65848 kB
Inactive:       119492 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        814100 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            29312 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:43:37 (client local time) WITH STATUS 30 IN 620.43 SECONDS
stats: 4827 0 620.43 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17874 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17874    35748 |    5958       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:16912     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   51999   115715 |   17333       0        0     nan |  0.000 % |
c |       100 |   51368   114289 |   19066      85      350     4.1 |  1.565 % |
c |       250 |   50947   113328 |   20972     219     1610     7.4 |  2.642 % |
c ==============================================================================
c [1mFound solution: -21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       314 |   50329   111988 |   16776     260     1785     6.9 |  2.642 % |
c |       414 |   48832   108571 |   18453     327     2196     6.7 |  8.316 % |
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       479 |   48520   107824 |   16173     388     2969     7.7 |  8.316 % |
c |       579 |   47712   105971 |   17790     468     3428     7.3 | 11.120 % |
c |       730 |   46718   103680 |   19569     580     4283     7.4 | 13.823 % |
c |       955 |   45440   100743 |   21526     777     5744     7.4 | 17.191 % |
c |      1292 |   42266    93394 |   23678    1001     7639     7.6 | 25.795 % |
c ==============================================================================
c [1mFound solution: -23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1325 |   42436    93882 |   14145    1022     8540     8.4 | 25.795 % |
c |      1425 |   41827    92452 |   15559    1088     8873     8.2 | 28.041 % |
c |      1575 |   41142    90860 |   17115    1212    10194     8.4 | 29.640 % |
c ==============================================================================
c [1mFound solution: -24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1765 |   39849    87856 |   13283    1350    12225     9.1 | 29.640 % |
c |      1865 |   39440    86910 |   14611    1419    15224    10.7 | 34.320 % |
c |      2015 |   38022    83614 |   16072    1484    16009    10.8 | 38.134 % |
c |      2241 |   37063    81370 |   17679    1663    18654    11.2 | 40.807 % |
c |      2578 |   34715    75865 |   19447    1816    22651    12.5 | 47.387 % |
c |      3084 |   32242    70095 |   21392    2138    26261    12.3 | 54.373 % |
c |      3843 |   30653    66354 |   23531    2673    42995    16.1 | 59.008 % |
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4895 |   29910    64641 |    9970    3646    87705    24.1 | 59.008 % |
c |      4995 |   29689    64130 |   10967    3693    88059    23.8 | 62.012 % |
c |      5145 |   29503    63691 |   12063    3825    89313    23.3 | 62.560 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5343 |   28597    61519 |    9532    3846    93272    24.3 | 62.560 % |
c |      5443 |   28500    61289 |   10485    3941    95884    24.3 | 65.410 % |
c |      5593 |   28046    60219 |   11533    4020    99310    24.7 | 66.718 % |
c |      5819 |   27875    59821 |   12687    4190   104539    24.9 | 67.216 % |
c |      6156 |   27344    58566 |   13955    4464   115129    25.8 | 68.717 % |
c |      6663 |   27139    58086 |   15351    4902   128157    26.1 | 69.299 % |
c |      7423 |   26181    55831 |   16886    5429   149674    27.6 | 72.151 % |
c |      8563 |   25828    55000 |   18575    6510   199111    30.6 | 73.197 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9381 |   25398    54006 |    8466    7082   255142    36.0 | 73.197 % |
c |      9481 |   25398    54006 |    9312    7182   258398    36.0 | 74.724 % |
c |      9631 |   25203    53547 |   10243    7310   263210    36.0 | 75.318 % |
c |      9856 |   25203    53547 |   11268    7535   270751    35.9 | 75.318 % |
c |     10194 |   25169    53467 |   12395    7846   286831    36.6 | 75.419 % |
c |     10700 |   25169    53467 |   13634    8352   316651    37.9 | 75.419 % |
c |     11461 |   25112    53335 |   14998    9038   358251    39.6 | 75.586 % |
c |     12600 |   24769    52530 |   16497   10061   423801    42.1 | 76.608 % |
c |     14308 |   24506    51897 |   18147   11639   525417    45.1 | 77.421 % |
c |     16871 |   24286    51387 |   19962   13797   675563    49.0 | 78.032 % |
c |     20715 |   24211    51208 |   21958   17619  1011434    57.4 | 78.275 % |
c |     26481 |   24081    50908 |   24154   23157  1395787    60.3 | 78.627 % |
c |     35131 |   24081    50908 |   26569   31807  1919940    60.4 | 78.627 % |
c |     48106 |   23672    49954 |   29226   23281  1292621    55.5 | 79.791 % |
c |     67568 |   23384    49274 |   32149   18773   804486    42.9 | 80.670 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     69476 |   23359    49195 |    7786   20677   931601    45.1 | 80.670 % |
c |     69576 |   23359    49195 |    8564   10439   454264    43.5 | 80.740 % |
c |     69726 |   23359    49195 |    9421   10589   459989    43.4 | 80.740 % |
c |     69952 |   23359    49195 |   10363   10815   470893    43.5 | 80.740 % |
c |     70289 |   23359    49195 |   11399   11152   491087    44.0 | 80.740 % |
c |     70795 |   23353    49181 |   12539   11636   514462    44.2 | 80.757 % |
c |     71556 |   23341    49153 |   13793   12395   552424    44.6 | 80.790 % |
c |     72697 |   23341    49153 |   15172   13536   602089    44.5 | 80.791 % |
c |     74405 |   23341    49153 |   16689   15244   674143    44.2 | 80.791 % |
c |     76968 |   23341    49153 |   18358   17807   760847    42.7 | 80.791 % |
c |     80813 |   23341    49153 |   20194   21652   902630    41.7 | 80.791 % |
c |     86579 |   23325    49115 |   22214   27417  1071750    39.1 | 80.841 % |
c |     95229 |   23319    49101 |   24435   19446   525585    27.0 | 80.858 % |
c |    108203 |   23069    48515 |   26879   32365  1020596    31.5 | 81.620 % |
c |    127664 |   23069    48515 |   29567   30038  1117126    37.2 | 81.620 % |
c |    156858 |   22992    48331 |   32524   35276  1312736    37.2 | 81.871 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    173130 |   22901    48120 |    7633   27376   742580    27.1 | 81.871 % |
c |    173231 |   22901    48120 |    8396   13789   337335    24.5 | 82.188 % |
c |    173381 |   22901    48120 |    9235   13939   340542    24.4 | 82.188 % |
c |    173606 |   22901    48120 |   10159   14164   346128    24.4 | 82.188 % |
c |    173943 |   22901    48120 |   11175   14501   353259    24.4 | 82.188 % |
c |    174449 |   22901    48120 |   12293   15007   363782    24.2 | 82.188 % |
c |    175208 |   22901    48120 |   13522   15766   382664    24.3 | 82.188 % |
c |    176347 |   22901    48120 |   14874   16905   407302    24.1 | 82.188 % |
c |    178057 |   22901    48120 |   16362   18615   451872    24.3 | 82.188 % |
c |    180619 |   22901    48120 |   17998   21177   519284    24.5 | 82.188 % |
c |    184463 |   22901    48120 |   19798   25021   594101    23.7 | 82.188 % |
c |    190230 |   22764    47829 |   21777   11284   224130    19.9 | 82.330 % |
c |    198879 |   22716    47715 |   23955   19924   539244    27.1 | 82.480 % |
c |    211854 |   22710    47701 |   26351   32898   916440    27.9 | 82.497 % |
c |    231315 |   22676    47619 |   28986   33202   840186    25.3 | 82.613 % |
c |    260507 |   22646    47549 |   31884   19879   442881    22.3 | 82.697 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 9022     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    294041 |   36084    78968 |   12028   30173   803694    26.6 | 82.697 % |
c |    294141 |   36084    78968 |   13230   15187   335887    22.1 | 61.060 % |
c |    294293 |   36084    78968 |   14553   15339   339975    22.2 | 61.060 % |
c |    294519 |   36084    78968 |   16009   15565   347542    22.3 | 61.060 % |
c |    294857 |   36084    78968 |   17610   15903   355223    22.3 | 61.060 % |
c |    295363 |   36084    78968 |   19371   16409   369941    22.5 | 61.060 % |
c |    296123 |   36084    78968 |   21308   17169   391547    22.8 | 61.060 % |
c |    297262 |   36084    78968 |   23439   18308   425690    23.3 | 61.060 % |
c |    298970 |   36084    78968 |   25783   20016   471512    23.6 | 61.060 % |
c |    301532 |   36084    78968 |   28361   22578   538810    23.9 | 61.059 % |
c |    305376 |   36053    78899 |   31197   26421   644321    24.4 | 61.107 % |
c |    311143 |   35992    78765 |   34317   32182   814544    25.3 | 61.214 % |
c |    319793 |   35986    78751 |   37749   40829  1077673    26.4 | 61.226 % |
c |    332767 |   35748    78139 |   41523   24169   566082    23.4 | 61.721 % |
c |    352228 |   35196    76994 |   45676   34100   855101    25.1 | 61.995 % |
c |    381420 |   32655    71397 |   50243   16037   292678    18.3 | 65.129 % |
c ==============================================================================
c [1mOptimal solution: -30[0m
s OPTIMUM FOUND
v -C450 -C449 -C448 -C447 -C446 -C445 -C444 C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 C391 C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 C305 -C304 -C303 -C302 -C301 -C300 C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 C211 -C210 C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 C138 -C137 -C136 -C135 -C134 -C133 -C132 C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 C98 -C97 -C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 -C86 C85 -C84 -C83 -C82 -C81 -C80 -C79 -C78 -C77 -C76 -C75 -C74 -C73 -C72 -C71 -C70 -C69 -C68 -C67 -C66 -C65 -C64 -C63 -C62 C61 -C60 -C59 -C58 -C57 -C56 -C55 -C54 -C53 -C52 -C51 -C50 C49 -C48 -C47 -C46 -C45 -C44 -C43 C42 -C41 -C40 -C39 -C38 -C37 -C36 -C35 -C34 -C33 -C32 -C31 C30 -C29 -C28 -C27 -C26 -C25 -C24 -C23 -C22 -C21 -C20 -C19 -C18 -C17 -C16 -C15 -C14 -C13 -C12 -C11 -C10 -C9 -C8 C7 -C6 -C5 -C4 -C3 -C2 -C1
c _______________________________________________________________________________
c 
c restarts              : 95
c conflicts             : 405564         (654 /sec)
c decisions             : 494708         (798 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 620.279 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.91 0.95 0.90 2/54 1997
Raw data (stat): 1997 (runsolver) R 1996 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481738748 1052672 99 4294967295 134512640 135381576 3221224464 3221219716 134979587 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99967 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 1677 0 0 0 994 4 0 0 25 0 1 0 481738748 8785920 1655 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2145 1655 603 41 0 2104 0
vsize: 8580
[startup+20.0009 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 2222 0 0 0 1992 5 0 0 25 0 1 0 481738748 11059200 2200 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2700 2200 603 41 0 2659 0
vsize: 10800
[startup+30.0015 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 2909 0 0 0 2989 7 0 0 25 0 1 0 481738748 13885440 2887 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3390 2887 603 41 0 3349 0
vsize: 13560
[startup+40.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 3395 0 0 0 3988 9 0 0 25 0 1 0 481738748 15880192 3373 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3877 3373 603 41 0 3836 0
vsize: 15508
[startup+50.002 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 3765 0 0 0 4987 10 0 0 25 0 1 0 481738748 17346560 3743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4235 3743 603 41 0 4194 0
vsize: 16940
[startup+60.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4116 0 0 0 5986 11 0 0 25 0 1 0 481738748 18948096 4094 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4094 603 41 0 4585 0
vsize: 18504
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4116 0 0 0 6986 11 0 0 25 0 1 0 481738748 18948096 4094 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4094 603 41 0 4585 0
vsize: 18504
[startup+80.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4116 0 0 0 7986 11 0 0 25 0 1 0 481738748 18948096 4094 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4094 603 41 0 4585 0
vsize: 18504
[startup+90.0021 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4120 0 0 0 8986 11 0 0 25 0 1 0 481738748 18948096 4098 4294967295 134512640 134672761 3221224560 3221223728 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4098 603 41 0 4585 0
vsize: 18504
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4136 0 0 0 9986 11 0 0 25 0 1 0 481738748 18948096 4114 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4114 603 41 0 4585 0
vsize: 18504
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4136 0 0 0 10987 11 0 0 25 0 1 0 481738748 18948096 4114 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4114 603 41 0 4585 0
vsize: 18504
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4136 0 0 0 11987 11 0 0 25 0 1 0 481738748 18948096 4114 4294967295 134512640 134672761 3221224560 3221223728 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4114 603 41 0 4585 0
vsize: 18504
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4136 0 0 0 12986 11 0 0 25 0 1 0 481738748 18948096 4114 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4114 603 41 0 4585 0
vsize: 18504
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4136 0 0 0 13987 11 0 0 25 0 1 0 481738748 18948096 4114 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4114 603 41 0 4585 0
vsize: 18504
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4137 0 0 0 14987 11 0 0 25 0 1 0 481738748 18948096 4115 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4115 603 41 0 4585 0
vsize: 18504
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4137 0 0 0 15987 11 0 0 25 0 1 0 481738748 18948096 4115 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4115 603 41 0 4585 0
vsize: 18504
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4137 0 0 0 16987 11 0 0 25 0 1 0 481738748 18948096 4115 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4115 603 41 0 4585 0
vsize: 18504
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4137 0 0 0 17987 11 0 0 25 0 1 0 481738748 18948096 4115 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4115 603 41 0 4585 0
vsize: 18504
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4137 0 0 0 18987 11 0 0 25 0 1 0 481738748 18948096 4115 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4115 603 41 0 4585 0
vsize: 18504
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4137 0 0 0 19987 11 0 0 25 0 1 0 481738748 18948096 4115 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4115 603 41 0 4585 0
vsize: 18504
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4138 0 0 0 20988 11 0 0 25 0 1 0 481738748 18948096 4116 4294967295 134512640 134672761 3221224560 3221223616 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4116 603 41 0 4585 0
vsize: 18504
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4138 0 0 0 21988 11 0 0 25 0 1 0 481738748 18948096 4116 4294967295 134512640 134672761 3221224560 3221223724 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4116 603 41 0 4585 0
vsize: 18504
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4138 0 0 0 22988 11 0 0 25 0 1 0 481738748 18948096 4116 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4116 603 41 0 4585 0
vsize: 18504
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4138 0 0 0 23988 11 0 0 25 0 1 0 481738748 18948096 4116 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4626 4116 603 41 0 4585 0
vsize: 18504
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4145 0 0 0 24988 11 0 0 25 0 1 0 481738748 19099648 4123 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4123 603 41 0 4622 0
vsize: 18652
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4147 0 0 0 25989 11 0 0 25 0 1 0 481738748 19099648 4125 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4125 603 41 0 4622 0
vsize: 18652
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4148 0 0 0 26989 12 0 0 25 0 1 0 481738748 19099648 4126 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4126 603 41 0 4622 0
vsize: 18652
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4155 0 0 0 27989 12 0 0 25 0 1 0 481738748 19099648 4133 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4133 603 41 0 4622 0
vsize: 18652
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4155 0 0 0 28989 12 0 0 25 0 1 0 481738748 19099648 4133 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4133 603 41 0 4622 0
vsize: 18652
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4155 0 0 0 29989 12 0 0 25 0 1 0 481738748 19099648 4133 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4133 603 41 0 4622 0
vsize: 18652
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4155 0 0 0 30989 12 0 0 25 0 1 0 481738748 19099648 4133 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4133 603 41 0 4622 0
vsize: 18652
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4155 0 0 0 31989 12 0 0 25 0 1 0 481738748 19099648 4133 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4133 603 41 0 4622 0
vsize: 18652
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4155 0 0 0 32990 12 0 0 25 0 1 0 481738748 19099648 4133 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4133 603 41 0 4622 0
vsize: 18652
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4162 0 0 0 33990 12 0 0 25 0 1 0 481738748 19099648 4140 4294967295 134512640 134672761 3221224560 3221223664 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4140 603 41 0 4622 0
vsize: 18652
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4162 0 0 0 34990 12 0 0 25 0 1 0 481738748 19099648 4140 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4140 603 41 0 4622 0
vsize: 18652
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4162 0 0 0 35990 12 0 0 25 0 1 0 481738748 19099648 4140 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4140 603 41 0 4622 0
vsize: 18652
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4162 0 0 0 36990 12 0 0 25 0 1 0 481738748 19099648 4140 4294967295 134512640 134672761 3221224560 3221223744 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4140 603 41 0 4622 0
vsize: 18652
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4162 0 0 0 37990 12 0 0 25 0 1 0 481738748 19099648 4140 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4140 603 41 0 4622 0
vsize: 18652
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4162 0 0 0 38990 12 0 0 25 0 1 0 481738748 19099648 4140 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4140 603 41 0 4622 0
vsize: 18652
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4162 0 0 0 39991 12 0 0 25 0 1 0 481738748 19099648 4140 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4663 4140 603 41 0 4622 0
vsize: 18652
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4396 0 0 0 40990 12 0 0 25 0 1 0 481738748 20553728 4370 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4370 603 41 0 4977 0
vsize: 20072
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4396 0 0 0 41991 12 0 0 25 0 1 0 481738748 20553728 4370 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4370 603 41 0 4977 0
vsize: 20072
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4396 0 0 0 42991 12 0 0 25 0 1 0 481738748 20553728 4370 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4370 603 41 0 4977 0
vsize: 20072
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4396 0 0 0 43991 12 0 0 25 0 1 0 481738748 20553728 4370 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4370 603 41 0 4977 0
vsize: 20072
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4396 0 0 0 44991 12 0 0 25 0 1 0 481738748 20553728 4370 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4370 603 41 0 4977 0
vsize: 20072
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4397 0 0 0 45991 12 0 0 25 0 1 0 481738748 20553728 4371 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4371 603 41 0 4977 0
vsize: 20072
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4402 0 0 0 46992 12 0 0 25 0 1 0 481738748 20553728 4376 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4376 603 41 0 4977 0
vsize: 20072
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4403 0 0 0 47992 12 0 0 25 0 1 0 481738748 20553728 4377 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4377 603 41 0 4977 0
vsize: 20072
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4403 0 0 0 48992 12 0 0 25 0 1 0 481738748 20553728 4377 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4377 603 41 0 4977 0
vsize: 20072
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4403 0 0 0 49992 12 0 0 25 0 1 0 481738748 20553728 4377 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4377 603 41 0 4977 0
vsize: 20072
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4403 0 0 0 50992 12 0 0 25 0 1 0 481738748 20553728 4377 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4377 603 41 0 4977 0
vsize: 20072
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4403 0 0 0 51992 12 0 0 25 0 1 0 481738748 20553728 4377 4294967295 134512640 134672761 3221224560 3221223728 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4377 603 41 0 4977 0
vsize: 20072
[startup+530.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4403 0 0 0 52993 12 0 0 25 0 1 0 481738748 20553728 4377 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4377 603 41 0 4977 0
vsize: 20072
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4403 0 0 0 53993 12 0 0 25 0 1 0 481738748 20553728 4377 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4377 603 41 0 4977 0
vsize: 20072
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4404 0 0 0 54993 12 0 0 25 0 1 0 481738748 20553728 4378 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4378 603 41 0 4977 0
vsize: 20072
[startup+560.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4408 0 0 0 55993 12 0 0 25 0 1 0 481738748 20553728 4382 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4382 603 41 0 4977 0
vsize: 20072
[startup+570.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4411 0 0 0 56993 12 0 0 25 0 1 0 481738748 20553728 4385 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4385 603 41 0 4977 0
vsize: 20072
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4411 0 0 0 57993 12 0 0 25 0 1 0 481738748 20553728 4385 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4385 603 41 0 4977 0
vsize: 20072
[startup+590.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4411 0 0 0 58994 12 0 0 25 0 1 0 481738748 20553728 4385 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4385 603 41 0 4977 0
vsize: 20072
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4411 0 0 0 59994 12 0 0 25 0 1 0 481738748 20553728 4385 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4385 603 41 0 4977 0
vsize: 20072
[startup+610.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4411 0 0 0 60994 12 0 0 25 0 1 0 481738748 20553728 4385 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4385 603 41 0 4977 0
vsize: 20072
[startup+620.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4411 0 0 0 61994 12 0 0 25 0 1 0 481738748 20553728 4385 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4385 603 41 0 4977 0
vsize: 20072
[startup+620.367 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 1997
Raw data (stat): 1997 (minisat+) R 1996 27222 27221 0 -1 0 4411 0 0 0 61994 12 0 0 25 0 1 0 481738748 20553728 4385 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5018 4385 603 41 0 4977 0
vsize: 0

Child status: 30
Real time (s): 620.366
CPU time (s): 620.43
CPU user time (s): 620.295
CPU system time (s): 0.134979
CPU usage (%): 100.01
Max. virtual memory (Kb): 20072
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	-30
#### END VERIFIER DATA ####