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-chnl10_20_pb.cnf.cr.opb
MD5SUMf6063d1ff7b0ba7c7cab7a438daedff8
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 21
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.014997
Number of variables400
Total number of constraints60
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)20
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint10
Maximum length of a constraint20

Trace number 821

Launcher Data

LAUNCH ON wulflinc19 THE 2005-09-18 12:38:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2397 boxname=wulflinc19 idbench=53 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f6063d1ff7b0ba7c7cab7a438daedff8  /oldhome/oroussel/tmp/wulflinc19/normalized-chnl10_20_pb.cnf.cr.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-chnl10_20_pb.cnf.cr.opb
IDLAUNCH: 2397
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        947856 kB
Buffers:         33828 kB
Cached:          25860 kB
SwapCached:        832 kB
Active:          48812 kB
Inactive:        13444 kB
HighTotal:      131008 kB
HighFree:       104412 kB
LowTotal:       903652 kB
LowFree:        843444 kB
SwapTotal:     2097892 kB
SwapFree:      2096460 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5696 kB
Slab:            18968 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 12:46:14 (client local time) WITH STATUS 20 IN 437.402 SECONDS
stats: 2397 7 437.402 20

Solver Data

c Parsing PB file...
c Converting 60 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1860     5140 |     620       0        0     nan |  0.000 % |
c |       105 |    1860     5140 |     682     105     3115    29.7 |  1.754 % |
c |       255 |    1860     5140 |     750     255     9122    35.8 |  1.754 % |
c |       483 |    1860     5140 |     825     483    17860    37.0 |  1.757 % |
c |       827 |    1860     5140 |     907     827    34782    42.1 |  1.754 % |
c |      1336 |    1860     5140 |     998     794    35805    45.1 |  1.754 % |
c |      2095 |    1860     5140 |    1098     963    46131    47.9 |  1.755 % |
c |      3236 |    1860     5140 |    1208     855    38655    45.2 |  1.754 % |
c |      4945 |    1860     5140 |    1329    1223    54808    44.8 |  1.754 % |
c |      7507 |    1860     5140 |    1461    1529    70881    46.4 |  1.754 % |
c |     11351 |    1860     5140 |    1608    1297    60011    46.3 |  1.754 % |
c |     17122 |    1860     5140 |    1768     913    38075    41.7 |  1.754 % |
c |     25774 |    1860     5140 |    1945    1876    79748    42.5 |  1.754 % |
c |     38751 |    1860     5140 |    2140    2159    98991    45.9 |  1.754 % |
c |     58213 |    1860     5140 |    2354    1826    83310    45.6 |  1.754 % |
c |     87405 |    1860     5140 |    2589    1714    82979    48.4 |  1.754 % |
c |    131197 |    1860     5140 |    2848    2605   131009    50.3 |  1.754 % |
c |    196881 |    1860     5140 |    3133    2788   128801    46.2 |  1.754 % |
c |    295409 |    1860     5140 |    3447    2681   117056    43.7 |  1.754 % |
c |    443198 |    1860     5140 |    3791    2782   140828    50.6 |  1.754 % |
c |    664881 |    1860     5140 |    4171    3279   124739    38.0 |  1.754 % |
c |    997406 |    1860     5140 |    4588    3602   150963    41.9 |  1.758 % |
c ==============================================================================
c UNSATISFIABLE
s UNSATISFIABLE
c _______________________________________________________________________________
c 
c restarts              : 22
c conflicts             : 1137344        (2601 /sec)
c decisions             : 1289572        (2949 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 437.285 s
c _______________________________________________________________________________

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/8591/stat): 8591 (minisat+_script) R 8590 8591 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841303248 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/8591/statm): 174 3 169 147 0 27 0
[pid=8591] 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=8592
New process pid=8593
New process pid=8594
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
One traced child (pid=8593) exited with status: 0
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=8594) exited with status: 0
One traced child (pid=8592) exited with status: 0
New process pid=8595
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-chnl10_20_pb.cnf.cr.opb

[startup+10.004 s]
Raw data (loadavg): 0.87 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 416 0 0 0 990 1 0 0 25 0 1 0 1841303254 1994752 403 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8595/statm): 487 403 145 145 0 342 0
[pid=8595] vsize: 1948
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 4072

[startup+20.0059 s]
Raw data (loadavg): 0.89 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 485 0 0 0 1988 2 0 0 25 0 1 0 1841303254 2273280 472 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 555 472 145 145 0 410 0
[pid=8595] vsize: 2220
Current children cumulated CPU time (s) 19.9
Current children cumulated vsize (Kb) 4344

[startup+30.0077 s]
Raw data (loadavg): 0.91 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 528 0 0 0 2988 2 0 0 25 0 1 0 1841303254 2449408 515 4294967295 134512640 135094434 3221224432 3221223088 134557908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/8595/statm): 598 515 145 145 0 453 0
[pid=8595] vsize: 2392
Current children cumulated CPU time (s) 29.9
Current children cumulated vsize (Kb) 4516

[startup+40.0085 s]
Raw data (loadavg): 0.92 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 554 0 0 0 3987 2 0 0 25 0 1 0 1841303254 2555904 541 4294967295 134512640 135094434 3221224432 3221223024 134557251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 624 541 145 145 0 479 0
[pid=8595] vsize: 2496
Current children cumulated CPU time (s) 39.89
Current children cumulated vsize (Kb) 4620

[startup+50.0093 s]
Raw data (loadavg): 0.93 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 587 0 0 0 4987 3 0 0 25 0 1 0 1841303254 2691072 574 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 657 574 145 145 0 512 0
[pid=8595] vsize: 2628
Current children cumulated CPU time (s) 49.9
Current children cumulated vsize (Kb) 4752

[startup+60.0101 s]
Raw data (loadavg): 0.94 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 598 0 0 0 5987 3 0 0 25 0 1 0 1841303254 2736128 585 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 668 585 145 145 0 523 0
[pid=8595] vsize: 2672
Current children cumulated CPU time (s) 59.9
Current children cumulated vsize (Kb) 4796

[startup+70.0109 s]
Raw data (loadavg): 0.95 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 629 0 0 0 6987 3 0 0 25 0 1 0 1841303254 2867200 616 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 700 616 145 145 0 555 0
[pid=8595] vsize: 2800
Current children cumulated CPU time (s) 69.9
Current children cumulated vsize (Kb) 4924

[startup+80.0127 s]
Raw data (loadavg): 0.96 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 638 0 0 0 7987 3 0 0 25 0 1 0 1841303254 2908160 625 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 710 625 145 145 0 565 0
[pid=8595] vsize: 2840
Current children cumulated CPU time (s) 79.9
Current children cumulated vsize (Kb) 4964

[startup+90.0135 s]
Raw data (loadavg): 0.96 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 661 0 0 0 8987 3 0 0 25 0 1 0 1841303254 3010560 648 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 735 648 145 145 0 590 0
[pid=8595] vsize: 2940
Current children cumulated CPU time (s) 89.9
Current children cumulated vsize (Kb) 5064

[startup+100.014 s]
Raw data (loadavg): 0.97 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 674 0 0 0 9987 3 0 0 25 0 1 0 1841303254 3076096 661 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 751 661 145 145 0 606 0
[pid=8595] vsize: 3004
Current children cumulated CPU time (s) 99.9
Current children cumulated vsize (Kb) 5128

[startup+110.015 s]
Raw data (loadavg): 0.97 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 703 0 0 0 10985 4 0 0 25 0 1 0 1841303254 3207168 690 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 783 690 145 145 0 638 0
[pid=8595] vsize: 3132
Current children cumulated CPU time (s) 109.89
Current children cumulated vsize (Kb) 5256

[startup+120.016 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 769 0 0 0 11985 4 0 0 25 0 1 0 1841303254 3485696 756 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 851 756 145 145 0 706 0
[pid=8595] vsize: 3404
Current children cumulated CPU time (s) 119.89
Current children cumulated vsize (Kb) 5528

[startup+130.018 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 776 0 0 0 12985 4 0 0 25 0 1 0 1841303254 3518464 763 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 859 763 145 145 0 714 0
[pid=8595] vsize: 3436
Current children cumulated CPU time (s) 129.89
Current children cumulated vsize (Kb) 5560

[startup+140.019 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 789 0 0 0 13985 4 0 0 25 0 1 0 1841303254 3563520 776 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 870 776 145 145 0 725 0
[pid=8595] vsize: 3480
Current children cumulated CPU time (s) 139.89
Current children cumulated vsize (Kb) 5604

[startup+150.019 s]
Raw data (loadavg): 0.98 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 816 0 0 0 14985 5 0 0 25 0 1 0 1841303254 3686400 803 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 900 803 145 145 0 755 0
[pid=8595] vsize: 3600
Current children cumulated CPU time (s) 149.9
Current children cumulated vsize (Kb) 5724

[startup+160.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 836 0 0 0 15985 5 0 0 25 0 1 0 1841303254 3772416 823 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 921 823 145 145 0 776 0
[pid=8595] vsize: 3684
Current children cumulated CPU time (s) 159.9
Current children cumulated vsize (Kb) 5808

[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 847 0 0 0 16985 5 0 0 25 0 1 0 1841303254 3829760 834 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 935 834 145 145 0 790 0
[pid=8595] vsize: 3740
Current children cumulated CPU time (s) 169.9
Current children cumulated vsize (Kb) 5864

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 867 0 0 0 17985 5 0 0 25 0 1 0 1841303254 3928064 854 4294967295 134512640 135094434 3221224432 3221222992 134550337 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 959 854 145 145 0 814 0
[pid=8595] vsize: 3836
Current children cumulated CPU time (s) 179.9
Current children cumulated vsize (Kb) 5960

[startup+190.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 887 0 0 0 18985 5 0 0 25 0 1 0 1841303254 4026368 874 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 983 874 145 145 0 838 0
[pid=8595] vsize: 3932
Current children cumulated CPU time (s) 189.9
Current children cumulated vsize (Kb) 6056

[startup+200.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 895 0 0 0 19985 5 0 0 25 0 1 0 1841303254 4059136 882 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 991 882 145 145 0 846 0
[pid=8595] vsize: 3964
Current children cumulated CPU time (s) 199.9
Current children cumulated vsize (Kb) 6088

[startup+210.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 901 0 0 0 20985 5 0 0 25 0 1 0 1841303254 4075520 888 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 995 888 145 145 0 850 0
[pid=8595] vsize: 3980
Current children cumulated CPU time (s) 209.9
Current children cumulated vsize (Kb) 6104

[startup+220.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 905 0 0 0 21986 5 0 0 25 0 1 0 1841303254 4091904 892 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 999 892 145 145 0 854 0
[pid=8595] vsize: 3996
Current children cumulated CPU time (s) 219.91
Current children cumulated vsize (Kb) 6120

[startup+230.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 909 0 0 0 22986 5 0 0 25 0 1 0 1841303254 4108288 896 4294967295 134512640 135094434 3221224432 3221223088 134558174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1003 896 145 145 0 858 0
[pid=8595] vsize: 4012
Current children cumulated CPU time (s) 229.91
Current children cumulated vsize (Kb) 6136

[startup+240.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 913 0 0 0 23986 5 0 0 25 0 1 0 1841303254 4124672 900 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1007 900 145 145 0 862 0
[pid=8595] vsize: 4028
Current children cumulated CPU time (s) 239.91
Current children cumulated vsize (Kb) 6152

[startup+250.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 931 0 0 0 24986 6 0 0 25 0 1 0 1841303254 4218880 918 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1030 918 145 145 0 885 0
[pid=8595] vsize: 4120
Current children cumulated CPU time (s) 249.92
Current children cumulated vsize (Kb) 6244

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 945 0 0 0 25986 6 0 0 25 0 1 0 1841303254 4284416 932 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1046 932 145 145 0 901 0
[pid=8595] vsize: 4184
Current children cumulated CPU time (s) 259.92
Current children cumulated vsize (Kb) 6308

[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 946 0 0 0 26986 6 0 0 25 0 1 0 1841303254 4284416 933 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1046 933 145 145 0 901 0
[pid=8595] vsize: 4184
Current children cumulated CPU time (s) 269.92
Current children cumulated vsize (Kb) 6308

[startup+280.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 962 0 0 0 27986 6 0 0 25 0 1 0 1841303254 4358144 949 4294967295 134512640 135094434 3221224432 3221223096 134556595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1064 949 145 145 0 919 0
[pid=8595] vsize: 4256
Current children cumulated CPU time (s) 279.92
Current children cumulated vsize (Kb) 6380

[startup+290.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 970 0 0 0 28986 6 0 0 25 0 1 0 1841303254 4399104 957 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1074 957 145 145 0 929 0
[pid=8595] vsize: 4296
Current children cumulated CPU time (s) 289.92
Current children cumulated vsize (Kb) 6420

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 992 0 0 0 29986 6 0 0 25 0 1 0 1841303254 4509696 979 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1101 979 145 145 0 956 0
[pid=8595] vsize: 4404
Current children cumulated CPU time (s) 299.92
Current children cumulated vsize (Kb) 6528

[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1001 0 0 0 30986 7 0 0 25 0 1 0 1841303254 4542464 988 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1109 988 145 145 0 964 0
[pid=8595] vsize: 4436
Current children cumulated CPU time (s) 309.93
Current children cumulated vsize (Kb) 6560

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1015 0 0 0 31986 7 0 0 25 0 1 0 1841303254 4599808 1002 4294967295 134512640 135094434 3221224432 3221223072 134562070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1123 1002 145 145 0 978 0
[pid=8595] vsize: 4492
Current children cumulated CPU time (s) 319.93
Current children cumulated vsize (Kb) 6616

[startup+330.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1027 0 0 0 32987 7 0 0 25 0 1 0 1841303254 4648960 1014 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1135 1014 145 145 0 990 0
[pid=8595] vsize: 4540
Current children cumulated CPU time (s) 329.94
Current children cumulated vsize (Kb) 6664

[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1052 0 0 0 33986 7 0 0 25 0 1 0 1841303254 4755456 1039 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1161 1039 145 145 0 1016 0
[pid=8595] vsize: 4644
Current children cumulated CPU time (s) 339.93
Current children cumulated vsize (Kb) 6768

[startup+350.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1065 0 0 0 34987 7 0 0 25 0 1 0 1841303254 4804608 1052 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1173 1052 145 145 0 1028 0
[pid=8595] vsize: 4692
Current children cumulated CPU time (s) 349.94
Current children cumulated vsize (Kb) 6816

[startup+360.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1065 0 0 0 35987 7 0 0 25 0 1 0 1841303254 4804608 1052 4294967295 134512640 135094434 3221224432 3221223104 134555826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1173 1052 145 145 0 1028 0
[pid=8595] vsize: 4692
Current children cumulated CPU time (s) 359.94
Current children cumulated vsize (Kb) 6816

[startup+370.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1071 0 0 0 36987 7 0 0 25 0 1 0 1841303254 4820992 1058 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1177 1058 145 145 0 1032 0
[pid=8595] vsize: 4708
Current children cumulated CPU time (s) 369.94
Current children cumulated vsize (Kb) 6832

[startup+380.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1089 0 0 0 37986 8 0 0 25 0 1 0 1841303254 4898816 1076 4294967295 134512640 135094434 3221224432 3221223008 134562748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1196 1076 145 145 0 1051 0
[pid=8595] vsize: 4784
Current children cumulated CPU time (s) 379.94
Current children cumulated vsize (Kb) 6908

[startup+390.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1094 0 0 0 38986 8 0 0 25 0 1 0 1841303254 4919296 1081 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1201 1081 145 145 0 1056 0
[pid=8595] vsize: 4804
Current children cumulated CPU time (s) 389.94
Current children cumulated vsize (Kb) 6928

[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1104 0 0 0 39986 8 0 0 25 0 1 0 1841303254 4960256 1091 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1211 1091 145 145 0 1066 0
[pid=8595] vsize: 4844
Current children cumulated CPU time (s) 399.94
Current children cumulated vsize (Kb) 6968

[startup+410.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1117 0 0 0 40986 8 0 0 25 0 1 0 1841303254 5021696 1104 4294967295 134512640 135094434 3221224432 3221223076 134562166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1226 1104 145 145 0 1081 0
[pid=8595] vsize: 4904
Current children cumulated CPU time (s) 409.94
Current children cumulated vsize (Kb) 7028

[startup+420.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1122 0 0 0 41987 8 0 0 25 0 1 0 1841303254 5038080 1109 4294967295 134512640 135094434 3221224432 3221223104 134555566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1230 1109 145 145 0 1085 0
[pid=8595] vsize: 4920
Current children cumulated CPU time (s) 419.95
Current children cumulated vsize (Kb) 7044

[startup+430.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 8595
Raw data (/proc/8591/stat): 8591 (minisat+_script) S 8590 8591 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841303248 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/8591/statm): 531 226 485 147 0 384 0
[pid=8591] vsize: 2124
Raw data (/proc/8595/stat): 8595 (minisat+_64-bit) R 8591 8591 5929 0 -1 0 1125 0 0 0 42987 8 0 0 25 0 1 0 1841303254 5038080 1112 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/8595/statm): 1230 1112 145 145 0 1085 0
[pid=8595] vsize: 4920
Current children cumulated CPU time (s) 429.95
Current children cumulated vsize (Kb) 7044
One traced child (pid=8595) exited with status: 20
One traced child (pid=8591) exited with status: 20
All traced children have exited ! Game is over.

Child status: 20
Real time (s): 437.467
CPU time (s): 437.402
CPU user time (s): 437.292
CPU system time (s): 0.110983
CPU usage (%): 99.9853
Max. virtual memory (cumulated for all children) (Kb): 7044

Verifier Data

ERROR: no interpretation found !