Name | submitted/manquinho/logic-synthesis/normalized-e64.b.opb |
MD5SUM | bf7f8537c6faa135d25c67c53576abb5 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 51 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 608 |
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 | 608 |
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 | 608 |
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.16 |
Number of variables | 607 |
Total number of constraints | 1053 |
Number of constraints which are clauses | 1022 |
Number of constraints which are cardinality constraints (but not clauses) | 31 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 3 |
Maximum length of a constraint | 32 |
LAUNCH ON wulflinc31 THE 2005-09-18 12:44:21 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2408 boxname=wulflinc31 idbench=64 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: bf7f8537c6faa135d25c67c53576abb5 /oldhome/oroussel/tmp/wulflinc31/normalized-e64.b.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc31/normalized-e64.b.opb IDLAUNCH: 2408 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 716528 kB Buffers: 35364 kB Cached: 252280 kB SwapCached: 1016 kB Active: 92892 kB Inactive: 197540 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 716276 kB SwapTotal: 2097892 kB SwapFree: 2096404 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5768 kB Slab: 21988 kB Committed_AS: 64376 kB PageTables: 340 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 13:04:31 (client local time) WITH STATUS 10 IN 1209.32 SECONDS stats: 2408 7 1209.32 10
c Parsing PB file... c Converting 1022 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 | 1022 8200 | 340 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 82[0m c ---[ 0]---> Sorter-cost:27428 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1 | 32888 82605 | 10962 1 16 16.0 | 0.000 % | c | 101 | 32731 82280 | 12058 94 1328 14.1 | 0.441 % | c | 251 | 32731 82280 | 13264 244 4888 20.0 | 0.441 % | c | 476 | 32693 82200 | 14590 467 9207 19.7 | 0.538 % | c | 815 | 32655 82120 | 16049 805 14538 18.1 | 0.636 % | c ============================================================================== c [1mFound solution: 64[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1118 | 32544 81867 | 10848 1108 20015 18.1 | 0.636 % | c | 1219 | 32544 81867 | 11932 1209 21890 18.1 | 1.342 % | c | 1371 | 32544 81867 | 13126 1361 27251 20.0 | 1.342 % | c | 1597 | 32544 81867 | 14438 1587 32001 20.2 | 1.342 % | c | 1935 | 32544 81867 | 15882 1925 44062 22.9 | 1.342 % | c | 2442 | 32526 81825 | 17470 2426 58440 24.1 | 1.397 % | c | 3201 | 32524 81821 | 19217 3182 81772 25.7 | 1.402 % | c | 4340 | 32524 81821 | 21139 4321 124438 28.8 | 1.402 % | c | 6049 | 32524 81821 | 23253 6030 236669 39.2 | 1.402 % | c | 8611 | 32524 81821 | 25579 8592 404633 47.1 | 1.402 % | c | 12456 | 32524 81821 | 28136 12437 881628 70.9 | 1.402 % | c ============================================================================== c [1mFound solution: 57[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17530 | 32583 81971 | 10861 17511 1261267 72.0 | 1.402 % | c | 17631 | 32583 81971 | 11947 8857 728551 82.3 | 1.404 % | c | 17781 | 32557 81915 | 13141 9005 733381 81.4 | 1.474 % | c | 18007 | 32557 81915 | 14455 9231 741448 80.3 | 1.474 % | c | 18344 | 32557 81915 | 15901 9568 749366 78.3 | 1.474 % | c | 18850 | 32557 81915 | 17491 10074 785392 78.0 | 1.474 % | c | 19609 | 32557 81915 | 19240 10833 859333 79.3 | 1.474 % | c | 20748 | 32557 81915 | 21165 11972 919844 76.8 | 1.474 % | c | 22458 | 32557 81915 | 23281 13682 1056358 77.2 | 1.474 % | c | 25020 | 32557 81915 | 25609 16244 1287855 79.3 | 1.474 % | c ============================================================================== c [1mFound solution: 55[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25537 | 32576 81969 | 10858 16761 1329272 79.3 | 1.474 % | c | 25637 | 32576 81969 | 11943 8481 589547 69.5 | 1.477 % | c | 25787 | 32576 81969 | 13138 8631 595037 68.9 | 1.477 % | c | 26012 | 32576 81969 | 14451 8856 607205 68.6 | 1.477 % | c | 26349 | 32576 81969 | 15897 9193 625383 68.0 | 1.477 % | c | 26855 | 32576 81969 | 17486 9699 645599 66.6 | 1.477 % | c | 27616 | 32576 81969 | 19235 10460 688721 65.8 | 1.477 % | c | 28755 | 32576 81969 | 21159 11599 760883 65.6 | 1.477 % | c | 30463 | 32576 81969 | 23275 13307 926598 69.6 | 1.477 % | c | 33026 | 32576 81969 | 25602 15870 1052589 66.3 | 1.477 % | c | 36872 | 32576 81969 | 28162 19716 1313125 66.6 | 1.477 % | c | 42638 | 32540 81893 | 30979 25472 1707177 67.0 | 1.570 % | c | 51288 | 32540 81893 | 34077 13453 850735 63.2 | 1.570 % | c | 64262 | 32540 81893 | 37484 26427 1854535 70.2 | 1.570 % | c ============================================================================== c [1mFound solution: 53[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 71120 | 32558 81945 | 10852 33285 2473346 74.3 | 1.570 % | c | 71222 | 32558 81945 | 11937 6680 548160 82.1 | 1.583 % | c | 71372 | 32558 81945 | 13130 6830 551418 80.7 | 1.583 % | c | 71597 | 32558 81945 | 14444 7055 563546 79.9 | 1.583 % | c | 71934 | 32558 81945 | 15888 7392 572407 77.4 | 1.583 % | c | 72440 | 32558 81945 | 17477 7898 589289 74.6 | 1.583 % | c | 73199 | 32558 81945 | 19224 8657 630654 72.8 | 1.583 % | c | 74340 | 32558 81945 | 21147 9798 684750 69.9 | 1.583 % | c | 76048 | 32558 81945 | 23262 11506 842785 73.2 | 1.583 % | c | 78611 | 32558 81945 | 25588 14069 1080790 76.8 | 1.583 % | c | 82457 | 32558 81945 | 28147 17915 1447445 80.8 | 1.583 % | c | 88223 | 32558 81945 | 30962 23681 1883985 79.6 | 1.583 % | c | 96872 | 32558 81945 | 34058 32330 2567295 79.4 | 1.583 % | c | 109848 | 32558 81945 | 37464 21298 1707483 80.2 | 1.583 % | c | 129309 | 32558 81945 | 41210 13470 1145174 85.0 | 1.583 % | c | 158501 | 32558 81945 | 45331 42662 3823977 89.6 | 1.583 % | c | 202290 | 32558 81945 | 49864 18699 1418328 75.9 | 1.583 % | c | 267976 | 32558 81945 | 54851 46288 3760997 81.3 | 1.583 % | c | 366502 | 32558 81945 | 60336 17595 1604710 91.2 | 1.583 % |
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/11981/stat): 11981 (minisat+_script) R 11980 11981 9102 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841311762 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/11981/statm): 174 3 169 147 0 27 0 [pid=11981] 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=11982 New process pid=11983 New process pid=11984 execve syscall for /bin/sed executable One traced child (pid=11983) 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=11984) exited with status: 0 One traced child (pid=11982) exited with status: 0 New process pid=11985 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc31/normalized-e64.b.opb [startup+10.0033 s] Raw data (loadavg): 0.94 0.99 0.97 2/58 11987 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 2310 0 0 0 974 9 0 0 25 0 1 0 1841311767 10403840 2244 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 2540 2244 145 145 0 2395 0 [pid=11985] vsize: 10160 Current children cumulated CPU time (s) 9.83 Current children cumulated vsize (Kb) 12284 [startup+20.0053 s] Raw data (loadavg): 0.95 0.99 0.97 2/58 11987 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 2905 0 0 0 1963 13 0 0 25 0 1 0 1841311767 12824576 2839 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 3131 2839 145 145 0 2986 0 [pid=11985] vsize: 12524 Current children cumulated CPU time (s) 19.76 Current children cumulated vsize (Kb) 14648 [startup+30.0062 s] Raw data (loadavg): 0.96 0.99 0.97 2/58 11987 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 3313 0 0 0 2955 17 0 0 25 0 1 0 1841311767 14536704 3247 4294967295 134512640 135094434 3221224448 3221223104 134557835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 3549 3247 145 145 0 3404 0 [pid=11985] vsize: 14196 Current children cumulated CPU time (s) 29.72 Current children cumulated vsize (Kb) 16320 [startup+40.0072 s] Raw data (loadavg): 0.96 0.99 0.97 2/58 11987 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 3313 0 0 0 3955 17 0 0 25 0 1 0 1841311767 14536704 3247 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 3549 3247 145 145 0 3404 0 [pid=11985] vsize: 14196 Current children cumulated CPU time (s) 39.72 Current children cumulated vsize (Kb) 16320 [startup+50.0091 s] Raw data (loadavg): 0.97 0.99 0.97 2/58 11987 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 3425 0 0 0 4951 20 0 0 25 0 1 0 1841311767 14995456 3359 4294967295 134512640 135094434 3221224448 3221223072 134557662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 3661 3359 145 145 0 3516 0 [pid=11985] vsize: 14644 Current children cumulated CPU time (s) 49.71 Current children cumulated vsize (Kb) 16768 [startup+60.01 s] Raw data (loadavg): 0.97 0.99 0.97 2/58 11987 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 3427 0 0 0 5951 20 0 0 25 0 1 0 1841311767 14995456 3361 4294967295 134512640 135094434 3221224448 3221223088 134562070 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 3661 3361 145 145 0 3516 0 [pid=11985] vsize: 14644 Current children cumulated CPU time (s) 59.71 Current children cumulated vsize (Kb) 16768 [startup+70.0119 s] Raw data (loadavg): 0.98 0.99 0.97 2/58 11989 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 3803 0 0 0 6943 24 0 0 25 0 1 0 1841311767 16515072 3737 4294967295 134512640 135094434 3221224448 3221223120 134556236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 4032 3737 145 145 0 3887 0 [pid=11985] vsize: 16128 Current children cumulated CPU time (s) 69.67 Current children cumulated vsize (Kb) 18252 [startup+80.0139 s] Raw data (loadavg): 0.98 0.99 0.97 2/58 11989 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4178 0 0 0 7936 27 0 0 25 0 1 0 1841311767 18030592 4112 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 4402 4112 145 145 0 4257 0 [pid=11985] vsize: 17608 Current children cumulated CPU time (s) 79.63 Current children cumulated vsize (Kb) 19732 [startup+90.0148 s] Raw data (loadavg): 0.98 0.99 0.97 2/58 11989 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4511 0 0 0 8930 30 0 0 25 0 1 0 1841311767 19521536 4445 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 4766 4445 145 145 0 4621 0 [pid=11985] vsize: 19064 Current children cumulated CPU time (s) 89.6 Current children cumulated vsize (Kb) 21188 [startup+100.017 s] Raw data (loadavg): 0.98 0.99 0.97 2/58 11989 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4547 0 0 0 9929 31 0 0 25 0 1 0 1841311767 19668992 4481 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 4802 4481 145 145 0 4657 0 [pid=11985] vsize: 19208 Current children cumulated CPU time (s) 99.6 Current children cumulated vsize (Kb) 21332 [startup+110.018 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11989 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4547 0 0 0 10928 31 0 0 25 0 1 0 1841311767 19668992 4481 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 4802 4481 145 145 0 4657 0 [pid=11985] vsize: 19208 Current children cumulated CPU time (s) 109.59 Current children cumulated vsize (Kb) 21332 [startup+120.02 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11989 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4547 0 0 0 11928 31 0 0 25 0 1 0 1841311767 19668992 4481 4294967295 134512640 135094434 3221224448 3221223120 134556071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 4802 4481 145 145 0 4657 0 [pid=11985] vsize: 19208 Current children cumulated CPU time (s) 119.59 Current children cumulated vsize (Kb) 21332 [startup+130.021 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11991 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4758 0 0 0 12924 34 0 0 25 0 1 0 1841311767 20533248 4692 4294967295 134512640 135094434 3221224448 3221223104 134558281 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 5013 4692 145 145 0 4868 0 [pid=11985] vsize: 20052 Current children cumulated CPU time (s) 129.58 Current children cumulated vsize (Kb) 22176 [startup+140.021 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11991 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4861 0 0 0 13923 35 0 0 25 0 1 0 1841311767 20955136 4795 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 5116 4795 145 145 0 4971 0 [pid=11985] vsize: 20464 Current children cumulated CPU time (s) 139.58 Current children cumulated vsize (Kb) 22588 [startup+150.023 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11991 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4861 0 0 0 14922 35 0 0 25 0 1 0 1841311767 20955136 4795 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 5116 4795 145 145 0 4971 0 [pid=11985] vsize: 20464 Current children cumulated CPU time (s) 149.57 Current children cumulated vsize (Kb) 22588 [startup+160.024 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11991 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4861 0 0 0 15922 36 0 0 25 0 1 0 1841311767 20955136 4795 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 5116 4795 145 145 0 4971 0 [pid=11985] vsize: 20464 Current children cumulated CPU time (s) 159.58 Current children cumulated vsize (Kb) 22588 [startup+170.026 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11991 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4861 0 0 0 16922 36 0 0 25 0 1 0 1841311767 20955136 4795 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 5116 4795 145 145 0 4971 0 [pid=11985] vsize: 20464 Current children cumulated CPU time (s) 169.58 Current children cumulated vsize (Kb) 22588 [startup+180.027 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11991 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 4998 0 0 0 17919 38 0 0 25 0 1 0 1841311767 21520384 4932 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 5254 4932 145 145 0 5109 0 [pid=11985] vsize: 21016 Current children cumulated CPU time (s) 179.57 Current children cumulated vsize (Kb) 23140 [startup+190.028 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11993 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 5469 0 0 0 18907 43 0 0 25 0 1 0 1841311767 23433216 5403 4294967295 134512640 135094434 3221224448 3221223104 134558715 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 5721 5403 145 145 0 5576 0 [pid=11985] vsize: 22884 Current children cumulated CPU time (s) 189.5 Current children cumulated vsize (Kb) 25008 [startup+200.029 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11993 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 5469 0 0 0 19907 43 0 0 25 0 1 0 1841311767 23433216 5403 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 5721 5403 145 145 0 5576 0 [pid=11985] vsize: 22884 Current children cumulated CPU time (s) 199.5 Current children cumulated vsize (Kb) 25008 [startup+210.03 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11993 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 5469 0 0 0 20906 44 0 0 25 0 1 0 1841311767 23433216 5403 4294967295 134512640 135094434 3221224448 3221223104 134561778 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 5721 5403 145 145 0 5576 0 [pid=11985] vsize: 22884 Current children cumulated CPU time (s) 209.5 Current children cumulated vsize (Kb) 25008 [startup+220.032 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11993 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 5469 0 0 0 21905 45 0 0 25 0 1 0 1841311767 23433216 5403 4294967295 134512640 135094434 3221224448 3221223120 134556071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 5721 5403 145 145 0 5576 0 [pid=11985] vsize: 22884 Current children cumulated CPU time (s) 219.5 Current children cumulated vsize (Kb) 25008 [startup+230.033 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11993 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 5469 0 0 0 22905 45 0 0 25 0 1 0 1841311767 23433216 5403 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 5721 5403 145 145 0 5576 0 [pid=11985] vsize: 22884 Current children cumulated CPU time (s) 229.5 Current children cumulated vsize (Kb) 25008 [startup+240.034 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11993 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 5694 0 0 0 23901 47 0 0 25 0 1 0 1841311767 24363008 5628 4294967295 134512640 135094434 3221224448 3221223104 134558011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 5948 5628 145 145 0 5803 0 [pid=11985] vsize: 23792 Current children cumulated CPU time (s) 239.48 Current children cumulated vsize (Kb) 25916 [startup+250.035 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11995 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6036 0 0 0 24893 51 0 0 25 0 1 0 1841311767 25759744 5970 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 6289 5970 145 145 0 6144 0 [pid=11985] vsize: 25156 Current children cumulated CPU time (s) 249.44 Current children cumulated vsize (Kb) 27280 [startup+260.036 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11995 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6045 0 0 0 25893 51 0 0 25 0 1 0 1841311767 25796608 5979 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 6298 5979 145 145 0 6153 0 [pid=11985] vsize: 25192 Current children cumulated CPU time (s) 259.44 Current children cumulated vsize (Kb) 27316 [startup+270.036 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11995 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6045 0 0 0 26893 51 0 0 25 0 1 0 1841311767 25796608 5979 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 6298 5979 145 145 0 6153 0 [pid=11985] vsize: 25192 Current children cumulated CPU time (s) 269.44 Current children cumulated vsize (Kb) 27316 [startup+280.037 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11995 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6046 0 0 0 27893 51 0 0 25 0 1 0 1841311767 25796608 5980 4294967295 134512640 135094434 3221224448 3221223120 134555560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 6298 5980 145 145 0 6153 0 [pid=11985] vsize: 25192 Current children cumulated CPU time (s) 279.44 Current children cumulated vsize (Kb) 27316 [startup+290.038 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11995 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6046 0 0 0 28893 51 0 0 25 0 1 0 1841311767 25796608 5980 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 6298 5980 145 145 0 6153 0 [pid=11985] vsize: 25192 Current children cumulated CPU time (s) 289.44 Current children cumulated vsize (Kb) 27316 [startup+300.039 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11995 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6046 0 0 0 29893 52 0 0 25 0 1 0 1841311767 25796608 5980 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 6298 5980 145 145 0 6153 0 [pid=11985] vsize: 25192 Current children cumulated CPU time (s) 299.45 Current children cumulated vsize (Kb) 27316 [startup+310.04 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11997 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6201 0 0 0 30890 53 0 0 25 0 1 0 1841311767 26435584 6135 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 6454 6135 145 145 0 6309 0 [pid=11985] vsize: 25816 Current children cumulated CPU time (s) 309.43 Current children cumulated vsize (Kb) 27940 [startup+320.041 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11997 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6576 0 0 0 31883 56 0 0 25 0 1 0 1841311767 27983872 6510 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 6832 6510 145 145 0 6687 0 [pid=11985] vsize: 27328 Current children cumulated CPU time (s) 319.39 Current children cumulated vsize (Kb) 29452 [startup+330.042 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11997 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 6939 0 0 0 32876 60 0 0 25 0 1 0 1841311767 29474816 6873 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7196 6873 145 145 0 7051 0 [pid=11985] vsize: 28784 Current children cumulated CPU time (s) 329.36 Current children cumulated vsize (Kb) 30908 [startup+340.043 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11997 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7184 0 0 0 33872 62 0 0 25 0 1 0 1841311767 30461952 7118 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7437 7118 145 145 0 7292 0 [pid=11985] vsize: 29748 Current children cumulated CPU time (s) 339.34 Current children cumulated vsize (Kb) 31872 [startup+350.044 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11997 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7184 0 0 0 34872 62 0 0 25 0 1 0 1841311767 30461952 7118 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7437 7118 145 145 0 7292 0 [pid=11985] vsize: 29748 Current children cumulated CPU time (s) 349.34 Current children cumulated vsize (Kb) 31872 [startup+360.045 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11997 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7184 0 0 0 35872 62 0 0 25 0 1 0 1841311767 30461952 7118 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7437 7118 145 145 0 7292 0 [pid=11985] vsize: 29748 Current children cumulated CPU time (s) 359.34 Current children cumulated vsize (Kb) 31872 [startup+370.046 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11999 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7184 0 0 0 36872 62 0 0 25 0 1 0 1841311767 30461952 7118 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7437 7118 145 145 0 7292 0 [pid=11985] vsize: 29748 Current children cumulated CPU time (s) 369.34 Current children cumulated vsize (Kb) 31872 [startup+380.047 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11999 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7196 0 0 0 37872 62 0 0 25 0 1 0 1841311767 30527488 7130 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7453 7130 145 145 0 7308 0 [pid=11985] vsize: 29812 Current children cumulated CPU time (s) 379.34 Current children cumulated vsize (Kb) 31936 [startup+390.048 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11999 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7206 0 0 0 38872 62 0 0 25 0 1 0 1841311767 30593024 7140 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7469 7140 145 145 0 7324 0 [pid=11985] vsize: 29876 Current children cumulated CPU time (s) 389.34 Current children cumulated vsize (Kb) 32000 [startup+400.05 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11999 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7207 0 0 0 39873 62 0 0 25 0 1 0 1841311767 30593024 7141 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7469 7141 145 145 0 7324 0 [pid=11985] vsize: 29876 Current children cumulated CPU time (s) 399.35 Current children cumulated vsize (Kb) 32000 [startup+410.051 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11999 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7208 0 0 0 40873 62 0 0 25 0 1 0 1841311767 30593024 7142 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7469 7142 145 145 0 7324 0 [pid=11985] vsize: 29876 Current children cumulated CPU time (s) 409.35 Current children cumulated vsize (Kb) 32000 [startup+420.051 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 11999 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 41873 62 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0 [pid=11985] vsize: 29940 Current children cumulated CPU time (s) 419.35 Current children cumulated vsize (Kb) 32064 [startup+430.052 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12001 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 42873 62 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0 [pid=11985] vsize: 29940 Current children cumulated CPU time (s) 429.35 Current children cumulated vsize (Kb) 32064 [startup+440.053 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12001 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 43873 62 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0 [pid=11985] vsize: 29940 Current children cumulated CPU time (s) 439.35 Current children cumulated vsize (Kb) 32064 [startup+450.054 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12001 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 44874 62 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223072 134557662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0 [pid=11985] vsize: 29940 Current children cumulated CPU time (s) 449.36 Current children cumulated vsize (Kb) 32064 [startup+460.055 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12001 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 45874 62 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0 [pid=11985] vsize: 29940 Current children cumulated CPU time (s) 459.36 Current children cumulated vsize (Kb) 32064 [startup+470.056 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12001 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 46874 63 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0 [pid=11985] vsize: 29940 Current children cumulated CPU time (s) 469.37 Current children cumulated vsize (Kb) 32064 [startup+480.057 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12001 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 47874 63 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0 [pid=11985] vsize: 29940 Current children cumulated CPU time (s) 479.37 Current children cumulated vsize (Kb) 32064 [startup+490.057 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12003 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 48874 63 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0 [pid=11985] vsize: 29940 Current children cumulated CPU time (s) 489.37 Current children cumulated vsize (Kb) 32064 [startup+500.059 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12003 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 49875 63 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0 [pid=11985] vsize: 29940 Current children cumulated CPU time (s) 499.38 Current children cumulated vsize (Kb) 32064 [startup+510.06 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12003 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 50875 63 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0 [pid=11985] vsize: 29940 Current children cumulated CPU time (s) 509.38 Current children cumulated vsize (Kb) 32064 [startup+520.061 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12003 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7220 0 0 0 51875 63 0 0 25 0 1 0 1841311767 30658560 7154 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7485 7154 145 145 0 7340 0 [pid=11985] vsize: 29940 Current children cumulated CPU time (s) 519.38 Current children cumulated vsize (Kb) 32064 [startup+530.062 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12003 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7422 0 0 0 52871 65 0 0 25 0 1 0 1841311767 31490048 7356 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7688 7356 145 145 0 7543 0 [pid=11985] vsize: 30752 Current children cumulated CPU time (s) 529.36 Current children cumulated vsize (Kb) 32876 [startup+540.063 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12003 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 53869 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0 [pid=11985] vsize: 31224 Current children cumulated CPU time (s) 539.35 Current children cumulated vsize (Kb) 33348 [startup+550.064 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12005 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 54869 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0 [pid=11985] vsize: 31224 Current children cumulated CPU time (s) 549.35 Current children cumulated vsize (Kb) 33348 [startup+560.064 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12005 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 55870 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0 [pid=11985] vsize: 31224 Current children cumulated CPU time (s) 559.36 Current children cumulated vsize (Kb) 33348 [startup+570.065 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12005 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 56870 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0 [pid=11985] vsize: 31224 Current children cumulated CPU time (s) 569.36 Current children cumulated vsize (Kb) 33348 [startup+580.066 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12005 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 57870 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0 [pid=11985] vsize: 31224 Current children cumulated CPU time (s) 579.36 Current children cumulated vsize (Kb) 33348 [startup+590.067 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12005 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 58870 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0 [pid=11985] vsize: 31224 Current children cumulated CPU time (s) 589.36 Current children cumulated vsize (Kb) 33348 [startup+600.069 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12005 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 59870 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0 [pid=11985] vsize: 31224 Current children cumulated CPU time (s) 599.36 Current children cumulated vsize (Kb) 33348 [startup+610.07 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12007 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 60871 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0 [pid=11985] vsize: 31224 Current children cumulated CPU time (s) 609.37 Current children cumulated vsize (Kb) 33348 [startup+620.072 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12007 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 61871 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0 [pid=11985] vsize: 31224 Current children cumulated CPU time (s) 619.37 Current children cumulated vsize (Kb) 33348 [startup+630.073 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12007 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 62871 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0 [pid=11985] vsize: 31224 Current children cumulated CPU time (s) 629.37 Current children cumulated vsize (Kb) 33348 [startup+640.073 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12007 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7542 0 0 0 63871 66 0 0 25 0 1 0 1841311767 31973376 7476 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7806 7476 145 145 0 7661 0 [pid=11985] vsize: 31224 Current children cumulated CPU time (s) 639.37 Current children cumulated vsize (Kb) 33348 [startup+650.074 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12007 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7547 0 0 0 64872 66 0 0 25 0 1 0 1841311767 32006144 7481 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 7814 7481 145 145 0 7669 0 [pid=11985] vsize: 31256 Current children cumulated CPU time (s) 649.38 Current children cumulated vsize (Kb) 33380 [startup+660.075 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12007 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7549 0 0 0 65871 67 0 0 25 0 1 0 1841311767 32006144 7483 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 7814 7483 145 145 0 7669 0 [pid=11985] vsize: 31256 Current children cumulated CPU time (s) 659.38 Current children cumulated vsize (Kb) 33380 [startup+670.076 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12009 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7640 0 0 0 66869 67 0 0 25 0 1 0 1841311767 32407552 7574 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11985/statm): 7912 7574 145 145 0 7767 0 [pid=11985] vsize: 31648 Current children cumulated CPU time (s) 669.36 Current children cumulated vsize (Kb) 33772 [startup+680.077 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12009 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 7882 0 0 0 67864 70 0 0 25 0 1 0 1841311767 33382400 7816 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8150 7816 145 145 0 8005 0 [pid=11985] vsize: 32600 Current children cumulated CPU time (s) 679.34 Current children cumulated vsize (Kb) 34724 [startup+690.078 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12009 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8123 0 0 0 68859 72 0 0 25 0 1 0 1841311767 34369536 8057 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8391 8057 145 145 0 8246 0 [pid=11985] vsize: 33564 Current children cumulated CPU time (s) 689.31 Current children cumulated vsize (Kb) 35688 [startup+700.079 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12009 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8139 0 0 0 69859 72 0 0 25 0 1 0 1841311767 34435072 8073 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8407 8073 145 145 0 8262 0 [pid=11985] vsize: 33628 Current children cumulated CPU time (s) 699.31 Current children cumulated vsize (Kb) 35752 [startup+710.08 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12009 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8145 0 0 0 70860 72 0 0 25 0 1 0 1841311767 34467840 8079 4294967295 134512640 135094434 3221224448 3221223120 134556288 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8415 8079 145 145 0 8270 0 [pid=11985] vsize: 33660 Current children cumulated CPU time (s) 709.32 Current children cumulated vsize (Kb) 35784 [startup+720.08 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12009 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8152 0 0 0 71860 72 0 0 25 0 1 0 1841311767 34500608 8086 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8423 8086 145 145 0 8278 0 [pid=11985] vsize: 33692 Current children cumulated CPU time (s) 719.32 Current children cumulated vsize (Kb) 35816 [startup+730.081 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12011 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8152 0 0 0 72860 72 0 0 25 0 1 0 1841311767 34500608 8086 4294967295 134512640 135094434 3221224448 3221223040 134557016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8423 8086 145 145 0 8278 0 [pid=11985] vsize: 33692 Current children cumulated CPU time (s) 729.32 Current children cumulated vsize (Kb) 35816 [startup+740.082 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12011 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8153 0 0 0 73860 72 0 0 25 0 1 0 1841311767 34500608 8087 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8423 8087 145 145 0 8278 0 [pid=11985] vsize: 33692 Current children cumulated CPU time (s) 739.32 Current children cumulated vsize (Kb) 35816 [startup+750.083 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12011 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8160 0 0 0 74860 72 0 0 25 0 1 0 1841311767 34533376 8094 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8431 8094 145 145 0 8286 0 [pid=11985] vsize: 33724 Current children cumulated CPU time (s) 749.32 Current children cumulated vsize (Kb) 35848 [startup+760.084 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12011 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8160 0 0 0 75860 72 0 0 25 0 1 0 1841311767 34533376 8094 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8431 8094 145 145 0 8286 0 [pid=11985] vsize: 33724 Current children cumulated CPU time (s) 759.32 Current children cumulated vsize (Kb) 35848 [startup+770.086 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12011 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8165 0 0 0 76861 72 0 0 25 0 1 0 1841311767 34566144 8099 4294967295 134512640 135094434 3221224448 3221223104 134557804 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8439 8099 145 145 0 8294 0 [pid=11985] vsize: 33756 Current children cumulated CPU time (s) 769.33 Current children cumulated vsize (Kb) 35880 [startup+780.087 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12011 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8166 0 0 0 77861 72 0 0 25 0 1 0 1841311767 34566144 8100 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8439 8100 145 145 0 8294 0 [pid=11985] vsize: 33756 Current children cumulated CPU time (s) 779.33 Current children cumulated vsize (Kb) 35880 [startup+790.087 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12013 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8166 0 0 0 78860 73 0 0 25 0 1 0 1841311767 34566144 8100 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8439 8100 145 145 0 8294 0 [pid=11985] vsize: 33756 Current children cumulated CPU time (s) 789.33 Current children cumulated vsize (Kb) 35880 [startup+800.089 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12013 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8176 0 0 0 79860 74 0 0 25 0 1 0 1841311767 34631680 8110 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8455 8110 145 145 0 8310 0 [pid=11985] vsize: 33820 Current children cumulated CPU time (s) 799.34 Current children cumulated vsize (Kb) 35944 [startup+810.09 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12013 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8282 0 0 0 80858 75 0 0 25 0 1 0 1841311767 35090432 8216 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8567 8216 145 145 0 8422 0 [pid=11985] vsize: 34268 Current children cumulated CPU time (s) 809.33 Current children cumulated vsize (Kb) 36392 [startup+820.091 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12013 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8519 0 0 0 81852 78 0 0 25 0 1 0 1841311767 36069376 8453 4294967295 134512640 135094434 3221224448 3221223120 134555795 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 8806 8453 145 145 0 8661 0 [pid=11985] vsize: 35224 Current children cumulated CPU time (s) 819.3 Current children cumulated vsize (Kb) 37348 [startup+830.092 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12013 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8766 0 0 0 82848 80 0 0 25 0 1 0 1841311767 37085184 8700 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9054 8700 145 145 0 8909 0 [pid=11985] vsize: 36216 Current children cumulated CPU time (s) 829.28 Current children cumulated vsize (Kb) 38340 [startup+840.093 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12013 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8870 0 0 0 83846 81 0 0 25 0 1 0 1841311767 37502976 8804 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9156 8804 145 145 0 9011 0 [pid=11985] vsize: 36624 Current children cumulated CPU time (s) 839.27 Current children cumulated vsize (Kb) 38748 [startup+850.093 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12015 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8870 0 0 0 84846 81 0 0 25 0 1 0 1841311767 37502976 8804 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9156 8804 145 145 0 9011 0 [pid=11985] vsize: 36624 Current children cumulated CPU time (s) 849.27 Current children cumulated vsize (Kb) 38748 [startup+860.094 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12015 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8880 0 0 0 85846 81 0 0 25 0 1 0 1841311767 37568512 8814 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9172 8814 145 145 0 9027 0 [pid=11985] vsize: 36688 Current children cumulated CPU time (s) 859.27 Current children cumulated vsize (Kb) 38812 [startup+870.096 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12015 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8881 0 0 0 86847 81 0 0 25 0 1 0 1841311767 37568512 8815 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9172 8815 145 145 0 9027 0 [pid=11985] vsize: 36688 Current children cumulated CPU time (s) 869.28 Current children cumulated vsize (Kb) 38812 [startup+880.097 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12015 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8894 0 0 0 87847 82 0 0 25 0 1 0 1841311767 37634048 8828 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9188 8828 145 145 0 9043 0 [pid=11985] vsize: 36752 Current children cumulated CPU time (s) 879.29 Current children cumulated vsize (Kb) 38876 [startup+890.098 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12015 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8895 0 0 0 88847 82 0 0 25 0 1 0 1841311767 37634048 8829 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9188 8829 145 145 0 9043 0 [pid=11985] vsize: 36752 Current children cumulated CPU time (s) 889.29 Current children cumulated vsize (Kb) 38876 [startup+900.099 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12015 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8895 0 0 0 89847 82 0 0 25 0 1 0 1841311767 37634048 8829 4294967295 134512640 135094434 3221224448 3221223040 134556937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9188 8829 145 145 0 9043 0 [pid=11985] vsize: 36752 Current children cumulated CPU time (s) 899.29 Current children cumulated vsize (Kb) 38876 [startup+910.1 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12017 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8895 0 0 0 90847 82 0 0 25 0 1 0 1841311767 37634048 8829 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9188 8829 145 145 0 9043 0 [pid=11985] vsize: 36752 Current children cumulated CPU time (s) 909.29 Current children cumulated vsize (Kb) 38876 [startup+920.102 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12017 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8896 0 0 0 91848 82 0 0 25 0 1 0 1841311767 37634048 8830 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9188 8830 145 145 0 9043 0 [pid=11985] vsize: 36752 Current children cumulated CPU time (s) 919.3 Current children cumulated vsize (Kb) 38876 [startup+930.103 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12017 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8896 0 0 0 92848 82 0 0 25 0 1 0 1841311767 37634048 8830 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9188 8830 145 145 0 9043 0 [pid=11985] vsize: 36752 Current children cumulated CPU time (s) 929.3 Current children cumulated vsize (Kb) 38876 [startup+940.104 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12017 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8909 0 0 0 93848 82 0 0 25 0 1 0 1841311767 37699584 8843 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9204 8843 145 145 0 9059 0 [pid=11985] vsize: 36816 Current children cumulated CPU time (s) 939.3 Current children cumulated vsize (Kb) 38940 [startup+950.105 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12017 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8910 0 0 0 94848 82 0 0 25 0 1 0 1841311767 37699584 8844 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9204 8844 145 145 0 9059 0 [pid=11985] vsize: 36816 Current children cumulated CPU time (s) 949.3 Current children cumulated vsize (Kb) 38940 [startup+960.106 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12017 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8910 0 0 0 95848 82 0 0 25 0 1 0 1841311767 37699584 8844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9204 8844 145 145 0 9059 0 [pid=11985] vsize: 36816 Current children cumulated CPU time (s) 959.3 Current children cumulated vsize (Kb) 38940 [startup+970.107 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12019 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8911 0 0 0 96848 82 0 0 25 0 1 0 1841311767 37699584 8845 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9204 8845 145 145 0 9059 0 [pid=11985] vsize: 36816 Current children cumulated CPU time (s) 969.3 Current children cumulated vsize (Kb) 38940 [startup+980.109 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12019 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 8913 0 0 0 97848 83 0 0 25 0 1 0 1841311767 37699584 8847 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9204 8847 145 145 0 9059 0 [pid=11985] vsize: 36816 Current children cumulated CPU time (s) 979.31 Current children cumulated vsize (Kb) 38940 [startup+990.11 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12019 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9003 0 0 0 98847 83 0 0 25 0 1 0 1841311767 38064128 8937 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9293 8937 145 145 0 9148 0 [pid=11985] vsize: 37172 Current children cumulated CPU time (s) 989.3 Current children cumulated vsize (Kb) 39296 [startup+1000.11 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12019 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9200 0 0 0 99843 85 0 0 25 0 1 0 1841311767 38895616 9134 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9496 9134 145 145 0 9351 0 [pid=11985] vsize: 37984 Current children cumulated CPU time (s) 999.28 Current children cumulated vsize (Kb) 40108 [startup+1010.11 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12019 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9252 0 0 0 100842 85 0 0 25 0 1 0 1841311767 39108608 9186 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9186 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1009.27 Current children cumulated vsize (Kb) 40316 [startup+1020.11 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12019 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9252 0 0 0 101842 86 0 0 25 0 1 0 1841311767 39108608 9186 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9186 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1019.28 Current children cumulated vsize (Kb) 40316 [startup+1030.11 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12021 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9252 0 0 0 102842 86 0 0 25 0 1 0 1841311767 39108608 9186 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9186 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1029.28 Current children cumulated vsize (Kb) 40316 [startup+1040.12 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12021 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9252 0 0 0 103842 86 0 0 25 0 1 0 1841311767 39108608 9186 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9186 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1039.28 Current children cumulated vsize (Kb) 40316 [startup+1050.12 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12021 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9252 0 0 0 104842 86 0 0 25 0 1 0 1841311767 39108608 9186 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9186 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1049.28 Current children cumulated vsize (Kb) 40316 [startup+1060.12 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12021 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9252 0 0 0 105843 86 0 0 25 0 1 0 1841311767 39108608 9186 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9186 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1059.29 Current children cumulated vsize (Kb) 40316 [startup+1070.12 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12021 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9253 0 0 0 106843 86 0 0 25 0 1 0 1841311767 39108608 9187 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9187 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1069.29 Current children cumulated vsize (Kb) 40316 [startup+1080.12 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12021 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9254 0 0 0 107843 86 0 0 25 0 1 0 1841311767 39108608 9188 4294967295 134512640 135094434 3221224448 3221223060 134563130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9188 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1079.29 Current children cumulated vsize (Kb) 40316 [startup+1090.12 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12023 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9254 0 0 0 108843 86 0 0 25 0 1 0 1841311767 39108608 9188 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9188 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1089.29 Current children cumulated vsize (Kb) 40316 [startup+1100.12 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12023 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9254 0 0 0 109843 86 0 0 25 0 1 0 1841311767 39108608 9188 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9188 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1099.29 Current children cumulated vsize (Kb) 40316 [startup+1110.12 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12023 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9254 0 0 0 110844 86 0 0 25 0 1 0 1841311767 39108608 9188 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9188 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1109.3 Current children cumulated vsize (Kb) 40316 [startup+1120.12 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12023 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9254 0 0 0 111844 86 0 0 25 0 1 0 1841311767 39108608 9188 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9188 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1119.3 Current children cumulated vsize (Kb) 40316 [startup+1130.12 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12023 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9255 0 0 0 112844 87 0 0 25 0 1 0 1841311767 39108608 9189 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9548 9189 145 145 0 9403 0 [pid=11985] vsize: 38192 Current children cumulated CPU time (s) 1129.31 Current children cumulated vsize (Kb) 40316 [startup+1140.13 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12023 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9264 0 0 0 113844 87 0 0 25 0 1 0 1841311767 39174144 9198 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9564 9198 145 145 0 9419 0 [pid=11985] vsize: 38256 Current children cumulated CPU time (s) 1139.31 Current children cumulated vsize (Kb) 40380 [startup+1150.13 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12025 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9275 0 0 0 114844 87 0 0 25 0 1 0 1841311767 39239680 9209 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9580 9209 145 145 0 9435 0 [pid=11985] vsize: 38320 Current children cumulated CPU time (s) 1149.31 Current children cumulated vsize (Kb) 40444 [startup+1160.13 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12025 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9294 0 0 0 115844 87 0 0 25 0 1 0 1841311767 39370752 9228 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9612 9228 145 145 0 9467 0 [pid=11985] vsize: 38448 Current children cumulated CPU time (s) 1159.31 Current children cumulated vsize (Kb) 40572 [startup+1170.13 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12025 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9295 0 0 0 116845 87 0 0 25 0 1 0 1841311767 39370752 9229 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9612 9229 145 145 0 9467 0 [pid=11985] vsize: 38448 Current children cumulated CPU time (s) 1169.32 Current children cumulated vsize (Kb) 40572 [startup+1180.13 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12025 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9304 0 0 0 117845 87 0 0 25 0 1 0 1841311767 39436288 9238 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9628 9238 145 145 0 9483 0 [pid=11985] vsize: 38512 Current children cumulated CPU time (s) 1179.32 Current children cumulated vsize (Kb) 40636 [startup+1190.13 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12025 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9315 0 0 0 118845 87 0 0 25 0 1 0 1841311767 39501824 9249 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9644 9249 145 145 0 9499 0 [pid=11985] vsize: 38576 Current children cumulated CPU time (s) 1189.32 Current children cumulated vsize (Kb) 40700 [startup+1200.13 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12025 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9392 0 0 0 119844 88 0 0 25 0 1 0 1841311767 39800832 9326 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9717 9326 145 145 0 9572 0 [pid=11985] vsize: 38868 Current children cumulated CPU time (s) 1199.32 Current children cumulated vsize (Kb) 40992 [startup+1210.13 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12027 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) R 11981 11981 9102 0 -1 0 9559 0 0 0 120840 89 0 0 25 0 1 0 1841311767 40488960 9493 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9885 9493 145 145 0 9740 0 [pid=11985] vsize: 39540 Current children cumulated CPU time (s) 1209.29 Current children cumulated vsize (Kb) 41664 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.14 s] Raw data (loadavg): 0.99 0.99 0.97 2/58 12027 Raw data (/proc/11981/stat): 11981 (minisat+_script) S 11980 11981 9102 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841311762 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11981/statm): 531 226 485 147 0 384 0 [pid=11981] vsize: 2124 Raw data (/proc/11985/stat): 11985 (minisat+_64-bit) T 11981 11981 9102 0 -1 0 9559 0 0 0 120840 89 0 0 25 0 1 0 1841311767 40488960 9493 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/11985/statm): 9885 9493 145 145 0 9740 0 [pid=11985] vsize: 39540 Current children cumulated CPU time (s) 1209.29 Current children cumulated vsize (Kb) 41664 Sending SIGTERM to -11981 Sleeping 2 seconds One traced child (pid=11981) ended because it received signal 15 (SIGTERM) One traced child (pid=11985) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.16 CPU time (s): 1209.32 CPU user time (s): 1208.41 CPU system time (s): 0.913861 CPU usage (%): 99.9312 Max. virtual memory (cumulated for all children) (Kb): 41664
ERROR: no interpretation found !