Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Nameweb/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.5:100.opb
MD5SUMdd81121db7c1c4b8597dd9571c707a87
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 3
Optimality of the best value was proved YES
Number of terms in the objective function 372
Biggest coefficient in the objective function 220
Number of bits for the biggest coefficient in the objective function 8
Sum of the numbers in the objective function 983
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 220
Number of bits of the biggest number in a constraint 8
Biggest sum of numbers in a constraint 983
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark19.3841
Number of variables372
Total number of constraints792
Number of constraints which are clauses345
Number of constraints which are cardinality constraints (but not clauses)447
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint18

Trace number 2354

Launcher Data

LAUNCH ON wulflinc27 THE 2005-09-18 19:09:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2736 boxname=wulflinc27 idbench=392 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  dd81121db7c1c4b8597dd9571c707a87  /oldhome/oroussel/tmp/wulflinc27/normalized-10:10:4.5:0.5:100.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-10:10:4.5:0.5:100.opb
IDLAUNCH: 2736
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        910912 kB
Buffers:         36040 kB
Cached:          55608 kB
SwapCached:        764 kB
Active:          66908 kB
Inactive:        27388 kB
HighTotal:      131008 kB
HighFree:        72828 kB
LowTotal:       903652 kB
LowFree:        838084 kB
SwapTotal:     2097892 kB
SwapFree:      2096616 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5724 kB
Slab:            23912 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:29:38 (client local time) WITH STATUS 10 IN 1208.63 SECONDS
stats: 2736 7 1208.63 10

Solver Data

c Parsing PB file...
c Converting 420 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   29
c ---[  82]---> BDD-cost:   35
c ---[  81]---> BDD-cost:   35
c ---[  80]---> BDD-cost:   32
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost:   26
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   20
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   32
c ---[  72]---> BDD-cost:   35
c ---[  71]---> BDD-cost:   35
c ---[  70]---> BDD-cost:   32
c ---[  69]---> BDD-cost:   35
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   23
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   38
c ---[  61]---> BDD-cost:   44
c ---[  60]---> BDD-cost:   35
c ---[  59]---> BDD-cost:   38
c ---[  58]---> BDD-cost:   32
c ---[  57]---> BDD-cost:   26
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   32
c ---[  52]---> BDD-cost:   44
c ---[  51]---> BDD-cost:   47
c ---[  50]---> BDD-cost:   41
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:   29
c ---[  47]---> BDD-cost:   21
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   21
c ---[  42]---> BDD-cost:   38
c ---[  41]---> BDD-cost:   32
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   20
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   26
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:    7
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    8
c ---[  23]---> BDD-cost:   11
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:    7
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    5
c ---[  13]---> BDD-cost:    8
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:    7
c ---[   7]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4084    11649 |    1361       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 355
c ---[   0]---> Sorter-cost:20800     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   39610    94771 |   13203       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 119
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        52 |   40635    97290 |   13545      47      509    10.8 |  0.000 % |
c |       153 |   40635    97290 |   14899     148     2006    13.6 |  0.807 % |
c |       303 |   40635    97290 |   16389     298     3680    12.3 |  0.807 % |
c ==============================================================================
c Found solution: 93
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       335 |   40816    97778 |   13605     330     3969    12.0 |  0.807 % |
c ==============================================================================
c Found solution: 74
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       381 |   40957    98168 |   13652     376     4254    11.3 |  0.807 % |
c |       482 |   40957    98168 |   15017     477     6680    14.0 |  0.809 % |
c ==============================================================================
c Found solution: 66
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       543 |   41021    98358 |   13673     538     7309    13.6 |  0.809 % |
c |       643 |   41007    98330 |   15040     637     8156    12.8 |  0.847 % |
c ==============================================================================
c Found solution: 39
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       741 |   41137    98688 |   13712     735    12723    17.3 |  0.847 % |
c |       841 |   41137    98688 |   15083     835    14812    17.7 |  0.858 % |
c |       991 |   41137    98688 |   16591     985    15900    16.1 |  0.858 % |
c |      1216 |   41137    98688 |   18250    1210    24830    20.5 |  0.858 % |
c ==============================================================================
c Found solution: 32
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1549 |   40826    98032 |   13608    1526    31796    20.8 |  0.858 % |
c |      1649 |   40807    97993 |   14968    1625    32748    20.2 |  1.610 % |
c |      1799 |   40807    97993 |   16465    1775    35020    19.7 |  1.610 % |
c |      2024 |   40807    97993 |   18112    2000    57066    28.5 |  1.610 % |
c |      2361 |   40157    96519 |   19923    2253    61245    27.2 |  2.962 % |
c |      2870 |   40157    96519 |   21915    2762    71091    25.7 |  2.962 % |
c |      3629 |   40157    96519 |   24107    3521    86728    24.6 |  2.962 % |
c |      4768 |   40069    96331 |   26518    4641   109000    23.5 |  3.209 % |
c |      6476 |   39881    95923 |   29169    6320   241528    38.2 |  3.710 % |
c |      9040 |   39881    95923 |   32086    8884   558335    62.8 |  3.710 % |
c |     12886 |   39881    95923 |   35295   12730   837536    65.8 |  3.710 % |
c |     18654 |   39881    95923 |   38825   18498  1338946    72.4 |  3.710 % |
c |     27303 |   39881    95923 |   42707   27147  2479319    91.3 |  3.710 % |
c ==============================================================================
c Found solution: 31
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30230 |   39885    95933 |   13295   30074  2833854    94.2 |  3.710 % |
c |     30330 |   39885    95933 |   14624   13138  1476713   112.4 |  3.714 % |
c |     30481 |   39885    95933 |   16086   13289  1480028   111.4 |  3.714 % |
c |     30709 |   39885    95933 |   17695   13517  1485023   109.9 |  3.714 % |
c |     31046 |   39885    95933 |   19465   13854  1491450   107.7 |  3.714 % |
c |     31552 |   39885    95933 |   21411   14360  1526895   106.3 |  3.714 % |
c |     32311 |   39885    95933 |   23552   15119  1570893   103.9 |  3.714 % |
c |     33452 |   39885    95933 |   25908   16260  1620404    99.7 |  3.714 % |
c |     35160 |   39871    95901 |   28499   17966  1667556    92.8 |  3.734 % |
c |     37722 |   39871    95901 |   31348   20528  1922784    93.7 |  3.734 % |
c ==============================================================================
c Found solution: 30
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37876 |   39892    95963 |   13297   20682  1934151    93.5 |  3.734 % |
c |     37977 |   39838    95840 |   14626   10433   624856    59.9 |  3.810 % |
c |     38128 |   39838    95840 |   16089   10584   628193    59.4 |  3.810 % |
c |     38354 |   39838    95840 |   17698   10810   630346    58.3 |  3.810 % |
c |     38692 |   39838    95840 |   19468   11148   638017    57.2 |  3.810 % |
c |     39198 |   39838    95840 |   21414   11654   656390    56.3 |  3.810 % |
c |     39957 |   39820    95799 |   23556   12406   664944    53.6 |  3.835 % |
c ==============================================================================
c Found solution: 25
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40470 |   39846    95875 |   13282   12919   696562    53.9 |  3.835 % |
c |     40570 |   39846    95875 |   14610   13019   698367    53.6 |  3.837 % |
c |     40720 |   39846    95875 |   16071   13169   700531    53.2 |  3.837 % |
c |     40945 |   39846    95875 |   17678   13394   705284    52.7 |  3.837 % |
c |     41282 |   39739    95631 |   19446   13723   724893    52.8 |  4.074 % |
c |     41789 |   39739    95631 |   21390   14230   774776    54.4 |  4.074 % |
c |     42549 |   39721    95589 |   23529   14989   793085    52.9 |  4.129 % |
c |     43688 |   39721    95589 |   25882   16128   862249    53.5 |  4.129 % |
c |     45397 |   39721    95589 |   28471   17837   943295    52.9 |  4.129 % |
c |     47959 |   39721    95589 |   31318   20399  1340906    65.7 |  4.129 % |
c |     51803 |   39721    95589 |   34450   24243  1730566    71.4 |  4.129 % |
c ==============================================================================
c Found solution: 18
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53697 |   39759    95694 |   13253   26132  1833701    70.2 |  4.129 % |
c |     53798 |   39759    95694 |   14578   13167   983300    74.7 |  4.137 % |
c |     53948 |   39721    95606 |   16036   13310   984452    74.0 |  4.197 % |
c |     54173 |   39721    95606 |   17639   13535   995185    73.5 |  4.197 % |
c |     54510 |   39721    95606 |   19403   13872  1004647    72.4 |  4.197 % |
c ==============================================================================
c Found solution: 9
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54616 |   39766    95725 |   13255   13978  1006538    72.0 |  4.197 % |
c |     54716 |   39748    95684 |   14580   14071  1007232    71.6 |  4.220 % |
c |     54866 |   39748    95684 |   16038   14221  1012093    71.2 |  4.220 % |
c |     55091 |   39742    95670 |   17642   14443  1014604    70.2 |  4.230 % |
c |     55428 |   39738    95661 |   19406   14779  1023087    69.2 |  4.235 % |
c |     55934 |   39738    95661 |   21347   15285  1037095    67.9 |  4.235 % |
c |     56693 |   39738    95661 |   23482   16044  1092277    68.1 |  4.235 % |
c |     57832 |   39738    95661 |   25830   17183  1134775    66.0 |  4.235 % |
c |     59541 |   39738    95661 |   28413   18892  1247008    66.0 |  4.235 % |
c |     62103 |   39738    95661 |   31254   21454  1403165    65.4 |  4.235 % |
c |     65947 |   39738    95661 |   34380   25298  2020808    79.9 |  4.235 % |
c |     71714 |   39738    95661 |   37818   31065  2590932    83.4 |  4.235 % |
c |     80363 |   39738    95661 |   41599   39714  3547339    89.3 |  4.235 % |
c |     93337 |   39738    95661 |   45759   19456  2317262   119.1 |  4.235 % |
c |    112798 |   39738    95661 |   50335   38917  5379251   138.2 |  4.235 % |
c |    141992 |   39716    95612 |   55369   26150  3557617   136.0 |  4.270 % |
c |    185781 |   39640    95444 |   60906   27874  1990715    71.4 |  4.457 % |
c |    251466 |   39640    95444 |   66997   44447  9458461   212.8 |  4.457 % |

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/9877/stat): 9877 (minisat+_script) R 9876 9877 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843647058 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/9877/statm): 174 3 169 147 0 27 0
[pid=9877] 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=9878
New process pid=9879
New process pid=9880
execve syscall for /bin/sed executable
One traced child (pid=9879) 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=9880) exited with status: 0
One traced child (pid=9878) exited with status: 0
New process pid=9881
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-10:10:4.5:0.5:100.opb

[startup+10.0039 s]
Raw data (loadavg): 0.90 0.95 0.90 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 2087 0 0 0 978 9 0 0 25 0 1 0 1843647063 9379840 1987 4294967295 134512640 135094434 3221224432 3221223064 134562981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 2290 1987 145 145 0 2145 0
[pid=9881] vsize: 9160
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 11284

[startup+20.0058 s]
Raw data (loadavg): 0.91 0.96 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 2558 0 0 0 1970 12 0 0 25 0 1 0 1843647063 11325440 2458 4294967295 134512640 135094434 3221224432 3221223104 134556327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 2765 2458 145 145 0 2620 0
[pid=9881] vsize: 11060
Current children cumulated CPU time (s) 19.83
Current children cumulated vsize (Kb) 13184

[startup+30.0076 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 2976 0 0 0 2961 16 0 0 25 0 1 0 1843647063 13017088 2876 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 3178 2876 145 145 0 3033 0
[pid=9881] vsize: 12712
Current children cumulated CPU time (s) 29.78
Current children cumulated vsize (Kb) 14836

[startup+40.0084 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 3385 0 0 0 3954 19 0 0 25 0 1 0 1843647063 14757888 3285 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 3603 3285 145 145 0 3458 0
[pid=9881] vsize: 14412
Current children cumulated CPU time (s) 39.74
Current children cumulated vsize (Kb) 16536

[startup+50.0102 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 3773 0 0 0 4945 23 0 0 25 0 1 0 1843647063 16334848 3673 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 3988 3673 145 145 0 3843 0
[pid=9881] vsize: 15952
Current children cumulated CPU time (s) 49.69
Current children cumulated vsize (Kb) 18076

[startup+60.011 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4156 0 0 0 5937 27 0 0 25 0 1 0 1843647063 17891328 4056 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 4368 4056 145 145 0 4223 0
[pid=9881] vsize: 17472
Current children cumulated CPU time (s) 59.65
Current children cumulated vsize (Kb) 19596

[startup+70.0129 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4546 0 0 0 6930 31 0 0 25 0 1 0 1843647063 19480576 4446 4294967295 134512640 135094434 3221224432 3221223024 134557287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 4756 4446 145 145 0 4611 0
[pid=9881] vsize: 19024
Current children cumulated CPU time (s) 69.62
Current children cumulated vsize (Kb) 21148

[startup+80.0147 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 7922 34 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221222080 134562864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0
[pid=9881] vsize: 20640
Current children cumulated CPU time (s) 79.57
Current children cumulated vsize (Kb) 22764

[startup+90.0155 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 8922 34 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0
[pid=9881] vsize: 20640
Current children cumulated CPU time (s) 89.57
Current children cumulated vsize (Kb) 22764

[startup+100.016 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 9922 35 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0
[pid=9881] vsize: 20640
Current children cumulated CPU time (s) 99.58
Current children cumulated vsize (Kb) 22764

[startup+110.018 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 10921 36 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0
[pid=9881] vsize: 20640
Current children cumulated CPU time (s) 109.58
Current children cumulated vsize (Kb) 22764

[startup+120.019 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 11921 36 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0
[pid=9881] vsize: 20640
Current children cumulated CPU time (s) 119.58
Current children cumulated vsize (Kb) 22764

[startup+130.02 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 12920 37 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0
[pid=9881] vsize: 20640
Current children cumulated CPU time (s) 129.58
Current children cumulated vsize (Kb) 22764

[startup+140.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 13919 37 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0
[pid=9881] vsize: 20640
Current children cumulated CPU time (s) 139.57
Current children cumulated vsize (Kb) 22764

[startup+150.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 14919 38 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0
[pid=9881] vsize: 20640
Current children cumulated CPU time (s) 149.58
Current children cumulated vsize (Kb) 22764

[startup+160.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 15919 38 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0
[pid=9881] vsize: 20640
Current children cumulated CPU time (s) 159.58
Current children cumulated vsize (Kb) 22764

[startup+170.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4954 0 0 0 16918 39 0 0 25 0 1 0 1843647063 21135360 4854 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 5160 4854 145 145 0 5015 0
[pid=9881] vsize: 20640
Current children cumulated CPU time (s) 169.58
Current children cumulated vsize (Kb) 22764

[startup+180.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 5208 0 0 0 17913 41 0 0 25 0 1 0 1843647063 22286336 5108 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 5441 5108 145 145 0 5296 0
[pid=9881] vsize: 21764
Current children cumulated CPU time (s) 179.55
Current children cumulated vsize (Kb) 23888

[startup+190.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 5600 0 0 0 18906 44 0 0 25 0 1 0 1843647063 23875584 5500 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 5829 5500 145 145 0 5684 0
[pid=9881] vsize: 23316
Current children cumulated CPU time (s) 189.51
Current children cumulated vsize (Kb) 25440

[startup+200.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 5939 0 0 0 19899 47 0 0 25 0 1 0 1843647063 25251840 5839 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 6165 5839 145 145 0 6020 0
[pid=9881] vsize: 24660
Current children cumulated CPU time (s) 199.47
Current children cumulated vsize (Kb) 26784

[startup+210.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 6343 0 0 0 20891 51 0 0 25 0 1 0 1843647063 26898432 6243 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 6567 6243 145 145 0 6422 0
[pid=9881] vsize: 26268
Current children cumulated CPU time (s) 209.43
Current children cumulated vsize (Kb) 28392

[startup+220.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 6757 0 0 0 21881 56 0 0 25 0 1 0 1843647063 28581888 6657 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 6978 6657 145 145 0 6833 0
[pid=9881] vsize: 27912
Current children cumulated CPU time (s) 219.38
Current children cumulated vsize (Kb) 30036

[startup+230.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7184 0 0 0 22872 59 0 0 25 0 1 0 1843647063 30322688 7084 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 7403 7084 145 145 0 7258 0
[pid=9881] vsize: 29612
Current children cumulated CPU time (s) 229.32
Current children cumulated vsize (Kb) 31736

[startup+240.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 23870 61 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0
[pid=9881] vsize: 29964
Current children cumulated CPU time (s) 239.32
Current children cumulated vsize (Kb) 32088

[startup+250.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 24870 61 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0
[pid=9881] vsize: 29964
Current children cumulated CPU time (s) 249.32
Current children cumulated vsize (Kb) 32088

[startup+260.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 25869 62 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0
[pid=9881] vsize: 29964
Current children cumulated CPU time (s) 259.32
Current children cumulated vsize (Kb) 32088

[startup+270.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 26869 63 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0
[pid=9881] vsize: 29964
Current children cumulated CPU time (s) 269.33
Current children cumulated vsize (Kb) 32088

[startup+280.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 27868 63 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0
[pid=9881] vsize: 29964
Current children cumulated CPU time (s) 279.32
Current children cumulated vsize (Kb) 32088

[startup+290.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 28868 63 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223104 134555821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0
[pid=9881] vsize: 29964
Current children cumulated CPU time (s) 289.32
Current children cumulated vsize (Kb) 32088

[startup+300.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 29867 64 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223056 134562110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0
[pid=9881] vsize: 29964
Current children cumulated CPU time (s) 299.32
Current children cumulated vsize (Kb) 32088

[startup+310.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7448 0 0 0 30864 66 0 0 25 0 1 0 1843647063 31399936 7348 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 7666 7348 145 145 0 7521 0
[pid=9881] vsize: 30664
Current children cumulated CPU time (s) 309.31
Current children cumulated vsize (Kb) 32788

[startup+320.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7855 0 0 0 31856 69 0 0 25 0 1 0 1843647063 33071104 7755 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 8074 7755 145 145 0 7929 0
[pid=9881] vsize: 32296
Current children cumulated CPU time (s) 319.26
Current children cumulated vsize (Kb) 34420

[startup+330.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 8206 0 0 0 32849 72 0 0 18 0 1 0 1843647063 34508800 8106 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 8425 8106 145 145 0 8280 0
[pid=9881] vsize: 33700
Current children cumulated CPU time (s) 329.22
Current children cumulated vsize (Kb) 35824

[startup+340.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 8580 0 0 0 33842 75 0 0 25 0 1 0 1843647063 36040704 8480 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 8799 8480 145 145 0 8654 0
[pid=9881] vsize: 35196
Current children cumulated CPU time (s) 339.18
Current children cumulated vsize (Kb) 37320

[startup+350.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 8958 0 0 0 34835 78 0 0 25 0 1 0 1843647063 37588992 8858 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 9177 8858 145 145 0 9032 0
[pid=9881] vsize: 36708
Current children cumulated CPU time (s) 349.14
Current children cumulated vsize (Kb) 38832

[startup+360.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 9366 0 0 0 35826 82 0 0 25 0 1 0 1843647063 39260160 9266 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 9585 9266 145 145 0 9440 0
[pid=9881] vsize: 38340
Current children cumulated CPU time (s) 359.09
Current children cumulated vsize (Kb) 40464

[startup+370.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 9743 0 0 0 36818 85 0 0 25 0 1 0 1843647063 40800256 9643 4294967295 134512640 135094434 3221224432 3221222896 134781611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 9961 9643 145 145 0 9816 0
[pid=9881] vsize: 39844
Current children cumulated CPU time (s) 369.04
Current children cumulated vsize (Kb) 41968

[startup+380.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) T 9877 9877 28974 0 -1 0 10183 0 0 0 37810 90 0 0 25 0 1 0 1843647063 42590208 10083 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/9881/statm): 10398 10083 145 145 0 10253 0
[pid=9881] vsize: 41592
Current children cumulated CPU time (s) 379.01
Current children cumulated vsize (Kb) 43716

[startup+390.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 10615 0 0 0 38803 93 0 0 25 0 1 0 1843647063 44351488 10515 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 10828 10515 145 145 0 10683 0
[pid=9881] vsize: 43312
Current children cumulated CPU time (s) 388.97
Current children cumulated vsize (Kb) 45436

[startup+400.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 39797 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 398.95
Current children cumulated vsize (Kb) 47080

[startup+410.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 40797 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 408.95
Current children cumulated vsize (Kb) 47080

[startup+420.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 41797 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 418.95
Current children cumulated vsize (Kb) 47080

[startup+430.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 42797 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 428.95
Current children cumulated vsize (Kb) 47080

[startup+440.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 43798 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 438.96
Current children cumulated vsize (Kb) 47080

[startup+450.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 44798 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 448.96
Current children cumulated vsize (Kb) 47080

[startup+460.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 45798 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 458.96
Current children cumulated vsize (Kb) 47080

[startup+470.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 46798 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 468.96
Current children cumulated vsize (Kb) 47080

[startup+480.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 47798 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 478.96
Current children cumulated vsize (Kb) 47080

[startup+490.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 48799 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 488.97
Current children cumulated vsize (Kb) 47080

[startup+500.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 49799 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 498.97
Current children cumulated vsize (Kb) 47080

[startup+510.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 50799 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 508.97
Current children cumulated vsize (Kb) 47080

[startup+520.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 51799 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 518.97
Current children cumulated vsize (Kb) 47080

[startup+530.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 52799 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 528.97
Current children cumulated vsize (Kb) 47080

[startup+540.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 53799 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 538.97
Current children cumulated vsize (Kb) 47080

[startup+550.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 54800 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223120 134554763 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 548.98
Current children cumulated vsize (Kb) 47080

[startup+560.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 55800 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 558.98
Current children cumulated vsize (Kb) 47080

[startup+570.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 56800 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 568.98
Current children cumulated vsize (Kb) 47080

[startup+580.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 57800 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 578.98
Current children cumulated vsize (Kb) 47080

[startup+590.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 58800 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 588.98
Current children cumulated vsize (Kb) 47080

[startup+600.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 59800 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 598.98
Current children cumulated vsize (Kb) 47080

[startup+610.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 60801 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 609
Current children cumulated vsize (Kb) 47080

[startup+620.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 61801 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 619
Current children cumulated vsize (Kb) 47080

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 62801 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 629
Current children cumulated vsize (Kb) 47080

[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 63801 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 639
Current children cumulated vsize (Kb) 47080

[startup+650.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 64801 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 649
Current children cumulated vsize (Kb) 47080

[startup+660.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 65802 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 659.01
Current children cumulated vsize (Kb) 47080

[startup+670.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 66802 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 669.01
Current children cumulated vsize (Kb) 47080

[startup+680.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 67802 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 679.01
Current children cumulated vsize (Kb) 47080

[startup+690.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 68802 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0
[pid=9881] vsize: 44956
Current children cumulated CPU time (s) 689.01
Current children cumulated vsize (Kb) 47080

[startup+700.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11081 0 0 0 69801 98 0 0 25 0 1 0 1843647063 46252032 10981 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11292 10981 145 145 0 11147 0
[pid=9881] vsize: 45168
Current children cumulated CPU time (s) 699
Current children cumulated vsize (Kb) 47292

[startup+710.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11413 0 0 0 70797 101 0 0 25 0 1 0 1843647063 47640576 11313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 11631 11313 145 145 0 11486 0
[pid=9881] vsize: 46524
Current children cumulated CPU time (s) 708.99
Current children cumulated vsize (Kb) 48648

[startup+720.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11788 0 0 0 71790 104 0 0 25 0 1 0 1843647063 49160192 11688 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 12002 11688 145 145 0 11857 0
[pid=9881] vsize: 48008
Current children cumulated CPU time (s) 718.95
Current children cumulated vsize (Kb) 50132

[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 12127 0 0 0 72784 106 0 0 25 0 1 0 1843647063 50540544 12027 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 12339 12027 145 145 0 12194 0
[pid=9881] vsize: 49356
Current children cumulated CPU time (s) 728.91
Current children cumulated vsize (Kb) 51480

[startup+740.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 12449 0 0 0 73778 108 0 0 25 0 1 0 1843647063 51847168 12349 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 12658 12349 145 145 0 12513 0
[pid=9881] vsize: 50632
Current children cumulated CPU time (s) 738.87
Current children cumulated vsize (Kb) 52756

[startup+750.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 12769 0 0 0 74772 111 0 0 25 0 1 0 1843647063 53153792 12669 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 12977 12669 145 145 0 12832 0
[pid=9881] vsize: 51908
Current children cumulated CPU time (s) 748.84
Current children cumulated vsize (Kb) 54032

[startup+760.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13075 0 0 0 75767 112 0 0 25 0 1 0 1843647063 54403072 12975 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13282 12975 145 145 0 13137 0
[pid=9881] vsize: 53128
Current children cumulated CPU time (s) 758.8
Current children cumulated vsize (Kb) 55252

[startup+770.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13357 0 0 0 76761 115 0 0 25 0 1 0 1843647063 55853056 13257 4294967295 134512640 135094434 3221224432 3221223088 134558254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13636 13257 145 145 0 13491 0
[pid=9881] vsize: 54544
Current children cumulated CPU time (s) 768.77
Current children cumulated vsize (Kb) 56668

[startup+780.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13650 0 0 0 77756 117 0 0 25 0 1 0 1843647063 57053184 13550 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13929 13550 145 145 0 13784 0
[pid=9881] vsize: 55716
Current children cumulated CPU time (s) 778.74
Current children cumulated vsize (Kb) 57840

[startup+790.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 78757 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 788.75
Current children cumulated vsize (Kb) 57852

[startup+800.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 79757 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221222992 134550337 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 798.75
Current children cumulated vsize (Kb) 57852

[startup+810.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 80757 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 808.75
Current children cumulated vsize (Kb) 57852

[startup+820.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 81757 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223104 134555453 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 818.75
Current children cumulated vsize (Kb) 57852

[startup+830.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 82757 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 828.75
Current children cumulated vsize (Kb) 57852

[startup+840.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 83757 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 838.75
Current children cumulated vsize (Kb) 57852

[startup+850.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 84758 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 848.76
Current children cumulated vsize (Kb) 57852

[startup+860.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 85758 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 858.76
Current children cumulated vsize (Kb) 57852

[startup+870.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 86758 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 868.76
Current children cumulated vsize (Kb) 57852

[startup+880.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 87758 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221222896 134781535 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 878.76
Current children cumulated vsize (Kb) 57852

[startup+890.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 88759 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 888.77
Current children cumulated vsize (Kb) 57852

[startup+900.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 89759 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 898.77
Current children cumulated vsize (Kb) 57852

[startup+910.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 90759 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 908.77
Current children cumulated vsize (Kb) 57852

[startup+920.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 91759 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 918.77
Current children cumulated vsize (Kb) 57852

[startup+930.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 92759 118 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 928.78
Current children cumulated vsize (Kb) 57852

[startup+940.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 93759 118 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 938.78
Current children cumulated vsize (Kb) 57852

[startup+950.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 94759 118 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 948.78
Current children cumulated vsize (Kb) 57852

[startup+960.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 95759 118 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 958.78
Current children cumulated vsize (Kb) 57852

[startup+970.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 96759 118 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 968.78
Current children cumulated vsize (Kb) 57852

[startup+980.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 97760 118 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0
[pid=9881] vsize: 55728
Current children cumulated CPU time (s) 978.79
Current children cumulated vsize (Kb) 57852

[startup+990.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13908 0 0 0 98753 121 0 0 25 0 1 0 1843647063 58109952 13808 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 14187 13808 145 145 0 14042 0
[pid=9881] vsize: 56748
Current children cumulated CPU time (s) 988.75
Current children cumulated vsize (Kb) 58872

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 14249 0 0 0 99747 124 0 0 25 0 1 0 1843647063 59506688 14149 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 14528 14149 145 145 0 14383 0
[pid=9881] vsize: 58112
Current children cumulated CPU time (s) 998.72
Current children cumulated vsize (Kb) 60236

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 14626 0 0 0 100739 127 0 0 25 0 1 0 1843647063 61050880 14526 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 14905 14526 145 145 0 14760 0
[pid=9881] vsize: 59620
Current children cumulated CPU time (s) 1008.67
Current children cumulated vsize (Kb) 61744

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15068 0 0 0 101731 130 0 0 25 0 1 0 1843647063 62853120 14968 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15345 14968 145 145 0 15200 0
[pid=9881] vsize: 61380
Current children cumulated CPU time (s) 1018.62
Current children cumulated vsize (Kb) 63504

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15435 0 0 0 102725 133 0 0 25 0 1 0 1843647063 64352256 15335 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15711 15335 145 145 0 15566 0
[pid=9881] vsize: 62844
Current children cumulated CPU time (s) 1028.59
Current children cumulated vsize (Kb) 64968

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 103721 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1038.56
Current children cumulated vsize (Kb) 65768

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 104721 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1048.56
Current children cumulated vsize (Kb) 65768

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 105721 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1058.56
Current children cumulated vsize (Kb) 65768

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 106722 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223104 134556519 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1068.57
Current children cumulated vsize (Kb) 65768

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 107722 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1078.57
Current children cumulated vsize (Kb) 65768

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 108722 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223084 134781722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1088.57
Current children cumulated vsize (Kb) 65768

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 109722 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1098.57
Current children cumulated vsize (Kb) 65768

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 110722 135 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1108.58
Current children cumulated vsize (Kb) 65768

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 111722 135 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1118.58
Current children cumulated vsize (Kb) 65768

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 112722 135 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1128.58
Current children cumulated vsize (Kb) 65768

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 113723 135 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1138.59
Current children cumulated vsize (Kb) 65768

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 114723 135 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1148.59
Current children cumulated vsize (Kb) 65768

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 115723 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1158.59
Current children cumulated vsize (Kb) 65768

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 116723 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1168.59
Current children cumulated vsize (Kb) 65768

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 117724 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1178.6
Current children cumulated vsize (Kb) 65768

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 118724 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1188.6
Current children cumulated vsize (Kb) 65768

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 119724 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1198.6
Current children cumulated vsize (Kb) 65768

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 120724 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1208.6
Current children cumulated vsize (Kb) 65768



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 9881
Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/9877/statm): 531 226 485 147 0 384 0
[pid=9877] vsize: 2124
Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 120724 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0
[pid=9881] vsize: 63644
Current children cumulated CPU time (s) 1208.6
Current children cumulated vsize (Kb) 65768

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1208.63
CPU user time (s): 1207.25
CPU system time (s): 1.38679
CPU usage (%): 99.8752
Max. virtual memory (cumulated for all children) (Kb): 65768

Verifier Data

ERROR: no interpretation found !