Name | normalized-opb/submitted/sorensson/garden/normalized-g15x15.opb |
MD5SUM | 6a083b86cc55025d2acb3bcf68562064 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 54 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 225 |
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 | 225 |
Number of bits of the sum of numbers in the objective function | 8 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 225 |
Number of bits of the biggest sum of numbers | 8 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.01784 |
Number of variables | 225 |
Total number of constraints | 225 |
Number of constraints which are clauses | 225 |
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 | 3 |
Maximum length of a constraint | 5 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc15 THE 2005-04-14 05:24:34 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4958 boxname=wulflinc15 idbench=382 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 6a083b86cc55025d2acb3bcf68562064 /oldhome/oroussel/tmp/wulflinc15/normalized-g15x15.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc15/normalized-g15x15.opb IDLAUNCH: 4958 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 890480 kB Buffers: 36792 kB Cached: 85640 kB SwapCached: 2144 kB Active: 66312 kB Inactive: 61072 kB HighTotal: 131008 kB HighFree: 41524 kB LowTotal: 903652 kB LowFree: 848956 kB SwapTotal: 2097136 kB SwapFree: 2094992 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6916 kB Slab: 11228 kB Committed_AS: 63476 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 05:44:37 (client local time) WITH STATUS 10 IN 1200.16 SECONDS stats: 4958 7 1200.16 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 225 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 | 225 1065 | 75 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 75[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6660 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 7880 18944 | 2626 0 0 nan | 0.000 % | c | 101 | 7833 18849 | 2888 96 1463 15.2 | 0.648 % | c | 251 | 7833 18849 | 3177 246 4130 16.8 | 0.648 % | c | 476 | 7833 18849 | 3495 471 7548 16.0 | 0.648 % | c | 813 | 7815 18811 | 3844 807 14594 18.1 | 0.839 % | c | 1319 | 7815 18811 | 4229 1313 22407 17.1 | 0.839 % | c | 2078 | 7815 18811 | 4652 2072 35096 16.9 | 0.839 % | c | 3218 | 7778 18732 | 5117 3196 64657 20.2 | 1.240 % | c ============================================================================== c [1mFound solution: 62[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3831 | 7874 18967 | 2624 3809 80986 21.3 | 1.240 % | c | 3932 | 7874 18967 | 2886 2006 47019 23.4 | 1.244 % | c | 4083 | 7858 18933 | 3175 2156 49776 23.1 | 1.414 % | c | 4311 | 7842 18899 | 3492 2383 52246 21.9 | 1.583 % | c | 4648 | 7829 18870 | 3841 2710 55952 20.6 | 1.734 % | c | 5154 | 7800 18807 | 4225 2997 63106 21.1 | 2.055 % | c | 5913 | 7800 18807 | 4648 3756 76082 20.3 | 2.055 % | c | 7052 | 7800 18807 | 5113 4895 95383 19.5 | 2.055 % | c | 8760 | 7777 18758 | 5624 6599 132092 20.0 | 2.300 % | c | 11322 | 7777 18758 | 6187 5862 151993 25.9 | 2.300 % | c | 15166 | 7770 18743 | 6805 6264 166593 26.6 | 2.375 % | c | 20934 | 7746 18691 | 7486 4979 73086 14.7 | 2.639 % | c | 29584 | 7746 18691 | 8235 5495 121003 22.0 | 2.639 % | c | 42562 | 7746 18691 | 9058 8643 253958 29.4 | 2.639 % | c | 62023 | 7729 18654 | 9964 7482 293519 39.2 | 2.828 % | c ============================================================================== c [1mFound solution: 60[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 82926 | 7732 18673 | 2577 5889 267788 45.5 | 2.828 % | c | 83026 | 7732 18673 | 2834 1573 37271 23.7 | 3.009 % | c | 83176 | 7732 18673 | 3118 1723 39197 22.7 | 3.009 % | c | 83401 | 7732 18673 | 3429 1948 43386 22.3 | 3.009 % | c | 83740 | 7732 18673 | 3772 2287 49778 21.8 | 3.009 % | c | 84246 | 7732 18673 | 4150 2793 58214 20.8 | 3.009 % | c | 85007 | 7730 18669 | 4565 3553 71012 20.0 | 3.028 % | c | 86147 | 7730 18669 | 5021 4693 101468 21.6 | 3.028 % | c | 87855 | 7730 18669 | 5524 3686 79696 21.6 | 3.028 % | c | 90417 | 7730 18669 | 6076 6248 143893 23.0 | 3.028 % | c | 94264 | 7730 18669 | 6684 6971 182901 26.2 | 3.028 % | c | 100033 | 7726 18661 | 7352 5471 139305 25.5 | 3.066 % | c | 108685 | 7726 18661 | 8087 6475 107535 16.6 | 3.066 % | c | 121659 | 7716 18639 | 8896 5512 193142 35.0 | 3.179 % | c | 141120 | 7716 18639 | 9786 9263 361472 39.0 | 3.178 % | c | 170312 | 7716 18639 | 10764 10279 353506 34.4 | 3.178 % | c | 214101 | 7716 18639 | 11841 11348 495137 43.6 | 3.178 % | c | 279785 | 7716 18639 | 13025 9072 248141 27.4 | 3.178 % | c | 378312 | 7716 18639 | 14327 7708 270624 35.1 | 3.178 % | c ============================================================================== c [1mFound solution: 58[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 518226 | 7738 18701 | 2579 14849 481198 32.4 | 3.178 % | c | 518326 | 7738 18701 | 2836 1957 43212 22.1 | 3.188 % | c | 518476 | 7738 18701 | 3120 2107 46360 22.0 | 3.188 % | c | 518703 | 7738 18701 | 3432 2334 50915 21.8 | 3.188 % | c | 519041 | 7738 18701 | 3775 2672 57879 21.7 | 3.188 % | c | 519549 | 7738 18701 | 4153 3180 67400 21.2 | 3.188 % | c | 520308 | 7738 18701 | 4568 3939 84338 21.4 | 3.188 % | c | 521447 | 7738 18701 | 5025 2631 43837 16.7 | 3.188 % | c | 523156 | 7713 18648 | 5528 2575 36654 14.2 | 3.451 % | c | 525720 | 7713 18648 | 6081 5139 109499 21.3 | 3.451 % | c | 529564 | 7713 18648 | 6689 8983 204736 22.8 | 3.451 % | c | 535331 | 7691 18600 | 7358 6698 147864 22.1 | 3.695 % | c | 543982 | 7691 18600 | 8094 6960 275619 39.6 | 3.695 % | c | 556956 | 7691 18600 | 8903 6646 246435 37.1 | 3.695 % | c | 576418 | 7691 18600 | 9793 10477 215457 20.6 | 3.695 % | c | 605612 | 7691 18600 | 10773 7116 272652 38.3 | 3.695 % | c | 649401 | 7678 18569 | 11850 10997 275428 25.0 | 3.863 % | c | 715085 | 7678 18569 | 13035 12319 413640 33.6 | 3.863 % | c | 813611 | 7678 18569 | 14339 7550 228042 30.2 | 3.863 % | c ============================================================================== c [1mFound solution: 56[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 851603 | 7695 18616 | 2565 12956 397284 30.7 | 3.863 % | c | 851703 | 7695 18616 | 2821 1720 31470 18.3 | 3.892 % | c | 851854 | 7695 18616 | 3103 1871 35434 18.9 | 3.892 % | c | 852081 | 7693 18612 | 3414 2097 38744 18.5 | 3.911 % | c | 852418 | 7693 18612 | 3755 2434 43532 17.9 | 3.911 % | c | 852924 | 7693 18612 | 4130 2940 56354 19.2 | 3.911 % | c | 853684 | 7693 18612 | 4544 3700 76355 20.6 | 3.911 % | c | 854827 | 7693 18612 | 4998 4843 102579 21.2 | 3.911 % | c | 856536 | 7693 18612 | 5498 3901 73991 19.0 | 3.911 % | c | 859099 | 7693 18612 | 6048 6464 145024 22.4 | 3.911 % | c | 862943 | 7690 18605 | 6652 3876 65509 16.9 | 3.948 % | c | 868714 | 7690 18605 | 7318 6158 115770 18.8 | 3.948 % | c | 877368 | 7690 18605 | 8050 7202 106459 14.8 | 3.948 % | c | 890342 | 7690 18605 | 8855 6654 235117 35.3 | 3.948 % | c | 909804 | 7680 18583 | 9740 7005 164322 23.5 | 4.061 % | c | 938996 | 7680 18583 | 10714 8504 305776 36.0 | 4.061 % | c | 982787 | 7680 18583 | 11786 11511 508585 44.2 | 4.061 % | c | 1048474 | 7680 18583 | 12964 11456 413707 36.1 | 4.061 % | c | 1147000 | 7678 18579 | 14261 12201 311601 25.5 | 4.079 % | c | 1294790 | 7661 18542 | 15687 15149 629931 41.6 | 4.266 % | c | 1516474 | 7658 18535 | 17256 16992 841342 49.5 | 4.304 % | #### 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.85 0.97 0.97 2/54 5373 Raw data (stat): 5373 (runsolver) R 5372 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423824990 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0001 s] Raw data (loadavg): 0.87 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 1065 0 0 0 995 3 0 0 25 0 1 0 423824990 6021120 1042 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1470 1042 603 41 0 1429 0 vsize: 5880 [startup+20.0008 s] Raw data (loadavg): 0.89 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 1278 0 0 0 1994 3 0 0 25 0 1 0 423824990 6959104 1255 4294967295 134512640 134672761 3221224640 3221223808 134564457 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1699 1255 603 41 0 1658 0 vsize: 6796 [startup+30.002 s] Raw data (loadavg): 0.91 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 1461 0 0 0 2994 4 0 0 25 0 1 0 423824990 7655424 1438 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1869 1438 603 41 0 1828 0 vsize: 7476 [startup+40.0028 s] Raw data (loadavg): 0.92 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 1805 0 0 0 3992 5 0 0 25 0 1 0 423824990 9142272 1782 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2232 1782 603 41 0 2191 0 vsize: 8928 [startup+50.0033 s] Raw data (loadavg): 0.93 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 1805 0 0 0 4991 5 0 0 25 0 1 0 423824990 9142272 1782 4294967295 134512640 134672761 3221224640 3221223808 134561025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2232 1782 603 41 0 2191 0 vsize: 8928 [startup+60.0034 s] Raw data (loadavg): 0.94 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 1805 0 0 0 5992 5 0 0 25 0 1 0 423824990 9142272 1782 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2232 1782 603 41 0 2191 0 vsize: 8928 [startup+70.0039 s] Raw data (loadavg): 0.95 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 1805 0 0 0 6992 5 0 0 25 0 1 0 423824990 9142272 1782 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2232 1782 603 41 0 2191 0 vsize: 8928 [startup+80.0048 s] Raw data (loadavg): 0.96 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 1805 0 0 0 7992 5 0 0 25 0 1 0 423824990 9142272 1782 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2232 1782 603 41 0 2191 0 vsize: 8928 [startup+90.0056 s] Raw data (loadavg): 0.96 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 1857 0 0 0 8992 6 0 0 25 0 1 0 423824990 9277440 1834 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2265 1834 603 41 0 2224 0 vsize: 9060 [startup+100.006 s] Raw data (loadavg): 0.97 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2102 0 0 0 9992 6 0 0 25 0 1 0 423824990 10358784 2079 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2529 2079 603 41 0 2488 0 vsize: 10116 [startup+110.006 s] Raw data (loadavg): 0.97 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2110 0 0 0 10992 6 0 0 25 0 1 0 423824990 10358784 2087 4294967295 134512640 134672761 3221224640 3221223792 134561040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2529 2087 603 41 0 2488 0 vsize: 10116 [startup+120.007 s] Raw data (loadavg): 0.98 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2110 0 0 0 11992 6 0 0 25 0 1 0 423824990 10358784 2087 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2529 2087 603 41 0 2488 0 vsize: 10116 [startup+130.007 s] Raw data (loadavg): 0.98 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2121 0 0 0 12992 7 0 0 25 0 1 0 423824990 10493952 2098 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2562 2098 603 41 0 2521 0 vsize: 10248 [startup+140.008 s] Raw data (loadavg): 0.98 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2131 0 0 0 13992 7 0 0 25 0 1 0 423824990 10493952 2108 4294967295 134512640 134672761 3221224640 3221223808 134561400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2562 2108 603 41 0 2521 0 vsize: 10248 [startup+150.009 s] Raw data (loadavg): 0.98 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2162 0 0 0 14992 7 0 0 25 0 1 0 423824990 10633216 2139 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2596 2139 603 41 0 2555 0 vsize: 10384 [startup+160.008 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2172 0 0 0 15992 7 0 0 25 0 1 0 423824990 10633216 2149 4294967295 134512640 134672761 3221224640 3221223824 134559663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2596 2149 603 41 0 2555 0 vsize: 10384 [startup+170.009 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2178 0 0 0 16992 7 0 0 25 0 1 0 423824990 10772480 2155 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2630 2155 603 41 0 2589 0 vsize: 10520 [startup+180.009 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2239 0 0 0 17992 7 0 0 25 0 1 0 423824990 11046912 2216 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2697 2216 603 41 0 2656 0 vsize: 10788 [startup+190.01 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2331 0 0 0 18992 7 0 0 25 0 1 0 423824990 11317248 2308 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2763 2308 603 41 0 2722 0 vsize: 11052 [startup+200.011 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2349 0 0 0 19992 7 0 0 25 0 1 0 423824990 11464704 2326 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2799 2326 603 41 0 2758 0 vsize: 11196 [startup+210.01 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2352 0 0 0 20993 7 0 0 25 0 1 0 423824990 11464704 2329 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2799 2329 603 41 0 2758 0 vsize: 11196 [startup+220.011 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2359 0 0 0 21993 7 0 0 25 0 1 0 423824990 11464704 2336 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2799 2336 603 41 0 2758 0 vsize: 11196 [startup+230.012 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2370 0 0 0 22993 7 0 0 25 0 1 0 423824990 11628544 2347 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2839 2347 603 41 0 2798 0 vsize: 11356 [startup+240.013 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2399 0 0 0 23993 8 0 0 25 0 1 0 423824990 11628544 2376 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2839 2376 603 41 0 2798 0 vsize: 11356 [startup+250.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2399 0 0 0 24993 8 0 0 25 0 1 0 423824990 11628544 2376 4294967295 134512640 134672761 3221224640 3221223808 134560842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2839 2376 603 41 0 2798 0 vsize: 11356 [startup+260.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2470 0 0 0 25993 8 0 0 25 0 1 0 423824990 12103680 2447 4294967295 134512640 134672761 3221224640 3221223808 134561139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2955 2447 603 41 0 2914 0 vsize: 11820 [startup+270.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2505 0 0 0 26993 8 0 0 25 0 1 0 423824990 12242944 2482 4294967295 134512640 134672761 3221224640 3221223808 134561003 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2989 2482 603 41 0 2948 0 vsize: 11956 [startup+280.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2511 0 0 0 27994 8 0 0 25 0 1 0 423824990 12242944 2488 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2989 2488 603 41 0 2948 0 vsize: 11956 [startup+290.015 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2544 0 0 0 28994 8 0 0 25 0 1 0 423824990 12402688 2521 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3028 2521 603 41 0 2987 0 vsize: 12112 [startup+300.016 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2552 0 0 0 29994 8 0 0 25 0 1 0 423824990 12402688 2529 4294967295 134512640 134672761 3221224640 3221223776 134560619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3028 2529 603 41 0 2987 0 vsize: 12112 [startup+310.016 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2562 0 0 0 30994 8 0 0 25 0 1 0 423824990 12546048 2539 4294967295 134512640 134672761 3221224640 3221223808 134560994 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3063 2539 603 41 0 3022 0 vsize: 12252 [startup+320.017 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2575 0 0 0 31994 8 0 0 25 0 1 0 423824990 12546048 2552 4294967295 134512640 134672761 3221224640 3221223776 134560577 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3063 2552 603 41 0 3022 0 vsize: 12252 [startup+330.017 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2603 0 0 0 32994 8 0 0 25 0 1 0 423824990 12681216 2580 4294967295 134512640 134672761 3221224640 3221223776 134565110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3096 2580 603 41 0 3055 0 vsize: 12384 [startup+340.018 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2632 0 0 0 33994 8 0 0 25 0 1 0 423824990 12816384 2609 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3129 2609 603 41 0 3088 0 vsize: 12516 [startup+350.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2639 0 0 0 34993 9 0 0 25 0 1 0 423824990 12816384 2616 4294967295 134512640 134672761 3221224640 3221223808 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3129 2616 603 41 0 3088 0 vsize: 12516 [startup+360.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2639 0 0 0 35993 9 0 0 25 0 1 0 423824990 12816384 2616 4294967295 134512640 134672761 3221224640 3221223744 134560361 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3129 2616 603 41 0 3088 0 vsize: 12516 [startup+370.02 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2639 0 0 0 36993 9 0 0 25 0 1 0 423824990 12816384 2616 4294967295 134512640 134672761 3221224640 3221223824 134559280 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3129 2616 603 41 0 3088 0 vsize: 12516 [startup+380.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2647 0 0 0 37993 9 0 0 25 0 1 0 423824990 12816384 2624 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3129 2624 603 41 0 3088 0 vsize: 12516 [startup+390.02 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2681 0 0 0 38993 9 0 0 25 0 1 0 423824990 12951552 2658 4294967295 134512640 134672761 3221224640 3221223800 134559749 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3162 2658 603 41 0 3121 0 vsize: 12648 [startup+400.021 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2690 0 0 0 39994 9 0 0 25 0 1 0 423824990 13090816 2667 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3196 2667 603 41 0 3155 0 vsize: 12784 [startup+410.021 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2717 0 0 0 40994 9 0 0 25 0 1 0 423824990 13225984 2694 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3229 2694 603 41 0 3188 0 vsize: 12916 [startup+420.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2741 0 0 0 41994 9 0 0 25 0 1 0 423824990 13225984 2718 4294967295 134512640 134672761 3221224640 3221223824 134559356 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3229 2718 603 41 0 3188 0 vsize: 12916 [startup+430.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2863 0 0 0 42994 9 0 0 25 0 1 0 423824990 13778944 2840 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3364 2840 603 41 0 3323 0 vsize: 13456 [startup+440.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2885 0 0 0 43994 10 0 0 25 0 1 0 423824990 13926400 2862 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3400 2862 603 41 0 3359 0 vsize: 13600 [startup+450.023 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2887 0 0 0 44994 10 0 0 25 0 1 0 423824990 13926400 2864 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3400 2864 603 41 0 3359 0 vsize: 13600 [startup+460.023 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2892 0 0 0 45994 10 0 0 25 0 1 0 423824990 13926400 2869 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3400 2869 603 41 0 3359 0 vsize: 13600 [startup+470.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 2907 0 0 0 46995 10 0 0 25 0 1 0 423824990 14061568 2884 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3433 2884 603 41 0 3392 0 vsize: 13732 [startup+480.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3010 0 0 0 47994 10 0 0 25 0 1 0 423824990 14467072 2987 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3532 2987 603 41 0 3491 0 vsize: 14128 [startup+490.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3045 0 0 0 48994 10 0 0 25 0 1 0 423824990 14602240 3022 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3565 3022 603 41 0 3524 0 vsize: 14260 [startup+500.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3112 0 0 0 49995 10 0 0 25 0 1 0 423824990 14880768 3089 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3633 3089 603 41 0 3592 0 vsize: 14532 [startup+510.026 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3115 0 0 0 50995 10 0 0 25 0 1 0 423824990 14880768 3092 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3633 3092 603 41 0 3592 0 vsize: 14532 [startup+520.026 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3115 0 0 0 51995 10 0 0 25 0 1 0 423824990 14880768 3092 4294967295 134512640 134672761 3221224640 3221223776 134565110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3633 3092 603 41 0 3592 0 vsize: 14532 [startup+530.026 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3115 0 0 0 52995 10 0 0 25 0 1 0 423824990 14880768 3092 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3633 3092 603 41 0 3592 0 vsize: 14532 [startup+540.027 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3125 0 0 0 53995 10 0 0 25 0 1 0 423824990 15015936 3102 4294967295 134512640 134672761 3221224640 3221223808 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3666 3102 603 41 0 3625 0 vsize: 14664 [startup+550.028 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3128 0 0 0 54996 10 0 0 25 0 1 0 423824990 15015936 3105 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3666 3105 603 41 0 3625 0 vsize: 14664 [startup+560.027 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3128 0 0 0 55996 10 0 0 25 0 1 0 423824990 15015936 3105 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3666 3105 603 41 0 3625 0 vsize: 14664 [startup+570.028 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3140 0 0 0 56996 10 0 0 25 0 1 0 423824990 15015936 3117 4294967295 134512640 134672761 3221224640 3221223824 134558883 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3666 3117 603 41 0 3625 0 vsize: 14664 [startup+580.028 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3168 0 0 0 57996 10 0 0 25 0 1 0 423824990 15147008 3145 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3698 3145 603 41 0 3657 0 vsize: 14792 [startup+590.028 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3168 0 0 0 58995 11 0 0 25 0 1 0 423824990 15147008 3145 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3698 3145 603 41 0 3657 0 vsize: 14792 [startup+600.029 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3168 0 0 0 59994 11 0 0 25 0 1 0 423824990 15147008 3145 4294967295 134512640 134672761 3221224640 3221223824 134559390 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3698 3145 603 41 0 3657 0 vsize: 14792 [startup+610.03 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3168 0 0 0 60994 11 0 0 25 0 1 0 423824990 15147008 3145 4294967295 134512640 134672761 3221224640 3221223776 134565054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3698 3145 603 41 0 3657 0 vsize: 14792 [startup+620.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3168 0 0 0 61994 11 0 0 25 0 1 0 423824990 15147008 3145 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3698 3145 603 41 0 3657 0 vsize: 14792 [startup+630.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3331 0 0 0 62993 12 0 0 25 0 1 0 423824990 15835136 3308 4294967295 134512640 134672761 3221224640 3221223808 134560909 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3866 3308 603 41 0 3825 0 vsize: 15464 [startup+640.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3352 0 0 0 63993 12 0 0 25 0 1 0 423824990 15986688 3329 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3903 3329 603 41 0 3862 0 vsize: 15612 [startup+650.032 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3371 0 0 0 64992 13 0 0 25 0 1 0 423824990 15986688 3348 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3903 3348 603 41 0 3862 0 vsize: 15612 [startup+660.032 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3371 0 0 0 65991 13 0 0 25 0 1 0 423824990 15986688 3348 4294967295 134512640 134672761 3221224640 3221223808 134561016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3903 3348 603 41 0 3862 0 vsize: 15612 [startup+670.032 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3372 0 0 0 66991 13 0 0 25 0 1 0 423824990 15986688 3349 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3903 3349 603 41 0 3862 0 vsize: 15612 [startup+680.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3426 0 0 0 67991 13 0 0 25 0 1 0 423824990 16248832 3403 4294967295 134512640 134672761 3221224640 3221223776 134560683 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3967 3403 603 41 0 3926 0 vsize: 15868 [startup+690.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3469 0 0 0 68992 13 0 0 25 0 1 0 423824990 16384000 3446 4294967295 134512640 134672761 3221224640 3221223792 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4000 3446 603 41 0 3959 0 vsize: 16000 [startup+700.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3469 0 0 0 69992 13 0 0 25 0 1 0 423824990 16384000 3446 4294967295 134512640 134672761 3221224640 3221223808 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4000 3446 603 41 0 3959 0 vsize: 16000 [startup+710.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3469 0 0 0 70992 13 0 0 25 0 1 0 423824990 16384000 3446 4294967295 134512640 134672761 3221224640 3221223808 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4000 3446 603 41 0 3959 0 vsize: 16000 [startup+720.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3493 0 0 0 71992 14 0 0 25 0 1 0 423824990 16523264 3470 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4034 3470 603 41 0 3993 0 vsize: 16136 [startup+730.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3493 0 0 0 72992 14 0 0 25 0 1 0 423824990 16523264 3470 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4034 3470 603 41 0 3993 0 vsize: 16136 [startup+740.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3493 0 0 0 73992 14 0 0 25 0 1 0 423824990 16523264 3470 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4034 3470 603 41 0 3993 0 vsize: 16136 [startup+750.034 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3493 0 0 0 74992 14 0 0 25 0 1 0 423824990 16523264 3470 4294967295 134512640 134672761 3221224640 3221223776 134560606 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4034 3470 603 41 0 3993 0 vsize: 16136 [startup+760.034 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3493 0 0 0 75992 14 0 0 25 0 1 0 423824990 16523264 3470 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4034 3470 603 41 0 3993 0 vsize: 16136 [startup+770.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3702 0 0 0 76992 14 0 0 25 0 1 0 423824990 17469440 3679 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4265 3679 603 41 0 4224 0 vsize: 17060 [startup+780.034 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3884 0 0 0 77992 15 0 0 25 0 1 0 423824990 18305024 3861 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3861 603 41 0 4428 0 vsize: 17876 [startup+790.034 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3884 0 0 0 78992 15 0 0 25 0 1 0 423824990 18305024 3861 4294967295 134512640 134672761 3221224640 3221223744 134560381 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3861 603 41 0 4428 0 vsize: 17876 [startup+800.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3884 0 0 0 79992 15 0 0 25 0 1 0 423824990 18305024 3861 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3861 603 41 0 4428 0 vsize: 17876 [startup+810.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3884 0 0 0 80992 15 0 0 25 0 1 0 423824990 18305024 3861 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3861 603 41 0 4428 0 vsize: 17876 [startup+820.036 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3884 0 0 0 81992 15 0 0 25 0 1 0 423824990 18305024 3861 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3861 603 41 0 4428 0 vsize: 17876 [startup+830.036 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3884 0 0 0 82993 15 0 0 25 0 1 0 423824990 18305024 3861 4294967295 134512640 134672761 3221224640 3221223808 134560808 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3861 603 41 0 4428 0 vsize: 17876 [startup+840.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3884 0 0 0 83993 15 0 0 25 0 1 0 423824990 18305024 3861 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3861 603 41 0 4428 0 vsize: 17876 [startup+850.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3885 0 0 0 84993 15 0 0 25 0 1 0 423824990 18305024 3862 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3862 603 41 0 4428 0 vsize: 17876 [startup+860.036 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3885 0 0 0 85993 15 0 0 25 0 1 0 423824990 18305024 3862 4294967295 134512640 134672761 3221224640 3221223744 134554673 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3862 603 41 0 4428 0 vsize: 17876 [startup+870.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3885 0 0 0 86993 15 0 0 25 0 1 0 423824990 18305024 3862 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3862 603 41 0 4428 0 vsize: 17876 [startup+880.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3885 0 0 0 87994 15 0 0 25 0 1 0 423824990 18305024 3862 4294967295 134512640 134672761 3221224640 3221223744 134560510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3862 603 41 0 4428 0 vsize: 17876 [startup+890.036 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3885 0 0 0 88993 15 0 0 25 0 1 0 423824990 18305024 3862 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3862 603 41 0 4428 0 vsize: 17876 [startup+900.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3885 0 0 0 89993 15 0 0 25 0 1 0 423824990 18305024 3862 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3862 603 41 0 4428 0 vsize: 17876 [startup+910.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 3886 0 0 0 90994 15 0 0 25 0 1 0 423824990 18305024 3863 4294967295 134512640 134672761 3221224640 3221223744 134560191 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4469 3863 603 41 0 4428 0 vsize: 17876 [startup+920.038 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4050 0 0 0 91993 15 0 0 25 0 1 0 423824990 18862080 4027 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4605 4027 603 41 0 4564 0 vsize: 18420 [startup+930.038 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4094 0 0 0 92993 16 0 0 25 0 1 0 423824990 19197952 4071 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4687 4071 603 41 0 4646 0 vsize: 18748 [startup+940.039 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4105 0 0 0 93993 16 0 0 25 0 1 0 423824990 19197952 4082 4294967295 134512640 134672761 3221224640 3221223808 134560979 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4687 4082 603 41 0 4646 0 vsize: 18748 [startup+950.039 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4126 0 0 0 94994 16 0 0 25 0 1 0 423824990 19394560 4103 4294967295 134512640 134672761 3221224640 3221223744 134559998 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4103 603 41 0 4694 0 vsize: 18940 [startup+960.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4127 0 0 0 95994 16 0 0 25 0 1 0 423824990 19394560 4104 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4104 603 41 0 4694 0 vsize: 18940 [startup+970.041 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4128 0 0 0 96994 16 0 0 25 0 1 0 423824990 19394560 4105 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4105 603 41 0 4694 0 vsize: 18940 [startup+980.042 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4128 0 0 0 97994 16 0 0 25 0 1 0 423824990 19394560 4105 4294967295 134512640 134672761 3221224640 3221223744 134560510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4105 603 41 0 4694 0 vsize: 18940 [startup+990.041 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4140 0 0 0 98994 16 0 0 25 0 1 0 423824990 19394560 4117 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4117 603 41 0 4694 0 vsize: 18940 [startup+1000.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4140 0 0 0 99995 16 0 0 25 0 1 0 423824990 19394560 4117 4294967295 134512640 134672761 3221224640 3221223824 134559498 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4117 603 41 0 4694 0 vsize: 18940 [startup+1010.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4140 0 0 0 100995 16 0 0 25 0 1 0 423824990 19394560 4117 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4117 603 41 0 4694 0 vsize: 18940 [startup+1020.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4140 0 0 0 101995 16 0 0 25 0 1 0 423824990 19394560 4117 4294967295 134512640 134672761 3221224640 3221223824 134559272 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4117 603 41 0 4694 0 vsize: 18940 [startup+1030.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4140 0 0 0 102996 16 0 0 25 0 1 0 423824990 19394560 4117 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4117 603 41 0 4694 0 vsize: 18940 [startup+1040.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4140 0 0 0 103996 16 0 0 25 0 1 0 423824990 19394560 4117 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4117 603 41 0 4694 0 vsize: 18940 [startup+1050.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4140 0 0 0 104996 16 0 0 25 0 1 0 423824990 19394560 4117 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4117 603 41 0 4694 0 vsize: 18940 [startup+1060.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4140 0 0 0 105996 16 0 0 25 0 1 0 423824990 19394560 4117 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4117 603 41 0 4694 0 vsize: 18940 [startup+1070.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4140 0 0 0 106997 16 0 0 25 0 1 0 423824990 19394560 4117 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4117 603 41 0 4694 0 vsize: 18940 [startup+1080.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4152 0 0 0 107997 16 0 0 25 0 1 0 423824990 19394560 4129 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4735 4129 603 41 0 4694 0 vsize: 18940 [startup+1090.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4287 0 0 0 108996 16 0 0 25 0 1 0 423824990 19959808 4264 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4873 4264 603 41 0 4832 0 vsize: 19492 [startup+1100.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4297 0 0 0 109996 17 0 0 25 0 1 0 423824990 20107264 4274 4294967295 134512640 134672761 3221224640 3221223824 134558435 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4909 4274 603 41 0 4868 0 vsize: 19636 [startup+1110.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4297 0 0 0 110996 17 0 0 25 0 1 0 423824990 20107264 4274 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4909 4274 603 41 0 4868 0 vsize: 19636 [startup+1120.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4304 0 0 0 111996 17 0 0 25 0 1 0 423824990 20107264 4281 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4909 4281 603 41 0 4868 0 vsize: 19636 [startup+1130.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4304 0 0 0 112996 17 0 0 25 0 1 0 423824990 20107264 4281 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4909 4281 603 41 0 4868 0 vsize: 19636 [startup+1140.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4304 0 0 0 113997 17 0 0 25 0 1 0 423824990 20107264 4281 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4909 4281 603 41 0 4868 0 vsize: 19636 [startup+1150.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4304 0 0 0 114997 17 0 0 25 0 1 0 423824990 20107264 4281 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4909 4281 603 41 0 4868 0 vsize: 19636 [startup+1160.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4312 0 0 0 115997 17 0 0 25 0 1 0 423824990 20107264 4289 4294967295 134512640 134672761 3221224640 3221223808 134561220 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4909 4289 603 41 0 4868 0 vsize: 19636 [startup+1170.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4316 0 0 0 116997 17 0 0 25 0 1 0 423824990 20107264 4293 4294967295 134512640 134672761 3221224640 3221223824 134559379 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4909 4293 603 41 0 4868 0 vsize: 19636 [startup+1180.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4330 0 0 0 117997 17 0 0 25 0 1 0 423824990 20254720 4307 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4945 4307 603 41 0 4904 0 vsize: 19780 [startup+1190.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4330 0 0 0 118997 17 0 0 25 0 1 0 423824990 20254720 4307 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4945 4307 603 41 0 4904 0 vsize: 19780 [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 5373 Raw data (stat): 5373 (minisat+) R 5372 29151 29150 0 -1 0 4334 0 0 0 119998 17 0 0 25 0 1 0 423824990 20254720 4311 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4945 4311 603 41 0 4904 0 vsize: 19780 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.06 s] Raw data (loadavg): 0.99 0.97 0.97 1/54 5373 Raw data (stat): 5373 (minisat+) Z 5372 29151 29150 0 -1 12 4337 0 0 0 119998 17 0 0 25 0 1 0 423824990 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.06 CPU time (s): 1200.16 CPU user time (s): 1199.98 CPU system time (s): 0.179972 CPU usage (%): 100.008 Max. virtual memory (Kb): 19780 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####