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/frb40-19-opb/normalized-frb40-19-4.opb
MD5SUM	7731f50c352d2fd7b2fe148b68bfdbab
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	760
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	760
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	760
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.06
Number of variables	760
Total number of constraints	41605
Number of constraints which are clauses	41605
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 5244

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-13 22:54:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3711 boxname=wulflinc11 idbench=327 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7731f50c352d2fd7b2fe148b68bfdbab  /oldhome/oroussel/tmp/wulflinc11/normalized-frb40-19-4.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc11/normalized-frb40-19-4.opb /oldhome/oroussel/tmp/wulflinc11/normalized-frb40-19-4.opb
IDLAUNCH: 3711
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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	: 2
cpu MHz		: 451.028
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:        915120 kB
Buffers:         34672 kB
Cached:          60560 kB
SwapCached:       4932 kB
Active:          55860 kB
Inactive:        47212 kB
HighTotal:      131008 kB
HighFree:        66640 kB
LowTotal:       903652 kB
LowFree:        848480 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10988 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:14:32 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3711 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41605 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 |   41605    83210 |   13868       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1492   maxlim: 29   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   51804   119684 |   17268       0        0     nan |  0.000 % |
c |       100 |   51786   119622 |   18994      92     1054    11.5 |  0.272 % |
c |       250 |   51768   119560 |   20894     236     2722    11.5 |  0.361 % |
c |       475 |   51750   119498 |   22983     457     5778    12.6 |  0.451 % |
c |       812 |   51723   119405 |   25282     788     9802    12.4 |  0.582 % |
c |      1318 |   51687   119281 |   27810    1285    16439    12.8 |  0.806 % |
c |      2079 |   51597   118971 |   30591    2021    26764    13.2 |  1.209 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2851 |   51578   118908 |   17192    2788    47178    16.9 |  1.209 % |
c |      2952 |   51578   118908 |   18911    2889    48348    16.7 |  1.390 % |
c |      3102 |   51569   118877 |   20802    3036    50580    16.7 |  1.431 % |
c |      3327 |   51518   118702 |   22882    3247    53524    16.5 |  1.699 % |
c |      3664 |   51459   118499 |   25170    3564    58641    16.5 |  2.061 % |
c |      4170 |   51273   117859 |   27687    4021    68867    17.1 |  3.180 % |
c |      4929 |   51030   117030 |   30456    4722    84969    18.0 |  4.651 % |
c |      6068 |   50895   116565 |   33502    5823   125038    21.5 |  5.501 % |
c |      7776 |   50284   114462 |   36852    7335   161667    22.0 |  9.571 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9472 |   49937   113257 |   16645    8889   210286    23.7 |  9.571 % |
c |      9572 |   49897   113121 |   18309    8980   212379    23.7 | 12.388 % |
c |      9722 |   49879   113059 |   20140    9124   217130    23.8 | 12.478 % |
c |      9947 |   49870   113028 |   22154    9317   227701    24.4 | 12.522 % |
c |     10284 |   49800   112786 |   24369    9643   239340    24.8 | 13.059 % |
c |     10791 |   49800   112786 |   26806   10150   286945    28.3 | 13.059 % |
c |     11552 |   49727   112531 |   29487   10859   317551    29.2 | 13.640 % |
c |     12691 |   49624   112182 |   32436   11968   404134    33.8 | 14.494 % |
c |     14400 |   49512   111796 |   35680   13624   501095    36.8 | 15.250 % |
c |     16962 |   49428   111506 |   39248   16129   717329    44.5 | 15.832 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 32   maxlim: 32   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19494 |   49508   111785 |   16502   18524   951046    51.3 | 15.832 % |
c |     19595 |   49508   111785 |   18152    9363   545024    58.2 | 16.320 % |
c |     19745 |   49496   111745 |   19967    9508   551047    58.0 | 16.409 % |
c |     19970 |   49458   111615 |   21964    9710   557342    57.4 | 16.678 % |
c |     20307 |   49395   111398 |   24160   10033   576973    57.5 | 17.161 % |
c |     20813 |   49285   111016 |   26576   10496   604755    57.6 | 18.045 % |
c |     21575 |   49247   110886 |   29234   11236   654655    58.3 | 18.314 % |
c |     22714 |   49228   110819 |   32157   12372   756864    61.2 | 18.492 % |
c |     24422 |   49217   110780 |   35373   14076   990201    70.3 | 18.579 % |
c |     26985 |   49072   110279 |   38910   16589  1207292    72.8 | 19.637 % |
c |     30831 |   49007   110056 |   42801   20402  1597773    78.3 | 20.039 % |
c |     36598 |   48843   109492 |   47082   26019  2163871    83.2 | 21.277 % |
c |     45247 |   48710   109029 |   51790   34565  3151344    91.2 | 22.291 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 33   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45604 |   48711   109036 |   16237   34922  3178919    91.0 | 22.291 % |
c |     45704 |   48685   108946 |   17860   15382  1318432    85.7 | 22.502 % |
c |     45854 |   48685   108946 |   19646   15532  1325898    85.4 | 22.502 % |
c |     46080 |   48551   108482 |   21611   15700  1330116    84.7 | 23.519 % |
c |     46418 |   48524   108391 |   23772   16023  1339236    83.6 | 23.696 % |
c |     46926 |   48515   108360 |   26149   16518  1376270    83.3 | 23.740 % |
c |     47685 |   48506   108329 |   28764   17263  1435287    83.1 | 23.784 % |
c |     48824 |   48493   108282 |   31641   18398  1493245    81.2 | 23.917 % |
c |     50532 |   48416   108017 |   34805   20062  1589983    79.3 | 24.492 % |
c |     53094 |   48380   107891 |   38285   22594  1820063    80.6 | 24.806 % |
c |     56938 |   48324   107697 |   42114   26429  2114434    80.0 | 25.291 % |
c |     62704 |   48229   107366 |   46326   32152  2471957    76.9 | 26.087 % |
c |     71353 |   48031   106678 |   50958   40696  3179953    78.1 | 27.630 % |
c |     84330 |   47972   106475 |   56054   15364  2146637   139.7 | 28.117 % |
c |    103791 |   47966   106455 |   61659   34822  5203135   149.4 | 28.161 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 34   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    114948 |   47887   106189 |   15962   45945  6271999   136.5 | 28.161 % |
c |    115048 |   47887   106189 |   17558   14651  1197520    81.7 | 28.900 % |
c |    115199 |   47887   106189 |   19314   14802  1201119    81.1 | 28.900 % |
c |    115425 |   47887   106189 |   21245   15028  1210785    80.6 | 28.900 % |
c |    115762 |   47887   106189 |   23369   15365  1231515    80.2 | 28.900 % |
c |    116268 |   47887   106189 |   25706   15871  1263268    79.6 | 28.900 % |
c |    117027 |   47887   106189 |   28277   16630  1345066    80.9 | 28.903 % |
c |    118167 |   47887   106189 |   31105   17770  1407540    79.2 | 28.900 % |
c |    119876 |   47887   106189 |   34215   19479  1571081    80.7 | 28.900 % |
c |    122439 |   47887   106189 |   37637   22042  1855515    84.2 | 28.903 % |
c |    126284 |   47881   106169 |   41401   25882  2058593    79.5 | 28.944 % |
c |    132050 |   47881   106169 |   45541   31648  2436855    77.0 | 28.947 % |
c |    140702 |   47881   106169 |   50095   40300  3232777    80.2 | 28.944 % |
c |    153676 |   47839   106023 |   55105   17312   788615    45.6 | 29.302 % |
c |    173137 |   47839   106023 |   60615   36773  1839246    50.0 | 29.302 % |
c |    202330 |   47839   106023 |   66677   19486   593423    30.5 | 29.302 % |
c |    246120 |   47839   106023 |   73344   63276  1879177    29.7 | 29.301 % |
c |    311805 |   47839   106023 |   80679   71907  2037338    28.3 | 29.301 % |
c |    410331 |   47839   106023 |   88747   41635  1972453    47.4 | 29.302 % |
c |    558120 |   47839   106023 |   97622   51810  2388088    46.1 | 29.301 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 C611 -C610 -C609 C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 C460 -C459 -C458 -C457 -C456 -C455 -C454 C453 -C452 -C451 -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 -#### 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 5294
Raw data (stat): 5294 (runsolver) R 5293 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421485048 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 2147 0 0 0 991 7 0 0 25 0 1 0 421485048 10416128 2125 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2543 2125 603 41 0 2502 0
vsize: 10172
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 2231 0 0 0 1990 7 0 0 25 0 1 0 421485048 10788864 2209 4294967295 134512640 134672761 3221224560 3221223712 134565179 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2634 2209 603 41 0 2593 0
vsize: 10536
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 3069 0 0 0 2987 10 0 0 25 0 1 0 421485048 14155776 3047 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3456 3047 603 41 0 3415 0
vsize: 13824
[startup+40.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 3821 0 0 0 3985 12 0 0 25 0 1 0 421485048 17248256 3799 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4211 3799 603 41 0 4170 0
vsize: 16844
[startup+50.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 4569 0 0 0 4984 14 0 0 25 0 1 0 421485048 20459520 4547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4995 4547 603 41 0 4954 0
vsize: 19980
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 4618 0 0 0 5983 14 0 0 25 0 1 0 421485048 20684800 4596 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5050 4596 603 41 0 5009 0
vsize: 20200
[startup+70.0029 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 4618 0 0 0 6983 14 0 0 25 0 1 0 421485048 20684800 4596 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5050 4596 603 41 0 5009 0
vsize: 20200
[startup+80.0041 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 4620 0 0 0 7983 14 0 0 25 0 1 0 421485048 20684800 4598 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5050 4598 603 41 0 5009 0
vsize: 20200
[startup+90.0038 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 4895 0 0 0 8982 15 0 0 25 0 1 0 421485048 21762048 4873 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5313 4873 603 41 0 5272 0
vsize: 21252
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 5595 0 0 0 9981 17 0 0 25 0 1 0 421485048 24576000 5573 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6000 5573 603 41 0 5959 0
vsize: 24000
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 6231 0 0 0 10979 19 0 0 25 0 1 0 421485048 27275264 6209 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6659 6209 603 41 0 6618 0
vsize: 26636
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 6820 0 0 0 11978 21 0 0 25 0 1 0 421485048 29696000 6798 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7250 6798 603 41 0 7209 0
vsize: 29000
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 6835 0 0 0 12978 21 0 0 25 0 1 0 421485048 29696000 6813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7250 6813 603 41 0 7209 0
vsize: 29000
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 6835 0 0 0 13978 21 0 0 25 0 1 0 421485048 29696000 6813 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7250 6813 603 41 0 7209 0
vsize: 29000
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 6835 0 0 0 14978 21 0 0 25 0 1 0 421485048 29696000 6813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7250 6813 603 41 0 7209 0
vsize: 29000
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 6925 0 0 0 15978 21 0 0 25 0 1 0 421485048 30101504 6903 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7349 6903 603 41 0 7308 0
vsize: 29396
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 7433 0 0 0 16977 23 0 0 25 0 1 0 421485048 32120832 7411 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7842 7411 603 41 0 7801 0
vsize: 31368
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8007 0 0 0 17975 24 0 0 25 0 1 0 421485048 34529280 7985 4294967295 134512640 134672761 3221224560 3221223860 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7985 603 41 0 8389 0
vsize: 33720
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8007 0 0 0 18975 24 0 0 25 0 1 0 421485048 34529280 7985 4294967295 134512640 134672761 3221224560 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7985 603 41 0 8389 0
vsize: 33720
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8007 0 0 0 19976 25 0 0 25 0 1 0 421485048 34529280 7985 4294967295 134512640 134672761 3221224560 3221223744 134558914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7985 603 41 0 8389 0
vsize: 33720
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8007 0 0 0 20976 25 0 0 25 0 1 0 421485048 34529280 7985 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7985 603 41 0 8389 0
vsize: 33720
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8007 0 0 0 21976 25 0 0 25 0 1 0 421485048 34529280 7985 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7985 603 41 0 8389 0
vsize: 33720
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8007 0 0 0 22976 25 0 0 25 0 1 0 421485048 34529280 7985 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7985 603 41 0 8389 0
vsize: 33720
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8007 0 0 0 23976 25 0 0 25 0 1 0 421485048 34529280 7985 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7985 603 41 0 8389 0
vsize: 33720
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8007 0 0 0 24977 25 0 0 25 0 1 0 421485048 34529280 7985 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7985 603 41 0 8389 0
vsize: 33720
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8007 0 0 0 25977 25 0 0 25 0 1 0 421485048 34529280 7985 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7985 603 41 0 8389 0
vsize: 33720
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8007 0 0 0 26977 25 0 0 25 0 1 0 421485048 34529280 7985 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7985 603 41 0 8389 0
vsize: 33720
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8007 0 0 0 27977 25 0 0 25 0 1 0 421485048 34529280 7985 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7985 603 41 0 8389 0
vsize: 33720
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8009 0 0 0 28977 25 0 0 25 0 1 0 421485048 34529280 7987 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7987 603 41 0 8389 0
vsize: 33720
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8013 0 0 0 29977 25 0 0 25 0 1 0 421485048 34529280 7991 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7991 603 41 0 8389 0
vsize: 33720
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8016 0 0 0 30977 25 0 0 25 0 1 0 421485048 34529280 7994 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7994 603 41 0 8389 0
vsize: 33720
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8016 0 0 0 31978 25 0 0 25 0 1 0 421485048 34529280 7994 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7994 603 41 0 8389 0
vsize: 33720
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5294
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8017 0 0 0 32978 25 0 0 25 0 1 0 421485048 34529280 7995 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8430 7995 603 41 0 8389 0
vsize: 33720
[startup+340.012 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 5347
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8019 0 0 0 33978 25 0 0 25 0 1 0 421485048 34529280 7997 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8430 7997 603 41 0 8389 0
vsize: 33720
[startup+350.013 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 5347
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8019 0 0 0 34978 25 0 0 25 0 1 0 421485048 34529280 7997 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8430 7997 603 41 0 8389 0
vsize: 33720
[startup+360.013 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 5347
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8019 0 0 0 35978 25 0 0 25 0 1 0 421485048 34529280 7997 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8430 7997 603 41 0 8389 0
vsize: 33720
[startup+370.014 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 5347
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8019 0 0 0 36978 25 0 0 25 0 1 0 421485048 34529280 7997 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8430 7997 603 41 0 8389 0
vsize: 33720
[startup+380.015 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 5347
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8019 0 0 0 37979 25 0 0 25 0 1 0 421485048 34529280 7997 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8430 7997 603 41 0 8389 0
vsize: 33720
[startup+390.014 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 5347
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8019 0 0 0 38979 25 0 0 25 0 1 0 421485048 34529280 7997 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8430 7997 603 41 0 8389 0
vsize: 33720
[startup+400.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 5347
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8021 0 0 0 39979 25 0 0 25 0 1 0 421485048 34529280 7999 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8430 7999 603 41 0 8389 0
vsize: 33720
[startup+410.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 5347
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8026 0 0 0 40979 25 0 0 25 0 1 0 421485048 34791424 8004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8004 603 41 0 8453 0
vsize: 33976
[startup+420.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8030 0 0 0 41979 25 0 0 25 0 1 0 421485048 34791424 8008 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8008 603 41 0 8453 0
vsize: 33976
[startup+430.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8032 0 0 0 42980 25 0 0 25 0 1 0 421485048 34791424 8010 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8010 603 41 0 8453 0
vsize: 33976
[startup+440.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8032 0 0 0 43980 25 0 0 25 0 1 0 421485048 34791424 8010 4294967295 134512640 134672761 3221224560 3221223744 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8010 603 41 0 8453 0
vsize: 33976
[startup+450.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8032 0 0 0 44980 25 0 0 25 0 1 0 421485048 34791424 8010 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8010 603 41 0 8453 0
vsize: 33976
[startup+460.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8033 0 0 0 45980 25 0 0 25 0 1 0 421485048 34791424 8011 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8011 603 41 0 8453 0
vsize: 33976
[startup+470.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8033 0 0 0 46980 25 0 0 25 0 1 0 421485048 34791424 8011 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8011 603 41 0 8453 0
vsize: 33976
[startup+480.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8033 0 0 0 47981 25 0 0 25 0 1 0 421485048 34791424 8011 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8011 603 41 0 8453 0
vsize: 33976
[startup+490.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8033 0 0 0 48981 25 0 0 25 0 1 0 421485048 34791424 8011 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8011 603 41 0 8453 0
vsize: 33976
[startup+500.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8033 0 0 0 49981 25 0 0 25 0 1 0 421485048 34791424 8011 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8011 603 41 0 8453 0
vsize: 33976
[startup+510.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8033 0 0 0 50981 25 0 0 25 0 1 0 421485048 34791424 8011 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8011 603 41 0 8453 0
vsize: 33976
[startup+520.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8033 0 0 0 51981 25 0 0 25 0 1 0 421485048 34791424 8011 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8011 603 41 0 8453 0
vsize: 33976
[startup+530.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8033 0 0 0 52981 25 0 0 25 0 1 0 421485048 34791424 8011 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8011 603 41 0 8453 0
vsize: 33976
[startup+540.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8033 0 0 0 53982 25 0 0 25 0 1 0 421485048 34791424 8011 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8011 603 41 0 8453 0
vsize: 33976
[startup+550.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8033 0 0 0 54982 25 0 0 25 0 1 0 421485048 34791424 8011 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8011 603 41 0 8453 0
vsize: 33976
[startup+560.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8033 0 0 0 55982 25 0 0 25 0 1 0 421485048 34791424 8011 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8494 8011 603 41 0 8453 0
vsize: 33976
[startup+570.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8034 0 0 0 56981 25 0 0 25 0 1 0 421485048 34791424 8012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8012 603 41 0 8453 0
vsize: 33976
[startup+580.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8037 0 0 0 57981 25 0 0 25 0 1 0 421485048 34791424 8015 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8015 603 41 0 8453 0
vsize: 33976
[startup+590.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8039 0 0 0 58981 25 0 0 25 0 1 0 421485048 34791424 8017 4294967295 134512640 134672761 3221224560 3221223728 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8017 603 41 0 8453 0
vsize: 33976
[startup+600.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8040 0 0 0 59981 25 0 0 25 0 1 0 421485048 34791424 8018 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8018 603 41 0 8453 0
vsize: 33976
[startup+610.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8040 0 0 0 60982 25 0 0 25 0 1 0 421485048 34791424 8018 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8018 603 41 0 8453 0
vsize: 33976
[startup+620.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8040 0 0 0 61982 25 0 0 25 0 1 0 421485048 34791424 8018 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8018 603 41 0 8453 0
vsize: 33976
[startup+630.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8040 0 0 0 62982 25 0 0 25 0 1 0 421485048 34791424 8018 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8018 603 41 0 8453 0
vsize: 33976
[startup+640.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8040 0 0 0 63982 25 0 0 25 0 1 0 421485048 34791424 8018 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8018 603 41 0 8453 0
vsize: 33976
[startup+650.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8040 0 0 0 64983 25 0 0 25 0 1 0 421485048 34791424 8018 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8018 603 41 0 8453 0
vsize: 33976
[startup+660.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8040 0 0 0 65983 25 0 0 25 0 1 0 421485048 34791424 8018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8018 603 41 0 8453 0
vsize: 33976
[startup+670.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5349
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8040 0 0 0 66983 25 0 0 25 0 1 0 421485048 34791424 8018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8018 603 41 0 8453 0
vsize: 33976
[startup+680.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8040 0 0 0 67983 25 0 0 25 0 1 0 421485048 34791424 8018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8018 603 41 0 8453 0
vsize: 33976
[startup+690.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8040 0 0 0 68983 25 0 0 25 0 1 0 421485048 34791424 8018 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8018 603 41 0 8453 0
vsize: 33976
[startup+700.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8040 0 0 0 69984 25 0 0 25 0 1 0 421485048 34791424 8018 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8018 603 41 0 8453 0
vsize: 33976
[startup+710.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8040 0 0 0 70984 25 0 0 25 0 1 0 421485048 34791424 8018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8018 603 41 0 8453 0
vsize: 33976
[startup+720.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8041 0 0 0 71984 25 0 0 25 0 1 0 421485048 34791424 8019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8019 603 41 0 8453 0
vsize: 33976
[startup+730.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8041 0 0 0 72984 25 0 0 25 0 1 0 421485048 34791424 8019 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8019 603 41 0 8453 0
vsize: 33976
[startup+740.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8041 0 0 0 73984 25 0 0 25 0 1 0 421485048 34791424 8019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8019 603 41 0 8453 0
vsize: 33976
[startup+750.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8041 0 0 0 74985 25 0 0 25 0 1 0 421485048 34791424 8019 4294967295 134512640 134672761 3221224560 3221223664 134559998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8019 603 41 0 8453 0
vsize: 33976
[startup+760.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8041 0 0 0 75984 25 0 0 25 0 1 0 421485048 34791424 8019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8019 603 41 0 8453 0
vsize: 33976
[startup+770.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8041 0 0 0 76985 25 0 0 25 0 1 0 421485048 34791424 8019 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8019 603 41 0 8453 0
vsize: 33976
[startup+780.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8041 0 0 0 77985 25 0 0 25 0 1 0 421485048 34791424 8019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8019 603 41 0 8453 0
vsize: 33976
[startup+790.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8041 0 0 0 78985 25 0 0 25 0 1 0 421485048 34791424 8019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8019 603 41 0 8453 0
vsize: 33976
[startup+800.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8041 0 0 0 79985 25 0 0 25 0 1 0 421485048 34791424 8019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8019 603 41 0 8453 0
vsize: 33976
[startup+810.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8041 0 0 0 80985 25 0 0 25 0 1 0 421485048 34791424 8019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8019 603 41 0 8453 0
vsize: 33976
[startup+820.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8041 0 0 0 81986 25 0 0 25 0 1 0 421485048 34791424 8019 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8019 603 41 0 8453 0
vsize: 33976
[startup+830.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8044 0 0 0 82986 25 0 0 25 0 1 0 421485048 34791424 8022 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8022 603 41 0 8453 0
vsize: 33976
[startup+840.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8048 0 0 0 83986 26 0 0 25 0 1 0 421485048 34791424 8026 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8026 603 41 0 8453 0
vsize: 33976
[startup+850.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 84986 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223576 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+860.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 85986 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+870.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 86987 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+880.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 87987 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+890.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 88987 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+900.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 89987 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+910.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 90987 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+920.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 91988 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+930.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 92988 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+940.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 93988 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+950.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 94988 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+960.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 95989 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+970.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 96989 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+980.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 97989 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+990.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 98989 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 99989 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 100990 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 101990 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 102990 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 103990 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 104991 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 105991 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 106990 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 107989 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 108988 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 109988 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 110989 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 111989 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 112989 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8049 0 0 0 113989 26 0 0 25 0 1 0 421485048 34791424 8027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8027 603 41 0 8453 0
vsize: 33976
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8051 0 0 0 114990 26 0 0 25 0 1 0 421485048 34791424 8029 4294967295 134512640 134672761 3221224560 3221223664 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8029 603 41 0 8453 0
vsize: 33976
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8055 0 0 0 115990 26 0 0 25 0 1 0 421485048 34791424 8033 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8494 8033 603 41 0 8453 0
vsize: 33976
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8083 0 0 0 116990 26 0 0 25 0 1 0 421485048 34922496 8061 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8526 8061 603 41 0 8485 0
vsize: 34104
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8083 0 0 0 117990 26 0 0 25 0 1 0 421485048 34922496 8061 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8526 8061 603 41 0 8485 0
vsize: 34104
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8083 0 0 0 118990 26 0 0 25 0 1 0 421485048 34922496 8061 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8526 8061 603 41 0 8485 0
vsize: 34104
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5351
Raw data (stat): 5294 (minisat+) R 5293 32461 32460 0 -1 0 8083 0 0 0 119990 26 0 0 25 0 1 0 421485048 34922496 8061 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8526 8061 603 41 0 8485 0
vsize: 34104
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 5351
Raw data (stat): 5294 (minisat+) Z 5293 32461 32460 0 -1 12 8086 0 0 0 119991 28 0 0 25 0 1 0 421485048 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.2
CPU user time (s): 1199.91
CPU system time (s): 0.285956
CPU usage (%): 100.01
Max. virtual memory (Kb): 34104
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####