Name | submitted/manquinho/primes-dimacs-cnf/normalized-jnh201.opb |
MD5SUM | ba509931ad93c2223be235a06a9b3100 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 84 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 200 |
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 | 200 |
Number of bits of the sum of numbers in the objective function | 8 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 200 |
Number of bits of the biggest sum of numbers | 8 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 236.038 |
Number of variables | 200 |
Total number of constraints | 900 |
Number of constraints which are clauses | 900 |
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 | 14 |
LAUNCH ON wulflinc18 THE 2005-09-18 18:04:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2569 boxname=wulflinc18 idbench=225 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ba509931ad93c2223be235a06a9b3100 /oldhome/oroussel/tmp/wulflinc18/normalized-jnh201.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-jnh201.opb IDLAUNCH: 2569 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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: 916556 kB Buffers: 35256 kB Cached: 47948 kB SwapCached: 844 kB Active: 66196 kB Inactive: 19608 kB HighTotal: 131008 kB HighFree: 80136 kB LowTotal: 903652 kB LowFree: 836420 kB SwapTotal: 2097892 kB SwapFree: 2096548 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5764 kB Slab: 26688 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:08:48 (client local time) WITH STATUS 30 IN 236.038 SECONDS stats: 2569 0 236.038 30
c Parsing PB file... c Converting 900 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 | 900 4354 | 300 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 91[0m c ---[ 0]---> Sorter-cost: 5812 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7 | 7643 20134 | 2547 7 55 7.9 | 0.000 % | c ============================================================================== c [1mFound solution: 90[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13 | 7637 20121 | 2545 13 297 22.8 | 0.000 % | c ============================================================================== c [1mFound solution: 89[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 45 | 7671 20224 | 2557 45 2338 52.0 | 0.000 % | c | 145 | 7661 20204 | 2812 144 4678 32.5 | 0.344 % | c | 296 | 7661 20204 | 3093 295 9597 32.5 | 0.344 % | c | 524 | 7661 20204 | 3403 523 14825 28.3 | 0.344 % | c | 863 | 7661 20204 | 3743 862 23294 27.0 | 0.344 % | c | 1369 | 7584 19885 | 4118 1367 35364 25.9 | 0.795 % | c ============================================================================== c [1mFound solution: 88[0m c ---[ 0]---> Sorter-cost: 5014 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2070 | 13182 32991 | 4394 2068 68009 32.9 | 0.795 % | c | 2170 | 13182 32991 | 4833 2168 71761 33.1 | 0.541 % | c | 2321 | 13182 32991 | 5316 2319 74583 32.2 | 0.541 % | c | 2546 | 13182 32991 | 5848 2544 82494 32.4 | 0.541 % | c | 2884 | 13182 32991 | 6433 2882 94988 33.0 | 0.541 % | c | 3391 | 13182 32991 | 7076 3389 103684 30.6 | 0.541 % | c | 4150 | 13182 32991 | 7784 4148 121382 29.3 | 0.541 % | c | 5289 | 13182 32991 | 8562 5287 172477 32.6 | 0.541 % | c | 6997 | 13137 32898 | 9418 6992 253826 36.3 | 0.829 % | c ============================================================================== c [1mFound solution: 87[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7544 | 13169 32996 | 4389 7539 283313 37.6 | 0.829 % | c | 7647 | 13169 32996 | 4827 3873 166067 42.9 | 0.851 % | c | 7797 | 13169 32996 | 5310 4023 171939 42.7 | 0.851 % | c | 8023 | 13169 32996 | 5841 4249 183522 43.2 | 0.851 % | c | 8360 | 13169 32996 | 6425 4586 197924 43.2 | 0.851 % | c | 8866 | 13169 32996 | 7068 5092 216423 42.5 | 0.851 % | c | 9625 | 13169 32996 | 7775 5851 242083 41.4 | 0.851 % | c | 10766 | 13169 32996 | 8552 6992 293834 42.0 | 0.851 % | c | 12479 | 13169 32996 | 9408 8705 369997 42.5 | 0.851 % | c ============================================================================== c [1mFound solution: 86[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13121 | 13161 32973 | 4387 9313 398952 42.8 | 0.851 % | c | 13222 | 13161 32973 | 4825 2430 86766 35.7 | 0.970 % | c | 13373 | 13161 32973 | 5308 2581 90040 34.9 | 0.970 % | c | 13600 | 13161 32973 | 5839 2808 98313 35.0 | 0.970 % | c | 13937 | 13161 32973 | 6423 3145 110420 35.1 | 0.970 % | c | 14449 | 13161 32973 | 7065 3657 134007 36.6 | 0.970 % | c | 15208 | 13161 32973 | 7771 4416 169709 38.4 | 0.970 % | c | 16347 | 13161 32973 | 8549 5555 215812 38.9 | 0.970 % | c | 18055 | 13161 32973 | 9403 7263 289205 39.8 | 0.970 % | c | 20617 | 13161 32973 | 10344 9825 408768 41.6 | 0.970 % | c | 24461 | 13161 32973 | 11378 7999 307594 38.5 | 0.970 % | c | 30228 | 13161 32973 | 12516 7497 290824 38.8 | 0.970 % | c | 38877 | 13161 32973 | 13768 9241 415530 45.0 | 0.970 % | c | 51851 | 13161 32973 | 15145 14631 684462 46.8 | 0.970 % | c | 71313 | 13161 32973 | 16659 9364 364970 39.0 | 0.970 % | c ============================================================================== c [1mFound solution: 85[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 77313 | 13184 33043 | 4394 15364 642247 41.8 | 0.970 % | c | 77413 | 13184 33043 | 4833 3941 120976 30.7 | 0.980 % | c | 77563 | 13184 33043 | 5316 4091 129505 31.7 | 0.980 % | c | 77789 | 13184 33043 | 5848 4317 139837 32.4 | 0.980 % | c | 78127 | 13184 33043 | 6433 4655 153420 33.0 | 0.980 % | c | 78634 | 13184 33043 | 7076 5162 173725 33.7 | 0.980 % | c | 79393 | 13184 33043 | 7784 5921 205280 34.7 | 0.980 % | c | 80534 | 13184 33043 | 8562 7062 255409 36.2 | 0.980 % | c | 82243 | 13184 33043 | 9418 8771 334044 38.1 | 0.980 % | c | 84805 | 13184 33043 | 10360 6041 210229 34.8 | 0.980 % | c | 88649 | 13184 33043 | 11396 9885 377028 38.1 | 0.980 % | c | 94417 | 13184 33043 | 12536 9730 415903 42.7 | 0.980 % | c | 103067 | 13184 33043 | 13790 11485 482514 42.0 | 0.980 % | c | 116041 | 13062 32646 | 15169 7081 268058 37.9 | 1.506 % | c ============================================================================== c [1mFound solution: 84[0m c ---[ 0]---> Sorter-cost: 5112 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 127961 | 18892 46287 | 6297 11073 399170 36.0 | 1.506 % | c | 128061 | 18892 46287 | 6926 5637 186107 33.0 | 1.099 % | c | 128212 | 18892 46287 | 7619 5788 192905 33.3 | 1.099 % | c | 128440 | 18892 46287 | 8381 6016 203393 33.8 | 1.099 % | c | 128777 | 18892 46287 | 9219 6353 217625 34.3 | 1.099 % | c | 129283 | 18892 46287 | 10141 6859 240003 35.0 | 1.099 % | c | 130042 | 18882 46267 | 11155 7617 269340 35.4 | 1.141 % | c | 131183 | 18865 46232 | 12271 8757 326443 37.3 | 1.214 % | c | 132892 | 18844 46189 | 13498 10465 394646 37.7 | 1.305 % | c | 135454 | 18844 46189 | 14847 13027 502469 38.6 | 1.305 % | c | 139298 | 18844 46189 | 16332 9116 320335 35.1 | 1.305 % | c | 145065 | 18764 45964 | 17966 9818 352820 35.9 | 1.584 % | c ============================================================================== c [1mOptimal solution: 84[0m s OPTIMUM FOUND v x1 -x2 -x3 x4 x5 -x6 -x7 x8 -x9 x10 -x11 -x12 -x13 -x14 x15 -x16 -x17 x18 -x19 x20 -x21 x22 x23 -x24 -x25 -x26 -x27 x28 -x29 -x30 -x31 x32 -x33 x34 -x35 x36 -x37 x38 -x39 x40 x41 -x42 x43 -x44 -x45 x46 x47 -x48 -x49 x50 x51 -x52 -x53 x54 -x55 x56 -x57 -x58 -x59 -x60 -x61 x62 -x63 x64 -x65 x66 -x67 -x68 x69 -x70 -x71 x72 -x73 x74 -x75 x76 x77 -x78 -x79 x80 x81 -x82 x83 -x84 -x85 -x86 -x87 x88 x89 -x90 -x91 -x92 x93 -x94 -x95 -x96 -x97 x98 -x99 x100 -x101 x102 x103 -x104 -x105 x106 x107 -x108 -x109 x110 -x111 x112 x113 -x114 -x115 x116 x117 -x118 x119 -x120 -x121 x122 -x123 x124 -x125 x126 -x127 x128 -x129 x130 -x131 x132 -x133 x134 -x135 x136 -x137 x138 x139 -x140 -x141 x142 x143 -x144 -x145 x146 x147 -x148 -x149 -x150 -x151 x152 x153 -x154 -x155 x156 x157 -x158 -x159 x160 -x161 x162 -x163 -x164 x165 -x166 -x167 -x168 -x169 x170 -x171 -x172 -x173 x174 x175 -x176 x177 -x178 -x179 x180 -x181 x182 -x183 x184 x185 -x186 -x187 x188 -x189 x190 -x191 -x192 -x193 x194 -x195 -x196 x197 -x198 -x199 x200 c _______________________________________________________________________________ c c restarts : 68 c conflicts : 147182 (624 /sec) c decisions : 230893 (979 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 235.784 s c _______________________________________________________________________________
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/5046/stat): 5046 (minisat+_script) R 5045 5046 31027 0 -1 0 19 0 0 0 0 0 0 0 21 0 1 0 1843241259 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/5046/statm): 174 3 169 147 0 27 0 [pid=5046] 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=5047 New process pid=5048 New process pid=5049 execve syscall for /bin/sed executable One traced child (pid=5048) 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=5049) exited with status: 0 One traced child (pid=5047) exited with status: 0 New process pid=5050 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-jnh201.opb [startup+10.0034 s] Raw data (loadavg): 0.69 0.93 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1170 0 0 0 982 6 0 0 25 0 1 0 1843241264 5521408 1151 4294967295 134512640 135094434 3221224448 3221223136 134554763 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5050/statm): 1348 1151 145 145 0 1203 0 [pid=5050] vsize: 5392 Current children cumulated CPU time (s) 9.89 Current children cumulated vsize (Kb) 7516 [startup+20.0043 s] Raw data (loadavg): 0.74 0.94 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1332 0 0 0 1980 8 0 0 25 0 1 0 1843241264 6209536 1313 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5050/statm): 1516 1313 145 145 0 1371 0 [pid=5050] vsize: 6064 Current children cumulated CPU time (s) 19.89 Current children cumulated vsize (Kb) 8188 [startup+30.0052 s] Raw data (loadavg): 0.78 0.94 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1440 0 0 0 2977 9 0 0 25 0 1 0 1843241264 6643712 1421 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5050/statm): 1622 1421 145 145 0 1477 0 [pid=5050] vsize: 6488 Current children cumulated CPU time (s) 29.87 Current children cumulated vsize (Kb) 8612 [startup+40.0062 s] Raw data (loadavg): 0.81 0.94 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1502 0 0 0 3975 10 0 0 25 0 1 0 1843241264 6893568 1483 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5050/statm): 1683 1483 145 145 0 1538 0 [pid=5050] vsize: 6732 Current children cumulated CPU time (s) 39.86 Current children cumulated vsize (Kb) 8856 [startup+50.0081 s] Raw data (loadavg): 0.84 0.94 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1642 0 0 0 4971 13 0 0 25 0 1 0 1843241264 7458816 1623 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5050/statm): 1821 1623 145 145 0 1676 0 [pid=5050] vsize: 7284 Current children cumulated CPU time (s) 49.85 Current children cumulated vsize (Kb) 9408 [startup+60.009 s] Raw data (loadavg): 0.86 0.94 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1732 0 0 0 5969 14 0 0 25 0 1 0 1843241264 7835648 1713 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5050/statm): 1913 1713 145 145 0 1768 0 [pid=5050] vsize: 7652 Current children cumulated CPU time (s) 59.84 Current children cumulated vsize (Kb) 9776 [startup+70.0099 s] Raw data (loadavg): 0.88 0.94 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1761 0 0 0 6969 15 0 0 25 0 1 0 1843241264 7950336 1742 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 1941 1742 145 145 0 1796 0 [pid=5050] vsize: 7764 Current children cumulated CPU time (s) 69.85 Current children cumulated vsize (Kb) 9888 [startup+80.0108 s] Raw data (loadavg): 0.90 0.94 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1859 0 0 0 7966 17 0 0 25 0 1 0 1843241264 8359936 1840 4294967295 134512640 135094434 3221224448 3221223040 134557357 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2041 1840 145 145 0 1896 0 [pid=5050] vsize: 8164 Current children cumulated CPU time (s) 79.84 Current children cumulated vsize (Kb) 10288 [startup+90.0117 s] Raw data (loadavg): 0.92 0.95 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1863 0 0 0 8965 17 0 0 25 0 1 0 1843241264 8392704 1844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2049 1844 145 145 0 1904 0 [pid=5050] vsize: 8196 Current children cumulated CPU time (s) 89.83 Current children cumulated vsize (Kb) 10320 [startup+100.013 s] Raw data (loadavg): 0.93 0.95 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1865 0 0 0 9965 17 0 0 25 0 1 0 1843241264 8392704 1846 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2049 1846 145 145 0 1904 0 [pid=5050] vsize: 8196 Current children cumulated CPU time (s) 99.83 Current children cumulated vsize (Kb) 10320 [startup+110.014 s] Raw data (loadavg): 0.94 0.95 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1888 0 0 0 10965 18 0 0 25 0 1 0 1843241264 8556544 1869 4294967295 134512640 135094434 3221224448 3221223120 134555957 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2089 1869 145 145 0 1944 0 [pid=5050] vsize: 8356 Current children cumulated CPU time (s) 109.84 Current children cumulated vsize (Kb) 10480 [startup+120.015 s] Raw data (loadavg): 0.95 0.95 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1890 0 0 0 11965 18 0 0 25 0 1 0 1843241264 8556544 1871 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2089 1871 145 145 0 1944 0 [pid=5050] vsize: 8356 Current children cumulated CPU time (s) 119.84 Current children cumulated vsize (Kb) 10480 [startup+130.015 s] Raw data (loadavg): 0.95 0.95 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1890 0 0 0 12965 18 0 0 25 0 1 0 1843241264 8556544 1871 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2089 1871 145 145 0 1944 0 [pid=5050] vsize: 8356 Current children cumulated CPU time (s) 129.84 Current children cumulated vsize (Kb) 10480 [startup+140.016 s] Raw data (loadavg): 0.96 0.95 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1890 0 0 0 13964 19 0 0 25 0 1 0 1843241264 8556544 1871 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5050/statm): 2089 1871 145 145 0 1944 0 [pid=5050] vsize: 8356 Current children cumulated CPU time (s) 139.84 Current children cumulated vsize (Kb) 10480 [startup+150.018 s] Raw data (loadavg): 0.97 0.95 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1890 0 0 0 14963 19 0 0 25 0 1 0 1843241264 8556544 1871 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2089 1871 145 145 0 1944 0 [pid=5050] vsize: 8356 Current children cumulated CPU time (s) 149.83 Current children cumulated vsize (Kb) 10480 [startup+160.019 s] Raw data (loadavg): 0.97 0.95 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1897 0 0 0 15963 19 0 0 25 0 1 0 1843241264 8589312 1878 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2097 1878 145 145 0 1952 0 [pid=5050] vsize: 8388 Current children cumulated CPU time (s) 159.83 Current children cumulated vsize (Kb) 10512 [startup+170.019 s] Raw data (loadavg): 0.98 0.95 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1902 0 0 0 16963 19 0 0 25 0 1 0 1843241264 8622080 1883 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2105 1883 145 145 0 1960 0 [pid=5050] vsize: 8420 Current children cumulated CPU time (s) 169.83 Current children cumulated vsize (Kb) 10544 [startup+180.02 s] Raw data (loadavg): 0.98 0.95 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1902 0 0 0 17964 19 0 0 25 0 1 0 1843241264 8622080 1883 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2105 1883 145 145 0 1960 0 [pid=5050] vsize: 8420 Current children cumulated CPU time (s) 179.84 Current children cumulated vsize (Kb) 10544 [startup+190.021 s] Raw data (loadavg): 0.98 0.96 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 1913 0 0 0 18963 20 0 0 25 0 1 0 1843241264 8671232 1894 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2117 1894 145 145 0 1972 0 [pid=5050] vsize: 8468 Current children cumulated CPU time (s) 189.84 Current children cumulated vsize (Kb) 10592 [startup+200.022 s] Raw data (loadavg): 0.98 0.96 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 2020 0 0 0 19963 20 0 0 25 0 1 0 1843241264 8908800 2001 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2175 2001 145 145 0 2030 0 [pid=5050] vsize: 8700 Current children cumulated CPU time (s) 199.84 Current children cumulated vsize (Kb) 10824 [startup+210.023 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 2021 0 0 0 20964 20 0 0 25 0 1 0 1843241264 8908800 2002 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2175 2002 145 145 0 2030 0 [pid=5050] vsize: 8700 Current children cumulated CPU time (s) 209.85 Current children cumulated vsize (Kb) 10824 [startup+220.024 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 2107 0 0 0 21962 21 0 0 25 0 1 0 1843241264 9265152 2088 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2262 2088 145 145 0 2117 0 [pid=5050] vsize: 9048 Current children cumulated CPU time (s) 219.84 Current children cumulated vsize (Kb) 11172 [startup+230.025 s] Raw data (loadavg): 0.99 0.96 0.97 2/57 5050 Raw data (/proc/5046/stat): 5046 (minisat+_script) S 5045 5046 31027 0 -1 0 288 239 0 0 0 1 0 0 16 0 1 0 1843241259 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5046/statm): 531 226 485 147 0 384 0 [pid=5046] vsize: 2124 Raw data (/proc/5050/stat): 5050 (minisat+_64-bit) R 5046 5046 31027 0 -1 0 2110 0 0 0 22962 21 0 0 25 0 1 0 1843241264 9277440 2091 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5050/statm): 2265 2091 145 145 0 2120 0 [pid=5050] vsize: 9060 Current children cumulated CPU time (s) 229.84 Current children cumulated vsize (Kb) 11184 One traced child (pid=5050) exited with status: 30 One traced child (pid=5046) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 236.199 CPU time (s): 236.038 CPU user time (s): 235.796 CPU system time (s): 0.241963 CPU usage (%): 99.9317 Max. virtual memory (cumulated for all children) (Kb): 11184
Verifier: OK 84