Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-5.opb |
MD5SUM | 70070c820bc7d178cc8f33b42e0deead |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -28 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 595 |
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 | 595 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 595 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.05 |
Number of variables | 595 |
Total number of constraints | 28143 |
Number of constraints which are clauses | 28143 |
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 | 2 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc5 THE 2005-05-25 17:14:29 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=21905 boxname=wulflinc5 idbench=323 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 70070c820bc7d178cc8f33b42e0deead /oldhome/oroussel/tmp/wulflinc5/normalized-frb35-17-5.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-frb35-17-5.opb IDLAUNCH: 21905 /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: 697676 kB Buffers: 34060 kB Cached: 281736 kB SwapCached: 472 kB Active: 78328 kB Inactive: 239556 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 697424 kB SwapTotal: 2097136 kB SwapFree: 2095792 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5228 kB Slab: 13328 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 17:34:59 (client local time) WITH STATUS 152 IN 1229.85 SECONDS stats: 21905 7 1229.85 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 28143 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 | 28143 56286 | 9381 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -21[0m c ---[ 0]---> Sorter-cost:26814 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 56290 122394 | 18763 0 0 nan | 0.000 % | c | 100 | 55818 121416 | 20639 78 529 6.8 | 1.319 % | c | 250 | 55350 120416 | 22703 201 1432 7.1 | 2.831 % | c | 475 | 54323 118193 | 24973 376 3383 9.0 | 5.942 % | c ============================================================================== c [1mFound solution: -26[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 678 | 53263 115977 | 17754 507 5021 9.9 | 5.942 % | c | 778 | 52841 115047 | 19529 588 6229 10.6 | 11.045 % | c | 928 | 52322 113884 | 21482 715 7585 10.6 | 12.707 % | c | 1153 | 51428 111886 | 23630 895 9815 11.0 | 15.557 % | c | 1490 | 49468 107434 | 25993 1105 12672 11.5 | 22.140 % | c | 1996 | 47638 103232 | 28592 1527 18207 11.9 | 28.026 % | c | 2756 | 44784 96705 | 31452 2088 27733 13.3 | 37.330 % | c | 3895 | 41359 88683 | 34597 2945 40667 13.8 | 48.818 % | c ============================================================================== c [1mFound solution: -27[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4578 | 40279 86235 | 13426 3372 48651 14.4 | 48.818 % | c | 4678 | 39986 85593 | 14768 3439 49906 14.5 | 53.601 % | c | 4828 | 39929 85464 | 16245 3585 53525 14.9 | 53.786 % | c | 5053 | 39738 84989 | 17870 3769 58890 15.6 | 54.485 % | c | 5390 | 39304 83962 | 19657 3970 63529 16.0 | 55.987 % | c | 5897 | 38689 82488 | 21622 4286 73190 17.1 | 58.330 % | c | 6656 | 37185 78940 | 23784 4674 86185 18.4 | 63.301 % | c | 7795 | 36622 77561 | 26163 5675 129966 22.9 | 65.275 % | c | 9504 | 35725 75401 | 28779 7136 192067 26.9 | 68.457 % | c ============================================================================== c [1mFound solution: -28[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10440 | 35152 73982 | 11717 7917 243425 30.7 | 68.457 % | c | 10540 | 35113 73891 | 12888 7988 246532 30.9 | 70.655 % | c | 10690 | 35113 73891 | 14177 8138 257579 31.7 | 70.655 % | c | 10915 | 35077 73801 | 15595 8322 262608 31.6 | 70.789 % | c | 11252 | 34978 73564 | 17154 8601 274225 31.9 | 71.134 % | c ============================================================================== c [1mFound solution: -29[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11391 | 34971 73570 | 11657 8688 275965 31.8 | 71.134 % | c | 11491 | 34902 73413 | 12822 8759 278380 31.8 | 71.445 % | c | 11641 | 34902 73413 | 14104 8909 284047 31.9 | 71.446 % | c | 11867 | 34896 73399 | 15515 9119 294059 32.2 | 71.466 % | c | 12204 | 34763 73092 | 17067 9394 321190 34.2 | 71.903 % | c | 12711 | 34609 72711 | 18773 9712 337264 34.7 | 72.472 % | c | 13470 | 34605 72698 | 20651 10457 386838 37.0 | 72.487 % | c | 14610 | 34380 72154 | 22716 11454 436165 38.1 | 73.293 % | c | 16319 | 33765 70670 | 24987 12907 541843 42.0 | 75.434 % | c ============================================================================== c [1mFound solution: -30[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16658 | 33651 70365 | 11217 13078 538486 41.2 | 75.434 % | c | 16758 | 33651 70365 | 12338 13178 543720 41.3 | 75.826 % | c | 16908 | 33598 70240 | 13572 13315 549004 41.2 | 76.011 % | c | 17133 | 33492 69992 | 14929 13474 555912 41.3 | 76.371 % | c | 17471 | 33492 69992 | 16422 13812 572516 41.5 | 76.370 % | c | 17978 | 33390 69747 | 18065 14288 590646 41.3 | 76.730 % | c | 18737 | 33266 69453 | 19871 15005 645411 43.0 | 77.151 % | c | 19876 | 33263 69446 | 21858 16138 775398 48.0 | 77.161 % | c | 21586 | 33025 68873 | 24044 17787 883974 49.7 | 78.013 % | c | 24149 | 33025 68873 | 26449 20350 1110021 54.5 | 78.013 % | c | 27994 | 33025 68873 | 29094 24195 1446802 59.8 | 78.013 % | c | 33762 | 32912 68606 | 32003 29913 1976061 66.1 | 78.408 % | c | 42412 | 32688 68047 | 35203 38230 2602127 68.1 | 79.250 % | c ============================================================================== c [1mFound solution: -31[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 54813 | 32709 68118 | 10903 50607 3631857 71.8 | 79.250 % | c | 54913 | 32665 68010 | 11993 17614 1027595 58.3 | 79.420 % | c | 55063 | 32665 68010 | 13192 17764 1033328 58.2 | 79.420 % | c | 55288 | 32632 67926 | 14511 17973 1042889 58.0 | 79.537 % | c | 55625 | 32632 67926 | 15963 18310 1077898 58.9 | 79.537 % | c | 56133 | 32626 67909 | 17559 18796 1115938 59.4 | 79.563 % | c | 56892 | 32626 67909 | 19315 19555 1163074 59.5 | 79.563 % | c | 58031 | 32585 67812 | 21246 20688 1247141 60.3 | 79.706 % | c | 59739 | 32585 67812 | 23371 22396 1358285 60.6 | 79.706 % | c ============================================================================== c [1mFound solution: -32[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 61766 | 32459 67492 | 10819 24393 1480169 60.7 | 79.706 % | c | 61866 | 32459 67492 | 11900 24493 1483862 60.6 | 80.152 % | c | 62016 | 32422 67401 | 13090 24627 1493869 60.7 | 80.285 % | c | 62241 | 32400 67340 | 14400 24844 1515014 61.0 | 80.372 % | c | 62579 | 32361 67247 | 15840 25167 1534905 61.0 | 80.510 % | c | 63085 | 32361 67247 | 17424 25673 1569859 61.1 | 80.510 % | c | 63845 | 32361 67247 | 19166 26433 1617338 61.2 | 80.510 % | c | 64985 | 32361 67247 | 21083 27573 1724425 62.5 | 80.510 % | c | 66693 | 32361 67247 | 23191 29281 1823567 62.3 | 80.510 % | c | 69255 | 32361 67247 | 25510 31843 2022398 63.5 | 80.510 % | c | 73099 | 32266 67009 | 28061 35630 2258988 63.4 | 80.852 % | c | 78867 | 32266 67009 | 30867 41398 2541641 61.4 | 80.852 % | c | 87517 | 32261 66998 | 33954 17592 605784 34.4 | 80.868 % | c | 100493 | 32145 66707 | 37350 30555 1527180 50.0 | 81.251 % | c | 119954 | 32136 66686 | 41085 50010 2776028 55.5 | 81.282 % | c | 149146 | 32059 66501 | 45193 39406 2390640 60.7 | 81.558 % | c | 192935 | 32018 66406 | 49713 40611 2365930 58.3 | 81.696 % | c ============================================================================== c [1mFound solution: -33[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 234340 | 31964 66282 | 10654 33803 1904300 56.3 | 81.696 % | c | 234440 | 31964 66282 | 11719 16070 660384 41.1 | 81.909 % | c | 234590 | 31939 66229 | 12891 16216 667281 41.1 | 81.980 % | c | 234817 | 31939 66229 | 14180 16443 680004 41.4 | 81.980 % | c | 235155 | 31853 66019 | 15598 16755 688813 41.1 | 82.286 % | c | 235661 | 31853 66019 | 17158 17261 714839 41.4 | 82.286 % | c | 236420 | 31848 66006 | 18874 18019 754497 41.9 | 82.307 % | c | 237559 | 31848 66006 | 20761 19158 827477 43.2 | 82.307 % | c | 239268 | 31848 66006 | 22837 20867 941214 45.1 | 82.307 % | c | 241830 | 31845 65999 | 25121 23424 1134066 48.4 | 82.317 % | c | 245674 | 31832 65966 | 27633 27261 1379284 50.6 | 82.368 % | c | 251442 | 31821 65939 | 30397 33025 1770495 53.6 | 82.409 % | c | 260091 | 31723 65693 | 33436 41618 2363593 56.8 | 82.781 % | c | 273065 | 31702 65642 | 36780 21888 1194237 54.6 | 82.858 % | c | 292526 | 31595 65388 | 40458 41329 2455787 59.4 | 83.236 % | c | 321718 | 31590 65375 | 44504 31574 1206245 38.2 | 83.256 % | c | 365507 | 31587 65368 | 48954 33871 1201100 35.5 | 83.266 % | c | 431191 | 31587 65368 | 53850 55118 1835677 33.3 | 83.266 % | c | 529717 | 31516 65201 | 59235 54938 1748182 31.8 | 83.511 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 24815 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.92 0.95 0.98 2/54 24811 Raw data (stat): 24811 (runsolver) R 24810 7266 7265 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782375625 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 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.0013 s] Raw data (loadavg): 0.93 0.96 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0018 s] Raw data (loadavg): 0.94 0.96 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0012 s] Raw data (loadavg): 0.95 0.96 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0013 s] Raw data (loadavg): 0.96 0.96 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.002 s] Raw data (loadavg): 0.96 0.96 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0024 s] Raw data (loadavg): 0.97 0.96 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0025 s] Raw data (loadavg): 0.97 0.96 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0022 s] Raw data (loadavg): 0.98 0.96 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0026 s] Raw data (loadavg): 0.98 0.96 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.003 s] Raw data (loadavg): 0.98 0.96 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.003 s] Raw data (loadavg): 0.98 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.004 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.004 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/55 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.7 s] Raw data (loadavg): 0.99 0.97 0.98 1/53 24815 Raw data (stat): 24811 (minisat+_script) S 24810 7266 7265 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 782375625 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.7 CPU time (s): 1229.85 CPU user time (s): 1229.52 CPU system time (s): 0.332949 CPU usage (%): 100.012 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####