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

Namemps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-blp-ic98.opb
MD5SUM4c475edac91e4650fa2d3e487e86c291
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 81920000000
Number of bits of the biggest number in a constraint 37
Biggest sum of numbers in a constraint 66700085225335
Number of bits of the biggest sum of numbers46
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables14923
Total number of constraints14313
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)14177
Number of constraints which are nor clauses,nor cardinality constraints136
Minimum length of a constraint1
Maximum length of a constraint13571

Trace number 6300

Launcher Data

LAUNCH ON wulflinc29 THE 2005-09-20 05:31:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3482 boxname=wulflinc29 idbench=1138 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4c475edac91e4650fa2d3e487e86c291  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-blp-ic98.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-blp-ic98.opb
IDLAUNCH: 3482
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        823896 kB
Buffers:         38640 kB
Cached:         140112 kB
SwapCached:        768 kB
Active:          50364 kB
Inactive:       130920 kB
HighTotal:      131008 kB
HighFree:        22484 kB
LowTotal:       903652 kB
LowFree:        801412 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            23788 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:39:43 (client local time) WITH STATUS 0 IN 473.535 SECONDS
stats: 3482 7 473.535 0

Solver Data

c Parsing PB file...
c Converting 853 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################################################################################
c   -- Clauses(.)/Splits(s): sssss
c ---[ 857]---> BDD-cost:    9
c ---[ 856]---> BDD-cost:    9
c ---[ 855]---> BDD-cost:   10
c ---[ 854]---> BDD-cost:   10
c ---[ 853]---> BDD-cost:   10
c ---[ 850]---> BDD-cost:   10
c ---[ 849]---> BDD-cost:   10
c ---[ 848]---> BDD-cost:   10
c ---[ 847]---> BDD-cost:   10
c ---[ 846]---> BDD-cost:   10
c ---[ 845]---> BDD-cost:    9
c ---[ 844]---> BDD-cost:   10
c ---[ 842]---> BDD-cost:   10
c ---[ 841]---> BDD-cost:   10
c ---[ 840]---> BDD-cost:   10
c ---[ 839]---> BDD-cost:   10
c ---[ 838]---> BDD-cost:   10
c ---[ 837]---> BDD-cost:   10
c ---[ 836]---> BDD-cost:   10
c ---[ 835]---> BDD-cost:    9
c ---[ 834]---> BDD-cost:   10
c ---[ 833]---> BDD-cost:   10
c ---[ 832]---> BDD-cost:   10
c ---[ 831]---> BDD-cost:    9
c ---[ 830]---> BDD-cost:    9
c ---[ 829]---> BDD-cost:   10
c ---[ 828]---> BDD-cost:   10
c ---[ 827]---> BDD-cost:   10
c ---[ 826]---> BDD-cost:   10
c ---[ 825]---> BDD-cost:    9
c ---[ 824]---> BDD-cost:   10
c ---[ 822]---> BDD-cost:    9
c ---[ 821]---> BDD-cost:   10
c ---[ 820]---> BDD-cost:   10
c ---[ 819]---> BDD-cost:   10
c ---[ 818]---> BDD-cost:   10
c ---[ 817]---> BDD-cost:   10
c ---[ 815]---> BDD-cost:   10
c ---[ 814]---> BDD-cost:   10
c ---[ 813]---> BDD-cost:   10
c ---[ 812]---> BDD-cost:    9
c ---[ 810]---> Adder-cost: 2530   maxlim: 234240   bits: 18/18
c ---[ 808]---> Adder-cost: 954   maxlim: 120832   bits: 17/17
c ---[ 806]---> Adder-cost: 6532   maxlim: 588800   bits: 20/20
c ---[ 804]---> Adder-cost: 1924   maxlim: 183808   bits: 18/18
c ---[ 802]---> Adder-cost: 428   maxlim: 42496   bits: 16/16
c ---[ 800]---> Adder-cost: 10296   maxlim: 957312   bits: 20/20
c ---[ 798]---> Adder-cost: 4976   maxlim: 633216   bits: 20/20
c ---[ 796]---> Adder-cost: 2746   maxlim: 422912   bits: 19/19
c ---[ 794]---> Adder-cost: 3164   maxlim: 333824   bits: 19/19
c ---[ 792]---> Adder-cost: 2142   maxlim: 224256   bits: 18/18
c ---[ 790]---> Adder-cost: 1618   maxlim: 166912   bits: 18/18
c ---[ 788]---> Adder-cost: 3844   maxlim: 508672   bits: 19/19
c ---[ 786]---> Adder-cost: 2790   maxlim: 318976   bits: 19/19
c ---[ 784]---> Adder-cost: 962   maxlim: 106752   bits: 17/17
c ---[ 782]---> Adder-cost: 1114   maxlim: 116352   bits: 17/17
c ---[ 780]---> Adder-cost: 1356   maxlim: 162304   bits: 18/18
c ---[ 778]---> Adder-cost: 2260   maxlim: 247808   bits: 18/18
c ---[ 776]---> Adder-cost: 2598   maxlim: 265472   bits: 19/19
c ---[ 774]---> Adder-cost: 1746   maxlim: 192512   bits: 18/18
c ---[ 772]---> Adder-cost: 2930   maxlim: 305152   bits: 19/19
c ---[ 770]---> Adder-cost: 1820   maxlim: 199296   bits: 18/18
c ---[ 768]---> Adder-cost: 4014   maxlim: 472960   bits: 19/19
c ---[ 766]---> Adder-cost: 6654   maxlim: 854656   bits: 20/20
c ---[ 764]---> Adder-cost: 2044   maxlim: 217728   bits: 18/18
c ---[ 762]---> Adder-cost: 1242   maxlim: 144000   bits: 18/18
c ---[ 760]---> Adder-cost: 268   maxlim: 42496   bits: 16/16
c ---[ 758]---> Adder-cost: 1576   maxlim: 318976   bits: 19/19
c ---[ 756]---> Adder-cost: 2740   maxlim: 299392   bits: 19/19
c ---[ 754]---> Adder-cost: 2394   maxlim: 288384   bits: 19/19
c ---[ 752]---> Adder-cost: 5924   maxlim: 678784   bits: 20/20
c ---[ 750]---> Adder-cost: 4334   maxlim: 547200   bits: 20/20
c ---[ 748]---> Adder-cost: 942   maxlim: 166784   bits: 18/18
c ---[ 746]---> Adder-cost: 4304   maxlim: 528384   bits: 20/20
c ---[ 744]---> Adder-cost: 784   maxlim: 89472   bits: 17/17
c ---[ 742]---> Adder-cost: 4446   maxlim: 610944   bits: 20/20
c ---[ 740]---> Adder-cost: 3354   maxlim: 494592   bits: 19/19
c ---[ 738]---> Adder-cost: 802   maxlim: 106368   bits: 17/17
c ---[ 736]---> Adder-cost: 1286   maxlim: 161408   bits: 18/18
c ---[ 734]---> Adder-cost: 1962   maxlim: 247040   bits: 18/18
c ---[ 732]---> Adder-cost: 1334   maxlim: 163200   bits:

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/5778/stat): 5778 (minisat+_script) R 5777 5778 19818 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1856027218 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/5778/statm): 174 3 169 147 0 27 0
[pid=5778] 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=5779
New process pid=5780
New process pid=5781
execve syscall for /bin/sed executable
One traced child (pid=5780) 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=5781) exited with status: 0
One traced child (pid=5779) exited with status: 0
New process pid=5782
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-blp-ic98.opb

[startup+10.0038 s]
Raw data (loadavg): 0.93 0.96 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 347 0 0 0 986 3 0 0 25 0 1 0 1856027223 1814528 333 4294967295 134512640 135094434 3221224432 3221223300 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 443 333 145 145 0 298 0
[pid=5782] vsize: 1772
Current children cumulated CPU time (s) 9.9
Current children cumulated vsize (Kb) 3896

[startup+20.0046 s]
Raw data (loadavg): 0.94 0.96 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 482 0 0 0 1984 5 0 0 25 0 1 0 1856027223 2682880 465 4294967295 134512640 135094434 3221224432 3221223300 134796010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 655 465 145 145 0 510 0
[pid=5782] vsize: 2620
Current children cumulated CPU time (s) 19.9
Current children cumulated vsize (Kb) 4744

[startup+30.0054 s]
Raw data (loadavg): 0.95 0.96 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 548 0 0 0 2983 6 0 0 25 0 1 0 1856027223 2854912 531 4294967295 134512640 135094434 3221224432 3221223300 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 697 531 145 145 0 552 0
[pid=5782] vsize: 2788
Current children cumulated CPU time (s) 29.9
Current children cumulated vsize (Kb) 4912

[startup+40.0062 s]
Raw data (loadavg): 0.96 0.96 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 575 0 0 0 3982 6 0 0 25 0 1 0 1856027223 2871296 558 4294967295 134512640 135094434 3221224432 3221223300 134796009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 701 558 145 145 0 556 0
[pid=5782] vsize: 2804
Current children cumulated CPU time (s) 39.89
Current children cumulated vsize (Kb) 4928

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.96 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 617 0 0 0 4981 8 0 0 25 0 1 0 1856027223 2961408 600 4294967295 134512640 135094434 3221224432 3221223300 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 723 600 145 145 0 578 0
[pid=5782] vsize: 2892
Current children cumulated CPU time (s) 49.9
Current children cumulated vsize (Kb) 5016

[startup+60.0087 s]
Raw data (loadavg): 0.97 0.96 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 812 0 0 0 5978 9 0 0 25 0 1 0 1856027223 3702784 721 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 904 721 145 145 0 759 0
[pid=5782] vsize: 3616
Current children cumulated CPU time (s) 59.88
Current children cumulated vsize (Kb) 5740

[startup+70.0095 s]
Raw data (loadavg): 0.97 0.96 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 821 0 0 0 6976 10 0 0 25 0 1 0 1856027223 3756032 730 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 917 730 145 145 0 772 0
[pid=5782] vsize: 3668
Current children cumulated CPU time (s) 69.87
Current children cumulated vsize (Kb) 5792

[startup+80.0103 s]
Raw data (loadavg): 0.98 0.96 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1172 0 0 0 7973 12 0 0 25 0 1 0 1856027223 4685824 801 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 1144 801 145 145 0 999 0
[pid=5782] vsize: 4576
Current children cumulated CPU time (s) 79.86
Current children cumulated vsize (Kb) 6700

[startup+90.0111 s]
Raw data (loadavg): 0.98 0.96 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1272 0 0 0 8969 14 0 0 25 0 1 0 1856027223 5169152 854 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 1262 854 145 145 0 1117 0
[pid=5782] vsize: 5048
Current children cumulated CPU time (s) 89.84
Current children cumulated vsize (Kb) 7172

[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1399 0 0 0 9967 15 0 0 25 0 1 0 1856027223 5693440 911 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 1390 911 145 145 0 1245 0
[pid=5782] vsize: 5560
Current children cumulated CPU time (s) 99.83
Current children cumulated vsize (Kb) 7684

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1474 0 0 0 10965 16 0 0 25 0 1 0 1856027223 6021120 986 4294967295 134512640 135094434 3221224432 3221223316 134796010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 1470 986 145 145 0 1325 0
[pid=5782] vsize: 5880
Current children cumulated CPU time (s) 109.82
Current children cumulated vsize (Kb) 8004

[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1587 0 0 0 11962 17 0 0 25 0 1 0 1856027223 6520832 1099 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 1592 1099 145 145 0 1447 0
[pid=5782] vsize: 6368
Current children cumulated CPU time (s) 119.8
Current children cumulated vsize (Kb) 8492

[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1813 0 0 0 12959 19 0 0 25 0 1 0 1856027223 7249920 1153 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 1770 1153 145 145 0 1625 0
[pid=5782] vsize: 7080
Current children cumulated CPU time (s) 129.79
Current children cumulated vsize (Kb) 9204

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1918 0 0 0 13956 21 0 0 25 0 1 0 1856027223 7761920 1258 4294967295 134512640 135094434 3221224432 3221223324 134796030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 1895 1258 145 145 0 1750 0
[pid=5782] vsize: 7580
Current children cumulated CPU time (s) 139.78
Current children cumulated vsize (Kb) 9704

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1956 0 0 0 14955 22 0 0 25 0 1 0 1856027223 7917568 1296 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 1933 1296 145 145 0 1788 0
[pid=5782] vsize: 7732
Current children cumulated CPU time (s) 149.78
Current children cumulated vsize (Kb) 9856

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2178 0 0 0 15951 24 0 0 25 0 1 0 1856027223 8638464 1352 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 2109 1352 145 145 0 1964 0
[pid=5782] vsize: 8436
Current children cumulated CPU time (s) 159.76
Current children cumulated vsize (Kb) 10560

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2391 0 0 0 16948 26 0 0 25 0 1 0 1856027223 9367552 1421 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 2287 1421 145 145 0 2142 0
[pid=5782] vsize: 9148
Current children cumulated CPU time (s) 169.75
Current children cumulated vsize (Kb) 11272

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2480 0 0 0 17945 27 0 0 25 0 1 0 1856027223 9707520 1442 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 2370 1442 145 145 0 2225 0
[pid=5782] vsize: 9480
Current children cumulated CPU time (s) 179.73
Current children cumulated vsize (Kb) 11604

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2515 0 0 0 18944 28 0 0 25 0 1 0 1856027223 9924608 1477 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 2423 1477 145 145 0 2278 0
[pid=5782] vsize: 9692
Current children cumulated CPU time (s) 189.73
Current children cumulated vsize (Kb) 11816

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2758 0 0 0 19941 30 0 0 25 0 1 0 1856027223 10731520 1537 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 2620 1537 145 145 0 2475 0
[pid=5782] vsize: 10480
Current children cumulated CPU time (s) 199.72
Current children cumulated vsize (Kb) 12604

[startup+210.02 s]
Raw data (loadavg): 1.07 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2947 0 0 0 20938 32 0 0 25 0 1 0 1856027223 11333632 1585 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 2767 1585 145 145 0 2622 0
[pid=5782] vsize: 11068
Current children cumulated CPU time (s) 209.71
Current children cumulated vsize (Kb) 13192

[startup+220.02 s]
Raw data (loadavg): 1.06 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2952 0 0 0 21934 34 0 0 25 0 1 0 1856027223 11333632 1590 4294967295 134512640 135094434 3221224432 3221223344 134587864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 2767 1590 145 145 0 2622 0
[pid=5782] vsize: 11068
Current children cumulated CPU time (s) 219.69
Current children cumulated vsize (Kb) 13192

[startup+230.021 s]
Raw data (loadavg): 1.05 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2980 0 0 0 22933 35 0 0 25 0 1 0 1856027223 11497472 1618 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 2807 1618 145 145 0 2662 0
[pid=5782] vsize: 11228
Current children cumulated CPU time (s) 229.69
Current children cumulated vsize (Kb) 13352

[startup+240.022 s]
Raw data (loadavg): 1.04 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 3632 0 0 0 23927 38 0 0 25 0 1 0 1856027223 13299712 1759 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 3247 1759 145 145 0 3102 0
[pid=5782] vsize: 12988
Current children cumulated CPU time (s) 239.66
Current children cumulated vsize (Kb) 15112

[startup+250.024 s]
Raw data (loadavg): 1.03 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 3632 0 0 0 24925 39 0 0 25 0 1 0 1856027223 13299712 1759 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 3247 1759 145 145 0 3102 0
[pid=5782] vsize: 12988
Current children cumulated CPU time (s) 249.65
Current children cumulated vsize (Kb) 15112

[startup+260.024 s]
Raw data (loadavg): 1.03 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 3944 0 0 0 25922 41 0 0 25 0 1 0 1856027223 14217216 1829 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 3471 1829 145 145 0 3326 0
[pid=5782] vsize: 13884
Current children cumulated CPU time (s) 259.64
Current children cumulated vsize (Kb) 16008

[startup+270.025 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4064 0 0 0 26918 44 0 0 25 0 1 0 1856027223 14794752 1892 4294967295 134512640 135094434 3221224432 3221223320 134795993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 3612 1892 145 145 0 3467 0
[pid=5782] vsize: 14448
Current children cumulated CPU time (s) 269.63
Current children cumulated vsize (Kb) 16572

[startup+280.026 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4184 0 0 0 27916 45 0 0 25 0 1 0 1856027223 15233024 1942 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 3719 1942 145 145 0 3574 0
[pid=5782] vsize: 14876
Current children cumulated CPU time (s) 279.62
Current children cumulated vsize (Kb) 17000

[startup+290.027 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4241 0 0 0 28915 46 0 0 25 0 1 0 1856027223 15564800 1999 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 3800 1999 145 145 0 3655 0
[pid=5782] vsize: 15200
Current children cumulated CPU time (s) 289.62
Current children cumulated vsize (Kb) 17324

[startup+300.029 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4347 0 0 0 29913 47 0 0 25 0 1 0 1856027223 16068608 2105 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 3923 2105 145 145 0 3778 0
[pid=5782] vsize: 15692
Current children cumulated CPU time (s) 299.61
Current children cumulated vsize (Kb) 17816

[startup+310.029 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4573 0 0 0 30910 50 0 0 25 0 1 0 1856027223 16793600 2160 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 4100 2160 145 145 0 3955 0
[pid=5782] vsize: 16400
Current children cumulated CPU time (s) 309.61
Current children cumulated vsize (Kb) 18524

[startup+320.03 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4684 0 0 0 31908 51 0 0 25 0 1 0 1856027223 17272832 2271 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5782/statm): 4217 2271 145 145 0 4072 0
[pid=5782] vsize: 16868
Current children cumulated CPU time (s) 319.6
Current children cumulated vsize (Kb) 18992

[startup+330.031 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4799 0 0 0 32906 51 0 0 25 0 1 0 1856027223 17752064 2322 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5782/statm): 4334 2322 145 145 0 4189 0
[pid=5782] vsize: 17336
Current children cumulated CPU time (s) 329.58
Current children cumulated vsize (Kb) 19460

[startup+340.032 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4989 0 0 0 33903 54 0 0 25 0 1 0 1856027223 18374656 2366 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5782/statm): 4486 2366 145 145 0 4341 0
[pid=5782] vsize: 17944
Current children cumulated CPU time (s) 339.58
Current children cumulated vsize (Kb) 20068

[startup+350.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 5177 0 0 0 34900 55 0 0 25 0 1 0 1856027223 18968576 2409 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 4631 2409 145 145 0 4486 0
[pid=5782] vsize: 18524
Current children cumulated CPU time (s) 349.56
Current children cumulated vsize (Kb) 20648

[startup+360.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 5250 0 0 0 35898 56 0 0 25 0 1 0 1856027223 19292160 2482 4294967295 134512640 135094434 3221224432 3221223344 134587868 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 4710 2482 145 145 0 4565 0
[pid=5782] vsize: 18840
Current children cumulated CPU time (s) 359.55
Current children cumulated vsize (Kb) 20964

[startup+370.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 5422 0 0 0 36895 57 0 0 25 0 1 0 1856027223 19759104 2518 4294967295 134512640 135094434 3221224432 3221223344 134587868 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5782/statm): 4824 2518 145 145 0 4679 0
[pid=5782] vsize: 19296
Current children cumulated CPU time (s) 369.53
Current children cumulated vsize (Kb) 21420

[startup+380.035 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 5612 0 0 0 37892 59 0 0 25 0 1 0 1856027223 20373504 2584 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/5782/statm): 4974 2584 145 145 0 4829 0
[pid=5782] vsize: 19896
Current children cumulated CPU time (s) 379.52
Current children cumulated vsize (Kb) 22020

[startup+390.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 5735 0 0 0 38890 61 0 0 25 0 1 0 1856027223 20844544 2635 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5782/statm): 5089 2635 145 145 0 4944 0
[pid=5782] vsize: 20356
Current children cumulated CPU time (s) 389.52
Current children cumulated vsize (Kb) 22480

[startup+400.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 5804 0 0 0 39886 62 0 0 25 0 1 0 1856027223 21123072 2704 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 5157 2704 145 145 0 5012 0
[pid=5782] vsize: 20628
Current children cumulated CPU time (s) 399.49
Current children cumulated vsize (Kb) 22752

[startup+410.037 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 8106 0 0 0 40872 70 0 0 25 0 1 0 1856027223 30314496 4580 4294967295 134512640 135094434 3221224432 3221220028 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/5782/statm): 7401 4580 145 145 0 7256 0
[pid=5782] vsize: 29604
Current children cumulated CPU time (s) 409.43
Current children cumulated vsize (Kb) 31728

[startup+420.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 11052 0 0 0 41857 79 0 0 25 0 1 0 1856027223 41996288 7113 4294967295 134512640 135094434 3221224432 3218839632 134597447 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 10253 7113 145 145 0 10108 0
[pid=5782] vsize: 41012
Current children cumulated CPU time (s) 419.37
Current children cumulated vsize (Kb) 43136

[startup+430.039 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 45064 0 0 0 42658 194 0 0 25 0 1 0 1856027223 138784768 30743 4294967295 134512640 135094434 3221224432 3219105052 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/5782/statm): 33883 30743 145 145 0 33738 0
[pid=5782] vsize: 135532
Current children cumulated CPU time (s) 428.53
Current children cumulated vsize (Kb) 137656

[startup+440.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 79741 0 0 0 43458 309 0 0 25 0 1 0 1856027223 237625344 54874 4294967295 134512640 135094434 3221224432 3220264768 134594880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 58014 54874 145 145 0 57869 0
[pid=5782] vsize: 232056
Current children cumulated CPU time (s) 437.68
Current children cumulated vsize (Kb) 234180

[startup+450.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 99345 0 0 0 44240 408 0 0 23 0 1 0 1856027223 317923328 74478 4294967295 134512640 135094434 3221224432 3218844624 134594844 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5782/statm): 77618 74478 145 145 0 77473 0
[pid=5782] vsize: 310472
Current children cumulated CPU time (s) 446.49
Current children cumulated vsize (Kb) 312596

[startup+460.041 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 153807 0 0 0 45009 564 0 0 22 0 1 0 1856027223 454610944 107849 4294967295 134512640 135094434 3221224432 3219613516 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/5782/statm): 110989 107849 145 145 0 110844 0
[pid=5782] vsize: 443956
Current children cumulated CPU time (s) 455.74
Current children cumulated vsize (Kb) 446080

[startup+470.042 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 176946 0 0 0 45754 677 0 0 21 0 1 0 1856027223 549388288 130988 4294967295 134512640 135094434 3221224432 3218840172 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/5782/statm): 134128 130988 145 145 0 133983 0
[pid=5782] vsize: 536512
Current children cumulated CPU time (s) 464.32
Current children cumulated vsize (Kb) 538636

[startup+480.044 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 200290 0 0 0 46502 786 0 0 22 0 1 0 1856027223 645009408 154332 4294967295 134512640 135094434 3221224432 3218876428 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/5782/statm): 157473 154332 145 145 0 157328 0
[pid=5782] vsize: 629892
Current children cumulated CPU time (s) 472.89
Current children cumulated vsize (Kb) 632016



Mem limit exceeded: sending SIGTERM then SIGKILL

[startup+480.471 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 5782
Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/5778/statm): 531 226 485 147 0 384 0
[pid=5778] vsize: 2124
Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 201286 0 0 0 46534 790 0 0 21 0 1 0 1856027223 994635776 155328 4294967295 134512640 135094434 3221224432 3218861484 134802701 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/5782/statm): 242831 155328 145 145 0 242686 0
[pid=5782] vsize: 971324
Current children cumulated CPU time (s) 473.25
Current children cumulated vsize (Kb) 973448

Sending SIGTERM to -5778
Sleeping 2 seconds
One traced child (pid=5778) ended because it received signal 15 (SIGTERM)
One traced child (pid=5782) ended because it received signal 11 (SIGSEGV)
All traced children have exited ! Game is over.

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 480.759
CPU time (s): 473.535
CPU user time (s): 465.343
CPU system time (s): 8.19175
CPU usage (%): 98.4975
Max. virtual memory (cumulated for all children) (Kb): 973448

Verifier Data

ERROR: no interpretation found !