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-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-gr4x6.opb
MD5SUMc1c7537cd9b3e10215a81ec1ca3be5cb
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 3046400
Optimality of the best value was proved NO
Number of terms in the objective function 504
Biggest coefficient in the objective function 148373504
Number of bits for the biggest coefficient in the objective function 28
Sum of the numbers in the objective function 3393589600
Number of bits of the sum of numbers in the objective function 32
Biggest number in a constraint 148373504
Number of bits of the biggest number in a constraint 28
Biggest sum of numbers in a constraint 3393589600
Number of bits of the biggest sum of numbers32
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1223.09
Number of variables504
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 constraint21
Maximum length of a constraint120

Trace number 6276

Launcher Data

LAUNCH ON wulflinc18 THE 2005-09-20 05:05:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3434 boxname=wulflinc18 idbench=1090 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c1c7537cd9b3e10215a81ec1ca3be5cb  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-gr4x6.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-gr4x6.opb
IDLAUNCH: 3434
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        909180 kB
Buffers:          4976 kB
Cached:          91844 kB
SwapCached:        760 kB
Active:          23076 kB
Inactive:        76308 kB
HighTotal:      131008 kB
HighFree:        35644 kB
LowTotal:       903652 kB
LowFree:        873536 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5772 kB
Slab:            20328 kB
Committed_AS:    64148 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:25:48 (client local time) WITH STATUS 10 IN 1209.35 SECONDS
stats: 3434 7 1209.35 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:  972     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  972     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost:  900     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  888     Base: 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[  23]---> BDD-cost:   19
c ---[  22]---> BDD-cost:   16
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   15
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   15
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   15
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   17
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   19
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   15349    36385 |    5116       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 5885984
c ---[   0]---> Sorter-cost:63755     Base: 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 |        78 |  192309   449611 |   64103      78      360     4.6 |  0.000 % |
c |       179 |  192309   449611 |   70513     179     1995    11.1 |  0.939 % |
c |       330 |  192309   449611 |   77564     330     2915     8.8 |  0.939 % |
c |       555 |  192309   449611 |   85321     555     4340     7.8 |  0.939 % |
c |       892 |  192309   449611 |   93853     892     6726     7.5 |  0.939 % |
c |      1399 |  192309   449611 |  103238    1399    14459    10.3 |  0.939 % |
c |      2158 |  192215   449400 |  113562    2155    30502    14.2 |  0.975 % |
c |      3297 |  192215   449400 |  124918    3294   177563    53.9 |  0.975 % |
c ==============================================================================
c Found solution: 4547392
c ---[   0]---> Sorter-cost:   12     Base: 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 |      3400 |  192789   451295 |   64263    3389   179355    52.9 |  0.975 % |
c |      3500 |  192789   451295 |   70689    3489   184974    53.0 |  1.010 % |
c |      3651 |  192769   451250 |   77758    3639   186369    51.2 |  1.017 % |
c |      3876 |  192357   450318 |   85534    3857   190287    49.3 |  1.191 % |
c ==============================================================================
c Found solution: 4505992
c ---[   0]---> Sorter-cost:   14     Base: 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 |      4161 |  192378   450633 |   64126    4129   197031    47.7 |  1.191 % |
c |      4261 |  192378   450633 |   70538    4229   198431    46.9 |  1.360 % |
c |      4411 |  192279   450409 |   77592    4377   200682    45.8 |  1.402 % |
c |      4636 |  192244   450331 |   85351    4599   203524    44.3 |  1.417 % |
c |      4973 |  192244   450331 |   93886    4936   248916    50.4 |  1.417 % |
c |      5480 |  192244   450331 |  103275    5443   257646    47.3 |  1.417 % |
c |      6239 |  192244   450331 |  113603    6202   282898    45.6 |  1.417 % |
c |      7379 |  192111   450029 |  124963    7106   316426    44.5 |  1.473 % |
c |      9089 |  191828   449383 |  137459    8807   401005    45.5 |  1.593 % |
c |     11653 |  191808   449338 |  151205   11369   430975    37.9 |  1.600 % |
c |     15499 |  191615   448906 |  166326   15206   784188    51.6 |  1.684 % |
c ==============================================================================
c Found solution: 3607624
c ---[   0]---> Sorter-cost:   12     Base: 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 |     16365 |  191688   449214 |   63896   16043   812376    50.6 |  1.684 % |
c ==============================================================================
c Found solution: 3423277
c ---[   0]---> Sorter-cost:   15     Base: 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 |     16372 |  191727   449409 |   63909   16050   812415    50.6 |  1.684 % |
c |     16472 |  191727   449409 |   70299   16150   822793    50.9 |  1.805 % |
c |     16622 |  191727   449409 |   77329   16300   832150    51.1 |  1.805 % |
c |     16847 |  191727   449409 |   85062   16525   848482    51.3 |  1.805 % |
c |     17185 |  191727   449409 |   93569   16863   864612    51.3 |  1.805 % |
c |     17691 |  191727   449409 |  102926   17369   939920    54.1 |  1.805 % |
c |     18450 |  191663   449264 |  113218   18127   990313    54.6 |  1.830 % |
c ==============================================================================
c Found solution: 3400032
c ---[   0]---> Sorter-cost:   11     Base: 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 |     19266 |  191676   449301 |   63892   18943  1179458    62.3 |  1.830 % |
c |     19367 |  191588   449103 |   70281   19024  1183836    62.2 |  1.871 % |
c |     19518 |  191416   448715 |   77309   19149  1190402    62.2 |  1.954 % |
c |     19744 |  191368   448606 |   85040   19374  1203086    62.1 |  1.975 % |
c |     20082 |  191368   448606 |   93544   19712  1240205    62.9 |  1.975 % |
c |     20591 |  191368   448606 |  102898   20221  1291193    63.9 |  1.975 % |
c |     21351 |  190404   446406 |  113188   20892  1335676    63.9 |  2.419 % |
c |     22490 |  190404   446406 |  124507   22031  1452208    65.9 |  2.419 % |
c |     24198 |  190404   446406 |  136958   23739  1636081    68.9 |  2.419 % |
c ==============================================================================
c Found solution: 3367610
c ---[   0]---> Sorter-cost:   16     Base: 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 |     24649 |  190424   446476 |   63474   24181  1665305    68.9 |  2.419 % |
c ==============================================================================
c Found solution: 3298476
c ---[   0]---> Sorter-cost:   16     Base: 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 |     24667 |  190445   446527 |   63481   24199  1665514    68.8 |  2.419 % |
c |     24767 |  190445   446527 |   69829   24299  1677707    69.0 |  2.422 % |
c |     24917 |  190445   446527 |   76812   24449  1680953    68.8 |  2.422 % |
c |     25143 |  190445   446527 |   84493   24675  1700084    68.9 |  2.422 % |
c |     25480 |  190445   446527 |   92942   25012  1704985    68.2 |  2.422 % |
c |     25988 |  190445   446527 |  102236   25520  1713199    67.1 |  2.422 % |
c |     26747 |  190445   446527 |  112460   26279  1847940    70.3 |  2.422 % |
c |     27886 |  190408   446443 |  123706   27412  2018790    73.6 |  2.440 % |
c |     29595 |  190388   446399 |  136077   29115  2098475    72.1 |  2.448 % |
c ==============================================================================
c Found solution: 3268695
c ---[   0]---> Sorter-cost:   15     Base: 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 |     30664 |  190409   446461 |   63469   30181  2278674    75.5 |  2.448 % |
c |     30764 |  190409   446461 |   69815   30281  2280211    75.3 |  2.457 % |
c |     30915 |  190409   446461 |   76797   30432  2286100    75.1 |  2.457 % |
c |     31141 |  190409   446461 |   84477   30658  2295700    74.9 |  2.457 % |
c |     31478 |  190409   446461 |   92924   30995  2327171    75.1 |  2.457 % |
c ==============================================================================
c Found solution: 3134720
c ---[   0]---> Sorter-cost:   10     Base: 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 |     31735 |  190420   446494 |   63473   31252  2353209    75.3 |  2.457 % |
c |     31835 |  190379   446400 |   69820   31351  2358121    75.2 |  2.475 % |
c |     31986 |  190379   446400 |   76802   31502  2369464    75.2 |  2.475 % |
c |     32211 |  190379   446400 |   84482   31727  2395563    75.5 |  2.475 % |
c |     32550 |  190379   446400 |   92930   32066  2438868    76.1 |  2.475 % |
c |     33056 |  190379   446400 |  102223   32572  2483971    76.3 |  2.475 % |
c |     33817 |  190379   446400 |  112446   33333  2627192    78.8 |  2.475 % |
c |     34956 |  190379   446400 |  123690   34472  2710906    78.6 |  2.475 % |
c |     36664 |  190317   446259 |  136060   36177  2807464    77.6 |  2.502 % |
c |     39226 |  190317   446259 |  149666   38739  3106741    80.2 |  2.502 % |
c |     43070 |  190317   446259 |  164632   42583  3440355    80.8 |  2.502 % |
c |     48838 |  190110   445788 |  181095   48336  3908973    80.9 |  2.592 % |
c |     57487 |  190110   445788 |  199205   56985  4842937    85.0 |  2.592 % |
c |     70462 |  190110   445788 |  219126   69960  5996043    85.7 |  2.592 % |
c ==============================================================================
c Found solution: 3127040
c ---[   0]---> Sorter-cost:    8     Base: 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 |     80923 |  190122   445817 |   63374   80421  6986009    86.9 |  2.592 % |
c |     81023 |  190122   445817 |   69711   21093  1212194    57.5 |  2.593 % |
c |     81173 |  190122   445817 |   76682   21243  1225608    57.7 |  2.593 % |
c |     81398 |  190122   445817 |   84350   21468  1245486    58.0 |  2.593 % |
c |     81739 |  190122   445817 |   92785   21809  1271020    58.3 |  2.593 % |
c |     82247 |  190122   445817 |  102064   22317  1310224    58.7 |  2.593 % |
c |     83007 |  190122   445817 |  112270   23077  1358767    58.9 |  2.593 % |
c |     84146 |  190122   445817 |  123497   24216  1430249    59.1 |  2.593 % |
c |     85854 |  190122   445817 |  135847   25924  1605179    61.9 |  2.593 % |
c ==============================================================================
c Found solution: 3059840
c ---[   0]---> Sorter-cost:   11     Base: 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 |     86384 |  190155   445901 |   63385   26454  1655034    62.6 |  2.593 % |
c |     86484 |  190155   445901 |   69723   26554  1660764    62.5 |  2.593 % |
c |     86636 |  190155   445901 |   76695   26706  1670505    62.6 |  2.593 % |
c |     86863 |  190155   445901 |   84365   26933  1691632    62.8 |  2.593 % |
c |     87200 |  190155   445901 |   92801   27270  1713092    62.8 |  2.593 % |
c |     87711 |  190148   445886 |  102082   27780  1742338    62.7 |  2.596 % |
c |     88471 |  190148   445886 |  112290   28540  1794240    62.9 |  2.596 % |
c |     89614 |  190148   445886 |  123519   29683  1899441    64.0 |  2.596 % |
c |     91323 |  190148   445886 |  135871   31392  2052966    65.4 |  2.596 % |
c |     93886 |  190148   445886 |  149458   33955  2331342    68.7 |  2.596 % |
c |     97731 |  190148   445886 |  164404   37800  2635628    69.7 |  2.596 % |
c |    103499 |  190042   445647 |  180844   43566  3104488    71.3 |  2.640 % |
c ==============================================================================
c Found solution: 3058432
c ---[   0]---> Sorter-cost:    9     Base: 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 |    104294 |  190008   445577 |   63336   44357  3167623    71.4 |  2.640 % |
c |    104398 |  190008   445577 |   69669   44461  3169160    71.3 |  2.660 % |
c |    104548 |  190008   445577 |   76636   44611  3171196    71.1 |  2.660 % |
c |    104774 |  190008   445577 |   84300   44837  3199431    71.4 |  2.660 % |
c |    105111 |  190008   445577 |   92730   45174  3234046    71.6 |  2.660 % |
c |    105617 |  190008   445577 |  102003   45680  3273663    71.7 |  2.660 % |
c |    106376 |  190008   445577 |  112203   46439  3351421    72.2 |  2.660 % |
c |    107516 |  190008   445577 |  123423   47579  3467405    72.9 |  2.660 % |
c |    109224 |  190008   445577 |  135766   49287  3626707    73.6 |  2.660 % |
c |    111787 |  190008   445577 |  149342   51850  3823598    73.7 |  2.660 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 X15_bit0 X15_bit1 X15_bit2 X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 X16_bit0 -X16_bit1 X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_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/28460/stat): 28460 (minisat+_script) R 28459 28460 31027 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855847240 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/28460/statm): 174 3 169 147 0 27 0
[pid=28460] 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=28461
New process pid=28462
New process pid=28463
execve syscall for /bin/sed executable
One traced child (pid=28462) 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=28463) exited with status: 0
One traced child (pid=28461) exited with status: 0
New process pid=28464
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-gr4x6.opb

[startup+10.0043 s]
Raw data (loadavg): 0.93 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 5681 0 0 0 953 22 0 0 25 0 1 0 1855847245 27901952 5509 4294967295 134512640 135094434 3221224432 3221223024 134557369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 6812 5509 145 145 0 6667 0
[pid=28464] vsize: 27248
Current children cumulated CPU time (s) 9.76
Current children cumulated vsize (Kb) 29372

[startup+20.0063 s]
Raw data (loadavg): 0.94 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 5977 0 0 0 1949 24 0 0 25 0 1 0 1855847245 29425664 5805 4294967295 134512640 135094434 3221224432 3221220672 134676317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 7184 5805 145 145 0 7039 0
[pid=28464] vsize: 28736
Current children cumulated CPU time (s) 19.74
Current children cumulated vsize (Kb) 30860

[startup+30.0082 s]
Raw data (loadavg): 0.95 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 5983 0 0 0 2949 25 0 0 25 0 1 0 1855847245 29425664 5811 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 7184 5811 145 145 0 7039 0
[pid=28464] vsize: 28736
Current children cumulated CPU time (s) 29.75
Current children cumulated vsize (Kb) 30860

[startup+40.0101 s]
Raw data (loadavg): 0.96 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 6037 0 0 0 3947 25 0 0 25 0 1 0 1855847245 29646848 5865 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 7238 5865 145 145 0 7093 0
[pid=28464] vsize: 28952
Current children cumulated CPU time (s) 39.73
Current children cumulated vsize (Kb) 31076

[startup+50.0111 s]
Raw data (loadavg): 0.96 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 6161 0 0 0 4945 27 0 0 25 0 1 0 1855847245 30179328 5989 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 7368 5989 145 145 0 7223 0
[pid=28464] vsize: 29472
Current children cumulated CPU time (s) 49.73
Current children cumulated vsize (Kb) 31596

[startup+60.012 s]
Raw data (loadavg): 0.97 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 6318 0 0 0 5941 30 0 0 25 0 1 0 1855847245 30806016 6146 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 7521 6146 145 145 0 7376 0
[pid=28464] vsize: 30084
Current children cumulated CPU time (s) 59.72
Current children cumulated vsize (Kb) 32208

[startup+70.0129 s]
Raw data (loadavg): 0.97 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 6464 0 0 0 6937 31 0 0 25 0 1 0 1855847245 31399936 6292 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 7666 6292 145 145 0 7521 0
[pid=28464] vsize: 30664
Current children cumulated CPU time (s) 69.69
Current children cumulated vsize (Kb) 32788

[startup+80.0148 s]
Raw data (loadavg): 0.98 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 6663 0 0 0 7936 32 0 0 25 0 1 0 1855847245 32067584 6459 4294967295 134512640 135094434 3221224432 3221221628 134600233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 7829 6459 145 145 0 7684 0
[pid=28464] vsize: 31316
Current children cumulated CPU time (s) 79.69
Current children cumulated vsize (Kb) 33440

[startup+90.0157 s]
Raw data (loadavg): 0.98 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 6720 0 0 0 8936 32 0 0 25 0 1 0 1855847245 32264192 6516 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 7877 6516 145 145 0 7732 0
[pid=28464] vsize: 31508
Current children cumulated CPU time (s) 89.69
Current children cumulated vsize (Kb) 33632

[startup+100.017 s]
Raw data (loadavg): 0.98 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 6838 0 0 0 9935 33 0 0 25 0 1 0 1855847245 32747520 6634 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 7995 6634 145 145 0 7850 0
[pid=28464] vsize: 31980
Current children cumulated CPU time (s) 99.69
Current children cumulated vsize (Kb) 34104

[startup+110.018 s]
Raw data (loadavg): 0.98 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 7115 0 0 0 10931 35 0 0 25 0 1 0 1855847245 33751040 6869 4294967295 134512640 135094434 3221224432 3221221632 134677320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 8240 6869 145 145 0 8095 0
[pid=28464] vsize: 32960
Current children cumulated CPU time (s) 109.67
Current children cumulated vsize (Kb) 35084

[startup+120.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 7164 0 0 0 11930 35 0 0 25 0 1 0 1855847245 33947648 6918 4294967295 134512640 135094434 3221224432 3221223120 134554736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 8288 6918 145 145 0 8143 0
[pid=28464] vsize: 33152
Current children cumulated CPU time (s) 119.66
Current children cumulated vsize (Kb) 35276

[startup+130.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 7246 0 0 0 12929 36 0 0 25 0 1 0 1855847245 34283520 7000 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 8370 7000 145 145 0 8225 0
[pid=28464] vsize: 33480
Current children cumulated CPU time (s) 129.66
Current children cumulated vsize (Kb) 35604

[startup+140.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 7350 0 0 0 13927 37 0 0 25 0 1 0 1855847245 34709504 7104 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 8474 7104 145 145 0 8329 0
[pid=28464] vsize: 33896
Current children cumulated CPU time (s) 139.65
Current children cumulated vsize (Kb) 36020

[startup+150.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 7421 0 0 0 14925 37 0 0 25 0 1 0 1855847245 35000320 7175 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 8545 7175 145 145 0 8400 0
[pid=28464] vsize: 34180
Current children cumulated CPU time (s) 149.63
Current children cumulated vsize (Kb) 36304

[startup+160.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 7531 0 0 0 15924 38 0 0 25 0 1 0 1855847245 35454976 7285 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 8656 7285 145 145 0 8511 0
[pid=28464] vsize: 34624
Current children cumulated CPU time (s) 159.63
Current children cumulated vsize (Kb) 36748

[startup+170.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 7713 0 0 0 16922 39 0 0 25 0 1 0 1855847245 35876864 7394 4294967295 134512640 135094434 3221224432 3221221104 134676480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 8759 7394 145 145 0 8614 0
[pid=28464] vsize: 35036
Current children cumulated CPU time (s) 169.62
Current children cumulated vsize (Kb) 37160

[startup+180.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 7747 0 0 0 17921 39 0 0 25 0 1 0 1855847245 36016128 7428 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 8793 7428 145 145 0 8648 0
[pid=28464] vsize: 35172
Current children cumulated CPU time (s) 179.61
Current children cumulated vsize (Kb) 37296

[startup+190.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 7914 0 0 0 18919 41 0 0 25 0 1 0 1855847245 36691968 7595 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 8958 7595 145 145 0 8813 0
[pid=28464] vsize: 35832
Current children cumulated CPU time (s) 189.61
Current children cumulated vsize (Kb) 37956

[startup+200.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 8037 0 0 0 19917 42 0 0 25 0 1 0 1855847245 37195776 7718 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 9081 7718 145 145 0 8936 0
[pid=28464] vsize: 36324
Current children cumulated CPU time (s) 199.6
Current children cumulated vsize (Kb) 38448

[startup+210.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 8112 0 0 0 20916 42 0 0 25 0 1 0 1855847245 37502976 7793 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 9156 7793 145 145 0 9011 0
[pid=28464] vsize: 36624
Current children cumulated CPU time (s) 209.59
Current children cumulated vsize (Kb) 38748

[startup+220.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 8254 0 0 0 21914 44 0 0 25 0 1 0 1855847245 38195200 7935 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 9325 7935 145 145 0 9180 0
[pid=28464] vsize: 37300
Current children cumulated CPU time (s) 219.59
Current children cumulated vsize (Kb) 39424

[startup+230.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 8305 0 0 0 22914 44 0 0 25 0 1 0 1855847245 38383616 7986 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 9371 7986 145 145 0 9226 0
[pid=28464] vsize: 37484
Current children cumulated CPU time (s) 229.59
Current children cumulated vsize (Kb) 39608

[startup+240.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 8423 0 0 0 23913 45 0 0 25 0 1 0 1855847245 38866944 8104 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 9489 8104 145 145 0 9344 0
[pid=28464] vsize: 37956
Current children cumulated CPU time (s) 239.59
Current children cumulated vsize (Kb) 40080

[startup+250.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 8449 0 0 0 24913 45 0 0 25 0 1 0 1855847245 38973440 8130 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 9515 8130 145 145 0 9370 0
[pid=28464] vsize: 38060
Current children cumulated CPU time (s) 249.59
Current children cumulated vsize (Kb) 40184

[startup+260.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 8566 0 0 0 25912 45 0 0 25 0 1 0 1855847245 39321600 8215 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 9600 8215 145 145 0 9455 0
[pid=28464] vsize: 38400
Current children cumulated CPU time (s) 259.58
Current children cumulated vsize (Kb) 40524

[startup+270.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 8686 0 0 0 26911 46 0 0 25 0 1 0 1855847245 39940096 8335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 9751 8335 145 145 0 9606 0
[pid=28464] vsize: 39004
Current children cumulated CPU time (s) 269.58
Current children cumulated vsize (Kb) 41128

[startup+280.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 8790 0 0 0 27908 47 0 0 25 0 1 0 1855847245 40366080 8439 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 9855 8439 145 145 0 9710 0
[pid=28464] vsize: 39420
Current children cumulated CPU time (s) 279.56
Current children cumulated vsize (Kb) 41544

[startup+290.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 8882 0 0 0 28907 48 0 0 25 0 1 0 1855847245 40734720 8531 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 9945 8531 145 145 0 9800 0
[pid=28464] vsize: 39780
Current children cumulated CPU time (s) 289.56
Current children cumulated vsize (Kb) 41904

[startup+300.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 8990 0 0 0 29905 49 0 0 25 0 1 0 1855847245 41172992 8639 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 10052 8639 145 145 0 9907 0
[pid=28464] vsize: 40208
Current children cumulated CPU time (s) 299.55
Current children cumulated vsize (Kb) 42332

[startup+310.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 9138 0 0 0 30903 50 0 0 25 0 1 0 1855847245 41771008 8787 4294967295 134512640 135094434 3221224432 3221223056 134557734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 10198 8787 145 145 0 10053 0
[pid=28464] vsize: 40792
Current children cumulated CPU time (s) 309.54
Current children cumulated vsize (Kb) 42916

[startup+320.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 9247 0 0 0 31901 50 0 0 25 0 1 0 1855847245 42217472 8896 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 10307 8896 145 145 0 10162 0
[pid=28464] vsize: 41228
Current children cumulated CPU time (s) 319.52
Current children cumulated vsize (Kb) 43352

[startup+330.039 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 9363 0 0 0 32900 51 0 0 25 0 1 0 1855847245 42688512 9012 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 10422 9012 145 145 0 10277 0
[pid=28464] vsize: 41688
Current children cumulated CPU time (s) 329.52
Current children cumulated vsize (Kb) 43812

[startup+340.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 9465 0 0 0 33899 51 0 0 25 0 1 0 1855847245 43102208 9114 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 10523 9114 145 145 0 10378 0
[pid=28464] vsize: 42092
Current children cumulated CPU time (s) 339.51
Current children cumulated vsize (Kb) 44216

[startup+350.042 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 9567 0 0 0 34898 51 0 0 25 0 1 0 1855847245 43515904 9216 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 10624 9216 145 145 0 10479 0
[pid=28464] vsize: 42496
Current children cumulated CPU time (s) 349.5
Current children cumulated vsize (Kb) 44620

[startup+360.043 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 9664 0 0 0 35897 52 0 0 25 0 1 0 1855847245 43909120 9313 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 10720 9313 145 145 0 10575 0
[pid=28464] vsize: 42880
Current children cumulated CPU time (s) 359.5
Current children cumulated vsize (Kb) 45004

[startup+370.044 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 9763 0 0 0 36895 53 0 0 25 0 1 0 1855847245 44306432 9412 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 10817 9412 145 145 0 10672 0
[pid=28464] vsize: 43268
Current children cumulated CPU time (s) 369.49
Current children cumulated vsize (Kb) 45392

[startup+380.046 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 9880 0 0 0 37892 54 0 0 25 0 1 0 1855847245 44781568 9529 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 10933 9529 145 145 0 10788 0
[pid=28464] vsize: 43732
Current children cumulated CPU time (s) 379.47
Current children cumulated vsize (Kb) 45856

[startup+390.047 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 10000 0 0 0 38891 55 0 0 25 0 1 0 1855847245 45268992 9649 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 11052 9649 145 145 0 10907 0
[pid=28464] vsize: 44208
Current children cumulated CPU time (s) 389.47
Current children cumulated vsize (Kb) 46332

[startup+400.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 10094 0 0 0 39889 56 0 0 25 0 1 0 1855847245 45649920 9743 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 11145 9743 145 145 0 11000 0
[pid=28464] vsize: 44580
Current children cumulated CPU time (s) 399.46
Current children cumulated vsize (Kb) 46704

[startup+410.048 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 10179 0 0 0 40888 57 0 0 25 0 1 0 1855847245 45993984 9828 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 11229 9828 145 145 0 11084 0
[pid=28464] vsize: 44916
Current children cumulated CPU time (s) 409.46
Current children cumulated vsize (Kb) 47040

[startup+420.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 10259 0 0 0 41886 57 0 0 25 0 1 0 1855847245 46317568 9908 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 11308 9908 145 145 0 11163 0
[pid=28464] vsize: 45232
Current children cumulated CPU time (s) 419.44
Current children cumulated vsize (Kb) 47356

[startup+430.05 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 10349 0 0 0 42885 58 0 0 25 0 1 0 1855847245 46682112 9998 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 11397 9998 145 145 0 11252 0
[pid=28464] vsize: 45588
Current children cumulated CPU time (s) 429.44
Current children cumulated vsize (Kb) 47712

[startup+440.051 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 10442 0 0 0 43883 59 0 0 25 0 1 0 1855847245 47058944 10091 4294967295 134512640 135094434 3221224432 3221223088 134558392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 11489 10091 145 145 0 11344 0
[pid=28464] vsize: 45956
Current children cumulated CPU time (s) 439.43
Current children cumulated vsize (Kb) 48080

[startup+450.052 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 10524 0 0 0 44883 59 0 0 25 0 1 0 1855847245 47394816 10173 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 11571 10173 145 145 0 11426 0
[pid=28464] vsize: 46284
Current children cumulated CPU time (s) 449.43
Current children cumulated vsize (Kb) 48408

[startup+460.053 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 10632 0 0 0 45881 60 0 0 25 0 1 0 1855847245 47841280 10281 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 11680 10281 145 145 0 11535 0
[pid=28464] vsize: 46720
Current children cumulated CPU time (s) 459.42
Current children cumulated vsize (Kb) 48844

[startup+470.054 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 10714 0 0 0 46880 61 0 0 25 0 1 0 1855847245 48164864 10363 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 11759 10363 145 145 0 11614 0
[pid=28464] vsize: 47036
Current children cumulated CPU time (s) 469.42
Current children cumulated vsize (Kb) 49160

[startup+480.056 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 10800 0 0 0 47879 61 0 0 25 0 1 0 1855847245 48517120 10449 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 11845 10449 145 145 0 11700 0
[pid=28464] vsize: 47380
Current children cumulated CPU time (s) 479.41
Current children cumulated vsize (Kb) 49504

[startup+490.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 10902 0 0 0 48878 62 0 0 25 0 1 0 1855847245 48930816 10551 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 11946 10551 145 145 0 11801 0
[pid=28464] vsize: 47784
Current children cumulated CPU time (s) 489.41
Current children cumulated vsize (Kb) 49908

[startup+500.057 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 11021 0 0 0 49877 62 0 0 25 0 1 0 1855847245 49422336 10670 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 12066 10670 145 145 0 11921 0
[pid=28464] vsize: 48264
Current children cumulated CPU time (s) 499.4
Current children cumulated vsize (Kb) 50388

[startup+510.059 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 11122 0 0 0 50876 63 0 0 25 0 1 0 1855847245 49827840 10771 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 12165 10771 145 145 0 12020 0
[pid=28464] vsize: 48660
Current children cumulated CPU time (s) 509.4
Current children cumulated vsize (Kb) 50784

[startup+520.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 11186 0 0 0 51875 63 0 0 25 0 1 0 1855847245 50085888 10835 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 12228 10835 145 145 0 12083 0
[pid=28464] vsize: 48912
Current children cumulated CPU time (s) 519.39
Current children cumulated vsize (Kb) 51036

[startup+530.061 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 11289 0 0 0 52874 64 0 0 25 0 1 0 1855847245 50503680 10938 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 12330 10938 145 145 0 12185 0
[pid=28464] vsize: 49320
Current children cumulated CPU time (s) 529.39
Current children cumulated vsize (Kb) 51444

[startup+540.063 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 11387 0 0 0 53873 65 0 0 25 0 1 0 1855847245 50900992 11036 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 12427 11036 145 145 0 12282 0
[pid=28464] vsize: 49708
Current children cumulated CPU time (s) 539.39
Current children cumulated vsize (Kb) 51832

[startup+550.063 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 11484 0 0 0 54871 66 0 0 25 0 1 0 1855847245 51298304 11133 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 12524 11133 145 145 0 12379 0
[pid=28464] vsize: 50096
Current children cumulated CPU time (s) 549.38
Current children cumulated vsize (Kb) 52220

[startup+560.064 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 11553 0 0 0 55871 66 0 0 25 0 1 0 1855847245 51576832 11202 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 12592 11202 145 145 0 12447 0
[pid=28464] vsize: 50368
Current children cumulated CPU time (s) 559.38
Current children cumulated vsize (Kb) 52492

[startup+570.066 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 11642 0 0 0 56869 67 0 0 25 0 1 0 1855847245 51937280 11291 4294967295 134512640 135094434 3221224432 3221223088 134557856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 12680 11291 145 145 0 12535 0
[pid=28464] vsize: 50720
Current children cumulated CPU time (s) 569.37
Current children cumulated vsize (Kb) 52844

[startup+580.067 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 11733 0 0 0 57868 69 0 0 25 0 1 0 1855847245 52310016 11382 4294967295 134512640 135094434 3221224432 3221223056 134557616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 12771 11382 145 145 0 12626 0
[pid=28464] vsize: 51084
Current children cumulated CPU time (s) 579.38
Current children cumulated vsize (Kb) 53208

[startup+590.068 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 11799 0 0 0 58866 70 0 0 25 0 1 0 1855847245 52576256 11448 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 12836 11448 145 145 0 12691 0
[pid=28464] vsize: 51344
Current children cumulated CPU time (s) 589.37
Current children cumulated vsize (Kb) 53468

[startup+600.07 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 11875 0 0 0 59863 72 0 0 25 0 1 0 1855847245 52883456 11524 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 12911 11524 145 145 0 12766 0
[pid=28464] vsize: 51644
Current children cumulated CPU time (s) 599.36
Current children cumulated vsize (Kb) 53768

[startup+610.071 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 11933 0 0 0 60861 73 0 0 25 0 1 0 1855847245 53116928 11582 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 12968 11582 145 145 0 12823 0
[pid=28464] vsize: 51872
Current children cumulated CPU time (s) 609.35
Current children cumulated vsize (Kb) 53996

[startup+620.072 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12015 0 0 0 61859 75 0 0 25 0 1 0 1855847245 53452800 11664 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 13050 11664 145 145 0 12905 0
[pid=28464] vsize: 52200
Current children cumulated CPU time (s) 619.35
Current children cumulated vsize (Kb) 54324

[startup+630.074 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12084 0 0 0 62857 76 0 0 25 0 1 0 1855847245 53735424 11733 4294967295 134512640 135094434 3221224432 3221223104 134556450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 13119 11733 145 145 0 12974 0
[pid=28464] vsize: 52476
Current children cumulated CPU time (s) 629.34
Current children cumulated vsize (Kb) 54600

[startup+640.075 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12156 0 0 0 63855 77 0 0 25 0 1 0 1855847245 54292480 11805 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 13255 11805 145 145 0 13110 0
[pid=28464] vsize: 53020
Current children cumulated CPU time (s) 639.33
Current children cumulated vsize (Kb) 55144

[startup+650.076 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12229 0 0 0 64853 78 0 0 25 0 1 0 1855847245 54587392 11878 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 13327 11878 145 145 0 13182 0
[pid=28464] vsize: 53308
Current children cumulated CPU time (s) 649.32
Current children cumulated vsize (Kb) 55432

[startup+660.078 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12302 0 0 0 65851 79 0 0 25 0 1 0 1855847245 54878208 11951 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 13398 11951 145 145 0 13253 0
[pid=28464] vsize: 53592
Current children cumulated CPU time (s) 659.31
Current children cumulated vsize (Kb) 55716

[startup+670.079 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12376 0 0 0 66850 80 0 0 25 0 1 0 1855847245 55181312 12025 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 13472 12025 145 145 0 13327 0
[pid=28464] vsize: 53888
Current children cumulated CPU time (s) 669.31
Current children cumulated vsize (Kb) 56012

[startup+680.08 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12441 0 0 0 67847 82 0 0 25 0 1 0 1855847245 55447552 12090 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 13537 12090 145 145 0 13392 0
[pid=28464] vsize: 54148
Current children cumulated CPU time (s) 679.3
Current children cumulated vsize (Kb) 56272

[startup+690.081 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12527 0 0 0 68846 83 0 0 25 0 1 0 1855847245 55795712 12176 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 13622 12176 145 145 0 13477 0
[pid=28464] vsize: 54488
Current children cumulated CPU time (s) 689.3
Current children cumulated vsize (Kb) 56612

[startup+700.081 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12593 0 0 0 69844 83 0 0 25 0 1 0 1855847245 56066048 12242 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 13688 12242 145 145 0 13543 0
[pid=28464] vsize: 54752
Current children cumulated CPU time (s) 699.28
Current children cumulated vsize (Kb) 56876

[startup+710.082 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12664 0 0 0 70844 83 0 0 25 0 1 0 1855847245 56352768 12313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 13758 12313 145 145 0 13613 0
[pid=28464] vsize: 55032
Current children cumulated CPU time (s) 709.28
Current children cumulated vsize (Kb) 57156

[startup+720.083 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12731 0 0 0 71843 84 0 0 25 0 1 0 1855847245 56623104 12380 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 13824 12380 145 145 0 13679 0
[pid=28464] vsize: 55296
Current children cumulated CPU time (s) 719.28
Current children cumulated vsize (Kb) 57420

[startup+730.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12800 0 0 0 72843 84 0 0 25 0 1 0 1855847245 56905728 12449 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 13893 12449 145 145 0 13748 0
[pid=28464] vsize: 55572
Current children cumulated CPU time (s) 729.28
Current children cumulated vsize (Kb) 57696

[startup+740.086 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12865 0 0 0 73842 85 0 0 25 0 1 0 1855847245 57167872 12514 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 13957 12514 145 145 0 13812 0
[pid=28464] vsize: 55828
Current children cumulated CPU time (s) 739.28
Current children cumulated vsize (Kb) 57952

[startup+750.087 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 12939 0 0 0 74840 85 0 0 25 0 1 0 1855847245 57466880 12588 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14030 12588 145 145 0 13885 0
[pid=28464] vsize: 56120
Current children cumulated CPU time (s) 749.26
Current children cumulated vsize (Kb) 58244

[startup+760.088 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13017 0 0 0 75840 86 0 0 25 0 1 0 1855847245 57786368 12666 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14108 12666 145 145 0 13963 0
[pid=28464] vsize: 56432
Current children cumulated CPU time (s) 759.27
Current children cumulated vsize (Kb) 58556

[startup+770.089 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13106 0 0 0 76838 86 0 0 25 0 1 0 1855847245 58159104 12755 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14199 12755 145 145 0 14054 0
[pid=28464] vsize: 56796
Current children cumulated CPU time (s) 769.25
Current children cumulated vsize (Kb) 58920

[startup+780.091 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13174 0 0 0 77838 86 0 0 25 0 1 0 1855847245 58433536 12823 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14266 12823 145 145 0 14121 0
[pid=28464] vsize: 57064
Current children cumulated CPU time (s) 779.25
Current children cumulated vsize (Kb) 59188

[startup+790.092 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13250 0 0 0 78837 87 0 0 25 0 1 0 1855847245 58744832 12899 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14342 12899 145 145 0 14197 0
[pid=28464] vsize: 57368
Current children cumulated CPU time (s) 789.25
Current children cumulated vsize (Kb) 59492

[startup+800.093 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13313 0 0 0 79836 88 0 0 25 0 1 0 1855847245 58994688 12962 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14403 12962 145 145 0 14258 0
[pid=28464] vsize: 57612
Current children cumulated CPU time (s) 799.25
Current children cumulated vsize (Kb) 59736

[startup+810.094 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13368 0 0 0 80836 88 0 0 25 0 1 0 1855847245 59224064 13017 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14459 13017 145 145 0 14314 0
[pid=28464] vsize: 57836
Current children cumulated CPU time (s) 809.25
Current children cumulated vsize (Kb) 59960

[startup+820.095 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13456 0 0 0 81834 89 0 0 25 0 1 0 1855847245 59576320 13105 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14545 13105 145 145 0 14400 0
[pid=28464] vsize: 58180
Current children cumulated CPU time (s) 819.24
Current children cumulated vsize (Kb) 60304

[startup+830.096 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13525 0 0 0 82834 90 0 0 25 0 1 0 1855847245 59858944 13174 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14614 13174 145 145 0 14469 0
[pid=28464] vsize: 58456
Current children cumulated CPU time (s) 829.25
Current children cumulated vsize (Kb) 60580

[startup+840.097 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13614 0 0 0 83833 90 0 0 25 0 1 0 1855847245 60088320 13231 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28464/statm): 14670 13231 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 839.24
Current children cumulated vsize (Kb) 60804

[startup+850.098 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13614 0 0 0 84833 90 0 0 25 0 1 0 1855847245 60088320 13231 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13231 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 849.24
Current children cumulated vsize (Kb) 60804

[startup+860.099 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13614 0 0 0 85833 90 0 0 25 0 1 0 1855847245 60088320 13231 4294967295 134512640 135094434 3221224432 3221223024 134556987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13231 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 859.24
Current children cumulated vsize (Kb) 60804

[startup+870.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13614 0 0 0 86833 90 0 0 25 0 1 0 1855847245 60088320 13231 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13231 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 869.24
Current children cumulated vsize (Kb) 60804

[startup+880.101 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13614 0 0 0 87833 90 0 0 25 0 1 0 1855847245 60088320 13231 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13231 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 879.24
Current children cumulated vsize (Kb) 60804

[startup+890.102 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13614 0 0 0 88833 90 0 0 25 0 1 0 1855847245 60088320 13231 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13231 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 889.24
Current children cumulated vsize (Kb) 60804

[startup+900.103 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13614 0 0 0 89834 90 0 0 25 0 1 0 1855847245 60088320 13231 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13231 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 899.25
Current children cumulated vsize (Kb) 60804

[startup+910.104 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13614 0 0 0 90834 90 0 0 25 0 1 0 1855847245 60088320 13231 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13231 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 909.25
Current children cumulated vsize (Kb) 60804

[startup+920.105 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13614 0 0 0 91834 90 0 0 25 0 1 0 1855847245 60088320 13231 4294967295 134512640 135094434 3221224432 3221223056 134557724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13231 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 919.25
Current children cumulated vsize (Kb) 60804

[startup+930.106 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13614 0 0 0 92834 90 0 0 25 0 1 0 1855847245 60088320 13231 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13231 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 929.25
Current children cumulated vsize (Kb) 60804

[startup+940.107 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 93835 90 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 939.26
Current children cumulated vsize (Kb) 60804

[startup+950.108 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 94835 90 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 949.26
Current children cumulated vsize (Kb) 60804

[startup+960.109 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 95835 90 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 959.26
Current children cumulated vsize (Kb) 60804

[startup+970.11 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 96835 90 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 969.26
Current children cumulated vsize (Kb) 60804

[startup+980.111 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 97836 90 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 979.27
Current children cumulated vsize (Kb) 60804

[startup+990.111 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 98836 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 989.28
Current children cumulated vsize (Kb) 60804

[startup+1000.11 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 99836 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 999.28
Current children cumulated vsize (Kb) 60804

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 100836 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1009.28
Current children cumulated vsize (Kb) 60804

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 101836 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1019.28
Current children cumulated vsize (Kb) 60804

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 102837 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1029.29
Current children cumulated vsize (Kb) 60804

[startup+1040.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 103837 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1039.29
Current children cumulated vsize (Kb) 60804

[startup+1050.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 104837 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1049.29
Current children cumulated vsize (Kb) 60804

[startup+1060.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 105837 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1059.29
Current children cumulated vsize (Kb) 60804

[startup+1070.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 106838 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1069.3
Current children cumulated vsize (Kb) 60804

[startup+1080.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 107838 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1079.3
Current children cumulated vsize (Kb) 60804

[startup+1090.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 108838 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1089.3
Current children cumulated vsize (Kb) 60804

[startup+1100.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 109838 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1099.3
Current children cumulated vsize (Kb) 60804

[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 110838 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221221520 134677086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1109.3
Current children cumulated vsize (Kb) 60804

[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 111838 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1119.3
Current children cumulated vsize (Kb) 60804

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 112839 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1129.31
Current children cumulated vsize (Kb) 60804

[startup+1140.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 113839 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1139.31
Current children cumulated vsize (Kb) 60804

[startup+1150.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 114839 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1149.31
Current children cumulated vsize (Kb) 60804

[startup+1160.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 115839 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1159.31
Current children cumulated vsize (Kb) 60804

[startup+1170.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 116840 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1169.32
Current children cumulated vsize (Kb) 60804

[startup+1180.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 117840 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1179.32
Current children cumulated vsize (Kb) 60804

[startup+1190.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 118840 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1189.32
Current children cumulated vsize (Kb) 60804

[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 119840 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1199.32
Current children cumulated vsize (Kb) 60804

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 120840 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1209.32
Current children cumulated vsize (Kb) 60804



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/57 28464
Raw data (/proc/28460/stat): 28460 (minisat+_script) S 28459 28460 31027 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855847240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28460/statm): 531 226 485 147 0 384 0
[pid=28460] vsize: 2124
Raw data (/proc/28464/stat): 28464 (minisat+_64-bit) R 28460 28460 31027 0 -1 0 13615 0 0 0 120840 91 0 0 25 0 1 0 1855847245 60088320 13232 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28464/statm): 14670 13232 145 145 0 14525 0
[pid=28464] vsize: 58680
Current children cumulated CPU time (s) 1209.32
Current children cumulated vsize (Kb) 60804

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

Child status: 10
Real time (s): 1210.17
CPU time (s): 1209.35
CPU user time (s): 1208.41
CPU system time (s): 0.942856
CPU usage (%): 99.9329
Max. virtual memory (cumulated for all children) (Kb): 60804

Verifier Data

ERROR: no interpretation found !