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 wulflinc25 THE 2005-04-14 05:29:23 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4965 boxname=wulflinc25 idbench=382 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6a083b86cc55025d2acb3bcf68562064 /oldhome/oroussel/tmp/wulflinc25/normalized-g15x15.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc25/normalized-g15x15.opb /oldhome/oroussel/tmp/wulflinc25/normalized-g15x15.opb IDLAUNCH: 4965 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 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.220 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: 859056 kB Buffers: 35216 kB Cached: 105848 kB SwapCached: 36 kB Active: 51268 kB Inactive: 92668 kB HighTotal: 131008 kB HighFree: 21476 kB LowTotal: 903652 kB LowFree: 837580 kB SwapTotal: 2097892 kB SwapFree: 2097856 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6920 kB Slab: 26036 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 05:49:25 (client local time) WITH STATUS 10 IN 1200.19 SECONDS stats: 4965 7 1200.19 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.92 0.98 0.92 2/54 3676 Raw data (stat): 3676 (runsolver) R 3675 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482087821 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.93 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 1054 0 0 0 995 3 0 0 25 0 1 0 482087821 6074368 1031 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1483 1031 603 41 0 1442 0 vsize: 5932 [startup+20.0004 s] Raw data (loadavg): 0.94 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 1267 0 0 0 1994 4 0 0 25 0 1 0 482087821 6881280 1244 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1680 1244 603 41 0 1639 0 vsize: 6720 [startup+30.0013 s] Raw data (loadavg): 0.95 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 1451 0 0 0 2993 4 0 0 25 0 1 0 482087821 7696384 1428 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1879 1428 603 41 0 1838 0 vsize: 7516 [startup+40.0044 s] Raw data (loadavg): 0.96 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 1794 0 0 0 3992 5 0 0 25 0 1 0 482087821 9039872 1771 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2207 1771 603 41 0 2166 0 vsize: 8828 [startup+50.0052 s] Raw data (loadavg): 0.96 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 1794 0 0 0 4993 5 0 0 25 0 1 0 482087821 9039872 1771 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2207 1771 603 41 0 2166 0 vsize: 8828 [startup+60.0045 s] Raw data (loadavg): 0.97 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 1794 0 0 0 5993 5 0 0 25 0 1 0 482087821 9039872 1771 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2207 1771 603 41 0 2166 0 vsize: 8828 [startup+70.0054 s] Raw data (loadavg): 0.97 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 1794 0 0 0 6993 5 0 0 25 0 1 0 482087821 9039872 1771 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2207 1771 603 41 0 2166 0 vsize: 8828 [startup+80.0057 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 1794 0 0 0 7993 5 0 0 25 0 1 0 482087821 9039872 1771 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2207 1771 603 41 0 2166 0 vsize: 8828 [startup+90.0055 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 1845 0 0 0 8993 5 0 0 25 0 1 0 482087821 9314304 1822 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2274 1822 603 41 0 2233 0 vsize: 9096 [startup+100.008 s] Raw data (loadavg): 0.98 0.98 0.92 3/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2091 0 0 0 9993 6 0 0 25 0 1 0 482087821 10264576 2068 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2506 2068 603 41 0 2465 0 vsize: 10024 [startup+110.008 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2099 0 0 0 10993 6 0 0 25 0 1 0 482087821 10420224 2076 4294967295 134512640 134672761 3221224560 3221223744 134559590 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2544 2076 603 41 0 2503 0 vsize: 10176 [startup+120.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2099 0 0 0 11994 6 0 0 25 0 1 0 482087821 10420224 2076 4294967295 134512640 134672761 3221224560 3221223712 134565073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2544 2076 603 41 0 2503 0 vsize: 10176 [startup+130.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2109 0 0 0 12994 6 0 0 25 0 1 0 482087821 10420224 2086 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2544 2086 603 41 0 2503 0 vsize: 10176 [startup+140.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2119 0 0 0 13994 6 0 0 25 0 1 0 482087821 10420224 2096 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2544 2096 603 41 0 2503 0 vsize: 10176 [startup+150.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2149 0 0 0 14994 7 0 0 25 0 1 0 482087821 10567680 2126 4294967295 134512640 134672761 3221224560 3221223696 134560560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2580 2126 603 41 0 2539 0 vsize: 10320 [startup+160.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2161 0 0 0 15994 7 0 0 25 0 1 0 482087821 10715136 2138 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2616 2138 603 41 0 2575 0 vsize: 10464 [startup+170.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2167 0 0 0 16994 7 0 0 25 0 1 0 482087821 10715136 2144 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2616 2144 603 41 0 2575 0 vsize: 10464 [startup+180.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2227 0 0 0 17993 7 0 0 25 0 1 0 482087821 11005952 2204 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2687 2204 603 41 0 2646 0 vsize: 10748 [startup+190.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2320 0 0 0 18993 7 0 0 25 0 1 0 482087821 11276288 2297 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2753 2297 603 41 0 2712 0 vsize: 11012 [startup+200.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2337 0 0 0 19994 7 0 0 25 0 1 0 482087821 11436032 2314 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2792 2314 603 41 0 2751 0 vsize: 11168 [startup+210.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2340 0 0 0 20994 7 0 0 25 0 1 0 482087821 11436032 2317 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2792 2317 603 41 0 2751 0 vsize: 11168 [startup+220.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2346 0 0 0 21994 7 0 0 25 0 1 0 482087821 11436032 2323 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2792 2323 603 41 0 2751 0 vsize: 11168 [startup+230.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2359 0 0 0 22994 7 0 0 25 0 1 0 482087821 11599872 2336 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2832 2336 603 41 0 2791 0 vsize: 11328 [startup+240.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2387 0 0 0 23994 7 0 0 25 0 1 0 482087821 11599872 2364 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2832 2364 603 41 0 2791 0 vsize: 11328 [startup+250.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2397 0 0 0 24994 8 0 0 25 0 1 0 482087821 11739136 2374 4294967295 134512640 134672761 3221224560 3221223664 134555130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2866 2374 603 41 0 2825 0 vsize: 11464 [startup+260.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2460 0 0 0 25994 8 0 0 25 0 1 0 482087821 12066816 2437 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2946 2437 603 41 0 2905 0 vsize: 11784 [startup+270.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2498 0 0 0 26994 8 0 0 25 0 1 0 482087821 12201984 2475 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2979 2475 603 41 0 2938 0 vsize: 11916 [startup+280.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2505 0 0 0 27994 8 0 0 25 0 1 0 482087821 12201984 2482 4294967295 134512640 134672761 3221224560 3221223744 134559572 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2979 2482 603 41 0 2938 0 vsize: 11916 [startup+290.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2536 0 0 0 28994 8 0 0 25 0 1 0 482087821 12337152 2513 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3012 2513 603 41 0 2971 0 vsize: 12048 [startup+300.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2549 0 0 0 29995 8 0 0 25 0 1 0 482087821 12484608 2526 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3048 2526 603 41 0 3007 0 vsize: 12192 [startup+310.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2554 0 0 0 30995 8 0 0 25 0 1 0 482087821 12484608 2531 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3048 2531 603 41 0 3007 0 vsize: 12192 [startup+320.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2568 0 0 0 31995 8 0 0 25 0 1 0 482087821 12484608 2545 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3048 2545 603 41 0 3007 0 vsize: 12192 [startup+330.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2594 0 0 0 32995 8 0 0 25 0 1 0 482087821 12619776 2571 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3081 2571 603 41 0 3040 0 vsize: 12324 [startup+340.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2621 0 0 0 33995 8 0 0 25 0 1 0 482087821 12767232 2598 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3117 2598 603 41 0 3076 0 vsize: 12468 [startup+350.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2627 0 0 0 34995 8 0 0 25 0 1 0 482087821 12767232 2604 4294967295 134512640 134672761 3221224560 3221223664 134560301 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3117 2604 603 41 0 3076 0 vsize: 12468 [startup+360.009 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2627 0 0 0 35994 8 0 0 25 0 1 0 482087821 12767232 2604 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3117 2604 603 41 0 3076 0 vsize: 12468 [startup+370.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2627 0 0 0 36994 8 0 0 25 0 1 0 482087821 12767232 2604 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3117 2604 603 41 0 3076 0 vsize: 12468 [startup+380.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2627 0 0 0 37995 8 0 0 25 0 1 0 482087821 12767232 2604 4294967295 134512640 134672761 3221224560 3221223664 134560340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3117 2604 603 41 0 3076 0 vsize: 12468 [startup+390.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2672 0 0 0 38994 9 0 0 25 0 1 0 482087821 13049856 2649 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3186 2649 603 41 0 3145 0 vsize: 12744 [startup+400.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2681 0 0 0 39995 9 0 0 25 0 1 0 482087821 13049856 2658 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3186 2658 603 41 0 3145 0 vsize: 12744 [startup+410.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2702 0 0 0 40995 9 0 0 25 0 1 0 482087821 13189120 2679 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3220 2679 603 41 0 3179 0 vsize: 12880 [startup+420.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2731 0 0 0 41995 9 0 0 25 0 1 0 482087821 13328384 2708 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3254 2708 603 41 0 3213 0 vsize: 13016 [startup+430.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2845 0 0 0 42995 9 0 0 25 0 1 0 482087821 13746176 2822 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3356 2822 603 41 0 3315 0 vsize: 13424 [startup+440.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2865 0 0 0 43995 9 0 0 25 0 1 0 482087821 13893632 2842 4294967295 134512640 134672761 3221224560 3221223744 134558648 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3392 2842 603 41 0 3351 0 vsize: 13568 [startup+450.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2867 0 0 0 44995 9 0 0 25 0 1 0 482087821 13893632 2844 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3392 2844 603 41 0 3351 0 vsize: 13568 [startup+460.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2879 0 0 0 45995 9 0 0 25 0 1 0 482087821 13893632 2856 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3392 2856 603 41 0 3351 0 vsize: 13568 [startup+470.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2884 0 0 0 46995 9 0 0 25 0 1 0 482087821 14028800 2861 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3425 2861 603 41 0 3384 0 vsize: 13700 [startup+480.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 2987 0 0 0 47995 10 0 0 25 0 1 0 482087821 14434304 2964 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3524 2964 603 41 0 3483 0 vsize: 14096 [startup+490.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3029 0 0 0 48995 10 0 0 25 0 1 0 482087821 14569472 3006 4294967295 134512640 134672761 3221224560 3221223696 134560726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3557 3006 603 41 0 3516 0 vsize: 14228 [startup+500.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3087 0 0 0 49995 10 0 0 25 0 1 0 482087821 14860288 3064 4294967295 134512640 134672761 3221224560 3221223728 134560822 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3628 3064 603 41 0 3587 0 vsize: 14512 [startup+510.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3090 0 0 0 50996 10 0 0 25 0 1 0 482087821 14860288 3067 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3628 3067 603 41 0 3587 0 vsize: 14512 [startup+520.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3091 0 0 0 51996 10 0 0 25 0 1 0 482087821 14860288 3068 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3628 3068 603 41 0 3587 0 vsize: 14512 [startup+530.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3091 0 0 0 52996 10 0 0 25 0 1 0 482087821 14860288 3068 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3628 3068 603 41 0 3587 0 vsize: 14512 [startup+540.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3101 0 0 0 53996 10 0 0 25 0 1 0 482087821 14995456 3078 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3661 3078 603 41 0 3620 0 vsize: 14644 [startup+550.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3104 0 0 0 54996 10 0 0 25 0 1 0 482087821 14995456 3081 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3661 3081 603 41 0 3620 0 vsize: 14644 [startup+560.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3104 0 0 0 55996 10 0 0 25 0 1 0 482087821 14995456 3081 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3661 3081 603 41 0 3620 0 vsize: 14644 [startup+570.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3129 0 0 0 56997 10 0 0 25 0 1 0 482087821 14995456 3106 4294967295 134512640 134672761 3221224560 3221223744 134558938 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3661 3106 603 41 0 3620 0 vsize: 14644 [startup+580.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3139 0 0 0 57997 10 0 0 25 0 1 0 482087821 15130624 3116 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3694 3116 603 41 0 3653 0 vsize: 14776 [startup+590.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3139 0 0 0 58996 10 0 0 25 0 1 0 482087821 15130624 3116 4294967295 134512640 134672761 3221224560 3221223744 134558629 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3694 3116 603 41 0 3653 0 vsize: 14776 [startup+600.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3139 0 0 0 59997 10 0 0 25 0 1 0 482087821 15130624 3116 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3694 3116 603 41 0 3653 0 vsize: 14776 [startup+610.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3139 0 0 0 60997 10 0 0 25 0 1 0 482087821 15130624 3116 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3694 3116 603 41 0 3653 0 vsize: 14776 [startup+620.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3141 0 0 0 61997 10 0 0 25 0 1 0 482087821 15130624 3118 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3694 3118 603 41 0 3653 0 vsize: 14776 [startup+630.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3306 0 0 0 62996 11 0 0 25 0 1 0 482087821 15810560 3283 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3860 3283 603 41 0 3819 0 vsize: 15440 [startup+640.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3338 0 0 0 63996 11 0 0 25 0 1 0 482087821 15958016 3315 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3896 3315 603 41 0 3855 0 vsize: 15584 [startup+650.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3338 0 0 0 64996 11 0 0 25 0 1 0 482087821 15958016 3315 4294967295 134512640 134672761 3221224560 3221223744 134558371 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3896 3315 603 41 0 3855 0 vsize: 15584 [startup+660.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3339 0 0 0 65997 11 0 0 25 0 1 0 482087821 15958016 3316 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3896 3316 603 41 0 3855 0 vsize: 15584 [startup+670.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3339 0 0 0 66997 11 0 0 25 0 1 0 482087821 15958016 3316 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3896 3316 603 41 0 3855 0 vsize: 15584 [startup+680.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3428 0 0 0 67997 11 0 0 25 0 1 0 482087821 16359424 3405 4294967295 134512640 134672761 3221224560 3221223744 134559045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3994 3405 603 41 0 3953 0 vsize: 15976 [startup+690.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3444 0 0 0 68997 11 0 0 25 0 1 0 482087821 16359424 3421 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3994 3421 603 41 0 3953 0 vsize: 15976 [startup+700.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3444 0 0 0 69997 11 0 0 25 0 1 0 482087821 16359424 3421 4294967295 134512640 134672761 3221224560 3221223664 134560477 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3994 3421 603 41 0 3953 0 vsize: 15976 [startup+710.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3452 0 0 0 70997 11 0 0 25 0 1 0 482087821 16515072 3429 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4032 3429 603 41 0 3991 0 vsize: 16128 [startup+720.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3462 0 0 0 71998 11 0 0 25 0 1 0 482087821 16515072 3439 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4032 3439 603 41 0 3991 0 vsize: 16128 [startup+730.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3462 0 0 0 72998 11 0 0 25 0 1 0 482087821 16515072 3439 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4032 3439 603 41 0 3991 0 vsize: 16128 [startup+740.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3462 0 0 0 73998 11 0 0 25 0 1 0 482087821 16515072 3439 4294967295 134512640 134672761 3221224560 3221223744 134558374 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4032 3439 603 41 0 3991 0 vsize: 16128 [startup+750.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3462 0 0 0 74998 11 0 0 25 0 1 0 482087821 16515072 3439 4294967295 134512640 134672761 3221224560 3221223728 134560845 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4032 3439 603 41 0 3991 0 vsize: 16128 [startup+760.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3592 0 0 0 75998 12 0 0 25 0 1 0 482087821 17047552 3569 4294967295 134512640 134672761 3221224560 3221223696 134560652 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4162 3569 603 41 0 4121 0 vsize: 16648 [startup+770.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3851 0 0 0 76997 12 0 0 25 0 1 0 482087821 18132992 3828 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4427 3828 603 41 0 4386 0 vsize: 17708 [startup+780.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3860 0 0 0 77997 12 0 0 25 0 1 0 482087821 18288640 3837 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3837 603 41 0 4424 0 vsize: 17860 [startup+790.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3860 0 0 0 78998 12 0 0 25 0 1 0 482087821 18288640 3837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3837 603 41 0 4424 0 vsize: 17860 [startup+800.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3860 0 0 0 79998 12 0 0 25 0 1 0 482087821 18288640 3837 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3837 603 41 0 4424 0 vsize: 17860 [startup+810.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3860 0 0 0 80998 12 0 0 25 0 1 0 482087821 18288640 3837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3837 603 41 0 4424 0 vsize: 17860 [startup+820.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3860 0 0 0 81998 12 0 0 25 0 1 0 482087821 18288640 3837 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3837 603 41 0 4424 0 vsize: 17860 [startup+830.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3860 0 0 0 82998 12 0 0 25 0 1 0 482087821 18288640 3837 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3837 603 41 0 4424 0 vsize: 17860 [startup+840.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3860 0 0 0 83998 12 0 0 25 0 1 0 482087821 18288640 3837 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3837 603 41 0 4424 0 vsize: 17860 [startup+850.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3861 0 0 0 84999 12 0 0 25 0 1 0 482087821 18288640 3838 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3838 603 41 0 4424 0 vsize: 17860 [startup+860.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3861 0 0 0 85999 12 0 0 25 0 1 0 482087821 18288640 3838 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3838 603 41 0 4424 0 vsize: 17860 [startup+870.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3861 0 0 0 86999 12 0 0 25 0 1 0 482087821 18288640 3838 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3838 603 41 0 4424 0 vsize: 17860 [startup+880.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3861 0 0 0 87999 13 0 0 25 0 1 0 482087821 18288640 3838 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3838 603 41 0 4424 0 vsize: 17860 [startup+890.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3862 0 0 0 88999 13 0 0 25 0 1 0 482087821 18288640 3839 4294967295 134512640 134672761 3221224560 3221223744 134558925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3839 603 41 0 4424 0 vsize: 17860 [startup+900.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3863 0 0 0 89999 13 0 0 25 0 1 0 482087821 18288640 3840 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3840 603 41 0 4424 0 vsize: 17860 [startup+910.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 3885 0 0 0 91000 13 0 0 25 0 1 0 482087821 18288640 3862 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4465 3862 603 41 0 4424 0 vsize: 17860 [startup+920.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4037 0 0 0 91999 13 0 0 25 0 1 0 482087821 18968576 4014 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4631 4014 603 41 0 4590 0 vsize: 18524 [startup+930.004 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4080 0 0 0 92999 13 0 0 25 0 1 0 482087821 19238912 4057 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4697 4057 603 41 0 4656 0 vsize: 18788 [startup+940.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4094 0 0 0 93999 13 0 0 25 0 1 0 482087821 19238912 4071 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4697 4071 603 41 0 4656 0 vsize: 18788 [startup+950.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4105 0 0 0 94999 13 0 0 25 0 1 0 482087821 19238912 4082 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4697 4082 603 41 0 4656 0 vsize: 18788 [startup+960.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4105 0 0 0 96000 13 0 0 25 0 1 0 482087821 19238912 4082 4294967295 134512640 134672761 3221224560 3221223728 134560836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4697 4082 603 41 0 4656 0 vsize: 18788 [startup+970.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4106 0 0 0 97000 13 0 0 25 0 1 0 482087821 19238912 4083 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4697 4083 603 41 0 4656 0 vsize: 18788 [startup+980.003 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4106 0 0 0 98000 13 0 0 25 0 1 0 482087821 19238912 4083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4697 4083 603 41 0 4656 0 vsize: 18788 [startup+990.002 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4119 0 0 0 99000 13 0 0 25 0 1 0 482087821 19402752 4096 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4737 4096 603 41 0 4696 0 vsize: 18948 [startup+1000 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4119 0 0 0 100000 13 0 0 25 0 1 0 482087821 19402752 4096 4294967295 134512640 134672761 3221224560 3221223664 134554636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4737 4096 603 41 0 4696 0 vsize: 18948 [startup+1010 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4119 0 0 0 101000 13 0 0 25 0 1 0 482087821 19402752 4096 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4737 4096 603 41 0 4696 0 vsize: 18948 [startup+1020 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4119 0 0 0 102001 13 0 0 25 0 1 0 482087821 19402752 4096 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4737 4096 603 41 0 4696 0 vsize: 18948 [startup+1030 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4119 0 0 0 103001 13 0 0 25 0 1 0 482087821 19402752 4096 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4737 4096 603 41 0 4696 0 vsize: 18948 [startup+1040 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4119 0 0 0 104001 13 0 0 25 0 1 0 482087821 19402752 4096 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4737 4096 603 41 0 4696 0 vsize: 18948 [startup+1050 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4119 0 0 0 105001 13 0 0 25 0 1 0 482087821 19402752 4096 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4737 4096 603 41 0 4696 0 vsize: 18948 [startup+1060 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4119 0 0 0 106001 13 0 0 25 0 1 0 482087821 19402752 4096 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4737 4096 603 41 0 4696 0 vsize: 18948 [startup+1070 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4119 0 0 0 107002 13 0 0 25 0 1 0 482087821 19402752 4096 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4737 4096 603 41 0 4696 0 vsize: 18948 [startup+1080 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4223 0 0 0 108001 14 0 0 25 0 1 0 482087821 19804160 4200 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4835 4200 603 41 0 4794 0 vsize: 19340 [startup+1090 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4272 0 0 0 109001 14 0 0 25 0 1 0 482087821 20074496 4249 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4901 4249 603 41 0 4860 0 vsize: 19604 [startup+1100 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4272 0 0 0 110001 14 0 0 25 0 1 0 482087821 20074496 4249 4294967295 134512640 134672761 3221224560 3221223744 134559559 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4901 4249 603 41 0 4860 0 vsize: 19604 [startup+1110 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4277 0 0 0 111001 14 0 0 25 0 1 0 482087821 20074496 4254 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4901 4254 603 41 0 4860 0 vsize: 19604 [startup+1120 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4277 0 0 0 112001 14 0 0 25 0 1 0 482087821 20074496 4254 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4901 4254 603 41 0 4860 0 vsize: 19604 [startup+1130 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4277 0 0 0 113001 14 0 0 25 0 1 0 482087821 20074496 4254 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4901 4254 603 41 0 4860 0 vsize: 19604 [startup+1140 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4277 0 0 0 114001 14 0 0 25 0 1 0 482087821 20074496 4254 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4901 4254 603 41 0 4860 0 vsize: 19604 [startup+1150 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4277 0 0 0 115002 14 0 0 25 0 1 0 482087821 20074496 4254 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4901 4254 603 41 0 4860 0 vsize: 19604 [startup+1160 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4287 0 0 0 116002 14 0 0 25 0 1 0 482087821 20074496 4264 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4901 4264 603 41 0 4860 0 vsize: 19604 [startup+1170 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4298 0 0 0 117002 14 0 0 25 0 1 0 482087821 20074496 4275 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4901 4275 603 41 0 4860 0 vsize: 19604 [startup+1180 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4301 0 0 0 118002 14 0 0 25 0 1 0 482087821 20221952 4278 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4937 4278 603 41 0 4896 0 vsize: 19748 [startup+1190 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4301 0 0 0 119002 14 0 0 25 0 1 0 482087821 20221952 4278 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4937 4278 603 41 0 4896 0 vsize: 19748 [startup+1200 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 3676 Raw data (stat): 3676 (minisat+) R 3675 28099 28098 0 -1 0 4317 0 0 0 120003 14 0 0 25 0 1 0 482087821 20221952 4294 4294967295 134512640 134672761 3221224560 3221223664 134554636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4937 4294 603 41 0 4896 0 vsize: 19748 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.01 s] Raw data (loadavg): 0.99 0.98 0.92 1/54 3676 Raw data (stat): 3676 (minisat+) Z 3675 28099 28098 0 -1 12 4320 0 0 0 120003 15 0 0 25 0 1 0 482087821 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.01 CPU time (s): 1200.19 CPU user time (s): 1200.03 CPU system time (s): 0.158975 CPU usage (%): 100.015 Max. virtual memory (Kb): 19748 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####