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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Nameweb/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb40-19-opb/normalized-frb40-19-3.opb
MD5SUM3acd642471b3f4559739eef7eb2e9b58
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -33
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 numbers10
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.03
Number of variables760
Total number of constraints41095
Number of constraints which are clauses41095
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint2

Trace number 2293

Launcher Data

LAUNCH ON wulflinc25 THE 2005-09-18 18:45:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2699 boxname=wulflinc25 idbench=355 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3acd642471b3f4559739eef7eb2e9b58  /oldhome/oroussel/tmp/wulflinc25/normalized-frb40-19-3.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-frb40-19-3.opb
IDLAUNCH: 2699
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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:        915476 kB
Buffers:         35352 kB
Cached:          56708 kB
SwapCached:        896 kB
Active:          66872 kB
Inactive:        27824 kB
HighTotal:      131008 kB
HighFree:        72912 kB
LowTotal:       903652 kB
LowFree:        842564 kB
SwapTotal:     2097892 kB
SwapFree:      2096496 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5716 kB
Slab:            18892 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:05:31 (client local time) WITH STATUS 10 IN 1209.45 SECONDS
stats: 2699 7 1209.45 10

Solver Data

c Parsing PB file...
c Converting 41095 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 |   41095    82190 |   13698       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -31
c ---[   0]---> Sorter-cost:35010     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   77395   167462 |   25798       0        0     nan |  0.000 % |
c |       101 |   77238   167143 |   28377      90      929    10.3 |  0.331 % |
c |       251 |   76847   166316 |   31215     211     2466    11.7 |  1.208 % |
c |       476 |   75972   164442 |   34337     395     4215    10.7 |  3.304 % |
c |       813 |   74494   161218 |   37770     658     7446    11.3 |  6.726 % |
c |      1319 |   71556   154677 |   41547    1013    11473    11.3 | 13.931 % |
c |      2078 |   68045   146771 |   45702    1564    17859    11.4 | 22.774 % |
c |      3217 |   62670   134504 |   50273    2321    28070    12.1 | 36.635 % |
c |      4925 |   56128   119095 |   55300    3417    45635    13.4 | 53.971 % |
c |      7487 |   51841   108909 |   60830    5071    80265    15.8 | 65.575 % |
c ==============================================================================
c Found solution: -32
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8864 |   50474   105612 |   16824    6059   132156    21.8 | 65.575 % |
c |      8964 |   50044   104589 |   18506    6068   132299    21.8 | 70.483 % |
c |      9114 |   49720   103800 |   20357    6093   133270    21.9 | 71.397 % |
c |      9339 |   49622   103571 |   22392    6281   138021    22.0 | 71.655 % |
c |      9677 |   49534   103357 |   24632    6586   144121    21.9 | 71.908 % |
c |     10183 |   49289   102776 |   27095    7005   153375    21.9 | 72.576 % |
c |     10942 |   48817   101638 |   29804    7437   174082    23.4 | 73.908 % |
c |     12081 |   48123    99987 |   32785    8315   226746    27.3 | 75.808 % |
c |     13789 |   47814    99243 |   36063    9822   297504    30.3 | 76.774 % |
c ==============================================================================
c Found solution: -33
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15122 |   47804    99246 |   15934   11128   367947    33.1 | 76.774 % |
c |     15222 |   47639    98853 |   17527   11109   366482    33.0 | 77.190 % |
c |     15372 |   47595    98751 |   19280   11227   369541    32.9 | 77.307 % |
c |     15597 |   47595    98751 |   21208   11452   386987    33.8 | 77.307 % |
c |     15936 |   47595    98751 |   23328   11791   400789    34.0 | 77.307 % |
c |     16442 |   47499    98515 |   25661   12216   419172    34.3 | 77.584 % |
c |     17201 |   47006    97343 |   28228   12699   460842    36.3 | 78.935 % |
c |     18340 |   46999    97326 |   31050   13820   534818    38.7 | 78.955 % |
c |     20048 |   46939    97192 |   34155   15464   658464    42.6 | 79.104 % |
c ==============================================================================
c Found solution: -34
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20986 |   46927    97141 |   15642   16249   721785    44.4 | 79.104 % |
c |     21086 |   46732    96676 |   17206   16212   722537    44.6 | 79.688 % |
c |     21236 |   46721    96649 |   18926   16356   727214    44.5 | 79.720 % |
c |     21463 |   46721    96649 |   20819   16583   740187    44.6 | 79.720 % |
c |     21800 |   46721    96649 |   22901   16920   757005    44.7 | 79.720 % |
c |     22306 |   46721    96649 |   25191   17426   776599    44.6 | 79.720 % |
c |     23065 |   46718    96642 |   27710   18177   823057    45.3 | 79.728 % |
c |     24204 |   46648    96470 |   30481   19252   920173    47.8 | 79.929 % |
c |     25912 |   46551    96239 |   33530   20864  1063720    51.0 | 80.183 % |
c |     28474 |   46411    95903 |   36883   23262  1288226    55.4 | 80.568 % |
c |     32318 |   46361    95779 |   40571   27052  1576672    58.3 | 80.713 % |
c |     38085 |   46232    95472 |   44628   32638  2119521    64.9 | 81.067 % |
c |     46736 |   46197    95387 |   49091   41194  3124221    75.8 | 81.163 % |
c |     59710 |   45887    94639 |   54000   53780  4274679    79.5 | 82.040 % |
c ==============================================================================
c Found solution: -35
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68731 |   45876    94626 |   15292   62730  5053895    80.6 | 82.040 % |
c |     68831 |   45876    94626 |   16821   18447  1108901    60.1 | 82.148 % |
c |     68981 |   45852    94564 |   18503   18590  1112238    59.8 | 82.220 % |
c |     69207 |   45846    94550 |   20353   18795  1124590    59.8 | 82.236 % |
c |     69544 |   45846    94550 |   22389   19132  1156718    60.5 | 82.236 % |
c |     70050 |   45846    94550 |   24627   19638  1198376    61.0 | 82.236 % |
c |     70809 |   45846    94550 |   27090   20397  1276601    62.6 | 82.236 % |
c |     71948 |   45846    94550 |   29799   21536  1352008    62.8 | 82.236 % |
c |     73656 |   45846    94550 |   32779   23244  1501208    64.6 | 82.236 % |
c |     76218 |   45772    94364 |   36057   25794  1717538    66.6 | 82.460 % |
c ==============================================================================
c Found solution: -36
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79852 |   45763    94329 |   15254   29426  2135545    72.6 | 82.460 % |
c |     79952 |   45763    94329 |   16779   29526  2141968    72.5 | 82.494 % |
c |     80102 |   45763    94329 |   18457   29676  2155080    72.6 | 82.494 % |
c |     80327 |   45763    94329 |   20303   29901  2168898    72.5 | 82.494 % |
c |     80665 |   45763    94329 |   22333   30239  2188372    72.4 | 82.494 % |
c |     81171 |   45763    94329 |   24566   30745  2229210    72.5 | 82.494 % |
c |     81930 |   45763    94329 |   27023   31504  2289974    72.7 | 82.494 % |
c |     83069 |   45763    94329 |   29725   32643  2381067    72.9 | 82.494 % |
c |     84777 |   45763    94329 |   32698   34351  2511357    73.1 | 82.494 % |
c |     87340 |   45753    94303 |   35968   36906  2770585    75.1 | 82.526 % |
c |     91184 |   45690    94150 |   39564   40741  3063992    75.2 | 82.706 % |
c |     96950 |   45658    94074 |   43521   46425  3529731    76.0 | 82.794 % |
c |    105600 |   45646    94046 |   47873   55068  4237732    77.0 | 82.826 % |
c |    118574 |   45646    94046 |   52660   68042  5330410    78.3 | 82.826 % |
c |    138036 |   45576    93882 |   57927   34000  2343565    68.9 | 83.014 % |
c ==============================================================================
c Found solution: -37
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    149466 |   45599    93945 |   15199   45430  3332463    73.4 | 83.014 % |
c |    149566 |   45599    93945 |   16718   17803  1045062    58.7 | 82.973 % |
c |    149718 |   45599    93945 |   18390   17955  1053066    58.7 | 82.973 % |
c |    149943 |   45599    93945 |   20229   18180  1067373    58.7 | 82.973 % |
c |    150281 |   45596    93938 |   22252   18516  1082787    58.5 | 82.981 % |
c |    150787 |   45593    93931 |   24478   19013  1111621    58.5 | 82.989 % |
c |    151546 |   45593    93931 |   26925   19772  1179618    59.7 | 82.989 % |
c |    152686 |   45593    93931 |   29618   20912  1287628    61.6 | 82.989 % |
c |    154394 |   45593    93931 |   32580   22620  1436347    63.5 | 82.989 % |
c |    156956 |   45580    93900 |   35838   25160  1626071    64.6 | 83.025 % |
c |    160800 |   45469    93635 |   39422   28964  1960525    67.7 | 83.337 % |
c |    166566 |   45422    93516 |   43364   34720  2450264    70.6 | 83.481 % |
c |    175216 |   45422    93516 |   47700   43370  3106157    71.6 | 83.481 % |
c |    188190 |   45409    93485 |   52471   56340  4190159    74.4 | 83.517 % |
c |    207651 |   45378    93412 |   57718   20752   843783    40.7 | 83.597 % |
c |    236844 |   45348    93342 |   63489   49941  3556546    71.2 | 83.677 % |
c |    280635 |   45332    93300 |   69838   29311  1271672    43.4 | 83.729 % |
c ==============================================================================
c Found solution: -38
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    344995 |   45289    93179 |   15096   22206   620998    28.0 | 83.729 % |
c |    345095 |   45289    93179 |   16605   22306   624408    28.0 | 83.859 % |
c |    345245 |   45289    93179 |   18266   22456   629871    28.0 | 83.859 % |
c |    345471 |   45289    93179 |   20092   22682   637923    28.1 | 83.859 % |
c |    345808 |   45289    93179 |   22102   23019   650581    28.3 | 83.859 % |
c |    346315 |   45289    93179 |   24312   23526   669167    28.4 | 83.859 % |
c |    347074 |   45221    93013 |   26743   24280   705523    29.1 | 84.055 % |
c |    348213 |   45212    92988 |   29417   25414   778295    30.6 | 84.087 % |
c |    349921 |   45141    92818 |   32359   27103   880732    32.5 | 84.283 % |
c |    352483 |   45141    92818 |   35595   29665  1032114    34.8 | 84.283 % |
c |    356327 |   45141    92818 |   39155   33509  1294905    38.6 | 84.283 % |
c |    362093 |   45141    92818 |   43070   39275  1678091    42.7 | 84.283 % |
c |    370742 |   45141    92818 |   47377   47924  2281068    47.6 | 84.283 % |
c |    383716 |   45141    92818 |   52115   60898  2875601    47.2 | 84.283 % |
c |    403178 |   45131    92794 |   57327   26764   757803    28.3 | 84.311 % |
c |    432371 |   45125    92780 |   63059   55955  2218138    39.6 | 84.327 % |
c |    476160 |   45116    92759 |   69365   36944  1091586    29.5 | 84.351 % |
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 -C75

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/14240/stat): 14240 (minisat+_script) R 14239 14240 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843544943 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/14240/statm): 174 3 169 147 0 27 0
[pid=14240] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=14241
New process pid=14242
New process pid=14243
execve syscall for /bin/sed executable
One traced child (pid=14242) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=14243) exited with status: 0
One traced child (pid=14241) exited with status: 0
New process pid=14244
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-frb40-19-3.opb

[startup+10.0033 s]
Raw data (loadavg): 0.93 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 2783 0 0 0 976 11 0 0 25 0 1 0 1843544948 12197888 2770 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14244/statm): 2978 2770 145 145 0 2833 0
[pid=14244] vsize: 11912
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 14036

[startup+20.0049 s]
Raw data (loadavg): 0.94 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 2802 0 0 0 1975 11 0 0 25 0 1 0 1843544948 12275712 2789 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14244/statm): 2997 2789 145 145 0 2852 0
[pid=14244] vsize: 11988
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 14112

[startup+30.0055 s]
Raw data (loadavg): 0.95 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 2846 0 0 0 2974 11 0 0 25 0 1 0 1843544948 12464128 2833 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14244/statm): 3043 2833 145 145 0 2898 0
[pid=14244] vsize: 12172
Current children cumulated CPU time (s) 29.85
Current children cumulated vsize (Kb) 14296

[startup+40.0061 s]
Raw data (loadavg): 0.96 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 3234 0 0 0 3966 15 0 0 25 0 1 0 1843544948 14295040 3221 4294967295 134512640 135094434 3221224448 3221223236 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14244/statm): 3490 3221 145 145 0 3345 0
[pid=14244] vsize: 13960
Current children cumulated CPU time (s) 39.81
Current children cumulated vsize (Kb) 16084

[startup+50.0067 s]
Raw data (loadavg): 0.96 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 3695 0 0 0 4957 21 0 0 25 0 1 0 1843544948 16224256 3682 4294967295 134512640 135094434 3221224448 3221223072 134557691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 3961 3682 145 145 0 3816 0
[pid=14244] vsize: 15844
Current children cumulated CPU time (s) 49.78
Current children cumulated vsize (Kb) 17968

[startup+60.0073 s]
Raw data (loadavg): 0.97 0.97 0.98 3/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 4267 0 0 0 5948 24 0 0 25 0 1 0 1843544948 18542592 4254 4294967295 134512640 135094434 3221224448 3221223184 134559634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14244/statm): 4527 4254 145 145 0 4382 0
[pid=14244] vsize: 18108
Current children cumulated CPU time (s) 59.72
Current children cumulated vsize (Kb) 20232

[startup+70.0089 s]
Raw data (loadavg): 0.97 0.97 0.98 3/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 4774 0 0 0 6938 28 0 0 25 0 1 0 1843544948 20598784 4761 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14244/statm): 5029 4761 145 145 0 4884 0
[pid=14244] vsize: 20116
Current children cumulated CPU time (s) 69.66
Current children cumulated vsize (Kb) 22240

[startup+80.0095 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 5325 0 0 0 7927 33 0 0 25 0 1 0 1843544948 22970368 5312 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14244/statm): 5608 5312 145 145 0 5463 0
[pid=14244] vsize: 22432
Current children cumulated CPU time (s) 79.6
Current children cumulated vsize (Kb) 24556

[startup+90.0111 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 5879 0 0 0 8918 38 0 0 25 0 1 0 1843544948 25223168 5866 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 6158 5866 145 145 0 6013 0
[pid=14244] vsize: 24632
Current children cumulated CPU time (s) 89.56
Current children cumulated vsize (Kb) 26756

[startup+100.012 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 6363 0 0 0 9908 42 0 0 25 0 1 0 1843544948 27189248 6350 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 6638 6350 145 145 0 6493 0
[pid=14244] vsize: 26552
Current children cumulated CPU time (s) 99.5
Current children cumulated vsize (Kb) 28676

[startup+110.012 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 6812 0 0 0 10901 46 0 0 25 0 1 0 1843544948 29011968 6799 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 7083 6799 145 145 0 6938 0
[pid=14244] vsize: 28332
Current children cumulated CPU time (s) 109.47
Current children cumulated vsize (Kb) 30456

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 7124 0 0 0 11895 49 0 0 25 0 1 0 1843544948 30277632 7111 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 7392 7111 145 145 0 7247 0
[pid=14244] vsize: 29568
Current children cumulated CPU time (s) 119.44
Current children cumulated vsize (Kb) 31692

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 7515 0 0 0 12888 52 0 0 25 0 1 0 1843544948 31862784 7502 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 7779 7502 145 145 0 7634 0
[pid=14244] vsize: 31116
Current children cumulated CPU time (s) 129.4
Current children cumulated vsize (Kb) 33240

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 7866 0 0 0 13881 55 0 0 25 0 1 0 1843544948 33288192 7853 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 8127 7853 145 145 0 7982 0
[pid=14244] vsize: 32508
Current children cumulated CPU time (s) 139.36
Current children cumulated vsize (Kb) 34632

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 8205 0 0 0 14875 57 0 0 25 0 1 0 1843544948 34660352 8192 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 8462 8192 145 145 0 8317 0
[pid=14244] vsize: 33848
Current children cumulated CPU time (s) 149.32
Current children cumulated vsize (Kb) 35972

[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 8394 0 0 0 15872 58 0 0 25 0 1 0 1843544948 35426304 8381 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 8649 8381 145 145 0 8504 0
[pid=14244] vsize: 34596
Current children cumulated CPU time (s) 159.3
Current children cumulated vsize (Kb) 36720

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 8394 0 0 0 16872 59 0 0 25 0 1 0 1843544948 35426304 8381 4294967295 134512640 135094434 3221224448 3221223120 134556254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 8649 8381 145 145 0 8504 0
[pid=14244] vsize: 34596
Current children cumulated CPU time (s) 169.31
Current children cumulated vsize (Kb) 36720

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 8394 0 0 0 17872 59 0 0 25 0 1 0 1843544948 35426304 8381 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 8649 8381 145 145 0 8504 0
[pid=14244] vsize: 34596
Current children cumulated CPU time (s) 179.31
Current children cumulated vsize (Kb) 36720

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 8394 0 0 0 18872 59 0 0 25 0 1 0 1843544948 35426304 8381 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 8649 8381 145 145 0 8504 0
[pid=14244] vsize: 34596
Current children cumulated CPU time (s) 189.31
Current children cumulated vsize (Kb) 36720

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 8394 0 0 0 19873 59 0 0 25 0 1 0 1843544948 35426304 8381 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 8649 8381 145 145 0 8504 0
[pid=14244] vsize: 34596
Current children cumulated CPU time (s) 199.32
Current children cumulated vsize (Kb) 36720

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 8394 0 0 0 20873 59 0 0 25 0 1 0 1843544948 35426304 8381 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 8649 8381 145 145 0 8504 0
[pid=14244] vsize: 34596
Current children cumulated CPU time (s) 209.32
Current children cumulated vsize (Kb) 36720

[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 8394 0 0 0 21873 59 0 0 25 0 1 0 1843544948 35426304 8381 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 8649 8381 145 145 0 8504 0
[pid=14244] vsize: 34596
Current children cumulated CPU time (s) 219.32
Current children cumulated vsize (Kb) 36720

[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 8394 0 0 0 22873 59 0 0 25 0 1 0 1843544948 35426304 8381 4294967295 134512640 135094434 3221224448 3221223040 134557152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 8649 8381 145 145 0 8504 0
[pid=14244] vsize: 34596
Current children cumulated CPU time (s) 229.32
Current children cumulated vsize (Kb) 36720

[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 8394 0 0 0 23873 59 0 0 25 0 1 0 1843544948 35426304 8381 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 8649 8381 145 145 0 8504 0
[pid=14244] vsize: 34596
Current children cumulated CPU time (s) 239.32
Current children cumulated vsize (Kb) 36720

[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 8408 0 0 0 24873 59 0 0 25 0 1 0 1843544948 35479552 8395 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 8662 8395 145 145 0 8517 0
[pid=14244] vsize: 34648
Current children cumulated CPU time (s) 249.32
Current children cumulated vsize (Kb) 36772

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 8740 0 0 0 25868 62 0 0 25 0 1 0 1843544948 37089280 8727 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14244/statm): 9055 8727 145 145 0 8910 0
[pid=14244] vsize: 36220
Current children cumulated CPU time (s) 259.3
Current children cumulated vsize (Kb) 38344

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9058 0 0 0 26862 64 0 0 25 0 1 0 1843544948 38383616 9045 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9371 9045 145 145 0 9226 0
[pid=14244] vsize: 37484
Current children cumulated CPU time (s) 269.26
Current children cumulated vsize (Kb) 39608

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 27858 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 279.25
Current children cumulated vsize (Kb) 40604

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 28858 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 289.25
Current children cumulated vsize (Kb) 40604

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 29858 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 299.25
Current children cumulated vsize (Kb) 40604

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 30858 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223136 134554736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 309.25
Current children cumulated vsize (Kb) 40604

[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 31859 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 319.26
Current children cumulated vsize (Kb) 40604

[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 32859 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 329.26
Current children cumulated vsize (Kb) 40604

[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 33859 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 339.26
Current children cumulated vsize (Kb) 40604

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 34859 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 349.26
Current children cumulated vsize (Kb) 40604

[startup+360.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 35859 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223040 134557401 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 359.26
Current children cumulated vsize (Kb) 40604

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 36860 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 369.27
Current children cumulated vsize (Kb) 40604

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 37860 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 379.27
Current children cumulated vsize (Kb) 40604

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.98 3/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 38860 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 389.27
Current children cumulated vsize (Kb) 40604

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 39860 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 399.27
Current children cumulated vsize (Kb) 40604

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 40860 67 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 409.27
Current children cumulated vsize (Kb) 40604

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 41860 68 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 419.28
Current children cumulated vsize (Kb) 40604

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 42860 68 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 429.28
Current children cumulated vsize (Kb) 40604

[startup+440.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 43860 68 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223040 134557372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 439.28
Current children cumulated vsize (Kb) 40604

[startup+450.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9310 0 0 0 44860 68 0 0 25 0 1 0 1843544948 39403520 9297 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9297 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 449.28
Current children cumulated vsize (Kb) 40604

[startup+460.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 45861 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 459.29
Current children cumulated vsize (Kb) 40604

[startup+470.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 46861 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 469.29
Current children cumulated vsize (Kb) 40604

[startup+480.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 47861 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 479.29
Current children cumulated vsize (Kb) 40604

[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 48861 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223040 134557131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 489.29
Current children cumulated vsize (Kb) 40604

[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 49861 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 499.29
Current children cumulated vsize (Kb) 40604

[startup+510.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 50861 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223040 134556834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 509.29
Current children cumulated vsize (Kb) 40604

[startup+520.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 51862 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 519.3
Current children cumulated vsize (Kb) 40604

[startup+530.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 52862 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 529.3
Current children cumulated vsize (Kb) 40604

[startup+540.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 53862 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 539.3
Current children cumulated vsize (Kb) 40604

[startup+550.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 54862 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223040 134557213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 549.3
Current children cumulated vsize (Kb) 40604

[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 55863 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 559.31
Current children cumulated vsize (Kb) 40604

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 56863 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 569.31
Current children cumulated vsize (Kb) 40604

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9312 0 0 0 57863 68 0 0 25 0 1 0 1843544948 39403520 9299 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9299 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 579.31
Current children cumulated vsize (Kb) 40604

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9313 0 0 0 58863 68 0 0 25 0 1 0 1843544948 39403520 9300 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9300 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 589.31
Current children cumulated vsize (Kb) 40604

[startup+600.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9315 0 0 0 59863 68 0 0 25 0 1 0 1843544948 39403520 9302 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9302 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 599.31
Current children cumulated vsize (Kb) 40604

[startup+610.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9318 0 0 0 60863 69 0 0 25 0 1 0 1843544948 39403520 9305 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9620 9305 145 145 0 9475 0
[pid=14244] vsize: 38480
Current children cumulated CPU time (s) 609.32
Current children cumulated vsize (Kb) 40604

[startup+620.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9478 0 0 0 61861 70 0 0 25 0 1 0 1843544948 40054784 9465 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9779 9465 145 145 0 9634 0
[pid=14244] vsize: 39116
Current children cumulated CPU time (s) 619.31
Current children cumulated vsize (Kb) 41240

[startup+630.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9571 0 0 0 62859 70 0 0 25 0 1 0 1843544948 40435712 9558 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9872 9558 145 145 0 9727 0
[pid=14244] vsize: 39488
Current children cumulated CPU time (s) 629.29
Current children cumulated vsize (Kb) 41612

[startup+640.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9571 0 0 0 63859 70 0 0 25 0 1 0 1843544948 40435712 9558 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14244/statm): 9872 9558 145 145 0 9727 0
[pid=14244] vsize: 39488
Current children cumulated CPU time (s) 639.29
Current children cumulated vsize (Kb) 41612

[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9571 0 0 0 64859 70 0 0 25 0 1 0 1843544948 40435712 9558 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9872 9558 145 145 0 9727 0
[pid=14244] vsize: 39488
Current children cumulated CPU time (s) 649.29
Current children cumulated vsize (Kb) 41612

[startup+660.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9571 0 0 0 65859 70 0 0 25 0 1 0 1843544948 40435712 9558 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9872 9558 145 145 0 9727 0
[pid=14244] vsize: 39488
Current children cumulated CPU time (s) 659.29
Current children cumulated vsize (Kb) 41612

[startup+670.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9571 0 0 0 66859 70 0 0 25 0 1 0 1843544948 40435712 9558 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9872 9558 145 145 0 9727 0
[pid=14244] vsize: 39488
Current children cumulated CPU time (s) 669.29
Current children cumulated vsize (Kb) 41612

[startup+680.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9571 0 0 0 67859 70 0 0 25 0 1 0 1843544948 40435712 9558 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9872 9558 145 145 0 9727 0
[pid=14244] vsize: 39488
Current children cumulated CPU time (s) 679.29
Current children cumulated vsize (Kb) 41612

[startup+690.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9576 0 0 0 68859 71 0 0 25 0 1 0 1843544948 40468480 9563 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9880 9563 145 145 0 9735 0
[pid=14244] vsize: 39520
Current children cumulated CPU time (s) 689.3
Current children cumulated vsize (Kb) 41644

[startup+700.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9576 0 0 0 69860 71 0 0 25 0 1 0 1843544948 40468480 9563 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9880 9563 145 145 0 9735 0
[pid=14244] vsize: 39520
Current children cumulated CPU time (s) 699.31
Current children cumulated vsize (Kb) 41644

[startup+710.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9576 0 0 0 70860 71 0 0 25 0 1 0 1843544948 40468480 9563 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9880 9563 145 145 0 9735 0
[pid=14244] vsize: 39520
Current children cumulated CPU time (s) 709.31
Current children cumulated vsize (Kb) 41644

[startup+720.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9576 0 0 0 71860 71 0 0 25 0 1 0 1843544948 40468480 9563 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9880 9563 145 145 0 9735 0
[pid=14244] vsize: 39520
Current children cumulated CPU time (s) 719.31
Current children cumulated vsize (Kb) 41644

[startup+730.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9576 0 0 0 72860 71 0 0 25 0 1 0 1843544948 40468480 9563 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9880 9563 145 145 0 9735 0
[pid=14244] vsize: 39520
Current children cumulated CPU time (s) 729.31
Current children cumulated vsize (Kb) 41644

[startup+740.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9576 0 0 0 73860 71 0 0 25 0 1 0 1843544948 40468480 9563 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9880 9563 145 145 0 9735 0
[pid=14244] vsize: 39520
Current children cumulated CPU time (s) 739.31
Current children cumulated vsize (Kb) 41644

[startup+750.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9576 0 0 0 74861 71 0 0 25 0 1 0 1843544948 40468480 9563 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9880 9563 145 145 0 9735 0
[pid=14244] vsize: 39520
Current children cumulated CPU time (s) 749.32
Current children cumulated vsize (Kb) 41644

[startup+760.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9576 0 0 0 75861 71 0 0 25 0 1 0 1843544948 40468480 9563 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9880 9563 145 145 0 9735 0
[pid=14244] vsize: 39520
Current children cumulated CPU time (s) 759.32
Current children cumulated vsize (Kb) 41644

[startup+770.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9576 0 0 0 76861 71 0 0 25 0 1 0 1843544948 40468480 9563 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9880 9563 145 145 0 9735 0
[pid=14244] vsize: 39520
Current children cumulated CPU time (s) 769.32
Current children cumulated vsize (Kb) 41644

[startup+780.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9579 0 0 0 77861 71 0 0 25 0 1 0 1843544948 40468480 9566 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9880 9566 145 145 0 9735 0
[pid=14244] vsize: 39520
Current children cumulated CPU time (s) 779.32
Current children cumulated vsize (Kb) 41644

[startup+790.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9587 0 0 0 78862 71 0 0 25 0 1 0 1843544948 40501248 9574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9888 9574 145 145 0 9743 0
[pid=14244] vsize: 39552
Current children cumulated CPU time (s) 789.33
Current children cumulated vsize (Kb) 41676

[startup+800.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9603 0 0 0 79862 71 0 0 25 0 1 0 1843544948 40574976 9590 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9590 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 799.33
Current children cumulated vsize (Kb) 41748

[startup+810.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9603 0 0 0 80862 71 0 0 25 0 1 0 1843544948 40574976 9590 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9590 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 809.33
Current children cumulated vsize (Kb) 41748

[startup+820.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9603 0 0 0 81862 71 0 0 25 0 1 0 1843544948 40574976 9590 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9590 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 819.33
Current children cumulated vsize (Kb) 41748

[startup+830.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9603 0 0 0 82862 71 0 0 25 0 1 0 1843544948 40574976 9590 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9590 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 829.33
Current children cumulated vsize (Kb) 41748

[startup+840.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9603 0 0 0 83862 71 0 0 25 0 1 0 1843544948 40574976 9590 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9590 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 839.33
Current children cumulated vsize (Kb) 41748

[startup+850.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9603 0 0 0 84862 71 0 0 25 0 1 0 1843544948 40574976 9590 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9590 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 849.33
Current children cumulated vsize (Kb) 41748

[startup+860.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9603 0 0 0 85863 71 0 0 25 0 1 0 1843544948 40574976 9590 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9590 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 859.34
Current children cumulated vsize (Kb) 41748

[startup+870.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 86863 71 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 869.34
Current children cumulated vsize (Kb) 41748

[startup+880.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 87863 71 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 879.34
Current children cumulated vsize (Kb) 41748

[startup+890.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 88863 71 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 889.34
Current children cumulated vsize (Kb) 41748

[startup+900.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 89863 71 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 899.34
Current children cumulated vsize (Kb) 41748

[startup+910.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 90863 71 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 909.34
Current children cumulated vsize (Kb) 41748

[startup+920.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 91864 71 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 919.35
Current children cumulated vsize (Kb) 41748

[startup+930.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 92864 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 929.36
Current children cumulated vsize (Kb) 41748

[startup+940.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 93864 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 939.36
Current children cumulated vsize (Kb) 41748

[startup+950.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 94864 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 949.36
Current children cumulated vsize (Kb) 41748

[startup+960.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 95864 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 959.36
Current children cumulated vsize (Kb) 41748

[startup+970.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 96865 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 969.37
Current children cumulated vsize (Kb) 41748

[startup+980.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 97865 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 979.37
Current children cumulated vsize (Kb) 41748

[startup+990.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 98865 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 989.37
Current children cumulated vsize (Kb) 41748

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 99865 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 999.37
Current children cumulated vsize (Kb) 41748

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 100865 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 1009.37
Current children cumulated vsize (Kb) 41748

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 101865 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 1019.37
Current children cumulated vsize (Kb) 41748

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 102866 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 1029.38
Current children cumulated vsize (Kb) 41748

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 103866 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 1039.38
Current children cumulated vsize (Kb) 41748

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9604 0 0 0 104866 72 0 0 25 0 1 0 1843544948 40574976 9591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9591 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 1049.38
Current children cumulated vsize (Kb) 41748

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9607 0 0 0 105866 72 0 0 25 0 1 0 1843544948 40574976 9594 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9594 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 1059.38
Current children cumulated vsize (Kb) 41748

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9607 0 0 0 106866 72 0 0 25 0 1 0 1843544948 40574976 9594 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9594 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 1069.38
Current children cumulated vsize (Kb) 41748

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9607 0 0 0 107867 72 0 0 25 0 1 0 1843544948 40574976 9594 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9594 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 1079.39
Current children cumulated vsize (Kb) 41748

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9607 0 0 0 108867 72 0 0 25 0 1 0 1843544948 40574976 9594 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9594 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 1089.39
Current children cumulated vsize (Kb) 41748

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9607 0 0 0 109867 72 0 0 25 0 1 0 1843544948 40574976 9594 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9906 9594 145 145 0 9761 0
[pid=14244] vsize: 39624
Current children cumulated CPU time (s) 1099.39
Current children cumulated vsize (Kb) 41748

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9610 0 0 0 110867 72 0 0 25 0 1 0 1843544948 40599552 9597 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9912 9597 145 145 0 9767 0
[pid=14244] vsize: 39648
Current children cumulated CPU time (s) 1109.39
Current children cumulated vsize (Kb) 41772

[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9622 0 0 0 111867 72 0 0 25 0 1 0 1843544948 40665088 9609 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9928 9609 145 145 0 9783 0
[pid=14244] vsize: 39712
Current children cumulated CPU time (s) 1119.39
Current children cumulated vsize (Kb) 41836

[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9622 0 0 0 112868 72 0 0 25 0 1 0 1843544948 40665088 9609 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9928 9609 145 145 0 9783 0
[pid=14244] vsize: 39712
Current children cumulated CPU time (s) 1129.4
Current children cumulated vsize (Kb) 41836

[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9623 0 0 0 113868 72 0 0 25 0 1 0 1843544948 40665088 9610 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9928 9610 145 145 0 9783 0
[pid=14244] vsize: 39712
Current children cumulated CPU time (s) 1139.4
Current children cumulated vsize (Kb) 41836

[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9623 0 0 0 114868 72 0 0 25 0 1 0 1843544948 40665088 9610 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9928 9610 145 145 0 9783 0
[pid=14244] vsize: 39712
Current children cumulated CPU time (s) 1149.4
Current children cumulated vsize (Kb) 41836

[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9624 0 0 0 115868 72 0 0 25 0 1 0 1843544948 40665088 9611 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9928 9611 145 145 0 9783 0
[pid=14244] vsize: 39712
Current children cumulated CPU time (s) 1159.4
Current children cumulated vsize (Kb) 41836

[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9625 0 0 0 116868 72 0 0 25 0 1 0 1843544948 40665088 9612 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9928 9612 145 145 0 9783 0
[pid=14244] vsize: 39712
Current children cumulated CPU time (s) 1169.4
Current children cumulated vsize (Kb) 41836

[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.98 3/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9625 0 0 0 117869 72 0 0 25 0 1 0 1843544948 40665088 9612 4294967295 134512640 135094434 3221224448 3221223104 134561460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9928 9612 145 145 0 9783 0
[pid=14244] vsize: 39712
Current children cumulated CPU time (s) 1179.41
Current children cumulated vsize (Kb) 41836

[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9625 0 0 0 118869 73 0 0 25 0 1 0 1843544948 40665088 9612 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9928 9612 145 145 0 9783 0
[pid=14244] vsize: 39712
Current children cumulated CPU time (s) 1189.42
Current children cumulated vsize (Kb) 41836

[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9625 0 0 0 119869 73 0 0 25 0 1 0 1843544948 40665088 9612 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9928 9612 145 145 0 9783 0
[pid=14244] vsize: 39712
Current children cumulated CPU time (s) 1199.42
Current children cumulated vsize (Kb) 41836

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9625 0 0 0 120869 73 0 0 25 0 1 0 1843544948 40665088 9612 4294967295 134512640 135094434 3221224448 3221223040 134556921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9928 9612 145 145 0 9783 0
[pid=14244] vsize: 39712
Current children cumulated CPU time (s) 1209.42
Current children cumulated vsize (Kb) 41836



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 14244
Raw data (/proc/14240/stat): 14240 (minisat+_script) S 14239 14240 4419 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843544943 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/14240/statm): 531 226 485 147 0 384 0
[pid=14240] vsize: 2124
Raw data (/proc/14244/stat): 14244 (minisat+_64-bit) R 14240 14240 4419 0 -1 0 9625 0 0 0 120869 73 0 0 25 0 1 0 1843544948 40665088 9612 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14244/statm): 9928 9612 145 145 0 9783 0
[pid=14244] vsize: 39712
Current children cumulated CPU time (s) 1209.42
Current children cumulated vsize (Kb) 41836

Sending SIGTERM to -14240
Sleeping 2 seconds
One traced child (pid=14240) ended because it received signal 15 (SIGTERM)
One traced child (pid=14244) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.1
CPU time (s): 1209.45
CPU user time (s): 1208.7
CPU system time (s): 0.752885
CPU usage (%): 99.9464
Max. virtual memory (cumulated for all children) (Kb): 41836

Verifier Data

ERROR: no interpretation found !