Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare1_1.opb |
MD5SUM | 452acf9ed3adc2d2cfe293dad01c0934 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 167110 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 180 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 6442450938 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 536870912 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 6442450938 |
Number of bits of the biggest sum of numbers | 33 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.02 |
Number of variables | 280 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 45 |
Number of constraints which are nor clauses,nor cardinality constraints | 11 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 130 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc5 THE 2005-05-25 20:41:39 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22298 boxname=wulflinc5 idbench=1114 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 452acf9ed3adc2d2cfe293dad01c0934 /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-markshare1_1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-markshare1_1.opb IDLAUNCH: 22298 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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.007 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: 637404 kB Buffers: 34416 kB Cached: 341832 kB SwapCached: 472 kB Active: 81400 kB Inactive: 296900 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 637152 kB SwapTotal: 2097136 kB SwapFree: 2095792 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5228 kB Slab: 13276 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 21:02:09 (client local time) WITH STATUS 152 IN 1229.85 SECONDS stats: 22298 7 1229.85 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 17 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###### c -- Clauses(.)/Splits(s): (none) c ---[ 16]---> BDD-cost: 10 c ---[ 15]---> BDD-cost: 10 c ---[ 14]---> BDD-cost: 10 c ---[ 13]---> BDD-cost: 10 c ---[ 12]---> BDD-cost: 10 c ---[ 10]---> Adder-cost: 662 maxlim: 3510008 bits: 23/22 c ---[ 8]---> Adder-cost: 660 maxlim: 3759828 bits: 23/22 c ---[ 6]---> Adder-cost: 770 maxlim: 3884662 bits: 23/22 c ---[ 4]---> Adder-cost: 500 maxlim: 3402645 bits: 23/22 c ---[ 2]---> Adder-cost: 574 maxlim: 3468109 bits: 23/22 c ---[ 0]---> Adder-cost: 558 maxlim: 3462997 bits: 23/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 25238 89630 | 8412 0 0 nan | 0.000 % | c | 100 | 25230 89604 | 9253 99 750 7.6 | 7.959 % | c | 250 | 25230 89604 | 10178 249 3701 14.9 | 7.959 % | c | 475 | 25230 89604 | 11196 474 5830 12.3 | 7.959 % | c ============================================================================== c [1mFound solution: 5377694[0m c ---[ 0]---> Sorter-cost: 1725 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 604 | 29633 99881 | 9877 603 6492 10.8 | 7.959 % | c ============================================================================== c [1mFound solution: 5293744[0m c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 607 | 29665 99990 | 9888 606 7209 11.9 | 7.959 % | c | 707 | 29657 99964 | 10876 705 9192 13.0 | 5.848 % | c | 857 | 29657 99964 | 11964 855 11646 13.6 | 5.848 % | c ============================================================================== c [1mFound solution: 4764672[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 862 | 29687 100034 | 9895 860 11711 13.6 | 5.848 % | c ============================================================================== c [1mFound solution: 1599618[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 881 | 29718 100104 | 9906 879 11938 13.6 | 5.848 % | c | 981 | 29718 100104 | 10896 979 12922 13.2 | 5.853 % | c | 1131 | 29718 100104 | 11986 1129 41916 37.1 | 5.853 % | c | 1356 | 29718 100104 | 13184 1354 49026 36.2 | 5.853 % | c | 1693 | 29702 100052 | 14503 1689 52554 31.1 | 5.887 % | c | 2199 | 29679 99985 | 15953 2192 59198 27.0 | 5.957 % | c | 2960 | 29671 99959 | 17549 2952 80220 27.2 | 5.975 % | c | 4099 | 29663 99933 | 19303 4090 121045 29.6 | 5.992 % | c | 5807 | 29655 99907 | 21234 5797 175882 30.3 | 6.010 % | c | 8369 | 29655 99907 | 23357 8359 283693 33.9 | 6.010 % | c | 12213 | 29639 99855 | 25693 12201 440130 36.1 | 6.045 % | c | 17980 | 29631 99829 | 28262 17966 664991 37.0 | 6.062 % | c | 26630 | 29631 99829 | 31089 26616 1159633 43.6 | 6.062 % | c | 39605 | 29631 99829 | 34198 20932 1149938 54.9 | 6.062 % | c | 59066 | 29623 99803 | 37618 16230 879352 54.2 | 6.080 % | c | 88259 | 29608 99762 | 41379 20636 1003940 48.6 | 6.132 % | c ============================================================================== c [1mFound solution: 279567[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 89650 | 29408 99201 | 9802 21458 995466 46.4 | 6.132 % | c | 89750 | 29408 99201 | 10782 5465 179655 32.9 | 7.083 % | c | 89900 | 29408 99201 | 11860 5615 182646 32.5 | 7.083 % | c | 90125 | 29408 99201 | 13046 5840 186971 32.0 | 7.083 % | c | 90462 | 29408 99201 | 14351 6177 196392 31.8 | 7.083 % | c | 90968 | 29408 99201 | 15786 6683 207978 31.1 | 7.083 % | c | 91727 | 29408 99201 | 17364 7442 224614 30.2 | 7.083 % | c | 92867 | 29408 99201 | 19101 8582 261733 30.5 | 7.083 % | c | 94575 | 29408 99201 | 21011 10290 361389 35.1 | 7.083 % | c | 97139 | 29408 99201 | 23112 12854 437079 34.0 | 7.083 % | c | 100983 | 29408 99201 | 25423 16698 596929 35.7 | 7.083 % | c | 106750 | 29408 99201 | 27966 22465 820896 36.5 | 7.083 % | c | 115400 | 29408 99201 | 30762 14540 507022 34.9 | 7.083 % | c | 128375 | 29390 99161 | 33839 27514 1069997 38.9 | 7.188 % | c | 147837 | 29382 99135 | 37223 25873 1158066 44.8 | 7.205 % | c | 177029 | 29382 99135 | 40945 28960 1496602 51.7 | 7.205 % | c | 220820 | 29358 99079 | 45039 18307 765399 41.8 | 7.362 % | c | 286504 | 29342 99027 | 49543 21496 871280 40.5 | 7.397 % | c | 385030 | 29334 99001 | 54498 47574 2572959 54.1 | 7.415 % | c | 532819 | 29287 98896 | 59948 32047 1863533 58.1 | 7.641 % | c | 754502 | 29287 98896 | 65942 32983 2410685 73.1 | 7.641 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 26056 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### 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 Raw data (loadavg): 0.91 0.97 0.96 2/54 26052 Raw data (stat): 26052 (runsolver) R 26051 7266 7265 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783618803 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0004 s] Raw data (loadavg): 0.93 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0201 s] Raw data (loadavg): 0.94 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0212 s] Raw data (loadavg): 0.95 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0204 s] Raw data (loadavg): 0.95 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0211 s] Raw data (loadavg): 0.96 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0212 s] Raw data (loadavg): 0.97 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0206 s] Raw data (loadavg): 0.97 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0214 s] Raw data (loadavg): 0.98 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0217 s] Raw data (loadavg): 0.98 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.022 s] Raw data (loadavg): 0.98 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.022 s] Raw data (loadavg): 0.98 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.022 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.022 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.022 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.027 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.027 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.028 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.029 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.029 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.029 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.04 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.04 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.04 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26056 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26109 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26109 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26109 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26109 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26109 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26109 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26109 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26111 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26111 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26111 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26111 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/55 26111 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.84 s] Raw data (loadavg): 0.99 0.97 0.96 1/53 26111 Raw data (stat): 26052 (minisat+_script) S 26051 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 15 0 1 0 783618803 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.84 CPU time (s): 1229.85 CPU user time (s): 1229.52 CPU system time (s): 0.329949 CPU usage (%): 100 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####