Name | mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-modglob.opb |
MD5SUM | 18f1d450b3ce1b90a2f0f08d0288db4f |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
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 | 9818 |
Biggest coefficient in the objective function | 22009559908352000000 |
Number of bits for the biggest coefficient in the objective function | 65 |
Sum of the numbers in the objective function | 1485172925553747165184 |
Number of bits of the sum of numbers in the objective function | 71 |
Biggest number in a constraint | 22009559908352000000 |
Number of bits of the biggest number in a constraint | 65 |
Biggest sum of numbers in a constraint | 1485172925553747165184 |
Number of bits of the biggest sum of numbers | 71 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 9818 |
Total number of constraints | 389 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 98 |
Number of constraints which are nor clauses,nor cardinality constraints | 291 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 270 |
LAUNCH ON wulflinc19 THE 2005-09-19 03:46:12 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2922 boxname=wulflinc19 idbench=578 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 18f1d450b3ce1b90a2f0f08d0288db4f /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-modglob.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-modglob.opb IDLAUNCH: 2922 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 886520 kB Buffers: 35928 kB Cached: 84892 kB SwapCached: 832 kB Active: 73468 kB Inactive: 49956 kB HighTotal: 131008 kB HighFree: 45332 kB LowTotal: 903652 kB LowFree: 841188 kB SwapTotal: 2097892 kB SwapFree: 2096460 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5700 kB Slab: 19092 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 04:06:23 (client local time) WITH STATUS 0 IN 1203.14 SECONDS stats: 2922 7 1203.14 0
c Parsing PB file... c PARSE ERROR! [line 426] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 382 PB-constraints to clauses... c -- Unit propagations: p c -- Detecting intervals from adjacent constraints: ############################################################################################# c -- Clauses(.)/Splits(s): (none) c ---[ 380]---> Sorter-cost: 799 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 379]---> BDD-cost: 36 c ---[ 378]---> BDD-cost: 36 c ---[ 377]---> BDD-cost: 36 c ---[ 376]---> BDD-cost: 36 c ---[ 375]---> BDD-cost: 36 c ---[ 374]---> BDD-cost: 36 c ---[ 373]---> BDD-cost: 36 c ---[ 372]---> BDD-cost: 36 c ---[ 371]---> BDD-cost: 36 c ---[ 370]---> BDD-cost: 36 c ---[ 368]---> BDD-cost: 0 c ---[ 367]---> BDD-cost: 36 c ---[ 366]---> BDD-cost: 36 c ---[ 365]---> BDD-cost: 36 c ---[ 364]---> BDD-cost: 36 c ---[ 363]---> BDD-cost: 36 c ---[ 362]---> BDD-cost: 36 c ---[ 361]---> BDD-cost: 36 c ---[ 360]---> BDD-cost: 36 c ---[ 359]---> BDD-cost: 36 c ---[ 358]---> BDD-cost: 36 c ---[ 356]---> BDD-cost: 0 c ---[ 355]---> BDD-cost: 36 c ---[ 354]---> BDD-cost: 36 c ---[ 353]---> BDD-cost: 36 c ---[ 352]---> BDD-cost: 36 c ---[ 351]---> BDD-cost: 36 c ---[ 350]---> BDD-cost: 36 c ---[ 349]---> BDD-cost: 36 c ---[ 348]---> BDD-cost: 36 c ---[ 347]---> BDD-cost: 36 c ---[ 346]---> BDD-cost: 36 c ---[ 344]---> BDD-cost: 0 c ---[ 343]---> BDD-cost: 36 c ---[ 342]---> BDD-cost: 36 c ---[ 341]---> BDD-cost: 36 c ---[ 340]---> BDD-cost: 36 c ---[ 339]---> BDD-cost: 36 c ---[ 338]---> BDD-cost: 36 c ---[ 337]---> BDD-cost: 36 c ---[ 336]---> BDD-cost: 36 c ---[ 335]---> BDD-cost: 36 c ---[ 334]---> BDD-cost: 36 c ---[ 332]---> BDD-cost: 0 c ---[ 331]---> BDD-cost: 36 c ---[ 330]---> BDD-cost: 36 c ---[ 329]---> BDD-cost: 36 c ---[ 328]---> BDD-cost: 36 c ---[ 327]---> BDD-cost: 36 c ---[ 326]---> BDD-cost: 36 c ---[ 325]---> BDD-cost: 36 c ---[ 324]---> BDD-cost: 36 c ---[ 323]---> BDD-cost: 36 c ---[ 322]---> BDD-cost: 36 c ---[ 320]---> BDD-cost: 0 c ---[ 319]---> BDD-cost: 36 c ---[ 318]---> BDD-cost: 36 c ---[ 317]---> BDD-cost: 36 c ---[ 316]---> BDD-cost: 36 c ---[ 315]---> BDD-cost: 36 c ---[ 314]---> BDD-cost: 36 c ---[ 313]---> BDD-cost: 36 c ---[ 312]---> BDD-cost: 36 c ---[ 311]---> BDD-cost: 36 c ---[ 310]---> BDD-cost: 36 c ---[ 308]---> BDD-cost: 0 c ---[ 307]---> BDD-cost: 36 c ---[ 306]---> BDD-cost: 36 c ---[ 305]---> BDD-cost: 36 c ---[ 304]---> BDD-cost: 36 c ---[ 303]---> BDD-cost: 36 c ---[ 302]---> BDD-cost: 36 c ---[ 301]---> BDD-cost: 36 c ---[ 300]---> BDD-cost: 36 c ---[ 299]---> BDD-cost: 36 c ---[ 298]---> BDD-cost: 36 c ---[ 296]---> BDD-cost: 0 c ---[ 295]---> BDD-cost: 36 c ---[ 294]---> BDD-cost: 36 c ---[ 293]---> BDD-cost: 36 c ---[ 292]---> BDD-cost: 36 c ---[ 291]---> BDD-cost: 36 c ---[ 290]---> BDD-cost: 36 c ---[ 289]---> BDD-cost: 36 c ---[ 288]---> BDD-cost: 36 c ---[ 287]---> BDD-cost: 36 c ---[ 286]---> BDD-cost: 36 c ---[ 284]---> BDD-cost: 0 c ---[ 283]---> BDD-cost: 36 c ---[ 282]---> BDD-cost: 36 c ---[ 281]---> BDD-cost: 36 c ---[ 280]---> BDD-cost: 36 c ---[ 279]---> BDD-cost: 36 c ---[ 278]---> BDD-cost: 36 c ---[ 277]---> BDD-cost: 36 c ---[ 276]---> BDD-cost: 36 c ---[ 275]---> BDD-cost: 36 c ---[ 274]---> BDD-cost: 36 c ---[ 272]---> BDD-cost: 0 c ---[ 271]---> BDD-cost: 36 c ---[ 270]---> BDD-cost: 36 c ---[ 269]---> BDD-cost: 36 c ---[ 268]---> BDD-cost: 36 c ---[ 267]---> BDD-cost: 36 c ---[ 266]---> BDD-cost: 36 c ---[ 265]---> BDD-cost: 36 c ---[ 264]---> BDD-cost: 36 c ---[ 263]---> BDD-cost: 36 c ---[ 262]---> BDD-cost: 36 c ---[ 260]---> BDD-cost: 0 c ---[ 259]---> BDD-cost: 36 c ---[ 258]---> BDD-cost: 36 c ---[ 257]---> BDD-cost: 36 c ---[ 256]---> BDD-cost: 36 c ---[ 255]---> BDD-cost: 36 c ---[ 254]---> BDD-cost: 36 c ---[ 253]---> BDD-cost: 36 c ---[ 252]---> BDD-cost: 36 c ---[ 251]---> BDD-cost: 36 c ---[ 250]---> BDD-cost: 36 c ---[ 248]--
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/22378/stat): 22378 (minisat+_script) R 22377 22378 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846747557 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/22378/statm): 174 3 169 147 0 27 0 [pid=22378] 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=22379 New process pid=22380 New process pid=22381 execve syscall for /bin/sed executable One traced child (pid=22380) 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=22381) exited with status: 0 One traced child (pid=22379) exited with status: 0 New process pid=22382 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-modglob.opb One traced child (pid=22382) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=22383 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-modglob.opb [startup+10.0036 s] Raw data (loadavg): 0.93 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 5085 0 0 0 948 23 0 0 25 0 1 0 1846747563 18812928 4393 4294967295 134512640 135167914 3221224448 3221197264 134849163 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22383/statm): 4593 4393 162 162 0 4431 0 [pid=22383] vsize: 18372 Current children cumulated CPU time (s) 9.73 Current children cumulated vsize (Kb) 20500 [startup+20.0054 s] Raw data (loadavg): 0.94 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 10682 0 0 0 1895 51 0 0 25 0 1 0 1846747563 39038976 9331 4294967295 134512640 135167914 3221224448 3221197204 134697403 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22383/statm): 9531 9331 162 162 0 9369 0 [pid=22383] vsize: 38124 Current children cumulated CPU time (s) 19.48 Current children cumulated vsize (Kb) 40252 [startup+30.0062 s] Raw data (loadavg): 0.95 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 17353 0 0 0 2843 75 0 0 25 0 1 0 1846747563 60964864 14684 4294967295 134512640 135167914 3221224448 3221200176 134849187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22383/statm): 14884 14684 162 162 0 14722 0 [pid=22383] vsize: 59536 Current children cumulated CPU time (s) 29.2 Current children cumulated vsize (Kb) 61664 [startup+40.006 s] Raw data (loadavg): 0.96 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 21837 0 0 0 3793 96 0 0 25 0 1 0 1846747563 79331328 19168 4294967295 134512640 135167914 3221224448 3221197220 134844636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 19368 19168 162 162 0 19206 0 [pid=22383] vsize: 77472 Current children cumulated CPU time (s) 38.91 Current children cumulated vsize (Kb) 79600 [startup+50.0068 s] Raw data (loadavg): 0.96 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 30669 0 0 0 4742 126 0 0 25 0 1 0 1846747563 104706048 25363 4294967295 134512640 135167914 3221224448 3221200992 134845913 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 25563 25363 162 162 0 25401 0 [pid=22383] vsize: 102252 Current children cumulated CPU time (s) 48.7 Current children cumulated vsize (Kb) 104380 [startup+60.0066 s] Raw data (loadavg): 0.97 0.98 0.99 1/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 35160 0 0 0 5696 146 0 0 25 0 1 0 1846747563 123101184 29854 4294967295 134512640 135167914 3221224448 3221199676 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/22383/statm): 30054 29854 162 162 0 29892 0 [pid=22383] vsize: 120216 Current children cumulated CPU time (s) 58.44 Current children cumulated vsize (Kb) 122344 [startup+70.0074 s] Raw data (loadavg): 0.97 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 39560 0 0 0 6648 166 0 0 25 0 1 0 1846747563 141123584 34254 4294967295 134512640 135167914 3221224448 3221198816 134694439 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 34454 34254 162 162 0 34292 0 [pid=22383] vsize: 137816 Current children cumulated CPU time (s) 68.16 Current children cumulated vsize (Kb) 139944 [startup+80.0083 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 54024 0 0 0 7583 207 0 0 25 0 1 0 1846747563 200368128 48718 4294967295 134512640 135167914 3221224448 3221198092 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22383/statm): 48918 48718 162 162 0 48756 0 [pid=22383] vsize: 195672 Current children cumulated CPU time (s) 77.92 Current children cumulated vsize (Kb) 197800 [startup+90.0081 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 56917 0 0 0 8548 222 0 0 25 0 1 0 1846747563 190619648 46338 4294967295 134512640 135167914 3221224448 3221197872 134623813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 46538 46338 162 162 0 46376 0 [pid=22383] vsize: 186152 Current children cumulated CPU time (s) 87.72 Current children cumulated vsize (Kb) 188280 [startup+100.009 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 61260 0 0 0 9500 242 0 0 25 0 1 0 1846747563 208408576 50681 4294967295 134512640 135167914 3221224448 3221200896 134844697 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 50881 50681 162 162 0 50719 0 [pid=22383] vsize: 203524 Current children cumulated CPU time (s) 97.44 Current children cumulated vsize (Kb) 205652 [startup+110.01 s] Raw data (loadavg): 0.98 0.98 0.99 1/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 65564 0 0 0 10452 264 0 0 25 0 1 0 1846747563 226037760 54985 4294967295 134512640 135167914 3221224448 3221197372 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/22383/statm): 55185 54985 162 162 0 55023 0 [pid=22383] vsize: 220740 Current children cumulated CPU time (s) 107.18 Current children cumulated vsize (Kb) 222868 [startup+120.011 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 69850 0 0 0 11406 283 0 0 25 0 1 0 1846747563 243593216 59271 4294967295 134512640 135167914 3221224448 3221195772 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/22383/statm): 59471 59271 162 162 0 59309 0 [pid=22383] vsize: 237884 Current children cumulated CPU time (s) 116.91 Current children cumulated vsize (Kb) 240012 [startup+130.011 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 74046 0 0 0 12362 301 0 0 25 0 1 0 1846747563 260780032 63467 4294967295 134512640 135167914 3221224448 3221202144 134696164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 63667 63467 162 162 0 63505 0 [pid=22383] vsize: 254668 Current children cumulated CPU time (s) 126.65 Current children cumulated vsize (Kb) 256796 [startup+140.011 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 78190 0 0 0 13319 320 0 0 25 0 1 0 1846747563 277745664 67611 4294967295 134512640 135167914 3221224448 3221195740 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/22383/statm): 67809 67611 162 162 0 67647 0 [pid=22383] vsize: 271236 Current children cumulated CPU time (s) 136.41 Current children cumulated vsize (Kb) 273364 [startup+150.012 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 82302 0 0 0 14274 338 0 0 25 0 1 0 1846747563 294580224 71723 4294967295 134512640 135167914 3221224448 3221196320 134695975 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 71919 71723 162 162 0 71757 0 [pid=22383] vsize: 287676 Current children cumulated CPU time (s) 146.14 Current children cumulated vsize (Kb) 289804 [startup+160.012 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 106921 0 0 0 15189 401 0 0 25 0 1 0 1846747563 395419648 96342 4294967295 134512640 135167914 3221224448 3221199952 134625468 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 96538 96342 162 162 0 96376 0 [pid=22383] vsize: 386152 Current children cumulated CPU time (s) 155.92 Current children cumulated vsize (Kb) 388280 [startup+170.013 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 108066 0 0 0 16175 408 0 0 25 0 1 0 1846747563 356913152 86941 4294967295 134512640 135167914 3221224448 3221197008 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 87137 86941 162 162 0 86975 0 [pid=22383] vsize: 348548 Current children cumulated CPU time (s) 165.85 Current children cumulated vsize (Kb) 350676 [startup+180.013 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 112119 0 0 0 17136 426 0 0 25 0 1 0 1846747563 373514240 90994 4294967295 134512640 135167914 3221224448 3221202416 134693563 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 91190 90994 162 162 0 91028 0 [pid=22383] vsize: 364760 Current children cumulated CPU time (s) 175.64 Current children cumulated vsize (Kb) 366888 [startup+190.014 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 116118 0 0 0 18089 445 0 0 25 0 1 0 1846747563 389894144 94993 4294967295 134512640 135167914 3221224448 3221196956 134843033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 95189 94993 162 162 0 95027 0 [pid=22383] vsize: 380756 Current children cumulated CPU time (s) 185.36 Current children cumulated vsize (Kb) 382884 [startup+200.015 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 120103 0 0 0 19047 462 0 0 25 0 1 0 1846747563 406212608 98978 4294967295 134512640 135167914 3221224448 3221199872 134843400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 99173 98978 162 162 0 99011 0 [pid=22383] vsize: 396692 Current children cumulated CPU time (s) 195.11 Current children cumulated vsize (Kb) 398820 [startup+210.015 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 124006 0 0 0 20003 480 0 0 25 0 1 0 1846747563 422199296 102881 4294967295 134512640 135167914 3221224448 3221197376 134694383 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22383/statm): 103076 102881 162 162 0 102914 0 [pid=22383] vsize: 412304 Current children cumulated CPU time (s) 204.85 Current children cumulated vsize (Kb) 414432 [startup+220.017 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 127931 0 0 0 20962 497 0 0 25 0 1 0 1846747563 438276096 106806 4294967295 134512640 135167914 3221224448 3221197376 134843107 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 107001 106806 162 162 0 106839 0 [pid=22383] vsize: 428004 Current children cumulated CPU time (s) 214.61 Current children cumulated vsize (Kb) 430132 [startup+230.018 s] Raw data (loadavg): 1.07 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 131793 0 0 0 21918 518 0 0 25 0 1 0 1846747563 454094848 110668 4294967295 134512640 135167914 3221224448 3221196004 134849086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 110863 110668 162 162 0 110701 0 [pid=22383] vsize: 443452 Current children cumulated CPU time (s) 224.38 Current children cumulated vsize (Kb) 445580 [startup+240.017 s] Raw data (loadavg): 1.06 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 135647 0 0 0 22874 535 0 0 25 0 1 0 1846747563 469880832 114522 4294967295 134512640 135167914 3221224448 3221199584 134849606 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 114717 114522 162 162 0 114555 0 [pid=22383] vsize: 458868 Current children cumulated CPU time (s) 234.11 Current children cumulated vsize (Kb) 460996 [startup+250.018 s] Raw data (loadavg): 1.05 1.00 1.00 1/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 139421 0 0 0 23836 550 0 0 25 0 1 0 1846747563 485339136 118296 4294967295 134512640 135167914 3221224448 3221198044 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/22383/statm): 118491 118296 162 162 0 118329 0 [pid=22383] vsize: 473964 Current children cumulated CPU time (s) 243.88 Current children cumulated vsize (Kb) 476092 [startup+260.019 s] Raw data (loadavg): 1.04 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 143190 0 0 0 24794 567 0 0 25 0 1 0 1846747563 500776960 122065 4294967295 134512640 135167914 3221224448 3221196700 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 122260 122065 162 162 0 122098 0 [pid=22383] vsize: 489040 Current children cumulated CPU time (s) 253.63 Current children cumulated vsize (Kb) 491168 [startup+270.02 s] Raw data (loadavg): 1.04 1.00 1.00 1/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 146907 0 0 0 25753 584 0 0 25 0 1 0 1846747563 516001792 125782 4294967295 134512640 135167914 3221224448 3221195468 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/22383/statm): 125977 125782 162 162 0 125815 0 [pid=22383] vsize: 503908 Current children cumulated CPU time (s) 263.39 Current children cumulated vsize (Kb) 506036 [startup+280.021 s] Raw data (loadavg): 1.03 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 150551 0 0 0 26714 601 0 0 25 0 1 0 1846747563 530927616 129426 4294967295 134512640 135167914 3221224448 3221198012 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/22383/statm): 129621 129426 162 162 0 129459 0 [pid=22383] vsize: 518484 Current children cumulated CPU time (s) 273.17 Current children cumulated vsize (Kb) 520612 [startup+290.021 s] Raw data (loadavg): 1.03 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 154208 0 0 0 27679 617 0 0 25 0 1 0 1846747563 545906688 133083 4294967295 134512640 135167914 3221224448 3221195804 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22383/statm): 133278 133083 162 162 0 133116 0 [pid=22383] vsize: 533112 Current children cumulated CPU time (s) 282.98 Current children cumulated vsize (Kb) 535240 [startup+300.022 s] Raw data (loadavg): 1.02 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) T 22378 22378 5929 0 -1 0 157877 0 0 0 28639 632 0 0 25 0 1 0 1846747563 560922624 136752 4294967295 134512640 135167914 3221224448 3221203164 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/22383/statm): 136944 136752 162 162 0 136782 0 [pid=22383] vsize: 547776 Current children cumulated CPU time (s) 292.73 Current children cumulated vsize (Kb) 549904 [startup+310.022 s] Raw data (loadavg): 1.02 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 29635 636 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221222984 134846944 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 302.73 Current children cumulated vsize (Kb) 465600 [startup+320.023 s] Raw data (loadavg): 1.01 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 30635 636 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217408 134849092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 312.73 Current children cumulated vsize (Kb) 465600 [startup+330.024 s] Raw data (loadavg): 1.01 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 31635 636 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217532 134844638 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 322.73 Current children cumulated vsize (Kb) 465600 [startup+340.024 s] Raw data (loadavg): 1.01 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 32635 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218476 134694368 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 332.74 Current children cumulated vsize (Kb) 465600 [startup+350.024 s] Raw data (loadavg): 1.01 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 33635 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218032 134843010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 342.74 Current children cumulated vsize (Kb) 465600 [startup+360.025 s] Raw data (loadavg): 1.01 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 34635 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217908 134845880 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 352.74 Current children cumulated vsize (Kb) 465600 [startup+370.026 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 35636 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218280 134722657 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 362.75 Current children cumulated vsize (Kb) 465600 [startup+380.027 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 36636 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218096 134849148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 372.75 Current children cumulated vsize (Kb) 465600 [startup+390.027 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 37636 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218256 134849148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 382.75 Current children cumulated vsize (Kb) 465600 [startup+400.027 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 38636 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217740 134845940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 392.75 Current children cumulated vsize (Kb) 465600 [startup+410.028 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 39636 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218096 134522315 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 402.75 Current children cumulated vsize (Kb) 465600 [startup+420.029 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 40637 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218464 134693570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 412.76 Current children cumulated vsize (Kb) 465600 [startup+430.03 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 41637 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219152 134849099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 422.76 Current children cumulated vsize (Kb) 465600 [startup+440.03 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 42637 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217712 134844637 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 432.76 Current children cumulated vsize (Kb) 465600 [startup+450.03 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 43637 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218064 134720491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 442.76 Current children cumulated vsize (Kb) 465600 [startup+460.03 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 44637 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218208 134845901 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 452.76 Current children cumulated vsize (Kb) 465600 [startup+470.032 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 45637 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217936 134849092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 462.76 Current children cumulated vsize (Kb) 465600 [startup+480.033 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 46638 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218208 134845895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 472.77 Current children cumulated vsize (Kb) 465600 [startup+490.033 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 47638 637 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219280 134696197 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 482.77 Current children cumulated vsize (Kb) 465600 [startup+500.034 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 48638 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218636 134722542 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 492.78 Current children cumulated vsize (Kb) 465600 [startup+510.034 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 49638 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218472 134693793 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 502.78 Current children cumulated vsize (Kb) 465600 [startup+520.035 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 50638 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219076 134843117 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 512.78 Current children cumulated vsize (Kb) 465600 [startup+530.036 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 51638 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217792 134630908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 522.78 Current children cumulated vsize (Kb) 465600 [startup+540.037 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 52639 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218620 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 532.79 Current children cumulated vsize (Kb) 465600 [startup+550.038 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 53639 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218944 134720491 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 542.79 Current children cumulated vsize (Kb) 465600 [startup+560.037 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 54639 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218824 134694321 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 552.79 Current children cumulated vsize (Kb) 465600 [startup+570.039 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 55639 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218368 134718181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 562.79 Current children cumulated vsize (Kb) 465600 [startup+580.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 56639 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219320 134845939 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 572.79 Current children cumulated vsize (Kb) 465600 [startup+590.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 57639 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218988 134849088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 582.79 Current children cumulated vsize (Kb) 465600 [startup+600.041 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 58640 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218756 134843031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 592.8 Current children cumulated vsize (Kb) 465600 [startup+610.042 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 59640 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218496 134629506 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 602.8 Current children cumulated vsize (Kb) 465600 [startup+620.042 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 60640 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217716 134845880 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 612.8 Current children cumulated vsize (Kb) 465600 [startup+630.043 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 61640 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219152 134849096 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 622.8 Current children cumulated vsize (Kb) 465600 [startup+640.044 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 62640 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218800 134843010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 632.8 Current children cumulated vsize (Kb) 465600 [startup+650.045 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 63641 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218304 134629123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 642.81 Current children cumulated vsize (Kb) 465600 [startup+660.046 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 64641 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218624 134694545 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 652.81 Current children cumulated vsize (Kb) 465600 [startup+670.046 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 65641 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218900 134718502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 662.81 Current children cumulated vsize (Kb) 465600 [startup+680.047 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 66641 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218976 134843130 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 672.81 Current children cumulated vsize (Kb) 465600 [startup+690.047 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 67641 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219628 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 682.81 Current children cumulated vsize (Kb) 465600 [startup+700.048 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 68642 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217872 134843064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 692.82 Current children cumulated vsize (Kb) 465600 [startup+710.049 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 69642 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219008 134629172 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 702.82 Current children cumulated vsize (Kb) 465600 [startup+720.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 70642 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218576 134849143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 712.82 Current children cumulated vsize (Kb) 465600 [startup+730.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 71642 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219080 134844633 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 722.82 Current children cumulated vsize (Kb) 465600 [startup+740.051 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 72643 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219508 134849147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 732.83 Current children cumulated vsize (Kb) 465600 [startup+750.052 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 73643 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218800 134694517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 742.83 Current children cumulated vsize (Kb) 465600 [startup+760.052 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 74643 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218800 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 752.83 Current children cumulated vsize (Kb) 465600 [startup+770.053 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 75643 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219168 134694351 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 762.83 Current children cumulated vsize (Kb) 465600 [startup+780.053 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 76643 638 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219192 134629047 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 772.83 Current children cumulated vsize (Kb) 465600 [startup+790.053 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 77643 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219944 134844674 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 782.84 Current children cumulated vsize (Kb) 465600 [startup+800.054 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 78644 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218448 134843010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 792.85 Current children cumulated vsize (Kb) 465600 [startup+810.055 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 79644 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221220028 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 802.85 Current children cumulated vsize (Kb) 465600 [startup+820.056 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 80644 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218544 134845933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 812.85 Current children cumulated vsize (Kb) 465600 [startup+830.057 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 81644 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218672 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 822.85 Current children cumulated vsize (Kb) 465600 [startup+840.057 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 82645 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218912 134843074 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 832.86 Current children cumulated vsize (Kb) 465600 [startup+850.058 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 83645 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218240 134849096 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 842.86 Current children cumulated vsize (Kb) 465600 [startup+860.058 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 84645 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218800 134849179 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 852.86 Current children cumulated vsize (Kb) 465600 [startup+870.059 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 85645 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219008 134629145 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 862.86 Current children cumulated vsize (Kb) 465600 [startup+880.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 86645 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217852 134844675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 872.86 Current children cumulated vsize (Kb) 465600 [startup+890.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 87646 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219520 134693561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 882.87 Current children cumulated vsize (Kb) 465600 [startup+900.061 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 88646 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218396 134723267 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 892.87 Current children cumulated vsize (Kb) 465600 [startup+910.061 s] Raw data (loadavg): 1.08 1.02 1.01 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 89646 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218720 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 902.87 Current children cumulated vsize (Kb) 465600 [startup+920.062 s] Raw data (loadavg): 1.07 1.02 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 90646 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218912 134845933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 912.87 Current children cumulated vsize (Kb) 465600 [startup+930.063 s] Raw data (loadavg): 1.06 1.01 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 91646 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218280 134722657 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 922.87 Current children cumulated vsize (Kb) 465600 [startup+940.062 s] Raw data (loadavg): 1.05 1.01 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 92647 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218736 134845895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 932.88 Current children cumulated vsize (Kb) 465600 [startup+950.063 s] Raw data (loadavg): 1.04 1.01 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 93647 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221220368 134849148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 942.88 Current children cumulated vsize (Kb) 465600 [startup+960.064 s] Raw data (loadavg): 1.03 1.01 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 94647 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218884 134844636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 952.88 Current children cumulated vsize (Kb) 465600 [startup+970.065 s] Raw data (loadavg): 1.03 1.01 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 95647 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219456 134696608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 962.88 Current children cumulated vsize (Kb) 465600 [startup+980.066 s] Raw data (loadavg): 1.02 1.01 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 96648 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219260 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 972.89 Current children cumulated vsize (Kb) 465600 [startup+990.067 s] Raw data (loadavg): 1.02 1.01 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 97648 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219704 134522321 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 982.89 Current children cumulated vsize (Kb) 465600 [startup+1000.07 s] Raw data (loadavg): 1.02 1.01 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 98648 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218496 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 992.89 Current children cumulated vsize (Kb) 465600 [startup+1010.07 s] Raw data (loadavg): 1.01 1.01 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 99648 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218912 134845903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1002.89 Current children cumulated vsize (Kb) 465600 [startup+1020.07 s] Raw data (loadavg): 1.01 1.01 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 100648 639 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218832 134629340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1012.89 Current children cumulated vsize (Kb) 465600 [startup+1030.07 s] Raw data (loadavg): 1.01 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 101648 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219888 134629285 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1022.9 Current children cumulated vsize (Kb) 465600 [startup+1040.07 s] Raw data (loadavg): 1.01 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 102648 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218096 134843107 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1032.9 Current children cumulated vsize (Kb) 465600 [startup+1050.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 103649 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218080 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1042.91 Current children cumulated vsize (Kb) 465600 [startup+1060.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 104649 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218672 134844736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1052.91 Current children cumulated vsize (Kb) 465600 [startup+1070.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 105649 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219904 134844703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1062.91 Current children cumulated vsize (Kb) 465600 [startup+1080.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 106649 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218208 134844731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1072.91 Current children cumulated vsize (Kb) 465600 [startup+1090.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 107649 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219148 134722225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1082.91 Current children cumulated vsize (Kb) 465600 [startup+1100.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 108649 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218288 134694351 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1092.91 Current children cumulated vsize (Kb) 465600 [startup+1110.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 109650 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219360 134630853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1102.92 Current children cumulated vsize (Kb) 465600 [startup+1120.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 110650 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221217368 134842997 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1112.92 Current children cumulated vsize (Kb) 465600 [startup+1130.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 111650 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218736 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1122.92 Current children cumulated vsize (Kb) 465600 [startup+1140.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 112650 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219360 134629290 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1132.92 Current children cumulated vsize (Kb) 465600 [startup+1150.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 113651 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219440 134845895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1142.93 Current children cumulated vsize (Kb) 465600 [startup+1160.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 114651 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218192 134845903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1152.93 Current children cumulated vsize (Kb) 465600 [startup+1170.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 115651 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221220448 134845903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1162.93 Current children cumulated vsize (Kb) 465600 [startup+1180.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 116651 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219024 134844653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1172.93 Current children cumulated vsize (Kb) 465600 [startup+1190.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 117651 640 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219704 134693553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1182.93 Current children cumulated vsize (Kb) 465600 [startup+1200.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 118651 641 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221219680 134843113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1192.94 Current children cumulated vsize (Kb) 465600 [startup+1210.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 119651 641 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218848 134630908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1202.94 Current children cumulated vsize (Kb) 465600 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 22383 Raw data (/proc/22378/stat): 22378 (minisat+_script) S 22377 22378 5929 0 -1 0 314 332 0 0 0 1 0 1 22 0 1 0 1846747557 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/22378/statm): 532 234 485 147 0 385 0 [pid=22378] vsize: 2128 Raw data (/proc/22383/stat): 22383 (minisat+_bignum) R 22378 22378 5929 0 -1 0 157892 0 0 0 119651 641 0 0 25 0 1 0 1846747563 474595328 115676 4294967295 134512640 135167914 3221224448 3221218800 134843400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22383/statm): 115868 115676 162 162 0 115706 0 [pid=22383] vsize: 463472 Current children cumulated CPU time (s) 1202.94 Current children cumulated vsize (Kb) 465600 Sending SIGTERM to -22378 Sleeping 2 seconds One traced child (pid=22378) ended because it received signal 15 (SIGTERM) One traced child (pid=22383) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.3 CPU time (s): 1203.14 CPU user time (s): 1196.52 CPU system time (s): 6.62099 CPU usage (%): 99.4087 Max. virtual memory (cumulated for all children) (Kb): 549904
ERROR: no interpretation found !