Name | mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-blp-ir98.opb |
MD5SUM | fb418db515bc70c21d294b6cce4dc63f |
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 | 31 |
Biggest coefficient in the objective function | 1073741824 |
Number of bits for the biggest coefficient in the objective function | 31 |
Sum of the numbers in the objective function | 2147483647 |
Number of bits of the sum of numbers in the objective function | 31 |
Biggest number in a constraint | 83886080000000 |
Number of bits of the biggest number in a constraint | 47 |
Biggest sum of numbers in a constraint | 400587756783443 |
Number of bits of the biggest sum of numbers | 49 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 7287 |
Total number of constraints | 6560 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 6451 |
Number of constraints which are nor clauses,nor cardinality constraints | 109 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 6062 |
LAUNCH ON wulflinc25 THE 2005-09-20 01:58:16 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3098 boxname=wulflinc25 idbench=754 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fb418db515bc70c21d294b6cce4dc63f /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-blp-ir98.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-blp-ir98.opb IDLAUNCH: 3098 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 888864 kB Buffers: 25032 kB Cached: 91468 kB SwapCached: 868 kB Active: 33440 kB Inactive: 85664 kB HighTotal: 131008 kB HighFree: 36260 kB LowTotal: 903652 kB LowFree: 852604 kB SwapTotal: 2097892 kB SwapFree: 2096524 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5724 kB Slab: 20892 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 02:08:06 (client local time) WITH STATUS 0 IN 538.755 SECONDS stats: 3098 7 538.755 0
c Parsing PB file... c PARSE ERROR! [line 12220] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 595 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################################################## c -- Clauses(.)/Splits(s): (none) c ---[ 594]---> BDD-cost: 13 c ---[ 593]---> BDD-cost: 13 c ---[ 592]---> BDD-cost: 13 c ---[ 591]---> BDD-cost: 13 c ---[ 590]---> BDD-cost: 13 c ---[ 589]---> BDD-cost: 12 c ---[ 588]---> BDD-cost: 12 c ---[ 587]---> BDD-cost: 13 c ---[ 586]---> BDD-cost: 12 c ---[ 585]---> BDD-cost: 12 c ---[ 584]---> BDD-cost: 12 c ---[ 583]---> BDD-cost: 13 c ---[ 582]---> BDD-cost: 13 c ---[ 581]---> BDD-cost: 13 c ---[ 580]---> BDD-cost: 13 c ---[ 579]---> BDD-cost: 13 c ---[ 578]---> BDD-cost: 13 c ---[ 577]---> BDD-cost: 13 c ---[ 576]---> BDD-cost: 13 c ---[ 575]---> BDD-cost: 13 c ---[ 574]---> BDD-cost: 13 c ---[ 573]---> BDD-cost: 13 c ---[ 572]---> BDD-cost: 13 c ---[ 571]---> BDD-cost: 13 c ---[ 570]---> BDD-cost: 13 c ---[ 569]---> BDD-cost: 13 c ---[ 568]---> BDD-cost: 13 c ---[ 567]---> BDD-cost: 13 c ---[ 566]---> BDD-cost: 12 c ---[ 565]---> BDD-cost: 13 c ---[ 564]---> BDD-cost: 13 c ---[ 563]---> BDD-cost: 13 c ---[ 562]---> BDD-cost: 13 c ---[ 561]---> BDD-cost: 13 c ---[ 559]---> BDD-cost: 13 c ---[ 558]---> BDD-cost: 13 c ---[ 557]---> BDD-cost: 13 c ---[ 556]---> BDD-cost: 13 c ---[ 555]---> BDD-cost: 12 c ---[ 553]---> BDD-cost: 13 c ---[ 552]---> BDD-cost: 13 c ---[ 550]---> Adder-cost: 2746 maxlim: 2016256 bits: 21/21 c ---[ 548]---> Adder-cost: 1572 maxlim: 1411072 bits: 21/21 c ---[ 546]---> Adder-cost: 1058 maxlim: 774144 bits: 20/20 c ---[ 544]---> Adder-cost: 2140 maxlim: 1574912 bits: 21/21 c ---[ 542]---> Adder-cost: 1068 maxlim: 774144 bits: 20/20 c ---[ 540]---> Adder-cost: 1464 maxlim: 1126400 bits: 21/21 c ---[ 538]---> Adder-cost: 868 maxlim: 768000 bits: 20/20 c ---[ 536]---> Adder-cost: 4790 maxlim: 3856 bits: 12/12 c ---[ 534]---> Adder-cost: 4484 maxlim: 3897344 bits: 22/22 c ---[ 532]---> Adder-cost: 3172 maxlim: 2772992 bits: 22/22 c ---[ 530]---> Adder-cost: 1998 maxlim: 1849344 bits: 21/21 c ---[ 528]---> Adder-cost: 2086 maxlim: 2099200 bits: 22/22 c ---[ 526]---> Adder-cost: 1392 maxlim: 1105920 bits: 21/21 c ---[ 524]---> Adder-cost: 542 maxlim: 446464 bits: 19/19 c ---[ 522]---> Adder-cost: 1530 maxlim: 1665024 bits: 21/21 c ---[ 520]---> Adder-cost: 1464 maxlim: 1197056 bits: 21/21 c ---[ 518]---> Adder-cost: 958 maxlim: 817152 bits: 20/20 c ---[ 516]---> Sorter-cost: 186 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 514]---> Sorter-cost: 186 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 512]---> Adder-cost: 1184 maxlim: 1048576 bits: 21/21 c ---[ 510]---> Adder-cost: 880 maxlim: 885760 bits: 20/20 c ---[ 508]---> Adder-cost: 1420 maxlim: 1622016 bits: 21/21 c ---[ 506]---> Adder-cost: 1164 maxlim: 1024000 bits: 20/20 c ---[ 504]---> Adder-cost: 710 maxlim: 592896 bits: 20/20 c ---[ 502]---> Adder-cost: 878 maxlim: 840704 bits: 20/20 c ---[ 500]---> Adder-cost: 610 maxlim: 606208 bits: 20/20 c ---[ 498]---> Adder-cost: 178 maxlim: 163840 bits: 18/18 c ---[ 496]---> Adder-cost: 3768 maxlim: 3709952 bits: 22/22 c ---[ 494]---> Adder-cost: 3484 maxlim: 3786752 bits: 22/22 c ---[ 492]---> Adder-cost: 1354 maxlim: 1294336 bits: 21/21 c ---[ 490]---> Adder-cost: 1116 maxlim: 1150976 bits: 21/21 c ---[ 488]---> Adder-cost: 418 maxlim: 422912 bits: 19/19 c ---[ 486]---> Adder-cost: 888 maxlim: 872448 bits: 20/20 c ---[ 484]---> Adder-cost: 382 maxlim: 438272 bits: 19/19 c ---[ 482]---> Adder-cost: 480 maxlim: 477184 bits: 19/19 c ---[ 480]---> BDD-cost: 37 c ---[ 478]---> Adder-cost: 3226 maxlim: 3408896 bits: 22/22 c ---[ 476]---> Adder-cost: 1816 maxlim: 1841152 bits: 21/21 c ---[ 474]---> Adder-cost: 1052 maxlim: 1198080 bits: 21/21 c ---[ 472]---> Adder-cost: 328 maxlim: 348160 bits: 19/19 c ---[ 470]---> Adder-cost: 160
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/26315/stat): 26315 (minisat+_script) R 26314 26315 4419 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854784185 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/26315/statm): 174 3 169 147 0 27 0 [pid=26315] 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=26316 New process pid=26317 New process pid=26318 execve syscall for /bin/sed executable One traced child (pid=26317) 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=26318) exited with status: 0 One traced child (pid=26316) exited with status: 0 New process pid=26319 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-blp-ir98.opb [startup+10.0035 s] Raw data (loadavg): 0.93 0.96 0.94 2/57 26319 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854784185 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 531 226 485 147 0 384 0 [pid=26315] vsize: 2124 Raw data (/proc/26319/stat): 26319 (minisat+_64-bit) R 26315 26315 4419 0 -1 0 452 0 0 0 986 4 0 0 25 0 1 0 1854784190 2277376 438 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26319/statm): 556 438 145 145 0 411 0 [pid=26319] vsize: 2224 Current children cumulated CPU time (s) 9.9 Current children cumulated vsize (Kb) 4348 [startup+20.0051 s] Raw data (loadavg): 0.94 0.96 0.94 2/57 26319 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854784185 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 531 226 485 147 0 384 0 [pid=26315] vsize: 2124 Raw data (/proc/26319/stat): 26319 (minisat+_64-bit) R 26315 26315 4419 0 -1 0 861 0 0 0 1980 7 0 0 25 0 1 0 1854784190 3723264 710 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26319/statm): 909 710 145 145 0 764 0 [pid=26319] vsize: 3636 Current children cumulated CPU time (s) 19.87 Current children cumulated vsize (Kb) 5760 [startup+30.0057 s] Raw data (loadavg): 0.95 0.96 0.94 2/57 26319 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1854784185 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 531 226 485 147 0 384 0 [pid=26315] vsize: 2124 Raw data (/proc/26319/stat): 26319 (minisat+_64-bit) R 26315 26315 4419 0 -1 0 1171 0 0 0 2973 10 0 0 25 0 1 0 1854784190 5062656 917 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26319/statm): 1236 917 145 145 0 1091 0 [pid=26319] vsize: 4944 Current children cumulated CPU time (s) 29.83 Current children cumulated vsize (Kb) 7068 One traced child (pid=26319) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=26320 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-blp-ir98.opb [startup+40.0073 s] Raw data (loadavg): 0.96 0.96 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 332 0 0 0 688 2 0 0 25 0 1 0 1854787492 1851392 317 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 452 317 162 162 0 290 0 [pid=26320] vsize: 1808 Current children cumulated CPU time (s) 39.8 Current children cumulated vsize (Kb) 3936 [startup+50.0079 s] Raw data (loadavg): 0.96 0.96 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 777 0 0 0 1678 7 0 0 25 0 1 0 1854787492 3616768 762 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 883 762 162 162 0 721 0 [pid=26320] vsize: 3532 Current children cumulated CPU time (s) 49.75 Current children cumulated vsize (Kb) 5660 [startup+60.0085 s] Raw data (loadavg): 0.97 0.96 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 1339 0 0 0 2669 11 0 0 25 0 1 0 1854787492 5095424 1126 4294967295 134512640 135167914 3221224448 3221223284 134860174 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 1244 1126 162 162 0 1082 0 [pid=26320] vsize: 4976 Current children cumulated CPU time (s) 59.7 Current children cumulated vsize (Kb) 7104 [startup+70.0101 s] Raw data (loadavg): 0.97 0.96 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 1973 0 0 0 3659 16 0 0 25 0 1 0 1854787492 6774784 1536 4294967295 134512640 135167914 3221224448 3221221432 134722657 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 1654 1536 162 162 0 1492 0 [pid=26320] vsize: 6616 Current children cumulated CPU time (s) 69.65 Current children cumulated vsize (Kb) 8744 [startup+80.0107 s] Raw data (loadavg): 0.98 0.96 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 2924 0 0 0 4648 22 0 0 25 0 1 0 1854787492 8462336 1879 4294967295 134512640 135167914 3221224448 3221223312 134608296 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 2066 1879 162 162 0 1904 0 [pid=26320] vsize: 8264 Current children cumulated CPU time (s) 79.6 Current children cumulated vsize (Kb) 10392 [startup+90.0113 s] Raw data (loadavg): 0.98 0.96 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 3305 0 0 0 5640 26 0 0 25 0 1 0 1854787492 10014720 2260 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26320/statm): 2445 2260 162 162 0 2283 0 [pid=26320] vsize: 9780 Current children cumulated CPU time (s) 89.56 Current children cumulated vsize (Kb) 11908 [startup+100.012 s] Raw data (loadavg): 0.98 0.96 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 3844 0 0 0 6631 29 0 0 25 0 1 0 1854787492 11657216 2663 4294967295 134512640 135167914 3221224448 3221223312 134608335 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 2846 2663 162 162 0 2684 0 [pid=26320] vsize: 11384 Current children cumulated CPU time (s) 99.5 Current children cumulated vsize (Kb) 13512 [startup+110.012 s] Raw data (loadavg): 0.98 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 4695 0 0 0 7624 33 0 0 25 0 1 0 1854787492 15073280 3429 4294967295 134512640 135167914 3221224448 3220885564 134722512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 3680 3429 162 162 0 3518 0 [pid=26320] vsize: 14720 Current children cumulated CPU time (s) 109.47 Current children cumulated vsize (Kb) 16848 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 6156 0 0 0 8614 39 0 0 25 0 1 0 1854787492 18919424 4372 4294967295 134512640 135167914 3221224448 3221221024 134843420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 4619 4372 162 162 0 4457 0 [pid=26320] vsize: 18476 Current children cumulated CPU time (s) 119.43 Current children cumulated vsize (Kb) 20604 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 6338 0 0 0 9613 40 0 0 25 0 1 0 1854787492 19369984 4554 4294967295 134512640 135167914 3221224448 3221222928 134844672 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 4729 4554 162 162 0 4567 0 [pid=26320] vsize: 18916 Current children cumulated CPU time (s) 129.43 Current children cumulated vsize (Kb) 21044 [startup+140.015 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 6673 0 0 0 10612 41 0 0 25 0 1 0 1854787492 22237184 4889 4294967295 134512640 135167914 3221224448 3220091580 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 5429 4889 162 162 0 5267 0 [pid=26320] vsize: 21716 Current children cumulated CPU time (s) 139.43 Current children cumulated vsize (Kb) 23844 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 11600 0 0 0 11565 63 0 0 25 0 1 0 1854787492 39878656 9196 4294967295 134512640 135167914 3221224448 3220013948 134842996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 9736 9196 162 162 0 9574 0 [pid=26320] vsize: 38944 Current children cumulated CPU time (s) 149.18 Current children cumulated vsize (Kb) 41072 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 16978 0 0 0 12511 89 0 0 25 0 1 0 1854787492 59207680 13915 4294967295 134512640 135167914 3221224448 3219869084 134722576 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 14455 13915 162 162 0 14293 0 [pid=26320] vsize: 57820 Current children cumulated CPU time (s) 158.9 Current children cumulated vsize (Kb) 59948 [startup+170.018 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 23655 0 0 0 13462 114 0 0 19 0 1 0 1854787492 81158144 19274 4294967295 134512640 135167914 3221224448 3219876640 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 19814 19274 162 162 0 19652 0 [pid=26320] vsize: 79256 Current children cumulated CPU time (s) 168.66 Current children cumulated vsize (Kb) 81384 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 32975 0 0 0 14410 144 0 0 25 0 1 0 1854787492 119332864 28594 4294967295 134512640 135167914 3221224448 3219891532 134722542 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 29134 28594 162 162 0 28972 0 [pid=26320] vsize: 116536 Current children cumulated CPU time (s) 178.44 Current children cumulated vsize (Kb) 118664 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 36911 0 0 0 15366 162 0 0 25 0 1 0 1854787492 124653568 29893 4294967295 134512640 135167914 3221224448 3219917472 134844720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 30433 29893 162 162 0 30271 0 [pid=26320] vsize: 121732 Current children cumulated CPU time (s) 188.18 Current children cumulated vsize (Kb) 123860 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 41364 0 0 0 16314 188 0 0 25 0 1 0 1854787492 142893056 34346 4294967295 134512640 135167914 3221224448 3219866684 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26320/statm): 34886 34346 162 162 0 34724 0 [pid=26320] vsize: 139544 Current children cumulated CPU time (s) 197.92 Current children cumulated vsize (Kb) 141672 [startup+210.021 s] Raw data (loadavg): 0.99 0.97 0.94 1/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 45763 0 0 0 17261 211 0 0 25 0 1 0 1854787492 160911360 38745 4294967295 134512640 135167914 3221224448 3219869164 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26320/statm): 39285 38745 162 162 0 39123 0 [pid=26320] vsize: 157140 Current children cumulated CPU time (s) 207.62 Current children cumulated vsize (Kb) 159268 [startup+220.021 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 59418 0 0 0 18201 250 0 0 25 0 1 0 1854787492 216842240 52400 4294967295 134512640 135167914 3221224448 3219918412 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 52940 52400 162 162 0 52778 0 [pid=26320] vsize: 211760 Current children cumulated CPU time (s) 217.41 Current children cumulated vsize (Kb) 213888 [startup+230.022 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 63356 0 0 0 19155 269 0 0 25 0 1 0 1854787492 211374080 51065 4294967295 134512640 135167914 3221224448 3219870144 134844703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 51605 51065 162 162 0 51443 0 [pid=26320] vsize: 206420 Current children cumulated CPU time (s) 227.14 Current children cumulated vsize (Kb) 208548 [startup+240.023 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 67807 0 0 0 20099 295 0 0 25 0 1 0 1854787492 229605376 55516 4294967295 134512640 135167914 3221224448 3219881264 134693570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 56056 55516 162 162 0 55894 0 [pid=26320] vsize: 224224 Current children cumulated CPU time (s) 236.84 Current children cumulated vsize (Kb) 226352 [startup+250.024 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 72330 0 0 0 21045 316 0 0 19 0 1 0 1854787492 248131584 60039 4294967295 134512640 135167914 3221224448 3219870848 134694419 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 60579 60039 162 162 0 60417 0 [pid=26320] vsize: 242316 Current children cumulated CPU time (s) 246.51 Current children cumulated vsize (Kb) 244444 [startup+260.025 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 76870 0 0 0 21996 338 0 0 25 0 1 0 1854787492 266727424 64579 4294967295 134512640 135167914 3221224448 3219869564 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26320/statm): 65119 64579 162 162 0 64957 0 [pid=26320] vsize: 260476 Current children cumulated CPU time (s) 256.24 Current children cumulated vsize (Kb) 262604 [startup+270.025 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 81437 0 0 0 22942 360 0 0 25 0 1 0 1854787492 285433856 69146 4294967295 134512640 135167914 3221224448 3219868316 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26320/statm): 69686 69146 162 162 0 69524 0 [pid=26320] vsize: 278744 Current children cumulated CPU time (s) 265.92 Current children cumulated vsize (Kb) 280872 [startup+280.026 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 86029 0 0 0 23893 381 0 0 19 0 1 0 1854787492 304242688 73738 4294967295 134512640 135167914 3221224448 3219875380 134697403 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 74278 73738 162 162 0 74116 0 [pid=26320] vsize: 297112 Current children cumulated CPU time (s) 275.64 Current children cumulated vsize (Kb) 299240 [startup+290.027 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 90601 0 0 0 24841 402 0 0 25 0 1 0 1854787492 322969600 78310 4294967295 134512640 135167914 3221224448 3219870528 134621365 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 78850 78310 162 162 0 78688 0 [pid=26320] vsize: 315400 Current children cumulated CPU time (s) 285.33 Current children cumulated vsize (Kb) 317528 [startup+300.028 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 112532 0 0 0 25785 453 0 0 25 0 1 0 1854787492 369602560 89695 4294967295 134512640 135167914 3221224448 3219979900 134934490 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 90235 89695 162 162 0 90073 0 [pid=26320] vsize: 360940 Current children cumulated CPU time (s) 295.28 Current children cumulated vsize (Kb) 363068 [startup+310.029 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 116535 0 0 0 26733 475 0 0 25 0 1 0 1854787492 385998848 93698 4294967295 134512640 135167914 3221224448 3219970044 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/26320/statm): 94238 93698 162 162 0 94076 0 [pid=26320] vsize: 376952 Current children cumulated CPU time (s) 304.98 Current children cumulated vsize (Kb) 379080 [startup+320.029 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 120996 0 0 0 27687 494 0 0 25 0 1 0 1854787492 404271104 98159 4294967295 134512640 135167914 3221224448 3219879164 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 98699 98159 162 162 0 98537 0 [pid=26320] vsize: 394796 Current children cumulated CPU time (s) 314.71 Current children cumulated vsize (Kb) 396924 [startup+330.03 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 125492 0 0 0 28634 519 0 0 25 0 1 0 1854787492 422690816 102655 4294967295 134512640 135167914 3221224448 3219870608 134845442 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 103196 102655 162 162 0 103034 0 [pid=26320] vsize: 412784 Current children cumulated CPU time (s) 324.43 Current children cumulated vsize (Kb) 414912 [startup+340.03 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 129954 0 0 0 29584 542 0 0 25 0 1 0 1854787492 440963072 107117 4294967295 134512640 135167914 3221224448 3219896168 134846971 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 107657 107117 162 162 0 107495 0 [pid=26320] vsize: 430628 Current children cumulated CPU time (s) 334.16 Current children cumulated vsize (Kb) 432756 [startup+350.031 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 134440 0 0 0 30533 563 0 0 25 0 1 0 1854787492 459337728 111603 4294967295 134512640 135167914 3221224448 3219890432 134843113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 112143 111603 162 162 0 111981 0 [pid=26320] vsize: 448572 Current children cumulated CPU time (s) 343.86 Current children cumulated vsize (Kb) 450700 [startup+360.032 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 138907 0 0 0 31482 585 0 0 25 0 1 0 1854787492 477634560 116070 4294967295 134512640 135167914 3221224448 3219881368 134849258 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 116610 116070 162 162 0 116448 0 [pid=26320] vsize: 466440 Current children cumulated CPU time (s) 353.57 Current children cumulated vsize (Kb) 468568 [startup+370.032 s] Raw data (loadavg): 0.99 0.97 0.94 1/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 143358 0 0 0 32430 608 0 0 25 0 1 0 1854787492 495865856 120521 4294967295 134512640 135167914 3221224448 3219869164 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26320/statm): 121061 120521 162 162 0 120899 0 [pid=26320] vsize: 484244 Current children cumulated CPU time (s) 363.28 Current children cumulated vsize (Kb) 486372 [startup+380.033 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 147793 0 0 0 33380 628 0 0 25 0 1 0 1854787492 514031616 124956 4294967295 134512640 135167914 3221224448 3219869920 134844668 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 125496 124956 162 162 0 125334 0 [pid=26320] vsize: 501984 Current children cumulated CPU time (s) 372.98 Current children cumulated vsize (Kb) 504112 [startup+390.034 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 152221 0 0 0 34329 649 0 0 19 0 1 0 1854787492 532168704 129384 4294967295 134512640 135167914 3221224448 3219897396 134619959 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 129924 129384 162 162 0 129762 0 [pid=26320] vsize: 519696 Current children cumulated CPU time (s) 382.68 Current children cumulated vsize (Kb) 521824 [startup+400.036 s] Raw data (loadavg): 0.99 0.97 0.94 1/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 156696 0 0 0 35280 670 0 0 25 0 1 0 1854787492 550498304 133859 4294967295 134512640 135167914 3221224448 3219867868 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26320/statm): 134399 133859 162 162 0 134237 0 [pid=26320] vsize: 537596 Current children cumulated CPU time (s) 392.4 Current children cumulated vsize (Kb) 539724 [startup+410.037 s] Raw data (loadavg): 0.99 0.97 0.94 1/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 161208 0 0 0 36231 690 0 0 25 0 1 0 1854787492 568979456 138371 4294967295 134512640 135167914 3221224448 3219872060 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26320/statm): 138911 138371 162 162 0 138749 0 [pid=26320] vsize: 555644 Current children cumulated CPU time (s) 402.11 Current children cumulated vsize (Kb) 557772 [startup+420.037 s] Raw data (loadavg): 0.99 0.97 0.94 1/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 165786 0 0 0 37179 711 0 0 25 0 1 0 1854787492 587730944 142949 4294967295 134512640 135167914 3221224448 3219879324 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26320/statm): 143489 142949 162 162 0 143327 0 [pid=26320] vsize: 573956 Current children cumulated CPU time (s) 411.8 Current children cumulated vsize (Kb) 576084 [startup+430.038 s] Raw data (loadavg): 0.99 0.97 0.94 1/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 170348 0 0 0 38127 734 0 0 25 0 1 0 1854787492 606416896 147511 4294967295 134512640 135167914 3221224448 3219866748 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/26320/statm): 148051 147511 162 162 0 147889 0 [pid=26320] vsize: 592204 Current children cumulated CPU time (s) 421.51 Current children cumulated vsize (Kb) 594332 [startup+440.039 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 174297 0 0 0 39080 755 0 0 25 0 1 0 1854787492 622592000 151460 4294967295 134512640 135167914 3221224448 3219965060 134620508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 152000 151460 162 162 0 151838 0 [pid=26320] vsize: 608000 Current children cumulated CPU time (s) 431.25 Current children cumulated vsize (Kb) 610128 [startup+450.04 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 218074 0 0 0 39964 858 0 0 25 0 1 0 1854787492 801902592 195237 4294967295 134512640 135167914 3221224448 3220053040 134694392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 195777 195237 162 162 0 195615 0 [pid=26320] vsize: 783108 Current children cumulated CPU time (s) 441.12 Current children cumulated vsize (Kb) 785236 [startup+460.041 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 218074 0 0 0 40964 858 0 0 25 0 1 0 1854787492 801902592 195237 4294967295 134512640 135167914 3221224448 3220053088 134625423 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 195777 195237 162 162 0 195615 0 [pid=26320] vsize: 783108 Current children cumulated CPU time (s) 451.12 Current children cumulated vsize (Kb) 785236 [startup+470.042 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 222426 0 0 0 41909 884 0 0 25 0 1 0 1854787492 733339648 178498 4294967295 134512640 135167914 3221224448 3219869344 134522502 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 179038 178498 162 162 0 178876 0 [pid=26320] vsize: 716152 Current children cumulated CPU time (s) 460.83 Current children cumulated vsize (Kb) 718280 [startup+480.043 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 226876 0 0 0 42853 908 0 0 25 0 1 0 1854787492 751566848 182948 4294967295 134512640 135167914 3221224448 3219890800 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 183488 182948 162 162 0 183326 0 [pid=26320] vsize: 733952 Current children cumulated CPU time (s) 470.51 Current children cumulated vsize (Kb) 736080 [startup+490.043 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 231344 0 0 0 43803 927 0 0 25 0 1 0 1854787492 769867776 187416 4294967295 134512640 135167914 3221224448 3219915996 134619797 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 187956 187416 162 162 0 187794 0 [pid=26320] vsize: 751824 Current children cumulated CPU time (s) 480.2 Current children cumulated vsize (Kb) 753952 [startup+500.044 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 235806 0 0 0 44754 948 0 0 25 0 1 0 1854787492 788144128 191878 4294967295 134512640 135167914 3221224448 3219866476 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26320/statm): 192418 191878 162 162 0 192256 0 [pid=26320] vsize: 769672 Current children cumulated CPU time (s) 489.92 Current children cumulated vsize (Kb) 771800 [startup+510.045 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 240187 0 0 0 45706 967 0 0 25 0 1 0 1854787492 806088704 196259 4294967295 134512640 135167914 3221224448 3219875852 134845882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 196799 196259 162 162 0 196637 0 [pid=26320] vsize: 787196 Current children cumulated CPU time (s) 499.63 Current children cumulated vsize (Kb) 789324 [startup+520.045 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 244571 0 0 0 46657 990 0 0 25 0 1 0 1854787492 824045568 200643 4294967295 134512640 135167914 3221224448 3219913040 134722521 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 201183 200643 162 162 0 201021 0 [pid=26320] vsize: 804732 Current children cumulated CPU time (s) 509.37 Current children cumulated vsize (Kb) 806860 [startup+530.046 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 248995 0 0 0 47603 1014 0 0 25 0 1 0 1854787492 842166272 205067 4294967295 134512640 135167914 3221224448 3219868992 134843026 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 205607 205067 162 162 0 205445 0 [pid=26320] vsize: 822428 Current children cumulated CPU time (s) 519.07 Current children cumulated vsize (Kb) 824556 [startup+540.046 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 253481 0 0 0 48552 1034 0 0 25 0 1 0 1854787492 860540928 209553 4294967295 134512640 135167914 3221224448 3219907248 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 210093 209553 162 162 0 209931 0 [pid=26320] vsize: 840372 Current children cumulated CPU time (s) 528.76 Current children cumulated vsize (Kb) 842500 [startup+550.047 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 258003 0 0 0 49501 1057 0 0 25 0 1 0 1854787492 879063040 214075 4294967295 134512640 135167914 3221224448 3219867584 134694405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 214615 214075 162 162 0 214453 0 [pid=26320] vsize: 858460 Current children cumulated CPU time (s) 538.48 Current children cumulated vsize (Kb) 860588 [startup+560.048 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 262515 0 0 0 50444 1080 0 0 25 0 1 0 1854787492 897544192 218587 4294967295 134512640 135167914 3221224448 3219901660 134693552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26320/statm): 219127 218587 162 162 0 218965 0 [pid=26320] vsize: 876508 Current children cumulated CPU time (s) 548.14 Current children cumulated vsize (Kb) 878636 [startup+570.049 s] Raw data (loadavg): 0.99 0.97 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 267069 0 1 0 51395 1099 0 0 25 0 1 0 1854787492 916045824 222990 4294967295 134512640 135167914 3221224448 3219867260 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26320/statm): 223644 222990 162 162 0 223482 0 [pid=26320] vsize: 894576 Current children cumulated CPU time (s) 557.84 Current children cumulated vsize (Kb) 896704 [startup+580.05 s] Raw data (loadavg): 1.07 0.99 0.94 2/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) R 26315 26315 4419 0 -1 0 271095 0 162 0 52153 1123 0 0 18 0 1 0 1854787492 930910208 225321 4294967295 134512640 135167914 3221224448 3219869600 134694405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26320/statm): 227273 225321 162 162 0 227111 0 [pid=26320] vsize: 909092 Current children cumulated CPU time (s) 565.66 Current children cumulated vsize (Kb) 911220 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+588.796 s] Raw data (loadavg): 1.06 0.99 0.94 1/57 26320 Raw data (/proc/26315/stat): 26315 (minisat+_script) S 26314 26315 4419 0 -1 0 314 1557 0 0 0 1 3277 12 19 0 1 0 1854784185 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26315/statm): 532 234 485 147 0 385 0 [pid=26315] vsize: 2128 Raw data (/proc/26320/stat): 26320 (minisat+_bignum) T 26315 26315 4419 0 -1 0 274379 0 407 0 52687 1145 0 0 19 0 1 0 1854787492 941543424 227408 4294967295 134512640 135167914 3221224448 3219868540 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/26320/statm): 229869 227408 162 162 0 229707 0 [pid=26320] vsize: 919476 Current children cumulated CPU time (s) 571.22 Current children cumulated vsize (Kb) 921604 Sending SIGTERM to -26315 Sleeping 2 seconds One traced child (pid=26315) ended because it received signal 15 (SIGTERM) One traced child (pid=26320) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 589.226 CPU time (s): 538.755 CPU user time (s): 526.876 CPU system time (s): 11.8792 CPU usage (%): 91.4344 Max. virtual memory (cumulated for all children) (Kb): 921604
ERROR: no interpretation found !