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-9symml.opb
MD5SUM48809ba02390b1184dab90aed89aff8e
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 4517
Optimality of the best value was proved YES
Number of terms in the objective function 651
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 28138
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 28138
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 benchmark281.067
Number of variables651
Total number of constraints1658
Number of constraints which are clauses1656
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints2
Minimum length of a constraint1
Maximum length of a constraint42

Trace number 2198

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        916828 kB
Buffers:         35288 kB
Cached:          47984 kB
SwapCached:        844 kB
Active:          66240 kB
Inactive:        19660 kB
HighTotal:      131008 kB
HighFree:        80136 kB
LowTotal:       903652 kB
LowFree:        836692 kB
SwapTotal:     2097892 kB
SwapFree:      2096548 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5764 kB
Slab:            26400 kB
Committed_AS:    64148 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 18:30:21 (client local time) WITH STATUS 10 IN 1208.03 SECONDS
stats: 2590 7 1208.03 10

Solver Data

c Parsing PB file...
c Converting 1579 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 |    1552     6592 |     517       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 6227
c ---[   0]---> Sorter-cost:101537     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  240640   564833 |   80213       0        0     nan |  0.000 % |
c |       100 |  240294   564068 |   88234      97      554     5.7 |  0.124 % |
c |       250 |  239475   562211 |   97057     242     1239     5.1 |  0.372 % |
c |       475 |  239475   562211 |  106763     467     2772     5.9 |  0.372 % |
c |       812 |  239475   562211 |  117439     804     5080     6.3 |  0.372 % |
c |      1318 |  239344   561924 |  129183    1306    10185     7.8 |  0.418 % |
c |      2077 |  239154   561493 |  142102    2061    21860    10.6 |  0.491 % |
c |      3217 |  238924   560969 |  156312    3195    43126    13.5 |  0.574 % |
c |      4925 |  238870   560853 |  171943    4898   147580    30.1 |  0.598 % |
c |      7488 |  238545   560119 |  189138    7447   199936    26.8 |  0.694 % |
c |     11333 |  238182   559291 |  208051   11252   264258    23.5 |  0.811 % |
c |     17099 |  237688   558162 |  228857   16994   352844    20.8 |  0.969 % |
c |     25751 |  237623   558014 |  251742   25643   903840    35.2 |  0.991 % |
c ==============================================================================
c Found solution: 5682
c ---[   0]---> Sorter-cost:81756     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29821 |  435689  1020432 |  145229   29713  1042028    35.1 |  0.991 % |
c |     29922 |  435689  1020432 |  159751   29814  1042915    35.0 |  0.570 % |
c |     30072 |  435689  1020432 |  175727   29964  1043798    34.8 |  0.570 % |
c |     30297 |  435410  1019814 |  193299   30186  1047211    34.7 |  0.617 % |
c |     30635 |  434343  1017394 |  212629   30492  1053024    34.5 |  0.811 % |
c |     31141 |  434343  1017394 |  233892   30998  1066445    34.4 |  0.811 % |
c |     31900 |  434343  1017394 |  257282   31757  1076013    33.9 |  0.811 % |
c |     33039 |  434343  1017394 |  283010   32896  1253111    38.1 |  0.811 % |
c |     34748 |  434343  1017394 |  311311   34605  1301864    37.6 |  0.811 % |
c |     37311 |  434331  1017367 |  342442   37166  1344836    36.2 |  0.813 % |
c |     41155 |  434331  1017367 |  376686   41010  1457843    35.5 |  0.813 % |
c |     46922 |  434331  1017367 |  414355   46777  2162173    46.2 |  0.813 % |
c |     55572 |  434242  1017165 |  455790   55424  3473368    62.7 |  0.830 % |
c |     68546 |  434242  1017165 |  501369   68398  6520599    95.3 |  0.830 % |
c |     88008 |  434235  1017150 |  551506   87857  9667702   110.0 |  0.832 % |
c |    117200 |  433771  1016104 |  606657  117042 19603779   167.5 |  0.911 % |

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/5246/stat): 5246 (minisat+_script) R 5245 5246 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843273101 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/5246/statm): 174 3 169 147 0 27 0
[pid=5246] 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=5247
New process pid=5248
New process pid=5249
execve syscall for /bin/sed executable
One traced child (pid=5248) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=5249) exited with status: 0
One traced child (pid=5247) exited with status: 0
New process pid=5250
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-9symml.opb

[startup+10.0039 s]
Raw data (loadavg): 0.91 0.94 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 7894 0 0 0 935 29 0 0 25 0 1 0 1843273106 33902592 7443 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 8277 7443 145 145 0 8132 0
[pid=5250] vsize: 33108
Current children cumulated CPU time (s) 9.65
Current children cumulated vsize (Kb) 35232

[startup+20.0058 s]
Raw data (loadavg): 0.92 0.94 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8018 0 0 0 1934 30 0 0 25 0 1 0 1843273106 34418688 7567 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 8403 7567 145 145 0 8258 0
[pid=5250] vsize: 33612
Current children cumulated CPU time (s) 19.65
Current children cumulated vsize (Kb) 35736

[startup+30.0077 s]
Raw data (loadavg): 0.93 0.94 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8106 0 0 0 2932 31 0 0 25 0 1 0 1843273106 34758656 7655 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 8486 7655 145 145 0 8341 0
[pid=5250] vsize: 33944
Current children cumulated CPU time (s) 29.64
Current children cumulated vsize (Kb) 36068

[startup+40.0086 s]
Raw data (loadavg): 0.94 0.94 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8194 0 0 0 3930 32 0 0 25 0 1 0 1843273106 35131392 7743 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 8577 7743 145 145 0 8432 0
[pid=5250] vsize: 34308
Current children cumulated CPU time (s) 39.63
Current children cumulated vsize (Kb) 36432

[startup+50.0095 s]
Raw data (loadavg): 0.95 0.94 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8331 0 0 0 4928 33 0 0 25 0 1 0 1843273106 35667968 7880 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 8708 7880 145 145 0 8563 0
[pid=5250] vsize: 34832
Current children cumulated CPU time (s) 49.62
Current children cumulated vsize (Kb) 36956

[startup+60.0105 s]
Raw data (loadavg): 0.96 0.94 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8571 0 0 0 5925 34 0 0 25 0 1 0 1843273106 36663296 8120 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 8951 8120 145 145 0 8806 0
[pid=5250] vsize: 35804
Current children cumulated CPU time (s) 59.6
Current children cumulated vsize (Kb) 37928

[startup+70.0114 s]
Raw data (loadavg): 0.96 0.95 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8770 0 0 0 6922 36 0 0 25 0 1 0 1843273106 37470208 8319 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 9148 8319 145 145 0 9003 0
[pid=5250] vsize: 36592
Current children cumulated CPU time (s) 69.59
Current children cumulated vsize (Kb) 38716

[startup+80.0133 s]
Raw data (loadavg): 0.97 0.95 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8862 0 0 0 7919 37 0 0 25 0 1 0 1843273106 37838848 8411 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 9238 8411 145 145 0 9093 0
[pid=5250] vsize: 36952
Current children cumulated CPU time (s) 79.57
Current children cumulated vsize (Kb) 39076

[startup+90.0142 s]
Raw data (loadavg): 0.97 0.95 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8968 0 0 0 8917 38 0 0 25 0 1 0 1843273106 38264832 8517 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 9342 8517 145 145 0 9197 0
[pid=5250] vsize: 37368
Current children cumulated CPU time (s) 89.56
Current children cumulated vsize (Kb) 39492

[startup+100.015 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 9098 0 0 0 9914 40 0 0 25 0 1 0 1843273106 38785024 8647 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 9469 8647 145 145 0 9324 0
[pid=5250] vsize: 37876
Current children cumulated CPU time (s) 99.55
Current children cumulated vsize (Kb) 40000

[startup+110.017 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15468 0 0 0 10867 65 0 0 25 0 1 0 1843273106 68468736 14562 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 16716 14562 145 145 0 16571 0
[pid=5250] vsize: 66864
Current children cumulated CPU time (s) 109.33
Current children cumulated vsize (Kb) 68988

[startup+120.019 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15529 0 0 0 11866 65 0 0 25 0 1 0 1843273106 68616192 14623 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 16752 14623 145 145 0 16607 0
[pid=5250] vsize: 67008
Current children cumulated CPU time (s) 119.32
Current children cumulated vsize (Kb) 69132

[startup+130.02 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15661 0 0 0 12863 67 0 0 25 0 1 0 1843273106 69152768 14755 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 16883 14755 145 145 0 16738 0
[pid=5250] vsize: 67532
Current children cumulated CPU time (s) 129.31
Current children cumulated vsize (Kb) 69656

[startup+140.021 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15773 0 0 0 13861 68 0 0 25 0 1 0 1843273106 69718016 14867 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 17021 14867 145 145 0 16876 0
[pid=5250] vsize: 68084
Current children cumulated CPU time (s) 139.3
Current children cumulated vsize (Kb) 70208

[startup+150.022 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15829 0 0 0 14860 69 0 0 25 0 1 0 1843273106 69894144 14923 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 17064 14923 145 145 0 16919 0
[pid=5250] vsize: 68256
Current children cumulated CPU time (s) 149.3
Current children cumulated vsize (Kb) 70380

[startup+160.024 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15896 0 0 0 15859 69 0 0 25 0 1 0 1843273106 70160384 14990 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 17129 14990 145 145 0 16984 0
[pid=5250] vsize: 68516
Current children cumulated CPU time (s) 159.29
Current children cumulated vsize (Kb) 70640

[startup+170.025 s]
Raw data (loadavg): 0.99 0.95 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15962 0 0 0 16858 70 0 0 25 0 1 0 1843273106 70422528 15056 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 17193 15056 145 145 0 17048 0
[pid=5250] vsize: 68772
Current children cumulated CPU time (s) 169.29
Current children cumulated vsize (Kb) 70896

[startup+180.027 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16024 0 0 0 17856 71 0 0 25 0 1 0 1843273106 70668288 15118 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 17253 15118 145 145 0 17108 0
[pid=5250] vsize: 69012
Current children cumulated CPU time (s) 179.28
Current children cumulated vsize (Kb) 71136

[startup+190.029 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16100 0 0 0 18854 72 0 0 25 0 1 0 1843273106 70987776 15194 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 17331 15194 145 145 0 17186 0
[pid=5250] vsize: 69324
Current children cumulated CPU time (s) 189.27
Current children cumulated vsize (Kb) 71448

[startup+200.029 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16209 0 0 0 19852 73 0 0 25 0 1 0 1843273106 71430144 15303 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 17439 15303 145 145 0 17294 0
[pid=5250] vsize: 69756
Current children cumulated CPU time (s) 199.26
Current children cumulated vsize (Kb) 71880

[startup+210.031 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16354 0 0 0 20849 74 0 0 25 0 1 0 1843273106 72019968 15448 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 17583 15448 145 145 0 17438 0
[pid=5250] vsize: 70332
Current children cumulated CPU time (s) 209.24
Current children cumulated vsize (Kb) 72456

[startup+220.032 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16484 0 0 0 21847 76 0 0 25 0 1 0 1843273106 72548352 15578 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 17712 15578 145 145 0 17567 0
[pid=5250] vsize: 70848
Current children cumulated CPU time (s) 219.24
Current children cumulated vsize (Kb) 72972

[startup+230.034 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16576 0 0 0 22845 77 0 0 25 0 1 0 1843273106 72925184 15670 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 17804 15670 145 145 0 17659 0
[pid=5250] vsize: 71216
Current children cumulated CPU time (s) 229.23
Current children cumulated vsize (Kb) 73340

[startup+240.035 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16742 0 0 0 23842 79 0 0 25 0 1 0 1843273106 73601024 15836 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 17969 15836 145 145 0 17824 0
[pid=5250] vsize: 71876
Current children cumulated CPU time (s) 239.22
Current children cumulated vsize (Kb) 74000

[startup+250.036 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16820 0 0 0 24841 79 0 0 25 0 1 0 1843273106 73912320 15914 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 18045 15914 145 145 0 17900 0
[pid=5250] vsize: 72180
Current children cumulated CPU time (s) 249.21
Current children cumulated vsize (Kb) 74304

[startup+260.038 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16908 0 0 0 25838 80 0 0 25 0 1 0 1843273106 74268672 16002 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 18132 16002 145 145 0 17987 0
[pid=5250] vsize: 72528
Current children cumulated CPU time (s) 259.19
Current children cumulated vsize (Kb) 74652

[startup+270.039 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16979 0 0 0 26837 82 0 0 25 0 1 0 1843273106 74555392 16073 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 18202 16073 145 145 0 18057 0
[pid=5250] vsize: 72808
Current children cumulated CPU time (s) 269.2
Current children cumulated vsize (Kb) 74932

[startup+280.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17102 0 0 0 27835 83 0 0 25 0 1 0 1843273106 75059200 16196 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 18325 16196 145 145 0 18180 0
[pid=5250] vsize: 73300
Current children cumulated CPU time (s) 279.19
Current children cumulated vsize (Kb) 75424

[startup+290.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17214 0 0 0 28832 85 0 0 25 0 1 0 1843273106 75513856 16308 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 18436 16308 145 145 0 18291 0
[pid=5250] vsize: 73744
Current children cumulated CPU time (s) 289.18
Current children cumulated vsize (Kb) 75868

[startup+300.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17385 0 0 0 29830 86 0 0 25 0 1 0 1843273106 76206080 16479 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 18605 16479 145 145 0 18460 0
[pid=5250] vsize: 74420
Current children cumulated CPU time (s) 299.17
Current children cumulated vsize (Kb) 76544

[startup+310.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17580 0 0 0 30827 88 0 0 25 0 1 0 1843273106 77000704 16674 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 18799 16674 145 145 0 18654 0
[pid=5250] vsize: 75196
Current children cumulated CPU time (s) 309.16
Current children cumulated vsize (Kb) 77320

[startup+320.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17727 0 0 0 31824 89 0 0 25 0 1 0 1843273106 77598720 16821 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 18945 16821 145 145 0 18800 0
[pid=5250] vsize: 75780
Current children cumulated CPU time (s) 319.14
Current children cumulated vsize (Kb) 77904

[startup+330.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17844 0 0 0 32822 90 0 0 25 0 1 0 1843273106 78077952 16938 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 19062 16938 145 145 0 18917 0
[pid=5250] vsize: 76248
Current children cumulated CPU time (s) 329.13
Current children cumulated vsize (Kb) 78372

[startup+340.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17967 0 0 0 33819 91 0 0 25 0 1 0 1843273106 78577664 17061 4294967295 134512640 135094434 3221224448 3221223040 134556864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 19184 17061 145 145 0 19039 0
[pid=5250] vsize: 76736
Current children cumulated CPU time (s) 339.11
Current children cumulated vsize (Kb) 78860

[startup+350.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18134 0 0 0 34817 93 0 0 25 0 1 0 1843273106 79257600 17228 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 19350 17228 145 145 0 19205 0
[pid=5250] vsize: 77400
Current children cumulated CPU time (s) 349.11
Current children cumulated vsize (Kb) 79524

[startup+360.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18181 0 0 0 35816 94 0 0 25 0 1 0 1843273106 79441920 17275 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 19395 17275 145 145 0 19250 0
[pid=5250] vsize: 77580
Current children cumulated CPU time (s) 359.11
Current children cumulated vsize (Kb) 79704

[startup+370.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18229 0 0 0 36814 95 0 0 25 0 1 0 1843273106 79634432 17323 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 19442 17323 145 145 0 19297 0
[pid=5250] vsize: 77768
Current children cumulated CPU time (s) 369.1
Current children cumulated vsize (Kb) 79892

[startup+380.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18271 0 0 0 37813 96 0 0 25 0 1 0 1843273106 79806464 17365 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 19484 17365 145 145 0 19339 0
[pid=5250] vsize: 77936
Current children cumulated CPU time (s) 379.1
Current children cumulated vsize (Kb) 80060

[startup+390.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18323 0 0 0 38812 97 0 0 25 0 1 0 1843273106 80015360 17417 4294967295 134512640 135094434 3221224448 3221223100 134562036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 19535 17417 145 145 0 19390 0
[pid=5250] vsize: 78140
Current children cumulated CPU time (s) 389.1
Current children cumulated vsize (Kb) 80264

[startup+400.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18370 0 0 0 39810 97 0 0 25 0 1 0 1843273106 80207872 17464 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 19582 17464 145 145 0 19437 0
[pid=5250] vsize: 78328
Current children cumulated CPU time (s) 399.08
Current children cumulated vsize (Kb) 80452

[startup+410.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18422 0 0 0 40809 98 0 0 25 0 1 0 1843273106 80416768 17516 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 19633 17516 145 145 0 19488 0
[pid=5250] vsize: 78532
Current children cumulated CPU time (s) 409.08
Current children cumulated vsize (Kb) 80656

[startup+420.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18498 0 0 0 41807 99 0 0 25 0 1 0 1843273106 80728064 17592 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 19709 17592 145 145 0 19564 0
[pid=5250] vsize: 78836
Current children cumulated CPU time (s) 419.07
Current children cumulated vsize (Kb) 80960

[startup+430.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18613 0 0 0 42804 101 0 0 25 0 1 0 1843273106 81195008 17707 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 19823 17707 145 145 0 19678 0
[pid=5250] vsize: 79292
Current children cumulated CPU time (s) 429.06
Current children cumulated vsize (Kb) 81416

[startup+440.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18973 0 0 0 43798 104 0 0 25 0 1 0 1843273106 82665472 18067 4294967295 134512640 135094434 3221224448 3221223040 134551922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 20182 18067 145 145 0 20037 0
[pid=5250] vsize: 80728
Current children cumulated CPU time (s) 439.03
Current children cumulated vsize (Kb) 82852

[startup+450.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 19378 0 0 0 44791 107 0 0 25 0 1 0 1843273106 84316160 18472 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 20585 18472 145 145 0 20440 0
[pid=5250] vsize: 82340
Current children cumulated CPU time (s) 448.99
Current children cumulated vsize (Kb) 84464

[startup+460.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 19819 0 0 0 45786 109 0 0 25 0 1 0 1843273106 86118400 18913 4294967295 134512640 135094434 3221224448 3221223040 134557143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 21025 18913 145 145 0 20880 0
[pid=5250] vsize: 84100
Current children cumulated CPU time (s) 458.96
Current children cumulated vsize (Kb) 86224

[startup+470.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 20332 0 0 0 46781 111 0 0 25 0 1 0 1843273106 88219648 19426 4294967295 134512640 135094434 3221224448 3221223040 134557391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 21538 19426 145 145 0 21393 0
[pid=5250] vsize: 86152
Current children cumulated CPU time (s) 468.93
Current children cumulated vsize (Kb) 88276

[startup+480.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 20764 0 0 0 47776 113 0 0 25 0 1 0 1843273106 90247168 19858 4294967295 134512640 135094434 3221224448 3221223040 134557389 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 22033 19858 145 145 0 21888 0
[pid=5250] vsize: 88132
Current children cumulated CPU time (s) 478.9
Current children cumulated vsize (Kb) 90256

[startup+490.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 21166 0 0 0 48771 116 0 0 25 0 1 0 1843273106 91897856 20260 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 22436 20260 145 145 0 22291 0
[pid=5250] vsize: 89744
Current children cumulated CPU time (s) 488.88
Current children cumulated vsize (Kb) 91868

[startup+500.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 21239 0 0 0 49769 117 0 0 25 0 1 0 1843273106 92184576 20333 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 22506 20333 145 145 0 22361 0
[pid=5250] vsize: 90024
Current children cumulated CPU time (s) 498.87
Current children cumulated vsize (Kb) 92148

[startup+510.073 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 21321 0 0 0 50767 118 0 0 25 0 1 0 1843273106 92508160 20415 4294967295 134512640 135094434 3221224448 3221223104 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 22585 20415 145 145 0 22440 0
[pid=5250] vsize: 90340
Current children cumulated CPU time (s) 508.86
Current children cumulated vsize (Kb) 92464

[startup+520.074 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 21386 0 0 0 51765 119 0 0 25 0 1 0 1843273106 92770304 20480 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 22649 20480 145 145 0 22504 0
[pid=5250] vsize: 90596
Current children cumulated CPU time (s) 518.85
Current children cumulated vsize (Kb) 92720

[startup+530.076 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 21530 0 0 0 52763 121 0 0 25 0 1 0 1843273106 93356032 20624 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 22792 20624 145 145 0 22647 0
[pid=5250] vsize: 91168
Current children cumulated CPU time (s) 528.85
Current children cumulated vsize (Kb) 93292

[startup+540.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 21769 0 0 0 53760 122 0 0 25 0 1 0 1843273106 94326784 20863 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 23029 20863 145 145 0 22884 0
[pid=5250] vsize: 92116
Current children cumulated CPU time (s) 538.83
Current children cumulated vsize (Kb) 94240

[startup+550.078 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 22013 0 0 0 54758 123 0 0 25 0 1 0 1843273106 95322112 21107 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 23272 21107 145 145 0 23127 0
[pid=5250] vsize: 93088
Current children cumulated CPU time (s) 548.82
Current children cumulated vsize (Kb) 95212

[startup+560.079 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 22271 0 0 0 55755 125 0 0 25 0 1 0 1843273106 96374784 21365 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 23529 21365 145 145 0 23384 0
[pid=5250] vsize: 94116
Current children cumulated CPU time (s) 558.81
Current children cumulated vsize (Kb) 96240

[startup+570.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 22556 0 0 0 56750 127 0 0 25 0 1 0 1843273106 97542144 21650 4294967295 134512640 135094434 3221224448 3221223040 134557391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 23814 21650 145 145 0 23669 0
[pid=5250] vsize: 95256
Current children cumulated CPU time (s) 568.78
Current children cumulated vsize (Kb) 97380

[startup+580.081 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 22806 0 0 0 57748 128 0 0 25 0 1 0 1843273106 98549760 21900 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 24060 21900 145 145 0 23915 0
[pid=5250] vsize: 96240
Current children cumulated CPU time (s) 578.77
Current children cumulated vsize (Kb) 98364

[startup+590.081 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 23066 0 0 0 58743 130 0 0 25 0 1 0 1843273106 99672064 22160 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 24334 22160 145 145 0 24189 0
[pid=5250] vsize: 97336
Current children cumulated CPU time (s) 588.74
Current children cumulated vsize (Kb) 99460

[startup+600.082 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 23302 0 0 0 59741 131 0 0 25 0 1 0 1843273106 100634624 22396 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 24569 22396 145 145 0 24424 0
[pid=5250] vsize: 98276
Current children cumulated CPU time (s) 598.73
Current children cumulated vsize (Kb) 100400

[startup+610.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 23542 0 0 0 60738 132 0 0 25 0 1 0 1843273106 101617664 22636 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 24809 22636 145 145 0 24664 0
[pid=5250] vsize: 99236
Current children cumulated CPU time (s) 608.71
Current children cumulated vsize (Kb) 101360

[startup+620.084 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 23749 0 0 0 61735 134 0 0 25 0 1 0 1843273106 102461440 22843 4294967295 134512640 135094434 3221224448 3221223040 134557137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 25015 22843 145 145 0 24870 0
[pid=5250] vsize: 100060
Current children cumulated CPU time (s) 618.7
Current children cumulated vsize (Kb) 102184

[startup+630.086 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 23966 0 0 0 62732 136 0 0 25 0 1 0 1843273106 103346176 23060 4294967295 134512640 135094434 3221224448 3221223040 134556823 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 25231 23060 145 145 0 25086 0
[pid=5250] vsize: 100924
Current children cumulated CPU time (s) 628.69
Current children cumulated vsize (Kb) 103048

[startup+640.087 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24196 0 0 0 63728 137 0 0 25 0 1 0 1843273106 104288256 23290 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5250/statm): 25461 23290 145 145 0 25316 0
[pid=5250] vsize: 101844
Current children cumulated CPU time (s) 638.66
Current children cumulated vsize (Kb) 103968

[startup+650.088 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24354 0 0 0 64726 137 0 0 25 0 1 0 1843273106 104931328 23448 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 25618 23448 145 145 0 25473 0
[pid=5250] vsize: 102472
Current children cumulated CPU time (s) 648.64
Current children cumulated vsize (Kb) 104596

[startup+660.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24489 0 0 0 65723 139 0 0 25 0 1 0 1843273106 105467904 23583 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 25749 23583 145 145 0 25604 0
[pid=5250] vsize: 102996
Current children cumulated CPU time (s) 658.63
Current children cumulated vsize (Kb) 105120

[startup+670.091 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24626 0 0 0 66720 140 0 0 25 0 1 0 1843273106 106020864 23720 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 25884 23720 145 145 0 25739 0
[pid=5250] vsize: 103536
Current children cumulated CPU time (s) 668.61
Current children cumulated vsize (Kb) 105660

[startup+680.093 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24675 0 0 0 67720 141 0 0 25 0 1 0 1843273106 106217472 23769 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 25932 23769 145 145 0 25787 0
[pid=5250] vsize: 103728
Current children cumulated CPU time (s) 678.62
Current children cumulated vsize (Kb) 105852

[startup+690.094 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24742 0 0 0 68718 142 0 0 25 0 1 0 1843273106 106487808 23836 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 25998 23836 145 145 0 25853 0
[pid=5250] vsize: 103992
Current children cumulated CPU time (s) 688.61
Current children cumulated vsize (Kb) 106116

[startup+700.095 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24865 0 0 0 69717 142 0 0 25 0 1 0 1843273106 106991616 23959 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 26121 23959 145 145 0 25976 0
[pid=5250] vsize: 104484
Current children cumulated CPU time (s) 698.6
Current children cumulated vsize (Kb) 106608

[startup+710.096 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24963 0 0 0 70716 143 0 0 25 0 1 0 1843273106 107388928 24057 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 26218 24057 145 145 0 26073 0
[pid=5250] vsize: 104872
Current children cumulated CPU time (s) 708.6
Current children cumulated vsize (Kb) 106996

[startup+720.096 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 25074 0 0 0 71714 144 0 0 25 0 1 0 1843273106 107843584 24168 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 26329 24168 145 145 0 26184 0
[pid=5250] vsize: 105316
Current children cumulated CPU time (s) 718.59
Current children cumulated vsize (Kb) 107440

[startup+730.097 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 25166 0 0 0 72713 144 0 0 25 0 1 0 1843273106 108220416 24260 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 26421 24260 145 145 0 26276 0
[pid=5250] vsize: 105684
Current children cumulated CPU time (s) 728.58
Current children cumulated vsize (Kb) 107808

[startup+740.098 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 25290 0 0 0 73712 145 0 0 25 0 1 0 1843273106 108724224 24384 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 26544 24384 145 145 0 26399 0
[pid=5250] vsize: 106176
Current children cumulated CPU time (s) 738.58
Current children cumulated vsize (Kb) 108300

[startup+750.099 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 25445 0 0 0 74710 146 0 0 25 0 1 0 1843273106 109359104 24539 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 26699 24539 145 145 0 26554 0
[pid=5250] vsize: 106796
Current children cumulated CPU time (s) 748.57
Current children cumulated vsize (Kb) 108920

[startup+760.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 25612 0 0 0 75707 147 0 0 25 0 1 0 1843273106 110043136 24706 4294967295 134512640 135094434 3221224448 3221223104 134557859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 26866 24706 145 145 0 26721 0
[pid=5250] vsize: 107464
Current children cumulated CPU time (s) 758.55
Current children cumulated vsize (Kb) 109588

[startup+770.101 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 25826 0 0 0 76704 148 0 0 25 0 1 0 1843273106 110923776 24920 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 27081 24920 145 145 0 26936 0
[pid=5250] vsize: 108324
Current children cumulated CPU time (s) 768.53
Current children cumulated vsize (Kb) 110448

[startup+780.103 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 26033 0 0 0 77701 150 0 0 25 0 1 0 1843273106 111763456 25127 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 27286 25127 145 145 0 27141 0
[pid=5250] vsize: 109144
Current children cumulated CPU time (s) 778.52
Current children cumulated vsize (Kb) 111268

[startup+790.104 s]
Raw data (loadavg): 0.99 0.97 0.96 3/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 26213 0 0 0 78698 151 0 0 25 0 1 0 1843273106 112496640 25307 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 27465 25307 145 145 0 27320 0
[pid=5250] vsize: 109860
Current children cumulated CPU time (s) 788.5
Current children cumulated vsize (Kb) 111984

[startup+800.104 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 26378 0 0 0 79696 152 0 0 25 0 1 0 1843273106 113172480 25472 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 27630 25472 145 145 0 27485 0
[pid=5250] vsize: 110520
Current children cumulated CPU time (s) 798.49
Current children cumulated vsize (Kb) 112644

[startup+810.105 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 26506 0 0 0 80694 153 0 0 25 0 1 0 1843273106 113692672 25600 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 27757 25600 145 145 0 27612 0
[pid=5250] vsize: 111028
Current children cumulated CPU time (s) 808.48
Current children cumulated vsize (Kb) 113152

[startup+820.106 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 26685 0 0 0 81691 154 0 0 25 0 1 0 1843273106 114425856 25779 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 27936 25779 145 145 0 27791 0
[pid=5250] vsize: 111744
Current children cumulated CPU time (s) 818.46
Current children cumulated vsize (Kb) 113868

[startup+830.107 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 26829 0 0 0 82689 155 0 0 25 0 1 0 1843273106 115011584 25923 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 28079 25923 145 145 0 27934 0
[pid=5250] vsize: 112316
Current children cumulated CPU time (s) 828.45
Current children cumulated vsize (Kb) 114440

[startup+840.107 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27009 0 0 0 83686 156 0 0 25 0 1 0 1843273106 115748864 26103 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 28259 26103 145 145 0 28114 0
[pid=5250] vsize: 113036
Current children cumulated CPU time (s) 838.43
Current children cumulated vsize (Kb) 115160

[startup+850.108 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27161 0 0 0 84684 156 0 0 25 0 1 0 1843273106 116371456 26255 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 28411 26255 145 145 0 28266 0
[pid=5250] vsize: 113644
Current children cumulated CPU time (s) 848.41
Current children cumulated vsize (Kb) 115768

[startup+860.109 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27287 0 0 0 85683 157 0 0 25 0 1 0 1843273106 116883456 26381 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 28536 26381 145 145 0 28391 0
[pid=5250] vsize: 114144
Current children cumulated CPU time (s) 858.41
Current children cumulated vsize (Kb) 116268

[startup+870.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27445 0 0 0 86681 158 0 0 25 0 1 0 1843273106 117530624 26539 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 28694 26539 145 145 0 28549 0
[pid=5250] vsize: 114776
Current children cumulated CPU time (s) 868.4
Current children cumulated vsize (Kb) 116900

[startup+880.111 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27623 0 0 0 87679 159 0 0 25 0 1 0 1843273106 118263808 26717 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 28873 26718 145 145 0 28728 0
[pid=5250] vsize: 115492
Current children cumulated CPU time (s) 878.39
Current children cumulated vsize (Kb) 117616

[startup+890.112 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27797 0 0 0 88677 160 0 0 25 0 1 0 1843273106 118968320 26891 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 29045 26891 145 145 0 28900 0
[pid=5250] vsize: 116180
Current children cumulated CPU time (s) 888.38
Current children cumulated vsize (Kb) 118304

[startup+900.113 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27974 0 0 0 89675 161 0 0 25 0 1 0 1843273106 119693312 27068 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 29222 27068 145 145 0 29077 0
[pid=5250] vsize: 116888
Current children cumulated CPU time (s) 898.37
Current children cumulated vsize (Kb) 119012

[startup+910.114 s]
Raw data (loadavg): 0.99 0.97 0.96 3/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 28116 0 0 0 90673 161 0 0 25 0 1 0 1843273106 120270848 27210 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 29363 27210 145 145 0 29218 0
[pid=5250] vsize: 117452
Current children cumulated CPU time (s) 908.35
Current children cumulated vsize (Kb) 119576

[startup+920.115 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 28299 0 0 0 91671 162 0 0 25 0 1 0 1843273106 121028608 27393 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 29548 27393 145 145 0 29403 0
[pid=5250] vsize: 118192
Current children cumulated CPU time (s) 918.34
Current children cumulated vsize (Kb) 120316

[startup+930.116 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 28449 0 0 0 92668 164 0 0 25 0 1 0 1843273106 121630720 27543 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 29695 27543 145 145 0 29550 0
[pid=5250] vsize: 118780
Current children cumulated CPU time (s) 928.33
Current children cumulated vsize (Kb) 120904

[startup+940.117 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 28632 0 0 0 93666 165 0 0 25 0 1 0 1843273106 122380288 27726 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 29878 27726 145 145 0 29733 0
[pid=5250] vsize: 119512
Current children cumulated CPU time (s) 938.32
Current children cumulated vsize (Kb) 121636

[startup+950.117 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 28792 0 0 0 94664 166 0 0 25 0 1 0 1843273106 123047936 27886 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 30041 27886 145 145 0 29896 0
[pid=5250] vsize: 120164
Current children cumulated CPU time (s) 948.31
Current children cumulated vsize (Kb) 122288

[startup+960.119 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 28995 0 0 0 95660 168 0 0 25 0 1 0 1843273106 123871232 28089 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 30242 28089 145 145 0 30097 0
[pid=5250] vsize: 120968
Current children cumulated CPU time (s) 958.29
Current children cumulated vsize (Kb) 123092

[startup+970.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29151 0 0 0 96657 169 0 0 25 0 1 0 1843273106 124518400 28245 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 30400 28245 145 145 0 30255 0
[pid=5250] vsize: 121600
Current children cumulated CPU time (s) 968.27
Current children cumulated vsize (Kb) 123724

[startup+980.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29275 0 0 0 97655 170 0 0 25 0 1 0 1843273106 125022208 28369 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 30523 28369 145 145 0 30378 0
[pid=5250] vsize: 122092
Current children cumulated CPU time (s) 978.26
Current children cumulated vsize (Kb) 124216

[startup+990.121 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29389 0 0 0 98653 171 0 0 25 0 1 0 1843273106 125485056 28483 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 30636 28483 145 145 0 30491 0
[pid=5250] vsize: 122544
Current children cumulated CPU time (s) 988.25
Current children cumulated vsize (Kb) 124668

[startup+1000.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29538 0 0 0 99650 173 0 0 25 0 1 0 1843273106 126091264 28632 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 30784 28632 145 145 0 30639 0
[pid=5250] vsize: 123136
Current children cumulated CPU time (s) 998.24
Current children cumulated vsize (Kb) 125260

[startup+1010.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29679 0 0 0 100648 174 0 0 25 0 1 0 1843273106 126668800 28773 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 30925 28773 145 145 0 30780 0
[pid=5250] vsize: 123700
Current children cumulated CPU time (s) 1008.23
Current children cumulated vsize (Kb) 125824

[startup+1020.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29821 0 0 0 101645 175 0 0 25 0 1 0 1843273106 127250432 28915 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 31067 28915 145 145 0 30922 0
[pid=5250] vsize: 124268
Current children cumulated CPU time (s) 1018.21
Current children cumulated vsize (Kb) 126392

[startup+1030.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29971 0 0 0 102643 177 0 0 25 0 1 0 1843273106 127868928 29065 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 31218 29065 145 145 0 31073 0
[pid=5250] vsize: 124872
Current children cumulated CPU time (s) 1028.21
Current children cumulated vsize (Kb) 126996

[startup+1040.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 30134 0 0 0 103641 178 0 0 25 0 1 0 1843273106 128532480 29228 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 31380 29228 145 145 0 31235 0
[pid=5250] vsize: 125520
Current children cumulated CPU time (s) 1038.2
Current children cumulated vsize (Kb) 127644

[startup+1050.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 30280 0 0 0 104639 179 0 0 25 0 1 0 1843273106 129130496 29374 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 31526 29374 145 145 0 31381 0
[pid=5250] vsize: 126104
Current children cumulated CPU time (s) 1048.19
Current children cumulated vsize (Kb) 128228

[startup+1060.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 30487 0 0 0 105635 180 0 0 25 0 1 0 1843273106 129974272 29581 4294967295 134512640 135094434 3221224448 3221223120 134555673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 31732 29581 145 145 0 31587 0
[pid=5250] vsize: 126928
Current children cumulated CPU time (s) 1058.16
Current children cumulated vsize (Kb) 129052

[startup+1070.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 30587 0 0 0 106634 181 0 0 25 0 1 0 1843273106 130383872 29681 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 31832 29681 145 145 0 31687 0
[pid=5250] vsize: 127328
Current children cumulated CPU time (s) 1068.16
Current children cumulated vsize (Kb) 129452

[startup+1080.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 30630 0 0 0 107633 181 0 0 25 0 1 0 1843273106 130555904 29724 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 31874 29724 145 145 0 31729 0
[pid=5250] vsize: 127496
Current children cumulated CPU time (s) 1078.15
Current children cumulated vsize (Kb) 129620

[startup+1090.13 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 30872 0 0 0 108631 183 0 0 25 0 1 0 1843273106 131522560 29966 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 32110 29966 145 145 0 31965 0
[pid=5250] vsize: 128440
Current children cumulated CPU time (s) 1088.15
Current children cumulated vsize (Kb) 130564

[startup+1100.14 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 31212 0 0 0 109627 185 0 0 25 0 1 0 1843273106 132915200 30306 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 32450 30306 145 145 0 32305 0
[pid=5250] vsize: 129800
Current children cumulated CPU time (s) 1098.13
Current children cumulated vsize (Kb) 131924

[startup+1110.14 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 31530 0 0 0 110624 186 0 0 25 0 1 0 1843273106 134213632 30624 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 32767 30624 145 145 0 32622 0
[pid=5250] vsize: 131068
Current children cumulated CPU time (s) 1108.11
Current children cumulated vsize (Kb) 133192

[startup+1120.15 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 31911 0 0 0 111621 188 0 0 25 0 1 0 1843273106 135770112 31005 4294967295 134512640 135094434 3221224448 3221223040 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 33147 31005 145 145 0 33002 0
[pid=5250] vsize: 132588
Current children cumulated CPU time (s) 1118.1
Current children cumulated vsize (Kb) 134712

[startup+1130.15 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 32204 0 0 0 112617 189 0 0 25 0 1 0 1843273106 136970240 31298 4294967295 134512640 135094434 3221224448 3221223040 134556975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 33440 31298 145 145 0 33295 0
[pid=5250] vsize: 133760
Current children cumulated CPU time (s) 1128.07
Current children cumulated vsize (Kb) 135884

[startup+1140.15 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 32600 0 0 0 113613 191 0 0 25 0 1 0 1843273106 138588160 31694 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 33835 31694 145 145 0 33690 0
[pid=5250] vsize: 135340
Current children cumulated CPU time (s) 1138.05
Current children cumulated vsize (Kb) 137464

[startup+1150.15 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 33002 0 0 0 114610 193 0 0 25 0 1 0 1843273106 140234752 32096 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 34237 32096 145 145 0 34092 0
[pid=5250] vsize: 136948
Current children cumulated CPU time (s) 1148.04
Current children cumulated vsize (Kb) 139072

[startup+1160.15 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 33310 0 0 0 115607 195 0 0 25 0 1 0 1843273106 141492224 32404 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 34544 32404 145 145 0 34399 0
[pid=5250] vsize: 138176
Current children cumulated CPU time (s) 1158.03
Current children cumulated vsize (Kb) 140300

[startup+1170.15 s]
Raw data (loadavg): 1.07 0.99 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 33700 0 0 0 116603 197 0 0 25 0 1 0 1843273106 143089664 32794 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 34934 32794 145 145 0 34789 0
[pid=5250] vsize: 139736
Current children cumulated CPU time (s) 1168.01
Current children cumulated vsize (Kb) 141860

[startup+1180.15 s]
Raw data (loadavg): 1.06 0.99 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 33985 0 0 0 117600 198 0 0 25 0 1 0 1843273106 144236544 33079 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 35214 33079 145 145 0 35069 0
[pid=5250] vsize: 140856
Current children cumulated CPU time (s) 1177.99
Current children cumulated vsize (Kb) 142980

[startup+1190.15 s]
Raw data (loadavg): 1.05 0.99 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 34359 0 0 0 118596 200 0 0 25 0 1 0 1843273106 145764352 33453 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 35587 33453 145 145 0 35442 0
[pid=5250] vsize: 142348
Current children cumulated CPU time (s) 1187.97
Current children cumulated vsize (Kb) 144472

[startup+1200.15 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 34563 0 0 0 119594 201 0 0 25 0 1 0 1843273106 146595840 33657 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 35790 33657 145 145 0 35645 0
[pid=5250] vsize: 143160
Current children cumulated CPU time (s) 1197.96
Current children cumulated vsize (Kb) 145284

[startup+1210.15 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 34581 0 0 0 120594 201 0 0 25 0 1 0 1843273106 146665472 33675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 35807 33675 145 145 0 35662 0
[pid=5250] vsize: 143228
Current children cumulated CPU time (s) 1207.96
Current children cumulated vsize (Kb) 145352



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.16 s]
Raw data (loadavg): 1.04 0.99 0.96 2/57 5250
Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5246/statm): 531 226 485 147 0 384 0
[pid=5246] vsize: 2124
Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 34581 0 0 0 120594 201 0 0 25 0 1 0 1843273106 146665472 33675 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5250/statm): 35807 33675 145 145 0 35662 0
[pid=5250] vsize: 143228
Current children cumulated CPU time (s) 1207.96
Current children cumulated vsize (Kb) 145352

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

Child status: 10
Real time (s): 1210.22
CPU time (s): 1208.03
CPU user time (s): 1205.95
CPU system time (s): 2.07768
CPU usage (%): 99.8184
Max. virtual memory (cumulated for all children) (Kb): 145352

Verifier Data

ERROR: no interpretation found !