Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-air01.opb |
MD5SUM | 90db1995bd949fc5ac74143a523f3bcf |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 3398 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 771 |
Biggest coefficient in the objective function | 3698 |
Number of bits for the biggest coefficient in the objective function | 12 |
Sum of the numbers in the objective function | 1192753 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 3698 |
Number of bits of the biggest number in a constraint | 12 |
Biggest sum of numbers in a constraint | 1192753 |
Number of bits of the biggest sum of numbers | 21 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02884 |
Number of variables | 771 |
Total number of constraints | 794 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 794 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 438 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc27 THE 2005-04-21 19:03:30 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=16614 boxname=wulflinc27 idbench=1278 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 90db1995bd949fc5ac74143a523f3bcf /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-air01.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-air01.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-air01.opb IDLAUNCH: 16614 /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: 778124 kB Buffers: 19212 kB Cached: 214740 kB SwapCached: 512 kB Active: 33424 kB Inactive: 202500 kB HighTotal: 131008 kB HighFree: 5544 kB LowTotal: 903652 kB LowFree: 772580 kB SwapTotal: 2097892 kB SwapFree: 2096468 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5092 kB Slab: 15092 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 19:23:33 (client local time) WITH STATUS 10 IN 1200.28 SECONDS stats: 16614 7 1200.28 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 46 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####################### c -- Clauses(.)/Splits(s): (none) c ---[ 44]---> BDD-cost: 49 c ---[ 42]---> BDD-cost: 39 c ---[ 40]---> BDD-cost: 41 c ---[ 38]---> BDD-cost: 53 c ---[ 36]---> BDD-cost: 63 c ---[ 34]---> BDD-cost: 61 c ---[ 32]---> BDD-cost: 83 c ---[ 30]---> BDD-cost: 111 c ---[ 28]---> BDD-cost: 139 c ---[ 26]---> BDD-cost: 197 c ---[ 24]---> BDD-cost: 233 c ---[ 22]---> BDD-cost: 273 c ---[ 20]---> BDD-cost: 353 c ---[ 18]---> BDD-cost: 331 c ---[ 16]---> BDD-cost: 527 c ---[ 14]---> BDD-cost: 589 c ---[ 12]---> BDD-cost: 607 c ---[ 10]---> BDD-cost: 559 c ---[ 8]---> BDD-cost: 755 c ---[ 6]---> BDD-cost: 769 c ---[ 4]---> BDD-cost: 741 c ---[ 2]---> BDD-cost: 781 c ---[ 0]---> BDD-cost: 873 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 36957 102667 | 12319 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 9600[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 7920 maxlim: 1183153 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25 | 92284 300283 | 30761 25 1588 63.5 | 0.000 % | c ============================================================================== c [1mFound solution: 8045[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1184708 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 37 | 92299 300397 | 30766 37 1920 51.9 | 0.000 % | c ============================================================================== c [1mFound solution: 7602[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1185151 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39 | 92309 300440 | 30769 39 2038 52.3 | 0.000 % | c ============================================================================== c [1mFound solution: 7071[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1185682 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40 | 92322 300533 | 30774 40 2041 51.0 | 0.000 % | c ============================================================================== c [1mFound solution: 6228[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1186525 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 43 | 92330 300634 | 30776 43 4471 104.0 | 0.000 % | c | 146 | 92287 300487 | 33853 142 20060 141.3 | 0.419 % | c ============================================================================== c [1mFound solution: 6155[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1186598 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 286 | 92298 300568 | 30766 282 54056 191.7 | 0.419 % | c ============================================================================== c [1mFound solution: 6118[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1186635 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 317 | 92301 300608 | 30767 313 55297 176.7 | 0.419 % | c ============================================================================== c [1mFound solution: 5874[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1186879 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 363 | 92303 300626 | 30767 359 62358 173.7 | 0.419 % | c | 463 | 92295 300596 | 33843 457 89183 195.1 | 0.483 % | c | 613 | 92295 300596 | 37228 607 98303 161.9 | 0.483 % | c | 839 | 92295 300596 | 40950 833 108131 129.8 | 0.483 % | c ============================================================================== c [1mFound solution: 5710[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1187043 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1085 | 92305 300655 | 30768 1079 180637 167.4 | 0.483 % | c | 1185 | 92305 300655 | 33844 1179 205973 174.7 | 0.507 % | c | 1340 | 92266 300527 | 37229 1328 232416 175.0 | 0.513 % | c | 1565 | 92266 300527 | 40952 1553 287797 185.3 | 0.513 % | c | 1906 | 92266 300527 | 45047 1894 423841 223.8 | 0.513 % | c ============================================================================== c [1mFound solution: 5686[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 5680 maxlim: 1186452 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2181 | 131914 442145 | 43971 2169 515824 237.8 | 0.513 % | c | 2281 | 131914 442145 | 48368 2269 552824 243.6 | 0.455 % | c | 2431 | 131914 442145 | 53204 2419 564533 233.4 | 0.455 % | c | 2657 | 131914 442145 | 58525 2645 713146 269.6 | 0.455 % | c | 2994 | 131914 442145 | 64377 2982 808284 271.1 | 0.455 % | c | 3500 | 131878 442021 | 70815 3484 997316 286.3 | 0.485 % | c ============================================================================== c [1mFound solution: 5200[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1186938 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3758 | 131885 442118 | 43961 3742 1120517 299.4 | 0.485 % | c | 3858 | 131885 442118 | 48357 3842 1142582 297.4 | 0.516 % | c | 4011 | 131885 442118 | 53192 3995 1207722 302.3 | 0.516 % | c | 4238 | 131885 442118 | 58512 4222 1329460 314.9 | 0.516 % | c | 4576 | 131885 442118 | 64363 4560 1553557 340.7 | 0.516 % | c | 5082 | 131814 441867 | 70799 5038 1705011 338.4 | 0.569 % | c ============================================================================== c [1mFound solution: 5149[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1186989 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5140 | 131819 441939 | 43939 5096 1713826 336.3 | 0.569 % | c | 5240 | 131819 441939 | 48332 5196 1759631 338.7 | 0.591 % | c | 5395 | 131819 441939 | 53166 5351 1778936 332.4 | 0.591 % | c | 5623 | 131819 441939 | 58482 5579 1981123 355.1 | 0.591 % | c | 5960 | 131718 441584 | 64331 5911 2117862 358.3 | 0.604 % | c | 6469 | 131699 441521 | 70764 6418 2510617 391.2 | 0.626 % | c | 7229 | 131699 441521 | 77840 7178 2746938 382.7 | 0.626 % | c ============================================================================== c [1mFound solution: 5103[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 5842 maxlim: 1185756 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7991 | 172505 587332 | 57501 7940 3016324 379.9 | 0.626 % | c | 8095 | 172497 587302 | 63251 8042 3026841 376.4 | 0.568 % | c | 8246 | 172497 587302 | 69576 8193 3121673 381.0 | 0.568 % | c | 8471 | 172497 587302 | 76533 8418 3179608 377.7 | 0.568 % | c | 8808 | 172490 587279 | 84187 8754 3262628 372.7 | 0.571 % | c | 9314 | 172490 587279 | 92605 9260 3525891 380.8 | 0.571 % | c | 10075 | 172490 587279 | 101866 10021 3918602 391.0 | 0.571 % | c | 11214 | 172490 587279 | 112053 11160 4528254 405.8 | 0.571 % | c ============================================================================== c [1mFound solution: 4762[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1186097 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11570 | 172474 587265 | 57491 11514 4549068 395.1 | 0.571 % | c | 11672 | 172474 587265 | 63240 11616 4622997 398.0 | 0.592 % | c | 11823 | 172474 587265 | 69564 11767 4655865 395.7 | 0.592 % | c | 12048 | 172474 587265 | 76520 11992 4771881 397.9 | 0.592 % | c ============================================================================== c [1mFound solution: 4493[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1186366 bits: 21/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12202 | 172491 587387 | 57497 12146 4810251 396.0 | 0.592 % | c | 12303 | 172491 587387 | 63246 12247 4814925 393.2 | 0.617 % | c | 12453 | 172491 587387 | 69571 12397 4855380 391.7 | 0.617 % | c | 12682 | 172491 587387 | 76528 12626 4872784 385.9 | 0.617 % | c | 13020 | 172491 587387 | 84181 12964 4910096 378.7 | 0.617 % | c | 13527 | 172491 587387 | 92599 13471 4973987 369.2 | 0.617 % | c | 14287 | 172491 587387 | 101859 14231 5297532 372.3 | 0.617 % | c | 15426 | 172425 587161 | 112045 15359 5586821 363.7 | 0.624 % | c | 17134 | 172356 586916 | 123249 17060 6103697 357.8 | 0.631 % | c | 19698 | 172305 586744 | 135574 19620 7151850 364.5 | 0.634 % | c | 23542 | 172297 586714 | 149132 23463 8904453 379.5 | 0.638 % | c | 29308 | 172289 586684 | 164045 29227 11246200 384.8 | 0.641 % | c | 37959 | 172212 586419 | 180450 37869 14748953 389.5 | 0.690 % | c | 50936 | 172207 586404 | 198495 50841 19984087 393.1 | 0.694 % | c | 70397 | 172043 585843 | 218344 70221 27253124 388.1 | 0.767 % | c c *** TERMINATED *** s SATISFIABLE v -CL000001_bit0 -CL000002_bit0 -CL000003_bit0 -CL000004_bit0 -CL000005_bit0 -CL000006_bit0 -CL000007_bit0 -CL000008_bit0 CL000009_bit0 -CL000010_bit0 -CL000011_bit0 -CL000012_bit0 -CL000013_bit0 -CL000014_bit0 -CL000015_bit0 -CL000016_bit0 -CL000017_bit0 -CL000018_bit0 -CL000019_bit0 -CL000020_bit0 -CL000021_bit0 -CL000022_bit0 -CL000023_bit0 -CL000024_bit0 -CL000025_bit0 -CL000026_bit0 -CL000027_bit0 -CL000028_bit0 -CL000029_bit0 -CL000030_bit0 -CL000031_bit0 -CL000032_bit0 -CL000033_bit0 -CL000034_bit0 -CL000035_bit0 -CL000036_bit0 -CL000037_bit0 -CL000038_bit0 -CL000039_bit0 -CL000040_bit0 -CL000041_bit0 -CL000042_bit0 -CL000043_bit0 -CL000044_bit0 -CL000045_bit0 -CL000046_bit0 -CL000047_bit0 -CL000048_bit0 -CL000049_bit0 -CL000050_bit0 -CL000051_bit0 -CL000052_bit0 CL000053_bit0 -CL000054_bit0 -CL000055_bit0 -CL000056_bit0 -CL000057_bit0 -CL000058_bit0 -CL000059_bit0 -CL000060_bit0 -CL000061_bit0 -CL000062_bit0 -CL000063_bit0 -CL000064_bit0 -CL000065_bit0 -CL000066_bit0 -CL000067_bit0 -CL000068_bit0 -CL000069_bit0 -CL000070_bit0 -CL000071_bit0 -CL000072_bit0 -CL000073_bit0 -CL000074_bit0 -CL000075_bit0 -CL000076_bit0 -CL000077_bit0 -CL000078_bit0 -CL000079_bit0 -CL000080_bit0 -CL000081_bit0 -CL000082_bit0 -CL000083_bit0 -CL000084_bit0 -CL000085_bit0 -CL000086_bit0 -CL000087_bit0 -CL000088_bit0 -CL000089_bit0 -CL000090_bit0 -CL000091_bit0 -CL000092_bit0 -CL000093_bit0 -CL000094_bit0 -CL000095_bit0 -CL000096_bit0 -CL000097_bit0 -CL000098_bit0 -CL000099_bit0 -CL000100_bit0 -CL000101_bit0 -CL000102_bit0 -CL000103_bit0 -CL000104_bit0 -CL000105_bit0 -CL000106_bit0 -CL000107_bit0 -CL000108_bit0 -CL000109_bit0 -CL000110_bit0 -CL000111_bit0 -CL000112_bit0 -CL000113_bit0 -CL000114_bit0 -CL000115_bit0 -CL000116_bit0 -CL000117_bit0 -CL000118_bit0 -CL000119_bit0 -CL000120_bit0 -CL000121_bit0 -CL000122_bit0 -CL000123_bit0 -CL000124_bit0 -CL000125_bit0 -CL000126_bit0 -CL000127_bit0 -CL000128_bit0 -CL000129_bit0 -CL000130_bit0 -CL000131_bit0 -CL000132_bit0 -CL000133_bit0 -CL000134_bit0 -CL000135_bit0 -CL000136_bit0 -CL000137_bit0 -CL000138_bit0 -CL000139_bit0 -CL000140_bit0 -CL000141_bit0 -CL000142_bit0 -CL000143_bit0 -CL000144_bit0 -CL000145_bit0 -CL000146_bit0 -CL000147_bit0 -CL000148_bit0 -CL000149_bit0 -CL000150_bit0 -CL000151_bit0 -CL000152_bit0 -CL000153_bit0 -CL000154_bit0 -CL000155_bit0 -CL000156_bit0 CL000157_bit0 -CL000158_bit0 -CL000159_bit0 -CL000160_bit0 -CL000161_bit0 -CL000162_bit0 -CL000163_bit0 -CL000164_bit0 -CL000165_bit0 -CL000166_bit0 -CL000167_bit0 -CL000168_bit0 -CL000169_bit0 -CL000170_bit0 -CL000171_bit0 -CL000172_bit0 -CL000173_bit0 -CL000174_bit0 -CL000175_bit0 -CL000176_bit0 -CL000177_bit0 -CL000178_bit0 -CL000179_bit0 -CL000180_bit0 -CL000181_bit0 -CL000182_bit0 -CL000183_bit0 -CL000184_bit0 -CL000185_bit0 -CL000186_bit0 -CL000187_bit0 -CL000188_bit0 -CL000189_bit0 -CL000190_bit0 -CL000191_bit0 -CL000192_bit0 -CL000193_bit0 -CL000194_bit0 -CL000195_bit0 -CL000196_bit0 -CL000197_bit0 -CL000198_bit0 -CL000199_bit0 -CL000200_bit0 -CL000201_bit0 -CL000202_bit0 -CL000203_bit0 -CL000204_bit0 -CL000205_bit0 -CL000206_bit0 -CL000207_bit0 -CL000208_bit0 -CL000209_bit0 -CL000210_bit0 -CL000211_bit0 -CL000212_bit0 -CL000213_bit0 -CL000214_bit0 -CL000215_bit0 -CL000216_bit0 -CL000217_bit0 -CL000218_bit0 -CL000219_bit0 -CL000220_bit0 -CL000221_bit0 -CL000222_bit0 -CL000223_bit0 -CL000224_bit0 -CL000225_bit0 -CL000226_bit0 -CL000227_bit0 -CL000228_bit0 -CL000229_bit0 -CL000230_bit0 -CL000231_bit0 -CL000232_bit0 -CL000233_bit0 -CL000234_bit0 -CL000235_bit0 -CL000236_bit0 -CL000237_bit0 -CL000238_bit0 -CL000239_bit0 -CL000240_bit0 -CL000241_bit0 -CL000242_bit0 -CL000243_bit0 -CL000244_bit0 -CL000245_bit0 -CL000246_bit0 -CL000247_bit0 -CL000248_bit0 -CL000249_bit0 -CL000250_bit0 -CL000251_bit0 -CL000252_bit0 -CL000253_bit0 -CL000254_bit0 -CL000255_bit0 -CL000256_bit0 -CL000257_bit0 -CL000258_bit0 -CL000259_bit0 -CL000260_bit0 -CL000261_bit0 -CL000262_bit0 -CL000263_bit0 -CL000264_bit0 -CL000265_bit0 -CL000266_bit0 -CL000267_bit0 -CL000268_bit0 -CL000269_bit0 -CL000270_bit0 -CL000271_bit0 -CL000272_bit0 -CL000273_bit0 -CL000274_bit0 -CL000275_bit0 -CL000276_bit0 -CL000277_bit0 -CL000278_bit0 -CL000279_bit0 -CL000280_bit0 -CL000281_bit0 -CL000282_bit0 -CL000283_bit0 -CL000284_bit0 -CL000285_bit0 -CL000286_bit0 CL000287_bit0 -CL000288_bit0 -CL000289_bit0 -CL000290_bit0 -CL000291_bit0 -CL000292_bit0 -CL000293_bit0 -CL000294_bit0 -CL000295_bit0 -CL000296_bit0 -CL000297_bit0 -CL000298_bit0 -CL000299_bit0 -CL000300_bit0 -CL000301_bit0 -CL000302_bit0 -CL000303_bit0 -CL000304_bit0 -CL000305_bit0 -CL000306_bit0 -CL000307_bit0 -CL000308_bit0 -CL000309_bit0 -CL000310_bit0 -CL000311_bit0 -CL000312_bit0 -CL000313_bit0 -CL000314_bit0 -CL000315_bit0 -CL000316_bit0 -CL000317_bit0 -CL000318_bit0 -CL000319_bit0 -CL000320_bit0 -CL000321_bit0 -CL000322_bit0 -CL000323_bit0 -CL000324_bit0 -CL000325_bit0 -CL000326_bit0 -CL000327_bit0 -CL000328_bit0 -CL000329_bit0 -CL000330_bit0 -CL000331_bit0 -CL000332_bit0 -CL000333_bit0 -CL000334_bit0 -CL000335_bit0 -CL000336_bit0 -CL000337_bit0 -CL000338_bit0 -CL000339_bit0 -CL000340_bit0 -CL000341_bit0 -CL000342_bit0 -CL000343_bit0 -CL000344_bit0 -CL000345_bit0 -CL000346_bit0 -CL000347_bit0 -CL000348_bit0 -CL000349_bit0 -CL000350_bit0 -CL000351_bit0 -CL000352_bit0 -CL000353_bit0 -CL000354_bit0 -CL000355_bit0 -CL000356_bit0 -CL000357_bit0 -CL000358_bit0 -CL000359_bit0 -CL000360_bit0 -CL000361_bit0 -CL000362_bit0 -CL000363_bit0 -CL000364_bit0 -CL000365_bit0 -CL000366_bit0 -CL000367_bit0 -CL000368_bit0 -CL000369_bit0 -CL000370_bit0 -CL000371_bit0 CL000372_bit0 -CL000373_bit0 -CL000374_bit0 -CL000375_bit0 -CL000376_bit0 -CL000377_bit0 -CL000378_bit0 -CL000379_bit0 -CL000380_bit0 -CL000381_bit0 -CL000382_bit0 -CL000383_bit0 -CL000384_bit0 -CL000385_bit0 -CL000386_bit0 -CL000387_bit0 -CL000388_bit0 -CL000389_bit0 -CL000390_bit0 -CL000391_bit0 -CL000392_bit0 -CL000393_bit0 -CL000394_bit0 -CL000395_bit0 -CL000396_bit0 -CL000397_bit0 -CL000398_bit0 -CL000399_bit0 -CL000400_bit0 -CL000401_bit0 -CL000402_bit0 -CL000403_bit0 -CL000404_bit0 -CL000405_bit0 -CL000406_bit0 -CL000407_bit0 -CL000408_bit0 -CL000409_bit0 -CL000410_bit0 -CL000411_bit0 -CL000412_bit0 -CL000413_bit0 -CL000414_bit0 -CL000415_bit0 -CL000416_bit0 -CL000417_bit0 -CL000418_bit0 -CL000419_bit0 -CL000420_bit0 -CL000421_bit0 -CL000422_bit0 -CL000423_bit0 -CL000424_bit0 -CL000425_bit0 -CL000426_bit0 -CL000427_bit0 -CL000428_bit0 -CL000429_bit0 -CL000430_bit0 -CL000431_bit0 -CL000432_bit0 -CL000433_bit0 -CL000434_bit0 -CL000435_bit0 -CL000436_bit0 -CL000437_bit0 -CL000438_bit0 -CL000439_bit0 -CL000440_bit0 -CL000441_bit0 -CL000442_bit0 -CL000443_bit0 -CL000444_bit0 -CL000445_bit0 -CL000446_bit0 -CL000447_bit0 -CL000448_bit0 -CL000449_bit0 -CL000450_bit0 -CL000451_bit0 -CL000452_bit0 -CL000453_bit0 -CL000454_bit0 -CL000455_bit0 -CL000456_bit0 -CL000457_bit0 -CL000458_bit0 -CL000459_bit0 -CL000460_bit0 -CL000461_bit0 -CL000462_bit0 -CL000463_bit0 -CL000464_bit0 -CL000465_bit0 -CL000466_bit0 -CL000467_bit0 -CL000468_bit0 -CL000469_bit0 -CL000470_bit0 -CL000471_bit0 -CL000472_bit0 -CL000473_bit0 -CL000474_bit0 -CL000475_bit0 -CL000476_bit0 -CL000477_bit0 -CL000478_bit0 -CL000479_bit0 -CL000480_bit0 -CL000481_bit0 -CL000482_bit0 -CL000483_bit0 -CL000484_bit0 -CL000485_bit0 -CL000486_bit0 -CL000487_bit0 -CL000488_bit0 -CL000489_bit0 -CL000490_bit0 -CL000491_bit0 -CL000492_bit0 -CL000493_bit0 -CL000494_bit0 -CL000495_bit0 -CL000496_bit0 -CL000497_bit0 -CL000498_bit0 -CL000499_bit0 -CL000500_bit0 -CL000501_bit0 -CL000502_bit0 -CL000503_bit0 -CL000504_bit0 -CL000505_bit0 -CL000506_bit0 -CL000507_bit0 -CL000508_bit0 -CL000509_bit0 -CL000510_bit0 -CL000511_bit0 -CL000512_bit0 -CL000513_bit0 -CL000514_bit0 -CL000515_bit0 -CL000516_bit0 -CL000517_bit0 -CL000518_bit0 -CL000519_bit0 -CL000520_bit0 -CL000521_bit0 -CL000522_bit0 -CL000523_bit0 -CL000524_bit0 -CL000525_bit0 -CL000526_bit0 -CL000527_bit0 -CL000528_bit0 -CL000529_bit0 -CL000530_bit0 -CL000531_bit0 -CL000532_bit0 -CL000533_bit0 -CL000534_bit0 -CL000535_bit0 -CL000536_bit0 -CL000537_bit0 -CL000538_bit0 -CL000539_bit0 -CL000540_bit0 -CL000541_bit0 -CL000542_bit0 -CL000543_bit0 -CL000544_bi#### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.92 0.98 0.91 2/54 23683 Raw data (stat): 23683 (runsolver) R 23682 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547448948 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+9.99992 s] Raw data (loadavg): 0.93 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 6750 0 0 0 980 18 0 0 25 0 1 0 547448948 25702400 4993 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6275 4993 603 41 0 6234 0 vsize: 25100 [startup+20.0009 s] Raw data (loadavg): 0.94 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 7860 0 0 0 1977 20 0 0 25 0 1 0 547448948 26357760 5140 4294967295 134512640 134672761 3221224544 3221221940 1075346926 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6435 5140 603 41 0 6394 0 vsize: 25740 [startup+30.0019 s] Raw data (loadavg): 0.95 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 8100 0 0 0 2976 21 0 0 25 0 1 0 547448948 27283456 5380 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6661 5380 603 41 0 6620 0 vsize: 26644 [startup+40.0023 s] Raw data (loadavg): 0.96 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 9267 0 0 0 3972 25 0 0 25 0 1 0 547448948 31219712 6285 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7622 6285 603 41 0 7581 0 vsize: 30488 [startup+50.0034 s] Raw data (loadavg): 0.96 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 9893 0 0 0 4971 27 0 0 25 0 1 0 547448948 32964608 6732 4294967295 134512640 134672761 3221224544 3221223844 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8048 6732 603 41 0 8007 0 vsize: 32192 [startup+60.0032 s] Raw data (loadavg): 0.97 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 10200 0 0 0 5970 28 0 0 25 0 1 0 547448948 34295808 7039 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8373 7039 603 41 0 8332 0 vsize: 33492 [startup+70.0037 s] Raw data (loadavg): 0.97 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 10700 0 0 0 6968 29 0 0 25 0 1 0 547448948 35467264 7334 4294967295 134512640 134672761 3221224544 3221222340 134544418 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8659 7334 603 41 0 8618 0 vsize: 34636 [startup+80.0039 s] Raw data (loadavg): 0.98 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 11040 0 0 0 7967 30 0 0 25 0 1 0 547448948 36765696 7669 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8976 7669 603 41 0 8935 0 vsize: 35904 [startup+90.0046 s] Raw data (loadavg): 0.98 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 11518 0 0 0 8966 32 0 0 25 0 1 0 547448948 38789120 8147 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9470 8147 603 41 0 9429 0 vsize: 37880 [startup+100.004 s] Raw data (loadavg): 0.98 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 11807 0 0 0 9966 32 0 0 25 0 1 0 547448948 39989248 8436 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9763 8436 603 41 0 9722 0 vsize: 39052 [startup+110.004 s] Raw data (loadavg): 0.98 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 12899 0 0 0 10963 35 0 0 25 0 1 0 547448948 43143168 9317 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10533 9317 603 41 0 10492 0 vsize: 42132 [startup+120.005 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 13246 0 0 0 11962 36 0 0 25 0 1 0 547448948 44470272 9664 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10857 9664 603 41 0 10816 0 vsize: 43428 [startup+130.005 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23683 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 13638 0 0 0 12961 37 0 0 25 0 1 0 547448948 46059520 10056 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11245 10056 603 41 0 11204 0 vsize: 44980 [startup+140.005 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 13996 0 0 0 13960 38 0 0 25 0 1 0 547448948 47607808 10414 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11623 10414 603 41 0 11582 0 vsize: 46492 [startup+150.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 14333 0 0 0 14959 40 0 0 25 0 1 0 547448948 48914432 10751 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11942 10751 603 41 0 11901 0 vsize: 47768 [startup+160.005 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 14816 0 0 0 15958 41 0 0 25 0 1 0 547448948 49979392 11013 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12202 11013 603 41 0 12161 0 vsize: 48808 [startup+170.005 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 15203 0 0 0 16957 42 0 0 25 0 1 0 547448948 50581504 11162 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12349 11162 603 41 0 12308 0 vsize: 49396 [startup+180.005 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 15406 0 0 0 17957 42 0 0 25 0 1 0 547448948 51388416 11365 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12546 11365 603 41 0 12505 0 vsize: 50184 [startup+190.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 15653 0 0 0 18956 43 0 0 25 0 1 0 547448948 52420608 11612 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12798 11612 603 41 0 12757 0 vsize: 51192 [startup+200.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 15814 0 0 0 19956 43 0 0 25 0 1 0 547448948 53096448 11773 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12963 11773 603 41 0 12922 0 vsize: 51852 [startup+210.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 16064 0 0 0 20956 44 0 0 25 0 1 0 547448948 54034432 12023 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13192 12023 603 41 0 13151 0 vsize: 52768 [startup+220.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 16341 0 0 0 21955 45 0 0 25 0 1 0 547448948 55279616 12300 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13496 12300 603 41 0 13455 0 vsize: 53984 [startup+230.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 16646 0 0 0 22954 46 0 0 25 0 1 0 547448948 56487936 12605 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13791 12605 603 41 0 13750 0 vsize: 55164 [startup+240.007 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 16910 0 0 0 23954 47 0 0 25 0 1 0 547448948 57536512 12869 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14047 12869 603 41 0 14006 0 vsize: 56188 [startup+250.007 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 17001 0 0 0 24954 47 0 0 25 0 1 0 547448948 57942016 12960 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14146 12960 603 41 0 14105 0 vsize: 56584 [startup+260.007 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 17431 0 0 0 25953 48 0 0 25 0 1 0 547448948 59682816 13390 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14571 13390 603 41 0 14530 0 vsize: 58284 [startup+270.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 17748 0 0 0 26952 49 0 0 25 0 1 0 547448948 61005824 13707 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14894 13707 603 41 0 14853 0 vsize: 59576 [startup+280.007 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 18120 0 0 0 27952 49 0 0 25 0 1 0 547448948 62472192 14079 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15252 14079 603 41 0 15211 0 vsize: 61008 [startup+290.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 18379 0 0 0 28951 50 0 0 25 0 1 0 547448948 63524864 14338 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15509 14338 603 41 0 15468 0 vsize: 62036 [startup+300.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 18756 0 0 0 29951 51 0 0 25 0 1 0 547448948 65097728 14715 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15893 14715 603 41 0 15852 0 vsize: 63572 [startup+310.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 19134 0 0 0 30950 52 0 0 25 0 1 0 547448948 66703360 15093 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16285 15093 603 41 0 16244 0 vsize: 65140 [startup+320.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 19479 0 0 0 31949 53 0 0 25 0 1 0 547448948 68116480 15438 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16630 15438 603 41 0 16589 0 vsize: 66520 [startup+330.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 19844 0 0 0 32948 54 0 0 25 0 1 0 547448948 69550080 15803 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16980 15803 603 41 0 16939 0 vsize: 67920 [startup+340.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 20167 0 0 0 33947 55 0 0 25 0 1 0 547448948 70836224 16126 4294967295 134512640 134672761 3221224544 3221223648 134560231 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17294 16126 603 41 0 17253 0 vsize: 69176 [startup+350.021 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 20554 0 0 0 34947 57 0 0 25 0 1 0 547448948 72458240 16513 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17690 16513 603 41 0 17649 0 vsize: 70760 [startup+360.03 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 20855 0 0 0 35948 57 0 0 25 0 1 0 547448948 73670656 16814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17986 16814 603 41 0 17945 0 vsize: 71944 [startup+370.03 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 21108 0 0 0 36947 58 0 0 25 0 1 0 547448948 74731520 17067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18245 17067 603 41 0 18204 0 vsize: 72980 [startup+380.03 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 21350 0 0 0 37947 58 0 0 25 0 1 0 547448948 75755520 17309 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18495 17309 603 41 0 18454 0 vsize: 73980 [startup+390.03 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 21595 0 0 0 38946 59 0 0 25 0 1 0 547448948 76664832 17554 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18717 17554 603 41 0 18676 0 vsize: 74868 [startup+400.03 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 21876 0 0 0 39945 61 0 0 25 0 1 0 547448948 77864960 17835 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19010 17835 603 41 0 18969 0 vsize: 76040 [startup+410.03 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 22146 0 0 0 40944 61 0 0 25 0 1 0 547448948 78934016 18105 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19271 18105 603 41 0 19230 0 vsize: 77084 [startup+420.031 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 22414 0 0 0 41943 62 0 0 25 0 1 0 547448948 80011264 18373 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19534 18373 603 41 0 19493 0 vsize: 78136 [startup+430.031 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 22707 0 0 0 42943 63 0 0 25 0 1 0 547448948 81309696 18666 4294967295 134512640 134672761 3221224544 3221223728 134559613 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19851 18666 603 41 0 19810 0 vsize: 79404 [startup+440.032 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 23008 0 0 0 43942 64 0 0 25 0 1 0 547448948 82485248 18967 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20138 18967 603 41 0 20097 0 vsize: 80552 [startup+450.031 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 23268 0 0 0 44942 65 0 0 25 0 1 0 547448948 83677184 19227 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20429 19227 603 41 0 20388 0 vsize: 81716 [startup+460.031 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 23578 0 0 0 45941 66 0 0 25 0 1 0 547448948 84996096 19537 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20751 19537 603 41 0 20710 0 vsize: 83004 [startup+470.031 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 23887 0 0 0 46940 67 0 0 25 0 1 0 547448948 86163456 19846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21036 19846 603 41 0 20995 0 vsize: 84144 [startup+480.031 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 24206 0 0 0 47939 68 0 0 25 0 1 0 547448948 87498752 20165 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21362 20165 603 41 0 21321 0 vsize: 85448 [startup+490.031 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 24490 0 0 0 48939 68 0 0 25 0 1 0 547448948 88678400 20449 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21650 20449 603 41 0 21609 0 vsize: 86600 [startup+500.032 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 24698 0 0 0 49939 69 0 0 25 0 1 0 547448948 89473024 20657 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21844 20657 603 41 0 21803 0 vsize: 87376 [startup+510.031 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 24976 0 0 0 50938 69 0 0 25 0 1 0 547448948 90660864 20935 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22134 20935 603 41 0 22093 0 vsize: 88536 [startup+520.032 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 25230 0 0 0 51938 69 0 0 25 0 1 0 547448948 91725824 21189 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22394 21189 603 41 0 22353 0 vsize: 89576 [startup+530.032 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 25454 0 0 0 52937 71 0 0 25 0 1 0 547448948 92655616 21413 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22621 21413 603 41 0 22580 0 vsize: 90484 [startup+540.033 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 25850 0 0 0 53936 72 0 0 25 0 1 0 547448948 94265344 21809 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23014 21809 603 41 0 22973 0 vsize: 92056 [startup+550.032 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 26135 0 0 0 54935 73 0 0 25 0 1 0 547448948 95440896 22094 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23301 22094 603 41 0 23260 0 vsize: 93204 [startup+560.032 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 26457 0 0 0 55934 74 0 0 25 0 1 0 547448948 96747520 22416 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23620 22416 603 41 0 23579 0 vsize: 94480 [startup+570.033 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 26688 0 0 0 56934 74 0 0 25 0 1 0 547448948 97685504 22647 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23849 22647 603 41 0 23808 0 vsize: 95396 [startup+580.033 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 26917 0 0 0 57934 75 0 0 25 0 1 0 547448948 98619392 22876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24077 22876 603 41 0 24036 0 vsize: 96308 [startup+590.034 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 27139 0 0 0 58934 75 0 0 25 0 1 0 547448948 99561472 23098 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24307 23098 603 41 0 24266 0 vsize: 97228 [startup+600.035 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 27360 0 0 0 59933 76 0 0 25 0 1 0 547448948 100352000 23319 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24500 23319 603 41 0 24459 0 vsize: 98000 [startup+610.034 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 27581 0 0 0 60932 77 0 0 25 0 1 0 547448948 101285888 23540 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24728 23540 603 41 0 24687 0 vsize: 98912 [startup+620.034 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 27841 0 0 0 61932 77 0 0 25 0 1 0 547448948 102367232 23800 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24992 23800 603 41 0 24951 0 vsize: 99968 [startup+630.035 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 28053 0 0 0 62931 78 0 0 25 0 1 0 547448948 103301120 24012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25220 24012 603 41 0 25179 0 vsize: 100880 [startup+640.036 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 28352 0 0 0 63931 79 0 0 25 0 1 0 547448948 104497152 24311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25512 24311 603 41 0 25471 0 vsize: 102048 [startup+650.036 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 28658 0 0 0 64930 80 0 0 25 0 1 0 547448948 105684992 24617 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25802 24617 603 41 0 25761 0 vsize: 103208 [startup+660.036 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 28857 0 0 0 65930 80 0 0 25 0 1 0 547448948 106491904 24816 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25999 24816 603 41 0 25958 0 vsize: 103996 [startup+670.036 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 29120 0 0 0 66929 81 0 0 25 0 1 0 547448948 107569152 25079 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26262 25079 603 41 0 26221 0 vsize: 105048 [startup+680.036 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 29376 0 0 0 67929 81 0 0 25 0 1 0 547448948 108650496 25335 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26526 25335 603 41 0 26485 0 vsize: 106104 [startup+690.037 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 29685 0 0 0 68928 82 0 0 25 0 1 0 547448948 109862912 25644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26822 25644 603 41 0 26781 0 vsize: 107288 [startup+700.038 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 30040 0 0 0 69927 83 0 0 25 0 1 0 547448948 111349760 25999 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27185 25999 603 41 0 27144 0 vsize: 108740 [startup+710.038 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 30322 0 0 0 70926 84 0 0 25 0 1 0 547448948 112562176 26281 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27481 26281 603 41 0 27440 0 vsize: 109924 [startup+720.039 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 30578 0 0 0 71925 86 0 0 25 0 1 0 547448948 113635328 26537 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27743 26537 603 41 0 27702 0 vsize: 110972 [startup+730.038 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 30792 0 0 0 72925 86 0 0 25 0 1 0 547448948 114462720 26751 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27945 26751 603 41 0 27904 0 vsize: 111780 [startup+740.039 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 31015 0 0 0 73924 87 0 0 25 0 1 0 547448948 115392512 26974 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28172 26974 603 41 0 28131 0 vsize: 112688 [startup+750.039 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 31220 0 0 0 74924 87 0 0 25 0 1 0 547448948 116195328 27179 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28368 27179 603 41 0 28327 0 vsize: 113472 [startup+760.039 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 31437 0 0 0 75923 88 0 0 25 0 1 0 547448948 117129216 27396 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28596 27396 603 41 0 28555 0 vsize: 114384 [startup+770.04 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 31654 0 0 0 76923 89 0 0 25 0 1 0 547448948 117940224 27613 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28794 27613 603 41 0 28753 0 vsize: 115176 [startup+780.047 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 31914 0 0 0 77923 89 0 0 25 0 1 0 547448948 118996992 27873 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29052 27873 603 41 0 29011 0 vsize: 116208 [startup+790.047 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 32124 0 0 0 78922 90 0 0 25 0 1 0 547448948 119922688 28083 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29278 28083 603 41 0 29237 0 vsize: 117112 [startup+800.048 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 32336 0 0 0 79922 91 0 0 25 0 1 0 547448948 120721408 28295 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29473 28295 603 41 0 29432 0 vsize: 117892 [startup+810.048 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 32554 0 0 0 80921 92 0 0 25 0 1 0 547448948 121659392 28513 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29702 28513 603 41 0 29661 0 vsize: 118808 [startup+820.049 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 32781 0 0 0 81921 93 0 0 25 0 1 0 547448948 122601472 28740 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29932 28740 603 41 0 29891 0 vsize: 119728 [startup+830.049 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 33057 0 0 0 82920 93 0 0 25 0 1 0 547448948 123654144 29016 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30189 29016 603 41 0 30148 0 vsize: 120756 [startup+840.049 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 33266 0 0 0 83920 94 0 0 25 0 1 0 547448948 124575744 29225 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30414 29225 603 41 0 30373 0 vsize: 121656 [startup+850.049 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 33509 0 0 0 84919 94 0 0 25 0 1 0 547448948 125616128 29468 4294967295 134512640 134672761 3221224544 3221223648 134560028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30668 29468 603 41 0 30627 0 vsize: 122672 [startup+860.049 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 33753 0 0 0 85919 95 0 0 25 0 1 0 547448948 126533632 29712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30892 29712 603 41 0 30851 0 vsize: 123568 [startup+870.05 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 33993 0 0 0 86919 95 0 0 25 0 1 0 547448948 127594496 29952 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31151 29952 603 41 0 31110 0 vsize: 124604 [startup+880.05 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 34277 0 0 0 87918 96 0 0 25 0 1 0 547448948 128643072 30236 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31407 30236 603 41 0 31366 0 vsize: 125628 [startup+890.051 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 34529 0 0 0 88918 97 0 0 25 0 1 0 547448948 129716224 30488 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31669 30488 603 41 0 31628 0 vsize: 126676 [startup+900.051 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 34727 0 0 0 89917 97 0 0 25 0 1 0 547448948 130498560 30686 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31860 30686 603 41 0 31819 0 vsize: 127440 [startup+910.051 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 34904 0 0 0 90917 98 0 0 25 0 1 0 547448948 131297280 30863 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32055 30863 603 41 0 32014 0 vsize: 128220 [startup+920.052 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 35071 0 0 0 91916 99 0 0 25 0 1 0 547448948 131960832 31030 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32217 31030 603 41 0 32176 0 vsize: 128868 [startup+930.052 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 35193 0 0 0 92916 99 0 0 25 0 1 0 547448948 132501504 31152 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32349 31152 603 41 0 32308 0 vsize: 129396 [startup+940.053 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 35374 0 0 0 93916 100 0 0 25 0 1 0 547448948 133136384 31333 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32504 31333 603 41 0 32463 0 vsize: 130016 [startup+950.053 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 35578 0 0 0 94915 100 0 0 25 0 1 0 547448948 134041600 31537 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32725 31537 603 41 0 32684 0 vsize: 130900 [startup+960.052 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 35762 0 0 0 95915 101 0 0 25 0 1 0 547448948 134819840 31721 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32915 31721 603 41 0 32874 0 vsize: 131660 [startup+970.052 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 35890 0 0 0 96915 101 0 0 25 0 1 0 547448948 135344128 31849 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33043 31849 603 41 0 33002 0 vsize: 132172 [startup+980.053 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36060 0 0 0 97915 102 0 0 25 0 1 0 547448948 135979008 32019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33198 32019 603 41 0 33157 0 vsize: 132792 [startup+990.054 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36246 0 0 0 98914 102 0 0 25 0 1 0 547448948 136765440 32205 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33390 32205 603 41 0 33349 0 vsize: 133560 [startup+1000.05 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36397 0 0 0 99914 102 0 0 25 0 1 0 547448948 137306112 32356 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33522 32356 603 41 0 33481 0 vsize: 134088 [startup+1010.05 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36540 0 0 0 100914 103 0 0 25 0 1 0 547448948 137916416 32499 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33671 32499 603 41 0 33630 0 vsize: 134684 [startup+1020.05 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36638 0 0 0 101914 103 0 0 25 0 1 0 547448948 138661888 32597 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33853 32597 603 41 0 33812 0 vsize: 135412 [startup+1030.05 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36796 0 0 0 102913 104 0 0 25 0 1 0 547448948 139292672 32755 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34007 32755 603 41 0 33966 0 vsize: 136028 [startup+1040.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 36983 0 0 0 103913 104 0 0 25 0 1 0 547448948 140087296 32942 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34201 32942 603 41 0 34160 0 vsize: 136804 [startup+1050.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 37139 0 0 0 104913 105 0 0 25 0 1 0 547448948 140611584 33098 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34329 33098 603 41 0 34288 0 vsize: 137316 [startup+1060.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 37329 0 0 0 105913 105 0 0 25 0 1 0 547448948 141389824 33288 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34519 33288 603 41 0 34478 0 vsize: 138076 [startup+1070.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 37606 0 0 0 106913 105 0 0 25 0 1 0 547448948 142548992 33565 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34802 33565 603 41 0 34761 0 vsize: 139208 [startup+1080.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 37823 0 0 0 107912 106 0 0 25 0 1 0 547448948 143462400 33782 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35025 33782 603 41 0 34984 0 vsize: 140100 [startup+1090.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 38050 0 0 0 108912 107 0 0 25 0 1 0 547448948 144375808 34009 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35248 34009 603 41 0 35207 0 vsize: 140992 [startup+1100.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 38275 0 0 0 109911 107 0 0 25 0 1 0 547448948 145281024 34234 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35469 34234 603 41 0 35428 0 vsize: 141876 [startup+1110.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 38493 0 0 0 110910 108 0 0 25 0 1 0 547448948 146219008 34452 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35698 34452 603 41 0 35657 0 vsize: 142792 [startup+1120.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 38717 0 0 0 111909 109 0 0 25 0 1 0 547448948 147161088 34676 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35928 34676 603 41 0 35887 0 vsize: 143712 [startup+1130.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 38916 0 0 0 112909 109 0 0 25 0 1 0 547448948 147963904 34875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 36124 34875 603 41 0 36083 0 vsize: 144496 [startup+1140.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 39154 0 0 0 113909 110 0 0 25 0 1 0 547448948 148897792 35113 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 36352 35113 603 41 0 36311 0 vsize: 145408 [startup+1150.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 39282 0 0 0 114908 110 0 0 25 0 1 0 547448948 149438464 35241 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 36484 35241 603 41 0 36443 0 vsize: 145936 [startup+1160.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 39588 0 0 0 115908 111 0 0 25 0 1 0 547448948 150642688 35547 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 36778 35547 603 41 0 36737 0 vsize: 147112 [startup+1170.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 39889 0 0 0 116908 111 0 0 25 0 1 0 547448948 151842816 35848 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 37071 35848 603 41 0 37030 0 vsize: 148284 [startup+1180.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 40223 0 0 0 117907 112 0 0 25 0 1 0 547448948 153313280 36182 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 37430 36182 603 41 0 37389 0 vsize: 149720 [startup+1190.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 40534 0 0 0 118907 113 0 0 25 0 1 0 547448948 154488832 36493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 37717 36493 603 41 0 37676 0 vsize: 150868 [startup+1200.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/54 23685 Raw data (stat): 23683 (minisat+) R 23682 18865 18864 0 -1 0 40791 0 0 0 119907 113 0 0 25 0 1 0 547448948 155537408 36750 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 37973 36750 603 41 0 37932 0 vsize: 151892 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.14 s] Raw data (loadavg): 0.99 0.98 0.91 1/54 23685 Raw data (stat): 23683 (minisat+) Z 23682 18865 18864 0 -1 12 40794 0 0 0 119907 120 0 0 25 0 1 0 547448948 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.14 CPU time (s): 1200.28 CPU user time (s): 1199.07 CPU system time (s): 1.20782 CPU usage (%): 100.012 Max. virtual memory (Kb): 151892 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####