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/aloul/FPGA_SAT05/normalized-chnl20_21_pb.cnf.cr.opb
MD5SUM112c693a7a90a8dc93ad23dc136d9b75
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 22
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.027994
Number of variables840
Total number of constraints82
Number of constraints which are clauses42
Number of constraints which are cardinality constraints (but not clauses)40
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint21

Trace number 1559

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        920604 kB
Buffers:         33880 kB
Cached:          52896 kB
SwapCached:        536 kB
Active:          62396 kB
Inactive:        26940 kB
HighTotal:      131008 kB
HighFree:        76104 kB
LowTotal:       903652 kB
LowFree:        844500 kB
SwapTotal:     2097892 kB
SwapFree:      2096832 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5860 kB
Slab:            19048 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 16:08:53 (client local time) WITH STATUS 0 IN 1209.77 SECONDS
stats: 2350 7 1209.77 0

Solver Data

c Parsing PB file...
c Converting 82 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................
c ---[  39]---> BDD-cost:   39
c ---[  38]---> BDD-cost:   39
c ---[  37]---> BDD-cost:   39
c ---[  36]---> BDD-cost:   39
c ---[  35]---> BDD-cost:   39
c ---[  34]---> BDD-cost:   39
c ---[  33]---> BDD-cost:   39
c ---[  32]---> BDD-cost:   39
c ---[  31]---> BDD-cost:   39
c ---[  30]---> BDD-cost:   39
c ---[  29]---> BDD-cost:   39
c ---[  28]---> BDD-cost:   39
c ---[  27]---> BDD-cost:   39
c ---[  26]---> BDD-cost:   39
c ---[  25]---> BDD-cost:   39
c ---[  24]---> BDD-cost:   39
c ---[  23]---> BDD-cost:   39
c ---[  22]---> BDD-cost:   39
c ---[  21]---> BDD-cost:   39
c ---[  20]---> BDD-cost:   39
c ---[  19]---> BDD-cost:   39
c ---[  18]---> BDD-cost:   39
c ---[  17]---> BDD-cost:   39
c ---[  16]---> BDD-cost:   39
c ---[  15]---> BDD-cost:   39
c ---[  14]---> BDD-cost:   39
c ---[  13]---> BDD-cost:   39
c ---[  12]---> BDD-cost:   39
c ---[  11]---> BDD-cost:   39
c ---[  10]---> BDD-cost:   39
c ---[   9]---> BDD-cost:   39
c ---[   8]---> BDD-cost:   39
c ---[   7]---> BDD-cost:   39
c ---[   6]---> BDD-cost:   39
c ---[   5]---> BDD-cost:   39
c ---[   4]---> BDD-cost:   39
c ---[   3]---> BDD-cost:   39
c ---[   2]---> BDD-cost:   39
c ---[   1]---> BDD-cost:   39
c ---[   0]---> BDD-cost:   39
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    3882    10840 |    1294       0        0     nan |  0.000 % |
c |       105 |    3882    10840 |    1423     105     7385    70.3 |  1.667 % |
c |       255 |    3882    10840 |    1565     255    18850    73.9 |  1.667 % |
c |       481 |    3882    10840 |    1722     481    40545    84.3 |  1.667 % |
c |       818 |    3882    10840 |    1894     818    71265    87.1 |  1.667 % |
c |      1330 |    3882    10840 |    2083    1330   131039    98.5 |  1.667 % |
c |      2092 |    3882    10840 |    2292    2092   211172   100.9 |  1.667 % |
c |      3231 |    3882    10840 |    2521    1659   186225   112.3 |  1.667 % |
c |      4942 |    3882    10840 |    2773    3370   365003   108.3 |  1.667 % |
c |      7507 |    3882    10840 |    3051    2457   314757   128.1 |  1.667 % |
c |     11351 |    3882    10840 |    3356    2383   263788   110.7 |  1.667 % |
c |     17118 |    3882    10840 |    3691    3938   513865   130.5 |  1.667 % |
c |     25770 |    3882    10840 |    4061    3926   537570   136.9 |  1.667 % |
c |     38745 |    3882    10840 |    4467    4621   522096   113.0 |  1.667 % |
c |     58208 |    3882    10840 |    4913    3339   584284   175.0 |  1.667 % |
c |     87400 |    3882    10840 |    5405    5035   947887   188.3 |  1.667 % |
c |    131189 |    3882    10840 |    5945    3280   620922   189.3 |  1.667 % |
c |    196874 |    3882    10840 |    6540    5430   876118   161.3 |  1.667 % |
c |    295400 |    3882    10840 |    7194    4105   759531   185.0 |  1.667 % |
c |    443191 |    3882    10840 |    7913    8832  1414915   160.2 |  1.667 % |
c |    664876 |    3882    10840 |    8705    6366  1068393   167.8 |  1.667 % |

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/26654/stat): 26654 (minisat+_script) R 26653 26654 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842458517 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/26654/statm): 174 3 169 147 0 27 0
[pid=26654] 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=26655
New process pid=26656
New process pid=26657
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
One traced child (pid=26656) exited with status: 0
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=26657) exited with status: 0
One traced child (pid=26655) exited with status: 0
New process pid=26658
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-chnl20_21_pb.cnf.cr.opb

[startup+10.0046 s]
Raw data (loadavg): 0.93 0.95 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1039 0 0 0 984 4 0 0 25 0 1 0 1842458522 4562944 1026 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 1114 1026 145 145 0 969 0
[pid=26658] vsize: 4456
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 6580

[startup+20.0053 s]
Raw data (loadavg): 0.94 0.96 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1338 0 0 0 1980 6 0 0 25 0 1 0 1842458522 5808128 1325 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 1418 1325 145 145 0 1273 0
[pid=26658] vsize: 5672
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 7796

[startup+30.0071 s]
Raw data (loadavg): 0.95 0.96 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1375 0 0 0 2979 7 0 0 25 0 1 0 1842458522 5955584 1362 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 1454 1362 145 145 0 1309 0
[pid=26658] vsize: 5816
Current children cumulated CPU time (s) 29.87
Current children cumulated vsize (Kb) 7940

[startup+40.0077 s]
Raw data (loadavg): 0.95 0.96 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1695 0 0 0 3974 9 0 0 25 0 1 0 1842458522 7274496 1682 4294967295 134512640 135094434 3221224432 3221223056 134557655 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 1776 1682 145 145 0 1631 0
[pid=26658] vsize: 7104
Current children cumulated CPU time (s) 39.84
Current children cumulated vsize (Kb) 9228

[startup+50.0094 s]
Raw data (loadavg): 0.96 0.96 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1788 0 0 0 4973 9 0 0 25 0 1 0 1842458522 7671808 1775 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 1873 1775 145 145 0 1728 0
[pid=26658] vsize: 7492
Current children cumulated CPU time (s) 49.83
Current children cumulated vsize (Kb) 9616

[startup+60.0102 s]
Raw data (loadavg): 0.97 0.96 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1925 0 0 0 5971 10 0 0 25 0 1 0 1842458522 8261632 1912 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2017 1912 145 145 0 1872 0
[pid=26658] vsize: 8068
Current children cumulated CPU time (s) 59.82
Current children cumulated vsize (Kb) 10192

[startup+70.0109 s]
Raw data (loadavg): 0.97 0.96 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1953 0 0 0 6971 10 0 0 25 0 1 0 1842458522 8376320 1940 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2045 1940 145 145 0 1900 0
[pid=26658] vsize: 8180
Current children cumulated CPU time (s) 69.82
Current children cumulated vsize (Kb) 10304

[startup+80.0116 s]
Raw data (loadavg): 0.98 0.96 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2246 0 0 0 7965 13 0 0 25 0 1 0 1842458522 9576448 2233 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2338 2233 145 145 0 2193 0
[pid=26658] vsize: 9352
Current children cumulated CPU time (s) 79.79
Current children cumulated vsize (Kb) 11476

[startup+90.0123 s]
Raw data (loadavg): 0.98 0.96 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2321 0 0 0 8965 13 0 0 25 0 1 0 1842458522 9887744 2308 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2414 2308 145 145 0 2269 0
[pid=26658] vsize: 9656
Current children cumulated CPU time (s) 89.79
Current children cumulated vsize (Kb) 11780

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2322 0 0 0 9964 14 0 0 25 0 1 0 1842458522 9887744 2309 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2414 2309 145 145 0 2269 0
[pid=26658] vsize: 9656
Current children cumulated CPU time (s) 99.79
Current children cumulated vsize (Kb) 11780

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2322 0 0 0 10965 14 0 0 25 0 1 0 1842458522 9887744 2309 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2414 2309 145 145 0 2269 0
[pid=26658] vsize: 9656
Current children cumulated CPU time (s) 109.8
Current children cumulated vsize (Kb) 11780

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2323 0 0 0 11964 14 0 0 25 0 1 0 1842458522 9887744 2310 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2414 2310 145 145 0 2269 0
[pid=26658] vsize: 9656
Current children cumulated CPU time (s) 119.79
Current children cumulated vsize (Kb) 11780

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2492 0 0 0 12961 17 0 0 25 0 1 0 1842458522 10579968 2479 4294967295 134512640 135094434 3221224432 3221223088 134558017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2583 2479 145 145 0 2438 0
[pid=26658] vsize: 10332
Current children cumulated CPU time (s) 129.79
Current children cumulated vsize (Kb) 12456

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2566 0 0 0 13960 17 0 0 25 0 1 0 1842458522 10883072 2553 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2657 2553 145 145 0 2512 0
[pid=26658] vsize: 10628
Current children cumulated CPU time (s) 139.78
Current children cumulated vsize (Kb) 12752

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2566 0 0 0 14960 18 0 0 25 0 1 0 1842458522 10883072 2553 4294967295 134512640 135094434 3221224432 3221223104 134556502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2657 2553 145 145 0 2512 0
[pid=26658] vsize: 10628
Current children cumulated CPU time (s) 149.79
Current children cumulated vsize (Kb) 12752

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2566 0 0 0 15960 18 0 0 25 0 1 0 1842458522 10883072 2553 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2657 2553 145 145 0 2512 0
[pid=26658] vsize: 10628
Current children cumulated CPU time (s) 159.79
Current children cumulated vsize (Kb) 12752

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2566 0 0 0 16960 18 0 0 25 0 1 0 1842458522 10883072 2553 4294967295 134512640 135094434 3221224432 3221223104 134556277 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2657 2553 145 145 0 2512 0
[pid=26658] vsize: 10628
Current children cumulated CPU time (s) 169.79
Current children cumulated vsize (Kb) 12752

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2566 0 0 0 17960 18 0 0 25 0 1 0 1842458522 10883072 2553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2657 2553 145 145 0 2512 0
[pid=26658] vsize: 10628
Current children cumulated CPU time (s) 179.79
Current children cumulated vsize (Kb) 12752

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2596 0 0 0 18959 19 0 0 25 0 1 0 1842458522 11001856 2583 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2686 2583 145 145 0 2541 0
[pid=26658] vsize: 10744
Current children cumulated CPU time (s) 189.79
Current children cumulated vsize (Kb) 12868

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2597 0 0 0 19959 19 0 0 25 0 1 0 1842458522 11001856 2584 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 2686 2584 145 145 0 2541 0
[pid=26658] vsize: 10744
Current children cumulated CPU time (s) 199.79
Current children cumulated vsize (Kb) 12868

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2599 0 0 0 20958 19 0 0 25 0 1 0 1842458522 11001856 2586 4294967295 134512640 135094434 3221224432 3221222912 134781611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 2686 2586 145 145 0 2541 0
[pid=26658] vsize: 10744
Current children cumulated CPU time (s) 209.78
Current children cumulated vsize (Kb) 12868

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2599 0 0 0 21958 19 0 0 25 0 1 0 1842458522 11001856 2586 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2686 2586 145 145 0 2541 0
[pid=26658] vsize: 10744
Current children cumulated CPU time (s) 219.78
Current children cumulated vsize (Kb) 12868

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2599 0 0 0 22958 19 0 0 25 0 1 0 1842458522 11001856 2586 4294967295 134512640 135094434 3221224432 3221223024 134551860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2686 2586 145 145 0 2541 0
[pid=26658] vsize: 10744
Current children cumulated CPU time (s) 229.78
Current children cumulated vsize (Kb) 12868

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2626 0 0 0 23957 20 0 0 25 0 1 0 1842458522 11116544 2613 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2714 2613 145 145 0 2569 0
[pid=26658] vsize: 10856
Current children cumulated CPU time (s) 239.78
Current children cumulated vsize (Kb) 12980

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2701 0 0 0 24957 20 0 0 25 0 1 0 1842458522 11423744 2688 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2789 2688 145 145 0 2644 0
[pid=26658] vsize: 11156
Current children cumulated CPU time (s) 249.78
Current children cumulated vsize (Kb) 13280

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2790 0 0 0 25955 21 0 0 25 0 1 0 1842458522 11788288 2777 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2878 2777 145 145 0 2733 0
[pid=26658] vsize: 11512
Current children cumulated CPU time (s) 259.77
Current children cumulated vsize (Kb) 13636

[startup+270.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2790 0 0 0 26955 21 0 0 25 0 1 0 1842458522 11788288 2777 4294967295 134512640 135094434 3221224432 3221223104 134555748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2878 2777 145 145 0 2733 0
[pid=26658] vsize: 11512
Current children cumulated CPU time (s) 269.77
Current children cumulated vsize (Kb) 13636

[startup+280.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2791 0 0 0 27956 21 0 0 25 0 1 0 1842458522 11788288 2778 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2878 2778 145 145 0 2733 0
[pid=26658] vsize: 11512
Current children cumulated CPU time (s) 279.78
Current children cumulated vsize (Kb) 13636

[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2889 0 0 0 28954 22 0 0 25 0 1 0 1842458522 12185600 2876 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2975 2876 145 145 0 2830 0
[pid=26658] vsize: 11900
Current children cumulated CPU time (s) 289.77
Current children cumulated vsize (Kb) 14024

[startup+300.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2889 0 0 0 29954 22 0 0 25 0 1 0 1842458522 12185600 2876 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 2975 2876 145 145 0 2830 0
[pid=26658] vsize: 11900
Current children cumulated CPU time (s) 299.77
Current children cumulated vsize (Kb) 14024

[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3021 0 0 0 30952 23 0 0 25 0 1 0 1842458522 12726272 3008 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3107 3008 145 145 0 2962 0
[pid=26658] vsize: 12428
Current children cumulated CPU time (s) 309.76
Current children cumulated vsize (Kb) 14552

[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3021 0 0 0 31952 23 0 0 25 0 1 0 1842458522 12726272 3008 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3107 3008 145 145 0 2962 0
[pid=26658] vsize: 12428
Current children cumulated CPU time (s) 319.76
Current children cumulated vsize (Kb) 14552

[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3021 0 0 0 32952 23 0 0 25 0 1 0 1842458522 12726272 3008 4294967295 134512640 135094434 3221224432 3221223104 134556091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3107 3008 145 145 0 2962 0
[pid=26658] vsize: 12428
Current children cumulated CPU time (s) 329.76
Current children cumulated vsize (Kb) 14552

[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3373 0 0 0 33947 25 0 0 25 0 1 0 1842458522 14176256 3360 4294967295 134512640 135094434 3221224432 3221223024 134557163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3461 3360 145 145 0 3316 0
[pid=26658] vsize: 13844
Current children cumulated CPU time (s) 339.73
Current children cumulated vsize (Kb) 15968

[startup+350.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3386 0 0 0 34947 25 0 0 25 0 1 0 1842458522 14229504 3373 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3474 3373 145 145 0 3329 0
[pid=26658] vsize: 13896
Current children cumulated CPU time (s) 349.73
Current children cumulated vsize (Kb) 16020

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3436 0 0 0 35946 26 0 0 25 0 1 0 1842458522 14434304 3423 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3423 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 359.73
Current children cumulated vsize (Kb) 16220

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3436 0 0 0 36946 26 0 0 25 0 1 0 1842458522 14434304 3423 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3423 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 369.73
Current children cumulated vsize (Kb) 16220

[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3436 0 0 0 37947 26 0 0 25 0 1 0 1842458522 14434304 3423 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3423 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 379.74
Current children cumulated vsize (Kb) 16220

[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3436 0 0 0 38947 26 0 0 25 0 1 0 1842458522 14434304 3423 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3423 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 389.74
Current children cumulated vsize (Kb) 16220

[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 39947 26 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 399.74
Current children cumulated vsize (Kb) 16220

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 40947 26 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 409.74
Current children cumulated vsize (Kb) 16220

[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 41947 26 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 419.74
Current children cumulated vsize (Kb) 16220

[startup+430.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 42947 26 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 429.74
Current children cumulated vsize (Kb) 16220

[startup+440.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 43947 26 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 439.74
Current children cumulated vsize (Kb) 16220

[startup+450.039 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 44948 27 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 449.76
Current children cumulated vsize (Kb) 16220

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 45948 27 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 459.76
Current children cumulated vsize (Kb) 16220

[startup+470.041 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 46948 27 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 469.76
Current children cumulated vsize (Kb) 16220

[startup+480.042 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3438 0 0 0 47948 27 0 0 25 0 1 0 1842458522 14434304 3425 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3425 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 479.76
Current children cumulated vsize (Kb) 16220

[startup+490.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3438 0 0 0 48948 27 0 0 25 0 1 0 1842458522 14434304 3425 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3524 3425 145 145 0 3379 0
[pid=26658] vsize: 14096
Current children cumulated CPU time (s) 489.76
Current children cumulated vsize (Kb) 16220

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3444 0 0 0 49948 27 0 0 25 0 1 0 1842458522 14475264 3431 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3534 3431 145 145 0 3389 0
[pid=26658] vsize: 14136
Current children cumulated CPU time (s) 499.76
Current children cumulated vsize (Kb) 16260

[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3474 0 0 0 50948 27 0 0 25 0 1 0 1842458522 14671872 3461 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3582 3461 145 145 0 3437 0
[pid=26658] vsize: 14328
Current children cumulated CPU time (s) 509.76
Current children cumulated vsize (Kb) 16452

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3474 0 0 0 51949 27 0 0 25 0 1 0 1842458522 14671872 3461 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3582 3461 145 145 0 3437 0
[pid=26658] vsize: 14328
Current children cumulated CPU time (s) 519.77
Current children cumulated vsize (Kb) 16452

[startup+530.047 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3475 0 0 0 52948 28 0 0 25 0 1 0 1842458522 14671872 3462 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3582 3462 145 145 0 3437 0
[pid=26658] vsize: 14328
Current children cumulated CPU time (s) 529.77
Current children cumulated vsize (Kb) 16452

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3495 0 0 0 53948 28 0 0 25 0 1 0 1842458522 14802944 3482 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3614 3482 145 145 0 3469 0
[pid=26658] vsize: 14456
Current children cumulated CPU time (s) 539.77
Current children cumulated vsize (Kb) 16580

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3542 0 0 0 54948 28 0 0 25 0 1 0 1842458522 15040512 3529 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3672 3529 145 145 0 3527 0
[pid=26658] vsize: 14688
Current children cumulated CPU time (s) 549.77
Current children cumulated vsize (Kb) 16812

[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3553 0 0 0 55948 28 0 0 25 0 1 0 1842458522 15106048 3540 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3688 3540 145 145 0 3543 0
[pid=26658] vsize: 14752
Current children cumulated CPU time (s) 559.77
Current children cumulated vsize (Kb) 16876

[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3553 0 0 0 56949 28 0 0 25 0 1 0 1842458522 15106048 3540 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3688 3540 145 145 0 3543 0
[pid=26658] vsize: 14752
Current children cumulated CPU time (s) 569.78
Current children cumulated vsize (Kb) 16876

[startup+580.05 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3556 0 0 0 57949 28 0 0 25 0 1 0 1842458522 15106048 3543 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3688 3543 145 145 0 3543 0
[pid=26658] vsize: 14752
Current children cumulated CPU time (s) 579.78
Current children cumulated vsize (Kb) 16876

[startup+590.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3563 0 0 0 58949 28 0 0 25 0 1 0 1842458522 15138816 3550 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3696 3550 145 145 0 3551 0
[pid=26658] vsize: 14784
Current children cumulated CPU time (s) 589.78
Current children cumulated vsize (Kb) 16908

[startup+600.053 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3563 0 0 0 59949 28 0 0 25 0 1 0 1842458522 15138816 3550 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3696 3550 145 145 0 3551 0
[pid=26658] vsize: 14784
Current children cumulated CPU time (s) 599.78
Current children cumulated vsize (Kb) 16908

[startup+610.053 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3574 0 0 0 60949 29 0 0 25 0 1 0 1842458522 15200256 3561 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 3711 3561 145 145 0 3566 0
[pid=26658] vsize: 14844
Current children cumulated CPU time (s) 609.79
Current children cumulated vsize (Kb) 16968

[startup+620.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3974 0 0 0 61945 30 0 0 25 0 1 0 1842458522 16842752 3961 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4112 3961 145 145 0 3967 0
[pid=26658] vsize: 16448
Current children cumulated CPU time (s) 619.76
Current children cumulated vsize (Kb) 18572

[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4024 0 0 0 62944 31 0 0 25 0 1 0 1842458522 17047552 4011 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4162 4011 145 145 0 4017 0
[pid=26658] vsize: 16648
Current children cumulated CPU time (s) 629.76
Current children cumulated vsize (Kb) 18772

[startup+640.055 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4025 0 0 0 63944 31 0 0 25 0 1 0 1842458522 17047552 4012 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4162 4012 145 145 0 4017 0
[pid=26658] vsize: 16648
Current children cumulated CPU time (s) 639.76
Current children cumulated vsize (Kb) 18772

[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4025 0 0 0 64944 31 0 0 25 0 1 0 1842458522 17047552 4012 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4162 4012 145 145 0 4017 0
[pid=26658] vsize: 16648
Current children cumulated CPU time (s) 649.76
Current children cumulated vsize (Kb) 18772

[startup+660.057 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4025 0 0 0 65944 31 0 0 25 0 1 0 1842458522 17047552 4012 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4162 4012 145 145 0 4017 0
[pid=26658] vsize: 16648
Current children cumulated CPU time (s) 659.76
Current children cumulated vsize (Kb) 18772

[startup+670.057 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4039 0 0 0 66944 31 0 0 25 0 1 0 1842458522 17104896 4026 4294967295 134512640 135094434 3221224432 3221222840 134782729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4176 4026 145 145 0 4031 0
[pid=26658] vsize: 16704
Current children cumulated CPU time (s) 669.76
Current children cumulated vsize (Kb) 18828

[startup+680.057 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4039 0 0 0 67944 31 0 0 25 0 1 0 1842458522 17104896 4026 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4176 4026 145 145 0 4031 0
[pid=26658] vsize: 16704
Current children cumulated CPU time (s) 679.76
Current children cumulated vsize (Kb) 18828

[startup+690.058 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4072 0 0 0 68944 31 0 0 25 0 1 0 1842458522 17256448 4059 4294967295 134512640 135094434 3221224432 3221223024 134556876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4213 4059 145 145 0 4068 0
[pid=26658] vsize: 16852
Current children cumulated CPU time (s) 689.76
Current children cumulated vsize (Kb) 18976

[startup+700.06 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4072 0 0 0 69944 32 0 0 25 0 1 0 1842458522 17256448 4059 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4213 4059 145 145 0 4068 0
[pid=26658] vsize: 16852
Current children cumulated CPU time (s) 699.77
Current children cumulated vsize (Kb) 18976

[startup+710.06 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4080 0 0 0 70944 32 0 0 25 0 1 0 1842458522 17289216 4067 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4221 4067 145 145 0 4076 0
[pid=26658] vsize: 16884
Current children cumulated CPU time (s) 709.77
Current children cumulated vsize (Kb) 19008

[startup+720.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4080 0 0 0 71944 33 0 0 25 0 1 0 1842458522 17289216 4067 4294967295 134512640 135094434 3221224432 3221223104 134556515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4221 4067 145 145 0 4076 0
[pid=26658] vsize: 16884
Current children cumulated CPU time (s) 719.78
Current children cumulated vsize (Kb) 19008

[startup+730.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4101 0 0 0 72943 34 0 0 25 0 1 0 1842458522 17387520 4088 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4245 4088 145 145 0 4100 0
[pid=26658] vsize: 16980
Current children cumulated CPU time (s) 729.78
Current children cumulated vsize (Kb) 19104

[startup+740.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4112 0 0 0 73943 34 0 0 25 0 1 0 1842458522 17453056 4099 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4261 4099 145 145 0 4116 0
[pid=26658] vsize: 17044
Current children cumulated CPU time (s) 739.78
Current children cumulated vsize (Kb) 19168

[startup+750.065 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4119 0 0 0 74943 34 0 0 25 0 1 0 1842458522 17485824 4106 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4269 4106 145 145 0 4124 0
[pid=26658] vsize: 17076
Current children cumulated CPU time (s) 749.78
Current children cumulated vsize (Kb) 19200

[startup+760.066 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4120 0 0 0 75943 34 0 0 25 0 1 0 1842458522 17485824 4107 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4269 4107 145 145 0 4124 0
[pid=26658] vsize: 17076
Current children cumulated CPU time (s) 759.78
Current children cumulated vsize (Kb) 19200

[startup+770.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4128 0 0 0 76943 35 0 0 25 0 1 0 1842458522 17518592 4115 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4277 4115 145 145 0 4132 0
[pid=26658] vsize: 17108
Current children cumulated CPU time (s) 769.79
Current children cumulated vsize (Kb) 19232

[startup+780.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4128 0 0 0 77943 35 0 0 25 0 1 0 1842458522 17518592 4115 4294967295 134512640 135094434 3221224432 3221223072 134562165 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4277 4115 145 145 0 4132 0
[pid=26658] vsize: 17108
Current children cumulated CPU time (s) 779.79
Current children cumulated vsize (Kb) 19232

[startup+790.068 s]
Raw data (loadavg): 1.07 0.99 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4128 0 0 0 78943 35 0 0 25 0 1 0 1842458522 17518592 4115 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4277 4115 145 145 0 4132 0
[pid=26658] vsize: 17108
Current children cumulated CPU time (s) 789.79
Current children cumulated vsize (Kb) 19232

[startup+800.069 s]
Raw data (loadavg): 1.06 0.99 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4139 0 0 0 79942 35 0 0 25 0 1 0 1842458522 17563648 4126 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 4288 4126 145 145 0 4143 0
[pid=26658] vsize: 17152
Current children cumulated CPU time (s) 799.78
Current children cumulated vsize (Kb) 19276

[startup+810.069 s]
Raw data (loadavg): 1.05 0.99 0.95 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4169 0 0 0 80941 36 0 0 25 0 1 0 1842458522 17715200 4156 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4325 4156 145 145 0 4180 0
[pid=26658] vsize: 17300
Current children cumulated CPU time (s) 809.78
Current children cumulated vsize (Kb) 19424

[startup+820.07 s]
Raw data (loadavg): 1.12 1.00 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4194 0 0 0 81941 36 0 0 25 0 1 0 1842458522 17846272 4181 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4357 4181 145 145 0 4212 0
[pid=26658] vsize: 17428
Current children cumulated CPU time (s) 819.78
Current children cumulated vsize (Kb) 19552

[startup+830.071 s]
Raw data (loadavg): 1.10 1.00 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4204 0 0 0 82941 37 0 0 25 0 1 0 1842458522 17895424 4191 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4369 4191 145 145 0 4224 0
[pid=26658] vsize: 17476
Current children cumulated CPU time (s) 829.79
Current children cumulated vsize (Kb) 19600

[startup+840.072 s]
Raw data (loadavg): 1.09 1.00 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4222 0 0 0 83941 37 0 0 25 0 1 0 1842458522 17993728 4209 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4393 4209 145 145 0 4248 0
[pid=26658] vsize: 17572
Current children cumulated CPU time (s) 839.79
Current children cumulated vsize (Kb) 19696

[startup+850.073 s]
Raw data (loadavg): 1.15 1.02 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4229 0 0 0 84941 37 0 0 25 0 1 0 1842458522 18026496 4216 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4401 4216 145 145 0 4256 0
[pid=26658] vsize: 17604
Current children cumulated CPU time (s) 849.79
Current children cumulated vsize (Kb) 19728

[startup+860.074 s]
Raw data (loadavg): 1.13 1.02 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4299 0 0 0 85940 37 0 0 25 0 1 0 1842458522 18325504 4286 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4474 4286 145 145 0 4329 0
[pid=26658] vsize: 17896
Current children cumulated CPU time (s) 859.78
Current children cumulated vsize (Kb) 20020

[startup+870.075 s]
Raw data (loadavg): 1.11 1.02 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4643 0 0 0 86936 39 0 0 25 0 1 0 1842458522 19755008 4630 4294967295 134512640 135094434 3221224432 3221223024 134551457 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4823 4630 145 145 0 4678 0
[pid=26658] vsize: 19292
Current children cumulated CPU time (s) 869.76
Current children cumulated vsize (Kb) 21416

[startup+880.076 s]
Raw data (loadavg): 1.09 1.01 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4668 0 0 0 87936 39 0 0 25 0 1 0 1842458522 19857408 4655 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4848 4655 145 145 0 4703 0
[pid=26658] vsize: 19392
Current children cumulated CPU time (s) 879.76
Current children cumulated vsize (Kb) 21516

[startup+890.077 s]
Raw data (loadavg): 1.08 1.01 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4723 0 0 0 88935 40 0 0 25 0 1 0 1842458522 20090880 4710 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4905 4710 145 145 0 4760 0
[pid=26658] vsize: 19620
Current children cumulated CPU time (s) 889.76
Current children cumulated vsize (Kb) 21744

[startup+900.078 s]
Raw data (loadavg): 1.06 1.01 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4723 0 0 0 89935 40 0 0 25 0 1 0 1842458522 20090880 4710 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4905 4710 145 145 0 4760 0
[pid=26658] vsize: 19620
Current children cumulated CPU time (s) 899.76
Current children cumulated vsize (Kb) 21744

[startup+910.079 s]
Raw data (loadavg): 1.05 1.01 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4724 0 0 0 90935 40 0 0 25 0 1 0 1842458522 20090880 4711 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4905 4711 145 145 0 4760 0
[pid=26658] vsize: 19620
Current children cumulated CPU time (s) 909.76
Current children cumulated vsize (Kb) 21744

[startup+920.079 s]
Raw data (loadavg): 1.05 1.01 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4724 0 0 0 91935 40 0 0 25 0 1 0 1842458522 20090880 4711 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4905 4711 145 145 0 4760 0
[pid=26658] vsize: 19620
Current children cumulated CPU time (s) 919.76
Current children cumulated vsize (Kb) 21744

[startup+930.08 s]
Raw data (loadavg): 1.04 1.01 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4724 0 0 0 92935 40 0 0 25 0 1 0 1842458522 20090880 4711 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 4905 4711 145 145 0 4760 0
[pid=26658] vsize: 19620
Current children cumulated CPU time (s) 929.76
Current children cumulated vsize (Kb) 21744

[startup+940.081 s]
Raw data (loadavg): 1.03 1.01 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4850 0 0 0 93934 41 0 0 25 0 1 0 1842458522 20602880 4837 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5030 4837 145 145 0 4885 0
[pid=26658] vsize: 20120
Current children cumulated CPU time (s) 939.76
Current children cumulated vsize (Kb) 22244

[startup+950.082 s]
Raw data (loadavg): 1.03 1.01 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4892 0 0 0 94933 42 0 0 25 0 1 0 1842458522 20774912 4879 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5072 4879 145 145 0 4927 0
[pid=26658] vsize: 20288
Current children cumulated CPU time (s) 949.76
Current children cumulated vsize (Kb) 22412

[startup+960.083 s]
Raw data (loadavg): 1.02 1.01 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 95932 42 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 959.75
Current children cumulated vsize (Kb) 22528

[startup+970.084 s]
Raw data (loadavg): 1.02 1.01 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 96932 43 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 969.76
Current children cumulated vsize (Kb) 22528

[startup+980.086 s]
Raw data (loadavg): 1.02 1.00 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 97932 43 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 979.76
Current children cumulated vsize (Kb) 22528

[startup+990.086 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 98931 44 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 989.76
Current children cumulated vsize (Kb) 22528

[startup+1000.09 s]
Raw data (loadavg): 1.09 1.02 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 99930 44 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 999.75
Current children cumulated vsize (Kb) 22528

[startup+1010.09 s]
Raw data (loadavg): 1.08 1.02 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 100930 45 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1009.76
Current children cumulated vsize (Kb) 22528

[startup+1020.09 s]
Raw data (loadavg): 1.06 1.02 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 101930 45 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1019.76
Current children cumulated vsize (Kb) 22528

[startup+1030.09 s]
Raw data (loadavg): 1.05 1.02 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4917 0 0 0 102930 46 0 0 25 0 1 0 1842458522 20893696 4904 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4904 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1029.77
Current children cumulated vsize (Kb) 22528

[startup+1040.09 s]
Raw data (loadavg): 1.04 1.02 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4917 0 0 0 103929 46 0 0 25 0 1 0 1842458522 20893696 4904 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4904 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1039.76
Current children cumulated vsize (Kb) 22528

[startup+1050.1 s]
Raw data (loadavg): 1.04 1.01 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4917 0 0 0 104929 46 0 0 25 0 1 0 1842458522 20893696 4904 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4904 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1049.76
Current children cumulated vsize (Kb) 22528

[startup+1060.1 s]
Raw data (loadavg): 1.03 1.01 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4917 0 0 0 105929 47 0 0 25 0 1 0 1842458522 20893696 4904 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4904 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1059.77
Current children cumulated vsize (Kb) 22528

[startup+1070.1 s]
Raw data (loadavg): 1.03 1.01 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4917 0 0 0 106929 47 0 0 25 0 1 0 1842458522 20893696 4904 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4904 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1069.77
Current children cumulated vsize (Kb) 22528

[startup+1080.1 s]
Raw data (loadavg): 1.02 1.01 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4918 0 0 0 107928 47 0 0 25 0 1 0 1842458522 20893696 4905 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4905 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1079.76
Current children cumulated vsize (Kb) 22528

[startup+1090.1 s]
Raw data (loadavg): 1.02 1.01 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4918 0 0 0 108928 47 0 0 25 0 1 0 1842458522 20893696 4905 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4905 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1089.76
Current children cumulated vsize (Kb) 22528

[startup+1100.1 s]
Raw data (loadavg): 1.01 1.01 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 109928 48 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1099.77
Current children cumulated vsize (Kb) 22528

[startup+1110.1 s]
Raw data (loadavg): 1.01 1.01 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 110928 48 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1109.77
Current children cumulated vsize (Kb) 22528

[startup+1120.1 s]
Raw data (loadavg): 1.01 1.01 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 111927 48 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1119.76
Current children cumulated vsize (Kb) 22528

[startup+1130.11 s]
Raw data (loadavg): 1.01 1.01 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 112927 49 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1129.77
Current children cumulated vsize (Kb) 22528

[startup+1140.11 s]
Raw data (loadavg): 1.01 1.01 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 113927 49 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1139.77
Current children cumulated vsize (Kb) 22528

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 114927 49 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1149.77
Current children cumulated vsize (Kb) 22528

[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 115926 50 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1159.77
Current children cumulated vsize (Kb) 22528

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 116926 50 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1169.77
Current children cumulated vsize (Kb) 22528

[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 117926 50 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0
[pid=26658] vsize: 20404
Current children cumulated CPU time (s) 1179.77
Current children cumulated vsize (Kb) 22528

[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 5187 0 0 0 118923 52 0 0 25 0 1 0 1842458522 21987328 5174 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 5368 5174 145 145 0 5223 0
[pid=26658] vsize: 21472
Current children cumulated CPU time (s) 1189.76
Current children cumulated vsize (Kb) 23596

[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 5261 0 0 0 119922 52 0 0 25 0 1 0 1842458522 22302720 5248 4294967295 134512640 135094434 3221224432 3221223072 134538541 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 5445 5248 145 145 0 5300 0
[pid=26658] vsize: 21780
Current children cumulated CPU time (s) 1199.75
Current children cumulated vsize (Kb) 23904

[startup+1210.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 5331 0 0 0 120922 53 0 0 25 0 1 0 1842458522 22589440 5318 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 5515 5318 145 145 0 5370 0
[pid=26658] vsize: 22060
Current children cumulated CPU time (s) 1209.76
Current children cumulated vsize (Kb) 24184



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 26658
Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26654/statm): 531 226 485 147 0 384 0
[pid=26654] vsize: 2124
Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 5331 0 0 0 120922 53 0 0 25 0 1 0 1842458522 22589440 5318 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26658/statm): 5515 5318 145 145 0 5370 0
[pid=26658] vsize: 22060
Current children cumulated CPU time (s) 1209.76
Current children cumulated vsize (Kb) 24184

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1209.77
CPU user time (s): 1209.22
CPU system time (s): 0.544917
CPU usage (%): 99.9703
Max. virtual memory (cumulated for all children) (Kb): 24184

Verifier Data

ERROR: no interpretation found !