Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-n3709.opb |
MD5SUM | bd3b7059f5a46c39741d1666410238f7 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 155000 |
Biggest coefficient in the objective function | 4294967296 |
Number of bits for the biggest coefficient in the objective function | 33 |
Sum of the numbers in the objective function | 29610373267604 |
Number of bits of the sum of numbers in the objective function | 45 |
Biggest number in a constraint | 4294967296 |
Number of bits of the biggest number in a constraint | 33 |
Biggest sum of numbers in a constraint | 29610373267604 |
Number of bits of the biggest sum of numbers | 45 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 1.42678 |
Number of variables | 155000 |
Total number of constraints | 5150 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 5150 |
Minimum length of a constraint | 31 |
Maximum length of a constraint | 3000 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc6 THE 2005-05-28 12:44:42 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=24615 boxname=wulflinc6 idbench=1087 idsolver=17 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: bd3b7059f5a46c39741d1666410238f7 /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-n3709.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-n3709.opb IDLAUNCH: 24615 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 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.042 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: 694768 kB Buffers: 34404 kB Cached: 282260 kB SwapCached: 624 kB Active: 32228 kB Inactive: 286620 kB HighTotal: 131008 kB HighFree: 48664 kB LowTotal: 903652 kB LowFree: 646104 kB SwapTotal: 2097136 kB SwapFree: 2095604 kB Dirty: 32 kB Writeback: 0 kB Mapped: 5180 kB Slab: 15284 kB Committed_AS: 63732 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-28 12:57:44 (client local time) WITH STATUS 1 IN 781.568 SECONDS stats: 24615 7 781.568 1 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c This solver internally uses Chaff 2004.11.15 Simplified Unexpected exception : St9bad_alloc #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Enforcing Stack size limit: 67108864 bytes Current StackSize limit: 67108864 bytes Raw data (loadavg): 0.94 0.96 0.91 2/54 3643 Raw data (stat): 3643 (runsolver) R 3642 25568 25567 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 806679466 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.0009 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 2200 0 0 0 994 5 0 0 25 0 1 0 806679466 8089600 1524 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 1975 1524 300 300 0 1675 0 vsize: 7900 [startup+20.002 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 2725 0 0 0 1992 7 0 0 25 0 1 0 806679466 9441280 2040 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 2305 2040 300 300 0 2005 0 vsize: 9220 [startup+30.0027 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 3874 0 0 0 2990 10 0 0 25 0 1 0 806679466 13410304 2478 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 3274 2478 300 300 0 2974 0 vsize: 13096 [startup+40.0039 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 4107 0 0 0 3990 10 0 0 25 0 1 0 806679466 13950976 2706 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3406 2706 300 300 0 3106 0 vsize: 13624 [startup+50.0051 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 4363 0 0 0 4989 11 0 0 25 0 1 0 806679466 14626816 2958 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3571 2958 300 300 0 3271 0 vsize: 14284 [startup+60.0052 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 4597 0 0 0 5988 12 0 0 25 0 1 0 806679466 15302656 3188 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3736 3188 300 300 0 3436 0 vsize: 14944 [startup+70.0058 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 4809 0 0 0 6988 13 0 0 25 0 1 0 806679466 15843328 3397 4294967295 134512640 135726644 3221224592 3221221792 134576140 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3868 3397 300 300 0 3568 0 vsize: 15472 [startup+80.0069 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 5009 0 0 0 7988 13 0 0 25 0 1 0 806679466 16384000 3593 4294967295 134512640 135726644 3221224592 3221221680 134556179 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4000 3593 300 300 0 3700 0 vsize: 16000 [startup+90.0077 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 5197 0 0 0 8987 14 0 0 25 0 1 0 806679466 16924672 3778 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4132 3778 300 300 0 3832 0 vsize: 16528 [startup+100.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 5375 0 0 0 9987 15 0 0 25 0 1 0 806679466 17330176 3953 4294967295 134512640 135726644 3221224592 3221221680 134556192 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 4231 3953 300 300 0 3931 0 vsize: 16924 [startup+110.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 7450 0 0 0 10982 20 0 0 25 0 1 0 806679466 25403392 4616 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6202 4616 300 300 0 5902 0 vsize: 24808 [startup+120.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 7508 0 0 0 11981 21 0 0 25 0 1 0 806679466 25403392 4671 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6202 4671 300 300 0 5902 0 vsize: 24808 [startup+130.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 7560 0 0 0 12981 22 0 0 25 0 1 0 806679466 25403392 4721 4294967295 134512640 135726644 3221224592 3221221620 134523458 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6202 4721 300 300 0 5902 0 vsize: 24808 [startup+140.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 7614 0 0 0 13980 22 0 0 25 0 1 0 806679466 25403392 4772 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6202 4772 300 300 0 5902 0 vsize: 24808 [startup+150.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 7691 0 0 0 14980 23 0 0 25 0 1 0 806679466 25403392 4847 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6202 4847 300 300 0 5902 0 vsize: 24808 [startup+160.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 7751 0 0 0 15979 23 0 0 25 0 1 0 806679466 25538560 4905 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6235 4905 300 300 0 5935 0 vsize: 24940 [startup+170.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 7886 0 0 0 16979 24 0 0 25 0 1 0 806679466 25808896 5038 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6301 5038 300 300 0 6001 0 vsize: 25204 [startup+180.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 8017 0 0 0 17979 25 0 0 25 0 1 0 806679466 26214400 5167 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6400 5167 300 300 0 6100 0 vsize: 25600 [startup+190.017 s] Raw data (loadavg): 1.15 1.00 0.92 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 8144 0 0 0 18979 25 0 0 25 0 1 0 806679466 26619904 5292 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6499 5292 300 300 0 6199 0 vsize: 25996 [startup+200.018 s] Raw data (loadavg): 1.12 1.00 0.92 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 8270 0 0 0 19978 26 0 0 25 0 1 0 806679466 26890240 5416 4294967295 134512640 135726644 3221224592 3221221680 134556192 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6565 5416 300 300 0 6265 0 vsize: 26260 [startup+210.018 s] Raw data (loadavg): 1.10 1.00 0.92 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 8390 0 0 0 20978 26 0 0 25 0 1 0 806679466 27160576 5534 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6631 5534 300 300 0 6331 0 vsize: 26524 [startup+220.02 s] Raw data (loadavg): 1.09 1.00 0.92 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 8510 0 0 0 21978 27 0 0 25 0 1 0 806679466 27566080 5652 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6730 5652 300 300 0 6430 0 vsize: 26920 [startup+230.02 s] Raw data (loadavg): 1.07 1.00 0.92 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 8627 0 0 0 22978 28 0 0 25 0 1 0 806679466 27836416 5767 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6796 5767 300 300 0 6496 0 vsize: 27184 [startup+240.021 s] Raw data (loadavg): 1.06 1.00 0.92 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 8741 0 0 0 23977 29 0 0 25 0 1 0 806679466 28106752 5879 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6862 5879 300 300 0 6562 0 vsize: 27448 [startup+250.021 s] Raw data (loadavg): 1.13 1.02 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 8853 0 0 0 24977 29 0 0 25 0 1 0 806679466 28377088 5989 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6928 5989 300 300 0 6628 0 vsize: 27712 [startup+260.023 s] Raw data (loadavg): 1.11 1.02 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 8963 0 0 0 25977 29 0 0 25 0 1 0 806679466 28782592 6097 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7027 6097 300 300 0 6727 0 vsize: 28108 [startup+270.023 s] Raw data (loadavg): 1.09 1.01 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 9071 0 0 0 26977 30 0 0 25 0 1 0 806679466 29052928 6204 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7093 6204 300 300 0 6793 0 vsize: 28372 [startup+280.023 s] Raw data (loadavg): 1.08 1.01 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 9178 0 0 0 27976 30 0 0 25 0 1 0 806679466 29323264 6309 4294967295 134512640 135726644 3221224592 3221221680 134556168 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7159 6309 300 300 0 6859 0 vsize: 28636 [startup+290.025 s] Raw data (loadavg): 1.06 1.01 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 9283 0 0 0 28977 31 0 0 25 0 1 0 806679466 29593600 6412 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7225 6412 300 300 0 6925 0 vsize: 28900 [startup+300.026 s] Raw data (loadavg): 1.05 1.01 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 9384 0 0 0 29976 32 0 0 25 0 1 0 806679466 29863936 6512 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7291 6512 300 300 0 6991 0 vsize: 29164 [startup+310.026 s] Raw data (loadavg): 1.04 1.01 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 9485 0 0 0 30976 32 0 0 25 0 1 0 806679466 30134272 6611 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7357 6611 300 300 0 7057 0 vsize: 29428 [startup+320.027 s] Raw data (loadavg): 1.04 1.01 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 9585 0 0 0 31976 33 0 0 25 0 1 0 806679466 30404608 6709 4294967295 134512640 135726644 3221224592 3221221680 134556168 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7423 6709 300 300 0 7123 0 vsize: 29692 [startup+330.026 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 9682 0 0 0 32975 34 0 0 25 0 1 0 806679466 30674944 6805 4294967295 134512640 135726644 3221224592 3221221680 134556168 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7489 6805 300 300 0 7189 0 vsize: 29956 [startup+340.025 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 9779 0 0 0 33975 34 0 0 25 0 1 0 806679466 30810112 6900 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7522 6900 300 300 0 7222 0 vsize: 30088 [startup+350.025 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 9873 0 0 0 34974 35 0 0 25 0 1 0 806679466 31080448 6993 4294967295 134512640 135726644 3221224592 3221221680 134556168 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7588 6993 300 300 0 7288 0 vsize: 30352 [startup+360.025 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 9968 0 0 0 35974 35 0 0 25 0 1 0 806679466 31350784 7086 4294967295 134512640 135726644 3221224592 3221221680 134556192 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7654 7086 300 300 0 7354 0 vsize: 30616 [startup+370.024 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 10060 0 0 0 36974 36 0 0 25 0 1 0 806679466 31621120 7177 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7720 7177 300 300 0 7420 0 vsize: 30880 [startup+380.024 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 10151 0 0 0 37974 36 0 0 25 0 1 0 806679466 31891456 7266 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7786 7266 300 300 0 7486 0 vsize: 31144 [startup+390.023 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 10242 0 0 0 38973 37 0 0 25 0 1 0 806679466 32161792 7356 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7852 7356 300 300 0 7552 0 vsize: 31408 [startup+400.023 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 10330 0 0 0 39973 37 0 0 25 0 1 0 806679466 32296960 7442 4294967295 134512640 135726644 3221224592 3221220992 135278611 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7885 7442 300 300 0 7585 0 vsize: 31540 [startup+410.023 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 10418 0 0 0 40973 38 0 0 25 0 1 0 806679466 32567296 7529 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7951 7529 300 300 0 7651 0 vsize: 31804 [startup+420.023 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 10506 0 0 0 41973 38 0 0 25 0 1 0 806679466 32837632 7615 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 8017 7615 300 300 0 7717 0 vsize: 32068 [startup+430.023 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 10591 0 0 0 42972 39 0 0 25 0 1 0 806679466 32972800 7699 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 8050 7699 300 300 0 7750 0 vsize: 32200 [startup+440.023 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 10676 0 0 0 43973 39 0 0 25 0 1 0 806679466 33243136 7783 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 8116 7783 300 300 0 7816 0 vsize: 32464 [startup+450.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 10761 0 0 0 44972 39 0 0 25 0 1 0 806679466 33513472 7866 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 8182 7866 300 300 0 7882 0 vsize: 32728 [startup+460.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 10844 0 0 0 45972 40 0 0 25 0 1 0 806679466 33648640 7948 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 8215 7948 300 300 0 7915 0 vsize: 32860 [startup+470.022 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 10926 0 0 0 46972 41 0 0 25 0 1 0 806679466 33918976 8029 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 8281 8029 300 300 0 7981 0 vsize: 33124 [startup+480.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 14821 0 0 0 47964 49 0 0 25 0 1 0 806679466 49254400 9104 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9104 300 300 0 11725 0 vsize: 48100 [startup+490.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 14850 0 0 0 48963 50 0 0 25 0 1 0 806679466 49254400 9132 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9132 300 300 0 11725 0 vsize: 48100 [startup+500.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 14878 0 0 0 49963 50 0 0 25 0 1 0 806679466 49254400 9159 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9159 300 300 0 11725 0 vsize: 48100 [startup+510.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 14905 0 0 0 50962 51 0 0 25 0 1 0 806679466 49254400 9185 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9185 300 300 0 11725 0 vsize: 48100 [startup+520.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 14934 0 0 0 51962 52 0 0 25 0 1 0 806679466 49254400 9212 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9212 300 300 0 11725 0 vsize: 48100 [startup+530.021 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 14961 0 0 0 52962 52 0 0 25 0 1 0 806679466 49254400 9238 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9238 300 300 0 11725 0 vsize: 48100 [startup+540.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 14988 0 0 0 53962 52 0 0 25 0 1 0 806679466 49254400 9264 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9264 300 300 0 11725 0 vsize: 48100 [startup+550.019 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 15015 0 0 0 54962 53 0 0 25 0 1 0 806679466 49254400 9290 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9290 300 300 0 11725 0 vsize: 48100 [startup+560.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 15043 0 0 0 55962 53 0 0 25 0 1 0 806679466 49254400 9316 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9316 300 300 0 11725 0 vsize: 48100 [startup+570.02 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 15070 0 0 0 56961 54 0 0 25 0 1 0 806679466 49254400 9342 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9342 300 300 0 11725 0 vsize: 48100 [startup+580.019 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 15096 0 0 0 57961 55 0 0 25 0 1 0 806679466 49254400 9367 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9367 300 300 0 11725 0 vsize: 48100 [startup+590.019 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 15122 0 0 0 58961 55 0 0 25 0 1 0 806679466 49254400 9392 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9392 300 300 0 11725 0 vsize: 48100 [startup+600.019 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 15147 0 0 0 59960 56 0 0 25 0 1 0 806679466 49254400 9416 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9416 300 300 0 11725 0 vsize: 48100 [startup+610.018 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 15189 0 0 0 60961 56 0 0 25 0 1 0 806679466 49254400 9456 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9456 300 300 0 11725 0 vsize: 48100 [startup+620.018 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 15226 0 0 0 61961 56 0 0 25 0 1 0 806679466 49254400 9492 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9492 300 300 0 11725 0 vsize: 48100 [startup+630.019 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 15251 0 0 0 62960 56 0 0 25 0 1 0 806679466 49254400 9516 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9516 300 300 0 11725 0 vsize: 48100 [startup+640.018 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 15276 0 0 0 63960 57 0 0 25 0 1 0 806679466 49254400 9540 4294967295 134512640 135726644 3221224592 3221221680 134556192 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9540 300 300 0 11725 0 vsize: 48100 [startup+650.017 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 15300 0 0 0 64960 57 0 0 25 0 1 0 806679466 49254400 9563 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9563 300 300 0 11725 0 vsize: 48100 [startup+660.017 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 15325 0 0 0 65960 57 0 0 25 0 1 0 806679466 49254400 9587 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 12025 9587 300 300 0 11725 0 vsize: 48100 [startup+670.016 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 16576 0 0 0 66957 60 0 0 25 0 1 0 806679466 54390784 10837 4294967295 134512640 135726644 3221224592 3221221176 134604401 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 13279 10837 300 300 0 12979 0 vsize: 53116 [startup+680.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 56151 0 0 0 67872 147 0 0 25 0 1 0 806679466 188362752 42534 4294967295 134512640 135726644 3221224592 3159630908 134604474 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 45987 42534 300 300 0 45687 0 vsize: 183948 [startup+690.035 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 93065 0 0 0 68794 226 0 0 25 0 1 0 806679466 308142080 60837 4294967295 134512640 135726644 3221224592 3164336780 135278568 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 75230 60837 300 300 0 74930 0 vsize: 300920 [startup+700.048 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 114865 0 0 0 69744 276 0 0 25 0 1 0 806679466 440590336 82406 4294967295 134512640 135726644 3221224592 3160863008 134784885 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 107566 82406 300 300 0 107266 0 vsize: 430264 [startup+710.048 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 140147 0 0 0 70686 335 0 0 25 0 1 0 806679466 449761280 95195 4294967295 134512640 135726644 3221224592 3167481672 135280770 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 109805 95195 300 300 0 109505 0 vsize: 439220 [startup+720.049 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 178034 0 0 0 71611 410 0 0 25 0 1 0 806679466 570540032 113488 4294967295 134512640 135726644 3221224592 3160520944 134554678 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 139292 113488 300 300 0 138992 0 vsize: 557168 [startup+730.048 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 214122 0 0 0 72530 492 0 0 25 0 1 0 806679466 671203328 124797 4294967295 134512640 135726644 3221224592 3160637708 134604458 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 163868 124798 300 300 0 163568 0 vsize: 655472 [startup+740.048 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 230183 0 0 0 73491 531 0 0 25 0 1 0 806679466 724762624 140662 4294967295 134512640 135726644 3221224592 3159768856 135282351 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 176944 140663 300 300 0 176644 0 vsize: 707776 [startup+750.049 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 251106 0 0 0 74445 577 0 0 25 0 1 0 806679466 755445760 161339 4294967295 134512640 135726644 3221224592 3159767448 135282351 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 184435 161341 300 300 0 184135 0 vsize: 737740 [startup+760.049 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 270892 0 0 0 75394 627 0 0 25 0 1 0 806679466 783425536 180900 4294967295 134512640 135726644 3221224592 3162254608 134784471 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 191266 180900 300 300 0 190966 0 vsize: 765064 [startup+770.057 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 274500 0 0 0 76386 635 0 0 25 0 1 0 806679466 789745664 184466 4294967295 134512640 135726644 3221224592 3185203132 135103081 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 192809 184466 300 300 0 192509 0 vsize: 771236 [startup+780.057 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 274502 0 0 0 77372 649 0 0 25 0 1 0 806679466 475156480 115577 4294967295 134512640 135726644 3221224592 3221222936 135280487 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 116005 115577 300 300 0 115705 0 vsize: 464020 [startup+781.403 s] Raw data (loadavg): 1.00 1.00 0.93 1/53 3643 Raw data (stat): 3643 (pb2sat) R 3642 25568 25567 0 -1 0 274502 0 0 0 77372 649 0 0 25 0 1 0 806679466 475156480 115577 4294967295 134512640 135726644 3221224592 3221222936 135280487 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 116005 115577 300 300 0 115705 0 vsize: 0 Child status: 1 Real time (s): 781.402 CPU time (s): 781.568 CPU user time (s): 774.835 CPU system time (s): 6.73298 CPU usage (%): 100.021 Max. virtual memory (Kb): 771236 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####