Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8b1.opb |
MD5SUM | 812314147c77e28d5e428080c7a2412d |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 191 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 672 |
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 | 672 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 672 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.03684 |
Number of variables | 672 |
Total number of constraints | 2404 |
Number of constraints which are clauses | 2404 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 8 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc15 THE 2005-04-14 02:12:28 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4303 boxname=wulflinc15 idbench=167 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 812314147c77e28d5e428080c7a2412d /oldhome/oroussel/tmp/wulflinc15/normalized-ii8b1.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc15/normalized-ii8b1.opb /oldhome/oroussel/tmp/wulflinc15/normalized-ii8b1.opb IDLAUNCH: 4303 /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: 899052 kB Buffers: 36520 kB Cached: 77480 kB SwapCached: 2144 kB Active: 64060 kB Inactive: 54976 kB HighTotal: 131008 kB HighFree: 49616 kB LowTotal: 903652 kB LowFree: 849436 kB SwapTotal: 2097136 kB SwapFree: 2094992 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6916 kB Slab: 11084 kB Committed_AS: 63476 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 02:32:30 (client local time) WITH STATUS 10 IN 1200.17 SECONDS stats: 4303 7 1200.17 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 2404 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 | 2404 5328 | 801 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 224[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:30564 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2 | 39371 91691 | 13123 2 14 7.0 | 0.000 % | c | 102 | 39094 91112 | 14435 93 3903 42.0 | 0.670 % | c | 252 | 39002 90914 | 15878 240 6701 27.9 | 0.882 % | c | 477 | 38987 90884 | 17466 464 15942 34.4 | 0.910 % | c | 815 | 37805 88284 | 19213 776 24356 31.4 | 3.726 % | c | 1322 | 37260 87073 | 21134 1269 45788 36.1 | 5.055 % | c | 2082 | 37129 86792 | 23248 2027 71701 35.4 | 5.354 % | c | 3223 | 37060 86641 | 25573 3166 105927 33.5 | 5.514 % | c | 4933 | 36659 85752 | 28130 4825 171835 35.6 | 6.479 % | c ============================================================================== c [1mFound solution: 213[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 | 5130 | 36761 86021 | 12253 5022 174707 34.8 | 6.479 % | c | 5230 | 36692 85868 | 13478 5120 176718 34.5 | 6.749 % | c | 5381 | 36692 85868 | 14826 5271 182366 34.6 | 6.749 % | c | 5606 | 36692 85868 | 16308 5496 187885 34.2 | 6.749 % | c | 5944 | 36590 85644 | 17939 5831 206859 35.5 | 6.987 % | c | 6450 | 36554 85568 | 19733 6324 229508 36.3 | 7.063 % | c | 7209 | 36479 85399 | 21706 7081 256581 36.2 | 7.249 % | c | 8348 | 36479 85399 | 23877 8220 321429 39.1 | 7.249 % | c ============================================================================== c [1mFound solution: 212[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 | 8492 | 36455 85340 | 12151 8328 322244 38.7 | 7.249 % | c | 8592 | 36412 85243 | 13366 8427 325487 38.6 | 7.439 % | c | 8742 | 36412 85243 | 14702 8577 331063 38.6 | 7.440 % | c ============================================================================== c [1mFound solution: 191[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 | 8825 | 36570 85630 | 12190 8660 333479 38.5 | 7.440 % | c | 8925 | 36570 85630 | 13409 8760 336090 38.4 | 7.604 % | c | 9075 | 36570 85630 | 14749 8910 343099 38.5 | 7.604 % | c | 9301 | 36570 85630 | 16224 9136 351679 38.5 | 7.605 % | c | 9638 | 36570 85630 | 17847 9473 362266 38.2 | 7.604 % | c | 10144 | 36472 85414 | 19632 9977 379563 38.0 | 7.834 % | c | 10905 | 36472 85414 | 21595 10738 407634 38.0 | 7.834 % | c | 12044 | 36472 85414 | 23754 11877 468101 39.4 | 7.834 % | c | 13754 | 36472 85414 | 26130 13587 522596 38.5 | 7.834 % | c | 16317 | 36470 85410 | 28743 16149 629422 39.0 | 7.838 % | c | 20161 | 36426 85316 | 31617 19992 838045 41.9 | 7.936 % | c | 25927 | 36382 85218 | 34779 25757 1118768 43.4 | 8.043 % | c | 34576 | 36305 85037 | 38257 34348 1535481 44.7 | 8.244 % | c | 47550 | 36181 84771 | 42083 21274 996051 46.8 | 8.517 % | c | 67011 | 36135 84671 | 46291 40732 1888951 46.4 | 8.624 % | c | 96203 | 36135 84671 | 50920 35083 1330080 37.9 | 8.624 % | c | 139993 | 36085 84561 | 56012 42013 1861233 44.3 | 8.742 % | c | 205677 | 36085 84561 | 61613 20830 839310 40.3 | 8.742 % | c | 304203 | 36085 84561 | 67775 23016 997862 43.4 | 8.742 % | #### 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.89 0.95 0.92 2/54 3755 Raw data (stat): 3755 (runsolver) R 3754 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422672202 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0004 s] Raw data (loadavg): 0.91 0.95 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 2398 0 0 0 992 6 0 0 25 0 1 0 422672202 11636736 2321 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2841 2321 603 41 0 2800 0 vsize: 11364 [startup+20.0015 s] Raw data (loadavg): 0.92 0.96 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 2682 0 0 0 1990 7 0 0 25 0 1 0 422672202 12972032 2605 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3167 2605 603 41 0 3126 0 vsize: 12668 [startup+30.0016 s] Raw data (loadavg): 0.93 0.96 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 2960 0 0 0 2988 8 0 0 25 0 1 0 422672202 14045184 2883 4294967295 134512640 134672761 3221224560 3221223632 134565153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3429 2883 603 41 0 3388 0 vsize: 13716 [startup+40.0017 s] Raw data (loadavg): 0.94 0.96 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 3202 0 0 0 3987 9 0 0 25 0 1 0 422672202 15085568 3125 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3683 3125 603 41 0 3642 0 vsize: 14732 [startup+50.0026 s] Raw data (loadavg): 0.95 0.96 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 3412 0 0 0 4986 10 0 0 25 0 1 0 422672202 16023552 3335 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3912 3335 603 41 0 3871 0 vsize: 15648 [startup+60.0021 s] Raw data (loadavg): 0.96 0.96 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 3618 0 0 0 5986 11 0 0 25 0 1 0 422672202 16818176 3541 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4106 3541 603 41 0 4065 0 vsize: 16424 [startup+70.0032 s] Raw data (loadavg): 0.96 0.96 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 3785 0 0 0 6986 11 0 0 25 0 1 0 422672202 17473536 3708 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4266 3708 603 41 0 4225 0 vsize: 17064 [startup+80.0041 s] Raw data (loadavg): 0.97 0.96 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 3956 0 0 0 7985 12 0 0 25 0 1 0 422672202 18137088 3879 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4428 3879 603 41 0 4387 0 vsize: 17712 [startup+90.0036 s] Raw data (loadavg): 0.97 0.96 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4157 0 0 0 8985 12 0 0 25 0 1 0 422672202 19070976 4080 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4656 4080 603 41 0 4615 0 vsize: 18624 [startup+100.004 s] Raw data (loadavg): 0.98 0.96 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4371 0 0 0 9984 13 0 0 25 0 1 0 422672202 20000768 4294 4294967295 134512640 134672761 3221224560 3221223744 134559274 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4883 4294 603 41 0 4842 0 vsize: 19532 [startup+110.005 s] Raw data (loadavg): 0.98 0.96 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4629 0 0 0 10983 14 0 0 25 0 1 0 422672202 21069824 4552 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5144 4552 603 41 0 5103 0 vsize: 20576 [startup+120.005 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4634 0 0 0 11984 14 0 0 25 0 1 0 422672202 21069824 4557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5144 4557 603 41 0 5103 0 vsize: 20576 [startup+130.005 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4636 0 0 0 12984 14 0 0 25 0 1 0 422672202 21069824 4559 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5144 4559 603 41 0 5103 0 vsize: 20576 [startup+140.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4640 0 0 0 13984 14 0 0 25 0 1 0 422672202 21069824 4563 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5144 4563 603 41 0 5103 0 vsize: 20576 [startup+150.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4646 0 0 0 14984 14 0 0 25 0 1 0 422672202 21069824 4569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5144 4569 603 41 0 5103 0 vsize: 20576 [startup+160.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4659 0 0 0 15984 14 0 0 25 0 1 0 422672202 21209088 4582 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5178 4582 603 41 0 5137 0 vsize: 20712 [startup+170.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4661 0 0 0 16984 14 0 0 25 0 1 0 422672202 21209088 4584 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5178 4584 603 41 0 5137 0 vsize: 20712 [startup+180.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4661 0 0 0 17984 14 0 0 25 0 1 0 422672202 21209088 4584 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5178 4584 603 41 0 5137 0 vsize: 20712 [startup+190.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4803 0 0 0 18984 15 0 0 25 0 1 0 422672202 21741568 4726 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5308 4726 603 41 0 5267 0 vsize: 21232 [startup+200.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4938 0 0 0 19983 16 0 0 25 0 1 0 422672202 22274048 4861 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5438 4861 603 41 0 5397 0 vsize: 21752 [startup+210.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5073 0 0 0 20983 17 0 0 25 0 1 0 422672202 22941696 4996 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5601 4996 603 41 0 5560 0 vsize: 22404 [startup+220.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5218 0 0 0 21982 17 0 0 25 0 1 0 422672202 23470080 5141 4294967295 134512640 134672761 3221224560 3221223728 134560970 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5730 5141 603 41 0 5689 0 vsize: 22920 [startup+230.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5241 0 0 0 22983 17 0 0 25 0 1 0 422672202 23605248 5164 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5763 5164 603 41 0 5722 0 vsize: 23052 [startup+240.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5243 0 0 0 23983 17 0 0 25 0 1 0 422672202 23605248 5166 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5763 5166 603 41 0 5722 0 vsize: 23052 [startup+250.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5250 0 0 0 24983 17 0 0 25 0 1 0 422672202 23605248 5173 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5763 5173 603 41 0 5722 0 vsize: 23052 [startup+260.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5256 0 0 0 25983 17 0 0 25 0 1 0 422672202 23605248 5179 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5763 5179 603 41 0 5722 0 vsize: 23052 [startup+270.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5269 0 0 0 26983 17 0 0 25 0 1 0 422672202 23769088 5192 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5803 5192 603 41 0 5762 0 vsize: 23212 [startup+280.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5270 0 0 0 27983 17 0 0 25 0 1 0 422672202 23769088 5193 4294967295 134512640 134672761 3221224560 3221223712 134541817 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5803 5193 603 41 0 5762 0 vsize: 23212 [startup+290.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5282 0 0 0 28983 18 0 0 25 0 1 0 422672202 23769088 5205 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5803 5205 603 41 0 5762 0 vsize: 23212 [startup+300.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5297 0 0 0 29983 18 0 0 25 0 1 0 422672202 23932928 5220 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5843 5220 603 41 0 5802 0 vsize: 23372 [startup+310.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5309 0 0 0 30983 18 0 0 25 0 1 0 422672202 23932928 5232 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5843 5232 603 41 0 5802 0 vsize: 23372 [startup+320.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5311 0 0 0 31983 18 0 0 25 0 1 0 422672202 23932928 5234 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5843 5234 603 41 0 5802 0 vsize: 23372 [startup+330.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5313 0 0 0 32983 18 0 0 25 0 1 0 422672202 23932928 5236 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5843 5236 603 41 0 5802 0 vsize: 23372 [startup+340.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5333 0 0 0 33983 18 0 0 25 0 1 0 422672202 24129536 5256 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5891 5256 603 41 0 5850 0 vsize: 23564 [startup+350.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5338 0 0 0 34984 18 0 0 25 0 1 0 422672202 24129536 5261 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5891 5261 603 41 0 5850 0 vsize: 23564 [startup+360.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5394 0 0 0 35984 18 0 0 25 0 1 0 422672202 24260608 5317 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5923 5317 603 41 0 5882 0 vsize: 23692 [startup+370.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5394 0 0 0 36984 18 0 0 25 0 1 0 422672202 24260608 5317 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5923 5317 603 41 0 5882 0 vsize: 23692 [startup+380.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5394 0 0 0 37984 18 0 0 25 0 1 0 422672202 24260608 5317 4294967295 134512640 134672761 3221224560 3221223664 134559902 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5923 5317 603 41 0 5882 0 vsize: 23692 [startup+390.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5398 0 0 0 38984 18 0 0 25 0 1 0 422672202 24260608 5321 4294967295 134512640 134672761 3221224560 3221223664 134559835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5923 5321 603 41 0 5882 0 vsize: 23692 [startup+400.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5403 0 0 0 39985 18 0 0 25 0 1 0 422672202 24412160 5326 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5960 5326 603 41 0 5919 0 vsize: 23840 [startup+410.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5403 0 0 0 40985 18 0 0 25 0 1 0 422672202 24412160 5326 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5960 5326 603 41 0 5919 0 vsize: 23840 [startup+420.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5403 0 0 0 41985 18 0 0 25 0 1 0 422672202 24412160 5326 4294967295 134512640 134672761 3221224560 3221223760 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5960 5326 603 41 0 5919 0 vsize: 23840 [startup+430.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5416 0 0 0 42985 18 0 0 25 0 1 0 422672202 24412160 5339 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5960 5339 603 41 0 5919 0 vsize: 23840 [startup+440.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5425 0 0 0 43985 18 0 0 25 0 1 0 422672202 24412160 5348 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5960 5348 603 41 0 5919 0 vsize: 23840 [startup+450.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5426 0 0 0 44985 18 0 0 25 0 1 0 422672202 24412160 5349 4294967295 134512640 134672761 3221224560 3221223656 1075347274 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5960 5349 603 41 0 5919 0 vsize: 23840 [startup+460.015 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5441 0 0 0 45985 18 0 0 25 0 1 0 422672202 24576000 5364 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6000 5364 603 41 0 5959 0 vsize: 24000 [startup+470.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5449 0 0 0 46985 18 0 0 25 0 1 0 422672202 24576000 5372 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6000 5372 603 41 0 5959 0 vsize: 24000 [startup+480.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5587 0 0 0 47984 19 0 0 25 0 1 0 422672202 25108480 5510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6130 5510 603 41 0 6089 0 vsize: 24520 [startup+490.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5726 0 0 0 48984 20 0 0 25 0 1 0 422672202 25636864 5649 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6259 5649 603 41 0 6218 0 vsize: 25036 [startup+500.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5831 0 0 0 49984 20 0 0 25 0 1 0 422672202 26161152 5754 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6387 5754 603 41 0 6346 0 vsize: 25548 [startup+510.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5945 0 0 0 50984 20 0 0 25 0 1 0 422672202 26558464 5868 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6484 5868 603 41 0 6443 0 vsize: 25936 [startup+520.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5945 0 0 0 51984 20 0 0 25 0 1 0 422672202 26558464 5868 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6484 5868 603 41 0 6443 0 vsize: 25936 [startup+530.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5948 0 0 0 52985 20 0 0 25 0 1 0 422672202 26558464 5871 4294967295 134512640 134672761 3221224560 3221223664 134560059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6484 5871 603 41 0 6443 0 vsize: 25936 [startup+540.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5948 0 0 0 53985 20 0 0 25 0 1 0 422672202 26558464 5871 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6484 5871 603 41 0 6443 0 vsize: 25936 [startup+550.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5948 0 0 0 54985 20 0 0 25 0 1 0 422672202 26558464 5871 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6484 5871 603 41 0 6443 0 vsize: 25936 [startup+560.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5948 0 0 0 55985 20 0 0 25 0 1 0 422672202 26558464 5871 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6484 5871 603 41 0 6443 0 vsize: 25936 [startup+570.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5968 0 0 0 56985 20 0 0 25 0 1 0 422672202 26730496 5891 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6526 5891 603 41 0 6485 0 vsize: 26104 [startup+580.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5987 0 0 0 57985 20 0 0 25 0 1 0 422672202 26730496 5910 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6526 5910 603 41 0 6485 0 vsize: 26104 [startup+590.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5987 0 0 0 58985 20 0 0 25 0 1 0 422672202 26730496 5910 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6526 5910 603 41 0 6485 0 vsize: 26104 [startup+600.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5993 0 0 0 59986 20 0 0 25 0 1 0 422672202 26927104 5916 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6574 5916 603 41 0 6533 0 vsize: 26296 [startup+610.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5995 0 0 0 60986 20 0 0 25 0 1 0 422672202 26927104 5918 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6574 5918 603 41 0 6533 0 vsize: 26296 [startup+620.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5996 0 0 0 61986 20 0 0 25 0 1 0 422672202 26927104 5919 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6574 5919 603 41 0 6533 0 vsize: 26296 [startup+630.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5996 0 0 0 62986 20 0 0 25 0 1 0 422672202 26927104 5919 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6574 5919 603 41 0 6533 0 vsize: 26296 [startup+640.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5997 0 0 0 63986 20 0 0 25 0 1 0 422672202 26927104 5920 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6574 5920 603 41 0 6533 0 vsize: 26296 [startup+650.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6000 0 0 0 64986 20 0 0 25 0 1 0 422672202 26927104 5923 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6574 5923 603 41 0 6533 0 vsize: 26296 [startup+660.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6013 0 0 0 65986 20 0 0 25 0 1 0 422672202 26927104 5936 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6574 5936 603 41 0 6533 0 vsize: 26296 [startup+670.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6127 0 0 0 66986 20 0 0 25 0 1 0 422672202 27324416 6050 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6050 603 41 0 6630 0 vsize: 26684 [startup+680.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6127 0 0 0 67987 20 0 0 25 0 1 0 422672202 27324416 6050 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6050 603 41 0 6630 0 vsize: 26684 [startup+690.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6127 0 0 0 68986 21 0 0 25 0 1 0 422672202 27324416 6050 4294967295 134512640 134672761 3221224560 3221223664 134559853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6050 603 41 0 6630 0 vsize: 26684 [startup+700.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 69986 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6051 603 41 0 6630 0 vsize: 26684 [startup+710.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 70987 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223744 134558831 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6051 603 41 0 6630 0 vsize: 26684 [startup+720.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 71987 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6051 603 41 0 6630 0 vsize: 26684 [startup+730.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 72987 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6051 603 41 0 6630 0 vsize: 26684 [startup+740.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 73987 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6051 603 41 0 6630 0 vsize: 26684 [startup+750.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 74987 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6051 603 41 0 6630 0 vsize: 26684 [startup+760.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 75987 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223744 134558376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6051 603 41 0 6630 0 vsize: 26684 [startup+770.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 76988 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6051 603 41 0 6630 0 vsize: 26684 [startup+780.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 77988 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6051 603 41 0 6630 0 vsize: 26684 [startup+790.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 78988 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223664 134560399 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6051 603 41 0 6630 0 vsize: 26684 [startup+800.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 79988 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6051 603 41 0 6630 0 vsize: 26684 [startup+810.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 80988 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6671 6051 603 41 0 6630 0 vsize: 26684 [startup+820.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6150 0 0 0 81989 21 0 0 25 0 1 0 422672202 27459584 6073 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6704 6073 603 41 0 6663 0 vsize: 26816 [startup+830.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6313 0 0 0 82988 21 0 0 25 0 1 0 422672202 28114944 6236 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6864 6236 603 41 0 6823 0 vsize: 27456 [startup+840.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6471 0 0 0 83988 21 0 0 25 0 1 0 422672202 28774400 6394 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7025 6394 603 41 0 6984 0 vsize: 28100 [startup+850.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6573 0 0 0 84988 22 0 0 25 0 1 0 422672202 29442048 6496 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7188 6496 603 41 0 7147 0 vsize: 28752 [startup+860.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6573 0 0 0 85988 22 0 0 25 0 1 0 422672202 29442048 6496 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7188 6496 603 41 0 7147 0 vsize: 28752 [startup+870.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6573 0 0 0 86988 22 0 0 25 0 1 0 422672202 29442048 6496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7188 6496 603 41 0 7147 0 vsize: 28752 [startup+880.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6576 0 0 0 87988 22 0 0 25 0 1 0 422672202 29442048 6499 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7188 6499 603 41 0 7147 0 vsize: 28752 [startup+890.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6579 0 0 0 88989 22 0 0 25 0 1 0 422672202 29442048 6502 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7188 6502 603 41 0 7147 0 vsize: 28752 [startup+900.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6579 0 0 0 89989 22 0 0 25 0 1 0 422672202 29442048 6502 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7188 6502 603 41 0 7147 0 vsize: 28752 [startup+910.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6593 0 0 0 90989 22 0 0 25 0 1 0 422672202 29585408 6516 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7223 6516 603 41 0 7182 0 vsize: 28892 [startup+920.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6606 0 0 0 91989 22 0 0 25 0 1 0 422672202 29585408 6529 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7223 6529 603 41 0 7182 0 vsize: 28892 [startup+930.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6618 0 0 0 92989 22 0 0 25 0 1 0 422672202 29585408 6541 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7223 6541 603 41 0 7182 0 vsize: 28892 [startup+940.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6621 0 0 0 93990 22 0 0 25 0 1 0 422672202 29745152 6544 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7262 6544 603 41 0 7221 0 vsize: 29048 [startup+950.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6627 0 0 0 94990 22 0 0 25 0 1 0 422672202 29745152 6550 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7262 6550 603 41 0 7221 0 vsize: 29048 [startup+960.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6638 0 0 0 95990 22 0 0 25 0 1 0 422672202 29745152 6561 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7262 6561 603 41 0 7221 0 vsize: 29048 [startup+970.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6658 0 0 0 96990 22 0 0 25 0 1 0 422672202 29908992 6581 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7302 6581 603 41 0 7261 0 vsize: 29208 [startup+980.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6663 0 0 0 97990 22 0 0 25 0 1 0 422672202 29908992 6586 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7302 6586 603 41 0 7261 0 vsize: 29208 [startup+990.027 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6682 0 0 0 98990 22 0 0 25 0 1 0 422672202 29908992 6605 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7302 6605 603 41 0 7261 0 vsize: 29208 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6687 0 0 0 99991 22 0 0 25 0 1 0 422672202 29908992 6610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7302 6610 603 41 0 7261 0 vsize: 29208 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6689 0 0 0 100991 22 0 0 25 0 1 0 422672202 29908992 6612 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7302 6612 603 41 0 7261 0 vsize: 29208 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6832 0 0 0 101990 22 0 0 25 0 1 0 422672202 30576640 6755 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7465 6755 603 41 0 7424 0 vsize: 29860 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 102990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7529 6835 603 41 0 7488 0 vsize: 30116 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 103990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7529 6835 603 41 0 7488 0 vsize: 30116 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 104990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7529 6835 603 41 0 7488 0 vsize: 30116 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 105989 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7529 6835 603 41 0 7488 0 vsize: 30116 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 106990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7529 6835 603 41 0 7488 0 vsize: 30116 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 107990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7529 6835 603 41 0 7488 0 vsize: 30116 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 108990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7529 6835 603 41 0 7488 0 vsize: 30116 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 109990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7529 6835 603 41 0 7488 0 vsize: 30116 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 110990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7529 6835 603 41 0 7488 0 vsize: 30116 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6918 0 0 0 111990 23 0 0 25 0 1 0 422672202 30838784 6841 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7529 6841 603 41 0 7488 0 vsize: 30116 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6922 0 0 0 112991 23 0 0 25 0 1 0 422672202 30978048 6845 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7563 6845 603 41 0 7522 0 vsize: 30252 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6929 0 0 0 113991 23 0 0 25 0 1 0 422672202 30978048 6852 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7563 6852 603 41 0 7522 0 vsize: 30252 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6929 0 0 0 114991 23 0 0 25 0 1 0 422672202 30978048 6852 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7563 6852 603 41 0 7522 0 vsize: 30252 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6934 0 0 0 115991 23 0 0 25 0 1 0 422672202 30978048 6857 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7563 6857 603 41 0 7522 0 vsize: 30252 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6963 0 0 0 116991 23 0 0 25 0 1 0 422672202 31174656 6886 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7611 6886 603 41 0 7570 0 vsize: 30444 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6966 0 0 0 117991 23 0 0 25 0 1 0 422672202 31174656 6889 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7611 6889 603 41 0 7570 0 vsize: 30444 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6966 0 0 0 118991 23 0 0 25 0 1 0 422672202 31174656 6889 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7611 6889 603 41 0 7570 0 vsize: 30444 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 3755 Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6992 0 0 0 119992 23 0 0 25 0 1 0 422672202 31354880 6915 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7655 6915 603 41 0 7614 0 vsize: 30620 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.92 1/54 3755 Raw data (stat): 3755 (minisat+) Z 3754 29151 29150 0 -1 12 6995 0 0 0 119992 25 0 0 25 0 1 0 422672202 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.05 CPU time (s): 1200.17 CPU user time (s): 1199.92 CPU system time (s): 0.250961 CPU usage (%): 100.01 Max. virtual memory (Kb): 30620 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####