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

Namesubmitted/sorensson/garden/normalized-g15x15.opb
MD5SUM6a083b86cc55025d2acb3bcf68562064
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 54
Optimality of the best value was proved NO
Number of terms in the objective function 225
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 225
Number of bits of the sum of numbers in the objective function 8
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 225
Number of bits of the biggest sum of numbers8
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.11
Number of variables225
Total number of constraints225
Number of constraints which are clauses225
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint3
Maximum length of a constraint5

Trace number 2253

Launcher Data

LAUNCH ON wulflinc28 THE 2005-09-18 18:13:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2611 boxname=wulflinc28 idbench=267 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6a083b86cc55025d2acb3bcf68562064  /oldhome/oroussel/tmp/wulflinc28/normalized-g15x15.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-g15x15.opb
IDLAUNCH: 2611
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        931140 kB
Buffers:         33860 kB
Cached:          41672 kB
SwapCached:        696 kB
Active:          60744 kB
Inactive:        17248 kB
HighTotal:      131008 kB
HighFree:        85792 kB
LowTotal:       903652 kB
LowFree:        845348 kB
SwapTotal:     2097640 kB
SwapFree:      2096372 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5812 kB
Slab:            19848 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 18:34:09 (client local time) WITH STATUS 10 IN 1209.89 SECONDS
stats: 2611 7 1209.89 10

Solver Data

c Parsing PB file...
c Converting 225 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     225     1065 |      75       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 75
c ---[   0]---> Sorter-cost: 6660     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    7880    18944 |    2626       0        0     nan |  0.000 % |
c |       101 |    7833    18849 |    2888      96     1463    15.2 |  0.648 % |
c |       251 |    7833    18849 |    3177     246     4130    16.8 |  0.648 % |
c |       476 |    7833    18849 |    3495     471     7548    16.0 |  0.648 % |
c |       813 |    7815    18811 |    3844     807    14594    18.1 |  0.839 % |
c |      1319 |    7815    18811 |    4229    1313    22407    17.1 |  0.839 % |
c |      2078 |    7815    18811 |    4652    2072    35096    16.9 |  0.839 % |
c |      3218 |    7778    18732 |    5117    3196    64657    20.2 |  1.240 % |
c ==============================================================================
c Found solution: 62
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3831 |    7874    18967 |    2624    3809    80986    21.3 |  1.240 % |
c |      3932 |    7874    18967 |    2886    2006    47019    23.4 |  1.244 % |
c |      4083 |    7858    18933 |    3175    2156    49776    23.1 |  1.414 % |
c |      4311 |    7842    18899 |    3492    2383    52246    21.9 |  1.583 % |
c |      4648 |    7829    18870 |    3841    2710    55952    20.6 |  1.734 % |
c |      5154 |    7800    18807 |    4225    2997    63106    21.1 |  2.055 % |
c |      5913 |    7800    18807 |    4648    3756    76082    20.3 |  2.055 % |
c |      7052 |    7800    18807 |    5113    4895    95383    19.5 |  2.055 % |
c |      8760 |    7777    18758 |    5624    6599   132092    20.0 |  2.300 % |
c |     11322 |    7777    18758 |    6187    5862   151993    25.9 |  2.300 % |
c |     15166 |    7770    18743 |    6805    6264   166593    26.6 |  2.375 % |
c |     20934 |    7746    18691 |    7486    4979    73086    14.7 |  2.639 % |
c |     29584 |    7746    18691 |    8235    5495   121003    22.0 |  2.639 % |
c |     42562 |    7746    18691 |    9058    8643   253958    29.4 |  2.639 % |
c |     62023 |    7729    18654 |    9964    7482   293519    39.2 |  2.828 % |
c ==============================================================================
c Found solution: 60
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82926 |    7732    18673 |    2577    5889   267788    45.5 |  2.828 % |
c |     83026 |    7732    18673 |    2834    1573    37271    23.7 |  3.009 % |
c |     83176 |    7732    18673 |    3118    1723    39197    22.7 |  3.009 % |
c |     83401 |    7732    18673 |    3429    1948    43386    22.3 |  3.009 % |
c |     83740 |    7732    18673 |    3772    2287    49778    21.8 |  3.009 % |
c |     84246 |    7732    18673 |    4150    2793    58214    20.8 |  3.009 % |
c |     85007 |    7730    18669 |    4565    3553    71012    20.0 |  3.028 % |
c |     86147 |    7730    18669 |    5021    4693   101468    21.6 |  3.028 % |
c |     87855 |    7730    18669 |    5524    3686    79696    21.6 |  3.028 % |
c |     90417 |    7730    18669 |    6076    6248   143893    23.0 |  3.028 % |
c |     94264 |    7730    18669 |    6684    6971   182901    26.2 |  3.028 % |
c |    100033 |    7726    18661 |    7352    5471   139305    25.5 |  3.066 % |
c |    108685 |    7726    18661 |    8087    6475   107535    16.6 |  3.066 % |
c |    121659 |    7716    18639 |    8896    5512   193142    35.0 |  3.179 % |
c |    141120 |    7716    18639 |    9786    9263   361472    39.0 |  3.178 % |
c |    170312 |    7716    18639 |   10764   10279   353506    34.4 |  3.178 % |
c |    214101 |    7716    18639 |   11841   11348   495137    43.6 |  3.178 % |
c |    279785 |    7716    18639 |   13025    9072   248141    27.4 |  3.178 % |
c |    378312 |    7716    18639 |   14327    7708   270624    35.1 |  3.178 % |
c ==============================================================================
c Found solution: 58
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    518226 |    7738    18701 |    2579   14849   481198    32.4 |  3.178 % |
c |    518326 |    7738    18701 |    2836    1957    43212    22.1 |  3.188 % |
c |    518476 |    7738    18701 |    3120    2107    46360    22.0 |  3.188 % |
c |    518703 |    7738    18701 |    3432    2334    50915    21.8 |  3.188 % |
c |    519041 |    7738    18701 |    3775    2672    57879    21.7 |  3.188 % |
c |    519549 |    7738    18701 |    4153    3180    67400    21.2 |  3.188 % |
c |    520308 |    7738    18701 |    4568    3939    84338    21.4 |  3.188 % |
c |    521447 |    7738    18701 |    5025    2631    43837    16.7 |  3.188 % |
c |    523156 |    7713    18648 |    5528    2575    36654    14.2 |  3.451 % |
c |    525720 |    7713    18648 |    6081    5139   109499    21.3 |  3.451 % |
c |    529564 |    7713    18648 |    6689    8983   204736    22.8 |  3.451 % |
c |    535331 |    7691    18600 |    7358    6698   147864    22.1 |  3.695 % |
c |    543982 |    7691    18600 |    8094    6960   275619    39.6 |  3.695 % |
c |    556956 |    7691    18600 |    8903    6646   246435    37.1 |  3.695 % |
c |    576418 |    7691    18600 |    9793   10477   215457    20.6 |  3.695 % |
c |    605612 |    7691    18600 |   10773    7116   272652    38.3 |  3.695 % |
c |    649401 |    7678    18569 |   11850   10997   275428    25.0 |  3.863 % |
c |    715085 |    7678    18569 |   13035   12319   413640    33.6 |  3.863 % |
c |    813611 |    7678    18569 |   14339    7550   228042    30.2 |  3.863 % |
c ==============================================================================
c Found solution: 56
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    851603 |    7695    18616 |    2565   12956   397284    30.7 |  3.863 % |
c |    851703 |    7695    18616 |    2821    1720    31470    18.3 |  3.892 % |
c |    851854 |    7695    18616 |    3103    1871    35434    18.9 |  3.892 % |
c |    852081 |    7693    18612 |    3414    2097    38744    18.5 |  3.911 % |
c |    852418 |    7693    18612 |    3755    2434    43532    17.9 |  3.911 % |
c |    852924 |    7693    18612 |    4130    2940    56354    19.2 |  3.911 % |
c |    853684 |    7693    18612 |    4544    3700    76355    20.6 |  3.911 % |
c |    854827 |    7693    18612 |    4998    4843   102579    21.2 |  3.911 % |
c |    856536 |    7693    18612 |    5498    3901    73991    19.0 |  3.911 % |
c |    859099 |    7693    18612 |    6048    6464   145024    22.4 |  3.911 % |
c |    862943 |    7690    18605 |    6652    3876    65509    16.9 |  3.948 % |
c |    868714 |    7690    18605 |    7318    6158   115770    18.8 |  3.948 % |
c |    877368 |    7690    18605 |    8050    7202   106459    14.8 |  3.948 % |
c |    890342 |    7690    18605 |    8855    6654   235117    35.3 |  3.948 % |
c |    909804 |    7680    18583 |    9740    7005   164322    23.5 |  4.061 % |
c |    938996 |    7680    18583 |   10714    8504   305776    36.0 |  4.061 % |
c |    982787 |    7680    18583 |   11786   11511   508585    44.2 |  4.061 % |
c |   1048474 |    7680    18583 |   12964   11456   413707    36.1 |  4.061 % |
c |   1147000 |    7678    18579 |   14261   12201   311601    25.5 |  4.079 % |
c |   1294790 |    7661    18542 |   15687   15149   629931    41.6 |  4.266 % |
c |   1516474 |    7658    18535 |   17256   16992   841342    49.5 |  4.304 % |

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/1972/stat): 1972 (minisat+_script) R 1971 1972 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843340199 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/1972/statm): 174 3 169 147 0 27 0
[pid=1972] 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=1973
New process pid=1974
New process pid=1975
execve syscall for /bin/sed executable
One traced child (pid=1974) 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=1975) exited with status: 0
One traced child (pid=1973) exited with status: 0
New process pid=1976
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-g15x15.opb

[startup+10.0048 s]
Raw data (loadavg): 0.93 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 899 0 0 0 985 6 0 0 25 0 1 0 1843340204 4108288 885 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1976/statm): 1003 885 145 145 0 858 0
[pid=1976] vsize: 4012
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 6136

[startup+20.0065 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1114 0 0 0 1981 7 0 0 25 0 1 0 1843340204 4980736 1100 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1976/statm): 1216 1100 145 145 0 1071 0
[pid=1976] vsize: 4864
Current children cumulated CPU time (s) 19.88
Current children cumulated vsize (Kb) 6988

[startup+30.0072 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1298 0 0 0 2977 9 0 0 25 0 1 0 1843340204 5754880 1284 4294967295 134512640 135094434 3221224448 3221223100 134562194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1976/statm): 1405 1284 145 145 0 1260 0
[pid=1976] vsize: 5620
Current children cumulated CPU time (s) 29.86
Current children cumulated vsize (Kb) 7744

[startup+40.0078 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1640 0 0 0 3971 11 0 0 25 0 1 0 1843340204 7159808 1626 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1976/statm): 1748 1626 145 145 0 1603 0
[pid=1976] vsize: 6992
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 9116

[startup+50.0085 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1640 0 0 0 4971 11 0 0 25 0 1 0 1843340204 7159808 1626 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 1748 1626 145 145 0 1603 0
[pid=1976] vsize: 6992
Current children cumulated CPU time (s) 49.82
Current children cumulated vsize (Kb) 9116

[startup+60.0102 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1640 0 0 0 5972 11 0 0 25 0 1 0 1843340204 7159808 1626 4294967295 134512640 135094434 3221224448 3221223104 134558286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 1748 1626 145 145 0 1603 0
[pid=1976] vsize: 6992
Current children cumulated CPU time (s) 59.83
Current children cumulated vsize (Kb) 9116

[startup+70.0108 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1640 0 0 0 6972 11 0 0 25 0 1 0 1843340204 7159808 1626 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 1748 1626 145 145 0 1603 0
[pid=1976] vsize: 6992
Current children cumulated CPU time (s) 69.83
Current children cumulated vsize (Kb) 9116

[startup+80.0115 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1640 0 0 0 7972 11 0 0 25 0 1 0 1843340204 7159808 1626 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 1748 1626 145 145 0 1603 0
[pid=1976] vsize: 6992
Current children cumulated CPU time (s) 79.83
Current children cumulated vsize (Kb) 9116

[startup+90.0122 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1692 0 0 0 8972 12 0 0 25 0 1 0 1843340204 7368704 1678 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 1799 1678 145 145 0 1654 0
[pid=1976] vsize: 7196
Current children cumulated CPU time (s) 89.84
Current children cumulated vsize (Kb) 9320

[startup+100.012 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1936 0 0 0 9968 13 0 0 25 0 1 0 1843340204 8380416 1922 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2046 1922 145 145 0 1901 0
[pid=1976] vsize: 8184
Current children cumulated CPU time (s) 99.81
Current children cumulated vsize (Kb) 10308

[startup+110.014 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1946 0 0 0 10968 13 0 0 25 0 1 0 1843340204 8437760 1932 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2060 1932 145 145 0 1915 0
[pid=1976] vsize: 8240
Current children cumulated CPU time (s) 109.81
Current children cumulated vsize (Kb) 10364

[startup+120.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1946 0 0 0 11968 13 0 0 25 0 1 0 1843340204 8437760 1932 4294967295 134512640 135094434 3221224448 3221223088 134538540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2060 1932 145 145 0 1915 0
[pid=1976] vsize: 8240
Current children cumulated CPU time (s) 119.81
Current children cumulated vsize (Kb) 10364

[startup+130.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1960 0 0 0 12969 13 0 0 25 0 1 0 1843340204 8503296 1946 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2076 1946 145 145 0 1931 0
[pid=1976] vsize: 8304
Current children cumulated CPU time (s) 129.82
Current children cumulated vsize (Kb) 10428

[startup+140.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1970 0 0 0 13969 13 0 0 25 0 1 0 1843340204 8552448 1956 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2088 1956 145 145 0 1943 0
[pid=1976] vsize: 8352
Current children cumulated CPU time (s) 139.82
Current children cumulated vsize (Kb) 10476

[startup+150.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1999 0 0 0 14969 13 0 0 25 0 1 0 1843340204 8699904 1985 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2124 1985 145 145 0 1979 0
[pid=1976] vsize: 8496
Current children cumulated CPU time (s) 149.82
Current children cumulated vsize (Kb) 10620

[startup+160.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2009 0 0 0 15969 13 0 0 25 0 1 0 1843340204 8740864 1995 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2134 1995 145 145 0 1989 0
[pid=1976] vsize: 8536
Current children cumulated CPU time (s) 159.82
Current children cumulated vsize (Kb) 10660

[startup+170.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2015 0 0 0 16969 13 0 0 25 0 1 0 1843340204 8773632 2001 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2142 2001 145 145 0 1997 0
[pid=1976] vsize: 8568
Current children cumulated CPU time (s) 169.82
Current children cumulated vsize (Kb) 10692

[startup+180.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2074 0 0 0 17968 14 0 0 25 0 1 0 1843340204 9039872 2060 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2207 2060 145 145 0 2062 0
[pid=1976] vsize: 8828
Current children cumulated CPU time (s) 179.82
Current children cumulated vsize (Kb) 10952

[startup+190.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2167 0 0 0 18968 14 0 0 25 0 1 0 1843340204 9428992 2153 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2302 2153 145 145 0 2157 0
[pid=1976] vsize: 9208
Current children cumulated CPU time (s) 189.82
Current children cumulated vsize (Kb) 11332

[startup+200.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2180 0 0 0 19968 14 0 0 25 0 1 0 1843340204 9494528 2166 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2318 2166 145 145 0 2173 0
[pid=1976] vsize: 9272
Current children cumulated CPU time (s) 199.82
Current children cumulated vsize (Kb) 11396

[startup+210.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2180 0 0 0 20968 14 0 0 25 0 1 0 1843340204 9494528 2166 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2318 2166 145 145 0 2173 0
[pid=1976] vsize: 9272
Current children cumulated CPU time (s) 209.82
Current children cumulated vsize (Kb) 11396

[startup+220.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2188 0 0 0 21968 14 0 0 25 0 1 0 1843340204 9527296 2174 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2326 2174 145 145 0 2181 0
[pid=1976] vsize: 9304
Current children cumulated CPU time (s) 219.82
Current children cumulated vsize (Kb) 11428

[startup+230.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2194 0 0 0 22969 14 0 0 25 0 1 0 1843340204 9560064 2180 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2334 2180 145 145 0 2189 0
[pid=1976] vsize: 9336
Current children cumulated CPU time (s) 229.83
Current children cumulated vsize (Kb) 11460

[startup+240.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2234 0 0 0 23968 15 0 0 25 0 1 0 1843340204 9732096 2220 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2376 2220 145 145 0 2231 0
[pid=1976] vsize: 9504
Current children cumulated CPU time (s) 239.83
Current children cumulated vsize (Kb) 11628

[startup+250.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2246 0 0 0 24968 15 0 0 25 0 1 0 1843340204 9773056 2232 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2386 2232 145 145 0 2241 0
[pid=1976] vsize: 9544
Current children cumulated CPU time (s) 249.83
Current children cumulated vsize (Kb) 11668

[startup+260.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2320 0 0 0 25967 15 0 0 25 0 1 0 1843340204 10158080 2306 4294967295 134512640 135094434 3221224448 3221223104 134558286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2480 2306 145 145 0 2335 0
[pid=1976] vsize: 9920
Current children cumulated CPU time (s) 259.82
Current children cumulated vsize (Kb) 12044

[startup+270.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2350 0 0 0 26968 15 0 0 25 0 1 0 1843340204 10276864 2336 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2509 2336 145 145 0 2364 0
[pid=1976] vsize: 10036
Current children cumulated CPU time (s) 269.83
Current children cumulated vsize (Kb) 12160

[startup+280.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2357 0 0 0 27968 15 0 0 25 0 1 0 1843340204 10301440 2343 4294967295 134512640 135094434 3221224448 3221223120 134556327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2515 2343 145 145 0 2370 0
[pid=1976] vsize: 10060
Current children cumulated CPU time (s) 279.83
Current children cumulated vsize (Kb) 12184

[startup+290.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2389 0 0 0 28967 15 0 0 25 0 1 0 1843340204 10440704 2375 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2549 2375 145 145 0 2404 0
[pid=1976] vsize: 10196
Current children cumulated CPU time (s) 289.82
Current children cumulated vsize (Kb) 12320

[startup+300.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2402 0 0 0 29967 15 0 0 25 0 1 0 1843340204 10506240 2388 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2565 2388 145 145 0 2420 0
[pid=1976] vsize: 10260
Current children cumulated CPU time (s) 299.82
Current children cumulated vsize (Kb) 12384

[startup+310.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2407 0 0 0 30967 15 0 0 25 0 1 0 1843340204 10539008 2393 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2573 2393 145 145 0 2428 0
[pid=1976] vsize: 10292
Current children cumulated CPU time (s) 309.82
Current children cumulated vsize (Kb) 12416

[startup+320.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2419 0 0 0 31968 15 0 0 25 0 1 0 1843340204 10596352 2405 4294967295 134512640 135094434 3221224448 3221223040 134556884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2587 2405 145 145 0 2442 0
[pid=1976] vsize: 10348
Current children cumulated CPU time (s) 319.83
Current children cumulated vsize (Kb) 12472

[startup+330.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2451 0 0 0 32967 16 0 0 25 0 1 0 1843340204 10756096 2437 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2626 2437 145 145 0 2481 0
[pid=1976] vsize: 10504
Current children cumulated CPU time (s) 329.83
Current children cumulated vsize (Kb) 12628

[startup+340.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2474 0 0 0 33967 16 0 0 25 0 1 0 1843340204 10887168 2460 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2658 2460 145 145 0 2513 0
[pid=1976] vsize: 10632
Current children cumulated CPU time (s) 339.83
Current children cumulated vsize (Kb) 12756

[startup+350.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2480 0 0 0 34967 16 0 0 25 0 1 0 1843340204 10903552 2466 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1976/statm): 2662 2466 145 145 0 2517 0
[pid=1976] vsize: 10648
Current children cumulated CPU time (s) 349.83
Current children cumulated vsize (Kb) 12772

[startup+360.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2480 0 0 0 35967 16 0 0 25 0 1 0 1843340204 10903552 2466 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2662 2466 145 145 0 2517 0
[pid=1976] vsize: 10648
Current children cumulated CPU time (s) 359.83
Current children cumulated vsize (Kb) 12772

[startup+370.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2480 0 0 0 36967 16 0 0 25 0 1 0 1843340204 10903552 2466 4294967295 134512640 135094434 3221224448 3221223120 134555940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2662 2466 145 145 0 2517 0
[pid=1976] vsize: 10648
Current children cumulated CPU time (s) 369.83
Current children cumulated vsize (Kb) 12772

[startup+380.03 s]
Raw data (loadavg): 0.99 0.98 0.99 3/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2484 0 0 0 37967 16 0 0 25 0 1 0 1843340204 10919936 2470 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2666 2470 145 145 0 2521 0
[pid=1976] vsize: 10664
Current children cumulated CPU time (s) 379.83
Current children cumulated vsize (Kb) 12788

[startup+390.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2526 0 0 0 38967 16 0 0 25 0 1 0 1843340204 11100160 2512 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2710 2512 145 145 0 2565 0
[pid=1976] vsize: 10840
Current children cumulated CPU time (s) 389.83
Current children cumulated vsize (Kb) 12964

[startup+400.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2546 0 0 0 39967 17 0 0 25 0 1 0 1843340204 11182080 2532 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2730 2532 145 145 0 2585 0
[pid=1976] vsize: 10920
Current children cumulated CPU time (s) 399.84
Current children cumulated vsize (Kb) 13044

[startup+410.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2564 0 0 0 40967 17 0 0 25 0 1 0 1843340204 11264000 2550 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2750 2550 145 145 0 2605 0
[pid=1976] vsize: 11000
Current children cumulated CPU time (s) 409.84
Current children cumulated vsize (Kb) 13124

[startup+420.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2594 0 0 0 41967 17 0 0 25 0 1 0 1843340204 11427840 2580 4294967295 134512640 135094434 3221224448 3221223072 134562092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2790 2580 145 145 0 2645 0
[pid=1976] vsize: 11160
Current children cumulated CPU time (s) 419.84
Current children cumulated vsize (Kb) 13284

[startup+430.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2701 0 0 0 42965 18 0 0 25 0 1 0 1843340204 11870208 2687 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2898 2687 145 145 0 2753 0
[pid=1976] vsize: 11592
Current children cumulated CPU time (s) 429.83
Current children cumulated vsize (Kb) 13716

[startup+440.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2721 0 0 0 43965 18 0 0 25 0 1 0 1843340204 11968512 2707 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2922 2707 145 145 0 2777 0
[pid=1976] vsize: 11688
Current children cumulated CPU time (s) 439.83
Current children cumulated vsize (Kb) 13812

[startup+450.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2722 0 0 0 44966 18 0 0 25 0 1 0 1843340204 11968512 2708 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2922 2708 145 145 0 2777 0
[pid=1976] vsize: 11688
Current children cumulated CPU time (s) 449.84
Current children cumulated vsize (Kb) 13812

[startup+460.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2737 0 0 0 45966 18 0 0 25 0 1 0 1843340204 12050432 2723 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2942 2723 145 145 0 2797 0
[pid=1976] vsize: 11768
Current children cumulated CPU time (s) 459.84
Current children cumulated vsize (Kb) 13892

[startup+470.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2744 0 0 0 46966 18 0 0 25 0 1 0 1843340204 12075008 2730 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 2948 2730 145 145 0 2803 0
[pid=1976] vsize: 11792
Current children cumulated CPU time (s) 469.84
Current children cumulated vsize (Kb) 13916

[startup+480.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2851 0 0 0 47964 19 0 0 25 0 1 0 1843340204 12525568 2837 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3058 2837 145 145 0 2913 0
[pid=1976] vsize: 12232
Current children cumulated CPU time (s) 479.83
Current children cumulated vsize (Kb) 14356

[startup+490.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2885 0 0 0 48963 19 0 0 25 0 1 0 1843340204 12681216 2871 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3096 2871 145 145 0 2951 0
[pid=1976] vsize: 12384
Current children cumulated CPU time (s) 489.82
Current children cumulated vsize (Kb) 14508

[startup+500.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2943 0 0 0 49962 20 0 0 25 0 1 0 1843340204 12926976 2929 4294967295 134512640 135094434 3221224448 3221223040 134557182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3156 2929 145 145 0 3011 0
[pid=1976] vsize: 12624
Current children cumulated CPU time (s) 499.82
Current children cumulated vsize (Kb) 14748

[startup+510.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2946 0 0 0 50963 20 0 0 25 0 1 0 1843340204 12943360 2932 4294967295 134512640 135094434 3221224448 3221223104 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3160 2932 145 145 0 3015 0
[pid=1976] vsize: 12640
Current children cumulated CPU time (s) 509.83
Current children cumulated vsize (Kb) 14764

[startup+520.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2947 0 0 0 51963 20 0 0 25 0 1 0 1843340204 12943360 2933 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3160 2933 145 145 0 3015 0
[pid=1976] vsize: 12640
Current children cumulated CPU time (s) 519.83
Current children cumulated vsize (Kb) 14764

[startup+530.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2947 0 0 0 52963 20 0 0 25 0 1 0 1843340204 12943360 2933 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3160 2933 145 145 0 3015 0
[pid=1976] vsize: 12640
Current children cumulated CPU time (s) 529.83
Current children cumulated vsize (Kb) 14764

[startup+540.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2958 0 0 0 53963 20 0 0 25 0 1 0 1843340204 13008896 2944 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3176 2944 145 145 0 3031 0
[pid=1976] vsize: 12704
Current children cumulated CPU time (s) 539.83
Current children cumulated vsize (Kb) 14828

[startup+550.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2961 0 0 0 54963 20 0 0 25 0 1 0 1843340204 13008896 2947 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3176 2947 145 145 0 3031 0
[pid=1976] vsize: 12704
Current children cumulated CPU time (s) 549.83
Current children cumulated vsize (Kb) 14828

[startup+560.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2961 0 0 0 55963 20 0 0 25 0 1 0 1843340204 13008896 2947 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3176 2947 145 145 0 3031 0
[pid=1976] vsize: 12704
Current children cumulated CPU time (s) 559.83
Current children cumulated vsize (Kb) 14828

[startup+570.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2993 0 0 0 56964 20 0 0 25 0 1 0 1843340204 13164544 2979 4294967295 134512640 135094434 3221224448 3221223040 134551463 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3214 2979 145 145 0 3069 0
[pid=1976] vsize: 12856
Current children cumulated CPU time (s) 569.84
Current children cumulated vsize (Kb) 14980

[startup+580.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2998 0 0 0 57963 20 0 0 25 0 1 0 1843340204 13197312 2984 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3222 2984 145 145 0 3077 0
[pid=1976] vsize: 12888
Current children cumulated CPU time (s) 579.83
Current children cumulated vsize (Kb) 15012

[startup+590.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2998 0 0 0 58963 20 0 0 25 0 1 0 1843340204 13197312 2984 4294967295 134512640 135094434 3221224448 3221223040 134552132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3222 2984 145 145 0 3077 0
[pid=1976] vsize: 12888
Current children cumulated CPU time (s) 589.83
Current children cumulated vsize (Kb) 15012

[startup+600.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2998 0 0 0 59963 20 0 0 25 0 1 0 1843340204 13197312 2984 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3222 2984 145 145 0 3077 0
[pid=1976] vsize: 12888
Current children cumulated CPU time (s) 599.83
Current children cumulated vsize (Kb) 15012

[startup+610.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2998 0 0 0 60964 20 0 0 25 0 1 0 1843340204 13197312 2984 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3222 2984 145 145 0 3077 0
[pid=1976] vsize: 12888
Current children cumulated CPU time (s) 609.84
Current children cumulated vsize (Kb) 15012

[startup+620.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3007 0 0 0 61964 20 0 0 25 0 1 0 1843340204 13238272 2993 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3232 2993 145 145 0 3087 0
[pid=1976] vsize: 12928
Current children cumulated CPU time (s) 619.84
Current children cumulated vsize (Kb) 15052

[startup+630.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3169 0 0 0 62961 21 0 0 25 0 1 0 1843340204 13926400 3155 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3400 3155 145 145 0 3255 0
[pid=1976] vsize: 13600
Current children cumulated CPU time (s) 629.82
Current children cumulated vsize (Kb) 15724

[startup+640.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3201 0 0 0 63961 22 0 0 25 0 1 0 1843340204 14057472 3187 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3432 3187 145 145 0 3287 0
[pid=1976] vsize: 13728
Current children cumulated CPU time (s) 639.83
Current children cumulated vsize (Kb) 15852

[startup+650.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3204 0 0 0 64961 22 0 0 25 0 1 0 1843340204 14069760 3190 4294967295 134512640 135094434 3221224448 3221223040 134784942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3435 3190 145 145 0 3290 0
[pid=1976] vsize: 13740
Current children cumulated CPU time (s) 649.83
Current children cumulated vsize (Kb) 15864

[startup+660.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3205 0 0 0 65961 22 0 0 25 0 1 0 1843340204 14069760 3191 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3435 3191 145 145 0 3290 0
[pid=1976] vsize: 13740
Current children cumulated CPU time (s) 659.83
Current children cumulated vsize (Kb) 15864

[startup+670.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3205 0 0 0 66962 22 0 0 25 0 1 0 1843340204 14069760 3191 4294967295 134512640 135094434 3221224448 3221223040 134551997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3435 3191 145 145 0 3290 0
[pid=1976] vsize: 13740
Current children cumulated CPU time (s) 669.84
Current children cumulated vsize (Kb) 15864

[startup+680.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3294 0 0 0 67960 22 0 0 25 0 1 0 1843340204 14467072 3280 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3532 3280 145 145 0 3387 0
[pid=1976] vsize: 14128
Current children cumulated CPU time (s) 679.82
Current children cumulated vsize (Kb) 16252

[startup+690.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3298 0 0 0 68961 22 0 0 25 0 1 0 1843340204 14483456 3284 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3536 3284 145 145 0 3391 0
[pid=1976] vsize: 14144
Current children cumulated CPU time (s) 689.83
Current children cumulated vsize (Kb) 16268

[startup+700.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3303 0 0 0 69961 22 0 0 25 0 1 0 1843340204 14516224 3289 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3544 3289 145 145 0 3399 0
[pid=1976] vsize: 14176
Current children cumulated CPU time (s) 699.83
Current children cumulated vsize (Kb) 16300

[startup+710.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3326 0 0 0 70961 23 0 0 25 0 1 0 1843340204 14647296 3312 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3576 3312 145 145 0 3431 0
[pid=1976] vsize: 14304
Current children cumulated CPU time (s) 709.84
Current children cumulated vsize (Kb) 16428

[startup+720.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3326 0 0 0 71961 23 0 0 25 0 1 0 1843340204 14647296 3312 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3576 3312 145 145 0 3431 0
[pid=1976] vsize: 14304
Current children cumulated CPU time (s) 719.84
Current children cumulated vsize (Kb) 16428

[startup+730.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3326 0 0 0 72961 23 0 0 25 0 1 0 1843340204 14647296 3312 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3576 3312 145 145 0 3431 0
[pid=1976] vsize: 14304
Current children cumulated CPU time (s) 729.84
Current children cumulated vsize (Kb) 16428

[startup+740.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3326 0 0 0 73962 23 0 0 25 0 1 0 1843340204 14647296 3312 4294967295 134512640 135094434 3221224448 3221223040 134551465 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3576 3312 145 145 0 3431 0
[pid=1976] vsize: 14304
Current children cumulated CPU time (s) 739.85
Current children cumulated vsize (Kb) 16428

[startup+750.057 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3326 0 0 0 74962 23 0 0 25 0 1 0 1843340204 14647296 3312 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3576 3312 145 145 0 3431 0
[pid=1976] vsize: 14304
Current children cumulated CPU time (s) 749.85
Current children cumulated vsize (Kb) 16428

[startup+760.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3521 0 0 0 75958 24 0 0 25 0 1 0 1843340204 15454208 3507 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3773 3507 145 145 0 3628 0
[pid=1976] vsize: 15092
Current children cumulated CPU time (s) 759.82
Current children cumulated vsize (Kb) 17216

[startup+770.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3702 0 0 0 76955 25 0 0 25 0 1 0 1843340204 16273408 3688 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3973 3688 145 145 0 3828 0
[pid=1976] vsize: 15892
Current children cumulated CPU time (s) 769.8
Current children cumulated vsize (Kb) 18016

[startup+780.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 77955 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 779.81
Current children cumulated vsize (Kb) 18048

[startup+790.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 78956 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 789.82
Current children cumulated vsize (Kb) 18048

[startup+800.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 79956 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223040 134556928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 799.82
Current children cumulated vsize (Kb) 18048

[startup+810.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 80956 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 809.82
Current children cumulated vsize (Kb) 18048

[startup+820.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 81956 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 819.82
Current children cumulated vsize (Kb) 18048

[startup+830.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 82956 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 829.82
Current children cumulated vsize (Kb) 18048

[startup+840.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 83957 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 839.83
Current children cumulated vsize (Kb) 18048

[startup+850.065 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3712 0 0 0 84957 26 0 0 25 0 1 0 1843340204 16306176 3698 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3981 3698 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 849.83
Current children cumulated vsize (Kb) 18048

[startup+860.066 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3712 0 0 0 85957 26 0 0 25 0 1 0 1843340204 16306176 3698 4294967295 134512640 135094434 3221224448 3221223120 134556460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3981 3698 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 859.83
Current children cumulated vsize (Kb) 18048

[startup+870.066 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3712 0 0 0 86957 26 0 0 25 0 1 0 1843340204 16306176 3698 4294967295 134512640 135094434 3221224448 3221223104 134557856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3981 3698 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 869.83
Current children cumulated vsize (Kb) 18048

[startup+880.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3712 0 0 0 87958 26 0 0 25 0 1 0 1843340204 16306176 3698 4294967295 134512640 135094434 3221224448 3221223120 134556198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1976/statm): 3981 3698 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 879.84
Current children cumulated vsize (Kb) 18048

[startup+890.068 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3712 0 0 0 88957 26 0 0 25 0 1 0 1843340204 16306176 3698 4294967295 134512640 135094434 3221224448 3221223104 134557934 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3981 3698 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 889.83
Current children cumulated vsize (Kb) 18048

[startup+900.069 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3713 0 0 0 89957 26 0 0 25 0 1 0 1843340204 16306176 3699 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 3981 3699 145 145 0 3836 0
[pid=1976] vsize: 15924
Current children cumulated CPU time (s) 899.83
Current children cumulated vsize (Kb) 18048

[startup+910.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3857 0 0 0 90955 27 0 0 25 0 1 0 1843340204 16912384 3843 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4129 3843 145 145 0 3984 0
[pid=1976] vsize: 16516
Current children cumulated CPU time (s) 909.82
Current children cumulated vsize (Kb) 18640

[startup+920.071 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3916 0 0 0 91954 27 0 0 25 0 1 0 1843340204 17178624 3902 4294967295 134512640 135094434 3221224448 3221223104 134557984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4194 3902 145 145 0 4049 0
[pid=1976] vsize: 16776
Current children cumulated CPU time (s) 919.81
Current children cumulated vsize (Kb) 18900

[startup+930.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3929 0 0 0 92955 27 0 0 25 0 1 0 1843340204 17260544 3915 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4214 3915 145 145 0 4069 0
[pid=1976] vsize: 16856
Current children cumulated CPU time (s) 929.82
Current children cumulated vsize (Kb) 18980

[startup+940.072 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3942 0 0 0 93955 27 0 0 25 0 1 0 1843340204 17326080 3928 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4230 3928 145 145 0 4085 0
[pid=1976] vsize: 16920
Current children cumulated CPU time (s) 939.82
Current children cumulated vsize (Kb) 19044

[startup+950.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3953 0 0 0 94955 27 0 0 25 0 1 0 1843340204 17391616 3939 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4246 3939 145 145 0 4101 0
[pid=1976] vsize: 16984
Current children cumulated CPU time (s) 949.82
Current children cumulated vsize (Kb) 19108

[startup+960.073 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3954 0 0 0 95955 27 0 0 25 0 1 0 1843340204 17391616 3940 4294967295 134512640 135094434 3221224448 3221223120 134556543 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4246 3940 145 145 0 4101 0
[pid=1976] vsize: 16984
Current children cumulated CPU time (s) 959.82
Current children cumulated vsize (Kb) 19108

[startup+970.074 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3954 0 0 0 96956 27 0 0 25 0 1 0 1843340204 17391616 3940 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4246 3940 145 145 0 4101 0
[pid=1976] vsize: 16984
Current children cumulated CPU time (s) 969.83
Current children cumulated vsize (Kb) 19108

[startup+980.075 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3960 0 0 0 97956 27 0 0 25 0 1 0 1843340204 17424384 3946 4294967295 134512640 135094434 3221224448 3221223104 134557859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4254 3946 145 145 0 4109 0
[pid=1976] vsize: 17016
Current children cumulated CPU time (s) 979.83
Current children cumulated vsize (Kb) 19140

[startup+990.075 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3966 0 0 0 98956 27 0 0 25 0 1 0 1843340204 17457152 3952 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4262 3952 145 145 0 4117 0
[pid=1976] vsize: 17048
Current children cumulated CPU time (s) 989.83
Current children cumulated vsize (Kb) 19172

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3966 0 0 0 99956 27 0 0 25 0 1 0 1843340204 17457152 3952 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4262 3952 145 145 0 4117 0
[pid=1976] vsize: 17048
Current children cumulated CPU time (s) 999.83
Current children cumulated vsize (Kb) 19172

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3966 0 0 0 100956 27 0 0 25 0 1 0 1843340204 17457152 3952 4294967295 134512640 135094434 3221224448 3221223040 134557398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4262 3952 145 145 0 4117 0
[pid=1976] vsize: 17048
Current children cumulated CPU time (s) 1009.83
Current children cumulated vsize (Kb) 19172

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3966 0 0 0 101957 27 0 0 25 0 1 0 1843340204 17457152 3952 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4262 3952 145 145 0 4117 0
[pid=1976] vsize: 17048
Current children cumulated CPU time (s) 1019.84
Current children cumulated vsize (Kb) 19172

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3966 0 0 0 102957 27 0 0 25 0 1 0 1843340204 17457152 3952 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4262 3952 145 145 0 4117 0
[pid=1976] vsize: 17048
Current children cumulated CPU time (s) 1029.84
Current children cumulated vsize (Kb) 19172

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3966 0 0 0 103957 27 0 0 25 0 1 0 1843340204 17457152 3952 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4262 3952 145 145 0 4117 0
[pid=1976] vsize: 17048
Current children cumulated CPU time (s) 1039.84
Current children cumulated vsize (Kb) 19172

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3971 0 0 0 104957 27 0 0 25 0 1 0 1843340204 17489920 3957 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4270 3957 145 145 0 4125 0
[pid=1976] vsize: 17080
Current children cumulated CPU time (s) 1049.84
Current children cumulated vsize (Kb) 19204

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3971 0 0 0 105958 27 0 0 25 0 1 0 1843340204 17489920 3957 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4270 3957 145 145 0 4125 0
[pid=1976] vsize: 17080
Current children cumulated CPU time (s) 1059.85
Current children cumulated vsize (Kb) 19204

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3971 0 0 0 106958 27 0 0 25 0 1 0 1843340204 17489920 3957 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4270 3957 145 145 0 4125 0
[pid=1976] vsize: 17080
Current children cumulated CPU time (s) 1069.85
Current children cumulated vsize (Kb) 19204

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4105 0 0 0 107956 29 0 0 25 0 1 0 1843340204 18051072 4091 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1976/statm): 4407 4091 145 145 0 4262 0
[pid=1976] vsize: 17628
Current children cumulated CPU time (s) 1079.85
Current children cumulated vsize (Kb) 19752

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4117 0 0 0 108955 29 0 0 25 0 1 0 1843340204 18104320 4103 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4420 4103 145 145 0 4275 0
[pid=1976] vsize: 17680
Current children cumulated CPU time (s) 1089.84
Current children cumulated vsize (Kb) 19804

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4132 0 0 0 109955 29 0 0 25 0 1 0 1843340204 18169856 4118 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4436 4118 145 145 0 4291 0
[pid=1976] vsize: 17744
Current children cumulated CPU time (s) 1099.84
Current children cumulated vsize (Kb) 19868

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4133 0 0 0 110955 29 0 0 25 0 1 0 1843340204 18169856 4119 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4436 4119 145 145 0 4291 0
[pid=1976] vsize: 17744
Current children cumulated CPU time (s) 1109.84
Current children cumulated vsize (Kb) 19868

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4133 0 0 0 111955 29 0 0 25 0 1 0 1843340204 18169856 4119 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4436 4119 145 145 0 4291 0
[pid=1976] vsize: 17744
Current children cumulated CPU time (s) 1119.84
Current children cumulated vsize (Kb) 19868

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4133 0 0 0 112956 29 0 0 25 0 1 0 1843340204 18169856 4119 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4436 4119 145 145 0 4291 0
[pid=1976] vsize: 17744
Current children cumulated CPU time (s) 1129.85
Current children cumulated vsize (Kb) 19868

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4133 0 0 0 113956 29 0 0 25 0 1 0 1843340204 18169856 4119 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4436 4119 145 145 0 4291 0
[pid=1976] vsize: 17744
Current children cumulated CPU time (s) 1139.85
Current children cumulated vsize (Kb) 19868

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4133 0 0 0 114956 29 0 0 25 0 1 0 1843340204 18169856 4119 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4436 4119 145 145 0 4291 0
[pid=1976] vsize: 17744
Current children cumulated CPU time (s) 1149.85
Current children cumulated vsize (Kb) 19868

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4141 0 0 0 115956 29 0 0 25 0 1 0 1843340204 18202624 4127 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4444 4127 145 145 0 4299 0
[pid=1976] vsize: 17776
Current children cumulated CPU time (s) 1159.85
Current children cumulated vsize (Kb) 19900

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4156 0 0 0 116957 29 0 0 25 0 1 0 1843340204 18284544 4142 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4464 4142 145 145 0 4319 0
[pid=1976] vsize: 17856
Current children cumulated CPU time (s) 1169.86
Current children cumulated vsize (Kb) 19980

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4156 0 0 0 117957 29 0 0 25 0 1 0 1843340204 18284544 4142 4294967295 134512640 135094434 3221224448 3221223040 134784942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4464 4142 145 145 0 4319 0
[pid=1976] vsize: 17856
Current children cumulated CPU time (s) 1179.86
Current children cumulated vsize (Kb) 19980

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4163 0 0 0 118957 29 0 0 25 0 1 0 1843340204 18300928 4149 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4468 4149 145 145 0 4323 0
[pid=1976] vsize: 17872
Current children cumulated CPU time (s) 1189.86
Current children cumulated vsize (Kb) 19996

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4172 0 0 0 119957 29 0 0 25 0 1 0 1843340204 18350080 4158 4294967295 134512640 135094434 3221224448 3221223040 134557421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4480 4158 145 145 0 4335 0
[pid=1976] vsize: 17920
Current children cumulated CPU time (s) 1199.86
Current children cumulated vsize (Kb) 20044

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4172 0 0 0 120958 29 0 0 25 0 1 0 1843340204 18350080 4158 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4480 4158 145 145 0 4335 0
[pid=1976] vsize: 17920
Current children cumulated CPU time (s) 1209.87
Current children cumulated vsize (Kb) 20044



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 1976
Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/1972/statm): 531 226 485 147 0 384 0
[pid=1972] vsize: 2124
Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4172 0 0 0 120958 29 0 0 25 0 1 0 1843340204 18350080 4158 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1976/statm): 4480 4158 145 145 0 4335 0
[pid=1976] vsize: 17920
Current children cumulated CPU time (s) 1209.87
Current children cumulated vsize (Kb) 20044

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.89
CPU user time (s): 1209.58
CPU system time (s): 0.304953
CPU usage (%): 99.9816
Max. virtual memory (cumulated for all children) (Kb): 20044

Verifier Data

ERROR: no interpretation found !