Name | submitted/manquinho/primes-dimacs-cnf/normalized-par32-3-c.opb |
MD5SUM | b552ff39062b6c42ea64365c815cbd78 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 2650 |
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 | 2650 |
Number of bits of the sum of numbers in the objective function | 12 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 2650 |
Number of bits of the biggest sum of numbers | 12 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 2650 |
Total number of constraints | 6619 |
Number of constraints which are clauses | 6619 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 3 |
LAUNCH ON wulflinc1 THE 2005-09-18 15:30:17 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2537 boxname=wulflinc1 idbench=193 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b552ff39062b6c42ea64365c815cbd78 /oldhome/oroussel/tmp/wulflinc1/normalized-par32-3-c.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-par32-3-c.opb IDLAUNCH: 2537 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 883716 kB Buffers: 37660 kB Cached: 83424 kB SwapCached: 908 kB Active: 91964 kB Inactive: 31948 kB HighTotal: 131008 kB HighFree: 51520 kB LowTotal: 903652 kB LowFree: 832196 kB SwapTotal: 2097136 kB SwapFree: 2095620 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5992 kB Slab: 21392 kB Committed_AS: 93132 kB PageTables: 344 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 15:50:17 (client local time) WITH STATUS 0 IN 1200.11 SECONDS stats: 2537 7 1200.11 0
c Parsing PB file... c Converting 6619 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 | 6619 18160 | 2206 0 0 nan | 0.000 % | c | 100 | 6619 18160 | 2426 100 3859 38.6 | 0.004 % | c | 251 | 6619 18160 | 2669 251 9809 39.1 | 0.000 % | c | 478 | 6619 18160 | 2936 478 17222 36.0 | 0.000 % | c | 816 | 6619 18160 | 3229 816 27693 33.9 | 0.000 % | c | 1322 | 6619 18160 | 3552 1322 42040 31.8 | 0.000 % | c | 2082 | 6619 18160 | 3908 2082 62382 30.0 | 0.000 % | c | 3221 | 6619 18160 | 4298 3221 93422 29.0 | 0.000 % | c | 4929 | 6619 18160 | 4728 2713 65736 24.2 | 0.000 % | c | 7492 | 6619 18160 | 5201 2841 73172 25.8 | 0.000 % | c | 11336 | 6619 18160 | 5721 3996 102988 25.8 | 0.000 % | c | 17103 | 6619 18160 | 6293 3920 89536 22.8 | 0.000 % | c | 25753 | 6619 18160 | 6923 6199 149088 24.1 | 0.000 % | c | 38727 | 6619 18160 | 7615 5119 134081 26.2 | 0.000 % | c | 58189 | 6619 18160 | 8377 5292 114882 21.7 | 0.000 % | c | 87383 | 6612 18144 | 9215 4809 110169 22.9 | 0.075 % | c | 131173 | 6612 18144 | 10136 6732 143285 21.3 | 0.075 % | c | 196857 | 6612 18144 | 11150 6021 122607 20.4 | 0.075 % | c | 295383 | 6612 18144 | 12265 9132 197753 21.7 | 0.075 % | c | 443173 | 6612 18144 | 13491 11957 351003 29.4 | 0.075 % | c | 664857 | 6612 18144 | 14840 9587 204805 21.4 | 0.075 % | c | 997382 | 6612 18144 | 16324 13400 288483 21.5 | 0.076 % |
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/25943/stat): 25943 (minisat+_script) R 25942 25943 17733 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1727264051 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/25943/statm): 174 3 169 147 0 27 0 [pid=25943] 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=25944 New process pid=25945 New process pid=25946 execve syscall for /bin/sed executable One traced child (pid=25945) 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=25946) exited with status: 0 One traced child (pid=25944) exited with status: 0 New process pid=25947 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-par32-3-c.opb [startup+10.0033 s] Raw data (loadavg): 0.71 0.87 0.88 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 735 0 0 0 989 3 0 0 25 0 1 0 1727264056 3313664 722 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 809 722 145 145 0 664 0 [pid=25947] vsize: 3236 Current children cumulated CPU time (s) 9.94 Current children cumulated vsize (Kb) 5360 [startup+20.0041 s] Raw data (loadavg): 0.76 0.88 0.88 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 735 0 0 0 1989 3 0 0 25 0 1 0 1727264056 3313664 722 4294967295 134512640 135094434 3221224448 3221223120 134556244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 809 722 145 145 0 664 0 [pid=25947] vsize: 3236 Current children cumulated CPU time (s) 19.94 Current children cumulated vsize (Kb) 5360 [startup+30.0059 s] Raw data (loadavg): 0.79 0.88 0.88 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 735 0 0 0 2988 3 0 0 25 0 1 0 1727264056 3313664 722 4294967295 134512640 135094434 3221224448 3221223088 134558043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 809 722 145 145 0 664 0 [pid=25947] vsize: 3236 Current children cumulated CPU time (s) 29.93 Current children cumulated vsize (Kb) 5360 [startup+40.0066 s] Raw data (loadavg): 0.82 0.89 0.88 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 735 0 0 0 3988 4 0 0 25 0 1 0 1727264056 3313664 722 4294967295 134512640 135094434 3221224448 3221223056 134781796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 809 722 145 145 0 664 0 [pid=25947] vsize: 3236 Current children cumulated CPU time (s) 39.94 Current children cumulated vsize (Kb) 5360 [startup+50.0074 s] Raw data (loadavg): 0.85 0.89 0.88 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 741 0 0 0 4988 4 0 0 25 0 1 0 1727264056 3338240 728 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 815 728 145 145 0 670 0 [pid=25947] vsize: 3260 Current children cumulated CPU time (s) 49.94 Current children cumulated vsize (Kb) 5384 [startup+60.0082 s] Raw data (loadavg): 0.87 0.89 0.88 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 744 0 0 0 5988 4 0 0 25 0 1 0 1727264056 3354624 731 4294967295 134512640 135094434 3221224448 3221223040 134556958 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 819 731 145 145 0 674 0 [pid=25947] vsize: 3276 Current children cumulated CPU time (s) 59.94 Current children cumulated vsize (Kb) 5400 [startup+70.009 s] Raw data (loadavg): 0.89 0.89 0.88 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 757 0 0 0 6987 4 0 0 25 0 1 0 1727264056 3440640 744 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 840 744 145 145 0 695 0 [pid=25947] vsize: 3360 Current children cumulated CPU time (s) 69.93 Current children cumulated vsize (Kb) 5484 [startup+80.0108 s] Raw data (loadavg): 0.91 0.90 0.89 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 763 0 0 0 7987 5 0 0 25 0 1 0 1727264056 3489792 750 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 852 750 145 145 0 707 0 [pid=25947] vsize: 3408 Current children cumulated CPU time (s) 79.94 Current children cumulated vsize (Kb) 5532 [startup+90.0116 s] Raw data (loadavg): 0.92 0.90 0.89 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 783 0 0 0 8987 5 0 0 25 0 1 0 1727264056 3571712 770 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 872 770 145 145 0 727 0 [pid=25947] vsize: 3488 Current children cumulated CPU time (s) 89.94 Current children cumulated vsize (Kb) 5612 [startup+100.011 s] Raw data (loadavg): 0.93 0.90 0.89 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 797 0 0 0 9986 6 0 0 25 0 1 0 1727264056 3629056 784 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 886 784 145 145 0 741 0 [pid=25947] vsize: 3544 Current children cumulated CPU time (s) 99.94 Current children cumulated vsize (Kb) 5668 [startup+110.013 s] Raw data (loadavg): 0.94 0.91 0.89 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 817 0 0 0 10986 6 0 0 25 0 1 0 1727264056 3723264 804 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 909 804 145 145 0 764 0 [pid=25947] vsize: 3636 Current children cumulated CPU time (s) 109.94 Current children cumulated vsize (Kb) 5760 [startup+120.014 s] Raw data (loadavg): 0.95 0.91 0.89 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 818 0 0 0 11986 6 0 0 25 0 1 0 1727264056 3723264 805 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 909 805 145 145 0 764 0 [pid=25947] vsize: 3636 Current children cumulated CPU time (s) 119.94 Current children cumulated vsize (Kb) 5760 [startup+130.015 s] Raw data (loadavg): 0.96 0.91 0.89 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 818 0 0 0 12986 6 0 0 25 0 1 0 1727264056 3723264 805 4294967295 134512640 135094434 3221224448 3221223040 134556847 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 909 805 145 145 0 764 0 [pid=25947] vsize: 3636 Current children cumulated CPU time (s) 129.94 Current children cumulated vsize (Kb) 5760 [startup+140.015 s] Raw data (loadavg): 0.96 0.91 0.89 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 821 0 0 0 13987 6 0 0 25 0 1 0 1727264056 3739648 808 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 913 808 145 145 0 768 0 [pid=25947] vsize: 3652 Current children cumulated CPU time (s) 139.95 Current children cumulated vsize (Kb) 5776 [startup+150.016 s] Raw data (loadavg): 0.97 0.92 0.89 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 828 0 0 0 14987 6 0 0 25 0 1 0 1727264056 3772416 815 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 921 815 145 145 0 776 0 [pid=25947] vsize: 3684 Current children cumulated CPU time (s) 149.95 Current children cumulated vsize (Kb) 5808 [startup+160.017 s] Raw data (loadavg): 0.97 0.92 0.89 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 844 0 0 0 15987 6 0 0 25 0 1 0 1727264056 3837952 831 4294967295 134512640 135094434 3221224448 3221223104 134557823 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 937 831 145 145 0 792 0 [pid=25947] vsize: 3748 Current children cumulated CPU time (s) 159.95 Current children cumulated vsize (Kb) 5872 [startup+170.017 s] Raw data (loadavg): 0.98 0.92 0.89 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 851 0 0 0 16987 6 0 0 25 0 1 0 1727264056 3870720 838 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 945 838 145 145 0 800 0 [pid=25947] vsize: 3780 Current children cumulated CPU time (s) 169.95 Current children cumulated vsize (Kb) 5904 [startup+180.018 s] Raw data (loadavg): 0.98 0.92 0.89 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 872 0 0 0 17987 6 0 0 25 0 1 0 1727264056 3969024 859 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 969 859 145 145 0 824 0 [pid=25947] vsize: 3876 Current children cumulated CPU time (s) 179.95 Current children cumulated vsize (Kb) 6000 [startup+190.018 s] Raw data (loadavg): 0.98 0.92 0.90 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 880 0 0 0 18987 6 0 0 25 0 1 0 1727264056 4018176 867 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 981 867 145 145 0 836 0 [pid=25947] vsize: 3924 Current children cumulated CPU time (s) 189.95 Current children cumulated vsize (Kb) 6048 [startup+200.018 s] Raw data (loadavg): 0.98 0.93 0.90 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 880 0 0 0 19987 6 0 0 25 0 1 0 1727264056 4018176 867 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 981 867 145 145 0 836 0 [pid=25947] vsize: 3924 Current children cumulated CPU time (s) 199.95 Current children cumulated vsize (Kb) 6048 [startup+210.019 s] Raw data (loadavg): 0.99 0.93 0.90 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 881 0 0 0 20987 6 0 0 25 0 1 0 1727264056 4018176 868 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 981 868 145 145 0 836 0 [pid=25947] vsize: 3924 Current children cumulated CPU time (s) 209.95 Current children cumulated vsize (Kb) 6048 [startup+220.02 s] Raw data (loadavg): 0.99 0.93 0.90 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 883 0 0 0 21988 6 0 0 25 0 1 0 1727264056 4018176 870 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 981 870 145 145 0 836 0 [pid=25947] vsize: 3924 Current children cumulated CPU time (s) 219.96 Current children cumulated vsize (Kb) 6048 [startup+230.021 s] Raw data (loadavg): 0.99 0.93 0.90 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 906 0 0 0 22987 6 0 0 25 0 1 0 1727264056 4104192 893 4294967295 134512640 135094434 3221224448 3221223072 134562108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1002 893 145 145 0 857 0 [pid=25947] vsize: 4008 Current children cumulated CPU time (s) 229.95 Current children cumulated vsize (Kb) 6132 [startup+240.021 s] Raw data (loadavg): 0.99 0.93 0.90 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 912 0 0 0 23987 6 0 0 25 0 1 0 1727264056 4124672 899 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1007 899 145 145 0 862 0 [pid=25947] vsize: 4028 Current children cumulated CPU time (s) 239.95 Current children cumulated vsize (Kb) 6152 [startup+250.021 s] Raw data (loadavg): 0.99 0.94 0.90 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 924 0 0 0 24987 6 0 0 25 0 1 0 1727264056 4186112 911 4294967295 134512640 135094434 3221224448 3221222992 134779252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1022 911 145 145 0 877 0 [pid=25947] vsize: 4088 Current children cumulated CPU time (s) 249.95 Current children cumulated vsize (Kb) 6212 [startup+260.023 s] Raw data (loadavg): 0.99 0.94 0.90 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 924 0 0 0 25987 6 0 0 25 0 1 0 1727264056 4186112 911 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1022 911 145 145 0 877 0 [pid=25947] vsize: 4088 Current children cumulated CPU time (s) 259.95 Current children cumulated vsize (Kb) 6212 [startup+270.023 s] Raw data (loadavg): 0.99 0.94 0.90 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 924 0 0 0 26988 6 0 0 25 0 1 0 1727264056 4186112 911 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1022 911 145 145 0 877 0 [pid=25947] vsize: 4088 Current children cumulated CPU time (s) 269.96 Current children cumulated vsize (Kb) 6212 [startup+280.024 s] Raw data (loadavg): 0.99 0.94 0.90 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 930 0 0 0 27988 6 0 0 25 0 1 0 1727264056 4235264 917 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1034 917 145 145 0 889 0 [pid=25947] vsize: 4136 Current children cumulated CPU time (s) 279.96 Current children cumulated vsize (Kb) 6260 [startup+290.024 s] Raw data (loadavg): 0.99 0.94 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 940 0 0 0 28988 6 0 0 25 0 1 0 1727264056 4284416 927 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1046 927 145 145 0 901 0 [pid=25947] vsize: 4184 Current children cumulated CPU time (s) 289.96 Current children cumulated vsize (Kb) 6308 [startup+300.025 s] Raw data (loadavg): 0.99 0.94 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 944 0 0 0 29988 6 0 0 25 0 1 0 1727264056 4300800 931 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1050 931 145 145 0 905 0 [pid=25947] vsize: 4200 Current children cumulated CPU time (s) 299.96 Current children cumulated vsize (Kb) 6324 [startup+310.026 s] Raw data (loadavg): 0.99 0.94 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 955 0 0 0 30989 6 0 0 25 0 1 0 1727264056 4366336 942 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1066 942 145 145 0 921 0 [pid=25947] vsize: 4264 Current children cumulated CPU time (s) 309.97 Current children cumulated vsize (Kb) 6388 [startup+320.026 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 958 0 0 0 31989 6 0 0 25 0 1 0 1727264056 4366336 945 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1066 945 145 145 0 921 0 [pid=25947] vsize: 4264 Current children cumulated CPU time (s) 319.97 Current children cumulated vsize (Kb) 6388 [startup+330.026 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 958 0 0 0 32989 6 0 0 25 0 1 0 1727264056 4366336 945 4294967295 134512640 135094434 3221224448 3221223120 134555323 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1066 945 145 145 0 921 0 [pid=25947] vsize: 4264 Current children cumulated CPU time (s) 329.97 Current children cumulated vsize (Kb) 6388 [startup+340.027 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 964 0 0 0 33989 6 0 0 25 0 1 0 1727264056 4399104 951 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1074 951 145 145 0 929 0 [pid=25947] vsize: 4296 Current children cumulated CPU time (s) 339.97 Current children cumulated vsize (Kb) 6420 [startup+350.027 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1016 0 0 0 34988 7 0 0 25 0 1 0 1727264056 4616192 1003 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1127 1003 145 145 0 982 0 [pid=25947] vsize: 4508 Current children cumulated CPU time (s) 349.97 Current children cumulated vsize (Kb) 6632 [startup+360.029 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1114 0 0 0 35986 8 0 0 25 0 1 0 1727264056 5025792 1101 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1227 1101 145 145 0 1082 0 [pid=25947] vsize: 4908 Current children cumulated CPU time (s) 359.96 Current children cumulated vsize (Kb) 7032 [startup+370.029 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1127 0 0 0 36986 8 0 0 25 0 1 0 1727264056 5079040 1114 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1240 1114 145 145 0 1095 0 [pid=25947] vsize: 4960 Current children cumulated CPU time (s) 369.96 Current children cumulated vsize (Kb) 7084 [startup+380.029 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1138 0 0 0 37986 8 0 0 25 0 1 0 1727264056 5120000 1125 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1250 1125 145 145 0 1105 0 [pid=25947] vsize: 5000 Current children cumulated CPU time (s) 379.96 Current children cumulated vsize (Kb) 7124 [startup+390.03 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1144 0 0 0 38986 8 0 0 25 0 1 0 1727264056 5152768 1131 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1258 1131 145 145 0 1113 0 [pid=25947] vsize: 5032 Current children cumulated CPU time (s) 389.96 Current children cumulated vsize (Kb) 7156 [startup+400.031 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1156 0 0 0 39986 8 0 0 25 0 1 0 1727264056 5206016 1143 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1271 1143 145 145 0 1126 0 [pid=25947] vsize: 5084 Current children cumulated CPU time (s) 399.96 Current children cumulated vsize (Kb) 7208 [startup+410.032 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1164 0 0 0 40987 8 0 0 25 0 1 0 1727264056 5238784 1151 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1279 1151 145 145 0 1134 0 [pid=25947] vsize: 5116 Current children cumulated CPU time (s) 409.97 Current children cumulated vsize (Kb) 7240 [startup+420.033 s] Raw data (loadavg): 0.99 0.95 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1164 0 0 0 41987 8 0 0 25 0 1 0 1727264056 5238784 1151 4294967295 134512640 135094434 3221224448 3221223040 134551428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1279 1151 145 145 0 1134 0 [pid=25947] vsize: 5116 Current children cumulated CPU time (s) 419.97 Current children cumulated vsize (Kb) 7240 [startup+430.033 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1170 0 0 0 42987 8 0 0 25 0 1 0 1727264056 5271552 1157 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1287 1157 145 145 0 1142 0 [pid=25947] vsize: 5148 Current children cumulated CPU time (s) 429.97 Current children cumulated vsize (Kb) 7272 [startup+440.034 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1176 0 0 0 43987 8 0 0 25 0 1 0 1727264056 5304320 1163 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1295 1163 145 145 0 1150 0 [pid=25947] vsize: 5180 Current children cumulated CPU time (s) 439.97 Current children cumulated vsize (Kb) 7304 [startup+450.034 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1176 0 0 0 44987 8 0 0 25 0 1 0 1727264056 5304320 1163 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1295 1163 145 145 0 1150 0 [pid=25947] vsize: 5180 Current children cumulated CPU time (s) 449.97 Current children cumulated vsize (Kb) 7304 [startup+460.035 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1176 0 0 0 45988 8 0 0 25 0 1 0 1727264056 5304320 1163 4294967295 134512640 135094434 3221224448 3221223120 134556275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1295 1163 145 145 0 1150 0 [pid=25947] vsize: 5180 Current children cumulated CPU time (s) 459.98 Current children cumulated vsize (Kb) 7304 [startup+470.035 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1176 0 0 0 46987 8 0 0 25 0 1 0 1727264056 5304320 1163 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1295 1163 145 145 0 1150 0 [pid=25947] vsize: 5180 Current children cumulated CPU time (s) 469.97 Current children cumulated vsize (Kb) 7304 [startup+480.036 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1176 0 0 0 47987 8 0 0 25 0 1 0 1727264056 5304320 1163 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1295 1163 145 145 0 1150 0 [pid=25947] vsize: 5180 Current children cumulated CPU time (s) 479.97 Current children cumulated vsize (Kb) 7304 [startup+490.037 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1189 0 0 0 48987 9 0 0 25 0 1 0 1727264056 5353472 1176 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 1307 1176 145 145 0 1162 0 [pid=25947] vsize: 5228 Current children cumulated CPU time (s) 489.98 Current children cumulated vsize (Kb) 7352 [startup+500.038 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1193 0 0 0 49986 9 0 0 25 0 1 0 1727264056 5369856 1180 4294967295 134512640 135094434 3221224448 3221223040 134556845 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 1311 1180 145 145 0 1166 0 [pid=25947] vsize: 5244 Current children cumulated CPU time (s) 499.97 Current children cumulated vsize (Kb) 7368 [startup+510.039 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1200 0 0 0 50985 9 0 0 25 0 1 0 1727264056 5402624 1187 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1319 1187 145 145 0 1174 0 [pid=25947] vsize: 5276 Current children cumulated CPU time (s) 509.96 Current children cumulated vsize (Kb) 7400 [startup+520.038 s] Raw data (loadavg): 0.99 0.96 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1205 0 0 0 51985 9 0 0 25 0 1 0 1727264056 5435392 1192 4294967295 134512640 135094434 3221224448 3221222544 134562769 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1327 1192 145 145 0 1182 0 [pid=25947] vsize: 5308 Current children cumulated CPU time (s) 519.96 Current children cumulated vsize (Kb) 7432 [startup+530.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1210 0 0 0 52986 9 0 0 25 0 1 0 1727264056 5468160 1197 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1335 1197 145 145 0 1190 0 [pid=25947] vsize: 5340 Current children cumulated CPU time (s) 529.97 Current children cumulated vsize (Kb) 7464 [startup+540.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1215 0 0 0 53986 9 0 0 25 0 1 0 1727264056 5500928 1202 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1343 1202 145 145 0 1198 0 [pid=25947] vsize: 5372 Current children cumulated CPU time (s) 539.97 Current children cumulated vsize (Kb) 7496 [startup+550.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1221 0 0 0 54986 9 0 0 25 0 1 0 1727264056 5533696 1208 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1351 1208 145 145 0 1206 0 [pid=25947] vsize: 5404 Current children cumulated CPU time (s) 549.97 Current children cumulated vsize (Kb) 7528 [startup+560.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1226 0 0 0 55986 9 0 0 25 0 1 0 1727264056 5566464 1213 4294967295 134512640 135094434 3221224448 3221223120 134555313 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1359 1213 145 145 0 1214 0 [pid=25947] vsize: 5436 Current children cumulated CPU time (s) 559.97 Current children cumulated vsize (Kb) 7560 [startup+570.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1227 0 0 0 56986 9 0 0 25 0 1 0 1727264056 5566464 1214 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1359 1214 145 145 0 1214 0 [pid=25947] vsize: 5436 Current children cumulated CPU time (s) 569.97 Current children cumulated vsize (Kb) 7560 [startup+580.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1227 0 0 0 57987 9 0 0 25 0 1 0 1727264056 5566464 1214 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1359 1214 145 145 0 1214 0 [pid=25947] vsize: 5436 Current children cumulated CPU time (s) 579.98 Current children cumulated vsize (Kb) 7560 [startup+590.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1233 0 0 0 58987 9 0 0 25 0 1 0 1727264056 5599232 1220 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1367 1220 145 145 0 1222 0 [pid=25947] vsize: 5468 Current children cumulated CPU time (s) 589.98 Current children cumulated vsize (Kb) 7592 [startup+600.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1233 0 0 0 59987 9 0 0 25 0 1 0 1727264056 5599232 1220 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1367 1220 145 145 0 1222 0 [pid=25947] vsize: 5468 Current children cumulated CPU time (s) 599.98 Current children cumulated vsize (Kb) 7592 [startup+610.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1236 0 0 0 60987 9 0 0 25 0 1 0 1727264056 5599232 1223 4294967295 134512640 135094434 3221224448 3221223060 134563130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1367 1223 145 145 0 1222 0 [pid=25947] vsize: 5468 Current children cumulated CPU time (s) 609.98 Current children cumulated vsize (Kb) 7592 [startup+620.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1237 0 0 0 61987 9 0 0 25 0 1 0 1727264056 5599232 1224 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1367 1224 145 145 0 1222 0 [pid=25947] vsize: 5468 Current children cumulated CPU time (s) 619.98 Current children cumulated vsize (Kb) 7592 [startup+630.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1238 0 0 0 62988 9 0 0 25 0 1 0 1727264056 5599232 1225 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1367 1225 145 145 0 1222 0 [pid=25947] vsize: 5468 Current children cumulated CPU time (s) 629.99 Current children cumulated vsize (Kb) 7592 [startup+640.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1238 0 0 0 63988 9 0 0 25 0 1 0 1727264056 5599232 1225 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1367 1225 145 145 0 1222 0 [pid=25947] vsize: 5468 Current children cumulated CPU time (s) 639.99 Current children cumulated vsize (Kb) 7592 [startup+650.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1238 0 0 0 64988 9 0 0 25 0 1 0 1727264056 5599232 1225 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1367 1225 145 145 0 1222 0 [pid=25947] vsize: 5468 Current children cumulated CPU time (s) 649.99 Current children cumulated vsize (Kb) 7592 [startup+660.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1239 0 0 0 65988 9 0 0 25 0 1 0 1727264056 5599232 1226 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1367 1226 145 145 0 1222 0 [pid=25947] vsize: 5468 Current children cumulated CPU time (s) 659.99 Current children cumulated vsize (Kb) 7592 [startup+670.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1239 0 0 0 66989 9 0 0 25 0 1 0 1727264056 5599232 1226 4294967295 134512640 135094434 3221224448 3221223104 134557835 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1367 1226 145 145 0 1222 0 [pid=25947] vsize: 5468 Current children cumulated CPU time (s) 670 Current children cumulated vsize (Kb) 7592 [startup+680.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1239 0 0 0 67989 9 0 0 25 0 1 0 1727264056 5599232 1226 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1367 1226 145 145 0 1222 0 [pid=25947] vsize: 5468 Current children cumulated CPU time (s) 680 Current children cumulated vsize (Kb) 7592 [startup+690.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1239 0 0 0 68989 9 0 0 25 0 1 0 1727264056 5599232 1226 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1367 1226 145 145 0 1222 0 [pid=25947] vsize: 5468 Current children cumulated CPU time (s) 690 Current children cumulated vsize (Kb) 7592 [startup+700.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1244 0 0 0 69989 9 0 0 25 0 1 0 1727264056 5632000 1231 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1375 1231 145 145 0 1230 0 [pid=25947] vsize: 5500 Current children cumulated CPU time (s) 700 Current children cumulated vsize (Kb) 7624 [startup+710.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1245 0 0 0 70989 9 0 0 25 0 1 0 1727264056 5632000 1232 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1375 1232 145 145 0 1230 0 [pid=25947] vsize: 5500 Current children cumulated CPU time (s) 710 Current children cumulated vsize (Kb) 7624 [startup+720.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1245 0 0 0 71990 9 0 0 25 0 1 0 1727264056 5632000 1232 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1375 1232 145 145 0 1230 0 [pid=25947] vsize: 5500 Current children cumulated CPU time (s) 720.01 Current children cumulated vsize (Kb) 7624 [startup+730.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1245 0 0 0 72990 9 0 0 25 0 1 0 1727264056 5632000 1232 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1375 1232 145 145 0 1230 0 [pid=25947] vsize: 5500 Current children cumulated CPU time (s) 730.01 Current children cumulated vsize (Kb) 7624 [startup+740.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1245 0 0 0 73990 9 0 0 25 0 1 0 1727264056 5632000 1232 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1375 1232 145 145 0 1230 0 [pid=25947] vsize: 5500 Current children cumulated CPU time (s) 740.01 Current children cumulated vsize (Kb) 7624 [startup+750.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1245 0 0 0 74990 9 0 0 25 0 1 0 1727264056 5632000 1232 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1375 1232 145 145 0 1230 0 [pid=25947] vsize: 5500 Current children cumulated CPU time (s) 750.01 Current children cumulated vsize (Kb) 7624 [startup+760.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1245 0 0 0 75991 9 0 0 25 0 1 0 1727264056 5632000 1232 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1375 1232 145 145 0 1230 0 [pid=25947] vsize: 5500 Current children cumulated CPU time (s) 760.02 Current children cumulated vsize (Kb) 7624 [startup+770.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1247 0 0 0 76991 9 0 0 25 0 1 0 1727264056 5632000 1234 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1375 1234 145 145 0 1230 0 [pid=25947] vsize: 5500 Current children cumulated CPU time (s) 770.02 Current children cumulated vsize (Kb) 7624 [startup+780.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1248 0 0 0 77991 9 0 0 25 0 1 0 1727264056 5632000 1235 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1375 1235 145 145 0 1230 0 [pid=25947] vsize: 5500 Current children cumulated CPU time (s) 780.02 Current children cumulated vsize (Kb) 7624 [startup+790.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1248 0 0 0 78991 9 0 0 25 0 1 0 1727264056 5632000 1235 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1375 1235 145 145 0 1230 0 [pid=25947] vsize: 5500 Current children cumulated CPU time (s) 790.02 Current children cumulated vsize (Kb) 7624 [startup+800.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1254 0 0 0 79991 9 0 0 25 0 1 0 1727264056 5664768 1241 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1383 1241 145 145 0 1238 0 [pid=25947] vsize: 5532 Current children cumulated CPU time (s) 800.02 Current children cumulated vsize (Kb) 7656 [startup+810.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1254 0 0 0 80991 9 0 0 25 0 1 0 1727264056 5664768 1241 4294967295 134512640 135094434 3221224448 3221223072 134562092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1383 1241 145 145 0 1238 0 [pid=25947] vsize: 5532 Current children cumulated CPU time (s) 810.02 Current children cumulated vsize (Kb) 7656 [startup+820.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1255 0 0 0 81991 9 0 0 25 0 1 0 1727264056 5664768 1242 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1383 1242 145 145 0 1238 0 [pid=25947] vsize: 5532 Current children cumulated CPU time (s) 820.02 Current children cumulated vsize (Kb) 7656 [startup+830.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1260 0 0 0 82992 9 0 0 25 0 1 0 1727264056 5697536 1247 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1391 1247 145 145 0 1246 0 [pid=25947] vsize: 5564 Current children cumulated CPU time (s) 830.03 Current children cumulated vsize (Kb) 7688 [startup+840.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1261 0 0 0 83992 9 0 0 25 0 1 0 1727264056 5697536 1248 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1391 1248 145 145 0 1246 0 [pid=25947] vsize: 5564 Current children cumulated CPU time (s) 840.03 Current children cumulated vsize (Kb) 7688 [startup+850.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1261 0 0 0 84992 9 0 0 25 0 1 0 1727264056 5697536 1248 4294967295 134512640 135094434 3221224448 3221223072 134562149 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1391 1248 145 145 0 1246 0 [pid=25947] vsize: 5564 Current children cumulated CPU time (s) 850.03 Current children cumulated vsize (Kb) 7688 [startup+860.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1261 0 0 0 85993 9 0 0 25 0 1 0 1727264056 5697536 1248 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1391 1248 145 145 0 1246 0 [pid=25947] vsize: 5564 Current children cumulated CPU time (s) 860.04 Current children cumulated vsize (Kb) 7688 [startup+870.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1267 0 0 0 86993 9 0 0 25 0 1 0 1727264056 5730304 1254 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1399 1254 145 145 0 1254 0 [pid=25947] vsize: 5596 Current children cumulated CPU time (s) 870.04 Current children cumulated vsize (Kb) 7720 [startup+880.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1267 0 0 0 87993 9 0 0 25 0 1 0 1727264056 5730304 1254 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1399 1254 145 145 0 1254 0 [pid=25947] vsize: 5596 Current children cumulated CPU time (s) 880.04 Current children cumulated vsize (Kb) 7720 [startup+890.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1273 0 0 0 88993 9 0 0 25 0 1 0 1727264056 5763072 1260 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1407 1260 145 145 0 1262 0 [pid=25947] vsize: 5628 Current children cumulated CPU time (s) 890.04 Current children cumulated vsize (Kb) 7752 [startup+900.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1273 0 0 0 89993 9 0 0 25 0 1 0 1727264056 5763072 1260 4294967295 134512640 135094434 3221224448 3221223040 134551428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1407 1260 145 145 0 1262 0 [pid=25947] vsize: 5628 Current children cumulated CPU time (s) 900.04 Current children cumulated vsize (Kb) 7752 [startup+910.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1273 0 0 0 90994 9 0 0 25 0 1 0 1727264056 5763072 1260 4294967295 134512640 135094434 3221224448 3221223120 134555238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1407 1260 145 145 0 1262 0 [pid=25947] vsize: 5628 Current children cumulated CPU time (s) 910.05 Current children cumulated vsize (Kb) 7752 [startup+920.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1278 0 0 0 91994 9 0 0 25 0 1 0 1727264056 5795840 1265 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1415 1265 145 145 0 1270 0 [pid=25947] vsize: 5660 Current children cumulated CPU time (s) 920.05 Current children cumulated vsize (Kb) 7784 [startup+930.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1278 0 0 0 92994 9 0 0 25 0 1 0 1727264056 5795840 1265 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1415 1265 145 145 0 1270 0 [pid=25947] vsize: 5660 Current children cumulated CPU time (s) 930.05 Current children cumulated vsize (Kb) 7784 [startup+940.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1278 0 0 0 93994 9 0 0 25 0 1 0 1727264056 5795840 1265 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1415 1265 145 145 0 1270 0 [pid=25947] vsize: 5660 Current children cumulated CPU time (s) 940.05 Current children cumulated vsize (Kb) 7784 [startup+950.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1278 0 0 0 94995 9 0 0 25 0 1 0 1727264056 5795840 1265 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1415 1265 145 145 0 1270 0 [pid=25947] vsize: 5660 Current children cumulated CPU time (s) 950.06 Current children cumulated vsize (Kb) 7784 [startup+960.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1278 0 0 0 95995 9 0 0 25 0 1 0 1727264056 5795840 1265 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1415 1265 145 145 0 1270 0 [pid=25947] vsize: 5660 Current children cumulated CPU time (s) 960.06 Current children cumulated vsize (Kb) 7784 [startup+970.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1278 0 0 0 96995 9 0 0 25 0 1 0 1727264056 5795840 1265 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1415 1265 145 145 0 1270 0 [pid=25947] vsize: 5660 Current children cumulated CPU time (s) 970.06 Current children cumulated vsize (Kb) 7784 [startup+980.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1283 0 0 0 97996 9 0 0 25 0 1 0 1727264056 5828608 1270 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1423 1270 145 145 0 1278 0 [pid=25947] vsize: 5692 Current children cumulated CPU time (s) 980.07 Current children cumulated vsize (Kb) 7816 [startup+990.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1283 0 0 0 98996 9 0 0 25 0 1 0 1727264056 5828608 1270 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1423 1270 145 145 0 1278 0 [pid=25947] vsize: 5692 Current children cumulated CPU time (s) 990.07 Current children cumulated vsize (Kb) 7816 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1283 0 0 0 99996 9 0 0 25 0 1 0 1727264056 5828608 1270 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1423 1270 145 145 0 1278 0 [pid=25947] vsize: 5692 Current children cumulated CPU time (s) 1000.07 Current children cumulated vsize (Kb) 7816 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1283 0 0 0 100996 9 0 0 25 0 1 0 1727264056 5828608 1270 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1423 1270 145 145 0 1278 0 [pid=25947] vsize: 5692 Current children cumulated CPU time (s) 1010.07 Current children cumulated vsize (Kb) 7816 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1283 0 0 0 101996 9 0 0 25 0 1 0 1727264056 5828608 1270 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1423 1270 145 145 0 1278 0 [pid=25947] vsize: 5692 Current children cumulated CPU time (s) 1020.07 Current children cumulated vsize (Kb) 7816 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1288 0 0 0 102997 9 0 0 25 0 1 0 1727264056 5861376 1275 4294967295 134512640 135094434 3221224448 3221223040 134557210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1431 1275 145 145 0 1286 0 [pid=25947] vsize: 5724 Current children cumulated CPU time (s) 1030.08 Current children cumulated vsize (Kb) 7848 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1288 0 0 0 103997 9 0 0 25 0 1 0 1727264056 5861376 1275 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1431 1275 145 145 0 1286 0 [pid=25947] vsize: 5724 Current children cumulated CPU time (s) 1040.08 Current children cumulated vsize (Kb) 7848 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1294 0 0 0 104997 9 0 0 25 0 1 0 1727264056 5894144 1281 4294967295 134512640 135094434 3221224448 3221223136 134554751 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1439 1281 145 145 0 1294 0 [pid=25947] vsize: 5756 Current children cumulated CPU time (s) 1050.08 Current children cumulated vsize (Kb) 7880 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1294 0 0 0 105997 9 0 0 25 0 1 0 1727264056 5894144 1281 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1439 1281 145 145 0 1294 0 [pid=25947] vsize: 5756 Current children cumulated CPU time (s) 1060.08 Current children cumulated vsize (Kb) 7880 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1294 0 0 0 106998 9 0 0 25 0 1 0 1727264056 5894144 1281 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1439 1281 145 145 0 1294 0 [pid=25947] vsize: 5756 Current children cumulated CPU time (s) 1070.09 Current children cumulated vsize (Kb) 7880 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1294 0 0 0 107998 9 0 0 25 0 1 0 1727264056 5894144 1281 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1439 1281 145 145 0 1294 0 [pid=25947] vsize: 5756 Current children cumulated CPU time (s) 1080.09 Current children cumulated vsize (Kb) 7880 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1294 0 0 0 108998 9 0 0 25 0 1 0 1727264056 5894144 1281 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1439 1281 145 145 0 1294 0 [pid=25947] vsize: 5756 Current children cumulated CPU time (s) 1090.09 Current children cumulated vsize (Kb) 7880 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1299 0 0 0 109998 9 0 0 25 0 1 0 1727264056 5926912 1286 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1447 1286 145 145 0 1302 0 [pid=25947] vsize: 5788 Current children cumulated CPU time (s) 1100.09 Current children cumulated vsize (Kb) 7912 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1301 0 0 0 110999 9 0 0 25 0 1 0 1727264056 5926912 1288 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1447 1288 145 145 0 1302 0 [pid=25947] vsize: 5788 Current children cumulated CPU time (s) 1110.1 Current children cumulated vsize (Kb) 7912 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1301 0 0 0 111999 9 0 0 25 0 1 0 1727264056 5926912 1288 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1447 1288 145 145 0 1302 0 [pid=25947] vsize: 5788 Current children cumulated CPU time (s) 1120.1 Current children cumulated vsize (Kb) 7912 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1301 0 0 0 112999 9 0 0 25 0 1 0 1727264056 5926912 1288 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1447 1288 145 145 0 1302 0 [pid=25947] vsize: 5788 Current children cumulated CPU time (s) 1130.1 Current children cumulated vsize (Kb) 7912 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1301 0 0 0 113999 9 0 0 25 0 1 0 1727264056 5926912 1288 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1447 1288 145 145 0 1302 0 [pid=25947] vsize: 5788 Current children cumulated CPU time (s) 1140.1 Current children cumulated vsize (Kb) 7912 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1306 0 0 0 114999 9 0 0 25 0 1 0 1727264056 5959680 1293 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1455 1293 145 145 0 1310 0 [pid=25947] vsize: 5820 Current children cumulated CPU time (s) 1150.1 Current children cumulated vsize (Kb) 7944 [startup+1160.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1307 0 0 0 116000 9 0 0 25 0 1 0 1727264056 5959680 1294 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1455 1294 145 145 0 1310 0 [pid=25947] vsize: 5820 Current children cumulated CPU time (s) 1160.11 Current children cumulated vsize (Kb) 7944 [startup+1170.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1307 0 0 0 117000 9 0 0 25 0 1 0 1727264056 5959680 1294 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1455 1294 145 145 0 1310 0 [pid=25947] vsize: 5820 Current children cumulated CPU time (s) 1170.11 Current children cumulated vsize (Kb) 7944 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1310 0 0 0 118000 9 0 0 25 0 1 0 1727264056 5959680 1297 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1455 1297 145 145 0 1310 0 [pid=25947] vsize: 5820 Current children cumulated CPU time (s) 1180.11 Current children cumulated vsize (Kb) 7944 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1310 0 0 0 119000 9 0 0 25 0 1 0 1727264056 5959680 1297 4294967295 134512640 135094434 3221224448 3221223084 134562042 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25947/statm): 1455 1297 145 145 0 1310 0 [pid=25947] vsize: 5820 Current children cumulated CPU time (s) 1190.11 Current children cumulated vsize (Kb) 7944 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1311 0 0 0 120000 9 0 0 25 0 1 0 1727264056 5959680 1298 4294967295 134512640 135094434 3221224448 3221223100 134562036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 1455 1298 145 145 0 1310 0 [pid=25947] vsize: 5820 Current children cumulated CPU time (s) 1200.11 Current children cumulated vsize (Kb) 7944 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/58 25947 Raw data (/proc/25943/stat): 25943 (minisat+_script) S 25942 25943 17733 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1727264051 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/25943/statm): 531 226 485 147 0 384 0 [pid=25943] vsize: 2124 Raw data (/proc/25947/stat): 25947 (minisat+_64-bit) R 25943 25943 17733 0 -1 0 1311 0 0 0 120000 9 0 0 25 0 1 0 1727264056 5959680 1298 4294967295 134512640 135094434 3221224448 3221223100 134562036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25947/statm): 1455 1298 145 145 0 1310 0 [pid=25947] vsize: 5820 Current children cumulated CPU time (s) 1200.11 Current children cumulated vsize (Kb) 7944 Sending SIGTERM to -25943 Sleeping 2 seconds One traced child (pid=25943) ended because it received signal 15 (SIGTERM) One traced child (pid=25947) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1200.09 CPU time (s): 1200.11 CPU user time (s): 1200 CPU system time (s): 0.102984 CPU usage (%): 100.001 Max. virtual memory (cumulated for all children) (Kb): 7944
ERROR: no interpretation found !