Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii32d1.opb |
MD5SUM | 151e246868267296e134c3c76a3cb289 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 285 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 664 |
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 | 664 |
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 | 664 |
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 | 1.02484 |
Number of variables | 664 |
Total number of constraints | 3035 |
Number of constraints which are clauses | 3035 |
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 | 32 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc31 THE 2005-05-27 04:45:00 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22909 boxname=wulflinc31 idbench=155 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 151e246868267296e134c3c76a3cb289 /oldhome/oroussel/tmp/wulflinc31/normalized-ii32d1.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc31/normalized-ii32d1.opb IDLAUNCH: 22909 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 669736 kB Buffers: 33856 kB Cached: 303252 kB SwapCached: 1056 kB Active: 85028 kB Inactive: 254252 kB HighTotal: 131008 kB HighFree: 11732 kB LowTotal: 903652 kB LowFree: 658004 kB SwapTotal: 2097892 kB SwapFree: 2095948 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5108 kB Slab: 19964 kB Committed_AS: 63800 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 05:05:30 (client local time) WITH STATUS 152 IN 1229.85 SECONDS stats: 22909 7 1229.85 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 3035 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 | 3035 9828 | 1011 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 319[0m c ---[ 0]---> Sorter-cost:30182 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22 | 39401 94869 | 13133 22 879 40.0 | 0.000 % | c ============================================================================== c [1mFound solution: 304[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 78 | 39566 95345 | 13188 77 5158 67.0 | 0.000 % | c ============================================================================== c [1mFound solution: 294[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 82 | 39693 95707 | 13231 81 5475 67.6 | 0.000 % | c | 182 | 39693 95707 | 14554 181 15088 83.4 | 0.172 % | c | 334 | 39693 95707 | 16009 333 24915 74.8 | 0.172 % | c | 559 | 39693 95707 | 17610 558 43774 78.4 | 0.172 % | c | 897 | 39610 95534 | 19371 893 84437 94.6 | 0.353 % | c | 1403 | 39610 95534 | 21308 1399 139614 99.8 | 0.353 % | c | 2164 | 39439 95178 | 23439 2155 228675 106.1 | 0.718 % | c | 3305 | 39396 95089 | 25783 3295 356671 108.2 | 0.806 % | c | 5014 | 39147 94550 | 28361 4996 564213 112.9 | 1.379 % | c ============================================================================== c [1mFound solution: 293[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6786 | 39147 94597 | 13049 6766 805584 119.1 | 1.379 % | c | 6886 | 38248 92654 | 14353 6843 807275 118.0 | 3.544 % | c | 7036 | 38101 92333 | 15789 6978 810806 116.2 | 3.889 % | c | 7261 | 38101 92333 | 17368 7203 835914 116.1 | 3.889 % | c | 7598 | 38101 92333 | 19105 7540 859380 114.0 | 3.889 % | c | 8107 | 38058 92242 | 21015 8048 902377 112.1 | 3.985 % | c | 8867 | 37957 92027 | 23117 8806 985841 112.0 | 4.209 % | c | 10007 | 37816 91714 | 25428 9942 1069396 107.6 | 4.550 % | c | 11717 | 37684 91426 | 27971 11649 1217804 104.5 | 4.858 % | c | 14279 | 37684 91426 | 30768 14211 1480329 104.2 | 4.858 % | c | 18124 | 35697 87013 | 33845 17979 1810517 100.7 | 9.636 % | c | 23891 | 35469 86509 | 37230 23742 2607070 109.8 | 10.169 % | c | 32540 | 35409 86375 | 40953 32384 3450033 106.5 | 10.317 % | c | 45515 | 35296 86126 | 45048 15064 1255595 83.4 | 10.585 % | c ============================================================================== c [1mFound solution: 292[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 51755 | 35264 86031 | 11754 21218 1737423 81.9 | 10.585 % | c | 51858 | 35264 86031 | 12929 10712 660163 61.6 | 10.688 % | c | 52010 | 35264 86031 | 14222 10864 673235 62.0 | 10.688 % | c | 52238 | 35264 86031 | 15644 11092 680554 61.4 | 10.688 % | c | 52575 | 35264 86031 | 17209 11429 710291 62.1 | 10.688 % | c | 53081 | 35264 86031 | 18929 11935 753857 63.2 | 10.688 % | c | 53840 | 35264 86031 | 20822 12694 821047 64.7 | 10.688 % | c | 54983 | 35264 86031 | 22905 13837 917888 66.3 | 10.688 % | c | 56691 | 35264 86031 | 25195 15545 1062283 68.3 | 10.688 % | c | 59253 | 35264 86031 | 27715 18107 1325662 73.2 | 10.688 % | c | 63098 | 35264 86031 | 30486 21952 1774222 80.8 | 10.688 % | c | 68864 | 35212 85914 | 33535 27717 2220091 80.1 | 10.817 % | c | 77513 | 35212 85914 | 36889 36366 2981361 82.0 | 10.817 % | c | 90487 | 35212 85914 | 40577 23247 1770661 76.2 | 10.817 % | c | 109948 | 35153 85787 | 44635 42707 3210142 75.2 | 10.953 % | c | 139140 | 35153 85787 | 49099 40523 2721836 67.2 | 10.953 % | c ============================================================================== c [1mFound solution: 291[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 148770 | 35121 85732 | 11707 50152 3413506 68.1 | 10.953 % | c | 148871 | 35121 85732 | 12877 9760 464349 47.6 | 11.093 % | c | 149026 | 35121 85732 | 14165 9915 478892 48.3 | 11.093 % | c | 149251 | 35121 85732 | 15582 10140 496222 48.9 | 11.093 % | c | 149591 | 35121 85732 | 17140 10480 520952 49.7 | 11.093 % | c | 150097 | 35121 85732 | 18854 10986 558194 50.8 | 11.093 % | c | 150858 | 35121 85732 | 20739 11747 618457 52.6 | 11.093 % | c | 151998 | 35121 85732 | 22813 12887 693350 53.8 | 11.093 % | c | 153707 | 35121 85732 | 25094 14596 828225 56.7 | 11.093 % | c | 156271 | 34396 84085 | 27604 17133 993365 58.0 | 12.902 % | c | 160118 | 34396 84085 | 30364 20980 1393378 66.4 | 12.902 % | c | 165886 | 34396 84085 | 33401 26748 2021075 75.6 | 12.902 % | c | 174535 | 34396 84085 | 36741 35397 2864710 80.9 | 12.902 % | c | 187509 | 34396 84085 | 40415 23543 1656176 70.3 | 12.902 % | c ============================================================================== c [1mFound solution: 290[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 205542 | 34380 84019 | 11460 41576 3086386 74.2 | 12.902 % | c | 205642 | 34380 84019 | 12606 8593 377408 43.9 | 12.961 % | c | 205794 | 34380 84019 | 13866 8745 388045 44.4 | 12.961 % | c | 206019 | 34380 84019 | 15253 8970 404742 45.1 | 12.961 % | c | 206356 | 34380 84019 | 16778 9307 431358 46.3 | 12.961 % | c | 206863 | 34380 84019 | 18456 9814 473568 48.3 | 12.961 % | c | 207622 | 34380 84019 | 20302 10573 515082 48.7 | 12.961 % | c | 208764 | 34380 84019 | 22332 11715 574466 49.0 | 12.961 % | c | 210472 | 34380 84019 | 24565 13423 669115 49.8 | 12.961 % | c | 213034 | 34380 84019 | 27022 15985 795872 49.8 | 12.961 % | c | 216881 | 34380 84019 | 29724 19832 998091 50.3 | 12.961 % | c | 222647 | 34380 84019 | 32696 25598 1341738 52.4 | 12.961 % | c | 231296 | 34380 84019 | 35966 34247 2022239 59.0 | 12.961 % | c | 244270 | 34380 84019 | 39563 21209 1538693 72.5 | 12.961 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 1005 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.84 0.89 0.73 2/55 1001 Raw data (stat): 1001 (runsolver) R 1000 29618 29617 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853361900 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.0012 s] Raw data (loadavg): 0.86 0.90 0.73 2/56 1005 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.0021 s] Raw data (loadavg): 0.88 0.90 0.73 2/56 1005 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.0025 s] Raw data (loadavg): 0.90 0.90 0.73 2/56 1005 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.0029 s] Raw data (loadavg): 0.91 0.91 0.74 2/56 1005 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.0039 s] Raw data (loadavg): 0.93 0.91 0.74 2/56 1007 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.0051 s] Raw data (loadavg): 0.94 0.91 0.74 2/56 1007 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.0057 s] Raw data (loadavg): 0.95 0.91 0.74 2/56 1007 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.0066 s] Raw data (loadavg): 0.95 0.92 0.74 2/56 1007 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.0079 s] Raw data (loadavg): 0.96 0.92 0.75 2/56 1007 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.008 s] Raw data (loadavg): 0.97 0.92 0.75 2/56 1007 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.009 s] Raw data (loadavg): 0.97 0.92 0.75 2/56 1009 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.011 s] Raw data (loadavg): 0.98 0.92 0.75 2/56 1009 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.01 s] Raw data (loadavg): 0.98 0.93 0.75 2/56 1009 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.011 s] Raw data (loadavg): 0.98 0.93 0.76 2/56 1009 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.012 s] Raw data (loadavg): 0.98 0.93 0.76 2/56 1009 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.013 s] Raw data (loadavg): 0.99 0.93 0.76 2/56 1009 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.013 s] Raw data (loadavg): 0.99 0.93 0.76 2/56 1011 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.013 s] Raw data (loadavg): 0.99 0.94 0.76 2/56 1011 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.014 s] Raw data (loadavg): 0.99 0.94 0.77 2/56 1011 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.014 s] Raw data (loadavg): 0.99 0.94 0.77 2/56 1011 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.015 s] Raw data (loadavg): 0.99 0.94 0.77 2/56 1011 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.016 s] Raw data (loadavg): 0.99 0.94 0.77 2/56 1011 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.015 s] Raw data (loadavg): 0.99 0.94 0.77 2/56 1013 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.017 s] Raw data (loadavg): 0.99 0.94 0.78 2/56 1013 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.017 s] Raw data (loadavg): 0.99 0.95 0.78 2/56 1013 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.018 s] Raw data (loadavg): 0.99 0.95 0.78 2/56 1013 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.019 s] Raw data (loadavg): 0.99 0.95 0.78 2/56 1013 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.019 s] Raw data (loadavg): 0.99 0.95 0.78 2/56 1013 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.02 s] Raw data (loadavg): 0.99 0.95 0.79 2/56 1015 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.02 s] Raw data (loadavg): 0.99 0.95 0.79 2/56 1015 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.022 s] Raw data (loadavg): 0.99 0.95 0.79 2/56 1015 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.022 s] Raw data (loadavg): 0.99 0.95 0.79 2/56 1015 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.022 s] Raw data (loadavg): 0.99 0.95 0.79 2/56 1015 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.023 s] Raw data (loadavg): 0.99 0.95 0.79 2/56 1015 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.022 s] Raw data (loadavg): 0.99 0.95 0.80 2/56 1017 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.024 s] Raw data (loadavg): 0.99 0.96 0.80 2/56 1017 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.024 s] Raw data (loadavg): 0.99 0.96 0.80 2/56 1017 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.024 s] Raw data (loadavg): 0.99 0.96 0.80 2/56 1017 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.026 s] Raw data (loadavg): 0.99 0.96 0.80 2/56 1017 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.026 s] Raw data (loadavg): 0.99 0.96 0.81 2/56 1017 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.027 s] Raw data (loadavg): 0.99 0.96 0.81 2/56 1019 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.027 s] Raw data (loadavg): 0.99 0.96 0.81 2/56 1019 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.028 s] Raw data (loadavg): 0.99 0.96 0.81 2/56 1019 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.029 s] Raw data (loadavg): 0.99 0.96 0.81 2/56 1019 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.029 s] Raw data (loadavg): 0.99 0.96 0.82 2/56 1019 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.03 s] Raw data (loadavg): 0.99 0.97 0.82 2/56 1019 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.03 s] Raw data (loadavg): 0.99 0.97 0.82 2/56 1021 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.03 s] Raw data (loadavg): 0.99 0.97 0.82 2/56 1021 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.03 s] Raw data (loadavg): 0.99 0.97 0.82 2/56 1021 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.03 s] Raw data (loadavg): 0.99 0.97 0.82 2/56 1021 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.031 s] Raw data (loadavg): 0.99 0.97 0.82 2/56 1021 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.031 s] Raw data (loadavg): 0.99 0.97 0.82 2/56 1021 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.031 s] Raw data (loadavg): 0.99 0.97 0.83 2/56 1023 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.032 s] Raw data (loadavg): 0.99 0.97 0.83 2/56 1023 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.033 s] Raw data (loadavg): 0.99 0.97 0.83 2/56 1023 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.033 s] Raw data (loadavg): 0.99 0.97 0.83 2/56 1023 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.033 s] Raw data (loadavg): 0.99 0.97 0.83 2/56 1023 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.034 s] Raw data (loadavg): 0.99 0.97 0.83 2/56 1023 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.034 s] Raw data (loadavg): 0.99 0.97 0.83 2/56 1025 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.034 s] Raw data (loadavg): 0.99 0.97 0.83 2/56 1025 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.033 s] Raw data (loadavg): 0.99 0.97 0.83 2/56 1025 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.033 s] Raw data (loadavg): 0.99 0.97 0.83 2/56 1025 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.034 s] Raw data (loadavg): 0.99 0.97 0.83 2/56 1025 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.034 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 1025 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.034 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 1027 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.034 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 1027 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.035 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 1027 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.035 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 1027 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.035 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 1027 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.035 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 1027 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.035 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 1029 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.035 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 1029 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.035 s] Raw data (loadavg): 0.99 0.97 0.84 2/56 1029 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.036 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 1029 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.036 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 1029 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.035 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 1029 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.035 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 1031 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.035 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 1031 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.036 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 1031 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.036 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 1031 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.036 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 1031 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.036 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 1031 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.036 s] Raw data (loadavg): 0.99 0.97 0.85 2/56 1033 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.037 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 1033 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.037 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 1033 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.037 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 1033 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.037 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 1033 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.038 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 1033 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.038 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 1035 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.038 s] Raw data (loadavg): 0.99 0.97 0.86 2/56 1035 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.038 s] Raw data (loadavg): 1.07 0.99 0.87 2/59 1072 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.037 s] Raw data (loadavg): 1.14 1.00 0.87 2/56 1088 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.038 s] Raw data (loadavg): 1.11 1.00 0.87 2/56 1088 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.039 s] Raw data (loadavg): 1.10 1.00 0.88 2/56 1088 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.039 s] Raw data (loadavg): 1.08 1.00 0.88 2/56 1090 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.039 s] Raw data (loadavg): 1.07 1.00 0.88 2/56 1090 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.04 s] Raw data (loadavg): 1.06 1.00 0.88 2/56 1090 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.041 s] Raw data (loadavg): 1.05 1.00 0.88 2/56 1092 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.042 s] Raw data (loadavg): 1.04 1.00 0.88 2/56 1092 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.04 s] Raw data (loadavg): 1.03 1.00 0.88 2/56 1092 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.04 s] Raw data (loadavg): 1.03 1.00 0.88 2/56 1094 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.04 s] Raw data (loadavg): 1.02 1.00 0.88 2/56 1094 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.04 s] Raw data (loadavg): 1.02 1.00 0.88 2/56 1094 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.04 s] Raw data (loadavg): 1.02 1.00 0.89 2/56 1094 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.01 1.00 0.89 2/56 1094 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.04 s] Raw data (loadavg): 1.01 1.00 0.89 2/56 1094 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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): 1.01 1.00 0.89 2/56 1096 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.01 1.00 0.89 2/56 1096 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.89 2/56 1096 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.89 2/56 1096 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.89 2/56 1096 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.89 2/56 1096 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.89 2/56 1098 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.90 2/56 1098 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.90 2/56 1098 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.90 2/56 1098 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.90 2/56 1098 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.90 2/56 1098 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.90 2/56 1100 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.90 2/56 1100 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.90 2/56 1100 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.05 s] Raw data (loadavg): 1.00 1.00 0.90 2/56 1100 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.72 s] Raw data (loadavg): 1.00 1.00 0.90 1/54 1100 Raw data (stat): 1001 (minisat+_script) S 1000 29618 29617 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853361900 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.72 CPU time (s): 1229.85 CPU user time (s): 1229.34 CPU system time (s): 0.504923 CPU usage (%): 100.011 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####