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/synthesis-ptl-cmos-circuits/normalized-my_adder.opb
MD5SUMfe8f615a95a6852516985b8e3e78bd85
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 4561
Optimality of the best value was proved YES
Number of terms in the objective function 577
Biggest coefficient in the objective function 61
Number of bits for the biggest coefficient in the objective function 6
Sum of the numbers in the objective function 24510
Number of bits of the sum of numbers in the objective function 15
Biggest number in a constraint 61
Number of bits of the biggest number in a constraint 6
Biggest sum of numbers in a constraint 24510
Number of bits of the biggest sum of numbers15
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark45.2981
Number of variables577
Total number of constraints1322
Number of constraints which are clauses1306
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints16
Minimum length of a constraint2
Maximum length of a constraint17

Trace number 2219

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        917672 kB
Buffers:         33656 kB
Cached:          54392 kB
SwapCached:        692 kB
Active:          46740 kB
Inactive:        43908 kB
HighTotal:      131008 kB
HighFree:        73500 kB
LowTotal:       903652 kB
LowFree:        844172 kB
SwapTotal:     2097136 kB
SwapFree:      2095920 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            20572 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:31:39 (client local time) WITH STATUS 10 IN 1207.97 SECONDS
stats: 2598 7 1207.97 10

Solver Data

c Parsing PB file...
c Converting 1322 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 |    1322     4977 |     440       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 6274
c ---[   0]---> Sorter-cost:87831     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |  210130   492551 |   70043       1        7     7.0 |  0.000 % |
c |       101 |  209639   491465 |   77047      98     1983    20.2 |  0.188 % |
c |       251 |  209398   490919 |   84752     246     3047    12.4 |  0.270 % |
c |       477 |  209398   490919 |   93227     472     5320    11.3 |  0.270 % |
c |       814 |  209398   490919 |  102549     809     7426     9.2 |  0.270 % |
c |      1320 |  209398   490919 |  112804    1315    12893     9.8 |  0.270 % |
c |      2079 |  208099   487975 |  124085    2062    18966     9.2 |  0.850 % |
c |      3223 |  207777   487250 |  136493    3203    75259    23.5 |  1.015 % |
c |      4934 |  207777   487250 |  150143    4914   465375    94.7 |  1.015 % |
c |      7496 |  207777   487250 |  165157    7476   523941    70.1 |  1.015 % |
c |     11343 |  207124   485763 |  181673   11316   605974    53.6 |  1.304 % |
c ==============================================================================
c Found solution: 6030
c ---[   0]---> Sorter-cost:63107     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15902 |  341282   799222 |  113760   15812   677541    42.8 |  1.304 % |
c |     16002 |  341282   799222 |  125136   15912   678586    42.6 |  1.292 % |
c |     16153 |  341282   799222 |  137649   16063   680125    42.3 |  1.292 % |
c |     16378 |  341282   799222 |  151414   16288   682659    41.9 |  1.292 % |
c |     16715 |  341282   799222 |  166556   16625   686273    41.3 |  1.292 % |
c |     17222 |  341282   799222 |  183211   17132   689710    40.3 |  1.292 % |
c |     17982 |  341282   799222 |  201532   17892   701677    39.2 |  1.292 % |
c ==============================================================================
c Found solution: 5941
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18575 |  341328   799730 |  113776   18485   726783    39.3 |  1.292 % |
c |     18675 |  341311   799693 |  125153   18584   727472    39.1 |  1.297 % |
c |     18825 |  341311   799693 |  137668   18734   728419    38.9 |  1.297 % |
c |     19050 |  341311   799693 |  151435   18959   730280    38.5 |  1.297 % |
c |     19388 |  341311   799693 |  166579   19297   732516    38.0 |  1.297 % |
c |     19894 |  341311   799693 |  183237   19803   738567    37.3 |  1.297 % |
c |     20653 |  341060   799139 |  201561   20560   748577    36.4 |  1.351 % |
c |     21792 |  341060   799139 |  221717   21699   757149    34.9 |  1.351 % |
c |     23500 |  341060   799139 |  243888   23407   808068    34.5 |  1.351 % |
c |     26064 |  340058   796875 |  268277   25935   888362    34.3 |  1.591 % |
c |     29909 |  340058   796875 |  295105   29780   993861    33.4 |  1.591 % |
c |     35675 |  340058   796875 |  324616   35546  1611580    45.3 |  1.591 % |
c |     44326 |  340058   796875 |  357077   44197  2011857    45.5 |  1.591 % |
c |     57300 |  339999   796741 |  392785   57162  2368847    41.4 |  1.609 % |
c |     76763 |  339999   796741 |  432064   76625  7374052    96.2 |  1.609 % |
c |    105956 |  339999   796741 |  475270  105818  9897084    93.5 |  1.609 % |
c ==============================================================================
c Found solution: 5700
c ---[   0]---> Sorter-cost:64909     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108372 |  479644  1122919 |  159881  108234 10027671    92.6 |  1.609 % |
c |    108473 |  479644  1122919 |  175869  108335 10028620    92.6 |  1.141 % |
c |    108623 |  479644  1122919 |  193456  108485 10030258    92.5 |  1.141 % |
c |    108848 |  479644  1122919 |  212801  108710 10032710    92.3 |  1.141 % |
c |    109185 |  479644  1122919 |  234081  109047 10045641    92.1 |  1.141 % |
c |    109691 |  479498  1122590 |  257489  109542 10064209    91.9 |  1.162 % |
c |    110451 |  479498  1122590 |  283238  110302 10074504    91.3 |  1.162 % |
c |    111590 |  479498  1122590 |  311562  111441 10093566    90.6 |  1.162 % |
c |    113298 |  479498  1122590 |  342719  113149 10108665    89.3 |  1.162 % |
c |    115860 |  479488  1122570 |  376991  115708 10180504    88.0 |  1.165 % |
c |    119704 |  479488  1122570 |  414690  119552 10487501    87.7 |  1.165 % |
c |    125470 |  479488  1122570 |  456159  125318 11610478    92.6 |  1.165 % |
c |    134119 |  479488  1122570 |  501775  133967 11828437    88.3 |  1.165 % |
c |    147093 |  479488  1122570 |  551952  146941 12479339    84.9 |  1.165 % |
c |    166556 |  479456  1122498 |  607147  166403 15031220    90.3 |  1.175 % |

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/10833/stat): 10833 (minisat+_script) R 10832 10833 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785077480 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/10833/statm): 174 3 169 147 0 27 0
[pid=10833] 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=10834
New process pid=10835
New process pid=10836
One traced child (pid=10835) exited with status: 0
execve syscall for /bin/sed executable
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=10836) exited with status: 0
One traced child (pid=10834) exited with status: 0
New process pid=10837
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-my_adder.opb

[startup+10.0045 s]
Raw data (loadavg): 0.93 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 7061 0 0 0 942 28 0 0 25 0 1 0 1785077485 30978048 6583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 7563 6583 145 145 0 7418 0
[pid=10837] vsize: 30252
Current children cumulated CPU time (s) 9.71
Current children cumulated vsize (Kb) 32376

[startup+20.0052 s]
Raw data (loadavg): 0.94 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 7382 0 0 0 1938 29 0 0 25 0 1 0 1785077485 32321536 6904 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 7891 6904 145 145 0 7746 0
[pid=10837] vsize: 31564
Current children cumulated CPU time (s) 19.68
Current children cumulated vsize (Kb) 33688

[startup+30.0071 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 7572 0 0 0 2935 31 0 0 25 0 1 0 1785077485 33116160 7094 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 8085 7094 145 145 0 7940 0
[pid=10837] vsize: 32340
Current children cumulated CPU time (s) 29.67
Current children cumulated vsize (Kb) 34464

[startup+40.0079 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 7686 0 0 0 3932 32 0 0 25 0 1 0 1785077485 33599488 7208 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 8203 7208 145 145 0 8058 0
[pid=10837] vsize: 32812
Current children cumulated CPU time (s) 39.65
Current children cumulated vsize (Kb) 34936

[startup+50.0087 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 7757 0 0 0 4930 33 0 0 25 0 1 0 1785077485 33878016 7279 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 8271 7279 145 145 0 8126 0
[pid=10837] vsize: 33084
Current children cumulated CPU time (s) 49.64
Current children cumulated vsize (Kb) 35208

[startup+60.0105 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 11987 0 0 0 5895 50 0 0 25 0 1 0 1785077485 57524224 11384 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 14044 11384 145 145 0 13899 0
[pid=10837] vsize: 56176
Current children cumulated CPU time (s) 59.46
Current children cumulated vsize (Kb) 58300

[startup+70.0113 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12336 0 0 0 6891 52 0 0 25 0 1 0 1785077485 58277888 11691 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 14228 11691 145 145 0 14083 0
[pid=10837] vsize: 56912
Current children cumulated CPU time (s) 69.44
Current children cumulated vsize (Kb) 59036

[startup+80.0131 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12366 0 0 0 7890 53 0 0 25 0 1 0 1785077485 58388480 11721 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 14255 11721 145 145 0 14110 0
[pid=10837] vsize: 57020
Current children cumulated CPU time (s) 79.44
Current children cumulated vsize (Kb) 59144

[startup+90.0139 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12450 0 0 0 8888 54 0 0 25 0 1 0 1785077485 58724352 11805 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 14337 11805 145 145 0 14192 0
[pid=10837] vsize: 57348
Current children cumulated CPU time (s) 89.43
Current children cumulated vsize (Kb) 59472

[startup+100.014 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12490 0 0 0 9887 54 0 0 25 0 1 0 1785077485 58888192 11845 4294967295 134512640 135094434 3221224448 3221223104 134557818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 14377 11845 145 145 0 14232 0
[pid=10837] vsize: 57508
Current children cumulated CPU time (s) 99.42
Current children cumulated vsize (Kb) 59632

[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12542 0 0 0 10887 55 0 0 25 0 1 0 1785077485 59092992 11897 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 14427 11897 145 145 0 14282 0
[pid=10837] vsize: 57708
Current children cumulated CPU time (s) 109.43
Current children cumulated vsize (Kb) 59832

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12609 0 0 0 11886 55 0 0 25 0 1 0 1785077485 59359232 11964 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 14492 11964 145 145 0 14347 0
[pid=10837] vsize: 57968
Current children cumulated CPU time (s) 119.42
Current children cumulated vsize (Kb) 60092

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12720 0 0 0 12884 56 0 0 25 0 1 0 1785077485 59932672 12075 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 14632 12075 145 145 0 14487 0
[pid=10837] vsize: 58528
Current children cumulated CPU time (s) 129.41
Current children cumulated vsize (Kb) 60652

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12886 0 0 0 13881 57 0 0 25 0 1 0 1785077485 60608512 12241 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 14797 12241 145 145 0 14652 0
[pid=10837] vsize: 59188
Current children cumulated CPU time (s) 139.39
Current children cumulated vsize (Kb) 61312

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13124 0 0 0 14877 59 0 0 25 0 1 0 1785077485 61579264 12479 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 15034 12479 145 145 0 14889 0
[pid=10837] vsize: 60136
Current children cumulated CPU time (s) 149.37
Current children cumulated vsize (Kb) 62260

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13306 0 0 0 15875 60 0 0 25 0 1 0 1785077485 62320640 12661 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 15215 12661 145 145 0 15070 0
[pid=10837] vsize: 60860
Current children cumulated CPU time (s) 159.36
Current children cumulated vsize (Kb) 62984

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13352 0 0 0 16874 60 0 0 25 0 1 0 1785077485 62504960 12707 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 15260 12707 145 145 0 15115 0
[pid=10837] vsize: 61040
Current children cumulated CPU time (s) 169.35
Current children cumulated vsize (Kb) 63164

[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13415 0 0 0 17873 61 0 0 25 0 1 0 1785077485 62754816 12770 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 15321 12770 145 145 0 15176 0
[pid=10837] vsize: 61284
Current children cumulated CPU time (s) 179.35
Current children cumulated vsize (Kb) 63408

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13539 0 0 0 18870 62 0 0 25 0 1 0 1785077485 63254528 12894 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 15443 12894 145 145 0 15298 0
[pid=10837] vsize: 61772
Current children cumulated CPU time (s) 189.33
Current children cumulated vsize (Kb) 63896

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13697 0 0 0 19866 63 0 0 25 0 1 0 1785077485 63897600 13052 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 15600 13052 145 145 0 15455 0
[pid=10837] vsize: 62400
Current children cumulated CPU time (s) 199.3
Current children cumulated vsize (Kb) 64524

[startup+210.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13782 0 0 0 20865 64 0 0 25 0 1 0 1785077485 64233472 13137 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 15682 13137 145 145 0 15537 0
[pid=10837] vsize: 62728
Current children cumulated CPU time (s) 209.3
Current children cumulated vsize (Kb) 64852

[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13901 0 0 0 21863 65 0 0 25 0 1 0 1785077485 64708608 13256 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 15798 13256 145 145 0 15653 0
[pid=10837] vsize: 63192
Current children cumulated CPU time (s) 219.29
Current children cumulated vsize (Kb) 65316

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13950 0 0 0 22862 65 0 0 25 0 1 0 1785077485 64905216 13305 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 15846 13305 145 145 0 15701 0
[pid=10837] vsize: 63384
Current children cumulated CPU time (s) 229.28
Current children cumulated vsize (Kb) 65508

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14016 0 0 0 23860 66 0 0 25 0 1 0 1785077485 65167360 13371 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 15910 13371 145 145 0 15765 0
[pid=10837] vsize: 63640
Current children cumulated CPU time (s) 239.27
Current children cumulated vsize (Kb) 65764

[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14084 0 0 0 24859 66 0 0 25 0 1 0 1785077485 65437696 13439 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 15976 13439 145 145 0 15831 0
[pid=10837] vsize: 63904
Current children cumulated CPU time (s) 249.26
Current children cumulated vsize (Kb) 66028

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14162 0 0 0 25858 67 0 0 25 0 1 0 1785077485 65748992 13517 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 16052 13517 145 145 0 15907 0
[pid=10837] vsize: 64208
Current children cumulated CPU time (s) 259.26
Current children cumulated vsize (Kb) 66332

[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14228 0 0 0 26856 67 0 0 25 0 1 0 1785077485 66015232 13583 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 16117 13583 145 145 0 15972 0
[pid=10837] vsize: 64468
Current children cumulated CPU time (s) 269.24
Current children cumulated vsize (Kb) 66592

[startup+280.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14294 0 0 0 27854 68 0 0 25 0 1 0 1785077485 66277376 13649 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 16181 13649 145 145 0 16036 0
[pid=10837] vsize: 64724
Current children cumulated CPU time (s) 279.23
Current children cumulated vsize (Kb) 66848

[startup+290.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14447 0 0 0 28852 69 0 0 25 0 1 0 1785077485 66899968 13802 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 16333 13802 145 145 0 16188 0
[pid=10837] vsize: 65332
Current children cumulated CPU time (s) 289.22
Current children cumulated vsize (Kb) 67456

[startup+300.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14679 0 0 0 29849 70 0 0 25 0 1 0 1785077485 67846144 14034 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 16564 14034 145 145 0 16419 0
[pid=10837] vsize: 66256
Current children cumulated CPU time (s) 299.2
Current children cumulated vsize (Kb) 68380

[startup+310.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14865 0 0 0 30848 71 0 0 25 0 1 0 1785077485 68608000 14220 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 16750 14220 145 145 0 16605 0
[pid=10837] vsize: 67000
Current children cumulated CPU time (s) 309.2
Current children cumulated vsize (Kb) 69124

[startup+320.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 15123 0 0 0 31845 73 0 0 25 0 1 0 1785077485 69660672 14478 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 17007 14478 145 145 0 16862 0
[pid=10837] vsize: 68028
Current children cumulated CPU time (s) 319.19
Current children cumulated vsize (Kb) 70152

[startup+330.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 15309 0 0 0 32843 73 0 0 25 0 1 0 1785077485 70418432 14664 4294967295 134512640 135094434 3221224448 3221223104 134558286 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 17192 14664 145 145 0 17047 0
[pid=10837] vsize: 68768
Current children cumulated CPU time (s) 329.17
Current children cumulated vsize (Kb) 70892

[startup+340.037 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 15574 0 0 0 33839 76 0 0 25 0 1 0 1785077485 71503872 14929 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 17457 14929 145 145 0 17312 0
[pid=10837] vsize: 69828
Current children cumulated CPU time (s) 339.16
Current children cumulated vsize (Kb) 71952

[startup+350.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 15822 0 0 0 34836 77 0 0 25 0 1 0 1785077485 72519680 15177 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 17705 15177 145 145 0 17560 0
[pid=10837] vsize: 70820
Current children cumulated CPU time (s) 349.14
Current children cumulated vsize (Kb) 72944

[startup+360.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 16058 0 0 0 35832 78 0 0 25 0 1 0 1785077485 73482240 15413 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 17940 15413 145 145 0 17795 0
[pid=10837] vsize: 71760
Current children cumulated CPU time (s) 359.11
Current children cumulated vsize (Kb) 73884

[startup+370.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) T 10833 10833 31778 0 -1 0 16307 0 0 0 36830 79 0 0 25 0 1 0 1785077485 74498048 15662 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/10837/statm): 18188 15662 145 145 0 18043 0
[pid=10837] vsize: 72752
Current children cumulated CPU time (s) 369.1
Current children cumulated vsize (Kb) 74876

[startup+380.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 16518 0 0 0 37827 80 0 0 25 0 1 0 1785077485 75362304 15873 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 18399 15873 145 145 0 18254 0
[pid=10837] vsize: 73596
Current children cumulated CPU time (s) 379.08
Current children cumulated vsize (Kb) 75720

[startup+390.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 16732 0 0 0 38824 82 0 0 25 0 1 0 1785077485 76496896 16087 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 18676 16087 145 145 0 18531 0
[pid=10837] vsize: 74704
Current children cumulated CPU time (s) 389.07
Current children cumulated vsize (Kb) 76828

[startup+400.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 16966 0 0 0 39821 83 0 0 25 0 1 0 1785077485 77455360 16321 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 18910 16321 145 145 0 18765 0
[pid=10837] vsize: 75640
Current children cumulated CPU time (s) 399.05
Current children cumulated vsize (Kb) 77764

[startup+410.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 17165 0 0 0 40818 85 0 0 25 0 1 0 1785077485 78270464 16520 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 19109 16520 145 145 0 18964 0
[pid=10837] vsize: 76436
Current children cumulated CPU time (s) 409.04
Current children cumulated vsize (Kb) 78560

[startup+420.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 17391 0 0 0 41815 86 0 0 25 0 1 0 1785077485 79192064 16746 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 19334 16746 145 145 0 19189 0
[pid=10837] vsize: 77336
Current children cumulated CPU time (s) 419.02
Current children cumulated vsize (Kb) 79460

[startup+430.044 s]
Raw data (loadavg): 0.99 0.97 0.99 3/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 17644 0 0 0 42811 88 0 0 25 0 1 0 1785077485 80224256 16999 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 19586 16999 145 145 0 19441 0
[pid=10837] vsize: 78344
Current children cumulated CPU time (s) 429
Current children cumulated vsize (Kb) 80468

[startup+440.045 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 17889 0 0 0 43808 89 0 0 25 0 1 0 1785077485 81227776 17244 4294967295 134512640 135094434 3221224448 3221223136 134554705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 19831 17244 145 145 0 19686 0
[pid=10837] vsize: 79324
Current children cumulated CPU time (s) 438.98
Current children cumulated vsize (Kb) 81448

[startup+450.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 18073 0 0 0 44805 90 0 0 25 0 1 0 1785077485 81973248 17428 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 20013 17428 145 145 0 19868 0
[pid=10837] vsize: 80052
Current children cumulated CPU time (s) 448.96
Current children cumulated vsize (Kb) 82176

[startup+460.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 18313 0 0 0 45802 92 0 0 25 0 1 0 1785077485 82956288 17668 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 20253 17668 145 145 0 20108 0
[pid=10837] vsize: 81012
Current children cumulated CPU time (s) 458.95
Current children cumulated vsize (Kb) 83136

[startup+470.048 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 18458 0 0 0 46800 93 0 0 25 0 1 0 1785077485 83546112 17813 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 20397 17813 145 145 0 20252 0
[pid=10837] vsize: 81588
Current children cumulated CPU time (s) 468.94
Current children cumulated vsize (Kb) 83712

[startup+480.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 18717 0 0 0 47797 94 0 0 25 0 1 0 1785077485 84606976 18072 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 20656 18072 145 145 0 20511 0
[pid=10837] vsize: 82624
Current children cumulated CPU time (s) 478.92
Current children cumulated vsize (Kb) 84748

[startup+490.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 18979 0 0 0 48793 96 0 0 25 0 1 0 1785077485 85676032 18334 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 20917 18334 145 145 0 20772 0
[pid=10837] vsize: 83668
Current children cumulated CPU time (s) 488.9
Current children cumulated vsize (Kb) 85792

[startup+500.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 19216 0 0 0 49790 97 0 0 25 0 1 0 1785077485 86642688 18571 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 21153 18571 145 145 0 21008 0
[pid=10837] vsize: 84612
Current children cumulated CPU time (s) 498.88
Current children cumulated vsize (Kb) 86736

[startup+510.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 19277 0 0 0 50789 98 0 0 25 0 1 0 1785077485 86888448 18632 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 21213 18632 145 145 0 21068 0
[pid=10837] vsize: 84852
Current children cumulated CPU time (s) 508.88
Current children cumulated vsize (Kb) 86976

[startup+520.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 19345 0 0 0 51788 98 0 0 25 0 1 0 1785077485 87162880 18700 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 21280 18700 145 145 0 21135 0
[pid=10837] vsize: 85120
Current children cumulated CPU time (s) 518.87
Current children cumulated vsize (Kb) 87244

[startup+530.053 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 19516 0 0 0 52784 100 0 0 25 0 1 0 1785077485 87855104 18871 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 21449 18871 145 145 0 21304 0
[pid=10837] vsize: 85796
Current children cumulated CPU time (s) 528.85
Current children cumulated vsize (Kb) 87920

[startup+540.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 19768 0 0 0 53780 102 0 0 25 0 1 0 1785077485 88887296 19123 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 21701 19123 145 145 0 21556 0
[pid=10837] vsize: 86804
Current children cumulated CPU time (s) 538.83
Current children cumulated vsize (Kb) 88928

[startup+550.055 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 19946 0 0 0 54777 104 0 0 25 0 1 0 1785077485 89608192 19301 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 21877 19301 145 145 0 21732 0
[pid=10837] vsize: 87508
Current children cumulated CPU time (s) 548.82
Current children cumulated vsize (Kb) 89632

[startup+560.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 20229 0 0 0 55772 105 0 0 25 0 1 0 1785077485 90755072 19584 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 22157 19584 145 145 0 22012 0
[pid=10837] vsize: 88628
Current children cumulated CPU time (s) 558.78
Current children cumulated vsize (Kb) 90752

[startup+570.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 20481 0 0 0 56767 108 0 0 25 0 1 0 1785077485 91779072 19836 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 22407 19836 145 145 0 22262 0
[pid=10837] vsize: 89628
Current children cumulated CPU time (s) 568.76
Current children cumulated vsize (Kb) 91752

[startup+580.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 20684 0 0 0 57764 109 0 0 25 0 1 0 1785077485 92606464 20039 4294967295 134512640 135094434 3221224448 3221223040 134556853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 22609 20039 145 145 0 22464 0
[pid=10837] vsize: 90436
Current children cumulated CPU time (s) 578.74
Current children cumulated vsize (Kb) 92560

[startup+590.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 20867 0 0 0 58760 111 0 0 25 0 1 0 1785077485 93347840 20222 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 22790 20222 145 145 0 22645 0
[pid=10837] vsize: 91160
Current children cumulated CPU time (s) 588.72
Current children cumulated vsize (Kb) 93284

[startup+600.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 21036 0 0 0 59757 112 0 0 25 0 1 0 1785077485 94031872 20391 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10837/statm): 22957 20391 145 145 0 22812 0
[pid=10837] vsize: 91828
Current children cumulated CPU time (s) 598.7
Current children cumulated vsize (Kb) 93952

[startup+610.061 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 21265 0 0 0 60754 114 0 0 25 0 1 0 1785077485 94965760 20620 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 23185 20620 145 145 0 23040 0
[pid=10837] vsize: 92740
Current children cumulated CPU time (s) 608.69
Current children cumulated vsize (Kb) 94864

[startup+620.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 21435 0 0 0 61752 115 0 0 25 0 1 0 1785077485 95657984 20790 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 23354 20790 145 145 0 23209 0
[pid=10837] vsize: 93416
Current children cumulated CPU time (s) 618.68
Current children cumulated vsize (Kb) 95540

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 21537 0 0 0 62750 115 0 0 25 0 1 0 1785077485 96067584 20892 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 23454 20892 145 145 0 23309 0
[pid=10837] vsize: 93816
Current children cumulated CPU time (s) 628.66
Current children cumulated vsize (Kb) 95940

[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 21749 0 0 0 63746 117 0 0 25 0 1 0 1785077485 96915456 21104 4294967295 134512640 135094434 3221224448 3221223072 134557642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 23661 21104 145 145 0 23516 0
[pid=10837] vsize: 94644
Current children cumulated CPU time (s) 638.64
Current children cumulated vsize (Kb) 96768

[startup+650.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 21931 0 0 0 64742 119 0 0 25 0 1 0 1785077485 97648640 21286 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 23840 21286 145 145 0 23695 0
[pid=10837] vsize: 95360
Current children cumulated CPU time (s) 648.62
Current children cumulated vsize (Kb) 97484

[startup+660.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 22128 0 0 0 65737 121 0 0 25 0 1 0 1785077485 98443264 21483 4294967295 134512640 135094434 3221224448 3221223040 134556884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 24034 21483 145 145 0 23889 0
[pid=10837] vsize: 96136
Current children cumulated CPU time (s) 658.59
Current children cumulated vsize (Kb) 98260

[startup+670.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 26985 0 0 0 66699 140 0 0 25 0 1 0 1785077485 113901568 25968 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 27808 25968 145 145 0 27663 0
[pid=10837] vsize: 111232
Current children cumulated CPU time (s) 668.4
Current children cumulated vsize (Kb) 113356

[startup+680.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27063 0 0 0 67698 140 0 0 25 0 1 0 1785077485 114212864 26046 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 27884 26046 145 145 0 27739 0
[pid=10837] vsize: 111536
Current children cumulated CPU time (s) 678.39
Current children cumulated vsize (Kb) 113660

[startup+690.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27135 0 0 0 68697 141 0 0 25 0 1 0 1785077485 114511872 26118 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 27957 26118 145 145 0 27812 0
[pid=10837] vsize: 111828
Current children cumulated CPU time (s) 688.39
Current children cumulated vsize (Kb) 113952

[startup+700.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27211 0 0 0 69695 142 0 0 25 0 1 0 1785077485 114814976 26194 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 28031 26194 145 145 0 27886 0
[pid=10837] vsize: 112124
Current children cumulated CPU time (s) 698.38
Current children cumulated vsize (Kb) 114248

[startup+710.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27256 0 0 0 70694 142 0 0 25 0 1 0 1785077485 114991104 26239 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 28074 26239 145 145 0 27929 0
[pid=10837] vsize: 112296
Current children cumulated CPU time (s) 708.37
Current children cumulated vsize (Kb) 114420

[startup+720.069 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27313 0 0 0 71693 143 0 0 25 0 1 0 1785077485 115220480 26296 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 28130 26296 145 145 0 27985 0
[pid=10837] vsize: 112520
Current children cumulated CPU time (s) 718.37
Current children cumulated vsize (Kb) 114644

[startup+730.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27392 0 0 0 72691 143 0 0 25 0 1 0 1785077485 115539968 26375 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 28208 26375 145 145 0 28063 0
[pid=10837] vsize: 112832
Current children cumulated CPU time (s) 728.35
Current children cumulated vsize (Kb) 114956

[startup+740.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27524 0 0 0 73690 144 0 0 25 0 1 0 1785077485 116076544 26507 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 28339 26507 145 145 0 28194 0
[pid=10837] vsize: 113356
Current children cumulated CPU time (s) 738.35
Current children cumulated vsize (Kb) 115480

[startup+750.072 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27614 0 0 0 74689 145 0 0 25 0 1 0 1785077485 116441088 26597 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 28428 26597 145 145 0 28283 0
[pid=10837] vsize: 113712
Current children cumulated CPU time (s) 748.35
Current children cumulated vsize (Kb) 115836

[startup+760.072 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27767 0 0 0 75686 146 0 0 25 0 1 0 1785077485 117063680 26750 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 28580 26750 145 145 0 28435 0
[pid=10837] vsize: 114320
Current children cumulated CPU time (s) 758.33
Current children cumulated vsize (Kb) 116444

[startup+770.073 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27904 0 0 0 76685 147 0 0 25 0 1 0 1785077485 117620736 26887 4294967295 134512640 135094434 3221224448 3221223040 134556843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 28716 26887 145 145 0 28571 0
[pid=10837] vsize: 114864
Current children cumulated CPU time (s) 768.33
Current children cumulated vsize (Kb) 116988

[startup+780.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28224 0 0 0 77680 149 0 0 25 0 1 0 1785077485 118927360 27207 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 29035 27207 145 145 0 28890 0
[pid=10837] vsize: 116140
Current children cumulated CPU time (s) 778.3
Current children cumulated vsize (Kb) 118264

[startup+790.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28422 0 0 0 78677 150 0 0 25 0 1 0 1785077485 119726080 27405 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 29230 27405 145 145 0 29085 0
[pid=10837] vsize: 116920
Current children cumulated CPU time (s) 788.28
Current children cumulated vsize (Kb) 119044

[startup+800.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28671 0 0 0 79672 152 0 0 25 0 1 0 1785077485 120737792 27654 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 29477 27654 145 145 0 29332 0
[pid=10837] vsize: 117908
Current children cumulated CPU time (s) 798.25
Current children cumulated vsize (Kb) 120032

[startup+810.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28791 0 0 0 80671 153 0 0 25 0 1 0 1785077485 121225216 27774 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 29596 27774 145 145 0 29451 0
[pid=10837] vsize: 118384
Current children cumulated CPU time (s) 808.25
Current children cumulated vsize (Kb) 120508

[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28843 0 0 0 81670 153 0 0 25 0 1 0 1785077485 121434112 27826 4294967295 134512640 135094434 3221224448 3221223120 134556288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 29647 27826 145 145 0 29502 0
[pid=10837] vsize: 118588
Current children cumulated CPU time (s) 818.24
Current children cumulated vsize (Kb) 120712

[startup+830.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28906 0 0 0 82669 153 0 0 25 0 1 0 1785077485 121683968 27889 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 29708 27889 145 145 0 29563 0
[pid=10837] vsize: 118832
Current children cumulated CPU time (s) 828.23
Current children cumulated vsize (Kb) 120956

[startup+840.079 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28969 0 0 0 83669 154 0 0 25 0 1 0 1785077485 122458112 27952 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 29897 27952 145 145 0 29752 0
[pid=10837] vsize: 119588
Current children cumulated CPU time (s) 838.24
Current children cumulated vsize (Kb) 121712

[startup+850.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29036 0 0 0 84668 154 0 0 25 0 1 0 1785077485 122724352 28019 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 29962 28019 145 145 0 29817 0
[pid=10837] vsize: 119848
Current children cumulated CPU time (s) 848.23
Current children cumulated vsize (Kb) 121972

[startup+860.081 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29155 0 0 0 85666 155 0 0 25 0 1 0 1785077485 123219968 28138 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 30083 28138 145 145 0 29938 0
[pid=10837] vsize: 120332
Current children cumulated CPU time (s) 858.22
Current children cumulated vsize (Kb) 122456

[startup+870.081 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29304 0 0 0 86664 156 0 0 25 0 1 0 1785077485 123826176 28287 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 30231 28287 145 145 0 30086 0
[pid=10837] vsize: 120924
Current children cumulated CPU time (s) 868.21
Current children cumulated vsize (Kb) 123048

[startup+880.082 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29361 0 0 0 87662 156 0 0 25 0 1 0 1785077485 124055552 28344 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 30287 28344 145 145 0 30142 0
[pid=10837] vsize: 121148
Current children cumulated CPU time (s) 878.19
Current children cumulated vsize (Kb) 123272

[startup+890.083 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29462 0 0 0 88661 157 0 0 25 0 1 0 1785077485 124456960 28445 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 30385 28445 145 145 0 30240 0
[pid=10837] vsize: 121540
Current children cumulated CPU time (s) 888.19
Current children cumulated vsize (Kb) 123664

[startup+900.084 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29530 0 0 0 89660 158 0 0 25 0 1 0 1785077485 124727296 28513 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 30451 28513 145 145 0 30306 0
[pid=10837] vsize: 121804
Current children cumulated CPU time (s) 898.19
Current children cumulated vsize (Kb) 123928

[startup+910.086 s]
Raw data (loadavg): 0.99 0.97 0.99 3/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29598 0 0 0 90659 158 0 0 25 0 1 0 1785077485 124997632 28581 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 30517 28581 145 145 0 30372 0
[pid=10837] vsize: 122068
Current children cumulated CPU time (s) 908.18
Current children cumulated vsize (Kb) 124192

[startup+920.087 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29682 0 0 0 91658 159 0 0 25 0 1 0 1785077485 125337600 28665 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 30600 28665 145 145 0 30455 0
[pid=10837] vsize: 122400
Current children cumulated CPU time (s) 918.18
Current children cumulated vsize (Kb) 124524

[startup+930.087 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29766 0 0 0 92656 160 0 0 25 0 1 0 1785077485 125677568 28749 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 30683 28749 145 145 0 30538 0
[pid=10837] vsize: 122732
Current children cumulated CPU time (s) 928.17
Current children cumulated vsize (Kb) 124856

[startup+940.088 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29852 0 0 0 93655 160 0 0 25 0 1 0 1785077485 126025728 28835 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 30768 28835 145 145 0 30623 0
[pid=10837] vsize: 123072
Current children cumulated CPU time (s) 938.16
Current children cumulated vsize (Kb) 125196

[startup+950.089 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29940 0 0 0 94654 161 0 0 25 0 1 0 1785077485 126382080 28923 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 30855 28923 145 145 0 30710 0
[pid=10837] vsize: 123420
Current children cumulated CPU time (s) 948.16
Current children cumulated vsize (Kb) 125544

[startup+960.091 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29992 0 0 0 95653 161 0 0 25 0 1 0 1785077485 126595072 28975 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 30907 28975 145 145 0 30762 0
[pid=10837] vsize: 123628
Current children cumulated CPU time (s) 958.15
Current children cumulated vsize (Kb) 125752

[startup+970.092 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 30173 0 0 0 96649 163 0 0 25 0 1 0 1785077485 127332352 29156 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 31087 29156 145 145 0 30942 0
[pid=10837] vsize: 124348
Current children cumulated CPU time (s) 968.13
Current children cumulated vsize (Kb) 126472

[startup+980.091 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 30314 0 0 0 97647 164 0 0 25 0 1 0 1785077485 127905792 29297 4294967295 134512640 135094434 3221224448 3221223104 134557818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 31227 29297 145 145 0 31082 0
[pid=10837] vsize: 124908
Current children cumulated CPU time (s) 978.12
Current children cumulated vsize (Kb) 127032

[startup+990.092 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 30410 0 0 0 98645 165 0 0 25 0 1 0 1785077485 128299008 29393 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 31323 29393 145 145 0 31178 0
[pid=10837] vsize: 125292
Current children cumulated CPU time (s) 988.11
Current children cumulated vsize (Kb) 127416

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 30521 0 0 0 99643 166 0 0 25 0 1 0 1785077485 128749568 29504 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 31433 29504 145 145 0 31288 0
[pid=10837] vsize: 125732
Current children cumulated CPU time (s) 998.1
Current children cumulated vsize (Kb) 127856

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 30703 0 0 0 100640 168 0 0 25 0 1 0 1785077485 129495040 29686 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 31615 29686 145 145 0 31470 0
[pid=10837] vsize: 126460
Current children cumulated CPU time (s) 1008.09
Current children cumulated vsize (Kb) 128584

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 30867 0 0 0 101638 169 0 0 25 0 1 0 1785077485 130166784 29850 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 31779 29850 145 145 0 31634 0
[pid=10837] vsize: 127116
Current children cumulated CPU time (s) 1018.08
Current children cumulated vsize (Kb) 129240

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31055 0 0 0 102634 171 0 0 25 0 1 0 1785077485 130932736 30038 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 31966 30038 145 145 0 31821 0
[pid=10837] vsize: 127864
Current children cumulated CPU time (s) 1028.06
Current children cumulated vsize (Kb) 129988

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31243 0 0 0 103633 172 0 0 25 0 1 0 1785077485 131698688 30226 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 32153 30226 145 145 0 32008 0
[pid=10837] vsize: 128612
Current children cumulated CPU time (s) 1038.06
Current children cumulated vsize (Kb) 130736

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31443 0 0 0 104631 173 0 0 25 0 1 0 1785077485 132517888 30426 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 32353 30426 145 145 0 32208 0
[pid=10837] vsize: 129412
Current children cumulated CPU time (s) 1048.05
Current children cumulated vsize (Kb) 131536

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31632 0 0 0 105629 174 0 0 25 0 1 0 1785077485 133275648 30615 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 32538 30615 145 145 0 32393 0
[pid=10837] vsize: 130152
Current children cumulated CPU time (s) 1058.04
Current children cumulated vsize (Kb) 132276

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31794 0 0 0 106626 175 0 0 25 0 1 0 1785077485 133935104 30777 4294967295 134512640 135094434 3221224448 3221223040 134557141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 32699 30777 145 145 0 32554 0
[pid=10837] vsize: 130796
Current children cumulated CPU time (s) 1068.02
Current children cumulated vsize (Kb) 132920

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31890 0 0 0 107624 176 0 0 25 0 1 0 1785077485 134324224 30873 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 32794 30873 145 145 0 32649 0
[pid=10837] vsize: 131176
Current children cumulated CPU time (s) 1078.01
Current children cumulated vsize (Kb) 133300

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31989 0 0 0 108623 177 0 0 25 0 1 0 1785077485 134729728 30972 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 32893 30972 145 145 0 32748 0
[pid=10837] vsize: 131572
Current children cumulated CPU time (s) 1088.01
Current children cumulated vsize (Kb) 133696

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32129 0 0 0 109621 177 0 0 25 0 1 0 1785077485 135299072 31112 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33032 31112 145 145 0 32887 0
[pid=10837] vsize: 132128
Current children cumulated CPU time (s) 1097.99
Current children cumulated vsize (Kb) 134252

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32275 0 0 0 110619 179 0 0 25 0 1 0 1785077485 135897088 31258 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33178 31258 145 145 0 33033 0
[pid=10837] vsize: 132712
Current children cumulated CPU time (s) 1107.99
Current children cumulated vsize (Kb) 134836

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32338 0 0 0 111617 179 0 0 25 0 1 0 1785077485 136142848 31321 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33238 31321 145 145 0 33093 0
[pid=10837] vsize: 132952
Current children cumulated CPU time (s) 1117.97
Current children cumulated vsize (Kb) 135076

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32389 0 0 0 112616 179 0 0 25 0 1 0 1785077485 136343552 31372 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33287 31372 145 145 0 33142 0
[pid=10837] vsize: 133148
Current children cumulated CPU time (s) 1127.96
Current children cumulated vsize (Kb) 135272

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32431 0 0 0 113616 180 0 0 25 0 1 0 1785077485 136507392 31414 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33327 31414 145 145 0 33182 0
[pid=10837] vsize: 133308
Current children cumulated CPU time (s) 1137.97
Current children cumulated vsize (Kb) 135432

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32457 0 0 0 114615 180 0 0 25 0 1 0 1785077485 136609792 31440 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33352 31440 145 145 0 33207 0
[pid=10837] vsize: 133408
Current children cumulated CPU time (s) 1147.96
Current children cumulated vsize (Kb) 135532

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32493 0 0 0 115615 180 0 0 25 0 1 0 1785077485 136753152 31476 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33387 31476 145 145 0 33242 0
[pid=10837] vsize: 133548
Current children cumulated CPU time (s) 1157.96
Current children cumulated vsize (Kb) 135672

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32596 0 0 0 116612 181 0 0 25 0 1 0 1785077485 137170944 31579 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33489 31579 145 145 0 33344 0
[pid=10837] vsize: 133956
Current children cumulated CPU time (s) 1167.94
Current children cumulated vsize (Kb) 136080

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32644 0 0 0 117611 181 0 0 25 0 1 0 1785077485 137363456 31627 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33536 31627 145 145 0 33391 0
[pid=10837] vsize: 134144
Current children cumulated CPU time (s) 1177.93
Current children cumulated vsize (Kb) 136268

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.99 3/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32720 0 0 0 118609 182 0 0 25 0 1 0 1785077485 137670656 31703 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33611 31703 145 145 0 33466 0
[pid=10837] vsize: 134444
Current children cumulated CPU time (s) 1187.92
Current children cumulated vsize (Kb) 136568

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32821 0 0 0 119608 183 0 0 25 0 1 0 1785077485 138084352 31804 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33712 31804 145 145 0 33567 0
[pid=10837] vsize: 134848
Current children cumulated CPU time (s) 1197.92
Current children cumulated vsize (Kb) 136972

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 33020 0 0 0 120606 184 0 0 25 0 1 0 1785077485 138895360 32003 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33910 32003 145 145 0 33765 0
[pid=10837] vsize: 135640
Current children cumulated CPU time (s) 1207.91
Current children cumulated vsize (Kb) 137764



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 10837
Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10833/statm): 531 226 485 147 0 384 0
[pid=10833] vsize: 2124
Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 33020 0 0 0 120606 184 0 0 25 0 1 0 1785077485 138895360 32003 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10837/statm): 33910 32003 145 145 0 33765 0
[pid=10837] vsize: 135640
Current children cumulated CPU time (s) 1207.91
Current children cumulated vsize (Kb) 137764

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

Child status: 10
Real time (s): 1210.18
CPU time (s): 1207.97
CPU user time (s): 1206.06
CPU system time (s): 1.90971
CPU usage (%): 99.8178
Max. virtual memory (cumulated for all children) (Kb): 137764

Verifier Data

ERROR: no interpretation found !