Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii16d1.opb |
MD5SUM | 38e9597c5e2c643da0b2660ad99fee98 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 984 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 2460 |
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 | 2460 |
Number of bits of the sum of numbers in the objective function | 12 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 2460 |
Number of bits of the biggest sum of numbers | 12 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.05 |
Number of variables | 2460 |
Total number of constraints | 17131 |
Number of constraints which are clauses | 17131 |
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 | 16 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc27 THE 2005-05-27 04:42:16 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22896 boxname=wulflinc27 idbench=142 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 38e9597c5e2c643da0b2660ad99fee98 /oldhome/oroussel/tmp/wulflinc27/normalized-ii16d1.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc27/normalized-ii16d1.opb IDLAUNCH: 22896 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 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.169 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: 882720 kB Buffers: 32824 kB Cached: 98072 kB SwapCached: 684 kB Active: 41448 kB Inactive: 91572 kB HighTotal: 131008 kB HighFree: 30212 kB LowTotal: 903652 kB LowFree: 852508 kB SwapTotal: 2097892 kB SwapFree: 2096360 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5092 kB Slab: 13192 kB Committed_AS: 63588 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 05:02:45 (client local time) WITH STATUS 152 IN 1229.88 SECONDS stats: 22896 7 1229.88 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 17131 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 | 17131 50250 | 5710 0 0 nan | 0.000 % | c | 100 | 17131 50250 | 6281 100 6615 66.2 | 0.002 % | c ============================================================================== c [1mFound solution: 1175[0m c ---[ 0]---> Sorter-cost:162876 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 242 | 217965 519635 | 72655 242 11848 49.0 | 0.002 % | c | 342 | 217965 519635 | 79920 342 17024 49.8 | 0.001 % | c | 492 | 217965 519635 | 87912 492 22263 45.2 | 0.001 % | c | 717 | 217314 518246 | 96703 698 34090 48.8 | 0.273 % | c | 1055 | 217266 518146 | 106374 1035 64326 62.2 | 0.292 % | c | 1561 | 216810 517160 | 117011 1527 79293 51.9 | 0.487 % | c | 2320 | 216810 517160 | 128712 2286 144302 63.1 | 0.487 % | c | 3462 | 215572 514442 | 141584 3406 259756 76.3 | 1.032 % | c | 5172 | 214952 513109 | 155742 4820 333113 69.1 | 1.291 % | c | 7735 | 214594 512323 | 171316 7375 429065 58.2 | 1.449 % | c ============================================================================== c [1mFound solution: 1121[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9795 | 215150 513986 | 71716 9430 510456 54.1 | 1.449 % | c | 9895 | 215150 513986 | 78887 9530 514482 54.0 | 1.579 % | c | 10045 | 215150 513986 | 86776 9680 520238 53.7 | 1.579 % | c | 10270 | 215150 513986 | 95453 9905 530805 53.6 | 1.579 % | c | 10608 | 215088 513846 | 104999 10242 548096 53.5 | 1.608 % | c | 11114 | 214387 512293 | 115499 10736 561078 52.3 | 1.921 % | c | 11873 | 214238 511978 | 127049 11492 580642 50.5 | 1.981 % | c | 13012 | 214149 511785 | 139754 12629 732983 58.0 | 2.018 % | c ============================================================================== c [1mFound solution: 941[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14155 | 216452 517526 | 72150 13772 782549 56.8 | 2.018 % | c | 14257 | 216452 517526 | 79365 13874 784939 56.6 | 2.003 % | c | 14407 | 216452 517526 | 87301 14024 790669 56.4 | 2.003 % | c | 14632 | 216267 517119 | 96031 14246 796451 55.9 | 2.084 % | c | 14970 | 216267 517119 | 105634 14584 807144 55.3 | 2.084 % | c | 15476 | 216214 517006 | 116198 15089 832405 55.2 | 2.105 % | c | 16235 | 216214 517006 | 127818 15848 890382 56.2 | 2.105 % | c | 17375 | 216143 516853 | 140599 16987 936368 55.1 | 2.135 % | c | 19083 | 215551 515559 | 154659 18650 1123950 60.3 | 2.386 % | c | 21646 | 212930 509742 | 170125 21131 1357586 64.2 | 3.544 % | c | 25493 | 212930 509742 | 187138 24978 1805324 72.3 | 3.544 % | c | 31259 | 212192 508088 | 205852 30715 2220344 72.3 | 3.877 % | c | 39909 | 211284 506058 | 226437 39332 2894793 73.6 | 4.283 % | c | 52883 | 210876 505146 | 249081 52250 4143761 79.3 | 4.465 % | c | 72344 | 210292 503868 | 273989 71682 6100824 85.1 | 4.715 % | c | 101536 | 207376 497402 | 301388 100675 10710849 106.4 | 6.001 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 28187 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.94 0.96 0.71 2/54 28183 Raw data (stat): 28183 (runsolver) R 28182 3394 3393 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853359792 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0009 s] Raw data (loadavg): 0.95 0.96 0.71 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0014 s] Raw data (loadavg): 0.95 0.96 0.71 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0022 s] Raw data (loadavg): 0.96 0.96 0.71 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0033 s] Raw data (loadavg): 0.97 0.96 0.72 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0038 s] Raw data (loadavg): 0.97 0.96 0.72 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0035 s] Raw data (loadavg): 0.98 0.96 0.72 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0043 s] Raw data (loadavg): 0.98 0.96 0.73 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0051 s] Raw data (loadavg): 0.98 0.96 0.73 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.006 s] Raw data (loadavg): 0.98 0.96 0.73 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.007 s] Raw data (loadavg): 0.99 0.97 0.73 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.008 s] Raw data (loadavg): 0.99 0.97 0.73 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.008 s] Raw data (loadavg): 0.99 0.97 0.74 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.008 s] Raw data (loadavg): 0.99 0.97 0.74 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.009 s] Raw data (loadavg): 0.99 0.97 0.74 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.01 s] Raw data (loadavg): 0.99 0.97 0.74 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.01 s] Raw data (loadavg): 0.99 0.97 0.74 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.01 s] Raw data (loadavg): 0.99 0.97 0.75 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.01 s] Raw data (loadavg): 0.99 0.97 0.75 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.01 s] Raw data (loadavg): 0.99 0.97 0.75 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.01 s] Raw data (loadavg): 0.99 0.97 0.75 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.01 s] Raw data (loadavg): 0.99 0.97 0.75 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.011 s] Raw data (loadavg): 0.99 0.97 0.76 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.011 s] Raw data (loadavg): 0.99 0.97 0.76 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.011 s] Raw data (loadavg): 0.99 0.97 0.76 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.012 s] Raw data (loadavg): 0.99 0.97 0.76 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.012 s] Raw data (loadavg): 0.99 0.97 0.76 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.012 s] Raw data (loadavg): 0.99 0.97 0.77 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.013 s] Raw data (loadavg): 0.99 0.97 0.77 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.013 s] Raw data (loadavg): 0.99 0.97 0.77 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.014 s] Raw data (loadavg): 0.99 0.97 0.77 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.014 s] Raw data (loadavg): 0.99 0.97 0.77 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.014 s] Raw data (loadavg): 0.99 0.97 0.78 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.015 s] Raw data (loadavg): 0.99 0.97 0.78 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.015 s] Raw data (loadavg): 0.99 0.97 0.78 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.016 s] Raw data (loadavg): 0.99 0.97 0.78 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.017 s] Raw data (loadavg): 0.99 0.97 0.78 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.018 s] Raw data (loadavg): 0.99 0.97 0.79 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.018 s] Raw data (loadavg): 0.99 0.97 0.79 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.018 s] Raw data (loadavg): 0.99 0.97 0.79 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.019 s] Raw data (loadavg): 0.99 0.97 0.79 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.019 s] Raw data (loadavg): 0.99 0.97 0.79 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.02 s] Raw data (loadavg): 0.99 0.97 0.80 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.02 s] Raw data (loadavg): 0.99 0.97 0.80 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.02 s] Raw data (loadavg): 0.99 0.97 0.80 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.021 s] Raw data (loadavg): 0.99 0.97 0.80 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.022 s] Raw data (loadavg): 0.99 0.97 0.80 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.023 s] Raw data (loadavg): 0.99 0.97 0.81 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.022 s] Raw data (loadavg): 0.99 0.97 0.81 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.022 s] Raw data (loadavg): 0.99 0.97 0.81 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.023 s] Raw data (loadavg): 0.99 0.97 0.81 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.023 s] Raw data (loadavg): 0.99 0.97 0.81 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.024 s] Raw data (loadavg): 0.99 0.97 0.81 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.024 s] Raw data (loadavg): 0.99 0.97 0.82 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.024 s] Raw data (loadavg): 0.99 0.97 0.82 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.024 s] Raw data (loadavg): 0.99 0.97 0.82 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.025 s] Raw data (loadavg): 0.99 0.97 0.82 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.026 s] Raw data (loadavg): 0.99 0.97 0.82 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.026 s] Raw data (loadavg): 0.99 0.97 0.82 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.026 s] Raw data (loadavg): 0.99 0.97 0.82 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.026 s] Raw data (loadavg): 0.99 0.97 0.82 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.026 s] Raw data (loadavg): 0.99 0.97 0.83 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.027 s] Raw data (loadavg): 0.99 0.97 0.83 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.028 s] Raw data (loadavg): 0.99 0.97 0.83 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.028 s] Raw data (loadavg): 0.99 0.97 0.83 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.028 s] Raw data (loadavg): 0.99 0.97 0.83 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.033 s] Raw data (loadavg): 0.99 0.97 0.83 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.034 s] Raw data (loadavg): 0.99 0.97 0.83 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.034 s] Raw data (loadavg): 0.99 0.97 0.83 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.033 s] Raw data (loadavg): 0.99 0.97 0.83 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.034 s] Raw data (loadavg): 0.99 0.97 0.83 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.035 s] Raw data (loadavg): 0.99 0.97 0.84 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.036 s] Raw data (loadavg): 0.99 0.97 0.84 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.037 s] Raw data (loadavg): 0.99 0.97 0.84 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.036 s] Raw data (loadavg): 0.99 0.97 0.84 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.037 s] Raw data (loadavg): 0.99 0.97 0.84 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.037 s] Raw data (loadavg): 0.99 0.97 0.84 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.038 s] Raw data (loadavg): 0.99 0.97 0.84 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.038 s] Raw data (loadavg): 0.99 0.97 0.84 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.037 s] Raw data (loadavg): 0.99 0.97 0.84 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.038 s] Raw data (loadavg): 0.99 0.97 0.84 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.038 s] Raw data (loadavg): 0.99 0.97 0.85 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.038 s] Raw data (loadavg): 0.99 0.97 0.85 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.039 s] Raw data (loadavg): 0.99 0.97 0.85 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.038 s] Raw data (loadavg): 0.99 0.97 0.85 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.038 s] Raw data (loadavg): 0.99 0.97 0.85 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.038 s] Raw data (loadavg): 0.99 0.97 0.85 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.039 s] Raw data (loadavg): 0.99 0.97 0.85 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.039 s] Raw data (loadavg): 0.99 0.97 0.85 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.039 s] Raw data (loadavg): 0.99 0.97 0.85 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.039 s] Raw data (loadavg): 0.99 0.97 0.85 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.039 s] Raw data (loadavg): 0.99 0.97 0.85 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.04 s] Raw data (loadavg): 0.99 0.97 0.86 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.041 s] Raw data (loadavg): 0.99 0.97 0.86 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.041 s] Raw data (loadavg): 0.99 0.97 0.86 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.042 s] Raw data (loadavg): 0.99 0.97 0.86 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.041 s] Raw data (loadavg): 0.99 0.97 0.86 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.042 s] Raw data (loadavg): 0.99 0.97 0.86 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.042 s] Raw data (loadavg): 0.99 0.97 0.86 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.042 s] Raw data (loadavg): 0.99 0.97 0.86 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.04 s] Raw data (loadavg): 0.99 0.97 0.86 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.04 s] Raw data (loadavg): 0.99 0.97 0.86 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.04 s] Raw data (loadavg): 0.99 0.97 0.87 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.04 s] Raw data (loadavg): 0.99 0.97 0.87 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.04 s] Raw data (loadavg): 0.99 0.97 0.87 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.04 s] Raw data (loadavg): 0.99 0.97 0.87 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.04 s] Raw data (loadavg): 0.99 0.97 0.87 2/55 28187 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.04 s] Raw data (loadavg): 1.07 0.99 0.88 2/56 28188 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.18 s] Raw data (loadavg): 1.22 1.02 0.89 3/57 28234 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.18 s] Raw data (loadavg): 1.18 1.02 0.89 2/55 28240 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.18 s] Raw data (loadavg): 1.15 1.02 0.89 2/55 28240 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.18 s] Raw data (loadavg): 1.13 1.02 0.89 2/55 28240 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.18 s] Raw data (loadavg): 1.11 1.02 0.89 2/55 28240 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.18 s] Raw data (loadavg): 1.09 1.02 0.89 2/55 28240 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.18 s] Raw data (loadavg): 1.08 1.01 0.89 2/55 28240 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.18 s] Raw data (loadavg): 1.06 1.01 0.89 2/55 28240 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.18 s] Raw data (loadavg): 1.05 1.01 0.90 2/55 28242 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.18 s] Raw data (loadavg): 1.05 1.01 0.90 2/55 28242 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.18 s] Raw data (loadavg): 1.04 1.01 0.90 2/55 28242 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.18 s] Raw data (loadavg): 1.03 1.01 0.90 2/55 28242 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.18 s] Raw data (loadavg): 1.03 1.01 0.90 2/55 28242 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.18 s] Raw data (loadavg): 1.02 1.01 0.90 2/55 28242 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.18 s] Raw data (loadavg): 1.02 1.01 0.90 2/55 28242 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.75 s] Raw data (loadavg): 1.02 1.01 0.90 1/53 28242 Raw data (stat): 28183 (minisat+_script) S 28182 3394 3393 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 853359792 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.75 CPU time (s): 1229.88 CPU user time (s): 1229.1 CPU system time (s): 0.78388 CPU usage (%): 100.011 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####