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/manquinho/primes-dimacs-cnf/normalized-ii8b1.opb
MD5SUM812314147c77e28d5e428080c7a2412d
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 191
Optimality of the best value was proved NO
Number of terms in the objective function 672
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 672
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 672
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.08
Number of variables672
Total number of constraints2404
Number of constraints which are clauses2404
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint8

Trace number 1522

Launcher Data

LAUNCH ON wulflinc24 THE 2005-09-18 15:23:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2502 boxname=wulflinc24 idbench=158 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  812314147c77e28d5e428080c7a2412d  /oldhome/oroussel/tmp/wulflinc24/normalized-ii8b1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-ii8b1.opb
IDLAUNCH: 2502
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        920780 kB
Buffers:         34648 kB
Cached:          51716 kB
SwapCached:        744 kB
Active:          62300 kB
Inactive:        26704 kB
HighTotal:      131008 kB
HighFree:        76048 kB
LowTotal:       903652 kB
LowFree:        844732 kB
SwapTotal:     2097892 kB
SwapFree:      2096644 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5736 kB
Slab:            19256 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 15:43:51 (client local time) WITH STATUS 10 IN 1209.61 SECONDS
stats: 2502 7 1209.61 10

Solver Data

c Parsing PB file...
c Converting 2404 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 |    2404     5328 |     801       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 224
c ---[   0]---> Sorter-cost:30564     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |   39371    91691 |   13123       2       14     7.0 |  0.000 % |
c |       102 |   39094    91112 |   14435      93     3903    42.0 |  0.670 % |
c |       252 |   39002    90914 |   15878     240     6701    27.9 |  0.882 % |
c |       477 |   38987    90884 |   17466     464    15942    34.4 |  0.910 % |
c |       815 |   37805    88284 |   19213     776    24356    31.4 |  3.726 % |
c |      1322 |   37260    87073 |   21134    1269    45788    36.1 |  5.055 % |
c |      2082 |   37129    86792 |   23248    2027    71701    35.4 |  5.354 % |
c |      3223 |   37060    86641 |   25573    3166   105927    33.5 |  5.514 % |
c |      4933 |   36659    85752 |   28130    4825   171835    35.6 |  6.479 % |
c ==============================================================================
c Found solution: 213
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5130 |   36761    86021 |   12253    5022   174707    34.8 |  6.479 % |
c |      5230 |   36692    85868 |   13478    5120   176718    34.5 |  6.749 % |
c |      5381 |   36692    85868 |   14826    5271   182366    34.6 |  6.749 % |
c |      5606 |   36692    85868 |   16308    5496   187885    34.2 |  6.749 % |
c |      5944 |   36590    85644 |   17939    5831   206859    35.5 |  6.987 % |
c |      6450 |   36554    85568 |   19733    6324   229508    36.3 |  7.063 % |
c |      7209 |   36479    85399 |   21706    7081   256581    36.2 |  7.249 % |
c |      8348 |   36479    85399 |   23877    8220   321429    39.1 |  7.249 % |
c ==============================================================================
c Found solution: 212
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8492 |   36455    85340 |   12151    8328   322244    38.7 |  7.249 % |
c |      8592 |   36412    85243 |   13366    8427   325487    38.6 |  7.439 % |
c |      8742 |   36412    85243 |   14702    8577   331063    38.6 |  7.440 % |
c ==============================================================================
c Found solution: 191
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8825 |   36570    85630 |   12190    8660   333479    38.5 |  7.440 % |
c |      8925 |   36570    85630 |   13409    8760   336090    38.4 |  7.604 % |
c |      9075 |   36570    85630 |   14749    8910   343099    38.5 |  7.604 % |
c |      9301 |   36570    85630 |   16224    9136   351679    38.5 |  7.605 % |
c |      9638 |   36570    85630 |   17847    9473   362266    38.2 |  7.604 % |
c |     10144 |   36472    85414 |   19632    9977   379563    38.0 |  7.834 % |
c |     10905 |   36472    85414 |   21595   10738   407634    38.0 |  7.834 % |
c |     12044 |   36472    85414 |   23754   11877   468101    39.4 |  7.834 % |
c |     13754 |   36472    85414 |   26130   13587   522596    38.5 |  7.834 % |
c |     16317 |   36470    85410 |   28743   16149   629422    39.0 |  7.838 % |
c |     20161 |   36426    85316 |   31617   19992   838045    41.9 |  7.936 % |
c |     25927 |   36382    85218 |   34779   25757  1118768    43.4 |  8.043 % |
c |     34576 |   36305    85037 |   38257   34348  1535481    44.7 |  8.244 % |
c |     47550 |   36181    84771 |   42083   21274   996051    46.8 |  8.517 % |
c |     67011 |   36135    84671 |   46291   40732  1888951    46.4 |  8.624 % |
c |     96203 |   36135    84671 |   50920   35083  1330080    37.9 |  8.624 % |
c |    139993 |   36085    84561 |   56012   42013  1861233    44.3 |  8.742 % |
c |    205677 |   36085    84561 |   61613   20830   839310    40.3 |  8.742 % |
c |    304203 |   36085    84561 |   67775   23016   997862    43.4 |  8.742 % |

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/24493/stat): 24493 (minisat+_script) R 24492 24493 20728 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842308236 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24493/statm): 174 3 169 147 0 27 0
[pid=24493] 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=24494
New process pid=24495
New process pid=24496
execve syscall for /bin/sed executable
One traced child (pid=24495) 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=24496) exited with status: 0
One traced child (pid=24494) exited with status: 0
New process pid=24497
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-ii8b1.opb

[startup+10.0032 s]
Raw data (loadavg): 0.92 0.95 0.98 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 2243 0 0 0 978 8 0 0 25 0 1 0 1842308241 9736192 2176 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 2377 2176 145 145 0 2232 0
[pid=24497] vsize: 9508
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 11632

[startup+20.0039 s]
Raw data (loadavg): 0.93 0.96 0.98 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 2535 0 0 0 1973 10 0 0 25 0 1 0 1842308241 11481088 2468 4294967295 134512640 135094434 3221224448 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 2803 2468 145 145 0 2658 0
[pid=24497] vsize: 11212
Current children cumulated CPU time (s) 19.85
Current children cumulated vsize (Kb) 13336

[startup+30.0056 s]
Raw data (loadavg): 0.94 0.96 0.98 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 2796 0 0 0 2967 12 0 0 25 0 1 0 1842308241 12529664 2729 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 3059 2729 145 145 0 2914 0
[pid=24497] vsize: 12236
Current children cumulated CPU time (s) 29.81
Current children cumulated vsize (Kb) 14360

[startup+40.0063 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 3032 0 0 0 3963 14 0 0 25 0 1 0 1842308241 13545472 2965 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 3307 2965 145 145 0 3162 0
[pid=24497] vsize: 13228
Current children cumulated CPU time (s) 39.79
Current children cumulated vsize (Kb) 15352

[startup+50.008 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 3238 0 0 0 4959 16 0 0 25 0 1 0 1842308241 14376960 3171 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 3510 3171 145 145 0 3365 0
[pid=24497] vsize: 14040
Current children cumulated CPU time (s) 49.77
Current children cumulated vsize (Kb) 16164

[startup+60.0087 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 3440 0 0 0 5954 18 0 0 25 0 1 0 1842308241 15187968 3373 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 3708 3373 145 145 0 3563 0
[pid=24497] vsize: 14832
Current children cumulated CPU time (s) 59.74
Current children cumulated vsize (Kb) 16956

[startup+70.0094 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 3611 0 0 0 6950 19 0 0 25 0 1 0 1842308241 15876096 3544 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 3876 3544 145 145 0 3731 0
[pid=24497] vsize: 15504
Current children cumulated CPU time (s) 69.71
Current children cumulated vsize (Kb) 17628

[startup+80.0111 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 3768 0 0 0 7947 21 0 0 25 0 1 0 1842308241 16510976 3701 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 4031 3701 145 145 0 3886 0
[pid=24497] vsize: 16124
Current children cumulated CPU time (s) 79.7
Current children cumulated vsize (Kb) 18248

[startup+90.0118 s]
Raw data (loadavg): 1.05 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 3967 0 0 0 8944 22 0 0 25 0 1 0 1842308241 17457152 3900 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 4262 3900 145 145 0 4117 0
[pid=24497] vsize: 17048
Current children cumulated CPU time (s) 89.68
Current children cumulated vsize (Kb) 19172

[startup+100.013 s]
Raw data (loadavg): 1.04 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4163 0 0 0 9940 23 0 0 25 0 1 0 1842308241 18259968 4096 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 4458 4096 145 145 0 4313 0
[pid=24497] vsize: 17832
Current children cumulated CPU time (s) 99.65
Current children cumulated vsize (Kb) 19956

[startup+110.013 s]
Raw data (loadavg): 1.04 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4381 0 0 0 10936 25 0 0 25 0 1 0 1842308241 19144704 4314 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 4674 4314 145 145 0 4529 0
[pid=24497] vsize: 18696
Current children cumulated CPU time (s) 109.63
Current children cumulated vsize (Kb) 20820

[startup+120.014 s]
Raw data (loadavg): 1.03 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4503 0 0 0 11933 26 0 0 25 0 1 0 1842308241 19636224 4436 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 4794 4436 145 145 0 4649 0
[pid=24497] vsize: 19176
Current children cumulated CPU time (s) 119.61
Current children cumulated vsize (Kb) 21300

[startup+130.015 s]
Raw data (loadavg): 1.02 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4508 0 0 0 12934 26 0 0 25 0 1 0 1842308241 19668992 4441 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 4802 4441 145 145 0 4657 0
[pid=24497] vsize: 19208
Current children cumulated CPU time (s) 129.62
Current children cumulated vsize (Kb) 21332

[startup+140.015 s]
Raw data (loadavg): 1.02 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4509 0 0 0 13934 26 0 0 25 0 1 0 1842308241 19668992 4442 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 4802 4442 145 145 0 4657 0
[pid=24497] vsize: 19208
Current children cumulated CPU time (s) 139.62
Current children cumulated vsize (Kb) 21332

[startup+150.016 s]
Raw data (loadavg): 1.02 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4513 0 0 0 14934 26 0 0 25 0 1 0 1842308241 19685376 4446 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 4806 4446 145 145 0 4661 0
[pid=24497] vsize: 19224
Current children cumulated CPU time (s) 149.62
Current children cumulated vsize (Kb) 21348

[startup+160.017 s]
Raw data (loadavg): 1.01 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4516 0 0 0 15934 27 0 0 25 0 1 0 1842308241 19718144 4449 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 4814 4449 145 145 0 4669 0
[pid=24497] vsize: 19256
Current children cumulated CPU time (s) 159.63
Current children cumulated vsize (Kb) 21380

[startup+170.017 s]
Raw data (loadavg): 1.01 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4528 0 0 0 16934 27 0 0 25 0 1 0 1842308241 19767296 4461 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 4826 4461 145 145 0 4681 0
[pid=24497] vsize: 19304
Current children cumulated CPU time (s) 169.63
Current children cumulated vsize (Kb) 21428

[startup+180.018 s]
Raw data (loadavg): 1.01 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4530 0 0 0 17934 27 0 0 25 0 1 0 1842308241 19767296 4463 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 4826 4463 145 145 0 4681 0
[pid=24497] vsize: 19304
Current children cumulated CPU time (s) 179.63
Current children cumulated vsize (Kb) 21428

[startup+190.019 s]
Raw data (loadavg): 1.01 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4571 0 0 0 18933 27 0 0 25 0 1 0 1842308241 19939328 4504 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 4868 4504 145 145 0 4723 0
[pid=24497] vsize: 19472
Current children cumulated CPU time (s) 189.62
Current children cumulated vsize (Kb) 21596

[startup+200.02 s]
Raw data (loadavg): 1.01 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4708 0 0 0 19931 28 0 0 25 0 1 0 1842308241 20492288 4641 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5003 4641 145 145 0 4858 0
[pid=24497] vsize: 20012
Current children cumulated CPU time (s) 199.61
Current children cumulated vsize (Kb) 22136

[startup+210.021 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4833 0 0 0 20928 29 0 0 25 0 1 0 1842308241 21000192 4766 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5127 4766 145 145 0 4982 0
[pid=24497] vsize: 20508
Current children cumulated CPU time (s) 209.59
Current children cumulated vsize (Kb) 22632

[startup+220.022 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4968 0 0 0 21926 30 0 0 25 0 1 0 1842308241 21544960 4901 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5260 4901 145 145 0 5115 0
[pid=24497] vsize: 21040
Current children cumulated CPU time (s) 219.58
Current children cumulated vsize (Kb) 23164

[startup+230.024 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5106 0 0 0 22924 31 0 0 25 0 1 0 1842308241 22097920 5039 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5395 5039 145 145 0 5250 0
[pid=24497] vsize: 21580
Current children cumulated CPU time (s) 229.57
Current children cumulated vsize (Kb) 23704

[startup+240.023 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5114 0 0 0 23924 31 0 0 25 0 1 0 1842308241 22130688 5047 4294967295 134512640 135094434 3221224448 3221223088 134562041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5403 5047 145 145 0 5258 0
[pid=24497] vsize: 21612
Current children cumulated CPU time (s) 239.57
Current children cumulated vsize (Kb) 23736

[startup+250.024 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5117 0 0 0 24924 31 0 0 25 0 1 0 1842308241 22196224 5050 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5419 5050 145 145 0 5274 0
[pid=24497] vsize: 21676
Current children cumulated CPU time (s) 249.57
Current children cumulated vsize (Kb) 23800

[startup+260.025 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5123 0 0 0 25924 31 0 0 25 0 1 0 1842308241 22196224 5056 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5419 5056 145 145 0 5274 0
[pid=24497] vsize: 21676
Current children cumulated CPU time (s) 259.57
Current children cumulated vsize (Kb) 23800

[startup+270.025 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5129 0 0 0 26925 31 0 0 25 0 1 0 1842308241 22228992 5062 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5427 5062 145 145 0 5282 0
[pid=24497] vsize: 21708
Current children cumulated CPU time (s) 269.58
Current children cumulated vsize (Kb) 23832

[startup+280.026 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5141 0 0 0 27925 31 0 0 25 0 1 0 1842308241 22294528 5074 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5443 5074 145 145 0 5298 0
[pid=24497] vsize: 21772
Current children cumulated CPU time (s) 279.58
Current children cumulated vsize (Kb) 23896

[startup+290.027 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5143 0 0 0 28925 31 0 0 25 0 1 0 1842308241 22294528 5076 4294967295 134512640 135094434 3221224448 3221223104 134558123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5443 5076 145 145 0 5298 0
[pid=24497] vsize: 21772
Current children cumulated CPU time (s) 289.58
Current children cumulated vsize (Kb) 23896

[startup+300.027 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5155 0 0 0 29925 31 0 0 25 0 1 0 1842308241 22392832 5088 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5467 5088 145 145 0 5322 0
[pid=24497] vsize: 21868
Current children cumulated CPU time (s) 299.58
Current children cumulated vsize (Kb) 23992

[startup+310.028 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5169 0 0 0 30925 31 0 0 25 0 1 0 1842308241 22458368 5102 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5483 5102 145 145 0 5338 0
[pid=24497] vsize: 21932
Current children cumulated CPU time (s) 309.58
Current children cumulated vsize (Kb) 24056

[startup+320.029 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5171 0 0 0 31926 31 0 0 25 0 1 0 1842308241 22458368 5104 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5483 5104 145 145 0 5338 0
[pid=24497] vsize: 21932
Current children cumulated CPU time (s) 319.59
Current children cumulated vsize (Kb) 24056

[startup+330.03 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5183 0 0 0 32926 31 0 0 25 0 1 0 1842308241 22523904 5116 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5499 5116 145 145 0 5354 0
[pid=24497] vsize: 21996
Current children cumulated CPU time (s) 329.59
Current children cumulated vsize (Kb) 24120

[startup+340.03 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5186 0 0 0 33926 31 0 0 25 0 1 0 1842308241 22523904 5119 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5499 5119 145 145 0 5354 0
[pid=24497] vsize: 21996
Current children cumulated CPU time (s) 339.59
Current children cumulated vsize (Kb) 24120

[startup+350.032 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5205 0 0 0 34926 31 0 0 25 0 1 0 1842308241 22654976 5138 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5531 5138 145 145 0 5386 0
[pid=24497] vsize: 22124
Current children cumulated CPU time (s) 349.59
Current children cumulated vsize (Kb) 24248

[startup+360.033 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5209 0 0 0 35927 31 0 0 25 0 1 0 1842308241 22654976 5142 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5531 5142 145 145 0 5386 0
[pid=24497] vsize: 22124
Current children cumulated CPU time (s) 359.6
Current children cumulated vsize (Kb) 24248

[startup+370.032 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5267 0 0 0 36926 31 0 0 25 0 1 0 1842308241 22888448 5200 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5588 5200 145 145 0 5443 0
[pid=24497] vsize: 22352
Current children cumulated CPU time (s) 369.59
Current children cumulated vsize (Kb) 24476

[startup+380.033 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5267 0 0 0 37926 31 0 0 25 0 1 0 1842308241 22888448 5200 4294967295 134512640 135094434 3221224448 3221223040 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5588 5200 145 145 0 5443 0
[pid=24497] vsize: 22352
Current children cumulated CPU time (s) 379.59
Current children cumulated vsize (Kb) 24476

[startup+390.034 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5267 0 0 0 38926 31 0 0 25 0 1 0 1842308241 22888448 5200 4294967295 134512640 135094434 3221224448 3221223040 134557423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5588 5200 145 145 0 5443 0
[pid=24497] vsize: 22352
Current children cumulated CPU time (s) 389.59
Current children cumulated vsize (Kb) 24476

[startup+400.034 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5267 0 0 0 39926 31 0 0 25 0 1 0 1842308241 22888448 5200 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5588 5200 145 145 0 5443 0
[pid=24497] vsize: 22352
Current children cumulated CPU time (s) 399.59
Current children cumulated vsize (Kb) 24476

[startup+410.035 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5271 0 0 0 40926 31 0 0 25 0 1 0 1842308241 22904832 5204 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5592 5204 145 145 0 5447 0
[pid=24497] vsize: 22368
Current children cumulated CPU time (s) 409.59
Current children cumulated vsize (Kb) 24492

[startup+420.036 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5277 0 0 0 41927 31 0 0 25 0 1 0 1842308241 22937600 5210 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5600 5210 145 145 0 5455 0
[pid=24497] vsize: 22400
Current children cumulated CPU time (s) 419.6
Current children cumulated vsize (Kb) 24524

[startup+430.036 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5277 0 0 0 42927 31 0 0 25 0 1 0 1842308241 22937600 5210 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5600 5210 145 145 0 5455 0
[pid=24497] vsize: 22400
Current children cumulated CPU time (s) 429.6
Current children cumulated vsize (Kb) 24524

[startup+440.037 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5277 0 0 0 43927 31 0 0 25 0 1 0 1842308241 22937600 5210 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5600 5210 145 145 0 5455 0
[pid=24497] vsize: 22400
Current children cumulated CPU time (s) 439.6
Current children cumulated vsize (Kb) 24524

[startup+450.038 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5292 0 0 0 44927 31 0 0 25 0 1 0 1842308241 23003136 5225 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5616 5225 145 145 0 5471 0
[pid=24497] vsize: 22464
Current children cumulated CPU time (s) 449.6
Current children cumulated vsize (Kb) 24588

[startup+460.039 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5300 0 0 0 45927 32 0 0 25 0 1 0 1842308241 23035904 5233 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5624 5233 145 145 0 5479 0
[pid=24497] vsize: 22496
Current children cumulated CPU time (s) 459.61
Current children cumulated vsize (Kb) 24620

[startup+470.039 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5301 0 0 0 46927 32 0 0 25 0 1 0 1842308241 23035904 5234 4294967295 134512640 135094434 3221224448 3221223040 134557393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5624 5234 145 145 0 5479 0
[pid=24497] vsize: 22496
Current children cumulated CPU time (s) 469.61
Current children cumulated vsize (Kb) 24620

[startup+480.04 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5319 0 0 0 47927 32 0 0 25 0 1 0 1842308241 23134208 5252 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5648 5252 145 145 0 5503 0
[pid=24497] vsize: 22592
Current children cumulated CPU time (s) 479.61
Current children cumulated vsize (Kb) 24716

[startup+490.041 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5326 0 0 0 48928 32 0 0 25 0 1 0 1842308241 23232512 5259 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5672 5259 145 145 0 5527 0
[pid=24497] vsize: 22688
Current children cumulated CPU time (s) 489.62
Current children cumulated vsize (Kb) 24812

[startup+500.042 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5474 0 0 0 49924 33 0 0 25 0 1 0 1842308241 23777280 5407 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5805 5407 145 145 0 5660 0
[pid=24497] vsize: 23220
Current children cumulated CPU time (s) 499.59
Current children cumulated vsize (Kb) 25344

[startup+510.043 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5607 0 0 0 50921 35 0 0 25 0 1 0 1842308241 24317952 5540 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 5937 5540 145 145 0 5792 0
[pid=24497] vsize: 23748
Current children cumulated CPU time (s) 509.58
Current children cumulated vsize (Kb) 25872

[startup+520.044 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5708 0 0 0 51919 36 0 0 25 0 1 0 1842308241 24719360 5641 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6035 5641 145 145 0 5890 0
[pid=24497] vsize: 24140
Current children cumulated CPU time (s) 519.57
Current children cumulated vsize (Kb) 26264

[startup+530.045 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5819 0 0 0 52918 37 0 0 25 0 1 0 1842308241 25161728 5752 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6143 5752 145 145 0 5998 0
[pid=24497] vsize: 24572
Current children cumulated CPU time (s) 529.57
Current children cumulated vsize (Kb) 26696

[startup+540.046 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5819 0 0 0 53918 37 0 0 25 0 1 0 1842308241 25161728 5752 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6143 5752 145 145 0 5998 0
[pid=24497] vsize: 24572
Current children cumulated CPU time (s) 539.57
Current children cumulated vsize (Kb) 26696

[startup+550.047 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5819 0 0 0 54918 37 0 0 25 0 1 0 1842308241 25161728 5752 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6143 5752 145 145 0 5998 0
[pid=24497] vsize: 24572
Current children cumulated CPU time (s) 549.57
Current children cumulated vsize (Kb) 26696

[startup+560.048 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5819 0 0 0 55918 37 0 0 25 0 1 0 1842308241 25161728 5752 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6143 5752 145 145 0 5998 0
[pid=24497] vsize: 24572
Current children cumulated CPU time (s) 559.57
Current children cumulated vsize (Kb) 26696

[startup+570.048 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5819 0 0 0 56919 37 0 0 25 0 1 0 1842308241 25161728 5752 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6143 5752 145 145 0 5998 0
[pid=24497] vsize: 24572
Current children cumulated CPU time (s) 569.58
Current children cumulated vsize (Kb) 26696

[startup+580.049 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5820 0 0 0 57919 37 0 0 25 0 1 0 1842308241 25161728 5753 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6143 5753 145 145 0 5998 0
[pid=24497] vsize: 24572
Current children cumulated CPU time (s) 579.58
Current children cumulated vsize (Kb) 26696

[startup+590.05 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5820 0 0 0 58919 37 0 0 25 0 1 0 1842308241 25161728 5753 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6143 5753 145 145 0 5998 0
[pid=24497] vsize: 24572
Current children cumulated CPU time (s) 589.58
Current children cumulated vsize (Kb) 26696

[startup+600.051 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5855 0 0 0 59919 37 0 0 25 0 1 0 1842308241 25358336 5788 4294967295 134512640 135094434 3221224448 3221223072 134557691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6191 5788 145 145 0 6046 0
[pid=24497] vsize: 24764
Current children cumulated CPU time (s) 599.58
Current children cumulated vsize (Kb) 26888

[startup+610.052 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5855 0 0 0 60919 37 0 0 25 0 1 0 1842308241 25358336 5788 4294967295 134512640 135094434 3221224448 3221223040 134556806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6191 5788 145 145 0 6046 0
[pid=24497] vsize: 24764
Current children cumulated CPU time (s) 609.58
Current children cumulated vsize (Kb) 26888

[startup+620.053 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5860 0 0 0 61919 37 0 0 25 0 1 0 1842308241 25489408 5793 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6223 5793 145 145 0 6078 0
[pid=24497] vsize: 24892
Current children cumulated CPU time (s) 619.58
Current children cumulated vsize (Kb) 27016

[startup+630.053 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5863 0 0 0 62920 37 0 0 25 0 1 0 1842308241 25489408 5796 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6223 5796 145 145 0 6078 0
[pid=24497] vsize: 24892
Current children cumulated CPU time (s) 629.59
Current children cumulated vsize (Kb) 27016

[startup+640.054 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5863 0 0 0 63920 37 0 0 25 0 1 0 1842308241 25489408 5796 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6223 5796 145 145 0 6078 0
[pid=24497] vsize: 24892
Current children cumulated CPU time (s) 639.59
Current children cumulated vsize (Kb) 27016

[startup+650.055 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5864 0 0 0 64920 37 0 0 25 0 1 0 1842308241 25489408 5797 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6223 5797 145 145 0 6078 0
[pid=24497] vsize: 24892
Current children cumulated CPU time (s) 649.59
Current children cumulated vsize (Kb) 27016

[startup+660.056 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5864 0 0 0 65920 37 0 0 25 0 1 0 1842308241 25489408 5797 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6223 5797 145 145 0 6078 0
[pid=24497] vsize: 24892
Current children cumulated CPU time (s) 659.59
Current children cumulated vsize (Kb) 27016

[startup+670.056 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5865 0 0 0 66921 37 0 0 25 0 1 0 1842308241 25489408 5798 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6223 5798 145 145 0 6078 0
[pid=24497] vsize: 24892
Current children cumulated CPU time (s) 669.6
Current children cumulated vsize (Kb) 27016

[startup+680.057 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5869 0 0 0 67921 37 0 0 25 0 1 0 1842308241 25489408 5802 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6223 5802 145 145 0 6078 0
[pid=24497] vsize: 24892
Current children cumulated CPU time (s) 679.6
Current children cumulated vsize (Kb) 27016

[startup+690.058 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5939 0 0 0 68920 37 0 0 25 0 1 0 1842308241 25714688 5872 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6278 5872 145 145 0 6133 0
[pid=24497] vsize: 25112
Current children cumulated CPU time (s) 689.59
Current children cumulated vsize (Kb) 27236

[startup+700.059 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6001 0 0 0 69919 38 0 0 25 0 1 0 1842308241 25976832 5934 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5934 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 699.59
Current children cumulated vsize (Kb) 27492

[startup+710.06 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6001 0 0 0 70919 38 0 0 25 0 1 0 1842308241 25976832 5934 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6342 5934 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 709.59
Current children cumulated vsize (Kb) 27492

[startup+720.061 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6001 0 0 0 71918 39 0 0 25 0 1 0 1842308241 25976832 5934 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5934 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 719.59
Current children cumulated vsize (Kb) 27492

[startup+730.061 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 72918 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 729.59
Current children cumulated vsize (Kb) 27492

[startup+740.062 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 73919 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 739.6
Current children cumulated vsize (Kb) 27492

[startup+750.063 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 74919 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 749.6
Current children cumulated vsize (Kb) 27492

[startup+760.063 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 75919 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 759.6
Current children cumulated vsize (Kb) 27492

[startup+770.064 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 76919 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 769.6
Current children cumulated vsize (Kb) 27492

[startup+780.066 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 77919 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 779.6
Current children cumulated vsize (Kb) 27492

[startup+790.067 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 78920 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223040 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 789.61
Current children cumulated vsize (Kb) 27492

[startup+800.067 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 79920 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 799.61
Current children cumulated vsize (Kb) 27492

[startup+810.068 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 80920 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 809.61
Current children cumulated vsize (Kb) 27492

[startup+820.069 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 81920 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 819.61
Current children cumulated vsize (Kb) 27492

[startup+830.069 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 82920 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 829.61
Current children cumulated vsize (Kb) 27492

[startup+840.07 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 83920 40 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 839.62
Current children cumulated vsize (Kb) 27492

[startup+850.072 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 84921 40 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0
[pid=24497] vsize: 25368
Current children cumulated CPU time (s) 849.63
Current children cumulated vsize (Kb) 27492

[startup+860.072 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6152 0 0 0 85918 41 0 0 25 0 1 0 1842308241 26591232 6085 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6492 6085 145 145 0 6347 0
[pid=24497] vsize: 25968
Current children cumulated CPU time (s) 859.61
Current children cumulated vsize (Kb) 28092

[startup+870.073 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6303 0 0 0 86915 42 0 0 25 0 1 0 1842308241 27209728 6236 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6643 6236 145 145 0 6498 0
[pid=24497] vsize: 26572
Current children cumulated CPU time (s) 869.59
Current children cumulated vsize (Kb) 28696

[startup+880.075 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6444 0 0 0 87912 44 0 0 25 0 1 0 1842308241 28045312 6377 4294967295 134512640 135094434 3221224448 3221223040 134551428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6847 6377 145 145 0 6702 0
[pid=24497] vsize: 27388
Current children cumulated CPU time (s) 879.58
Current children cumulated vsize (Kb) 29512

[startup+890.076 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6444 0 0 0 88912 44 0 0 25 0 1 0 1842308241 28045312 6377 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6847 6377 145 145 0 6702 0
[pid=24497] vsize: 27388
Current children cumulated CPU time (s) 889.58
Current children cumulated vsize (Kb) 29512

[startup+900.077 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6444 0 0 0 89912 44 0 0 25 0 1 0 1842308241 28045312 6377 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6847 6377 145 145 0 6702 0
[pid=24497] vsize: 27388
Current children cumulated CPU time (s) 899.58
Current children cumulated vsize (Kb) 29512

[startup+910.079 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6445 0 0 0 90911 45 0 0 25 0 1 0 1842308241 28045312 6378 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6847 6378 145 145 0 6702 0
[pid=24497] vsize: 27388
Current children cumulated CPU time (s) 909.58
Current children cumulated vsize (Kb) 29512

[startup+920.08 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6447 0 0 0 91911 45 0 0 25 0 1 0 1842308241 28057600 6380 4294967295 134512640 135094434 3221224448 3221223104 134558279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6850 6380 145 145 0 6705 0
[pid=24497] vsize: 27400
Current children cumulated CPU time (s) 919.58
Current children cumulated vsize (Kb) 29524

[startup+930.081 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6447 0 0 0 92911 46 0 0 25 0 1 0 1842308241 28057600 6380 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6850 6380 145 145 0 6705 0
[pid=24497] vsize: 27400
Current children cumulated CPU time (s) 929.59
Current children cumulated vsize (Kb) 29524

[startup+940.082 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6459 0 0 0 93910 46 0 0 25 0 1 0 1842308241 28106752 6392 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6862 6392 145 145 0 6717 0
[pid=24497] vsize: 27448
Current children cumulated CPU time (s) 939.58
Current children cumulated vsize (Kb) 29572

[startup+950.084 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6466 0 0 0 94910 47 0 0 25 0 1 0 1842308241 28139520 6399 4294967295 134512640 135094434 3221224448 3221223120 134555576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6870 6399 145 145 0 6725 0
[pid=24497] vsize: 27480
Current children cumulated CPU time (s) 949.59
Current children cumulated vsize (Kb) 29604

[startup+960.085 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6478 0 0 0 95909 48 0 0 25 0 1 0 1842308241 28188672 6411 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6882 6411 145 145 0 6737 0
[pid=24497] vsize: 27528
Current children cumulated CPU time (s) 959.59
Current children cumulated vsize (Kb) 29652

[startup+970.085 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6490 0 0 0 96909 48 0 0 25 0 1 0 1842308241 28286976 6423 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6906 6423 145 145 0 6761 0
[pid=24497] vsize: 27624
Current children cumulated CPU time (s) 969.59
Current children cumulated vsize (Kb) 29748

[startup+980.087 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6495 0 0 0 97909 48 0 0 25 0 1 0 1842308241 28286976 6428 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6906 6428 145 145 0 6761 0
[pid=24497] vsize: 27624
Current children cumulated CPU time (s) 979.59
Current children cumulated vsize (Kb) 29748

[startup+990.089 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6497 0 0 0 98909 49 0 0 25 0 1 0 1842308241 28286976 6430 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6906 6430 145 145 0 6761 0
[pid=24497] vsize: 27624
Current children cumulated CPU time (s) 989.6
Current children cumulated vsize (Kb) 29748

[startup+1000.09 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6514 0 0 0 99908 49 0 0 25 0 1 0 1842308241 28352512 6447 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6922 6447 145 145 0 6777 0
[pid=24497] vsize: 27688
Current children cumulated CPU time (s) 999.59
Current children cumulated vsize (Kb) 29812

[startup+1010.09 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6530 0 0 0 100907 50 0 0 25 0 1 0 1842308241 28418048 6463 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6938 6463 145 145 0 6793 0
[pid=24497] vsize: 27752
Current children cumulated CPU time (s) 1009.59
Current children cumulated vsize (Kb) 29876

[startup+1020.09 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6532 0 0 0 101906 51 0 0 25 0 1 0 1842308241 28418048 6465 4294967295 134512640 135094434 3221224448 3221223040 134557271 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6938 6465 145 145 0 6793 0
[pid=24497] vsize: 27752
Current children cumulated CPU time (s) 1019.59
Current children cumulated vsize (Kb) 29876

[startup+1030.09 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6551 0 0 0 102904 53 0 0 25 0 1 0 1842308241 28614656 6484 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6986 6484 145 145 0 6841 0
[pid=24497] vsize: 27944
Current children cumulated CPU time (s) 1029.59
Current children cumulated vsize (Kb) 30068

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6557 0 0 0 103903 54 0 0 25 0 1 0 1842308241 28614656 6490 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 6986 6490 145 145 0 6841 0
[pid=24497] vsize: 27944
Current children cumulated CPU time (s) 1039.59
Current children cumulated vsize (Kb) 30068

[startup+1050.1 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6605 0 0 0 104902 55 0 0 25 0 1 0 1842308241 28749824 6538 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 7019 6538 145 145 0 6874 0
[pid=24497] vsize: 28076
Current children cumulated CPU time (s) 1049.59
Current children cumulated vsize (Kb) 30200

[startup+1060.1 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6742 0 0 0 105898 57 0 0 25 0 1 0 1842308241 29306880 6675 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 7155 6675 145 145 0 7010 0
[pid=24497] vsize: 28620
Current children cumulated CPU time (s) 1059.57
Current children cumulated vsize (Kb) 30744

[startup+1070.1 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 106897 58 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0
[pid=24497] vsize: 28772
Current children cumulated CPU time (s) 1069.57
Current children cumulated vsize (Kb) 30896

[startup+1080.1 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 107897 59 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0
[pid=24497] vsize: 28772
Current children cumulated CPU time (s) 1079.58
Current children cumulated vsize (Kb) 30896

[startup+1090.1 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 108896 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0
[pid=24497] vsize: 28772
Current children cumulated CPU time (s) 1089.58
Current children cumulated vsize (Kb) 30896

[startup+1100.1 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 109896 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0
[pid=24497] vsize: 28772
Current children cumulated CPU time (s) 1099.58
Current children cumulated vsize (Kb) 30896

[startup+1110.1 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 110896 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0
[pid=24497] vsize: 28772
Current children cumulated CPU time (s) 1109.58
Current children cumulated vsize (Kb) 30896

[startup+1120.1 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 111897 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0
[pid=24497] vsize: 28772
Current children cumulated CPU time (s) 1119.59
Current children cumulated vsize (Kb) 30896

[startup+1130.11 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 112897 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134558176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0
[pid=24497] vsize: 28772
Current children cumulated CPU time (s) 1129.59
Current children cumulated vsize (Kb) 30896

[startup+1140.11 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 113897 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0
[pid=24497] vsize: 28772
Current children cumulated CPU time (s) 1139.59
Current children cumulated vsize (Kb) 30896

[startup+1150.11 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 114897 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0
[pid=24497] vsize: 28772
Current children cumulated CPU time (s) 1149.59
Current children cumulated vsize (Kb) 30896

[startup+1160.11 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6787 0 0 0 115897 60 0 0 25 0 1 0 1842308241 29478912 6720 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7197 6720 145 145 0 7052 0
[pid=24497] vsize: 28788
Current children cumulated CPU time (s) 1159.59
Current children cumulated vsize (Kb) 30912

[startup+1170.11 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6790 0 0 0 116898 60 0 0 25 0 1 0 1842308241 29495296 6723 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7201 6723 145 145 0 7056 0
[pid=24497] vsize: 28804
Current children cumulated CPU time (s) 1169.6
Current children cumulated vsize (Kb) 30928

[startup+1180.11 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6797 0 0 0 117898 60 0 0 25 0 1 0 1842308241 29528064 6730 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7209 6730 145 145 0 7064 0
[pid=24497] vsize: 28836
Current children cumulated CPU time (s) 1179.6
Current children cumulated vsize (Kb) 30960

[startup+1190.11 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6797 0 0 0 118898 60 0 0 25 0 1 0 1842308241 29528064 6730 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7209 6730 145 145 0 7064 0
[pid=24497] vsize: 28836
Current children cumulated CPU time (s) 1189.6
Current children cumulated vsize (Kb) 30960

[startup+1200.11 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6797 0 0 0 119898 60 0 0 25 0 1 0 1842308241 29528064 6730 4294967295 134512640 135094434 3221224448 3221223040 134557221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7209 6730 145 145 0 7064 0
[pid=24497] vsize: 28836
Current children cumulated CPU time (s) 1199.6
Current children cumulated vsize (Kb) 30960

[startup+1210.11 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6831 0 0 0 120898 60 0 0 25 0 1 0 1842308241 29691904 6764 4294967295 134512640 135094434 3221224448 3221223040 134556914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7249 6764 145 145 0 7104 0
[pid=24497] vsize: 28996
Current children cumulated CPU time (s) 1209.6
Current children cumulated vsize (Kb) 31120



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.00 0.98 0.99 2/57 24497
Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24493/statm): 531 226 485 147 0 384 0
[pid=24493] vsize: 2124
Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6831 0 0 0 120898 60 0 0 25 0 1 0 1842308241 29691904 6764 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24497/statm): 7249 6764 145 145 0 7104 0
[pid=24497] vsize: 28996
Current children cumulated CPU time (s) 1209.6
Current children cumulated vsize (Kb) 31120

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1209.61
CPU user time (s): 1208.99
CPU system time (s): 0.622905
CPU usage (%): 99.9571
Max. virtual memory (cumulated for all children) (Kb): 31120

Verifier Data

ERROR: no interpretation found !