Name | submitted/manquinho/logic-synthesis/normalized-f51m.b.opb |
MD5SUM | 4fc22abde8250807abd95442a25fac44 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 18 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 407 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 407 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 407 |
Number of bits of the biggest sum of numbers | 9 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 99.3649 |
Number of variables | 406 |
Total number of constraints | 538 |
Number of constraints which are clauses | 520 |
Number of constraints which are cardinality constraints (but not clauses) | 18 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 123 |
LAUNCH ON wulflinc8 THE 2005-09-18 12:44:48 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2411 boxname=wulflinc8 idbench=67 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4fc22abde8250807abd95442a25fac44 /oldhome/oroussel/tmp/wulflinc8/normalized-f51m.b.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-f51m.b.opb IDLAUNCH: 2411 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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 : 2 cpu MHz : 451.007 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: 946448 kB Buffers: 33752 kB Cached: 29784 kB SwapCached: 792 kB Active: 53964 kB Inactive: 12276 kB HighTotal: 131008 kB HighFree: 97412 kB LowTotal: 903652 kB LowFree: 849036 kB SwapTotal: 2097136 kB SwapFree: 2095876 kB Dirty: 32 kB Writeback: 0 kB Mapped: 5752 kB Slab: 16380 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 13:04:58 (client local time) WITH STATUS 10 IN 1209.94 SECONDS stats: 2411 7 1209.94 10
c Parsing PB file... c Converting 498 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................. c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 498 13351 | 166 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 26[0m c ---[ 0]---> Sorter-cost:14920 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1 | 16604 50904 | 5534 1 18 18.0 | 0.000 % | c | 101 | 16604 50904 | 6087 101 2898 28.7 | 0.055 % | c ============================================================================== c [1mFound solution: 21[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 208 | 16615 50935 | 5538 187 12825 68.6 | 0.055 % | c | 309 | 16615 50935 | 6091 288 21975 76.3 | 0.192 % | c | 459 | 16615 50935 | 6700 438 33909 77.4 | 0.192 % | c | 686 | 16615 50935 | 7371 665 58415 87.8 | 0.192 % | c | 1029 | 16615 50935 | 8108 1008 95310 94.6 | 0.192 % | c | 1536 | 16615 50935 | 8919 1515 138105 91.2 | 0.192 % | c ============================================================================== c [1mFound solution: 19[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1913 | 16410 50460 | 5470 1862 174770 93.9 | 0.192 % | c | 2013 | 16410 50460 | 6017 1962 183811 93.7 | 1.618 % | c | 2163 | 16402 50444 | 6618 2111 189584 89.8 | 1.655 % | c | 2388 | 16402 50444 | 7280 2336 201318 86.2 | 1.655 % | c | 2726 | 16402 50444 | 8008 2674 217793 81.4 | 1.655 % | c | 3232 | 16402 50444 | 8809 3180 247166 77.7 | 1.655 % | c | 3992 | 16402 50444 | 9690 3940 279064 70.8 | 1.655 % | c | 5131 | 16402 50444 | 10659 5079 327949 64.6 | 1.655 % | c | 6839 | 16402 50444 | 11725 6787 409251 60.3 | 1.655 % | c | 9401 | 16402 50444 | 12897 9349 513437 54.9 | 1.655 % | c | 13245 | 16402 50444 | 14187 13193 698978 53.0 | 1.655 % | c | 19011 | 16402 50444 | 15606 11519 497107 43.2 | 1.655 % | c | 27660 | 16402 50444 | 17167 12053 609989 50.6 | 1.655 % | c ============================================================================== c [1mFound solution: 18[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 33376 | 16414 50475 | 5471 17769 928999 52.3 | 1.655 % | c | 33478 | 16414 50475 | 6018 4545 221744 48.8 | 1.663 % | c | 33628 | 16414 50475 | 6619 4695 229759 48.9 | 1.663 % | c | 33855 | 16414 50475 | 7281 4922 240660 48.9 | 1.663 % | c | 34192 | 16414 50475 | 8010 5259 254469 48.4 | 1.663 % | c | 34700 | 16414 50475 | 8811 5767 274708 47.6 | 1.663 % | c | 35461 | 16414 50475 | 9692 6528 308203 47.2 | 1.663 % | c | 36601 | 16414 50475 | 10661 7668 361716 47.2 | 1.663 % | c | 38309 | 16414 50475 | 11727 9376 425326 45.4 | 1.663 % | c | 40871 | 16414 50475 | 12900 11938 539786 45.2 | 1.663 % | c | 44717 | 16414 50475 | 14190 9168 330073 36.0 | 1.663 % | c | 50487 | 16414 50475 | 15609 7682 245410 31.9 | 1.663 % | c | 59136 | 16414 50475 | 17170 8283 287557 34.7 | 1.663 % | c | 72111 | 16414 50475 | 18887 12406 433973 35.0 | 1.663 % | c | 91574 | 16414 50475 | 20776 12488 450296 36.1 | 1.663 % | c | 120768 | 16414 50475 | 22853 20303 750005 36.9 | 1.663 % | c | 164558 | 16414 50475 | 25139 17290 577512 33.4 | 1.663 % | c | 230246 | 16414 50475 | 27653 18531 543896 29.4 | 1.663 % | c | 328772 | 16414 50475 | 30418 14118 592755 42.0 | 1.663 % | c | 476561 | 16414 50475 | 33460 30736 1029565 33.5 | 1.663 % |
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/29832/stat): 29832 (minisat+_script) R 29831 29832 27660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1769561544 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/29832/statm): 174 3 169 147 0 27 0 [pid=29832] 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=29833 New process pid=29834 New process pid=29835 execve syscall for /bin/sed executable One traced child (pid=29834) 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=29835) exited with status: 0 One traced child (pid=29833) exited with status: 0 New process pid=29836 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-f51m.b.opb [startup+10.0042 s] Raw data (loadavg): 0.94 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 1440 0 0 0 980 7 0 0 25 0 1 0 1769561549 6647808 1423 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 1623 1423 145 145 0 1478 0 [pid=29836] vsize: 6492 Current children cumulated CPU time (s) 9.89 Current children cumulated vsize (Kb) 8616 [startup+20.005 s] Raw data (loadavg): 0.95 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) T 29832 29832 27660 0 -1 0 1708 0 0 0 1975 9 0 0 25 0 1 0 1769561549 7766016 1691 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/29836/statm): 1896 1691 145 145 0 1751 0 [pid=29836] vsize: 7584 Current children cumulated CPU time (s) 19.86 Current children cumulated vsize (Kb) 9708 [startup+30.0068 s] Raw data (loadavg): 0.95 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 1979 0 0 0 2969 11 0 0 25 0 1 0 1769561549 8867840 1962 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2165 1962 145 145 0 2020 0 [pid=29836] vsize: 8660 Current children cumulated CPU time (s) 29.82 Current children cumulated vsize (Kb) 10784 [startup+40.0076 s] Raw data (loadavg): 0.96 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 1990 0 0 0 3969 11 0 0 25 0 1 0 1769561549 8937472 1973 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2182 1973 145 145 0 2037 0 [pid=29836] vsize: 8728 Current children cumulated CPU time (s) 39.82 Current children cumulated vsize (Kb) 10852 [startup+50.0094 s] Raw data (loadavg): 0.97 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2009 0 0 0 4969 11 0 0 25 0 1 0 1769561549 9031680 1992 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2205 1992 145 145 0 2060 0 [pid=29836] vsize: 8820 Current children cumulated CPU time (s) 49.82 Current children cumulated vsize (Kb) 10944 [startup+60.0102 s] Raw data (loadavg): 0.97 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2042 0 0 0 5969 12 0 0 25 0 1 0 1769561549 9162752 2025 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2237 2025 145 145 0 2092 0 [pid=29836] vsize: 8948 Current children cumulated CPU time (s) 59.83 Current children cumulated vsize (Kb) 11072 [startup+70.0109 s] Raw data (loadavg): 0.97 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2169 0 0 0 6967 13 0 0 25 0 1 0 1769561549 9682944 2152 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2364 2152 145 145 0 2219 0 [pid=29836] vsize: 9456 Current children cumulated CPU time (s) 69.82 Current children cumulated vsize (Kb) 11580 [startup+80.0117 s] Raw data (loadavg): 0.98 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2289 0 0 0 7965 14 0 0 25 0 1 0 1769561549 10235904 2272 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2499 2272 145 145 0 2354 0 [pid=29836] vsize: 9996 Current children cumulated CPU time (s) 79.81 Current children cumulated vsize (Kb) 12120 [startup+90.0125 s] Raw data (loadavg): 0.98 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2289 0 0 0 8965 14 0 0 25 0 1 0 1769561549 10235904 2272 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2499 2272 145 145 0 2354 0 [pid=29836] vsize: 9996 Current children cumulated CPU time (s) 89.81 Current children cumulated vsize (Kb) 12120 [startup+100.013 s] Raw data (loadavg): 0.98 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2289 0 0 0 9965 14 0 0 25 0 1 0 1769561549 10235904 2272 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2499 2272 145 145 0 2354 0 [pid=29836] vsize: 9996 Current children cumulated CPU time (s) 99.81 Current children cumulated vsize (Kb) 12120 [startup+110.014 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2289 0 0 0 10966 14 0 0 25 0 1 0 1769561549 10235904 2272 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2499 2272 145 145 0 2354 0 [pid=29836] vsize: 9996 Current children cumulated CPU time (s) 109.82 Current children cumulated vsize (Kb) 12120 [startup+120.015 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2293 0 0 0 11966 14 0 0 25 0 1 0 1769561549 10252288 2276 4294967295 134512640 135094434 3221224448 3221223072 134557691 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2503 2276 145 145 0 2358 0 [pid=29836] vsize: 10012 Current children cumulated CPU time (s) 119.82 Current children cumulated vsize (Kb) 12136 [startup+130.016 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2297 0 0 0 12966 14 0 0 25 0 1 0 1769561549 10268672 2280 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2507 2280 145 145 0 2362 0 [pid=29836] vsize: 10028 Current children cumulated CPU time (s) 129.82 Current children cumulated vsize (Kb) 12152 [startup+140.016 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2304 0 0 0 13966 14 0 0 25 0 1 0 1769561549 10301440 2287 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2515 2287 145 145 0 2370 0 [pid=29836] vsize: 10060 Current children cumulated CPU time (s) 139.82 Current children cumulated vsize (Kb) 12184 [startup+150.018 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2304 0 0 0 14967 14 0 0 25 0 1 0 1769561549 10301440 2287 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2515 2287 145 145 0 2370 0 [pid=29836] vsize: 10060 Current children cumulated CPU time (s) 149.83 Current children cumulated vsize (Kb) 12184 [startup+160.019 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2343 0 0 0 15966 14 0 0 25 0 1 0 1769561549 10547200 2326 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2575 2326 145 145 0 2430 0 [pid=29836] vsize: 10300 Current children cumulated CPU time (s) 159.82 Current children cumulated vsize (Kb) 12424 [startup+170.019 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2344 0 0 0 16966 14 0 0 25 0 1 0 1769561549 10547200 2327 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2575 2327 145 145 0 2430 0 [pid=29836] vsize: 10300 Current children cumulated CPU time (s) 169.82 Current children cumulated vsize (Kb) 12424 [startup+180.02 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2344 0 0 0 17966 15 0 0 25 0 1 0 1769561549 10547200 2327 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29836/statm): 2575 2327 145 145 0 2430 0 [pid=29836] vsize: 10300 Current children cumulated CPU time (s) 179.83 Current children cumulated vsize (Kb) 12424 [startup+190.021 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2349 0 0 0 18965 16 0 0 25 0 1 0 1769561549 10563584 2332 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29836/statm): 2579 2332 145 145 0 2434 0 [pid=29836] vsize: 10316 Current children cumulated CPU time (s) 189.83 Current children cumulated vsize (Kb) 12440 [startup+200.021 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2359 0 0 0 19964 16 0 0 25 0 1 0 1769561549 10612736 2342 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29836/statm): 2591 2342 145 145 0 2446 0 [pid=29836] vsize: 10364 Current children cumulated CPU time (s) 199.82 Current children cumulated vsize (Kb) 12488 [startup+210.022 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2391 0 0 0 20963 17 0 0 25 0 1 0 1769561549 10752000 2374 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29836/statm): 2625 2374 145 145 0 2480 0 [pid=29836] vsize: 10500 Current children cumulated CPU time (s) 209.82 Current children cumulated vsize (Kb) 12624 [startup+220.023 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2439 0 0 0 21962 18 0 0 25 0 1 0 1769561549 10956800 2422 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29836/statm): 2675 2422 145 145 0 2530 0 [pid=29836] vsize: 10700 Current children cumulated CPU time (s) 219.82 Current children cumulated vsize (Kb) 12824 [startup+230.024 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2451 0 0 0 22962 18 0 0 25 0 1 0 1769561549 11005952 2434 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29836/statm): 2687 2434 145 145 0 2542 0 [pid=29836] vsize: 10748 Current children cumulated CPU time (s) 229.82 Current children cumulated vsize (Kb) 12872 [startup+240.024 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2456 0 0 0 23962 18 0 0 25 0 1 0 1769561549 11071488 2439 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2703 2439 145 145 0 2558 0 [pid=29836] vsize: 10812 Current children cumulated CPU time (s) 239.82 Current children cumulated vsize (Kb) 12936 [startup+250.024 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2474 0 0 0 24962 19 0 0 25 0 1 0 1769561549 11120640 2457 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2715 2457 145 145 0 2570 0 [pid=29836] vsize: 10860 Current children cumulated CPU time (s) 249.83 Current children cumulated vsize (Kb) 12984 [startup+260.025 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2476 0 0 0 25962 19 0 0 25 0 1 0 1769561549 11120640 2459 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2715 2459 145 145 0 2570 0 [pid=29836] vsize: 10860 Current children cumulated CPU time (s) 259.83 Current children cumulated vsize (Kb) 12984 [startup+270.026 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2484 0 0 0 26962 19 0 0 25 0 1 0 1769561549 11153408 2467 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2723 2467 145 145 0 2578 0 [pid=29836] vsize: 10892 Current children cumulated CPU time (s) 269.83 Current children cumulated vsize (Kb) 13016 [startup+280.026 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2484 0 0 0 27963 19 0 0 25 0 1 0 1769561549 11153408 2467 4294967295 134512640 135094434 3221224448 3221223104 134558292 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2723 2467 145 145 0 2578 0 [pid=29836] vsize: 10892 Current children cumulated CPU time (s) 279.84 Current children cumulated vsize (Kb) 13016 [startup+290.027 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2484 0 0 0 28963 19 0 0 25 0 1 0 1769561549 11153408 2467 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2723 2467 145 145 0 2578 0 [pid=29836] vsize: 10892 Current children cumulated CPU time (s) 289.84 Current children cumulated vsize (Kb) 13016 [startup+300.027 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2503 0 0 0 29963 19 0 0 25 0 1 0 1769561549 11235328 2486 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2743 2486 145 145 0 2598 0 [pid=29836] vsize: 10972 Current children cumulated CPU time (s) 299.84 Current children cumulated vsize (Kb) 13096 [startup+310.028 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2569 0 0 0 30961 20 0 0 25 0 1 0 1769561549 11493376 2552 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2806 2552 145 145 0 2661 0 [pid=29836] vsize: 11224 Current children cumulated CPU time (s) 309.83 Current children cumulated vsize (Kb) 13348 [startup+320.029 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2587 0 0 0 31961 20 0 0 25 0 1 0 1769561549 11591680 2570 4294967295 134512640 135094434 3221224448 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2830 2570 145 145 0 2685 0 [pid=29836] vsize: 11320 Current children cumulated CPU time (s) 319.83 Current children cumulated vsize (Kb) 13444 [startup+330.029 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2601 0 0 0 32961 20 0 0 25 0 1 0 1769561549 11689984 2584 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2854 2584 145 145 0 2709 0 [pid=29836] vsize: 11416 Current children cumulated CPU time (s) 329.83 Current children cumulated vsize (Kb) 13540 [startup+340.03 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2614 0 0 0 33961 20 0 0 25 0 1 0 1769561549 11722752 2597 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2862 2597 145 145 0 2717 0 [pid=29836] vsize: 11448 Current children cumulated CPU time (s) 339.83 Current children cumulated vsize (Kb) 13572 [startup+350.03 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2614 0 0 0 34962 20 0 0 25 0 1 0 1769561549 11722752 2597 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2862 2597 145 145 0 2717 0 [pid=29836] vsize: 11448 Current children cumulated CPU time (s) 349.84 Current children cumulated vsize (Kb) 13572 [startup+360.032 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2620 0 0 0 35962 20 0 0 25 0 1 0 1769561549 11755520 2603 4294967295 134512640 135094434 3221224448 3221223136 134554676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2870 2603 145 145 0 2725 0 [pid=29836] vsize: 11480 Current children cumulated CPU time (s) 359.84 Current children cumulated vsize (Kb) 13604 [startup+370.032 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2620 0 0 0 36962 20 0 0 25 0 1 0 1769561549 11755520 2603 4294967295 134512640 135094434 3221224448 3221223060 134563134 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2870 2603 145 145 0 2725 0 [pid=29836] vsize: 11480 Current children cumulated CPU time (s) 369.84 Current children cumulated vsize (Kb) 13604 [startup+380.033 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2620 0 0 0 37962 20 0 0 25 0 1 0 1769561549 11755520 2603 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2870 2603 145 145 0 2725 0 [pid=29836] vsize: 11480 Current children cumulated CPU time (s) 379.84 Current children cumulated vsize (Kb) 13604 [startup+390.034 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2641 0 0 0 38962 20 0 0 25 0 1 0 1769561549 11886592 2624 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2902 2624 145 145 0 2757 0 [pid=29836] vsize: 11608 Current children cumulated CPU time (s) 389.84 Current children cumulated vsize (Kb) 13732 [startup+400.035 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2651 0 0 0 39962 21 0 0 25 0 1 0 1769561549 11948032 2634 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2917 2634 145 145 0 2772 0 [pid=29836] vsize: 11668 Current children cumulated CPU time (s) 399.85 Current children cumulated vsize (Kb) 13792 [startup+410.036 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2658 0 0 0 40963 21 0 0 25 0 1 0 1769561549 11964416 2641 4294967295 134512640 135094434 3221224448 3221223136 134554728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2921 2641 145 145 0 2776 0 [pid=29836] vsize: 11684 Current children cumulated CPU time (s) 409.86 Current children cumulated vsize (Kb) 13808 [startup+420.036 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2661 0 0 0 41963 21 0 0 25 0 1 0 1769561549 12029952 2644 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2937 2644 145 145 0 2792 0 [pid=29836] vsize: 11748 Current children cumulated CPU time (s) 419.86 Current children cumulated vsize (Kb) 13872 [startup+430.038 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2698 0 0 0 42963 21 0 0 25 0 1 0 1769561549 12165120 2681 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2970 2681 145 145 0 2825 0 [pid=29836] vsize: 11880 Current children cumulated CPU time (s) 429.86 Current children cumulated vsize (Kb) 14004 [startup+440.039 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2698 0 0 0 43963 21 0 0 25 0 1 0 1769561549 12165120 2681 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2970 2681 145 145 0 2825 0 [pid=29836] vsize: 11880 Current children cumulated CPU time (s) 439.86 Current children cumulated vsize (Kb) 14004 [startup+450.04 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2709 0 0 0 44963 21 0 0 25 0 1 0 1769561549 12214272 2692 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2982 2692 145 145 0 2837 0 [pid=29836] vsize: 11928 Current children cumulated CPU time (s) 449.86 Current children cumulated vsize (Kb) 14052 [startup+460.041 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2710 0 0 0 45964 21 0 0 25 0 1 0 1769561549 12214272 2693 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 2982 2693 145 145 0 2837 0 [pid=29836] vsize: 11928 Current children cumulated CPU time (s) 459.87 Current children cumulated vsize (Kb) 14052 [startup+470.04 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2747 0 0 0 46963 21 0 0 25 0 1 0 1769561549 12378112 2730 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3022 2730 145 145 0 2877 0 [pid=29836] vsize: 12088 Current children cumulated CPU time (s) 469.86 Current children cumulated vsize (Kb) 14212 [startup+480.042 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2747 0 0 0 47963 21 0 0 25 0 1 0 1769561549 12378112 2730 4294967295 134512640 135094434 3221224448 3221223072 134557722 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3022 2730 145 145 0 2877 0 [pid=29836] vsize: 12088 Current children cumulated CPU time (s) 479.86 Current children cumulated vsize (Kb) 14212 [startup+490.043 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2755 0 0 0 48964 21 0 0 25 0 1 0 1769561549 12410880 2738 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3030 2738 145 145 0 2885 0 [pid=29836] vsize: 12120 Current children cumulated CPU time (s) 489.87 Current children cumulated vsize (Kb) 14244 [startup+500.044 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2762 0 0 0 49964 21 0 0 25 0 1 0 1769561549 12443648 2745 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3038 2745 145 145 0 2893 0 [pid=29836] vsize: 12152 Current children cumulated CPU time (s) 499.87 Current children cumulated vsize (Kb) 14276 [startup+510.044 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2762 0 0 0 50964 21 0 0 25 0 1 0 1769561549 12443648 2745 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3038 2745 145 145 0 2893 0 [pid=29836] vsize: 12152 Current children cumulated CPU time (s) 509.87 Current children cumulated vsize (Kb) 14276 [startup+520.045 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2767 0 0 0 51964 21 0 0 25 0 1 0 1769561549 12476416 2750 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3046 2750 145 145 0 2901 0 [pid=29836] vsize: 12184 Current children cumulated CPU time (s) 519.87 Current children cumulated vsize (Kb) 14308 [startup+530.046 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2778 0 0 0 52964 22 0 0 25 0 1 0 1769561549 12525568 2761 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3058 2761 145 145 0 2913 0 [pid=29836] vsize: 12232 Current children cumulated CPU time (s) 529.88 Current children cumulated vsize (Kb) 14356 [startup+540.047 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2778 0 0 0 53964 22 0 0 25 0 1 0 1769561549 12525568 2761 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3058 2761 145 145 0 2913 0 [pid=29836] vsize: 12232 Current children cumulated CPU time (s) 539.88 Current children cumulated vsize (Kb) 14356 [startup+550.048 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2784 0 0 0 54965 22 0 0 25 0 1 0 1769561549 12558336 2767 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3066 2767 145 145 0 2921 0 [pid=29836] vsize: 12264 Current children cumulated CPU time (s) 549.89 Current children cumulated vsize (Kb) 14388 [startup+560.048 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2792 0 0 0 55965 22 0 0 25 0 1 0 1769561549 12591104 2775 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3074 2775 145 145 0 2929 0 [pid=29836] vsize: 12296 Current children cumulated CPU time (s) 559.89 Current children cumulated vsize (Kb) 14420 [startup+570.049 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2793 0 0 0 56965 22 0 0 25 0 1 0 1769561549 12591104 2776 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3074 2776 145 145 0 2929 0 [pid=29836] vsize: 12296 Current children cumulated CPU time (s) 569.89 Current children cumulated vsize (Kb) 14420 [startup+580.05 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2807 0 0 0 57964 22 0 0 25 0 1 0 1769561549 12656640 2790 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29836/statm): 3090 2790 145 145 0 2945 0 [pid=29836] vsize: 12360 Current children cumulated CPU time (s) 579.88 Current children cumulated vsize (Kb) 14484 [startup+590.051 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2809 0 0 0 58964 22 0 0 25 0 1 0 1769561549 12656640 2792 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3090 2792 145 145 0 2945 0 [pid=29836] vsize: 12360 Current children cumulated CPU time (s) 589.88 Current children cumulated vsize (Kb) 14484 [startup+600.052 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2828 0 0 0 59964 22 0 0 25 0 1 0 1769561549 12754944 2811 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3114 2811 145 145 0 2969 0 [pid=29836] vsize: 12456 Current children cumulated CPU time (s) 599.88 Current children cumulated vsize (Kb) 14580 [startup+610.052 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2829 0 0 0 60963 22 0 0 25 0 1 0 1769561549 12754944 2812 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3114 2812 145 145 0 2969 0 [pid=29836] vsize: 12456 Current children cumulated CPU time (s) 609.87 Current children cumulated vsize (Kb) 14580 [startup+620.052 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2850 0 0 0 61964 22 0 0 25 0 1 0 1769561549 12886016 2833 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3146 2833 145 145 0 3001 0 [pid=29836] vsize: 12584 Current children cumulated CPU time (s) 619.88 Current children cumulated vsize (Kb) 14708 [startup+630.053 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2864 0 0 0 62964 23 0 0 25 0 1 0 1769561549 12951552 2847 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3162 2847 145 145 0 3017 0 [pid=29836] vsize: 12648 Current children cumulated CPU time (s) 629.89 Current children cumulated vsize (Kb) 14772 [startup+640.054 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2865 0 0 0 63964 23 0 0 25 0 1 0 1769561549 12951552 2848 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3162 2848 145 145 0 3017 0 [pid=29836] vsize: 12648 Current children cumulated CPU time (s) 639.89 Current children cumulated vsize (Kb) 14772 [startup+650.053 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2865 0 0 0 64964 23 0 0 25 0 1 0 1769561549 12951552 2848 4294967295 134512640 135094434 3221224448 3221223136 134554763 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3162 2848 145 145 0 3017 0 [pid=29836] vsize: 12648 Current children cumulated CPU time (s) 649.89 Current children cumulated vsize (Kb) 14772 [startup+660.054 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2874 0 0 0 65964 23 0 0 25 0 1 0 1769561549 13017088 2857 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3178 2857 145 145 0 3033 0 [pid=29836] vsize: 12712 Current children cumulated CPU time (s) 659.89 Current children cumulated vsize (Kb) 14836 [startup+670.055 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2877 0 0 0 66964 23 0 0 25 0 1 0 1769561549 13017088 2860 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3178 2860 145 145 0 3033 0 [pid=29836] vsize: 12712 Current children cumulated CPU time (s) 669.89 Current children cumulated vsize (Kb) 14836 [startup+680.056 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2879 0 0 0 67965 23 0 0 25 0 1 0 1769561549 13017088 2862 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3178 2862 145 145 0 3033 0 [pid=29836] vsize: 12712 Current children cumulated CPU time (s) 679.9 Current children cumulated vsize (Kb) 14836 [startup+690.057 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2880 0 0 0 68965 23 0 0 25 0 1 0 1769561549 13017088 2863 4294967295 134512640 135094434 3221224448 3221223100 134562036 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3178 2863 145 145 0 3033 0 [pid=29836] vsize: 12712 Current children cumulated CPU time (s) 689.9 Current children cumulated vsize (Kb) 14836 [startup+700.057 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 69965 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0 [pid=29836] vsize: 12712 Current children cumulated CPU time (s) 699.9 Current children cumulated vsize (Kb) 14836 [startup+710.058 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 70965 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223104 134557815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0 [pid=29836] vsize: 12712 Current children cumulated CPU time (s) 709.9 Current children cumulated vsize (Kb) 14836 [startup+720.059 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 71966 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0 [pid=29836] vsize: 12712 Current children cumulated CPU time (s) 719.91 Current children cumulated vsize (Kb) 14836 [startup+730.06 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 72966 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223104 134558286 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0 [pid=29836] vsize: 12712 Current children cumulated CPU time (s) 729.91 Current children cumulated vsize (Kb) 14836 [startup+740.061 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 73966 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0 [pid=29836] vsize: 12712 Current children cumulated CPU time (s) 739.91 Current children cumulated vsize (Kb) 14836 [startup+750.061 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 74966 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0 [pid=29836] vsize: 12712 Current children cumulated CPU time (s) 749.91 Current children cumulated vsize (Kb) 14836 [startup+760.062 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 75966 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0 [pid=29836] vsize: 12712 Current children cumulated CPU time (s) 759.91 Current children cumulated vsize (Kb) 14836 [startup+770.062 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2881 0 0 0 76966 23 0 0 25 0 1 0 1769561549 13017088 2864 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3178 2864 145 145 0 3033 0 [pid=29836] vsize: 12712 Current children cumulated CPU time (s) 769.91 Current children cumulated vsize (Kb) 14836 [startup+780.064 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2898 0 0 0 77967 23 0 0 25 0 1 0 1769561549 13082624 2881 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3194 2881 145 145 0 3049 0 [pid=29836] vsize: 12776 Current children cumulated CPU time (s) 779.92 Current children cumulated vsize (Kb) 14900 [startup+790.064 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2985 0 0 0 78964 25 0 0 25 0 1 0 1769561549 13438976 2968 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3281 2968 145 145 0 3136 0 [pid=29836] vsize: 13124 Current children cumulated CPU time (s) 789.91 Current children cumulated vsize (Kb) 15248 [startup+800.064 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2998 0 0 0 79964 25 0 0 25 0 1 0 1769561549 13504512 2981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3297 2981 145 145 0 3152 0 [pid=29836] vsize: 13188 Current children cumulated CPU time (s) 799.91 Current children cumulated vsize (Kb) 15312 [startup+810.065 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 2998 0 0 0 80964 25 0 0 25 0 1 0 1769561549 13504512 2981 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3297 2981 145 145 0 3152 0 [pid=29836] vsize: 13188 Current children cumulated CPU time (s) 809.91 Current children cumulated vsize (Kb) 15312 [startup+820.066 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3062 0 0 0 81963 26 0 0 25 0 1 0 1769561549 13774848 3045 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3363 3045 145 145 0 3218 0 [pid=29836] vsize: 13452 Current children cumulated CPU time (s) 819.91 Current children cumulated vsize (Kb) 15576 [startup+830.067 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3062 0 0 0 82962 26 0 0 25 0 1 0 1769561549 13774848 3045 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3363 3045 145 145 0 3218 0 [pid=29836] vsize: 13452 Current children cumulated CPU time (s) 829.9 Current children cumulated vsize (Kb) 15576 [startup+840.067 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3071 0 0 0 83963 26 0 0 25 0 1 0 1769561549 13824000 3054 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3375 3054 145 145 0 3230 0 [pid=29836] vsize: 13500 Current children cumulated CPU time (s) 839.91 Current children cumulated vsize (Kb) 15624 [startup+850.068 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3117 0 0 0 84962 27 0 0 25 0 1 0 1769561549 14012416 3100 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3421 3100 145 145 0 3276 0 [pid=29836] vsize: 13684 Current children cumulated CPU time (s) 849.91 Current children cumulated vsize (Kb) 15808 [startup+860.069 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3249 0 0 0 85960 28 0 0 25 0 1 0 1769561549 14548992 3232 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3552 3232 145 145 0 3407 0 [pid=29836] vsize: 14208 Current children cumulated CPU time (s) 859.9 Current children cumulated vsize (Kb) 16332 [startup+870.07 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3369 0 0 0 86958 28 0 0 25 0 1 0 1769561549 15048704 3352 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3674 3352 145 145 0 3529 0 [pid=29836] vsize: 14696 Current children cumulated CPU time (s) 869.88 Current children cumulated vsize (Kb) 16820 [startup+880.072 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3381 0 0 0 87958 29 0 0 25 0 1 0 1769561549 15114240 3364 4294967295 134512640 135094434 3221224448 3221223104 134558156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3690 3364 145 145 0 3545 0 [pid=29836] vsize: 14760 Current children cumulated CPU time (s) 879.89 Current children cumulated vsize (Kb) 16884 [startup+890.072 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3382 0 0 0 88958 29 0 0 25 0 1 0 1769561549 15114240 3365 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3690 3365 145 145 0 3545 0 [pid=29836] vsize: 14760 Current children cumulated CPU time (s) 889.89 Current children cumulated vsize (Kb) 16884 [startup+900.073 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3396 0 0 0 89958 29 0 0 25 0 1 0 1769561549 15179776 3379 4294967295 134512640 135094434 3221224448 3221223072 134557655 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3706 3379 145 145 0 3561 0 [pid=29836] vsize: 14824 Current children cumulated CPU time (s) 899.89 Current children cumulated vsize (Kb) 16948 [startup+910.074 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3399 0 0 0 90958 29 0 0 25 0 1 0 1769561549 15179776 3382 4294967295 134512640 135094434 3221224448 3221223072 134557675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3706 3382 145 145 0 3561 0 [pid=29836] vsize: 14824 Current children cumulated CPU time (s) 909.89 Current children cumulated vsize (Kb) 16948 [startup+920.075 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3399 0 0 0 91959 29 0 0 25 0 1 0 1769561549 15179776 3382 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3706 3382 145 145 0 3561 0 [pid=29836] vsize: 14824 Current children cumulated CPU time (s) 919.9 Current children cumulated vsize (Kb) 16948 [startup+930.075 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3402 0 0 0 92959 29 0 0 25 0 1 0 1769561549 15179776 3385 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3706 3385 145 145 0 3561 0 [pid=29836] vsize: 14824 Current children cumulated CPU time (s) 929.9 Current children cumulated vsize (Kb) 16948 [startup+940.076 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3406 0 0 0 93959 29 0 0 25 0 1 0 1769561549 15179776 3389 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3706 3389 145 145 0 3561 0 [pid=29836] vsize: 14824 Current children cumulated CPU time (s) 939.9 Current children cumulated vsize (Kb) 16948 [startup+950.077 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3415 0 0 0 94959 29 0 0 25 0 1 0 1769561549 15212544 3398 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3714 3398 145 145 0 3569 0 [pid=29836] vsize: 14856 Current children cumulated CPU time (s) 949.9 Current children cumulated vsize (Kb) 16980 [startup+960.078 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3415 0 0 0 95959 29 0 0 25 0 1 0 1769561549 15212544 3398 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3714 3398 145 145 0 3569 0 [pid=29836] vsize: 14856 Current children cumulated CPU time (s) 959.9 Current children cumulated vsize (Kb) 16980 [startup+970.079 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3415 0 0 0 96959 29 0 0 25 0 1 0 1769561549 15212544 3398 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3714 3398 145 145 0 3569 0 [pid=29836] vsize: 14856 Current children cumulated CPU time (s) 969.9 Current children cumulated vsize (Kb) 16980 [startup+980.079 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3416 0 0 0 97960 29 0 0 25 0 1 0 1769561549 15212544 3399 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3714 3399 145 145 0 3569 0 [pid=29836] vsize: 14856 Current children cumulated CPU time (s) 979.91 Current children cumulated vsize (Kb) 16980 [startup+990.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3429 0 0 0 98960 30 0 0 25 0 1 0 1769561549 15310848 3412 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3738 3412 145 145 0 3593 0 [pid=29836] vsize: 14952 Current children cumulated CPU time (s) 989.92 Current children cumulated vsize (Kb) 17076 [startup+1000.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3441 0 0 0 99960 30 0 0 25 0 1 0 1769561549 15343616 3424 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3746 3424 145 145 0 3601 0 [pid=29836] vsize: 14984 Current children cumulated CPU time (s) 999.92 Current children cumulated vsize (Kb) 17108 [startup+1010.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3446 0 0 0 100960 30 0 0 25 0 1 0 1769561549 15360000 3429 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3750 3429 145 145 0 3605 0 [pid=29836] vsize: 15000 Current children cumulated CPU time (s) 1009.92 Current children cumulated vsize (Kb) 17124 [startup+1020.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3449 0 0 0 101960 30 0 0 25 0 1 0 1769561549 15360000 3432 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3750 3432 145 145 0 3605 0 [pid=29836] vsize: 15000 Current children cumulated CPU time (s) 1019.92 Current children cumulated vsize (Kb) 17124 [startup+1030.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3451 0 0 0 102960 30 0 0 25 0 1 0 1769561549 15360000 3434 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3750 3434 145 145 0 3605 0 [pid=29836] vsize: 15000 Current children cumulated CPU time (s) 1029.92 Current children cumulated vsize (Kb) 17124 [startup+1040.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3451 0 0 0 103961 30 0 0 25 0 1 0 1769561549 15360000 3434 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3750 3434 145 145 0 3605 0 [pid=29836] vsize: 15000 Current children cumulated CPU time (s) 1039.93 Current children cumulated vsize (Kb) 17124 [startup+1050.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3451 0 0 0 104961 30 0 0 25 0 1 0 1769561549 15360000 3434 4294967295 134512640 135094434 3221224448 3221223104 134558184 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3750 3434 145 145 0 3605 0 [pid=29836] vsize: 15000 Current children cumulated CPU time (s) 1049.93 Current children cumulated vsize (Kb) 17124 [startup+1060.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3476 0 0 0 105961 30 0 0 25 0 1 0 1769561549 15491072 3459 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3782 3459 145 145 0 3637 0 [pid=29836] vsize: 15128 Current children cumulated CPU time (s) 1059.93 Current children cumulated vsize (Kb) 17252 [startup+1070.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3493 0 0 0 106961 30 0 0 25 0 1 0 1769561549 15556608 3476 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3798 3476 145 145 0 3653 0 [pid=29836] vsize: 15192 Current children cumulated CPU time (s) 1069.93 Current children cumulated vsize (Kb) 17316 [startup+1080.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3493 0 0 0 107961 30 0 0 25 0 1 0 1769561549 15556608 3476 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3798 3476 145 145 0 3653 0 [pid=29836] vsize: 15192 Current children cumulated CPU time (s) 1079.93 Current children cumulated vsize (Kb) 17316 [startup+1090.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3493 0 0 0 108961 30 0 0 25 0 1 0 1769561549 15556608 3476 4294967295 134512640 135094434 3221224448 3221223120 134555570 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3798 3476 145 145 0 3653 0 [pid=29836] vsize: 15192 Current children cumulated CPU time (s) 1089.93 Current children cumulated vsize (Kb) 17316 [startup+1100.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3493 0 0 0 109962 30 0 0 25 0 1 0 1769561549 15556608 3476 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3798 3476 145 145 0 3653 0 [pid=29836] vsize: 15192 Current children cumulated CPU time (s) 1099.94 Current children cumulated vsize (Kb) 17316 [startup+1110.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3498 0 0 0 110962 30 0 0 25 0 1 0 1769561549 15589376 3481 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3806 3481 145 145 0 3661 0 [pid=29836] vsize: 15224 Current children cumulated CPU time (s) 1109.94 Current children cumulated vsize (Kb) 17348 [startup+1120.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3507 0 0 0 111962 30 0 0 25 0 1 0 1769561549 15654912 3490 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3822 3490 145 145 0 3677 0 [pid=29836] vsize: 15288 Current children cumulated CPU time (s) 1119.94 Current children cumulated vsize (Kb) 17412 [startup+1130.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3508 0 0 0 112962 30 0 0 25 0 1 0 1769561549 15654912 3491 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3822 3491 145 145 0 3677 0 [pid=29836] vsize: 15288 Current children cumulated CPU time (s) 1129.94 Current children cumulated vsize (Kb) 17412 [startup+1140.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3508 0 0 0 113962 30 0 0 25 0 1 0 1769561549 15654912 3491 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3822 3491 145 145 0 3677 0 [pid=29836] vsize: 15288 Current children cumulated CPU time (s) 1139.94 Current children cumulated vsize (Kb) 17412 [startup+1150.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3521 0 0 0 114962 30 0 0 25 0 1 0 1769561549 15720448 3504 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3838 3504 145 145 0 3693 0 [pid=29836] vsize: 15352 Current children cumulated CPU time (s) 1149.94 Current children cumulated vsize (Kb) 17476 [startup+1160.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3522 0 0 0 115963 30 0 0 25 0 1 0 1769561549 15720448 3505 4294967295 134512640 135094434 3221224448 3221223072 134557583 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3838 3505 145 145 0 3693 0 [pid=29836] vsize: 15352 Current children cumulated CPU time (s) 1159.95 Current children cumulated vsize (Kb) 17476 [startup+1170.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3523 0 0 0 116963 30 0 0 25 0 1 0 1769561549 15720448 3506 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3838 3506 145 145 0 3693 0 [pid=29836] vsize: 15352 Current children cumulated CPU time (s) 1169.95 Current children cumulated vsize (Kb) 17476 [startup+1180.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3524 0 0 0 117963 30 0 0 25 0 1 0 1769561549 15720448 3507 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3838 3507 145 145 0 3693 0 [pid=29836] vsize: 15352 Current children cumulated CPU time (s) 1179.95 Current children cumulated vsize (Kb) 17476 [startup+1190.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3524 0 0 0 118964 30 0 0 25 0 1 0 1769561549 15720448 3507 4294967295 134512640 135094434 3221224448 3221223040 134557004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29836/statm): 3838 3507 145 145 0 3693 0 [pid=29836] vsize: 15352 Current children cumulated CPU time (s) 1189.96 Current children cumulated vsize (Kb) 17476 [startup+1200.1 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3557 0 0 0 119963 31 0 0 25 0 1 0 1769561549 15982592 3540 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29836/statm): 3902 3540 145 145 0 3757 0 [pid=29836] vsize: 15608 Current children cumulated CPU time (s) 1199.96 Current children cumulated vsize (Kb) 17732 [startup+1210.1 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3558 0 0 0 120961 31 0 0 25 0 1 0 1769561549 15982592 3541 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29836/statm): 3902 3541 145 145 0 3757 0 [pid=29836] vsize: 15608 Current children cumulated CPU time (s) 1209.94 Current children cumulated vsize (Kb) 17732 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 29836 Raw data (/proc/29832/stat): 29832 (minisat+_script) S 29831 29832 27660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1769561544 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/29832/statm): 531 226 485 147 0 384 0 [pid=29832] vsize: 2124 Raw data (/proc/29836/stat): 29836 (minisat+_64-bit) R 29832 29832 27660 0 -1 0 3558 0 0 0 120961 31 0 0 25 0 1 0 1769561549 15982592 3541 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29836/statm): 3902 3541 145 145 0 3757 0 [pid=29836] vsize: 15608 Current children cumulated CPU time (s) 1209.94 Current children cumulated vsize (Kb) 17732 Sending SIGTERM to -29832 Sleeping 2 seconds One traced child (pid=29832) ended because it received signal 15 (SIGTERM) One traced child (pid=29836) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.11 CPU time (s): 1209.94 CPU user time (s): 1209.62 CPU system time (s): 0.32595 CPU usage (%): 99.9862 Max. virtual memory (cumulated for all children) (Kb): 17732
ERROR: no interpretation found !