Name | submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-my_adder.opb |
MD5SUM | fe8f615a95a6852516985b8e3e78bd85 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 4561 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 577 |
Biggest coefficient in the objective function | 61 |
Number of bits for the biggest coefficient in the objective function | 6 |
Sum of the numbers in the objective function | 24510 |
Number of bits of the sum of numbers in the objective function | 15 |
Biggest number in a constraint | 61 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 24510 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 45.2981 |
Number of variables | 577 |
Total number of constraints | 1322 |
Number of constraints which are clauses | 1306 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 16 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 17 |
LAUNCH ON wulflinc15 THE 2005-09-18 18:11:28 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2598 boxname=wulflinc15 idbench=254 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fe8f615a95a6852516985b8e3e78bd85 /oldhome/oroussel/tmp/wulflinc15/normalized-my_adder.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-my_adder.opb IDLAUNCH: 2598 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 917672 kB Buffers: 33656 kB Cached: 54392 kB SwapCached: 692 kB Active: 46740 kB Inactive: 43908 kB HighTotal: 131008 kB HighFree: 73500 kB LowTotal: 903652 kB LowFree: 844172 kB SwapTotal: 2097136 kB SwapFree: 2095920 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5732 kB Slab: 20572 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 18:31:39 (client local time) WITH STATUS 10 IN 1207.97 SECONDS stats: 2598 7 1207.97 10
c Parsing PB file... c Converting 1322 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 | 1322 4977 | 440 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 6274[0m c ---[ 0]---> Sorter-cost:87831 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1 | 210130 492551 | 70043 1 7 7.0 | 0.000 % | c | 101 | 209639 491465 | 77047 98 1983 20.2 | 0.188 % | c | 251 | 209398 490919 | 84752 246 3047 12.4 | 0.270 % | c | 477 | 209398 490919 | 93227 472 5320 11.3 | 0.270 % | c | 814 | 209398 490919 | 102549 809 7426 9.2 | 0.270 % | c | 1320 | 209398 490919 | 112804 1315 12893 9.8 | 0.270 % | c | 2079 | 208099 487975 | 124085 2062 18966 9.2 | 0.850 % | c | 3223 | 207777 487250 | 136493 3203 75259 23.5 | 1.015 % | c | 4934 | 207777 487250 | 150143 4914 465375 94.7 | 1.015 % | c | 7496 | 207777 487250 | 165157 7476 523941 70.1 | 1.015 % | c | 11343 | 207124 485763 | 181673 11316 605974 53.6 | 1.304 % | c ============================================================================== c [1mFound solution: 6030[0m c ---[ 0]---> Sorter-cost:63107 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15902 | 341282 799222 | 113760 15812 677541 42.8 | 1.304 % | c | 16002 | 341282 799222 | 125136 15912 678586 42.6 | 1.292 % | c | 16153 | 341282 799222 | 137649 16063 680125 42.3 | 1.292 % | c | 16378 | 341282 799222 | 151414 16288 682659 41.9 | 1.292 % | c | 16715 | 341282 799222 | 166556 16625 686273 41.3 | 1.292 % | c | 17222 | 341282 799222 | 183211 17132 689710 40.3 | 1.292 % | c | 17982 | 341282 799222 | 201532 17892 701677 39.2 | 1.292 % | c ============================================================================== c [1mFound solution: 5941[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18575 | 341328 799730 | 113776 18485 726783 39.3 | 1.292 % | c | 18675 | 341311 799693 | 125153 18584 727472 39.1 | 1.297 % | c | 18825 | 341311 799693 | 137668 18734 728419 38.9 | 1.297 % | c | 19050 | 341311 799693 | 151435 18959 730280 38.5 | 1.297 % | c | 19388 | 341311 799693 | 166579 19297 732516 38.0 | 1.297 % | c | 19894 | 341311 799693 | 183237 19803 738567 37.3 | 1.297 % | c | 20653 | 341060 799139 | 201561 20560 748577 36.4 | 1.351 % | c | 21792 | 341060 799139 | 221717 21699 757149 34.9 | 1.351 % | c | 23500 | 341060 799139 | 243888 23407 808068 34.5 | 1.351 % | c | 26064 | 340058 796875 | 268277 25935 888362 34.3 | 1.591 % | c | 29909 | 340058 796875 | 295105 29780 993861 33.4 | 1.591 % | c | 35675 | 340058 796875 | 324616 35546 1611580 45.3 | 1.591 % | c | 44326 | 340058 796875 | 357077 44197 2011857 45.5 | 1.591 % | c | 57300 | 339999 796741 | 392785 57162 2368847 41.4 | 1.609 % | c | 76763 | 339999 796741 | 432064 76625 7374052 96.2 | 1.609 % | c | 105956 | 339999 796741 | 475270 105818 9897084 93.5 | 1.609 % | c ============================================================================== c [1mFound solution: 5700[0m c ---[ 0]---> Sorter-cost:64909 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 108372 | 479644 1122919 | 159881 108234 10027671 92.6 | 1.609 % | c | 108473 | 479644 1122919 | 175869 108335 10028620 92.6 | 1.141 % | c | 108623 | 479644 1122919 | 193456 108485 10030258 92.5 | 1.141 % | c | 108848 | 479644 1122919 | 212801 108710 10032710 92.3 | 1.141 % | c | 109185 | 479644 1122919 | 234081 109047 10045641 92.1 | 1.141 % | c | 109691 | 479498 1122590 | 257489 109542 10064209 91.9 | 1.162 % | c | 110451 | 479498 1122590 | 283238 110302 10074504 91.3 | 1.162 % | c | 111590 | 479498 1122590 | 311562 111441 10093566 90.6 | 1.162 % | c | 113298 | 479498 1122590 | 342719 113149 10108665 89.3 | 1.162 % | c | 115860 | 479488 1122570 | 376991 115708 10180504 88.0 | 1.165 % | c | 119704 | 479488 1122570 | 414690 119552 10487501 87.7 | 1.165 % | c | 125470 | 479488 1122570 | 456159 125318 11610478 92.6 | 1.165 % | c | 134119 | 479488 1122570 | 501775 133967 11828437 88.3 | 1.165 % | c | 147093 | 479488 1122570 | 551952 146941 12479339 84.9 | 1.165 % | c | 166556 | 479456 1122498 | 607147 166403 15031220 90.3 | 1.175 % |
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/10833/stat): 10833 (minisat+_script) R 10832 10833 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785077480 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/10833/statm): 174 3 169 147 0 27 0 [pid=10833] 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=10834 New process pid=10835 New process pid=10836 One traced child (pid=10835) exited with status: 0 execve syscall for /bin/sed executable 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=10836) exited with status: 0 One traced child (pid=10834) exited with status: 0 New process pid=10837 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-my_adder.opb [startup+10.0045 s] Raw data (loadavg): 0.93 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 7061 0 0 0 942 28 0 0 25 0 1 0 1785077485 30978048 6583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 7563 6583 145 145 0 7418 0 [pid=10837] vsize: 30252 Current children cumulated CPU time (s) 9.71 Current children cumulated vsize (Kb) 32376 [startup+20.0052 s] Raw data (loadavg): 0.94 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 7382 0 0 0 1938 29 0 0 25 0 1 0 1785077485 32321536 6904 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 7891 6904 145 145 0 7746 0 [pid=10837] vsize: 31564 Current children cumulated CPU time (s) 19.68 Current children cumulated vsize (Kb) 33688 [startup+30.0071 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 7572 0 0 0 2935 31 0 0 25 0 1 0 1785077485 33116160 7094 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 8085 7094 145 145 0 7940 0 [pid=10837] vsize: 32340 Current children cumulated CPU time (s) 29.67 Current children cumulated vsize (Kb) 34464 [startup+40.0079 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 7686 0 0 0 3932 32 0 0 25 0 1 0 1785077485 33599488 7208 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 8203 7208 145 145 0 8058 0 [pid=10837] vsize: 32812 Current children cumulated CPU time (s) 39.65 Current children cumulated vsize (Kb) 34936 [startup+50.0087 s] Raw data (loadavg): 0.96 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 7757 0 0 0 4930 33 0 0 25 0 1 0 1785077485 33878016 7279 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 8271 7279 145 145 0 8126 0 [pid=10837] vsize: 33084 Current children cumulated CPU time (s) 49.64 Current children cumulated vsize (Kb) 35208 [startup+60.0105 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 11987 0 0 0 5895 50 0 0 25 0 1 0 1785077485 57524224 11384 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 14044 11384 145 145 0 13899 0 [pid=10837] vsize: 56176 Current children cumulated CPU time (s) 59.46 Current children cumulated vsize (Kb) 58300 [startup+70.0113 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12336 0 0 0 6891 52 0 0 25 0 1 0 1785077485 58277888 11691 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 14228 11691 145 145 0 14083 0 [pid=10837] vsize: 56912 Current children cumulated CPU time (s) 69.44 Current children cumulated vsize (Kb) 59036 [startup+80.0131 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12366 0 0 0 7890 53 0 0 25 0 1 0 1785077485 58388480 11721 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 14255 11721 145 145 0 14110 0 [pid=10837] vsize: 57020 Current children cumulated CPU time (s) 79.44 Current children cumulated vsize (Kb) 59144 [startup+90.0139 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12450 0 0 0 8888 54 0 0 25 0 1 0 1785077485 58724352 11805 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 14337 11805 145 145 0 14192 0 [pid=10837] vsize: 57348 Current children cumulated CPU time (s) 89.43 Current children cumulated vsize (Kb) 59472 [startup+100.014 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12490 0 0 0 9887 54 0 0 25 0 1 0 1785077485 58888192 11845 4294967295 134512640 135094434 3221224448 3221223104 134557818 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 14377 11845 145 145 0 14232 0 [pid=10837] vsize: 57508 Current children cumulated CPU time (s) 99.42 Current children cumulated vsize (Kb) 59632 [startup+110.014 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12542 0 0 0 10887 55 0 0 25 0 1 0 1785077485 59092992 11897 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 14427 11897 145 145 0 14282 0 [pid=10837] vsize: 57708 Current children cumulated CPU time (s) 109.43 Current children cumulated vsize (Kb) 59832 [startup+120.015 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12609 0 0 0 11886 55 0 0 25 0 1 0 1785077485 59359232 11964 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 14492 11964 145 145 0 14347 0 [pid=10837] vsize: 57968 Current children cumulated CPU time (s) 119.42 Current children cumulated vsize (Kb) 60092 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12720 0 0 0 12884 56 0 0 25 0 1 0 1785077485 59932672 12075 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 14632 12075 145 145 0 14487 0 [pid=10837] vsize: 58528 Current children cumulated CPU time (s) 129.41 Current children cumulated vsize (Kb) 60652 [startup+140.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 12886 0 0 0 13881 57 0 0 25 0 1 0 1785077485 60608512 12241 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 14797 12241 145 145 0 14652 0 [pid=10837] vsize: 59188 Current children cumulated CPU time (s) 139.39 Current children cumulated vsize (Kb) 61312 [startup+150.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13124 0 0 0 14877 59 0 0 25 0 1 0 1785077485 61579264 12479 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 15034 12479 145 145 0 14889 0 [pid=10837] vsize: 60136 Current children cumulated CPU time (s) 149.37 Current children cumulated vsize (Kb) 62260 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13306 0 0 0 15875 60 0 0 25 0 1 0 1785077485 62320640 12661 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 15215 12661 145 145 0 15070 0 [pid=10837] vsize: 60860 Current children cumulated CPU time (s) 159.36 Current children cumulated vsize (Kb) 62984 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13352 0 0 0 16874 60 0 0 25 0 1 0 1785077485 62504960 12707 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 15260 12707 145 145 0 15115 0 [pid=10837] vsize: 61040 Current children cumulated CPU time (s) 169.35 Current children cumulated vsize (Kb) 63164 [startup+180.021 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13415 0 0 0 17873 61 0 0 25 0 1 0 1785077485 62754816 12770 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 15321 12770 145 145 0 15176 0 [pid=10837] vsize: 61284 Current children cumulated CPU time (s) 179.35 Current children cumulated vsize (Kb) 63408 [startup+190.022 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13539 0 0 0 18870 62 0 0 25 0 1 0 1785077485 63254528 12894 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 15443 12894 145 145 0 15298 0 [pid=10837] vsize: 61772 Current children cumulated CPU time (s) 189.33 Current children cumulated vsize (Kb) 63896 [startup+200.023 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13697 0 0 0 19866 63 0 0 25 0 1 0 1785077485 63897600 13052 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 15600 13052 145 145 0 15455 0 [pid=10837] vsize: 62400 Current children cumulated CPU time (s) 199.3 Current children cumulated vsize (Kb) 64524 [startup+210.025 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13782 0 0 0 20865 64 0 0 25 0 1 0 1785077485 64233472 13137 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 15682 13137 145 145 0 15537 0 [pid=10837] vsize: 62728 Current children cumulated CPU time (s) 209.3 Current children cumulated vsize (Kb) 64852 [startup+220.025 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13901 0 0 0 21863 65 0 0 25 0 1 0 1785077485 64708608 13256 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 15798 13256 145 145 0 15653 0 [pid=10837] vsize: 63192 Current children cumulated CPU time (s) 219.29 Current children cumulated vsize (Kb) 65316 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 13950 0 0 0 22862 65 0 0 25 0 1 0 1785077485 64905216 13305 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 15846 13305 145 145 0 15701 0 [pid=10837] vsize: 63384 Current children cumulated CPU time (s) 229.28 Current children cumulated vsize (Kb) 65508 [startup+240.027 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14016 0 0 0 23860 66 0 0 25 0 1 0 1785077485 65167360 13371 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 15910 13371 145 145 0 15765 0 [pid=10837] vsize: 63640 Current children cumulated CPU time (s) 239.27 Current children cumulated vsize (Kb) 65764 [startup+250.028 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14084 0 0 0 24859 66 0 0 25 0 1 0 1785077485 65437696 13439 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 15976 13439 145 145 0 15831 0 [pid=10837] vsize: 63904 Current children cumulated CPU time (s) 249.26 Current children cumulated vsize (Kb) 66028 [startup+260.029 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14162 0 0 0 25858 67 0 0 25 0 1 0 1785077485 65748992 13517 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 16052 13517 145 145 0 15907 0 [pid=10837] vsize: 64208 Current children cumulated CPU time (s) 259.26 Current children cumulated vsize (Kb) 66332 [startup+270.029 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14228 0 0 0 26856 67 0 0 25 0 1 0 1785077485 66015232 13583 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 16117 13583 145 145 0 15972 0 [pid=10837] vsize: 64468 Current children cumulated CPU time (s) 269.24 Current children cumulated vsize (Kb) 66592 [startup+280.031 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14294 0 0 0 27854 68 0 0 25 0 1 0 1785077485 66277376 13649 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 16181 13649 145 145 0 16036 0 [pid=10837] vsize: 64724 Current children cumulated CPU time (s) 279.23 Current children cumulated vsize (Kb) 66848 [startup+290.032 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14447 0 0 0 28852 69 0 0 25 0 1 0 1785077485 66899968 13802 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 16333 13802 145 145 0 16188 0 [pid=10837] vsize: 65332 Current children cumulated CPU time (s) 289.22 Current children cumulated vsize (Kb) 67456 [startup+300.033 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14679 0 0 0 29849 70 0 0 25 0 1 0 1785077485 67846144 14034 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 16564 14034 145 145 0 16419 0 [pid=10837] vsize: 66256 Current children cumulated CPU time (s) 299.2 Current children cumulated vsize (Kb) 68380 [startup+310.034 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 14865 0 0 0 30848 71 0 0 25 0 1 0 1785077485 68608000 14220 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 16750 14220 145 145 0 16605 0 [pid=10837] vsize: 67000 Current children cumulated CPU time (s) 309.2 Current children cumulated vsize (Kb) 69124 [startup+320.034 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 15123 0 0 0 31845 73 0 0 25 0 1 0 1785077485 69660672 14478 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 17007 14478 145 145 0 16862 0 [pid=10837] vsize: 68028 Current children cumulated CPU time (s) 319.19 Current children cumulated vsize (Kb) 70152 [startup+330.036 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 15309 0 0 0 32843 73 0 0 25 0 1 0 1785077485 70418432 14664 4294967295 134512640 135094434 3221224448 3221223104 134558286 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 17192 14664 145 145 0 17047 0 [pid=10837] vsize: 68768 Current children cumulated CPU time (s) 329.17 Current children cumulated vsize (Kb) 70892 [startup+340.037 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 15574 0 0 0 33839 76 0 0 25 0 1 0 1785077485 71503872 14929 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 17457 14929 145 145 0 17312 0 [pid=10837] vsize: 69828 Current children cumulated CPU time (s) 339.16 Current children cumulated vsize (Kb) 71952 [startup+350.038 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 15822 0 0 0 34836 77 0 0 25 0 1 0 1785077485 72519680 15177 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 17705 15177 145 145 0 17560 0 [pid=10837] vsize: 70820 Current children cumulated CPU time (s) 349.14 Current children cumulated vsize (Kb) 72944 [startup+360.04 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 16058 0 0 0 35832 78 0 0 25 0 1 0 1785077485 73482240 15413 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 17940 15413 145 145 0 17795 0 [pid=10837] vsize: 71760 Current children cumulated CPU time (s) 359.11 Current children cumulated vsize (Kb) 73884 [startup+370.041 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) T 10833 10833 31778 0 -1 0 16307 0 0 0 36830 79 0 0 25 0 1 0 1785077485 74498048 15662 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/10837/statm): 18188 15662 145 145 0 18043 0 [pid=10837] vsize: 72752 Current children cumulated CPU time (s) 369.1 Current children cumulated vsize (Kb) 74876 [startup+380.041 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 16518 0 0 0 37827 80 0 0 25 0 1 0 1785077485 75362304 15873 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 18399 15873 145 145 0 18254 0 [pid=10837] vsize: 73596 Current children cumulated CPU time (s) 379.08 Current children cumulated vsize (Kb) 75720 [startup+390.042 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 16732 0 0 0 38824 82 0 0 25 0 1 0 1785077485 76496896 16087 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 18676 16087 145 145 0 18531 0 [pid=10837] vsize: 74704 Current children cumulated CPU time (s) 389.07 Current children cumulated vsize (Kb) 76828 [startup+400.042 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 16966 0 0 0 39821 83 0 0 25 0 1 0 1785077485 77455360 16321 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 18910 16321 145 145 0 18765 0 [pid=10837] vsize: 75640 Current children cumulated CPU time (s) 399.05 Current children cumulated vsize (Kb) 77764 [startup+410.043 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 17165 0 0 0 40818 85 0 0 25 0 1 0 1785077485 78270464 16520 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 19109 16520 145 145 0 18964 0 [pid=10837] vsize: 76436 Current children cumulated CPU time (s) 409.04 Current children cumulated vsize (Kb) 78560 [startup+420.044 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 17391 0 0 0 41815 86 0 0 25 0 1 0 1785077485 79192064 16746 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 19334 16746 145 145 0 19189 0 [pid=10837] vsize: 77336 Current children cumulated CPU time (s) 419.02 Current children cumulated vsize (Kb) 79460 [startup+430.044 s] Raw data (loadavg): 0.99 0.97 0.99 3/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 17644 0 0 0 42811 88 0 0 25 0 1 0 1785077485 80224256 16999 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 19586 16999 145 145 0 19441 0 [pid=10837] vsize: 78344 Current children cumulated CPU time (s) 429 Current children cumulated vsize (Kb) 80468 [startup+440.045 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 17889 0 0 0 43808 89 0 0 25 0 1 0 1785077485 81227776 17244 4294967295 134512640 135094434 3221224448 3221223136 134554705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 19831 17244 145 145 0 19686 0 [pid=10837] vsize: 79324 Current children cumulated CPU time (s) 438.98 Current children cumulated vsize (Kb) 81448 [startup+450.046 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 18073 0 0 0 44805 90 0 0 25 0 1 0 1785077485 81973248 17428 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 20013 17428 145 145 0 19868 0 [pid=10837] vsize: 80052 Current children cumulated CPU time (s) 448.96 Current children cumulated vsize (Kb) 82176 [startup+460.047 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 18313 0 0 0 45802 92 0 0 25 0 1 0 1785077485 82956288 17668 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 20253 17668 145 145 0 20108 0 [pid=10837] vsize: 81012 Current children cumulated CPU time (s) 458.95 Current children cumulated vsize (Kb) 83136 [startup+470.048 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 18458 0 0 0 46800 93 0 0 25 0 1 0 1785077485 83546112 17813 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 20397 17813 145 145 0 20252 0 [pid=10837] vsize: 81588 Current children cumulated CPU time (s) 468.94 Current children cumulated vsize (Kb) 83712 [startup+480.05 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 18717 0 0 0 47797 94 0 0 25 0 1 0 1785077485 84606976 18072 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 20656 18072 145 145 0 20511 0 [pid=10837] vsize: 82624 Current children cumulated CPU time (s) 478.92 Current children cumulated vsize (Kb) 84748 [startup+490.05 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 18979 0 0 0 48793 96 0 0 25 0 1 0 1785077485 85676032 18334 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 20917 18334 145 145 0 20772 0 [pid=10837] vsize: 83668 Current children cumulated CPU time (s) 488.9 Current children cumulated vsize (Kb) 85792 [startup+500.05 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 19216 0 0 0 49790 97 0 0 25 0 1 0 1785077485 86642688 18571 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 21153 18571 145 145 0 21008 0 [pid=10837] vsize: 84612 Current children cumulated CPU time (s) 498.88 Current children cumulated vsize (Kb) 86736 [startup+510.051 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 19277 0 0 0 50789 98 0 0 25 0 1 0 1785077485 86888448 18632 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 21213 18632 145 145 0 21068 0 [pid=10837] vsize: 84852 Current children cumulated CPU time (s) 508.88 Current children cumulated vsize (Kb) 86976 [startup+520.052 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 19345 0 0 0 51788 98 0 0 25 0 1 0 1785077485 87162880 18700 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 21280 18700 145 145 0 21135 0 [pid=10837] vsize: 85120 Current children cumulated CPU time (s) 518.87 Current children cumulated vsize (Kb) 87244 [startup+530.053 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 19516 0 0 0 52784 100 0 0 25 0 1 0 1785077485 87855104 18871 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 21449 18871 145 145 0 21304 0 [pid=10837] vsize: 85796 Current children cumulated CPU time (s) 528.85 Current children cumulated vsize (Kb) 87920 [startup+540.054 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 19768 0 0 0 53780 102 0 0 25 0 1 0 1785077485 88887296 19123 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 21701 19123 145 145 0 21556 0 [pid=10837] vsize: 86804 Current children cumulated CPU time (s) 538.83 Current children cumulated vsize (Kb) 88928 [startup+550.055 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 19946 0 0 0 54777 104 0 0 25 0 1 0 1785077485 89608192 19301 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 21877 19301 145 145 0 21732 0 [pid=10837] vsize: 87508 Current children cumulated CPU time (s) 548.82 Current children cumulated vsize (Kb) 89632 [startup+560.057 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 20229 0 0 0 55772 105 0 0 25 0 1 0 1785077485 90755072 19584 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 22157 19584 145 145 0 22012 0 [pid=10837] vsize: 88628 Current children cumulated CPU time (s) 558.78 Current children cumulated vsize (Kb) 90752 [startup+570.058 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 20481 0 0 0 56767 108 0 0 25 0 1 0 1785077485 91779072 19836 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 22407 19836 145 145 0 22262 0 [pid=10837] vsize: 89628 Current children cumulated CPU time (s) 568.76 Current children cumulated vsize (Kb) 91752 [startup+580.058 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 20684 0 0 0 57764 109 0 0 25 0 1 0 1785077485 92606464 20039 4294967295 134512640 135094434 3221224448 3221223040 134556853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 22609 20039 145 145 0 22464 0 [pid=10837] vsize: 90436 Current children cumulated CPU time (s) 578.74 Current children cumulated vsize (Kb) 92560 [startup+590.058 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 20867 0 0 0 58760 111 0 0 25 0 1 0 1785077485 93347840 20222 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 22790 20222 145 145 0 22645 0 [pid=10837] vsize: 91160 Current children cumulated CPU time (s) 588.72 Current children cumulated vsize (Kb) 93284 [startup+600.06 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 21036 0 0 0 59757 112 0 0 25 0 1 0 1785077485 94031872 20391 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10837/statm): 22957 20391 145 145 0 22812 0 [pid=10837] vsize: 91828 Current children cumulated CPU time (s) 598.7 Current children cumulated vsize (Kb) 93952 [startup+610.061 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 21265 0 0 0 60754 114 0 0 25 0 1 0 1785077485 94965760 20620 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 23185 20620 145 145 0 23040 0 [pid=10837] vsize: 92740 Current children cumulated CPU time (s) 608.69 Current children cumulated vsize (Kb) 94864 [startup+620.062 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 21435 0 0 0 61752 115 0 0 25 0 1 0 1785077485 95657984 20790 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 23354 20790 145 145 0 23209 0 [pid=10837] vsize: 93416 Current children cumulated CPU time (s) 618.68 Current children cumulated vsize (Kb) 95540 [startup+630.063 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 21537 0 0 0 62750 115 0 0 25 0 1 0 1785077485 96067584 20892 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 23454 20892 145 145 0 23309 0 [pid=10837] vsize: 93816 Current children cumulated CPU time (s) 628.66 Current children cumulated vsize (Kb) 95940 [startup+640.064 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 21749 0 0 0 63746 117 0 0 25 0 1 0 1785077485 96915456 21104 4294967295 134512640 135094434 3221224448 3221223072 134557642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 23661 21104 145 145 0 23516 0 [pid=10837] vsize: 94644 Current children cumulated CPU time (s) 638.64 Current children cumulated vsize (Kb) 96768 [startup+650.063 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 21931 0 0 0 64742 119 0 0 25 0 1 0 1785077485 97648640 21286 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 23840 21286 145 145 0 23695 0 [pid=10837] vsize: 95360 Current children cumulated CPU time (s) 648.62 Current children cumulated vsize (Kb) 97484 [startup+660.065 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 22128 0 0 0 65737 121 0 0 25 0 1 0 1785077485 98443264 21483 4294967295 134512640 135094434 3221224448 3221223040 134556884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 24034 21483 145 145 0 23889 0 [pid=10837] vsize: 96136 Current children cumulated CPU time (s) 658.59 Current children cumulated vsize (Kb) 98260 [startup+670.066 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 26985 0 0 0 66699 140 0 0 25 0 1 0 1785077485 113901568 25968 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 27808 25968 145 145 0 27663 0 [pid=10837] vsize: 111232 Current children cumulated CPU time (s) 668.4 Current children cumulated vsize (Kb) 113356 [startup+680.066 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27063 0 0 0 67698 140 0 0 25 0 1 0 1785077485 114212864 26046 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 27884 26046 145 145 0 27739 0 [pid=10837] vsize: 111536 Current children cumulated CPU time (s) 678.39 Current children cumulated vsize (Kb) 113660 [startup+690.067 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27135 0 0 0 68697 141 0 0 25 0 1 0 1785077485 114511872 26118 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 27957 26118 145 145 0 27812 0 [pid=10837] vsize: 111828 Current children cumulated CPU time (s) 688.39 Current children cumulated vsize (Kb) 113952 [startup+700.067 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27211 0 0 0 69695 142 0 0 25 0 1 0 1785077485 114814976 26194 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 28031 26194 145 145 0 27886 0 [pid=10837] vsize: 112124 Current children cumulated CPU time (s) 698.38 Current children cumulated vsize (Kb) 114248 [startup+710.068 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27256 0 0 0 70694 142 0 0 25 0 1 0 1785077485 114991104 26239 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 28074 26239 145 145 0 27929 0 [pid=10837] vsize: 112296 Current children cumulated CPU time (s) 708.37 Current children cumulated vsize (Kb) 114420 [startup+720.069 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27313 0 0 0 71693 143 0 0 25 0 1 0 1785077485 115220480 26296 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 28130 26296 145 145 0 27985 0 [pid=10837] vsize: 112520 Current children cumulated CPU time (s) 718.37 Current children cumulated vsize (Kb) 114644 [startup+730.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27392 0 0 0 72691 143 0 0 25 0 1 0 1785077485 115539968 26375 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 28208 26375 145 145 0 28063 0 [pid=10837] vsize: 112832 Current children cumulated CPU time (s) 728.35 Current children cumulated vsize (Kb) 114956 [startup+740.071 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27524 0 0 0 73690 144 0 0 25 0 1 0 1785077485 116076544 26507 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 28339 26507 145 145 0 28194 0 [pid=10837] vsize: 113356 Current children cumulated CPU time (s) 738.35 Current children cumulated vsize (Kb) 115480 [startup+750.072 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27614 0 0 0 74689 145 0 0 25 0 1 0 1785077485 116441088 26597 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 28428 26597 145 145 0 28283 0 [pid=10837] vsize: 113712 Current children cumulated CPU time (s) 748.35 Current children cumulated vsize (Kb) 115836 [startup+760.072 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27767 0 0 0 75686 146 0 0 25 0 1 0 1785077485 117063680 26750 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 28580 26750 145 145 0 28435 0 [pid=10837] vsize: 114320 Current children cumulated CPU time (s) 758.33 Current children cumulated vsize (Kb) 116444 [startup+770.073 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 27904 0 0 0 76685 147 0 0 25 0 1 0 1785077485 117620736 26887 4294967295 134512640 135094434 3221224448 3221223040 134556843 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 28716 26887 145 145 0 28571 0 [pid=10837] vsize: 114864 Current children cumulated CPU time (s) 768.33 Current children cumulated vsize (Kb) 116988 [startup+780.074 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28224 0 0 0 77680 149 0 0 25 0 1 0 1785077485 118927360 27207 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 29035 27207 145 145 0 28890 0 [pid=10837] vsize: 116140 Current children cumulated CPU time (s) 778.3 Current children cumulated vsize (Kb) 118264 [startup+790.075 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28422 0 0 0 78677 150 0 0 25 0 1 0 1785077485 119726080 27405 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 29230 27405 145 145 0 29085 0 [pid=10837] vsize: 116920 Current children cumulated CPU time (s) 788.28 Current children cumulated vsize (Kb) 119044 [startup+800.075 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28671 0 0 0 79672 152 0 0 25 0 1 0 1785077485 120737792 27654 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 29477 27654 145 145 0 29332 0 [pid=10837] vsize: 117908 Current children cumulated CPU time (s) 798.25 Current children cumulated vsize (Kb) 120032 [startup+810.077 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28791 0 0 0 80671 153 0 0 25 0 1 0 1785077485 121225216 27774 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 29596 27774 145 145 0 29451 0 [pid=10837] vsize: 118384 Current children cumulated CPU time (s) 808.25 Current children cumulated vsize (Kb) 120508 [startup+820.077 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28843 0 0 0 81670 153 0 0 25 0 1 0 1785077485 121434112 27826 4294967295 134512640 135094434 3221224448 3221223120 134556288 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 29647 27826 145 145 0 29502 0 [pid=10837] vsize: 118588 Current children cumulated CPU time (s) 818.24 Current children cumulated vsize (Kb) 120712 [startup+830.077 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28906 0 0 0 82669 153 0 0 25 0 1 0 1785077485 121683968 27889 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 29708 27889 145 145 0 29563 0 [pid=10837] vsize: 118832 Current children cumulated CPU time (s) 828.23 Current children cumulated vsize (Kb) 120956 [startup+840.079 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 28969 0 0 0 83669 154 0 0 25 0 1 0 1785077485 122458112 27952 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 29897 27952 145 145 0 29752 0 [pid=10837] vsize: 119588 Current children cumulated CPU time (s) 838.24 Current children cumulated vsize (Kb) 121712 [startup+850.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29036 0 0 0 84668 154 0 0 25 0 1 0 1785077485 122724352 28019 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 29962 28019 145 145 0 29817 0 [pid=10837] vsize: 119848 Current children cumulated CPU time (s) 848.23 Current children cumulated vsize (Kb) 121972 [startup+860.081 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29155 0 0 0 85666 155 0 0 25 0 1 0 1785077485 123219968 28138 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 30083 28138 145 145 0 29938 0 [pid=10837] vsize: 120332 Current children cumulated CPU time (s) 858.22 Current children cumulated vsize (Kb) 122456 [startup+870.081 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29304 0 0 0 86664 156 0 0 25 0 1 0 1785077485 123826176 28287 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 30231 28287 145 145 0 30086 0 [pid=10837] vsize: 120924 Current children cumulated CPU time (s) 868.21 Current children cumulated vsize (Kb) 123048 [startup+880.082 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29361 0 0 0 87662 156 0 0 25 0 1 0 1785077485 124055552 28344 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 30287 28344 145 145 0 30142 0 [pid=10837] vsize: 121148 Current children cumulated CPU time (s) 878.19 Current children cumulated vsize (Kb) 123272 [startup+890.083 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29462 0 0 0 88661 157 0 0 25 0 1 0 1785077485 124456960 28445 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 30385 28445 145 145 0 30240 0 [pid=10837] vsize: 121540 Current children cumulated CPU time (s) 888.19 Current children cumulated vsize (Kb) 123664 [startup+900.084 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29530 0 0 0 89660 158 0 0 25 0 1 0 1785077485 124727296 28513 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 30451 28513 145 145 0 30306 0 [pid=10837] vsize: 121804 Current children cumulated CPU time (s) 898.19 Current children cumulated vsize (Kb) 123928 [startup+910.086 s] Raw data (loadavg): 0.99 0.97 0.99 3/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29598 0 0 0 90659 158 0 0 25 0 1 0 1785077485 124997632 28581 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 30517 28581 145 145 0 30372 0 [pid=10837] vsize: 122068 Current children cumulated CPU time (s) 908.18 Current children cumulated vsize (Kb) 124192 [startup+920.087 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29682 0 0 0 91658 159 0 0 25 0 1 0 1785077485 125337600 28665 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 30600 28665 145 145 0 30455 0 [pid=10837] vsize: 122400 Current children cumulated CPU time (s) 918.18 Current children cumulated vsize (Kb) 124524 [startup+930.087 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29766 0 0 0 92656 160 0 0 25 0 1 0 1785077485 125677568 28749 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 30683 28749 145 145 0 30538 0 [pid=10837] vsize: 122732 Current children cumulated CPU time (s) 928.17 Current children cumulated vsize (Kb) 124856 [startup+940.088 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29852 0 0 0 93655 160 0 0 25 0 1 0 1785077485 126025728 28835 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 30768 28835 145 145 0 30623 0 [pid=10837] vsize: 123072 Current children cumulated CPU time (s) 938.16 Current children cumulated vsize (Kb) 125196 [startup+950.089 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29940 0 0 0 94654 161 0 0 25 0 1 0 1785077485 126382080 28923 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 30855 28923 145 145 0 30710 0 [pid=10837] vsize: 123420 Current children cumulated CPU time (s) 948.16 Current children cumulated vsize (Kb) 125544 [startup+960.091 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 29992 0 0 0 95653 161 0 0 25 0 1 0 1785077485 126595072 28975 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 30907 28975 145 145 0 30762 0 [pid=10837] vsize: 123628 Current children cumulated CPU time (s) 958.15 Current children cumulated vsize (Kb) 125752 [startup+970.092 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 30173 0 0 0 96649 163 0 0 25 0 1 0 1785077485 127332352 29156 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 31087 29156 145 145 0 30942 0 [pid=10837] vsize: 124348 Current children cumulated CPU time (s) 968.13 Current children cumulated vsize (Kb) 126472 [startup+980.091 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 30314 0 0 0 97647 164 0 0 25 0 1 0 1785077485 127905792 29297 4294967295 134512640 135094434 3221224448 3221223104 134557818 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 31227 29297 145 145 0 31082 0 [pid=10837] vsize: 124908 Current children cumulated CPU time (s) 978.12 Current children cumulated vsize (Kb) 127032 [startup+990.092 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 30410 0 0 0 98645 165 0 0 25 0 1 0 1785077485 128299008 29393 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 31323 29393 145 145 0 31178 0 [pid=10837] vsize: 125292 Current children cumulated CPU time (s) 988.11 Current children cumulated vsize (Kb) 127416 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 30521 0 0 0 99643 166 0 0 25 0 1 0 1785077485 128749568 29504 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 31433 29504 145 145 0 31288 0 [pid=10837] vsize: 125732 Current children cumulated CPU time (s) 998.1 Current children cumulated vsize (Kb) 127856 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 30703 0 0 0 100640 168 0 0 25 0 1 0 1785077485 129495040 29686 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 31615 29686 145 145 0 31470 0 [pid=10837] vsize: 126460 Current children cumulated CPU time (s) 1008.09 Current children cumulated vsize (Kb) 128584 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 30867 0 0 0 101638 169 0 0 25 0 1 0 1785077485 130166784 29850 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 31779 29850 145 145 0 31634 0 [pid=10837] vsize: 127116 Current children cumulated CPU time (s) 1018.08 Current children cumulated vsize (Kb) 129240 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31055 0 0 0 102634 171 0 0 25 0 1 0 1785077485 130932736 30038 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 31966 30038 145 145 0 31821 0 [pid=10837] vsize: 127864 Current children cumulated CPU time (s) 1028.06 Current children cumulated vsize (Kb) 129988 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31243 0 0 0 103633 172 0 0 25 0 1 0 1785077485 131698688 30226 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 32153 30226 145 145 0 32008 0 [pid=10837] vsize: 128612 Current children cumulated CPU time (s) 1038.06 Current children cumulated vsize (Kb) 130736 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31443 0 0 0 104631 173 0 0 25 0 1 0 1785077485 132517888 30426 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 32353 30426 145 145 0 32208 0 [pid=10837] vsize: 129412 Current children cumulated CPU time (s) 1048.05 Current children cumulated vsize (Kb) 131536 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31632 0 0 0 105629 174 0 0 25 0 1 0 1785077485 133275648 30615 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 32538 30615 145 145 0 32393 0 [pid=10837] vsize: 130152 Current children cumulated CPU time (s) 1058.04 Current children cumulated vsize (Kb) 132276 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31794 0 0 0 106626 175 0 0 25 0 1 0 1785077485 133935104 30777 4294967295 134512640 135094434 3221224448 3221223040 134557141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 32699 30777 145 145 0 32554 0 [pid=10837] vsize: 130796 Current children cumulated CPU time (s) 1068.02 Current children cumulated vsize (Kb) 132920 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31890 0 0 0 107624 176 0 0 25 0 1 0 1785077485 134324224 30873 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 32794 30873 145 145 0 32649 0 [pid=10837] vsize: 131176 Current children cumulated CPU time (s) 1078.01 Current children cumulated vsize (Kb) 133300 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 31989 0 0 0 108623 177 0 0 25 0 1 0 1785077485 134729728 30972 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 32893 30972 145 145 0 32748 0 [pid=10837] vsize: 131572 Current children cumulated CPU time (s) 1088.01 Current children cumulated vsize (Kb) 133696 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32129 0 0 0 109621 177 0 0 25 0 1 0 1785077485 135299072 31112 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33032 31112 145 145 0 32887 0 [pid=10837] vsize: 132128 Current children cumulated CPU time (s) 1097.99 Current children cumulated vsize (Kb) 134252 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32275 0 0 0 110619 179 0 0 25 0 1 0 1785077485 135897088 31258 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33178 31258 145 145 0 33033 0 [pid=10837] vsize: 132712 Current children cumulated CPU time (s) 1107.99 Current children cumulated vsize (Kb) 134836 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32338 0 0 0 111617 179 0 0 25 0 1 0 1785077485 136142848 31321 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33238 31321 145 145 0 33093 0 [pid=10837] vsize: 132952 Current children cumulated CPU time (s) 1117.97 Current children cumulated vsize (Kb) 135076 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32389 0 0 0 112616 179 0 0 25 0 1 0 1785077485 136343552 31372 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33287 31372 145 145 0 33142 0 [pid=10837] vsize: 133148 Current children cumulated CPU time (s) 1127.96 Current children cumulated vsize (Kb) 135272 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32431 0 0 0 113616 180 0 0 25 0 1 0 1785077485 136507392 31414 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33327 31414 145 145 0 33182 0 [pid=10837] vsize: 133308 Current children cumulated CPU time (s) 1137.97 Current children cumulated vsize (Kb) 135432 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32457 0 0 0 114615 180 0 0 25 0 1 0 1785077485 136609792 31440 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33352 31440 145 145 0 33207 0 [pid=10837] vsize: 133408 Current children cumulated CPU time (s) 1147.96 Current children cumulated vsize (Kb) 135532 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32493 0 0 0 115615 180 0 0 25 0 1 0 1785077485 136753152 31476 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33387 31476 145 145 0 33242 0 [pid=10837] vsize: 133548 Current children cumulated CPU time (s) 1157.96 Current children cumulated vsize (Kb) 135672 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32596 0 0 0 116612 181 0 0 25 0 1 0 1785077485 137170944 31579 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33489 31579 145 145 0 33344 0 [pid=10837] vsize: 133956 Current children cumulated CPU time (s) 1167.94 Current children cumulated vsize (Kb) 136080 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32644 0 0 0 117611 181 0 0 25 0 1 0 1785077485 137363456 31627 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33536 31627 145 145 0 33391 0 [pid=10837] vsize: 134144 Current children cumulated CPU time (s) 1177.93 Current children cumulated vsize (Kb) 136268 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.99 3/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32720 0 0 0 118609 182 0 0 25 0 1 0 1785077485 137670656 31703 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33611 31703 145 145 0 33466 0 [pid=10837] vsize: 134444 Current children cumulated CPU time (s) 1187.92 Current children cumulated vsize (Kb) 136568 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 32821 0 0 0 119608 183 0 0 25 0 1 0 1785077485 138084352 31804 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33712 31804 145 145 0 33567 0 [pid=10837] vsize: 134848 Current children cumulated CPU time (s) 1197.92 Current children cumulated vsize (Kb) 136972 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 33020 0 0 0 120606 184 0 0 25 0 1 0 1785077485 138895360 32003 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33910 32003 145 145 0 33765 0 [pid=10837] vsize: 135640 Current children cumulated CPU time (s) 1207.91 Current children cumulated vsize (Kb) 137764 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 10837 Raw data (/proc/10833/stat): 10833 (minisat+_script) S 10832 10833 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1785077480 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/10833/statm): 531 226 485 147 0 384 0 [pid=10833] vsize: 2124 Raw data (/proc/10837/stat): 10837 (minisat+_64-bit) R 10833 10833 31778 0 -1 0 33020 0 0 0 120606 184 0 0 25 0 1 0 1785077485 138895360 32003 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10837/statm): 33910 32003 145 145 0 33765 0 [pid=10837] vsize: 135640 Current children cumulated CPU time (s) 1207.91 Current children cumulated vsize (Kb) 137764 Sending SIGTERM to -10833 Sleeping 2 seconds One traced child (pid=10833) ended because it received signal 15 (SIGTERM) One traced child (pid=10837) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.18 CPU time (s): 1207.97 CPU user time (s): 1206.06 CPU system time (s): 1.90971 CPU usage (%): 99.8178 Max. virtual memory (cumulated for all children) (Kb): 137764
ERROR: no interpretation found !