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

Namemps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-gr4x6.opb
MD5SUMd90fce7408f7990dccb3ba4f8fa1c8f6
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 24752128
Optimality of the best value was proved NO
Number of terms in the objective function 744
Biggest coefficient in the objective function 151934468096
Number of bits for the biggest coefficient in the objective function 38
Sum of the numbers in the objective function 3470370333536
Number of bits of the sum of numbers in the objective function 42
Biggest number in a constraint 151934468096
Number of bits of the biggest number in a constraint 38
Biggest sum of numbers in a constraint 3470370333536
Number of bits of the biggest sum of numbers42
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.05
Number of variables744
Total number of constraints34
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints34
Minimum length of a constraint31
Maximum length of a constraint180

Trace number 4558

Launcher Data

LAUNCH ON wulflinc30 THE 2005-09-19 18:23:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3021 boxname=wulflinc30 idbench=677 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d90fce7408f7990dccb3ba4f8fa1c8f6  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-gr4x6.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-gr4x6.opb
IDLAUNCH: 3021
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        903156 kB
Buffers:         32680 kB
Cached:          70256 kB
SwapCached:        764 kB
Active:          33452 kB
Inactive:        72092 kB
HighTotal:      131008 kB
HighFree:        60088 kB
LowTotal:       903652 kB
LowFree:        843068 kB
SwapTotal:     2097892 kB
SwapFree:      2096620 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5712 kB
Slab:            20480 kB
Committed_AS:    64304 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:43:20 (client local time) WITH STATUS 10 IN 1209.37 SECONDS
stats: 3021 7 1209.37 10

Solver Data

c Parsing PB file...
c Converting 44 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########
c   -- Clauses(.)/Splits(s): (none)
c ---[  42]---> Sorter-cost: 1236     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1236     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost: 1164     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost: 1152     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  591     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  519     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> BDD-cost:   22
c ---[  22]---> BDD-cost:   19
c ---[  21]---> BDD-cost:   16
c ---[  20]---> BDD-cost:   16
c ---[  19]---> BDD-cost:   18
c ---[  18]---> BDD-cost:   18
c ---[  17]---> BDD-cost:   18
c ---[  16]---> BDD-cost:   18
c ---[  15]---> BDD-cost:   16
c ---[  14]---> BDD-cost:   16
c ---[  13]---> BDD-cost:   18
c ---[  12]---> BDD-cost:   18
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   18
c ---[   9]---> BDD-cost:   18
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   18
c ---[   5]---> BDD-cost:   16
c ---[   4]---> BDD-cost:   16
c ---[   3]---> BDD-cost:   22
c ---[   2]---> BDD-cost:   19
c ---[   1]---> BDD-cost:   20
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   20089    47581 |    6696       0        0     nan |  0.000 % |
c |       100 |   20089    47581 |    7365     100      393     3.9 | 10.732 % |
c |       250 |   20039    47467 |    8102     246     1058     4.3 | 10.902 % |
c ==============================================================================
c Found solution: 48834098
c ---[   0]---> Sorter-cost:80542     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       370 |  245919   574838 |   81973     366     1616     4.4 | 10.902 % |
c |       472 |  245919   574838 |   90170     468     2875     6.1 |  0.987 % |
c |       622 |  245919   574838 |   99187     618     5853     9.5 |  0.987 % |
c |       849 |  245919   574838 |  109106     845    14016    16.6 |  0.987 % |
c |      1186 |  245907   574812 |  120016    1180    28174    23.9 |  0.992 % |
c |      1692 |  245756   574471 |  132018    1682    32367    19.2 |  1.040 % |
c |      2452 |  245756   574471 |  145220    2442    41855    17.1 |  1.040 % |
c |      3591 |  245756   574471 |  159742    3581    60900    17.0 |  1.040 % |
c |      5299 |  245756   574471 |  175716    5289    78968    14.9 |  1.040 % |
c ==============================================================================
c Found solution: 48658918
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6135 |  246491   576704 |   82163    6125    91885    15.0 |  1.040 % |
c |      6235 |  246491   576704 |   90379    6225    92395    14.8 |  1.036 % |
c |      6385 |  246491   576704 |   99417    6375    93090    14.6 |  1.036 % |
c |      6612 |  246491   576704 |  109358    6602    95928    14.5 |  1.036 % |
c |      6950 |  246433   576574 |  120294    6934    99591    14.4 |  1.054 % |
c ==============================================================================
c Found solution: 48585107
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6973 |  246457   576787 |   82152    6957    99867    14.4 |  1.054 % |
c |      7073 |  246457   576787 |   90367    7057   103129    14.6 |  1.055 % |
c ==============================================================================
c Found solution: 47745280
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7205 |  246689   577396 |   82229    7184   104557    14.6 |  1.055 % |
c |      7306 |  246689   577396 |   90451    7285   105083    14.4 |  1.089 % |
c ==============================================================================
c Found solution: 47085915
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7349 |  246710   577456 |   82236    7328   105520    14.4 |  1.089 % |
c |      7452 |  246710   577456 |   90459    7431   107688    14.5 |  1.090 % |
c |      7603 |  246710   577456 |   99505    7582   110295    14.5 |  1.090 % |
c ==============================================================================
c Found solution: 44602157
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7643 |  246761   577605 |   82253    7622   110961    14.6 |  1.090 % |
c |      7744 |  246761   577605 |   90478    7723   111503    14.4 |  1.091 % |
c |      7894 |  246761   577605 |   99526    7873   114029    14.5 |  1.091 % |
c |      8120 |  246761   577605 |  109478    8099   116121    14.3 |  1.091 % |
c |      8458 |  246761   577605 |  120426    8437   121174    14.4 |  1.091 % |
c |      8964 |  246761   577605 |  132469    8943   140295    15.7 |  1.091 % |
c |      9723 |  246713   577497 |  145716    9698   160602    16.6 |  1.105 % |
c ==============================================================================
c Found solution: 43117436
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10758 |  246413   576829 |   82137   10726   172946    16.1 |  1.105 % |
c |     10859 |  246381   576755 |   90350   10825   177797    16.4 |  1.228 % |
c ==============================================================================
c Found solution: 38341632
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10911 |  246445   576993 |   82148   10877   179492    16.5 |  1.228 % |
c |     11011 |  246445   576993 |   90362   10977   189352    17.2 |  1.229 % |
c |     11162 |  246445   576993 |   99399   11128   194545    17.5 |  1.229 % |
c |     11387 |  246445   576993 |  109338   11353   205177    18.1 |  1.229 % |
c ==============================================================================
c Found solution: 35700986
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11451 |  246500   577138 |   82166   11417   206570    18.1 |  1.229 % |
c |     11552 |  246500   577138 |   90382   11518   211394    18.4 |  1.230 % |
c |     11702 |  246473   577079 |   99420   11667   213352    18.3 |  1.239 % |
c |     11928 |  246473   577079 |  109362   11893   217733    18.3 |  1.239 % |
c |     12266 |  246228   576531 |  120299   12227   220451    18.0 |  1.313 % |
c ==============================================================================
c Found solution: 29162936
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12282 |  246318   576755 |   82106   12243   220850    18.0 |  1.313 % |
c ==============================================================================
c Found solution: 28818010
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12306 |  246341   576816 |   82113   12267   221457    18.1 |  1.313 % |
c |     12406 |  246341   576816 |   90324   12367   227128    18.4 |  1.315 % |
c |     12556 |  246341   576816 |   99356   12517   240047    19.2 |  1.315 % |
c |     12781 |  246341   576816 |  109292   12742   249695    19.6 |  1.315 % |
c |     13119 |  246341   576816 |  120221   13080   273178    20.9 |  1.315 % |
c |     13625 |  246305   576737 |  132243   13584   291747    21.5 |  1.326 % |
c |     14385 |  246305   576737 |  145468   14344   421666    29.4 |  1.326 % |
c ==============================================================================
c Found solution: 27811840
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14935 |  246168   576442 |   82056   14861   451718    30.4 |  1.326 % |
c |     15035 |  246168   576442 |   90261   14961   458151    30.6 |  1.387 % |
c |     15185 |  246168   576442 |   99287   15111   473156    31.3 |  1.387 % |
c |     15414 |  246168   576442 |  109216   15340   492350    32.1 |  1.387 % |
c |     15751 |  246168   576442 |  120138   15677   502654    32.1 |  1.387 % |
c |     16259 |  246138   576375 |  132152   16181   514597    31.8 |  1.397 % |
c |     17018 |  246138   576375 |  145367   16940   530603    31.3 |  1.397 % |
c ==============================================================================
c Found solution: 27486201
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17219 |  246181   576484 |   82060   17141   574441    33.5 |  1.397 % |
c ==============================================================================
c Found solution: 26736640
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17237 |  246199   576531 |   82066   17159   580599    33.8 |  1.397 % |
c |     17337 |  246199   576531 |   90272   17259   582604    33.8 |  1.398 % |
c |     17487 |  246199   576531 |   99299   17409   593424    34.1 |  1.398 % |
c |     17712 |  246183   576496 |  109229   17631   634871    36.0 |  1.403 % |
c |     18050 |  246183   576496 |  120152   17969   667698    37.2 |  1.403 % |
c |     18556 |  246183   576496 |  132168   18475   712989    38.6 |  1.403 % |
c |     19315 |  245813   575658 |  145384   19220   766158    39.9 |  1.529 % |
c ==============================================================================
c Found solution: 25860848
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19568 |  245849   575750 |   81949   19473   776405    39.9 |  1.529 % |
c |     19668 |  245849   575750 |   90143   19573   781991    40.0 |  1.530 % |
c |     19818 |  245849   575750 |   99158   19723   793227    40.2 |  1.530 % |
c |     20044 |  245849   575750 |  109074   19949   816105    40.9 |  1.530 % |
c |     20382 |  245755   575540 |  119981   20274   827520    40.8 |  1.559 % |
c |     20890 |  245755   575540 |  131979   20782   939777    45.2 |  1.559 % |
c |     21651 |  245755   575540 |  145177   21543   986826    45.8 |  1.559 % |
c ==============================================================================
c Found solution: 25036840
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21707 |  245768   575574 |   81922   21596   987544    45.7 |  1.559 % |
c ==============================================================================
c Found solution: 24012840
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21712 |  245800   575656 |   81933   21601   988103    45.7 |  1.559 % |
c ==============================================================================
c Found solution: 22640640
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21744 |  245821   575712 |   81940   21633   989391    45.7 |  1.559 % |
c |     21844 |  245821   575712 |   90134   21733   992254    45.7 |  1.566 % |
c |     21994 |  245817   575703 |   99147   21882   992899    45.4 |  1.568 % |
c |     22219 |  245610   575234 |  109062   22102  1004170    45.4 |  1.636 % |
c |     22556 |  245610   575234 |  119968   22439  1034715    46.1 |  1.636 % |
c |     23062 |  245610   575234 |  131965   22945  1065473    46.4 |  1.636 % |
c |     23821 |  245610   575234 |  145161   23704  1114638    47.0 |  1.636 % |
c |     24960 |  245610   575234 |  159677   24843  1137537    45.8 |  1.636 % |
c |     26669 |  245610   575234 |  175645   26552  1257092    47.3 |  1.636 % |
c |     29232 |  245610   575234 |  193210   29115  1377406    47.3 |  1.636 % |
c |     33077 |  245610   575234 |  212531   32960  1607439    48.8 |  1.636 % |
c ==============================================================================
c Found solution: 21642240
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36344 |  245635   575301 |   81878   36227  1831204    50.5 |  1.636 % |
c |     36444 |  245635   575301 |   90065   36327  1835433    50.5 |  1.637 % |
c |     36594 |  245635   575301 |   99072   36477  1849218    50.7 |  1.637 % |
c |     36823 |  245635   575301 |  108979   36706  1861752    50.7 |  1.637 % |
c |     37161 |  245635   575301 |  119877   37044  1892278    51.1 |  1.637 % |
c |     37667 |  245635   575301 |  131865   37550  1918629    51.1 |  1.637 % |
c |     38427 |  245635   575301 |  145051   38310  1970730    51.4 |  1.637 % |
c |     39566 |  245635   575301 |  159557   39449  2053390    52.1 |  1.637 % |
c |     41275 |  245635   575301 |  175512   41158  2249325    54.7 |  1.637 % |
c |     43839 |  245498   574990 |  193064   43717  2344544    53.6 |  1.685 % |
c |     47683 |  245451   574885 |  212370   47558  2554400    53.7 |  1.700 % |
c |     53449 |  245425   574826 |  233607   53322  2987332    56.0 |  1.708 % |
c |     62099 |  245425   574826 |  256968   61972  3566467    57.5 |  1.708 % |
c |     75074 |  245318   574589 |  282665   74924  4460326    59.5 |  1.759 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_10 -X0_bit_9 -X0_bit_8 -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 X0_bit0 X0_bit1 X0_bit2 X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X0_bit13 -X0_bit14 -X0_bit15 -X0_bit16 -X0_bit17 -X0_bit18 -X0_bit19 -X1_bit_10 -X1_bit_9 -X1_bit_8 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 X1_bit1 X1_bit2 X1_bit3 X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X1_bit13 -X1_bit14 -X1_bit15 -X1_bit16 -X1_bit17 -X1_bit18 -X1_bit19 -X2_bit_10 -X2_bit_9 -X2_bit_8 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X2_bit13 -X2_bit14 -X2_bit15 -X2_bit16 -X2_bit17 -X2_bit18 -X2_bit19 -X3_bit_10 -X3_bit_9 -X3_bit_8 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X3_bit13 -X3_bit14 -X3_bit15 -X3_bit16 -X3_bit17 -X3_bit18 -X3_bit19 -X4_bit_10 -X4_bit_9 -X4_bit_8 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X4_bit13 -X4_bit14 -X4_bit15 -X4_bit16 -X4_bit17 -X4_bit18 -X4_bit19 -X5_bit_10 -X5_bit_9 -X5_bit_8 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X5_bit13 -X5_bit14 -X5_bit15 -X5_bit16 -X5_bit17 -X5_bit18 -X5_bit19 -X6_bit_10 -X6_bit_9 -X6_bit_8 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X6_bit13 -X6_bit14 -X6_bit15 -X6_bit16 -X6_bit17 -X6_bit18 -X6_bit19 -X7_bit_10 -X7_bit_9 -X7_bit_8 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X7_bit13 -X7_bit14 -X7_bit15 -X7_bit16 -X7_bit17 -X7_bit18 -X7_bit19 -X8_bit_10 -X8_bit_9 -X8_bit_8 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 X8_bit0 -X8_bit1 -X8_bit2 X8_bit3 X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X8_bit13 -X8_bit14 -X8_bit15 -X8_bit16 -X8_bit17 -X8_bit18 -X8_bit19 -X9_bit_10 -X9_bit_9 -X9_bit_8 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 X9_bit1 -X9_bit2 X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X9_bit13 -X9_bit14 -X9_bit15 -X9_bit16 -X9_bit17 -X9_bit18 -X9_bit19 -X10_bit_10 -X10_bit_9 -X10_bit_8 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X10_bit13 -X10_bit14 -X10_bit15 -X10_bit16 -X10_bit17 -X10_bit18 -X10_bit19 -X11_bit_10 -X11_bit_9 -X11_bit_8 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X11_bit13 -X11_bit14 -X11_bit15 -X11_bit16 -X11_bit17 -X11_bit18 -X11_bit19 -X12_bit_10 -X12_bit_9 -X12_bit_8 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 X12_bit2 -X12_bit3 X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X12_bit13 -X12_bit14 -X12_bit15 -X12_bit16 -X12_bit17 -X12_bit18 -X12_bit19 -X13_bit_10 -X13_bit_9 -X13_bit_8 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bi

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/22633/stat): 22633 (minisat+_script) R 22632 22633 5245 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1852013372 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/22633/statm): 174 3 169 147 0 27 0
[pid=22633] 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=22634
New process pid=22635
New process pid=22636
execve syscall for /bin/sed executable
One traced child (pid=22635) 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=22636) exited with status: 0
One traced child (pid=22634) exited with status: 0
New process pid=22637
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-gr4x6.opb

[startup+10.0038 s]
Raw data (loadavg): 0.93 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7248 0 0 0 943 25 0 0 25 0 1 0 1852013377 32722944 6930 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 7989 6930 145 145 0 7844 0
[pid=22637] vsize: 31956
Current children cumulated CPU time (s) 9.68
Current children cumulated vsize (Kb) 34080

[startup+20.0056 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7344 0 0 0 1940 26 0 0 25 0 1 0 1852013377 33046528 7026 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 8068 7026 145 145 0 7923 0
[pid=22637] vsize: 32272
Current children cumulated CPU time (s) 19.66
Current children cumulated vsize (Kb) 34396

[startup+30.0074 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7577 0 0 0 2937 27 0 0 25 0 1 0 1852013377 34066432 7259 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 8317 7259 145 145 0 8172 0
[pid=22637] vsize: 33268
Current children cumulated CPU time (s) 29.64
Current children cumulated vsize (Kb) 35392

[startup+40.0071 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7652 0 0 0 3937 28 0 0 25 0 1 0 1852013377 34107392 7270 4294967295 134512640 135094434 3221224432 3221221860 134676608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 8327 7270 145 145 0 8182 0
[pid=22637] vsize: 33308
Current children cumulated CPU time (s) 39.65
Current children cumulated vsize (Kb) 35432

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7706 0 0 0 4937 28 0 0 25 0 1 0 1852013377 34320384 7324 4294967295 134512640 135094434 3221224432 3221221280 134677340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 8379 7324 145 145 0 8234 0
[pid=22637] vsize: 33516
Current children cumulated CPU time (s) 49.65
Current children cumulated vsize (Kb) 35640

[startup+60.0087 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7718 0 0 0 5937 28 0 0 25 0 1 0 1852013377 34369536 7336 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 8391 7336 145 145 0 8246 0
[pid=22637] vsize: 33564
Current children cumulated CPU time (s) 59.65
Current children cumulated vsize (Kb) 35688

[startup+70.0105 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7917 0 0 0 6935 29 0 0 25 0 1 0 1852013377 34516992 7372 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 8427 7372 145 145 0 8282 0
[pid=22637] vsize: 33708
Current children cumulated CPU time (s) 69.64
Current children cumulated vsize (Kb) 35832

[startup+80.0113 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8050 0 0 0 7933 30 0 0 25 0 1 0 1852013377 34648064 7406 4294967295 134512640 135094434 3221224432 3221222160 134677271 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 8459 7406 145 145 0 8314 0
[pid=22637] vsize: 33836
Current children cumulated CPU time (s) 79.63
Current children cumulated vsize (Kb) 35960

[startup+90.0121 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8271 0 0 0 8931 32 0 0 25 0 1 0 1852013377 34959360 7490 4294967295 134512640 135094434 3221224432 3221221440 134600162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 8535 7490 145 145 0 8390 0
[pid=22637] vsize: 34140
Current children cumulated CPU time (s) 89.63
Current children cumulated vsize (Kb) 36264

[startup+100.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8288 0 0 0 9931 32 0 0 25 0 1 0 1852013377 35020800 7507 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 8550 7507 145 145 0 8405 0
[pid=22637] vsize: 34200
Current children cumulated CPU time (s) 99.63
Current children cumulated vsize (Kb) 36324

[startup+110.015 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8368 0 0 0 10929 33 0 0 25 0 1 0 1852013377 35356672 7587 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 8632 7587 145 145 0 8487 0
[pid=22637] vsize: 34528
Current children cumulated CPU time (s) 109.62
Current children cumulated vsize (Kb) 36652

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8539 0 0 0 11928 34 0 0 25 0 1 0 1852013377 35782656 7694 4294967295 134512640 135094434 3221224432 3221221104 134599970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 8736 7694 145 145 0 8591 0
[pid=22637] vsize: 34944
Current children cumulated CPU time (s) 119.62
Current children cumulated vsize (Kb) 37068

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8619 0 0 0 12926 35 0 0 25 0 1 0 1852013377 35962880 7738 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 8780 7738 145 145 0 8635 0
[pid=22637] vsize: 35120
Current children cumulated CPU time (s) 129.61
Current children cumulated vsize (Kb) 37244

[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8654 0 0 0 13926 36 0 0 25 0 1 0 1852013377 36167680 7773 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 8830 7773 145 145 0 8685 0
[pid=22637] vsize: 35320
Current children cumulated CPU time (s) 139.62
Current children cumulated vsize (Kb) 37444

[startup+150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8808 0 0 0 14925 36 0 0 25 0 1 0 1852013377 36392960 7828 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 8885 7828 145 145 0 8740 0
[pid=22637] vsize: 35540
Current children cumulated CPU time (s) 149.61
Current children cumulated vsize (Kb) 37664

[startup+160.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8984 0 0 0 15923 38 0 0 25 0 1 0 1852013377 36737024 7907 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 8969 7907 145 145 0 8824 0
[pid=22637] vsize: 35876
Current children cumulated CPU time (s) 159.61
Current children cumulated vsize (Kb) 38000

[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9066 0 0 0 16922 38 0 0 25 0 1 0 1852013377 37044224 7989 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9044 7989 145 145 0 8899 0
[pid=22637] vsize: 36176
Current children cumulated CPU time (s) 169.6
Current children cumulated vsize (Kb) 38300

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9214 0 0 0 17921 39 0 0 25 0 1 0 1852013377 37380096 8072 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9126 8072 145 145 0 8981 0
[pid=22637] vsize: 36504
Current children cumulated CPU time (s) 179.6
Current children cumulated vsize (Kb) 38628

[startup+190.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9292 0 0 0 18919 39 0 0 25 0 1 0 1852013377 37548032 8114 4294967295 134512640 135094434 3221224432 3221223184 134559512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9167 8114 145 145 0 9022 0
[pid=22637] vsize: 36668
Current children cumulated CPU time (s) 189.58
Current children cumulated vsize (Kb) 38792

[startup+200.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9407 0 0 0 19918 40 0 0 25 0 1 0 1852013377 38019072 8229 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9282 8229 145 145 0 9137 0
[pid=22637] vsize: 37128
Current children cumulated CPU time (s) 199.58
Current children cumulated vsize (Kb) 39252

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9543 0 0 0 20917 41 0 0 25 0 1 0 1852013377 38305792 8301 4294967295 134512640 135094434 3221224432 3221221808 134600904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9352 8301 145 145 0 9207 0
[pid=22637] vsize: 37408
Current children cumulated CPU time (s) 209.58
Current children cumulated vsize (Kb) 39532

[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9734 0 0 0 21916 42 0 0 25 0 1 0 1852013377 38535168 8357 4294967295 134512640 135094434 3221224432 3221221808 134676586 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9408 8357 145 145 0 9263 0
[pid=22637] vsize: 37632
Current children cumulated CPU time (s) 219.58
Current children cumulated vsize (Kb) 39756

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9736 0 0 0 22916 42 0 0 25 0 1 0 1852013377 38535168 8359 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9408 8359 145 145 0 9263 0
[pid=22637] vsize: 37632
Current children cumulated CPU time (s) 229.58
Current children cumulated vsize (Kb) 39756

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9781 0 0 0 23916 42 0 0 25 0 1 0 1852013377 38715392 8404 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9452 8404 145 145 0 9307 0
[pid=22637] vsize: 37808
Current children cumulated CPU time (s) 239.58
Current children cumulated vsize (Kb) 39932

[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9818 0 0 0 24916 43 0 0 25 0 1 0 1852013377 38866944 8441 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9489 8441 145 145 0 9344 0
[pid=22637] vsize: 37956
Current children cumulated CPU time (s) 249.59
Current children cumulated vsize (Kb) 40080

[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9854 0 0 0 25915 43 0 0 25 0 1 0 1852013377 39010304 8477 4294967295 134512640 135094434 3221224432 3221223056 134557619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9524 8477 145 145 0 9379 0
[pid=22637] vsize: 38096
Current children cumulated CPU time (s) 259.58
Current children cumulated vsize (Kb) 40220

[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9902 0 0 0 26914 43 0 0 25 0 1 0 1852013377 39202816 8525 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9571 8525 145 145 0 9426 0
[pid=22637] vsize: 38284
Current children cumulated CPU time (s) 269.57
Current children cumulated vsize (Kb) 40408

[startup+280.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9958 0 0 0 27914 44 0 0 25 0 1 0 1852013377 39428096 8581 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9626 8581 145 145 0 9481 0
[pid=22637] vsize: 38504
Current children cumulated CPU time (s) 279.58
Current children cumulated vsize (Kb) 40628

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10015 0 0 0 28913 44 0 0 25 0 1 0 1852013377 39661568 8638 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9683 8638 145 145 0 9538 0
[pid=22637] vsize: 38732
Current children cumulated CPU time (s) 289.57
Current children cumulated vsize (Kb) 40856

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10065 0 0 0 29912 45 0 0 25 0 1 0 1852013377 39862272 8688 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9732 8688 145 145 0 9587 0
[pid=22637] vsize: 38928
Current children cumulated CPU time (s) 299.57
Current children cumulated vsize (Kb) 41052

[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10123 0 0 0 30911 45 0 0 25 0 1 0 1852013377 40095744 8746 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9789 8746 145 145 0 9644 0
[pid=22637] vsize: 39156
Current children cumulated CPU time (s) 309.56
Current children cumulated vsize (Kb) 41280

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10181 0 0 0 31910 46 0 0 25 0 1 0 1852013377 40329216 8804 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9846 8804 145 145 0 9701 0
[pid=22637] vsize: 39384
Current children cumulated CPU time (s) 319.56
Current children cumulated vsize (Kb) 41508

[startup+330.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10232 0 0 0 32909 47 0 0 25 0 1 0 1852013377 40534016 8855 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9896 8855 145 145 0 9751 0
[pid=22637] vsize: 39584
Current children cumulated CPU time (s) 329.56
Current children cumulated vsize (Kb) 41708

[startup+340.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10280 0 0 0 33908 47 0 0 25 0 1 0 1852013377 40730624 8903 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9944 8903 145 145 0 9799 0
[pid=22637] vsize: 39776
Current children cumulated CPU time (s) 339.55
Current children cumulated vsize (Kb) 41900

[startup+350.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10331 0 0 0 34908 47 0 0 25 0 1 0 1852013377 40935424 8954 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 9994 8954 145 145 0 9849 0
[pid=22637] vsize: 39976
Current children cumulated CPU time (s) 349.55
Current children cumulated vsize (Kb) 42100

[startup+360.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10371 0 0 0 35908 48 0 0 25 0 1 0 1852013377 41099264 8994 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10034 8994 145 145 0 9889 0
[pid=22637] vsize: 40136
Current children cumulated CPU time (s) 359.56
Current children cumulated vsize (Kb) 42260

[startup+370.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10428 0 0 0 36907 48 0 0 25 0 1 0 1852013377 41459712 9051 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10122 9051 145 145 0 9977 0
[pid=22637] vsize: 40488
Current children cumulated CPU time (s) 369.55
Current children cumulated vsize (Kb) 42612

[startup+380.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10481 0 0 0 37907 48 0 0 25 0 1 0 1852013377 41672704 9104 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10174 9104 145 145 0 10029 0
[pid=22637] vsize: 40696
Current children cumulated CPU time (s) 379.55
Current children cumulated vsize (Kb) 42820

[startup+390.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10532 0 0 0 38905 49 0 0 25 0 1 0 1852013377 41877504 9155 4294967295 134512640 135094434 3221224432 3221223080 134558037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10224 9155 145 145 0 10079 0
[pid=22637] vsize: 40896
Current children cumulated CPU time (s) 389.54
Current children cumulated vsize (Kb) 43020

[startup+400.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10587 0 0 0 39904 49 0 0 25 0 1 0 1852013377 42102784 9210 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10279 9210 145 145 0 10134 0
[pid=22637] vsize: 41116
Current children cumulated CPU time (s) 399.53
Current children cumulated vsize (Kb) 43240

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10635 0 0 0 40904 49 0 0 25 0 1 0 1852013377 42295296 9258 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10326 9258 145 145 0 10181 0
[pid=22637] vsize: 41304
Current children cumulated CPU time (s) 409.53
Current children cumulated vsize (Kb) 43428

[startup+420.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10777 0 0 0 41902 50 0 0 25 0 1 0 1852013377 42471424 9301 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10369 9301 145 145 0 10224 0
[pid=22637] vsize: 41476
Current children cumulated CPU time (s) 419.52
Current children cumulated vsize (Kb) 43600

[startup+430.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10847 0 0 0 42902 51 0 0 25 0 1 0 1852013377 42754048 9371 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10438 9371 145 145 0 10293 0
[pid=22637] vsize: 41752
Current children cumulated CPU time (s) 429.53
Current children cumulated vsize (Kb) 43876

[startup+440.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10905 0 0 0 43901 51 0 0 25 0 1 0 1852013377 42987520 9429 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10495 9429 145 145 0 10350 0
[pid=22637] vsize: 41980
Current children cumulated CPU time (s) 439.52
Current children cumulated vsize (Kb) 44104

[startup+450.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10969 0 0 0 44901 51 0 0 25 0 1 0 1852013377 43253760 9493 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10560 9493 145 145 0 10415 0
[pid=22637] vsize: 42240
Current children cumulated CPU time (s) 449.52
Current children cumulated vsize (Kb) 44364

[startup+460.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11020 0 0 0 45900 52 0 0 25 0 1 0 1852013377 43454464 9544 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10609 9544 145 145 0 10464 0
[pid=22637] vsize: 42436
Current children cumulated CPU time (s) 459.52
Current children cumulated vsize (Kb) 44560

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11094 0 0 0 46899 52 0 0 25 0 1 0 1852013377 43753472 9618 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10682 9618 145 145 0 10537 0
[pid=22637] vsize: 42728
Current children cumulated CPU time (s) 469.51
Current children cumulated vsize (Kb) 44852

[startup+480.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11182 0 0 0 47898 53 0 0 25 0 1 0 1852013377 44118016 9706 4294967295 134512640 135094434 3221224432 3221223056 134562076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10771 9706 145 145 0 10626 0
[pid=22637] vsize: 43084
Current children cumulated CPU time (s) 479.51
Current children cumulated vsize (Kb) 45208

[startup+490.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11238 0 0 0 48898 53 0 0 25 0 1 0 1852013377 44343296 9762 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10826 9762 145 145 0 10681 0
[pid=22637] vsize: 43304
Current children cumulated CPU time (s) 489.51
Current children cumulated vsize (Kb) 45428

[startup+500.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11295 0 0 0 49897 54 0 0 25 0 1 0 1852013377 44576768 9819 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10883 9819 145 145 0 10738 0
[pid=22637] vsize: 43532
Current children cumulated CPU time (s) 499.51
Current children cumulated vsize (Kb) 45656

[startup+510.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11345 0 0 0 50897 54 0 0 25 0 1 0 1852013377 44781568 9869 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10933 9869 145 145 0 10788 0
[pid=22637] vsize: 43732
Current children cumulated CPU time (s) 509.51
Current children cumulated vsize (Kb) 45856

[startup+520.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11384 0 0 0 51896 55 0 0 25 0 1 0 1852013377 44941312 9908 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 10972 9908 145 145 0 10827 0
[pid=22637] vsize: 43888
Current children cumulated CPU time (s) 519.51
Current children cumulated vsize (Kb) 46012

[startup+530.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11435 0 0 0 52895 55 0 0 25 0 1 0 1852013377 45146112 9959 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11022 9959 145 145 0 10877 0
[pid=22637] vsize: 44088
Current children cumulated CPU time (s) 529.5
Current children cumulated vsize (Kb) 46212

[startup+540.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11522 0 0 0 53893 56 0 0 25 0 1 0 1852013377 45502464 10046 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11109 10046 145 145 0 10964 0
[pid=22637] vsize: 44436
Current children cumulated CPU time (s) 539.49
Current children cumulated vsize (Kb) 46560

[startup+550.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11584 0 0 0 54892 56 0 0 25 0 1 0 1852013377 45744128 10108 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11168 10108 145 145 0 11023 0
[pid=22637] vsize: 44672
Current children cumulated CPU time (s) 549.48
Current children cumulated vsize (Kb) 46796

[startup+560.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11639 0 0 0 55892 57 0 0 25 0 1 0 1852013377 45969408 10163 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11223 10163 145 145 0 11078 0
[pid=22637] vsize: 44892
Current children cumulated CPU time (s) 559.49
Current children cumulated vsize (Kb) 47016

[startup+570.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11676 0 0 0 56892 57 0 0 25 0 1 0 1852013377 46116864 10200 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11259 10200 145 145 0 11114 0
[pid=22637] vsize: 45036
Current children cumulated CPU time (s) 569.49
Current children cumulated vsize (Kb) 47160

[startup+580.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11723 0 0 0 57892 57 0 0 25 0 1 0 1852013377 46309376 10247 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11306 10247 145 145 0 11161 0
[pid=22637] vsize: 45224
Current children cumulated CPU time (s) 579.49
Current children cumulated vsize (Kb) 47348

[startup+590.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11763 0 0 0 58892 57 0 0 25 0 1 0 1852013377 46469120 10287 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11345 10287 145 145 0 11200 0
[pid=22637] vsize: 45380
Current children cumulated CPU time (s) 589.49
Current children cumulated vsize (Kb) 47504

[startup+600.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11808 0 0 0 59891 57 0 0 25 0 1 0 1852013377 46653440 10332 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11390 10332 145 145 0 11245 0
[pid=22637] vsize: 45560
Current children cumulated CPU time (s) 599.48
Current children cumulated vsize (Kb) 47684

[startup+610.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11861 0 0 0 60890 58 0 0 25 0 1 0 1852013377 46866432 10385 4294967295 134512640 135094434 3221224432 3221223056 134557630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11442 10385 145 145 0 11297 0
[pid=22637] vsize: 45768
Current children cumulated CPU time (s) 609.48
Current children cumulated vsize (Kb) 47892

[startup+620.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11903 0 0 0 61890 58 0 0 25 0 1 0 1852013377 47038464 10427 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11484 10427 145 145 0 11339 0
[pid=22637] vsize: 45936
Current children cumulated CPU time (s) 619.48
Current children cumulated vsize (Kb) 48060

[startup+630.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11951 0 0 0 62890 58 0 0 25 0 1 0 1852013377 47230976 10475 4294967295 134512640 135094434 3221224432 3221223024 134556776 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11531 10475 145 145 0 11386 0
[pid=22637] vsize: 46124
Current children cumulated CPU time (s) 629.48
Current children cumulated vsize (Kb) 48248

[startup+640.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12000 0 0 0 63889 59 0 0 25 0 1 0 1852013377 47435776 10524 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11581 10524 145 145 0 11436 0
[pid=22637] vsize: 46324
Current children cumulated CPU time (s) 639.48
Current children cumulated vsize (Kb) 48448

[startup+650.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12056 0 0 0 64889 59 0 0 25 0 1 0 1852013377 47656960 10580 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11635 10580 145 145 0 11490 0
[pid=22637] vsize: 46540
Current children cumulated CPU time (s) 649.48
Current children cumulated vsize (Kb) 48664

[startup+660.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12119 0 0 0 65887 60 0 0 25 0 1 0 1852013377 47910912 10643 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11697 10643 145 145 0 11552 0
[pid=22637] vsize: 46788
Current children cumulated CPU time (s) 659.47
Current children cumulated vsize (Kb) 48912

[startup+670.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12162 0 0 0 66887 60 0 0 25 0 1 0 1852013377 48087040 10686 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11740 10686 145 145 0 11595 0
[pid=22637] vsize: 46960
Current children cumulated CPU time (s) 669.47
Current children cumulated vsize (Kb) 49084

[startup+680.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12208 0 0 0 67887 60 0 0 25 0 1 0 1852013377 48271360 10732 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11785 10732 145 145 0 11640 0
[pid=22637] vsize: 47140
Current children cumulated CPU time (s) 679.47
Current children cumulated vsize (Kb) 49264

[startup+690.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12249 0 0 0 68886 61 0 0 25 0 1 0 1852013377 48435200 10773 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11825 10773 145 145 0 11680 0
[pid=22637] vsize: 47300
Current children cumulated CPU time (s) 689.47
Current children cumulated vsize (Kb) 49424

[startup+700.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12294 0 0 0 69886 61 0 0 25 0 1 0 1852013377 48619520 10818 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11870 10818 145 145 0 11725 0
[pid=22637] vsize: 47480
Current children cumulated CPU time (s) 699.47
Current children cumulated vsize (Kb) 49604

[startup+710.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12352 0 0 0 70885 62 0 0 25 0 1 0 1852013377 48852992 10876 4294967295 134512640 135094434 3221224432 3221223056 134557627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11927 10876 145 145 0 11782 0
[pid=22637] vsize: 47708
Current children cumulated CPU time (s) 709.47
Current children cumulated vsize (Kb) 49832

[startup+720.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12397 0 0 0 71884 62 0 0 25 0 1 0 1852013377 49033216 10921 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 11971 10921 145 145 0 11826 0
[pid=22637] vsize: 47884
Current children cumulated CPU time (s) 719.46
Current children cumulated vsize (Kb) 50008

[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12444 0 0 0 72884 62 0 0 25 0 1 0 1852013377 49225728 10968 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 12018 10968 145 145 0 11873 0
[pid=22637] vsize: 48072
Current children cumulated CPU time (s) 729.46
Current children cumulated vsize (Kb) 50196

[startup+740.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12494 0 0 0 73883 63 0 0 25 0 1 0 1852013377 49426432 11018 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 12067 11018 145 145 0 11922 0
[pid=22637] vsize: 48268
Current children cumulated CPU time (s) 739.46
Current children cumulated vsize (Kb) 50392

[startup+750.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12541 0 0 0 74883 63 0 0 25 0 1 0 1852013377 49614848 11065 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 12113 11065 145 145 0 11968 0
[pid=22637] vsize: 48452
Current children cumulated CPU time (s) 749.46
Current children cumulated vsize (Kb) 50576

[startup+760.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12604 0 0 0 75882 64 0 0 25 0 1 0 1852013377 49872896 11128 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 12176 11128 145 145 0 12031 0
[pid=22637] vsize: 48704
Current children cumulated CPU time (s) 759.46
Current children cumulated vsize (Kb) 50828

[startup+770.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12664 0 0 0 76881 64 0 0 25 0 1 0 1852013377 50114560 11188 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 12235 11188 145 145 0 12090 0
[pid=22637] vsize: 48940
Current children cumulated CPU time (s) 769.45
Current children cumulated vsize (Kb) 51064

[startup+780.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12723 0 0 0 77881 65 0 0 25 0 1 0 1852013377 50352128 11247 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 12293 11247 145 145 0 12148 0
[pid=22637] vsize: 49172
Current children cumulated CPU time (s) 779.46
Current children cumulated vsize (Kb) 51296

[startup+790.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12786 0 0 0 78880 65 0 0 25 0 1 0 1852013377 50610176 11310 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 12356 11310 145 145 0 12211 0
[pid=22637] vsize: 49424
Current children cumulated CPU time (s) 789.45
Current children cumulated vsize (Kb) 51548

[startup+800.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12841 0 0 0 79878 66 0 0 25 0 1 0 1852013377 50839552 11365 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 12412 11365 145 145 0 12267 0
[pid=22637] vsize: 49648
Current children cumulated CPU time (s) 799.44
Current children cumulated vsize (Kb) 51772

[startup+810.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12900 0 0 0 80878 67 0 0 25 0 1 0 1852013377 51081216 11424 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 12471 11424 145 145 0 12326 0
[pid=22637] vsize: 49884
Current children cumulated CPU time (s) 809.45
Current children cumulated vsize (Kb) 52008

[startup+820.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12957 0 0 0 81876 68 0 0 25 0 1 0 1852013377 51318784 11481 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 12529 11481 145 145 0 12384 0
[pid=22637] vsize: 50116
Current children cumulated CPU time (s) 819.44
Current children cumulated vsize (Kb) 52240

[startup+830.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13004 0 0 0 82874 69 0 0 25 0 1 0 1852013377 51503104 11528 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 12574 11528 145 145 0 12429 0
[pid=22637] vsize: 50296
Current children cumulated CPU time (s) 829.43
Current children cumulated vsize (Kb) 52420

[startup+840.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13060 0 0 0 83873 70 0 0 25 0 1 0 1852013377 51990528 11584 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 12693 11584 145 145 0 12548 0
[pid=22637] vsize: 50772
Current children cumulated CPU time (s) 839.43
Current children cumulated vsize (Kb) 52896

[startup+850.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13118 0 0 0 84872 70 0 0 25 0 1 0 1852013377 52224000 11642 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 12750 11642 145 145 0 12605 0
[pid=22637] vsize: 51000
Current children cumulated CPU time (s) 849.42
Current children cumulated vsize (Kb) 53124

[startup+860.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13175 0 0 0 85871 71 0 0 25 0 1 0 1852013377 52453376 11699 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 12806 11699 145 145 0 12661 0
[pid=22637] vsize: 51224
Current children cumulated CPU time (s) 859.42
Current children cumulated vsize (Kb) 53348

[startup+870.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13227 0 0 0 86869 72 0 0 25 0 1 0 1852013377 52662272 11751 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 12857 11751 145 145 0 12712 0
[pid=22637] vsize: 51428
Current children cumulated CPU time (s) 869.41
Current children cumulated vsize (Kb) 53552

[startup+880.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13287 0 0 0 87868 73 0 0 25 0 1 0 1852013377 52899840 11811 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 12915 11811 145 145 0 12770 0
[pid=22637] vsize: 51660
Current children cumulated CPU time (s) 879.41
Current children cumulated vsize (Kb) 53784

[startup+890.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13342 0 0 0 88867 74 0 0 25 0 1 0 1852013377 53121024 11866 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 12969 11866 145 145 0 12824 0
[pid=22637] vsize: 51876
Current children cumulated CPU time (s) 889.41
Current children cumulated vsize (Kb) 54000

[startup+900.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13399 0 0 0 89866 74 0 0 25 0 1 0 1852013377 53362688 11923 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 13028 11923 145 145 0 12883 0
[pid=22637] vsize: 52112
Current children cumulated CPU time (s) 899.4
Current children cumulated vsize (Kb) 54236

[startup+910.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13444 0 0 0 90865 75 0 0 25 0 1 0 1852013377 53551104 11968 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 13074 11968 145 145 0 12929 0
[pid=22637] vsize: 52296
Current children cumulated CPU time (s) 909.4
Current children cumulated vsize (Kb) 54420

[startup+920.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13492 0 0 0 91864 75 0 0 25 0 1 0 1852013377 53747712 12016 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13122 12016 145 145 0 12977 0
[pid=22637] vsize: 52488
Current children cumulated CPU time (s) 919.39
Current children cumulated vsize (Kb) 54612

[startup+930.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13559 0 0 0 92863 76 0 0 25 0 1 0 1852013377 54050816 12083 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13196 12083 145 145 0 13051 0
[pid=22637] vsize: 52784
Current children cumulated CPU time (s) 929.39
Current children cumulated vsize (Kb) 54908

[startup+940.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13637 0 0 0 93862 77 0 0 25 0 1 0 1852013377 54374400 12161 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13275 12161 145 145 0 13130 0
[pid=22637] vsize: 53100
Current children cumulated CPU time (s) 939.39
Current children cumulated vsize (Kb) 55224

[startup+950.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13713 0 0 0 94861 77 0 0 25 0 1 0 1852013377 54685696 12237 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13351 12237 145 145 0 13206 0
[pid=22637] vsize: 53404
Current children cumulated CPU time (s) 949.38
Current children cumulated vsize (Kb) 55528

[startup+960.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13776 0 0 0 95860 78 0 0 25 0 1 0 1852013377 54939648 12300 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13413 12300 145 145 0 13268 0
[pid=22637] vsize: 53652
Current children cumulated CPU time (s) 959.38
Current children cumulated vsize (Kb) 55776

[startup+970.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13847 0 0 0 96859 78 0 0 25 0 1 0 1852013377 55230464 12371 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 13484 12371 145 145 0 13339 0
[pid=22637] vsize: 53936
Current children cumulated CPU time (s) 969.37
Current children cumulated vsize (Kb) 56060

[startup+980.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13910 0 0 0 97858 79 0 0 25 0 1 0 1852013377 55480320 12434 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13545 12434 145 145 0 13400 0
[pid=22637] vsize: 54180
Current children cumulated CPU time (s) 979.37
Current children cumulated vsize (Kb) 56304

[startup+990.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13969 0 0 0 98857 79 0 0 25 0 1 0 1852013377 55713792 12493 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13602 12493 145 145 0 13457 0
[pid=22637] vsize: 54408
Current children cumulated CPU time (s) 989.36
Current children cumulated vsize (Kb) 56532

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14037 0 0 0 99856 80 0 0 25 0 1 0 1852013377 56000512 12561 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13672 12561 145 145 0 13527 0
[pid=22637] vsize: 54688
Current children cumulated CPU time (s) 999.36
Current children cumulated vsize (Kb) 56812

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14095 0 0 0 100855 80 0 0 25 0 1 0 1852013377 56250368 12619 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13733 12619 145 145 0 13588 0
[pid=22637] vsize: 54932
Current children cumulated CPU time (s) 1009.35
Current children cumulated vsize (Kb) 57056

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14142 0 0 0 101855 80 0 0 25 0 1 0 1852013377 56434688 12666 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13778 12666 145 145 0 13633 0
[pid=22637] vsize: 55112
Current children cumulated CPU time (s) 1019.35
Current children cumulated vsize (Kb) 57236

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14199 0 0 0 102855 80 0 0 25 0 1 0 1852013377 56668160 12723 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13835 12723 145 145 0 13690 0
[pid=22637] vsize: 55340
Current children cumulated CPU time (s) 1029.35
Current children cumulated vsize (Kb) 57464

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14249 0 0 0 103854 81 0 0 25 0 1 0 1852013377 56868864 12773 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22637/statm): 13884 12773 145 145 0 13739 0
[pid=22637] vsize: 55536
Current children cumulated CPU time (s) 1039.35
Current children cumulated vsize (Kb) 57660

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14287 0 0 0 104853 81 0 0 25 0 1 0 1852013377 57020416 12811 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13921 12811 145 145 0 13776 0
[pid=22637] vsize: 55684
Current children cumulated CPU time (s) 1049.34
Current children cumulated vsize (Kb) 57808

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14332 0 0 0 105853 82 0 0 25 0 1 0 1852013377 57200640 12856 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 13965 12856 145 145 0 13820 0
[pid=22637] vsize: 55860
Current children cumulated CPU time (s) 1059.35
Current children cumulated vsize (Kb) 57984

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14388 0 0 0 106852 82 0 0 25 0 1 0 1852013377 57438208 12912 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14023 12912 145 145 0 13878 0
[pid=22637] vsize: 56092
Current children cumulated CPU time (s) 1069.34
Current children cumulated vsize (Kb) 58216

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14433 0 0 0 107851 83 0 0 25 0 1 0 1852013377 57610240 12957 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14065 12957 145 145 0 13920 0
[pid=22637] vsize: 56260
Current children cumulated CPU time (s) 1079.34
Current children cumulated vsize (Kb) 58384

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14493 0 0 0 108851 83 0 0 25 0 1 0 1852013377 57876480 13017 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14130 13017 145 145 0 13985 0
[pid=22637] vsize: 56520
Current children cumulated CPU time (s) 1089.34
Current children cumulated vsize (Kb) 58644

[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14563 0 0 0 109850 83 0 0 25 0 1 0 1852013377 58183680 13087 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14205 13087 145 145 0 14060 0
[pid=22637] vsize: 56820
Current children cumulated CPU time (s) 1099.33
Current children cumulated vsize (Kb) 58944

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14616 0 0 0 110849 84 0 0 25 0 1 0 1852013377 58396672 13140 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14257 13140 145 145 0 14112 0
[pid=22637] vsize: 57028
Current children cumulated CPU time (s) 1109.33
Current children cumulated vsize (Kb) 59152

[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14669 0 0 0 111849 84 0 0 25 0 1 0 1852013377 58621952 13193 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14312 13193 145 145 0 14167 0
[pid=22637] vsize: 57248
Current children cumulated CPU time (s) 1119.33
Current children cumulated vsize (Kb) 59372

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14738 0 0 0 112849 85 0 0 25 0 1 0 1852013377 58896384 13262 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14379 13262 145 145 0 14234 0
[pid=22637] vsize: 57516
Current children cumulated CPU time (s) 1129.34
Current children cumulated vsize (Kb) 59640

[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14792 0 0 0 113848 85 0 0 25 0 1 0 1852013377 59129856 13316 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14436 13316 145 145 0 14291 0
[pid=22637] vsize: 57744
Current children cumulated CPU time (s) 1139.33
Current children cumulated vsize (Kb) 59868

[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14850 0 0 0 114848 85 0 0 25 0 1 0 1852013377 59359232 13374 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14492 13374 145 145 0 14347 0
[pid=22637] vsize: 57968
Current children cumulated CPU time (s) 1149.33
Current children cumulated vsize (Kb) 60092

[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14890 0 0 0 115848 85 0 0 25 0 1 0 1852013377 59527168 13414 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14533 13414 145 145 0 14388 0
[pid=22637] vsize: 58132
Current children cumulated CPU time (s) 1159.33
Current children cumulated vsize (Kb) 60256

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14941 0 0 0 116847 86 0 0 25 0 1 0 1852013377 59744256 13465 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14586 13465 145 145 0 14441 0
[pid=22637] vsize: 58344
Current children cumulated CPU time (s) 1169.33
Current children cumulated vsize (Kb) 60468

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14989 0 0 0 117847 86 0 0 25 0 1 0 1852013377 59932672 13513 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14632 13513 145 145 0 14487 0
[pid=22637] vsize: 58528
Current children cumulated CPU time (s) 1179.33
Current children cumulated vsize (Kb) 60652

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 15039 0 0 0 118846 87 0 0 25 0 1 0 1852013377 60133376 13563 4294967295 134512640 135094434 3221224432 3221223056 134557606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14681 13563 145 145 0 14536 0
[pid=22637] vsize: 58724
Current children cumulated CPU time (s) 1189.33
Current children cumulated vsize (Kb) 60848

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 15097 0 0 0 119845 88 0 0 25 0 1 0 1852013377 60387328 13621 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14743 13621 145 145 0 14598 0
[pid=22637] vsize: 58972
Current children cumulated CPU time (s) 1199.33
Current children cumulated vsize (Kb) 61096

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 15157 0 0 0 120845 88 0 0 25 0 1 0 1852013377 60637184 13681 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14804 13681 145 145 0 14659 0
[pid=22637] vsize: 59216
Current children cumulated CPU time (s) 1209.33
Current children cumulated vsize (Kb) 61340



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 22637
Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22633/statm): 531 226 485 147 0 384 0
[pid=22633] vsize: 2124
Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 15157 0 0 0 120845 88 0 0 25 0 1 0 1852013377 60637184 13681 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22637/statm): 14804 13681 145 145 0 14659 0
[pid=22637] vsize: 59216
Current children cumulated CPU time (s) 1209.33
Current children cumulated vsize (Kb) 61340

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1209.37
CPU user time (s): 1208.46
CPU system time (s): 0.906862
CPU usage (%): 99.9344
Max. virtual memory (cumulated for all children) (Kb): 61340

Verifier Data

ERROR: no interpretation found !