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/logic-synthesis/normalized-e64.b.opb
MD5SUMbf7f8537c6faa135d25c67c53576abb5
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 51
Optimality of the best value was proved NO
Number of terms in the objective function 608
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 608
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 608
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.16
Number of variables607
Total number of constraints1053
Number of constraints which are clauses1022
Number of constraints which are cardinality constraints (but not clauses)31
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint3
Maximum length of a constraint32

Trace number 909

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        716528 kB
Buffers:         35364 kB
Cached:         252280 kB
SwapCached:       1016 kB
Active:          92892 kB
Inactive:       197540 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        716276 kB
SwapTotal:     2097892 kB
SwapFree:      2096404 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5768 kB
Slab:            21988 kB
Committed_AS:    64376 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 13:04:31 (client local time) WITH STATUS 10 IN 1209.32 SECONDS
stats: 2408 7 1209.32 10

Solver Data

c Parsing PB file...
c Converting 1022 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 |    1022     8200 |     340       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 82
c ---[   0]---> Sorter-cost:27428     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   32888    82605 |   10962       1       16    16.0 |  0.000 % |
c |       101 |   32731    82280 |   12058      94     1328    14.1 |  0.441 % |
c |       251 |   32731    82280 |   13264     244     4888    20.0 |  0.441 % |
c |       476 |   32693    82200 |   14590     467     9207    19.7 |  0.538 % |
c |       815 |   32655    82120 |   16049     805    14538    18.1 |  0.636 % |
c ==============================================================================
c Found solution: 64
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1118 |   32544    81867 |   10848    1108    20015    18.1 |  0.636 % |
c |      1219 |   32544    81867 |   11932    1209    21890    18.1 |  1.342 % |
c |      1371 |   32544    81867 |   13126    1361    27251    20.0 |  1.342 % |
c |      1597 |   32544    81867 |   14438    1587    32001    20.2 |  1.342 % |
c |      1935 |   32544    81867 |   15882    1925    44062    22.9 |  1.342 % |
c |      2442 |   32526    81825 |   17470    2426    58440    24.1 |  1.397 % |
c |      3201 |   32524    81821 |   19217    3182    81772    25.7 |  1.402 % |
c |      4340 |   32524    81821 |   21139    4321   124438    28.8 |  1.402 % |
c |      6049 |   32524    81821 |   23253    6030   236669    39.2 |  1.402 % |
c |      8611 |   32524    81821 |   25579    8592   404633    47.1 |  1.402 % |
c |     12456 |   32524    81821 |   28136   12437   881628    70.9 |  1.402 % |
c ==============================================================================
c Found solution: 57
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17530 |   32583    81971 |   10861   17511  1261267    72.0 |  1.402 % |
c |     17631 |   32583    81971 |   11947    8857   728551    82.3 |  1.404 % |
c |     17781 |   32557    81915 |   13141    9005   733381    81.4 |  1.474 % |
c |     18007 |   32557    81915 |   14455    9231   741448    80.3 |  1.474 % |
c |     18344 |   32557    81915 |   15901    9568   749366    78.3 |  1.474 % |
c |     18850 |   32557    81915 |   17491   10074   785392    78.0 |  1.474 % |
c |     19609 |   32557    81915 |   19240   10833   859333    79.3 |  1.474 % |
c |     20748 |   32557    81915 |   21165   11972   919844    76.8 |  1.474 % |
c |     22458 |   32557    81915 |   23281   13682  1056358    77.2 |  1.474 % |
c |     25020 |   32557    81915 |   25609   16244  1287855    79.3 |  1.474 % |
c ==============================================================================
c Found solution: 55
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25537 |   32576    81969 |   10858   16761  1329272    79.3 |  1.474 % |
c |     25637 |   32576    81969 |   11943    8481   589547    69.5 |  1.477 % |
c |     25787 |   32576    81969 |   13138    8631   595037    68.9 |  1.477 % |
c |     26012 |   32576    81969 |   14451    8856   607205    68.6 |  1.477 % |
c |     26349 |   32576    81969 |   15897    9193   625383    68.0 |  1.477 % |
c |     26855 |   32576    81969 |   17486    9699   645599    66.6 |  1.477 % |
c |     27616 |   32576    81969 |   19235   10460   688721    65.8 |  1.477 % |
c |     28755 |   32576    81969 |   21159   11599   760883    65.6 |  1.477 % |
c |     30463 |   32576    81969 |   23275   13307   926598    69.6 |  1.477 % |
c |     33026 |   32576    81969 |   25602   15870  1052589    66.3 |  1.477 % |
c |     36872 |   32576    81969 |   28162   19716  1313125    66.6 |  1.477 % |
c |     42638 |   32540    81893 |   30979   25472  1707177    67.0 |  1.570 % |
c |     51288 |   32540    81893 |   34077   13453   850735    63.2 |  1.570 % |
c |     64262 |   32540    81893 |   37484   26427  1854535    70.2 |  1.570 % |
c ==============================================================================
c Found solution: 53
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71120 |   32558    81945 |   10852   33285  2473346    74.3 |  1.570 % |
c |     71222 |   32558    81945 |   11937    6680   548160    82.1 |  1.583 % |
c |     71372 |   32558    81945 |   13130    6830   551418    80.7 |  1.583 % |
c |     71597 |   32558    81945 |   14444    7055   563546    79.9 |  1.583 % |
c |     71934 |   32558    81945 |   15888    7392   572407    77.4 |  1.583 % |
c |     72440 |   32558    81945 |   17477    7898   589289    74.6 |  1.583 % |
c |     73199 |   32558    81945 |   19224    8657   630654    72.8 |  1.583 % |
c |     74340 |   32558    81945 |   21147    9798   684750    69.9 |  1.583 % |
c |     76048 |   32558    81945 |   23262   11506   842785    73.2 |  1.583 % |
c |     78611 |   32558    81945 |   25588   14069  1080790    76.8 |  1.583 % |
c |     82457 |   32558    81945 |   28147   17915  1447445    80.8 |  1.583 % |
c |     88223 |   32558    81945 |   30962   23681  1883985    79.6 |  1.583 % |
c |     96872 |   32558    81945 |   34058   32330  2567295    79.4 |  1.583 % |
c |    109848 |   32558    81945 |   37464   21298  1707483    80.2 |  1.583 % |
c |    129309 |   32558    81945 |   41210   13470  1145174    85.0 |  1.583 % |
c |    158501 |   32558    81945 |   45331   42662  3823977    89.6 |  1.583 % |
c |    202290 |   32558    81945 |   49864   18699  1418328    75.9 |  1.583 % |
c |    267976 |   32558    81945 |   54851   46288  3760997    81.3 |  1.583 % |
c |    366502 |   32558    81945 |   60336   17595  1604710    91.2 |  1.583 % |

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/11981/stat): 11981 (minisat+_script) R 11980 11981 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841311762 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/11981/statm): 174 3 169 147 0 27 0
[pid=11981] 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=11982
New process pid=11983
New process pid=11984
execve syscall for /bin/sed executable
One traced child (pid=11983) 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=11984) exited with status: 0
One traced child (pid=11982) exited with status: 0
New process pid=11985
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-e64.b.opb

[startup+10.0033 s]
Raw data (loadavg): 0.94 0.99 0.97 2/58 11987
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 2310 0 0 0 974 9 0 0 25 0 1 0 1841311767 10403840 2244 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 2540 2244 145 145 0 2395 0
[pid=11985] vsize: 10160
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 12284

[startup+20.0053 s]
Raw data (loadavg): 0.95 0.99 0.97 2/58 11987
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 2905 0 0 0 1963 13 0 0 25 0 1 0 1841311767 12824576 2839 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 3131 2839 145 145 0 2986 0
[pid=11985] vsize: 12524
Current children cumulated CPU time (s) 19.76
Current children cumulated vsize (Kb) 14648

[startup+30.0062 s]
Raw data (loadavg): 0.96 0.99 0.97 2/58 11987
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 3313 0 0 0 2955 17 0 0 25 0 1 0 1841311767 14536704 3247 4294967295 134512640 135094434 3221224448 3221223104 134557835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 3549 3247 145 145 0 3404 0
[pid=11985] vsize: 14196
Current children cumulated CPU time (s) 29.72
Current children cumulated vsize (Kb) 16320

[startup+40.0072 s]
Raw data (loadavg): 0.96 0.99 0.97 2/58 11987
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 3313 0 0 0 3955 17 0 0 25 0 1 0 1841311767 14536704 3247 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 3549 3247 145 145 0 3404 0
[pid=11985] vsize: 14196
Current children cumulated CPU time (s) 39.72
Current children cumulated vsize (Kb) 16320

[startup+50.0091 s]
Raw data (loadavg): 0.97 0.99 0.97 2/58 11987
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 3425 0 0 0 4951 20 0 0 25 0 1 0 1841311767 14995456 3359 4294967295 134512640 135094434 3221224448 3221223072 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 3661 3359 145 145 0 3516 0
[pid=11985] vsize: 14644
Current children cumulated CPU time (s) 49.71
Current children cumulated vsize (Kb) 16768

[startup+60.01 s]
Raw data (loadavg): 0.97 0.99 0.97 2/58 11987
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 3427 0 0 0 5951 20 0 0 25 0 1 0 1841311767 14995456 3361 4294967295 134512640 135094434 3221224448 3221223088 134562070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 3661 3361 145 145 0 3516 0
[pid=11985] vsize: 14644
Current children cumulated CPU time (s) 59.71
Current children cumulated vsize (Kb) 16768

[startup+70.0119 s]
Raw data (loadavg): 0.98 0.99 0.97 2/58 11989
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 3803 0 0 0 6943 24 0 0 25 0 1 0 1841311767 16515072 3737 4294967295 134512640 135094434 3221224448 3221223120 134556236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 4032 3737 145 145 0 3887 0
[pid=11985] vsize: 16128
Current children cumulated CPU time (s) 69.67
Current children cumulated vsize (Kb) 18252

[startup+80.0139 s]
Raw data (loadavg): 0.98 0.99 0.97 2/58 11989
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4178 0 0 0 7936 27 0 0 25 0 1 0 1841311767 18030592 4112 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 4402 4112 145 145 0 4257 0
[pid=11985] vsize: 17608
Current children cumulated CPU time (s) 79.63
Current children cumulated vsize (Kb) 19732

[startup+90.0148 s]
Raw data (loadavg): 0.98 0.99 0.97 2/58 11989
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4511 0 0 0 8930 30 0 0 25 0 1 0 1841311767 19521536 4445 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 4766 4445 145 145 0 4621 0
[pid=11985] vsize: 19064
Current children cumulated CPU time (s) 89.6
Current children cumulated vsize (Kb) 21188

[startup+100.017 s]
Raw data (loadavg): 0.98 0.99 0.97 2/58 11989
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4547 0 0 0 9929 31 0 0 25 0 1 0 1841311767 19668992 4481 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 4802 4481 145 145 0 4657 0
[pid=11985] vsize: 19208
Current children cumulated CPU time (s) 99.6
Current children cumulated vsize (Kb) 21332

[startup+110.018 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11989
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4547 0 0 0 10928 31 0 0 25 0 1 0 1841311767 19668992 4481 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 4802 4481 145 145 0 4657 0
[pid=11985] vsize: 19208
Current children cumulated CPU time (s) 109.59
Current children cumulated vsize (Kb) 21332

[startup+120.02 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11989
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4547 0 0 0 11928 31 0 0 25 0 1 0 1841311767 19668992 4481 4294967295 134512640 135094434 3221224448 3221223120 134556071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 4802 4481 145 145 0 4657 0
[pid=11985] vsize: 19208
Current children cumulated CPU time (s) 119.59
Current children cumulated vsize (Kb) 21332

[startup+130.021 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11991
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4758 0 0 0 12924 34 0 0 25 0 1 0 1841311767 20533248 4692 4294967295 134512640 135094434 3221224448 3221223104 134558281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 5013 4692 145 145 0 4868 0
[pid=11985] vsize: 20052
Current children cumulated CPU time (s) 129.58
Current children cumulated vsize (Kb) 22176

[startup+140.021 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11991
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4861 0 0 0 13923 35 0 0 25 0 1 0 1841311767 20955136 4795 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 5116 4795 145 145 0 4971 0
[pid=11985] vsize: 20464
Current children cumulated CPU time (s) 139.58
Current children cumulated vsize (Kb) 22588

[startup+150.023 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11991
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4861 0 0 0 14922 35 0 0 25 0 1 0 1841311767 20955136 4795 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 5116 4795 145 145 0 4971 0
[pid=11985] vsize: 20464
Current children cumulated CPU time (s) 149.57
Current children cumulated vsize (Kb) 22588

[startup+160.024 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11991
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4861 0 0 0 15922 36 0 0 25 0 1 0 1841311767 20955136 4795 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 5116 4795 145 145 0 4971 0
[pid=11985] vsize: 20464
Current children cumulated CPU time (s) 159.58
Current children cumulated vsize (Kb) 22588

[startup+170.026 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11991
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4861 0 0 0 16922 36 0 0 25 0 1 0 1841311767 20955136 4795 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 5116 4795 145 145 0 4971 0
[pid=11985] vsize: 20464
Current children cumulated CPU time (s) 169.58
Current children cumulated vsize (Kb) 22588

[startup+180.027 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11991
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4998 0 0 0 17919 38 0 0 25 0 1 0 1841311767 21520384 4932 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 5254 4932 145 145 0 5109 0
[pid=11985] vsize: 21016
Current children cumulated CPU time (s) 179.57
Current children cumulated vsize (Kb) 23140

[startup+190.028 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11993
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 5469 0 0 0 18907 43 0 0 25 0 1 0 1841311767 23433216 5403 4294967295 134512640 135094434 3221224448 3221223104 134558715 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 5721 5403 145 145 0 5576 0
[pid=11985] vsize: 22884
Current children cumulated CPU time (s) 189.5
Current children cumulated vsize (Kb) 25008

[startup+200.029 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11993
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 5469 0 0 0 19907 43 0 0 25 0 1 0 1841311767 23433216 5403 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 5721 5403 145 145 0 5576 0
[pid=11985] vsize: 22884
Current children cumulated CPU time (s) 199.5
Current children cumulated vsize (Kb) 25008

[startup+210.03 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11993
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 5469 0 0 0 20906 44 0 0 25 0 1 0 1841311767 23433216 5403 4294967295 134512640 135094434 3221224448 3221223104 134561778 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 5721 5403 145 145 0 5576 0
[pid=11985] vsize: 22884
Current children cumulated CPU time (s) 209.5
Current children cumulated vsize (Kb) 25008

[startup+220.032 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11993
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 5469 0 0 0 21905 45 0 0 25 0 1 0 1841311767 23433216 5403 4294967295 134512640 135094434 3221224448 3221223120 134556071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 5721 5403 145 145 0 5576 0
[pid=11985] vsize: 22884
Current children cumulated CPU time (s) 219.5
Current children cumulated vsize (Kb) 25008

[startup+230.033 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11993
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 5469 0 0 0 22905 45 0 0 25 0 1 0 1841311767 23433216 5403 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 5721 5403 145 145 0 5576 0
[pid=11985] vsize: 22884
Current children cumulated CPU time (s) 229.5
Current children cumulated vsize (Kb) 25008

[startup+240.034 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11993
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 5694 0 0 0 23901 47 0 0 25 0 1 0 1841311767 24363008 5628 4294967295 134512640 135094434 3221224448 3221223104 134558011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 5948 5628 145 145 0 5803 0
[pid=11985] vsize: 23792
Current children cumulated CPU time (s) 239.48
Current children cumulated vsize (Kb) 25916

[startup+250.035 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11995
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6036 0 0 0 24893 51 0 0 25 0 1 0 1841311767 25759744 5970 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 6289 5970 145 145 0 6144 0
[pid=11985] vsize: 25156
Current children cumulated CPU time (s) 249.44
Current children cumulated vsize (Kb) 27280

[startup+260.036 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11995
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6045 0 0 0 25893 51 0 0 25 0 1 0 1841311767 25796608 5979 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 6298 5979 145 145 0 6153 0
[pid=11985] vsize: 25192
Current children cumulated CPU time (s) 259.44
Current children cumulated vsize (Kb) 27316

[startup+270.036 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11995
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6045 0 0 0 26893 51 0 0 25 0 1 0 1841311767 25796608 5979 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 6298 5979 145 145 0 6153 0
[pid=11985] vsize: 25192
Current children cumulated CPU time (s) 269.44
Current children cumulated vsize (Kb) 27316

[startup+280.037 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11995
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6046 0 0 0 27893 51 0 0 25 0 1 0 1841311767 25796608 5980 4294967295 134512640 135094434 3221224448 3221223120 134555560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 6298 5980 145 145 0 6153 0
[pid=11985] vsize: 25192
Current children cumulated CPU time (s) 279.44
Current children cumulated vsize (Kb) 27316

[startup+290.038 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11995
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6046 0 0 0 28893 51 0 0 25 0 1 0 1841311767 25796608 5980 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 6298 5980 145 145 0 6153 0
[pid=11985] vsize: 25192
Current children cumulated CPU time (s) 289.44
Current children cumulated vsize (Kb) 27316

[startup+300.039 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11995
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6046 0 0 0 29893 52 0 0 25 0 1 0 1841311767 25796608 5980 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 6298 5980 145 145 0 6153 0
[pid=11985] vsize: 25192
Current children cumulated CPU time (s) 299.45
Current children cumulated vsize (Kb) 27316

[startup+310.04 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11997
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6201 0 0 0 30890 53 0 0 25 0 1 0 1841311767 26435584 6135 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 6454 6135 145 145 0 6309 0
[pid=11985] vsize: 25816
Current children cumulated CPU time (s) 309.43
Current children cumulated vsize (Kb) 27940

[startup+320.041 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11997
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6576 0 0 0 31883 56 0 0 25 0 1 0 1841311767 27983872 6510 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 6832 6510 145 145 0 6687 0
[pid=11985] vsize: 27328
Current children cumulated CPU time (s) 319.39
Current children cumulated vsize (Kb) 29452

[startup+330.042 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11997
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6939 0 0 0 32876 60 0 0 25 0 1 0 1841311767 29474816 6873 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7196 6873 145 145 0 7051 0
[pid=11985] vsize: 28784
Current children cumulated CPU time (s) 329.36
Current children cumulated vsize (Kb) 30908

[startup+340.043 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11997
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7184 0 0 0 33872 62 0 0 25 0 1 0 1841311767 30461952 7118 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7437 7118 145 145 0 7292 0
[pid=11985] vsize: 29748
Current children cumulated CPU time (s) 339.34
Current children cumulated vsize (Kb) 31872

[startup+350.044 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11997
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7184 0 0 0 34872 62 0 0 25 0 1 0 1841311767 30461952 7118 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7437 7118 145 145 0 7292 0
[pid=11985] vsize: 29748
Current children cumulated CPU time (s) 349.34
Current children cumulated vsize (Kb) 31872

[startup+360.045 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11997
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7184 0 0 0 35872 62 0 0 25 0 1 0 1841311767 30461952 7118 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7437 7118 145 145 0 7292 0
[pid=11985] vsize: 29748
Current children cumulated CPU time (s) 359.34
Current children cumulated vsize (Kb) 31872

[startup+370.046 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11999
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7184 0 0 0 36872 62 0 0 25 0 1 0 1841311767 30461952 7118 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7437 7118 145 145 0 7292 0
[pid=11985] vsize: 29748
Current children cumulated CPU time (s) 369.34
Current children cumulated vsize (Kb) 31872

[startup+380.047 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11999
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7196 0 0 0 37872 62 0 0 25 0 1 0 1841311767 30527488 7130 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7453 7130 145 145 0 7308 0
[pid=11985] vsize: 29812
Current children cumulated CPU time (s) 379.34
Current children cumulated vsize (Kb) 31936

[startup+390.048 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11999
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7206 0 0 0 38872 62 0 0 25 0 1 0 1841311767 30593024 7140 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7469 7140 145 145 0 7324 0
[pid=11985] vsize: 29876
Current children cumulated CPU time (s) 389.34
Current children cumulated vsize (Kb) 32000

[startup+400.05 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11999
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7207 0 0 0 39873 62 0 0 25 0 1 0 1841311767 30593024 7141 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7469 7141 145 145 0 7324 0
[pid=11985] vsize: 29876
Current children cumulated CPU time (s) 399.35
Current children cumulated vsize (Kb) 32000

[startup+410.051 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11999
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7208 0 0 0 40873 62 0 0 25 0 1 0 1841311767 30593024 7142 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7469 7142 145 145 0 7324 0
[pid=11985] vsize: 29876
Current children cumulated CPU time (s) 409.35
Current children cumulated vsize (Kb) 32000

[startup+420.051 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 11999
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 41873 62 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0
[pid=11985] vsize: 29940
Current children cumulated CPU time (s) 419.35
Current children cumulated vsize (Kb) 32064

[startup+430.052 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12001
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 42873 62 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0
[pid=11985] vsize: 29940
Current children cumulated CPU time (s) 429.35
Current children cumulated vsize (Kb) 32064

[startup+440.053 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12001
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 43873 62 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0
[pid=11985] vsize: 29940
Current children cumulated CPU time (s) 439.35
Current children cumulated vsize (Kb) 32064

[startup+450.054 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12001
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 44874 62 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223072 134557662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0
[pid=11985] vsize: 29940
Current children cumulated CPU time (s) 449.36
Current children cumulated vsize (Kb) 32064

[startup+460.055 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12001
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 45874 62 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0
[pid=11985] vsize: 29940
Current children cumulated CPU time (s) 459.36
Current children cumulated vsize (Kb) 32064

[startup+470.056 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12001
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 46874 63 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0
[pid=11985] vsize: 29940
Current children cumulated CPU time (s) 469.37
Current children cumulated vsize (Kb) 32064

[startup+480.057 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12001
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 47874 63 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0
[pid=11985] vsize: 29940
Current children cumulated CPU time (s) 479.37
Current children cumulated vsize (Kb) 32064

[startup+490.057 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12003
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 48874 63 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0
[pid=11985] vsize: 29940
Current children cumulated CPU time (s) 489.37
Current children cumulated vsize (Kb) 32064

[startup+500.059 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12003
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 49875 63 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0
[pid=11985] vsize: 29940
Current children cumulated CPU time (s) 499.38
Current children cumulated vsize (Kb) 32064

[startup+510.06 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12003
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 50875 63 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0
[pid=11985] vsize: 29940
Current children cumulated CPU time (s) 509.38
Current children cumulated vsize (Kb) 32064

[startup+520.061 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12003
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 51875 63 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0
[pid=11985] vsize: 29940
Current children cumulated CPU time (s) 519.38
Current children cumulated vsize (Kb) 32064

[startup+530.062 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12003
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7422 0 0 0 52871 65 0 0 25 0 1 0 1841311767 31490048 7356 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7688 7356 145 145 0 7543 0
[pid=11985] vsize: 30752
Current children cumulated CPU time (s) 529.36
Current children cumulated vsize (Kb) 32876

[startup+540.063 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12003
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 53869 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0
[pid=11985] vsize: 31224
Current children cumulated CPU time (s) 539.35
Current children cumulated vsize (Kb) 33348

[startup+550.064 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12005
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 54869 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0
[pid=11985] vsize: 31224
Current children cumulated CPU time (s) 549.35
Current children cumulated vsize (Kb) 33348

[startup+560.064 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12005
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 55870 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0
[pid=11985] vsize: 31224
Current children cumulated CPU time (s) 559.36
Current children cumulated vsize (Kb) 33348

[startup+570.065 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12005
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 56870 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0
[pid=11985] vsize: 31224
Current children cumulated CPU time (s) 569.36
Current children cumulated vsize (Kb) 33348

[startup+580.066 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12005
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 57870 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0
[pid=11985] vsize: 31224
Current children cumulated CPU time (s) 579.36
Current children cumulated vsize (Kb) 33348

[startup+590.067 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12005
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 58870 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0
[pid=11985] vsize: 31224
Current children cumulated CPU time (s) 589.36
Current children cumulated vsize (Kb) 33348

[startup+600.069 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12005
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 59870 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0
[pid=11985] vsize: 31224
Current children cumulated CPU time (s) 599.36
Current children cumulated vsize (Kb) 33348

[startup+610.07 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12007
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 60871 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0
[pid=11985] vsize: 31224
Current children cumulated CPU time (s) 609.37
Current children cumulated vsize (Kb) 33348

[startup+620.072 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12007
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 61871 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0
[pid=11985] vsize: 31224
Current children cumulated CPU time (s) 619.37
Current children cumulated vsize (Kb) 33348

[startup+630.073 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12007
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 62871 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0
[pid=11985] vsize: 31224
Current children cumulated CPU time (s) 629.37
Current children cumulated vsize (Kb) 33348

[startup+640.073 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12007
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 63871 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0
[pid=11985] vsize: 31224
Current children cumulated CPU time (s) 639.37
Current children cumulated vsize (Kb) 33348

[startup+650.074 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12007
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7547 0 0 0 64872 66 0 0 25 0 1 0 1841311767 32006144 7481 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 7814 7481 145 145 0 7669 0
[pid=11985] vsize: 31256
Current children cumulated CPU time (s) 649.38
Current children cumulated vsize (Kb) 33380

[startup+660.075 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12007
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7549 0 0 0 65871 67 0 0 25 0 1 0 1841311767 32006144 7483 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 7814 7483 145 145 0 7669 0
[pid=11985] vsize: 31256
Current children cumulated CPU time (s) 659.38
Current children cumulated vsize (Kb) 33380

[startup+670.076 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12009
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7640 0 0 0 66869 67 0 0 25 0 1 0 1841311767 32407552 7574 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/11985/statm): 7912 7574 145 145 0 7767 0
[pid=11985] vsize: 31648
Current children cumulated CPU time (s) 669.36
Current children cumulated vsize (Kb) 33772

[startup+680.077 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12009
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7882 0 0 0 67864 70 0 0 25 0 1 0 1841311767 33382400 7816 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8150 7816 145 145 0 8005 0
[pid=11985] vsize: 32600
Current children cumulated CPU time (s) 679.34
Current children cumulated vsize (Kb) 34724

[startup+690.078 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12009
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8123 0 0 0 68859 72 0 0 25 0 1 0 1841311767 34369536 8057 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8391 8057 145 145 0 8246 0
[pid=11985] vsize: 33564
Current children cumulated CPU time (s) 689.31
Current children cumulated vsize (Kb) 35688

[startup+700.079 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12009
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8139 0 0 0 69859 72 0 0 25 0 1 0 1841311767 34435072 8073 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8407 8073 145 145 0 8262 0
[pid=11985] vsize: 33628
Current children cumulated CPU time (s) 699.31
Current children cumulated vsize (Kb) 35752

[startup+710.08 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12009
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8145 0 0 0 70860 72 0 0 25 0 1 0 1841311767 34467840 8079 4294967295 134512640 135094434 3221224448 3221223120 134556288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8415 8079 145 145 0 8270 0
[pid=11985] vsize: 33660
Current children cumulated CPU time (s) 709.32
Current children cumulated vsize (Kb) 35784

[startup+720.08 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12009
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8152 0 0 0 71860 72 0 0 25 0 1 0 1841311767 34500608 8086 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8423 8086 145 145 0 8278 0
[pid=11985] vsize: 33692
Current children cumulated CPU time (s) 719.32
Current children cumulated vsize (Kb) 35816

[startup+730.081 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12011
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8152 0 0 0 72860 72 0 0 25 0 1 0 1841311767 34500608 8086 4294967295 134512640 135094434 3221224448 3221223040 134557016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8423 8086 145 145 0 8278 0
[pid=11985] vsize: 33692
Current children cumulated CPU time (s) 729.32
Current children cumulated vsize (Kb) 35816

[startup+740.082 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12011
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8153 0 0 0 73860 72 0 0 25 0 1 0 1841311767 34500608 8087 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8423 8087 145 145 0 8278 0
[pid=11985] vsize: 33692
Current children cumulated CPU time (s) 739.32
Current children cumulated vsize (Kb) 35816

[startup+750.083 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12011
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8160 0 0 0 74860 72 0 0 25 0 1 0 1841311767 34533376 8094 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8431 8094 145 145 0 8286 0
[pid=11985] vsize: 33724
Current children cumulated CPU time (s) 749.32
Current children cumulated vsize (Kb) 35848

[startup+760.084 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12011
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8160 0 0 0 75860 72 0 0 25 0 1 0 1841311767 34533376 8094 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8431 8094 145 145 0 8286 0
[pid=11985] vsize: 33724
Current children cumulated CPU time (s) 759.32
Current children cumulated vsize (Kb) 35848

[startup+770.086 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12011
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8165 0 0 0 76861 72 0 0 25 0 1 0 1841311767 34566144 8099 4294967295 134512640 135094434 3221224448 3221223104 134557804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8439 8099 145 145 0 8294 0
[pid=11985] vsize: 33756
Current children cumulated CPU time (s) 769.33
Current children cumulated vsize (Kb) 35880

[startup+780.087 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12011
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8166 0 0 0 77861 72 0 0 25 0 1 0 1841311767 34566144 8100 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8439 8100 145 145 0 8294 0
[pid=11985] vsize: 33756
Current children cumulated CPU time (s) 779.33
Current children cumulated vsize (Kb) 35880

[startup+790.087 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12013
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8166 0 0 0 78860 73 0 0 25 0 1 0 1841311767 34566144 8100 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8439 8100 145 145 0 8294 0
[pid=11985] vsize: 33756
Current children cumulated CPU time (s) 789.33
Current children cumulated vsize (Kb) 35880

[startup+800.089 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12013
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8176 0 0 0 79860 74 0 0 25 0 1 0 1841311767 34631680 8110 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8455 8110 145 145 0 8310 0
[pid=11985] vsize: 33820
Current children cumulated CPU time (s) 799.34
Current children cumulated vsize (Kb) 35944

[startup+810.09 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12013
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8282 0 0 0 80858 75 0 0 25 0 1 0 1841311767 35090432 8216 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8567 8216 145 145 0 8422 0
[pid=11985] vsize: 34268
Current children cumulated CPU time (s) 809.33
Current children cumulated vsize (Kb) 36392

[startup+820.091 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12013
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8519 0 0 0 81852 78 0 0 25 0 1 0 1841311767 36069376 8453 4294967295 134512640 135094434 3221224448 3221223120 134555795 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 8806 8453 145 145 0 8661 0
[pid=11985] vsize: 35224
Current children cumulated CPU time (s) 819.3
Current children cumulated vsize (Kb) 37348

[startup+830.092 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12013
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8766 0 0 0 82848 80 0 0 25 0 1 0 1841311767 37085184 8700 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9054 8700 145 145 0 8909 0
[pid=11985] vsize: 36216
Current children cumulated CPU time (s) 829.28
Current children cumulated vsize (Kb) 38340

[startup+840.093 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12013
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8870 0 0 0 83846 81 0 0 25 0 1 0 1841311767 37502976 8804 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9156 8804 145 145 0 9011 0
[pid=11985] vsize: 36624
Current children cumulated CPU time (s) 839.27
Current children cumulated vsize (Kb) 38748

[startup+850.093 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12015
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8870 0 0 0 84846 81 0 0 25 0 1 0 1841311767 37502976 8804 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9156 8804 145 145 0 9011 0
[pid=11985] vsize: 36624
Current children cumulated CPU time (s) 849.27
Current children cumulated vsize (Kb) 38748

[startup+860.094 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12015
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8880 0 0 0 85846 81 0 0 25 0 1 0 1841311767 37568512 8814 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9172 8814 145 145 0 9027 0
[pid=11985] vsize: 36688
Current children cumulated CPU time (s) 859.27
Current children cumulated vsize (Kb) 38812

[startup+870.096 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12015
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8881 0 0 0 86847 81 0 0 25 0 1 0 1841311767 37568512 8815 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9172 8815 145 145 0 9027 0
[pid=11985] vsize: 36688
Current children cumulated CPU time (s) 869.28
Current children cumulated vsize (Kb) 38812

[startup+880.097 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12015
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8894 0 0 0 87847 82 0 0 25 0 1 0 1841311767 37634048 8828 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9188 8828 145 145 0 9043 0
[pid=11985] vsize: 36752
Current children cumulated CPU time (s) 879.29
Current children cumulated vsize (Kb) 38876

[startup+890.098 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12015
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8895 0 0 0 88847 82 0 0 25 0 1 0 1841311767 37634048 8829 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9188 8829 145 145 0 9043 0
[pid=11985] vsize: 36752
Current children cumulated CPU time (s) 889.29
Current children cumulated vsize (Kb) 38876

[startup+900.099 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12015
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8895 0 0 0 89847 82 0 0 25 0 1 0 1841311767 37634048 8829 4294967295 134512640 135094434 3221224448 3221223040 134556937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9188 8829 145 145 0 9043 0
[pid=11985] vsize: 36752
Current children cumulated CPU time (s) 899.29
Current children cumulated vsize (Kb) 38876

[startup+910.1 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12017
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8895 0 0 0 90847 82 0 0 25 0 1 0 1841311767 37634048 8829 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9188 8829 145 145 0 9043 0
[pid=11985] vsize: 36752
Current children cumulated CPU time (s) 909.29
Current children cumulated vsize (Kb) 38876

[startup+920.102 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12017
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8896 0 0 0 91848 82 0 0 25 0 1 0 1841311767 37634048 8830 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9188 8830 145 145 0 9043 0
[pid=11985] vsize: 36752
Current children cumulated CPU time (s) 919.3
Current children cumulated vsize (Kb) 38876

[startup+930.103 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12017
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8896 0 0 0 92848 82 0 0 25 0 1 0 1841311767 37634048 8830 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9188 8830 145 145 0 9043 0
[pid=11985] vsize: 36752
Current children cumulated CPU time (s) 929.3
Current children cumulated vsize (Kb) 38876

[startup+940.104 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12017
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8909 0 0 0 93848 82 0 0 25 0 1 0 1841311767 37699584 8843 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9204 8843 145 145 0 9059 0
[pid=11985] vsize: 36816
Current children cumulated CPU time (s) 939.3
Current children cumulated vsize (Kb) 38940

[startup+950.105 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12017
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8910 0 0 0 94848 82 0 0 25 0 1 0 1841311767 37699584 8844 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9204 8844 145 145 0 9059 0
[pid=11985] vsize: 36816
Current children cumulated CPU time (s) 949.3
Current children cumulated vsize (Kb) 38940

[startup+960.106 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12017
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8910 0 0 0 95848 82 0 0 25 0 1 0 1841311767 37699584 8844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9204 8844 145 145 0 9059 0
[pid=11985] vsize: 36816
Current children cumulated CPU time (s) 959.3
Current children cumulated vsize (Kb) 38940

[startup+970.107 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12019
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8911 0 0 0 96848 82 0 0 25 0 1 0 1841311767 37699584 8845 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9204 8845 145 145 0 9059 0
[pid=11985] vsize: 36816
Current children cumulated CPU time (s) 969.3
Current children cumulated vsize (Kb) 38940

[startup+980.109 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12019
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8913 0 0 0 97848 83 0 0 25 0 1 0 1841311767 37699584 8847 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9204 8847 145 145 0 9059 0
[pid=11985] vsize: 36816
Current children cumulated CPU time (s) 979.31
Current children cumulated vsize (Kb) 38940

[startup+990.11 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12019
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9003 0 0 0 98847 83 0 0 25 0 1 0 1841311767 38064128 8937 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9293 8937 145 145 0 9148 0
[pid=11985] vsize: 37172
Current children cumulated CPU time (s) 989.3
Current children cumulated vsize (Kb) 39296

[startup+1000.11 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12019
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9200 0 0 0 99843 85 0 0 25 0 1 0 1841311767 38895616 9134 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9496 9134 145 145 0 9351 0
[pid=11985] vsize: 37984
Current children cumulated CPU time (s) 999.28
Current children cumulated vsize (Kb) 40108

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12019
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9252 0 0 0 100842 85 0 0 25 0 1 0 1841311767 39108608 9186 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9186 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1009.27
Current children cumulated vsize (Kb) 40316

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12019
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9252 0 0 0 101842 86 0 0 25 0 1 0 1841311767 39108608 9186 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9186 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1019.28
Current children cumulated vsize (Kb) 40316

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12021
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9252 0 0 0 102842 86 0 0 25 0 1 0 1841311767 39108608 9186 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9186 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1029.28
Current children cumulated vsize (Kb) 40316

[startup+1040.12 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12021
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9252 0 0 0 103842 86 0 0 25 0 1 0 1841311767 39108608 9186 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9186 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1039.28
Current children cumulated vsize (Kb) 40316

[startup+1050.12 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12021
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9252 0 0 0 104842 86 0 0 25 0 1 0 1841311767 39108608 9186 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9186 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1049.28
Current children cumulated vsize (Kb) 40316

[startup+1060.12 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12021
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9252 0 0 0 105843 86 0 0 25 0 1 0 1841311767 39108608 9186 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9186 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1059.29
Current children cumulated vsize (Kb) 40316

[startup+1070.12 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12021
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9253 0 0 0 106843 86 0 0 25 0 1 0 1841311767 39108608 9187 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9187 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1069.29
Current children cumulated vsize (Kb) 40316

[startup+1080.12 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12021
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9254 0 0 0 107843 86 0 0 25 0 1 0 1841311767 39108608 9188 4294967295 134512640 135094434 3221224448 3221223060 134563130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9188 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1079.29
Current children cumulated vsize (Kb) 40316

[startup+1090.12 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12023
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9254 0 0 0 108843 86 0 0 25 0 1 0 1841311767 39108608 9188 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9188 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1089.29
Current children cumulated vsize (Kb) 40316

[startup+1100.12 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12023
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9254 0 0 0 109843 86 0 0 25 0 1 0 1841311767 39108608 9188 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9188 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1099.29
Current children cumulated vsize (Kb) 40316

[startup+1110.12 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12023
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9254 0 0 0 110844 86 0 0 25 0 1 0 1841311767 39108608 9188 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9188 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1109.3
Current children cumulated vsize (Kb) 40316

[startup+1120.12 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12023
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9254 0 0 0 111844 86 0 0 25 0 1 0 1841311767 39108608 9188 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9188 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1119.3
Current children cumulated vsize (Kb) 40316

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12023
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9255 0 0 0 112844 87 0 0 25 0 1 0 1841311767 39108608 9189 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9548 9189 145 145 0 9403 0
[pid=11985] vsize: 38192
Current children cumulated CPU time (s) 1129.31
Current children cumulated vsize (Kb) 40316

[startup+1140.13 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12023
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9264 0 0 0 113844 87 0 0 25 0 1 0 1841311767 39174144 9198 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9564 9198 145 145 0 9419 0
[pid=11985] vsize: 38256
Current children cumulated CPU time (s) 1139.31
Current children cumulated vsize (Kb) 40380

[startup+1150.13 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12025
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9275 0 0 0 114844 87 0 0 25 0 1 0 1841311767 39239680 9209 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9580 9209 145 145 0 9435 0
[pid=11985] vsize: 38320
Current children cumulated CPU time (s) 1149.31
Current children cumulated vsize (Kb) 40444

[startup+1160.13 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12025
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9294 0 0 0 115844 87 0 0 25 0 1 0 1841311767 39370752 9228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9612 9228 145 145 0 9467 0
[pid=11985] vsize: 38448
Current children cumulated CPU time (s) 1159.31
Current children cumulated vsize (Kb) 40572

[startup+1170.13 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12025
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9295 0 0 0 116845 87 0 0 25 0 1 0 1841311767 39370752 9229 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9612 9229 145 145 0 9467 0
[pid=11985] vsize: 38448
Current children cumulated CPU time (s) 1169.32
Current children cumulated vsize (Kb) 40572

[startup+1180.13 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12025
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9304 0 0 0 117845 87 0 0 25 0 1 0 1841311767 39436288 9238 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9628 9238 145 145 0 9483 0
[pid=11985] vsize: 38512
Current children cumulated CPU time (s) 1179.32
Current children cumulated vsize (Kb) 40636

[startup+1190.13 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12025
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9315 0 0 0 118845 87 0 0 25 0 1 0 1841311767 39501824 9249 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9644 9249 145 145 0 9499 0
[pid=11985] vsize: 38576
Current children cumulated CPU time (s) 1189.32
Current children cumulated vsize (Kb) 40700

[startup+1200.13 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12025
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9392 0 0 0 119844 88 0 0 25 0 1 0 1841311767 39800832 9326 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9717 9326 145 145 0 9572 0
[pid=11985] vsize: 38868
Current children cumulated CPU time (s) 1199.32
Current children cumulated vsize (Kb) 40992

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12027
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9559 0 0 0 120840 89 0 0 25 0 1 0 1841311767 40488960 9493 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9885 9493 145 145 0 9740 0
[pid=11985] vsize: 39540
Current children cumulated CPU time (s) 1209.29
Current children cumulated vsize (Kb) 41664



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.14 s]
Raw data (loadavg): 0.99 0.99 0.97 2/58 12027
Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/11981/statm): 531 226 485 147 0 384 0
[pid=11981] vsize: 2124
Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) T 11981 11981 9102 0 -1 0 9559 0 0 0 120840 89 0 0 25 0 1 0 1841311767 40488960 9493 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/11985/statm): 9885 9493 145 145 0 9740 0
[pid=11985] vsize: 39540
Current children cumulated CPU time (s) 1209.29
Current children cumulated vsize (Kb) 41664

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1209.32
CPU user time (s): 1208.41
CPU system time (s): 0.913861
CPU usage (%): 99.9312
Max. virtual memory (cumulated for all children) (Kb): 41664

Verifier Data

ERROR: no interpretation found !