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_15_pb.cnf.cr.opb
MD5SUMba9cd165dfff9daff67f98334a7b589e
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 16
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.011997
Number of variables300
Total number of constraints50
Number of constraints which are clauses30
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 constraint15

Trace number 770

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        939468 kB
Buffers:         34492 kB
Cached:          31928 kB
SwapCached:        832 kB
Active:          54472 kB
Inactive:        14644 kB
HighTotal:      131008 kB
HighFree:        95368 kB
LowTotal:       903652 kB
LowFree:        844100 kB
SwapTotal:     2097892 kB
SwapFree:      2096604 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            20396 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 12:32:06 (client local time) WITH STATUS 20 IN 495.049 SECONDS
stats: 2346 7 495.049 20

Solver Data

c Parsing PB file...
c Converting 50 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   27
c ---[  16]---> BDD-cost:   27
c ---[  15]---> BDD-cost:   27
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   27
c ---[  10]---> BDD-cost:   27
c ---[   9]---> BDD-cost:   27
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   27
c ---[   4]---> BDD-cost:   27
c ---[   3]---> BDD-cost:   27
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1350     3740 |     450       0        0     nan |  0.000 % |
c |       102 |    1350     3740 |     495     102     2925    28.7 |  2.381 % |
c |       253 |    1350     3740 |     544     253    10189    40.3 |  2.381 % |
c |       479 |    1350     3740 |     598     479    19178    40.0 |  2.381 % |
c |       818 |    1350     3740 |     658     428    17229    40.3 |  2.381 % |
c |      1324 |    1350     3740 |     724     516    21892    42.4 |  2.381 % |
c |      2083 |    1350     3740 |     797     823    37368    45.4 |  2.381 % |
c |      3222 |    1350     3740 |     876     604    27269    45.1 |  2.381 % |
c |      4930 |    1350     3740 |     964     784    35160    44.8 |  2.381 % |
c |      7495 |    1350     3740 |    1061     614    24724    40.3 |  2.381 % |
c |     11341 |    1350     3740 |    1167     776    29718    38.3 |  2.381 % |
c |     17108 |    1350     3740 |    1283    1208    43585    36.1 |  2.381 % |
c |     25759 |    1350     3740 |    1412    1284    53632    41.8 |  2.381 % |
c |     38736 |    1350     3740 |    1553     908    38284    42.2 |  2.381 % |
c |     58201 |    1350     3740 |    1708    1609    80418    50.0 |  2.381 % |
c |     87393 |    1350     3740 |    1879    1080    44530    41.2 |  2.381 % |
c |    131183 |    1350     3740 |    2067    1049    49794    47.5 |  2.381 % |
c |    196867 |    1350     3740 |    2274    2099    75813    36.1 |  2.381 % |
c |    295393 |    1350     3740 |    2501    2117    88662    41.9 |  2.381 % |
c |    443183 |    1350     3740 |    2752    2411   116404    48.3 |  2.381 % |
c |    664872 |    1350     3740 |    3027    2070    81156    39.2 |  2.381 % |
c |    997399 |    1350     3740 |    3330    2348   103803    44.2 |  2.381 % |
c |   1496187 |    1291     3582 |    3663    3443   105928    30.8 |  6.195 % |
c ==============================================================================
c UNSATISFIABLE
s UNSATISFIABLE
c _______________________________________________________________________________
c 
c restarts              : 23
c conflicts             : 1503240        (3037 /sec)
c decisions             : 1693200        (3421 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 494.904 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/5400/stat): 5400 (minisat+_script) R 5399 5400 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841228521 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/5400/statm): 174 3 169 147 0 27 0
[pid=5400] 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=5401
New process pid=5402
New process pid=5403
execve syscall for /bin/sed executable
One traced child (pid=5402) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=5403) exited with status: 0
One traced child (pid=5401) exited with status: 0
New process pid=5404
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-chnl10_15_pb.cnf.cr.opb

[startup+10.0049 s]
Raw data (loadavg): 0.81 0.92 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 348 0 2 0 984 2 0 0 25 0 1 0 1841228526 1679360 337 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 410 337 145 145 0 265 0
[pid=5404] vsize: 1640
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 3764

[startup+20.0057 s]
Raw data (loadavg): 0.84 0.93 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 402 0 2 0 1982 3 0 0 25 0 1 0 1841228526 1900544 391 4294967295 134512640 135094434 3221224432 3221223104 134555849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5404/statm): 464 391 145 145 0 319 0
[pid=5404] vsize: 1856
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 3980

[startup+30.0074 s]
Raw data (loadavg): 0.87 0.93 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 453 0 2 0 2981 3 0 0 25 0 1 0 1841228526 2113536 442 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 516 442 145 145 0 371 0
[pid=5404] vsize: 2064
Current children cumulated CPU time (s) 29.85
Current children cumulated vsize (Kb) 4188

[startup+40.0081 s]
Raw data (loadavg): 0.89 0.93 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 488 0 2 0 3981 4 0 0 25 0 1 0 1841228526 2256896 477 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 551 477 145 145 0 406 0
[pid=5404] vsize: 2204
Current children cumulated CPU time (s) 39.86
Current children cumulated vsize (Kb) 4328

[startup+50.0099 s]
Raw data (loadavg): 0.90 0.93 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 517 0 2 0 4980 4 0 0 25 0 1 0 1841228526 2375680 506 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 580 506 145 145 0 435 0
[pid=5404] vsize: 2320
Current children cumulated CPU time (s) 49.85
Current children cumulated vsize (Kb) 4444

[startup+60.0106 s]
Raw data (loadavg): 0.92 0.93 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 536 0 2 0 5980 4 0 0 25 0 1 0 1841228526 2449408 525 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5404/statm): 598 525 145 145 0 453 0
[pid=5404] vsize: 2392
Current children cumulated CPU time (s) 59.85
Current children cumulated vsize (Kb) 4516

[startup+70.0113 s]
Raw data (loadavg): 0.93 0.94 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 575 0 2 0 6979 5 0 0 25 0 1 0 1841228526 2609152 564 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 637 564 145 145 0 492 0
[pid=5404] vsize: 2548
Current children cumulated CPU time (s) 69.85
Current children cumulated vsize (Kb) 4672

[startup+80.013 s]
Raw data (loadavg): 0.94 0.94 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 588 0 2 0 7979 5 0 0 25 0 1 0 1841228526 2662400 577 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 650 577 145 145 0 505 0
[pid=5404] vsize: 2600
Current children cumulated CPU time (s) 79.85
Current children cumulated vsize (Kb) 4724

[startup+90.0138 s]
Raw data (loadavg): 0.95 0.94 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 606 0 2 0 8979 5 0 0 25 0 1 0 1841228526 2736128 595 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 668 595 145 145 0 523 0
[pid=5404] vsize: 2672
Current children cumulated CPU time (s) 89.85
Current children cumulated vsize (Kb) 4796

[startup+100.015 s]
Raw data (loadavg): 0.96 0.94 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 612 0 2 0 9979 5 0 0 25 0 1 0 1841228526 2760704 601 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 674 601 145 145 0 529 0
[pid=5404] vsize: 2696
Current children cumulated CPU time (s) 99.85
Current children cumulated vsize (Kb) 4820

[startup+110.015 s]
Raw data (loadavg): 0.96 0.94 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 620 0 2 0 10979 5 0 0 25 0 1 0 1841228526 2793472 609 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 682 609 145 145 0 537 0
[pid=5404] vsize: 2728
Current children cumulated CPU time (s) 109.85
Current children cumulated vsize (Kb) 4852

[startup+120.016 s]
Raw data (loadavg): 0.97 0.94 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 626 0 2 0 11979 6 0 0 25 0 1 0 1841228526 2818048 615 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 688 615 145 145 0 543 0
[pid=5404] vsize: 2752
Current children cumulated CPU time (s) 119.86
Current children cumulated vsize (Kb) 4876

[startup+130.017 s]
Raw data (loadavg): 0.97 0.94 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 649 0 2 0 12979 6 0 0 25 0 1 0 1841228526 2912256 638 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 711 638 145 145 0 566 0
[pid=5404] vsize: 2844
Current children cumulated CPU time (s) 129.86
Current children cumulated vsize (Kb) 4968

[startup+140.017 s]
Raw data (loadavg): 0.98 0.95 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 671 0 2 0 13979 6 0 0 25 0 1 0 1841228526 3002368 660 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 733 660 145 145 0 588 0
[pid=5404] vsize: 2932
Current children cumulated CPU time (s) 139.86
Current children cumulated vsize (Kb) 5056

[startup+150.019 s]
Raw data (loadavg): 0.98 0.95 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 675 0 2 0 14979 6 0 0 25 0 1 0 1841228526 3018752 664 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 737 664 145 145 0 592 0
[pid=5404] vsize: 2948
Current children cumulated CPU time (s) 149.86
Current children cumulated vsize (Kb) 5072

[startup+160.02 s]
Raw data (loadavg): 0.98 0.95 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 686 0 2 0 15979 6 0 0 25 0 1 0 1841228526 3063808 675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 748 675 145 145 0 603 0
[pid=5404] vsize: 2992
Current children cumulated CPU time (s) 159.86
Current children cumulated vsize (Kb) 5116

[startup+170.021 s]
Raw data (loadavg): 0.98 0.95 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 700 0 2 0 16979 6 0 0 25 0 1 0 1841228526 3121152 689 4294967295 134512640 135094434 3221224432 3221223152 134538526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 762 689 145 145 0 617 0
[pid=5404] vsize: 3048
Current children cumulated CPU time (s) 169.86
Current children cumulated vsize (Kb) 5172

[startup+180.021 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 708 0 2 0 17979 7 0 0 25 0 1 0 1841228526 3162112 697 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 772 697 145 145 0 627 0
[pid=5404] vsize: 3088
Current children cumulated CPU time (s) 179.87
Current children cumulated vsize (Kb) 5212

[startup+190.022 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 720 0 2 0 18979 7 0 0 25 0 1 0 1841228526 3211264 709 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 784 709 145 145 0 639 0
[pid=5404] vsize: 3136
Current children cumulated CPU time (s) 189.87
Current children cumulated vsize (Kb) 5260

[startup+200.024 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 724 0 2 0 19979 7 0 0 25 0 1 0 1841228526 3227648 713 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 788 713 145 145 0 643 0
[pid=5404] vsize: 3152
Current children cumulated CPU time (s) 199.87
Current children cumulated vsize (Kb) 5276

[startup+210.024 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 733 0 2 0 20979 7 0 0 25 0 1 0 1841228526 3264512 722 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 797 722 145 145 0 652 0
[pid=5404] vsize: 3188
Current children cumulated CPU time (s) 209.87
Current children cumulated vsize (Kb) 5312

[startup+220.025 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 736 0 2 0 21979 7 0 0 25 0 1 0 1841228526 3276800 725 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 800 725 145 145 0 655 0
[pid=5404] vsize: 3200
Current children cumulated CPU time (s) 219.87
Current children cumulated vsize (Kb) 5324

[startup+230.026 s]
Raw data (loadavg): 0.99 0.95 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 744 0 2 0 22979 8 0 0 25 0 1 0 1841228526 3321856 733 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 811 733 145 145 0 666 0
[pid=5404] vsize: 3244
Current children cumulated CPU time (s) 229.88
Current children cumulated vsize (Kb) 5368

[startup+240.027 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 759 0 2 0 23979 8 0 0 25 0 1 0 1841228526 3403776 748 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 831 748 145 145 0 686 0
[pid=5404] vsize: 3324
Current children cumulated CPU time (s) 239.88
Current children cumulated vsize (Kb) 5448

[startup+250.027 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 765 0 2 0 24979 8 0 0 25 0 1 0 1841228526 3436544 754 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 839 754 145 145 0 694 0
[pid=5404] vsize: 3356
Current children cumulated CPU time (s) 249.88
Current children cumulated vsize (Kb) 5480

[startup+260.029 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 768 0 2 0 25979 8 0 0 25 0 1 0 1841228526 3452928 757 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 843 757 145 145 0 698 0
[pid=5404] vsize: 3372
Current children cumulated CPU time (s) 259.88
Current children cumulated vsize (Kb) 5496

[startup+270.03 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 777 0 2 0 26980 8 0 0 25 0 1 0 1841228526 3497984 766 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 854 766 145 145 0 709 0
[pid=5404] vsize: 3416
Current children cumulated CPU time (s) 269.89
Current children cumulated vsize (Kb) 5540

[startup+280.031 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 794 0 2 0 27980 8 0 0 25 0 1 0 1841228526 3571712 783 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 872 783 145 145 0 727 0
[pid=5404] vsize: 3488
Current children cumulated CPU time (s) 279.89
Current children cumulated vsize (Kb) 5612

[startup+290.031 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 809 0 2 0 28980 8 0 0 25 0 1 0 1841228526 3653632 798 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 892 798 145 145 0 747 0
[pid=5404] vsize: 3568
Current children cumulated CPU time (s) 289.89
Current children cumulated vsize (Kb) 5692

[startup+300.032 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 830 0 2 0 29980 8 0 0 25 0 1 0 1841228526 3768320 819 4294967295 134512640 135094434 3221224432 3221223104 134555940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 920 819 145 145 0 775 0
[pid=5404] vsize: 3680
Current children cumulated CPU time (s) 299.89
Current children cumulated vsize (Kb) 5804

[startup+310.033 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 830 0 2 0 30980 8 0 0 25 0 1 0 1841228526 3768320 819 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 920 819 145 145 0 775 0
[pid=5404] vsize: 3680
Current children cumulated CPU time (s) 309.89
Current children cumulated vsize (Kb) 5804

[startup+320.034 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 839 0 2 0 31980 8 0 0 25 0 1 0 1841228526 3817472 828 4294967295 134512640 135094434 3221224432 3221223072 134556681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 932 828 145 145 0 787 0
[pid=5404] vsize: 3728
Current children cumulated CPU time (s) 319.89
Current children cumulated vsize (Kb) 5852

[startup+330.035 s]
Raw data (loadavg): 0.99 0.96 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 848 0 2 0 32980 8 0 0 25 0 1 0 1841228526 3866624 837 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 944 837 145 145 0 799 0
[pid=5404] vsize: 3776
Current children cumulated CPU time (s) 329.89
Current children cumulated vsize (Kb) 5900

[startup+340.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 869 0 2 0 33980 9 0 0 25 0 1 0 1841228526 3981312 858 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 972 858 145 145 0 827 0
[pid=5404] vsize: 3888
Current children cumulated CPU time (s) 339.9
Current children cumulated vsize (Kb) 6012

[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 878 0 2 0 34980 9 0 0 25 0 1 0 1841228526 4030464 867 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 984 867 145 145 0 839 0
[pid=5404] vsize: 3936
Current children cumulated CPU time (s) 349.9
Current children cumulated vsize (Kb) 6060

[startup+360.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 884 0 2 0 35980 9 0 0 25 0 1 0 1841228526 4063232 873 4294967295 134512640 135094434 3221224432 3221223104 134556543 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 992 873 145 145 0 847 0
[pid=5404] vsize: 3968
Current children cumulated CPU time (s) 359.9
Current children cumulated vsize (Kb) 6092

[startup+370.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 904 0 2 0 36980 9 0 0 25 0 1 0 1841228526 4141056 893 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1011 893 145 145 0 866 0
[pid=5404] vsize: 4044
Current children cumulated CPU time (s) 369.9
Current children cumulated vsize (Kb) 6168

[startup+380.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 919 0 2 0 37980 9 0 0 25 0 1 0 1841228526 4206592 908 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1027 908 145 145 0 882 0
[pid=5404] vsize: 4108
Current children cumulated CPU time (s) 379.9
Current children cumulated vsize (Kb) 6232

[startup+390.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 919 0 2 0 38980 9 0 0 25 0 1 0 1841228526 4206592 908 4294967295 134512640 135094434 3221224432 3221223088 134558240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1027 908 145 145 0 882 0
[pid=5404] vsize: 4108
Current children cumulated CPU time (s) 389.9
Current children cumulated vsize (Kb) 6232

[startup+400.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 922 0 2 0 39981 9 0 0 25 0 1 0 1841228526 4222976 911 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1031 911 145 145 0 886 0
[pid=5404] vsize: 4124
Current children cumulated CPU time (s) 399.91
Current children cumulated vsize (Kb) 6248

[startup+410.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 930 0 2 0 40981 10 0 0 25 0 1 0 1841228526 4255744 919 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1039 919 145 145 0 894 0
[pid=5404] vsize: 4156
Current children cumulated CPU time (s) 409.92
Current children cumulated vsize (Kb) 6280

[startup+420.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 945 0 2 0 41981 10 0 0 25 0 1 0 1841228526 4321280 934 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1055 934 145 145 0 910 0
[pid=5404] vsize: 4220
Current children cumulated CPU time (s) 419.92
Current children cumulated vsize (Kb) 6344

[startup+430.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 956 0 2 0 42981 10 0 0 25 0 1 0 1841228526 4370432 945 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1067 945 145 145 0 922 0
[pid=5404] vsize: 4268
Current children cumulated CPU time (s) 429.92
Current children cumulated vsize (Kb) 6392

[startup+440.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 962 0 2 0 43981 10 0 0 25 0 1 0 1841228526 4403200 951 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1075 951 145 145 0 930 0
[pid=5404] vsize: 4300
Current children cumulated CPU time (s) 439.92
Current children cumulated vsize (Kb) 6424

[startup+450.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 975 0 2 0 44981 10 0 0 25 0 1 0 1841228526 4468736 964 4294967295 134512640 135094434 3221224432 3221223104 134556462 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1091 964 145 145 0 946 0
[pid=5404] vsize: 4364
Current children cumulated CPU time (s) 449.92
Current children cumulated vsize (Kb) 6488

[startup+460.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 999 0 2 0 45981 10 0 0 25 0 1 0 1841228526 4567040 988 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1115 988 145 145 0 970 0
[pid=5404] vsize: 4460
Current children cumulated CPU time (s) 459.92
Current children cumulated vsize (Kb) 6584

[startup+470.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 1003 0 2 0 46981 10 0 0 25 0 1 0 1841228526 4583424 992 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1119 992 145 145 0 974 0
[pid=5404] vsize: 4476
Current children cumulated CPU time (s) 469.92
Current children cumulated vsize (Kb) 6600

[startup+480.048 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 1006 0 2 0 47982 10 0 0 25 0 1 0 1841228526 4599808 995 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1123 995 145 145 0 978 0
[pid=5404] vsize: 4492
Current children cumulated CPU time (s) 479.93
Current children cumulated vsize (Kb) 6616

[startup+490.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/57 5404
Raw data (/proc/5400/stat): 5400 (minisat+_script) S 5399 5400 2660 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1841228521 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5400/statm): 531 226 485 147 0 384 0
[pid=5400] vsize: 2124
Raw data (/proc/5404/stat): 5404 (minisat+_64-bit) R 5400 5400 2660 0 -1 0 1006 0 2 0 48982 10 0 0 25 0 1 0 1841228526 4599808 995 4294967295 134512640 135094434 3221224432 3221223024 134556908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5404/statm): 1123 995 145 145 0 978 0
[pid=5404] vsize: 4492
Current children cumulated CPU time (s) 489.93
Current children cumulated vsize (Kb) 6616
One traced child (pid=5404) exited with status: 20
One traced child (pid=5400) exited with status: 20
All traced children have exited ! Game is over.

Child status: 20
Real time (s): 495.142
CPU time (s): 495.049
CPU user time (s): 494.913
CPU system time (s): 0.135979
CPU usage (%): 99.9813
Max. virtual memory (cumulated for all children) (Kb): 6616

Verifier Data

ERROR: no interpretation found !