Name | web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-2.opb |
MD5SUM | 409f1cf0658f035df65cb61f3e4f598e |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -30 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 595 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 595 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 595 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.03 |
Number of variables | 595 |
Total number of constraints | 27847 |
Number of constraints which are clauses | 27847 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 2 |
LAUNCH ON wulflinc19 THE 2005-09-18 18:39:29 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2691 boxname=wulflinc19 idbench=347 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 409f1cf0658f035df65cb61f3e4f598e /oldhome/oroussel/tmp/wulflinc19/normalized-frb35-17-2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-frb35-17-2.opb IDLAUNCH: 2691 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 922200 kB Buffers: 34512 kB Cached: 50676 kB SwapCached: 832 kB Active: 60996 kB Inactive: 26816 kB HighTotal: 131008 kB HighFree: 79548 kB LowTotal: 903652 kB LowFree: 842652 kB SwapTotal: 2097892 kB SwapFree: 2096460 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5700 kB Slab: 18996 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:59:39 (client local time) WITH STATUS 10 IN 1209.38 SECONDS stats: 2691 7 1209.38 10
c Parsing PB file... c Converting 27847 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 | 27847 55694 | 9282 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -24[0m c ---[ 0]---> Sorter-cost:26814 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 56112 122082 | 18704 0 0 nan | 0.000 % | c | 100 | 55441 120669 | 20574 62 485 7.8 | 1.950 % | c | 252 | 54383 118381 | 22631 186 1801 9.7 | 5.130 % | c | 477 | 53349 116119 | 24895 313 3077 9.8 | 8.306 % | c | 814 | 51759 112535 | 27384 516 5065 9.8 | 13.461 % | c | 1321 | 49950 108452 | 30122 920 9543 10.4 | 19.341 % | c ============================================================================== c [1mFound solution: -26[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1658 | 48453 105089 | 16151 1166 13758 11.8 | 19.341 % | c | 1758 | 48207 104544 | 17766 1257 15573 12.4 | 25.098 % | c | 1908 | 47653 103297 | 19542 1386 16993 12.3 | 26.885 % | c | 2133 | 47022 101840 | 21496 1582 20176 12.8 | 29.018 % | c | 2471 | 45334 97977 | 23646 1783 22714 12.7 | 34.745 % | c | 2977 | 43116 92786 | 26011 2128 28051 13.2 | 41.789 % | c ============================================================================== c [1mFound solution: -27[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3108 | 42804 92166 | 14268 2242 29536 13.2 | 41.789 % | c | 3208 | 42633 91773 | 15694 2311 32120 13.9 | 43.581 % | c | 3358 | 42086 90483 | 17264 2410 34663 14.4 | 45.442 % | c | 3583 | 41186 88373 | 18990 2527 36936 14.6 | 48.512 % | c | 3920 | 39875 85257 | 20889 2675 39865 14.9 | 53.073 % | c | 4427 | 38250 81393 | 22978 2937 45919 15.6 | 58.815 % | c | 5186 | 37415 79400 | 25276 3573 58638 16.4 | 61.715 % | c ============================================================================== c [1mFound solution: -28[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5777 | 36536 77244 | 12178 3923 69803 17.8 | 61.715 % | c | 5877 | 36375 76873 | 13395 4009 70834 17.7 | 65.308 % | c | 6027 | 36111 76265 | 14735 4119 72852 17.7 | 66.182 % | c | 6252 | 35833 75598 | 16208 4304 78604 18.3 | 67.328 % | c | 6590 | 35525 74869 | 17829 4581 87877 19.2 | 68.259 % | c | 7096 | 35132 73939 | 19612 5015 102250 20.4 | 69.626 % | c | 7855 | 35004 73641 | 21574 5721 119858 21.0 | 70.063 % | c | 8994 | 34621 72729 | 23731 6710 156327 23.3 | 71.405 % | c | 10702 | 34449 72319 | 26104 8303 266846 32.1 | 72.007 % | c ============================================================================== c [1mFound solution: -29[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10930 | 34398 72230 | 11466 8491 276955 32.6 | 72.007 % | c | 11030 | 34307 72002 | 12612 8543 279040 32.7 | 72.564 % | c | 11180 | 34307 72002 | 13873 8693 286044 32.9 | 72.564 % | c | 11405 | 34227 71812 | 15261 8862 292699 33.0 | 72.846 % | c | 11743 | 33985 71231 | 16787 9032 296460 32.8 | 73.704 % | c | 12250 | 33985 71231 | 18466 9539 330834 34.7 | 73.704 % | c | 13010 | 33963 71183 | 20312 10270 353365 34.4 | 73.770 % | c | 14149 | 33552 70232 | 22343 11249 423515 37.6 | 75.141 % | c | 15857 | 33222 69433 | 24578 12762 568784 44.6 | 76.291 % | c | 18419 | 33120 69188 | 27036 15273 761555 49.9 | 76.651 % | c | 22263 | 32930 68727 | 29739 18985 1120606 59.0 | 77.344 % | c ============================================================================== c [1mFound solution: -30[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26467 | 32657 68028 | 10885 22867 1465252 64.1 | 77.344 % | c | 26567 | 32647 68006 | 11973 22966 1468382 63.9 | 78.332 % | c | 26717 | 32647 68006 | 13170 23116 1476425 63.9 | 78.332 % | c | 26942 | 32647 68006 | 14487 23341 1495373 64.1 | 78.332 % | c | 27279 | 32477 67592 | 15936 23347 1512616 64.8 | 78.938 % | c | 27785 | 32364 67313 | 17530 23764 1543363 64.9 | 79.364 % | c | 28544 | 32254 67045 | 19283 24353 1597203 65.6 | 79.764 % | c | 29683 | 32254 67045 | 21211 25492 1710400 67.1 | 79.764 % | c | 31391 | 32254 67045 | 23332 27200 1919412 70.6 | 79.764 % | c | 33955 | 32254 67045 | 25666 29764 2101826 70.6 | 79.764 % | c ============================================================================== c [1mFound solution: -31[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35137 | 31980 66414 | 10660 30812 2169138 70.4 | 79.764 % | c | 35238 | 31946 66328 | 11726 15491 930133 60.0 | 80.939 % | c | 35389 | 31915 66258 | 12898 15639 935925 59.8 | 81.041 % | c | 35614 | 31915 66258 | 14188 15864 948886 59.8 | 81.041 % | c | 35951 | 31915 66258 | 15607 16201 965361 59.6 | 81.041 % | c | 36458 | 31915 66258 | 17168 16708 996138 59.6 | 81.041 % | c | 37217 | 31915 66258 | 18884 17467 1044393 59.8 | 81.041 % | c | 38357 | 31910 66247 | 20773 18600 1113004 59.8 | 81.056 % | c | 40065 | 31845 66095 | 22850 20288 1216954 60.0 | 81.276 % | c | 42627 | 31804 65994 | 25135 22834 1375865 60.3 | 81.429 % | c | 46471 | 31804 65994 | 27649 26678 1735048 65.0 | 81.429 % | c | 52237 | 31510 65286 | 30414 32374 2209723 68.3 | 82.477 % | c | 60886 | 31481 65217 | 33455 40961 2771939 67.7 | 82.579 % | c | 73860 | 31477 65205 | 36801 19710 946500 48.0 | 82.600 % | c | 93322 | 31477 65205 | 40481 39172 2462580 62.9 | 82.600 % | c ============================================================================== c [1mFound solution: -32[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 98887 | 31443 65100 | 10481 44676 2833202 63.4 | 82.600 % | c | 98987 | 31443 65100 | 11529 17731 914127 51.6 | 82.724 % | c | 99137 | 31443 65100 | 12682 17881 921601 51.5 | 82.724 % | c | 99362 | 31405 65004 | 13950 18104 938348 51.8 | 82.867 % | c | 99699 | 31381 64946 | 15345 18412 962309 52.3 | 82.954 % | c | 100205 | 31381 64946 | 16879 18918 1006461 53.2 | 82.954 % | c | 100964 | 31370 64919 | 18567 19674 1054745 53.6 | 82.995 % | c | 102103 | 31370 64919 | 20424 20813 1143158 54.9 | 82.995 % | c | 103813 | 31365 64908 | 22466 22519 1262523 56.1 | 83.011 % | c | 106376 | 31365 64908 | 24713 25082 1418165 56.5 | 83.011 % | c | 110222 | 31365 64908 | 27185 28928 1703939 58.9 | 83.011 % | c | 115988 | 31330 64825 | 29903 34689 2037716 58.7 | 83.133 % | c | 124637 | 31284 64708 | 32893 43252 2666638 61.7 | 83.307 % | c | 137612 | 31239 64605 | 36183 22486 988221 43.9 | 83.450 % | c | 157073 | 31239 64605 | 39801 41947 2056155 49.0 | 83.450 % | c | 186265 | 31236 64598 | 43781 31773 1941768 61.1 | 83.460 % | c | 230054 | 31231 64587 | 48159 32261 2906002 90.1 | 83.476 % | c ============================================================================== c [1mFound solution: -33[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 278557 | 31244 64621 | 10414 32296 2237077 69.3 | 83.476 % | c | 278658 | 31244 64621 | 11455 16249 954352 58.7 | 83.452 % | c | 278809 | 31244 64621 | 12600 16400 966097 58.9 | 83.452 % | c | 279034 | 31244 64621 | 13861 16625 981948 59.1 | 83.452 % | c | 279372 | 31244 64621 | 15247 16963 1000566 59.0 | 83.452 % | c | 279878 | 31244 64621 | 16771 17469 1034794 59.2 | 83.452 % | c | 280638 | 31244 64621 | 18449 18229 1067205 58.5 | 83.452 % | c | 281777 | 31244 64621 | 20293 19368 1125638 58.1 | 83.452 % | c | 283486 | 31244 64621 | 22323 21077 1208886 57.4 | 83.452 % | c | 286048 | 31244 64621 | 24555 23639 1365631 57.8 | 83.452 % | c | 289893 | 31244 64621 | 27011 27484 1608741 58.5 | 83.452 % | c | 295659 | 31207 64527 | 29712 33206 1964370 59.2 | 83.595 % | c | 304308 | 31207 64527 | 32683 41855 2460979 58.8 | 83.595 % | c | 317282 | 31197 64503 | 35951 22333 712494 31.9 | 83.630 % | c | 336743 | 31197 64503 | 39547 41794 1397205 33.4 | 83.630 % | c | 365935 | 31193 64493 | 43501 34344 952519 27.7 | 83.646 % | c | 409725 | 31143 64373 | 47852 34709 1222470 35.2 | 83.824 % | c | 475409 | 31136 64358 | 52637 54302 1647686 30.3 | 83.845 % | c | 573935 | 31106 64290 | 57900 50437 1608080 31.9 | 83.942 % |
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/12763/stat): 12763 (minisat+_script) R 12762 12763 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843466770 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/12763/statm): 174 3 169 147 0 27 0 [pid=12763] 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=12764 New process pid=12765 New process pid=12766 execve syscall for /bin/sed executable One traced child (pid=12765) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=12766) exited with status: 0 One traced child (pid=12764) exited with status: 0 New process pid=12767 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-frb35-17-2.opb [startup+10.0042 s] Raw data (loadavg): 1.00 0.95 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 2152 0 0 0 979 8 0 0 25 0 1 0 1843466775 9752576 2139 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 2381 2139 145 145 0 2236 0 [pid=12767] vsize: 9524 Current children cumulated CPU time (s) 9.88 Current children cumulated vsize (Kb) 11648 [startup+20.006 s] Raw data (loadavg): 1.00 0.95 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 2235 0 0 0 1978 9 0 0 25 0 1 0 1843466775 10092544 2222 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 2464 2222 145 145 0 2319 0 [pid=12767] vsize: 9856 Current children cumulated CPU time (s) 19.88 Current children cumulated vsize (Kb) 11980 [startup+30.0068 s] Raw data (loadavg): 1.00 0.95 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 2852 0 0 0 2968 14 0 0 25 0 1 0 1843466775 12619776 2839 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 3081 2839 145 145 0 2936 0 [pid=12767] vsize: 12324 Current children cumulated CPU time (s) 29.83 Current children cumulated vsize (Kb) 14448 [startup+40.0076 s] Raw data (loadavg): 1.00 0.95 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 3528 0 0 0 3954 21 0 0 25 0 1 0 1843466775 15429632 3515 4294967295 134512640 135094434 3221224448 3221223120 134556242 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 3767 3515 145 145 0 3622 0 [pid=12767] vsize: 15068 Current children cumulated CPU time (s) 39.76 Current children cumulated vsize (Kb) 17192 [startup+50.0094 s] Raw data (loadavg): 1.00 0.95 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 3944 0 0 0 4946 25 0 0 25 0 1 0 1843466775 17117184 3931 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 4179 3931 145 145 0 4034 0 [pid=12767] vsize: 16716 Current children cumulated CPU time (s) 49.72 Current children cumulated vsize (Kb) 18840 [startup+60.0092 s] Raw data (loadavg): 1.00 0.95 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 4465 0 0 0 5935 29 0 0 25 0 1 0 1843466775 19230720 4452 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 4695 4452 145 145 0 4550 0 [pid=12767] vsize: 18780 Current children cumulated CPU time (s) 59.65 Current children cumulated vsize (Kb) 20904 [startup+70.01 s] Raw data (loadavg): 1.00 0.95 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 4549 0 0 0 6933 30 0 0 25 0 1 0 1843466775 19570688 4536 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 4778 4536 145 145 0 4633 0 [pid=12767] vsize: 19112 Current children cumulated CPU time (s) 69.64 Current children cumulated vsize (Kb) 21236 [startup+80.0108 s] Raw data (loadavg): 1.00 0.95 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 4549 0 0 0 7933 30 0 0 25 0 1 0 1843466775 19570688 4536 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 4778 4536 145 145 0 4633 0 [pid=12767] vsize: 19112 Current children cumulated CPU time (s) 79.64 Current children cumulated vsize (Kb) 21236 [startup+90.0116 s] Raw data (loadavg): 1.00 0.96 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 4587 0 0 0 8932 30 0 0 25 0 1 0 1843466775 19722240 4574 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 4815 4574 145 145 0 4670 0 [pid=12767] vsize: 19260 Current children cumulated CPU time (s) 89.63 Current children cumulated vsize (Kb) 21384 [startup+100.012 s] Raw data (loadavg): 1.00 0.96 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 4987 0 0 0 9925 34 0 0 25 0 1 0 1843466775 21471232 4974 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 5242 4974 145 145 0 5097 0 [pid=12767] vsize: 20968 Current children cumulated CPU time (s) 99.6 Current children cumulated vsize (Kb) 23092 [startup+110.013 s] Raw data (loadavg): 1.00 0.96 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 5352 0 0 0 10918 37 0 0 25 0 1 0 1843466775 22949888 5339 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 5603 5339 145 145 0 5458 0 [pid=12767] vsize: 22412 Current children cumulated CPU time (s) 109.56 Current children cumulated vsize (Kb) 24536 [startup+120.014 s] Raw data (loadavg): 1.00 0.96 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 5673 0 0 0 11911 41 0 0 25 0 1 0 1843466775 24244224 5660 4294967295 134512640 135094434 3221224448 3221223040 134557531 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 5919 5660 145 145 0 5774 0 [pid=12767] vsize: 23676 Current children cumulated CPU time (s) 119.53 Current children cumulated vsize (Kb) 25800 [startup+130.015 s] Raw data (loadavg): 1.00 0.96 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 5963 0 0 0 12906 43 0 0 25 0 1 0 1843466775 25415680 5950 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6205 5950 145 145 0 6060 0 [pid=12767] vsize: 24820 Current children cumulated CPU time (s) 129.5 Current children cumulated vsize (Kb) 26944 [startup+140.016 s] Raw data (loadavg): 1.00 0.96 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6040 0 0 0 13905 44 0 0 25 0 1 0 1843466775 25726976 6027 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6281 6027 145 145 0 6136 0 [pid=12767] vsize: 25124 Current children cumulated CPU time (s) 139.5 Current children cumulated vsize (Kb) 27248 [startup+150.016 s] Raw data (loadavg): 1.00 0.96 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6040 0 0 0 14905 44 0 0 25 0 1 0 1843466775 25726976 6027 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6281 6027 145 145 0 6136 0 [pid=12767] vsize: 25124 Current children cumulated CPU time (s) 149.5 Current children cumulated vsize (Kb) 27248 [startup+160.016 s] Raw data (loadavg): 1.00 0.96 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6040 0 0 0 15904 44 0 0 25 0 1 0 1843466775 25726976 6027 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6281 6027 145 145 0 6136 0 [pid=12767] vsize: 25124 Current children cumulated CPU time (s) 159.49 Current children cumulated vsize (Kb) 27248 [startup+170.017 s] Raw data (loadavg): 1.00 0.96 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6040 0 0 0 16904 44 0 0 25 0 1 0 1843466775 25726976 6027 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6281 6027 145 145 0 6136 0 [pid=12767] vsize: 25124 Current children cumulated CPU time (s) 169.49 Current children cumulated vsize (Kb) 27248 [startup+180.018 s] Raw data (loadavg): 1.00 0.96 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6040 0 0 0 17903 45 0 0 25 0 1 0 1843466775 25726976 6027 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6281 6027 145 145 0 6136 0 [pid=12767] vsize: 25124 Current children cumulated CPU time (s) 179.49 Current children cumulated vsize (Kb) 27248 [startup+190.02 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 18903 45 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 189.49 Current children cumulated vsize (Kb) 27404 [startup+200.02 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 19903 46 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 199.5 Current children cumulated vsize (Kb) 27404 [startup+210.02 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 20902 46 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 209.49 Current children cumulated vsize (Kb) 27404 [startup+220.022 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 21902 47 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 219.5 Current children cumulated vsize (Kb) 27404 [startup+230.023 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 22901 47 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 229.49 Current children cumulated vsize (Kb) 27404 [startup+240.024 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 23899 49 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 239.49 Current children cumulated vsize (Kb) 27404 [startup+250.025 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 24898 51 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 249.5 Current children cumulated vsize (Kb) 27404 [startup+260.025 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 25897 51 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 259.49 Current children cumulated vsize (Kb) 27404 [startup+270.026 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 26896 52 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223088 134562165 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 269.49 Current children cumulated vsize (Kb) 27404 [startup+280.027 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 27895 53 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223136 134554793 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 279.49 Current children cumulated vsize (Kb) 27404 [startup+290.029 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 28895 53 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 289.49 Current children cumulated vsize (Kb) 27404 [startup+300.03 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 29894 54 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 299.49 Current children cumulated vsize (Kb) 27404 [startup+310.029 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 30894 55 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 309.5 Current children cumulated vsize (Kb) 27404 [startup+320.03 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6062 0 0 0 31893 55 0 0 25 0 1 0 1843466775 25886720 6049 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6320 6049 145 145 0 6175 0 [pid=12767] vsize: 25280 Current children cumulated CPU time (s) 319.49 Current children cumulated vsize (Kb) 27404 [startup+330.031 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6088 0 0 0 32892 56 0 0 25 0 1 0 1843466775 25980928 6075 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6343 6075 145 145 0 6198 0 [pid=12767] vsize: 25372 Current children cumulated CPU time (s) 329.49 Current children cumulated vsize (Kb) 27496 [startup+340.032 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6088 0 0 0 33892 56 0 0 25 0 1 0 1843466775 25980928 6075 4294967295 134512640 135094434 3221224448 3221223040 134556847 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6343 6075 145 145 0 6198 0 [pid=12767] vsize: 25372 Current children cumulated CPU time (s) 339.49 Current children cumulated vsize (Kb) 27496 [startup+350.033 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6088 0 0 0 34892 57 0 0 25 0 1 0 1843466775 25980928 6075 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6343 6075 145 145 0 6198 0 [pid=12767] vsize: 25372 Current children cumulated CPU time (s) 349.5 Current children cumulated vsize (Kb) 27496 [startup+360.033 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6088 0 0 0 35892 57 0 0 25 0 1 0 1843466775 25980928 6075 4294967295 134512640 135094434 3221224448 3221223120 134555991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6343 6075 145 145 0 6198 0 [pid=12767] vsize: 25372 Current children cumulated CPU time (s) 359.5 Current children cumulated vsize (Kb) 27496 [startup+370.034 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6093 0 0 0 36891 57 0 0 25 0 1 0 1843466775 26009600 6080 4294967295 134512640 135094434 3221224448 3221223072 134557675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6350 6080 145 145 0 6205 0 [pid=12767] vsize: 25400 Current children cumulated CPU time (s) 369.49 Current children cumulated vsize (Kb) 27524 [startup+380.035 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6093 0 0 0 37890 58 0 0 25 0 1 0 1843466775 26009600 6080 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6350 6080 145 145 0 6205 0 [pid=12767] vsize: 25400 Current children cumulated CPU time (s) 379.49 Current children cumulated vsize (Kb) 27524 [startup+390.036 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6496 0 0 0 38882 62 0 0 25 0 1 0 1843466775 27660288 6483 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 6753 6483 145 145 0 6608 0 [pid=12767] vsize: 27012 Current children cumulated CPU time (s) 389.45 Current children cumulated vsize (Kb) 29136 [startup+400.038 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6873 0 0 0 39875 65 0 0 25 0 1 0 1843466775 29208576 6860 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 7131 6860 145 145 0 6986 0 [pid=12767] vsize: 28524 Current children cumulated CPU time (s) 399.41 Current children cumulated vsize (Kb) 30648 [startup+410.038 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7325 0 0 0 40865 69 0 0 25 0 1 0 1843466775 31059968 7312 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 7583 7312 145 145 0 7438 0 [pid=12767] vsize: 30332 Current children cumulated CPU time (s) 409.35 Current children cumulated vsize (Kb) 32456 [startup+420.039 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 41857 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223120 134556450 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0 [pid=12767] vsize: 31884 Current children cumulated CPU time (s) 419.3 Current children cumulated vsize (Kb) 34008 [startup+430.04 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 42857 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0 [pid=12767] vsize: 31884 Current children cumulated CPU time (s) 429.3 Current children cumulated vsize (Kb) 34008 [startup+440.041 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 43857 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134558141 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0 [pid=12767] vsize: 31884 Current children cumulated CPU time (s) 439.3 Current children cumulated vsize (Kb) 34008 [startup+450.042 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 44858 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0 [pid=12767] vsize: 31884 Current children cumulated CPU time (s) 449.31 Current children cumulated vsize (Kb) 34008 [startup+460.041 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 45858 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0 [pid=12767] vsize: 31884 Current children cumulated CPU time (s) 459.31 Current children cumulated vsize (Kb) 34008 [startup+470.042 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 46858 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0 [pid=12767] vsize: 31884 Current children cumulated CPU time (s) 469.31 Current children cumulated vsize (Kb) 34008 [startup+480.042 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 47858 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0 [pid=12767] vsize: 31884 Current children cumulated CPU time (s) 479.31 Current children cumulated vsize (Kb) 34008 [startup+490.043 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 48858 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0 [pid=12767] vsize: 31884 Current children cumulated CPU time (s) 489.31 Current children cumulated vsize (Kb) 34008 [startup+500.044 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 49859 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0 [pid=12767] vsize: 31884 Current children cumulated CPU time (s) 499.32 Current children cumulated vsize (Kb) 34008 [startup+510.043 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7988 0 0 0 50854 74 0 0 25 0 1 0 1843466775 33763328 7975 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8243 7975 145 145 0 8098 0 [pid=12767] vsize: 32972 Current children cumulated CPU time (s) 509.29 Current children cumulated vsize (Kb) 35096 [startup+520.044 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8273 0 0 0 51849 77 0 0 25 0 1 0 1843466775 34926592 8260 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8527 8260 145 145 0 8382 0 [pid=12767] vsize: 34108 Current children cumulated CPU time (s) 519.27 Current children cumulated vsize (Kb) 36232 [startup+530.045 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8543 0 0 0 52844 79 0 0 25 0 1 0 1843466775 36032512 8530 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8797 8530 145 145 0 8652 0 [pid=12767] vsize: 35188 Current children cumulated CPU time (s) 529.24 Current children cumulated vsize (Kb) 37312 [startup+540.046 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 53844 79 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557859 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 539.24 Current children cumulated vsize (Kb) 37792 [startup+550.047 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 54844 79 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 549.24 Current children cumulated vsize (Kb) 37792 [startup+560.048 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 55844 80 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223236 134553508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 559.25 Current children cumulated vsize (Kb) 37792 [startup+570.048 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 56843 80 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 569.24 Current children cumulated vsize (Kb) 37792 [startup+580.049 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 57842 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 579.24 Current children cumulated vsize (Kb) 37792 [startup+590.05 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 58842 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 589.24 Current children cumulated vsize (Kb) 37792 [startup+600.051 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 59842 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 599.24 Current children cumulated vsize (Kb) 37792 [startup+610.051 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 60842 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 609.24 Current children cumulated vsize (Kb) 37792 [startup+620.051 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 61843 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 619.25 Current children cumulated vsize (Kb) 37792 [startup+630.052 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 62843 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 629.25 Current children cumulated vsize (Kb) 37792 [startup+640.053 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 63843 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223072 134557583 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 639.25 Current children cumulated vsize (Kb) 37792 [startup+650.054 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 64843 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 649.25 Current children cumulated vsize (Kb) 37792 [startup+660.055 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 65843 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 659.25 Current children cumulated vsize (Kb) 37792 [startup+670.055 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 66844 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 669.26 Current children cumulated vsize (Kb) 37792 [startup+680.055 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 67844 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 679.26 Current children cumulated vsize (Kb) 37792 [startup+690.056 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 68844 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 689.26 Current children cumulated vsize (Kb) 37792 [startup+700.057 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 69844 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 699.26 Current children cumulated vsize (Kb) 37792 [startup+710.057 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 70844 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 709.26 Current children cumulated vsize (Kb) 37792 [startup+720.057 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 71844 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 719.26 Current children cumulated vsize (Kb) 37792 [startup+730.057 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 72845 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223120 134556288 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 729.27 Current children cumulated vsize (Kb) 37792 [startup+740.058 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 73845 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 739.27 Current children cumulated vsize (Kb) 37792 [startup+750.059 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 74845 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134558172 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 749.27 Current children cumulated vsize (Kb) 37792 [startup+760.059 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 75845 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 759.27 Current children cumulated vsize (Kb) 37792 [startup+770.059 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 76846 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 769.28 Current children cumulated vsize (Kb) 37792 [startup+780.06 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 77846 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 779.28 Current children cumulated vsize (Kb) 37792 [startup+790.061 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 78846 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 789.28 Current children cumulated vsize (Kb) 37792 [startup+800.062 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 79846 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 799.28 Current children cumulated vsize (Kb) 37792 [startup+810.063 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 80846 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223120 134556244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 809.28 Current children cumulated vsize (Kb) 37792 [startup+820.063 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 81846 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 819.28 Current children cumulated vsize (Kb) 37792 [startup+830.064 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 82847 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 829.29 Current children cumulated vsize (Kb) 37792 [startup+840.065 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 83847 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 839.29 Current children cumulated vsize (Kb) 37792 [startup+850.066 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 84847 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 849.29 Current children cumulated vsize (Kb) 37792 [startup+860.067 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 85847 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223040 134556817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 859.29 Current children cumulated vsize (Kb) 37792 [startup+870.067 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 86847 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 869.29 Current children cumulated vsize (Kb) 37792 [startup+880.068 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 87848 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 879.3 Current children cumulated vsize (Kb) 37792 [startup+890.07 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 88848 82 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223120 134555889 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 889.31 Current children cumulated vsize (Kb) 37792 [startup+900.071 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 89848 82 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 899.31 Current children cumulated vsize (Kb) 37792 [startup+910.072 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 90848 82 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 909.31 Current children cumulated vsize (Kb) 37792 [startup+920.073 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 91849 82 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 919.32 Current children cumulated vsize (Kb) 37792 [startup+930.073 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 92849 82 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 929.32 Current children cumulated vsize (Kb) 37792 [startup+940.074 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 93849 82 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 939.32 Current children cumulated vsize (Kb) 37792 [startup+950.076 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 94848 83 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0 [pid=12767] vsize: 35668 Current children cumulated CPU time (s) 949.32 Current children cumulated vsize (Kb) 37792 [startup+960.076 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8615 0 0 0 95847 83 0 0 25 0 1 0 1843466775 36638720 8602 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8602 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 959.31 Current children cumulated vsize (Kb) 37904 [startup+970.077 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8616 0 0 0 96848 83 0 0 25 0 1 0 1843466775 36638720 8603 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8603 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 969.32 Current children cumulated vsize (Kb) 37904 [startup+980.077 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 97848 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 979.32 Current children cumulated vsize (Kb) 37904 [startup+990.078 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 98848 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 989.32 Current children cumulated vsize (Kb) 37904 [startup+1000.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 99848 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 999.32 Current children cumulated vsize (Kb) 37904 [startup+1010.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 100848 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1009.32 Current children cumulated vsize (Kb) 37904 [startup+1020.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 101849 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223040 134557137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1019.33 Current children cumulated vsize (Kb) 37904 [startup+1030.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 102849 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223120 134556242 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1029.33 Current children cumulated vsize (Kb) 37904 [startup+1040.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 103849 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1039.33 Current children cumulated vsize (Kb) 37904 [startup+1050.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 104849 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1049.33 Current children cumulated vsize (Kb) 37904 [startup+1060.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 105849 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1059.33 Current children cumulated vsize (Kb) 37904 [startup+1070.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 106849 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1069.33 Current children cumulated vsize (Kb) 37904 [startup+1080.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 107850 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1079.34 Current children cumulated vsize (Kb) 37904 [startup+1090.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 108850 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223040 134557331 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1089.34 Current children cumulated vsize (Kb) 37904 [startup+1100.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 109850 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1099.34 Current children cumulated vsize (Kb) 37904 [startup+1110.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 110850 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1109.34 Current children cumulated vsize (Kb) 37904 [startup+1120.08 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 111850 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1119.34 Current children cumulated vsize (Kb) 37904 [startup+1130.09 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 112851 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1129.35 Current children cumulated vsize (Kb) 37904 [startup+1140.09 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 113851 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1139.35 Current children cumulated vsize (Kb) 37904 [startup+1150.09 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 114850 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1149.34 Current children cumulated vsize (Kb) 37904 [startup+1160.09 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 115850 84 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1159.35 Current children cumulated vsize (Kb) 37904 [startup+1170.09 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 116851 84 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1169.36 Current children cumulated vsize (Kb) 37904 [startup+1180.09 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 117851 84 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1179.36 Current children cumulated vsize (Kb) 37904 [startup+1190.09 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8626 0 0 0 118851 84 0 0 25 0 1 0 1843466775 36638720 8613 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8613 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1189.36 Current children cumulated vsize (Kb) 37904 [startup+1200.09 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8627 0 0 0 119851 84 0 0 25 0 1 0 1843466775 36638720 8614 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8614 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1199.36 Current children cumulated vsize (Kb) 37904 [startup+1210.09 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8627 0 0 0 120851 84 0 0 25 0 1 0 1843466775 36638720 8614 4294967295 134512640 135094434 3221224448 3221223072 134562152 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8614 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1209.36 Current children cumulated vsize (Kb) 37904 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 1.00 0.97 0.95 2/57 12767 Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12763/statm): 531 226 485 147 0 384 0 [pid=12763] vsize: 2124 Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8627 0 0 0 120851 84 0 0 25 0 1 0 1843466775 36638720 8614 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12767/statm): 8945 8614 145 145 0 8800 0 [pid=12767] vsize: 35780 Current children cumulated CPU time (s) 1209.36 Current children cumulated vsize (Kb) 37904 Sending SIGTERM to -12763 Sleeping 2 seconds One traced child (pid=12763) ended because it received signal 15 (SIGTERM) One traced child (pid=12767) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.11 CPU time (s): 1209.38 CPU user time (s): 1208.52 CPU system time (s): 0.861868 CPU usage (%): 99.9396 Max. virtual memory (cumulated for all children) (Kb): 37904
ERROR: no interpretation found !