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-5.opb
MD5SUM	38d41fdbe49543e8928c5210e4323f00
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-31
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.08
Number of variables	760
Total number of constraints	41619
Number of constraints which are clauses	41619
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 5245

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-13 22:54:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3712 boxname=wulflinc31 idbench=328 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  38d41fdbe49543e8928c5210e4323f00  /oldhome/oroussel/tmp/wulflinc31/normalized-frb40-19-5.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc31/normalized-frb40-19-5.opb /oldhome/oroussel/tmp/wulflinc31/normalized-frb40-19-5.opb
IDLAUNCH: 3712
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        907244 kB
Buffers:         34716 kB
Cached:          54040 kB
SwapCached:        392 kB
Active:          49200 kB
Inactive:        42736 kB
HighTotal:      131008 kB
HighFree:        73248 kB
LowTotal:       903652 kB
LowFree:        833996 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29884 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:14:35 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3712 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41619 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 |   41619    83238 |   13873       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1492   maxlim: 27   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   51813   119694 |   17271       0        0     nan |  0.000 % |
c |       100 |   51813   119694 |   18998     100     1230    12.3 |  0.138 % |
c |       250 |   51760   119509 |   20897     230     2712    11.8 |  0.408 % |
c |       475 |   51742   119447 |   22987     451     5515    12.2 |  0.497 % |
c |       812 |   51742   119447 |   25286     788     9735    12.4 |  0.496 % |
c |      1320 |   51697   119292 |   27815    1283    19870    15.5 |  0.720 % |
c |      2079 |   51625   119044 |   30596    2023    30563    15.1 |  1.076 % |
c |      3218 |   51438   118401 |   33656    3116    48503    15.6 |  2.151 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 29   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3708 |   51375   118185 |   17125    3586    55984    15.6 |  2.151 % |
c |      3808 |   51366   118154 |   18837    3684    57817    15.7 |  2.641 % |
c |      3958 |   51366   118154 |   20721    3834    60776    15.9 |  2.641 % |
c |      4183 |   51324   118010 |   22793    4047    66837    16.5 |  2.910 % |
c |      4520 |   51187   117541 |   25072    4341    73244    16.9 |  3.671 % |
c |      5026 |   50993   116873 |   27579    4770    83011    17.4 |  4.884 % |
c |      5785 |   50837   116337 |   30337    5491   103499    18.8 |  5.864 % |
c |      6924 |   50573   115433 |   33371    6522   128650    19.7 |  7.479 % |
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 |      8449 |   50168   114038 |   16722    7877   178023    22.6 |  7.479 % |
c |      8551 |   50162   114018 |   18394    7976   181478    22.8 | 10.376 % |
c |      8702 |   50162   114018 |   20233    8127   194391    23.9 | 10.380 % |
c |      8927 |   50124   113888 |   22256    8341   201307    24.1 | 10.651 % |
c |      9264 |   50109   113837 |   24482    8674   221872    25.6 | 10.733 % |
c |      9770 |   50010   113496 |   26930    9141   254827    27.9 | 11.498 % |
c |     10529 |   49610   112122 |   29624    9777   272478    27.9 | 14.759 % |
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 |     11104 |   49415   111437 |   16471   10282   292388    28.4 | 14.759 % |
c |     11205 |   49388   111346 |   18118   10371   294965    28.4 | 16.592 % |
c |     11355 |   49388   111346 |   19929   10521   300039    28.5 | 16.592 % |
c |     11580 |   49368   111276 |   21922   10738   309987    28.9 | 16.731 % |
c |     11917 |   49224   110782 |   24115   11028   318955    28.9 | 17.889 % |
c |     12424 |   49224   110782 |   26526   11535   356121    30.9 | 17.889 % |
c |     13183 |   49134   110466 |   29179   12236   390269    31.9 | 18.560 % |
c |     14322 |   49102   110352 |   32097   13361   509040    38.1 | 18.876 % |
c |     16030 |   48983   109941 |   35307   15030   604466    40.2 | 19.767 % |
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 |     16437 |   49118   110389 |   16372   15437   627189    40.6 | 19.767 % |
c |     16537 |   49109   110358 |   18009   15531   630805    40.6 | 19.774 % |
c |     16687 |   49100   110327 |   19810   15643   639118    40.9 | 19.814 % |
c |     16912 |   49100   110327 |   21791   15868   653594    41.2 | 19.814 % |
c |     17249 |   49011   110020 |   23970   16144   663042    41.1 | 20.478 % |
c |     17756 |   48938   109767 |   26367   16636   684352    41.1 | 21.097 % |
c |     18515 |   48887   109590 |   29003   17334   736384    42.5 | 21.499 % |
c |     19657 |   48827   109378 |   31904   18451   828828    44.9 | 22.026 % |
c |     21367 |   48679   108868 |   35094   20027   934608    46.7 | 23.264 % |
c |     23929 |   48596   108581 |   38604   22491  1140982    50.7 | 23.883 % |
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 |     26535 |   48534   108373 |   16178   24893  1386049    55.7 | 23.883 % |
c |     26635 |   48525   108342 |   17795   12538   750443    59.9 | 24.315 % |
c |     26786 |   48485   108204 |   19575   12681   757236    59.7 | 24.624 % |
c |     27011 |   48437   108038 |   21532   12897   764369    59.3 | 25.022 % |
c |     27348 |   48437   108038 |   23686   13234   799377    60.4 | 25.022 % |
c |     27856 |   48428   108007 |   26054   13721   831771    60.6 | 25.066 % |
c |     28615 |   48410   107945 |   28660   14458   854493    59.1 | 25.155 % |
c |     29754 |   48410   107945 |   31526   15597   946655    60.7 | 25.159 % |
c |     31463 |   48341   107710 |   34678   17218  1100303    63.9 | 25.556 % |
c |     34026 |   48296   107557 |   38146   19749  1224783    62.0 | 25.818 % |
c |     37870 |   48270   107467 |   41961   23524  1556590    66.2 | 25.995 % |
c |     43639 |   48178   107157 |   46157   29221  2182283    74.7 | 26.702 % |
c |     52288 |   48178   107157 |   50773   37870  3185392    84.1 | 26.702 % |
c |     65263 |   48136   107011 |   55850   50791  5131701   101.0 | 27.056 % |
c |     84726 |   47979   106470 |   61435   27865  3254239   116.8 | 28.338 % |
c |    113918 |   47979   106470 |   67579   57057  7489018   131.3 | 28.341 % |
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 |    153668 |   47935   106325 |   15978   42607  4791882   112.5 | 28.341 % |
c |    153768 |   47927   106297 |   17575   13730  1524080   111.0 | 28.723 % |
c |    153918 |   47927   106297 |   19333   13880  1531256   110.3 | 28.726 % |
c |    154149 |   47927   106297 |   21266   14111  1543489   109.4 | 28.723 % |
c |    154487 |   47927   106297 |   23393   14449  1555560   107.7 | 28.727 % |
c |    154995 |   47927   106297 |   25732   14957  1595792   106.7 | 28.723 % |
c |    155754 |   47901   106207 |   28306   15706  1623965   103.4 | 28.900 % |
c |    156893 |   47901   106207 |   31136   16845  1673261    99.3 | 28.903 % |
c |    158601 |   47901   106207 |   34250   18553  1800647    97.1 | 28.900 % |
c |    161163 |   47901   106207 |   37675   21115  1969013    93.3 | 28.903 % |
c |    165007 |   47901   106207 |   41442   24959  2264053    90.7 | 28.900 % |
c |    170773 |   47871   106101 |   45587   30712  2634474    85.8 | 29.165 % |
c |    179422 |   47871   106101 |   50145   39361  3447144    87.6 | 29.167 % |
c |    192397 |   47871   106101 |   55160   15417  1467813    95.2 | 29.165 % |
c |    211860 |   47819   105923 |   60676   34789  2445649    70.3 | 29.607 % |
c |    241056 |   47819   105923 |   66744   16665  1532012    91.9 | 29.609 % |
c |    284847 |   47819   105923 |   73418   60456  6794968   112.4 | 29.610 % |
c |    350532 |   47819   105923 |   80760   65561  7276172   111.0 | 29.610 % |
c |    449059 |   47819   105923 |   88836   32370  2903192    89.7 | 29.610 % |
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.84 0.94 0.90 2/54 26721
Raw data (stat): 26721 (runsolver) R 26720 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479695992 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 2144 0 0 0 992 5 0 0 25 0 1 0 479695992 10399744 2122 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2539 2122 603 41 0 2498 0
vsize: 10156
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 2185 0 0 0 1992 6 0 0 25 0 1 0 479695992 10534912 2163 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2163 603 41 0 2531 0
vsize: 10288
[startup+30.0024 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 2720 0 0 0 2989 8 0 0 25 0 1 0 479695992 12791808 2698 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3123 2698 603 41 0 3082 0
vsize: 12492
[startup+40.0033 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 3043 0 0 0 3988 9 0 0 25 0 1 0 479695992 14131200 3021 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 3021 603 41 0 3409 0
vsize: 13800
[startup+50.0029 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 3943 0 0 0 4985 13 0 0 25 0 1 0 479695992 17752064 3921 4294967295 134512640 134672761 3221224560 3221223744 134559581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4334 3921 603 41 0 4293 0
vsize: 17336
[startup+60.0031 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 4596 0 0 0 5983 15 0 0 25 0 1 0 479695992 20549632 4574 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5017 4574 603 41 0 4976 0
vsize: 20068
[startup+70.0043 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 5215 0 0 0 6980 18 0 0 25 0 1 0 479695992 23101440 5193 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5640 5193 603 41 0 5599 0
vsize: 22560
[startup+80.0061 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 6024 0 0 0 7978 20 0 0 25 0 1 0 479695992 26324992 6002 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6427 6002 603 41 0 6386 0
vsize: 25708
[startup+90.007 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 6671 0 0 0 8977 21 0 0 25 0 1 0 479695992 29016064 6649 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7084 6649 603 41 0 7043 0
vsize: 28336
[startup+100.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 7346 0 0 0 9975 22 0 0 25 0 1 0 479695992 31834112 7324 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7772 7324 603 41 0 7731 0
vsize: 31088
[startup+110.008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 7972 0 0 0 10974 24 0 0 25 0 1 0 479695992 34390016 7950 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8396 7950 603 41 0 8355 0
vsize: 33584
[startup+120.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 8020 0 0 0 11974 24 0 0 25 0 1 0 479695992 34525184 7998 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7998 603 41 0 8388 0
vsize: 33716
[startup+130.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 8020 0 0 0 12974 24 0 0 25 0 1 0 479695992 34525184 7998 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7998 603 41 0 8388 0
vsize: 33716
[startup+140.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 8020 0 0 0 13975 24 0 0 25 0 1 0 479695992 34525184 7998 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7998 603 41 0 8388 0
vsize: 33716
[startup+150.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 8020 0 0 0 14975 24 0 0 25 0 1 0 479695992 34525184 7998 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7998 603 41 0 8388 0
vsize: 33716
[startup+160.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 8020 0 0 0 15975 24 0 0 25 0 1 0 479695992 34525184 7998 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7998 603 41 0 8388 0
vsize: 33716
[startup+170.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 8020 0 0 0 16975 24 0 0 25 0 1 0 479695992 34525184 7998 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 7998 603 41 0 8388 0
vsize: 33716
[startup+180.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 8031 0 0 0 17975 24 0 0 25 0 1 0 479695992 34525184 8009 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8429 8009 603 41 0 8388 0
vsize: 33716
[startup+190.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 8488 0 0 0 18974 25 0 0 25 0 1 0 479695992 36397056 8466 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8886 8466 603 41 0 8845 0
vsize: 35544
[startup+200.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 8922 0 0 0 19974 26 0 0 25 0 1 0 479695992 38260736 8900 4294967295 134512640 134672761 3221224560 3221223664 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9341 8900 603 41 0 9300 0
vsize: 37364
[startup+210.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 9325 0 0 0 20973 27 0 0 25 0 1 0 479695992 39878656 9303 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9736 9303 603 41 0 9695 0
vsize: 38944
[startup+220.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 9752 0 0 0 21972 28 0 0 25 0 1 0 479695992 41627648 9730 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10163 9730 603 41 0 10122 0
vsize: 40652
[startup+230.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10149 0 0 0 22971 30 0 0 25 0 1 0 479695992 43233280 10127 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10555 10127 603 41 0 10514 0
vsize: 42220
[startup+240.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10545 0 0 0 23970 31 0 0 25 0 1 0 479695992 45088768 10523 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11008 10523 603 41 0 10967 0
vsize: 44032
[startup+250.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10923 0 0 0 24968 33 0 0 25 0 1 0 479695992 46690304 10901 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11399 10901 603 41 0 11358 0
vsize: 45596
[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 25968 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 26968 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 27969 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 28969 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 29969 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 30969 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 31970 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+330.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26721
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 32970 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+340.021 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 26774
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 33970 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+350.021 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 26774
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 34970 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223744 134559559 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+360.022 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 26774
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 35970 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+370.022 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 26774
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 36970 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+380.023 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 26774
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 37971 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+390.024 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 26774
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 38971 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+400.024 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 26774
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 39971 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+410.025 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 40971 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560931 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+420.025 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 41971 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+430.026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 42972 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+440.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 43972 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+450.027 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 44972 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+460.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 45972 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223560 1075351128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+470.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 46972 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+480.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 47973 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+490.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 48973 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+500.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10993 0 0 0 49973 33 0 0 25 0 1 0 479695992 46952448 10971 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10971 603 41 0 11422 0
vsize: 45852
[startup+510.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10994 0 0 0 50973 33 0 0 25 0 1 0 479695992 46952448 10972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10972 603 41 0 11422 0
vsize: 45852
[startup+520.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10994 0 0 0 51973 33 0 0 25 0 1 0 479695992 46952448 10972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10972 603 41 0 11422 0
vsize: 45852
[startup+530.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10994 0 0 0 52974 33 0 0 25 0 1 0 479695992 46952448 10972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10972 603 41 0 11422 0
vsize: 45852
[startup+540.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10994 0 0 0 53974 33 0 0 25 0 1 0 479695992 46952448 10972 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10972 603 41 0 11422 0
vsize: 45852
[startup+550.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10994 0 0 0 54974 33 0 0 25 0 1 0 479695992 46952448 10972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10972 603 41 0 11422 0
vsize: 45852
[startup+560.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10994 0 0 0 55974 33 0 0 25 0 1 0 479695992 46952448 10972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10972 603 41 0 11422 0
vsize: 45852
[startup+570.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10994 0 0 0 56974 33 0 0 25 0 1 0 479695992 46952448 10972 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10972 603 41 0 11422 0
vsize: 45852
[startup+580.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10994 0 0 0 57974 33 0 0 25 0 1 0 479695992 46952448 10972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10972 603 41 0 11422 0
vsize: 45852
[startup+590.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10994 0 0 0 58975 33 0 0 25 0 1 0 479695992 46952448 10972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10972 603 41 0 11422 0
vsize: 45852
[startup+600.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10994 0 0 0 59975 33 0 0 25 0 1 0 479695992 46952448 10972 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10972 603 41 0 11422 0
vsize: 45852
[startup+610.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10996 0 0 0 60975 33 0 0 25 0 1 0 479695992 46952448 10974 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10974 603 41 0 11422 0
vsize: 45852
[startup+620.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 10998 0 0 0 61975 33 0 0 25 0 1 0 479695992 46952448 10976 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10976 603 41 0 11422 0
vsize: 45852
[startup+630.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26776
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11000 0 0 0 62975 33 0 0 25 0 1 0 479695992 46952448 10978 4294967295 134512640 134672761 3221224560 3221223696 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10978 603 41 0 11422 0
vsize: 45852
[startup+640.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 63976 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+650.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 64976 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+660.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 65976 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+670.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 66976 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+680.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 67976 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+690.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 68977 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+700.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 69977 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+710.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 70977 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+720.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 71977 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+730.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 72977 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+740.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 73978 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+750.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 74978 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+760.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 75978 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+770.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 76978 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+780.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11001 0 0 0 77978 33 0 0 25 0 1 0 479695992 46952448 10979 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10979 603 41 0 11422 0
vsize: 45852
[startup+790.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11003 0 0 0 78978 33 0 0 25 0 1 0 479695992 46952448 10981 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11463 10981 603 41 0 11422 0
vsize: 45852
[startup+800.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11003 0 0 0 79978 33 0 0 25 0 1 0 479695992 46952448 10981 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10981 603 41 0 11422 0
vsize: 45852
[startup+810.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11003 0 0 0 80978 33 0 0 25 0 1 0 479695992 46952448 10981 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10981 603 41 0 11422 0
vsize: 45852
[startup+820.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11004 0 0 0 81978 33 0 0 25 0 1 0 479695992 46952448 10982 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10982 603 41 0 11422 0
vsize: 45852
[startup+830.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11210 0 0 0 82978 34 0 0 25 0 1 0 479695992 47755264 11188 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11659 11188 603 41 0 11618 0
vsize: 46636
[startup+840.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11493 0 0 0 83978 34 0 0 25 0 1 0 479695992 48955392 11471 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11952 11471 603 41 0 11911 0
vsize: 47808
[startup+850.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 84977 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+860.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 85977 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+870.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 86978 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223664 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+880.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 87978 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+890.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 88978 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+900.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 89978 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+910.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 90978 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+920.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 91979 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+930.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 92979 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+940.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 93979 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+950.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 94979 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+960.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 95979 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+970.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 96979 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223712 134565119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+980.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 97980 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+990.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 98980 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 99980 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 100980 35 0 0 25 0 1 0 479695992 49750016 11655 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12146 11655 603 41 0 12105 0
vsize: 48584
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 101980 35 0 0 25 0 1 0 479695992 49729536 11655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11655 603 41 0 12100 0
vsize: 48564
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 102981 35 0 0 25 0 1 0 479695992 49729536 11655 4294967295 134512640 134672761 3221224560 3221223664 134560125 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11655 603 41 0 12100 0
vsize: 48564
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 103981 35 0 0 25 0 1 0 479695992 49729536 11655 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11655 603 41 0 12100 0
vsize: 48564
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 104981 35 0 0 25 0 1 0 479695992 49729536 11655 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12141 11655 603 41 0 12100 0
vsize: 48564
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 105980 35 0 0 25 0 1 0 479695992 49729536 11655 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12141 11655 603 41 0 12100 0
vsize: 48564
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 106979 36 0 0 25 0 1 0 479695992 49729536 11655 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12141 11655 603 41 0 12100 0
vsize: 48564
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 107978 36 0 0 25 0 1 0 479695992 49729536 11655 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11655 603 41 0 12100 0
vsize: 48564
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 108979 36 0 0 25 0 1 0 479695992 49729536 11655 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11655 603 41 0 12100 0
vsize: 48564
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 109979 36 0 0 25 0 1 0 479695992 49729536 11655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11655 603 41 0 12100 0
vsize: 48564
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11677 0 0 0 110979 36 0 0 25 0 1 0 479695992 49729536 11655 4294967295 134512640 134672761 3221224560 3221223744 134559019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11655 603 41 0 12100 0
vsize: 48564
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11678 0 0 0 111979 36 0 0 25 0 1 0 479695992 49729536 11656 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11656 603 41 0 12100 0
vsize: 48564
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11678 0 0 0 112980 36 0 0 25 0 1 0 479695992 49729536 11656 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11656 603 41 0 12100 0
vsize: 48564
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11678 0 0 0 113980 36 0 0 25 0 1 0 479695992 49729536 11656 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11656 603 41 0 12100 0
vsize: 48564
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11678 0 0 0 114980 36 0 0 25 0 1 0 479695992 49729536 11656 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11656 603 41 0 12100 0
vsize: 48564
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11678 0 0 0 115980 36 0 0 25 0 1 0 479695992 49729536 11656 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11656 603 41 0 12100 0
vsize: 48564
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11678 0 0 0 116980 36 0 0 25 0 1 0 479695992 49729536 11656 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11656 603 41 0 12100 0
vsize: 48564
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11678 0 0 0 117980 36 0 0 25 0 1 0 479695992 49729536 11656 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11656 603 41 0 12100 0
vsize: 48564
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11678 0 0 0 118981 36 0 0 25 0 1 0 479695992 49729536 11656 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11656 603 41 0 12100 0
vsize: 48564
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26778
Raw data (stat): 26721 (minisat+) R 26720 23176 23175 0 -1 0 11678 0 0 0 119981 36 0 0 25 0 1 0 479695992 49729536 11656 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12141 11656 603 41 0 12100 0
vsize: 48564
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 26778
Raw data (stat): 26721 (minisat+) Z 26720 23176 23175 0 -1 12 11681 0 0 0 119981 38 0 0 25 0 1 0 479695992 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.09
CPU time (s): 1200.2
CPU user time (s): 1199.81
CPU system time (s): 0.385941
CPU usage (%): 100.009
Max. virtual memory (Kb): 48584
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####