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 wulflinc20 THE 2005-04-21 19:02:53 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=16612 boxname=wulflinc20 idbench=1278 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 90db1995bd949fc5ac74143a523f3bcf /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-air01.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-air01.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-air01.opb IDLAUNCH: 16612 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 661916 kB Buffers: 25392 kB Cached: 324292 kB SwapCached: 516 kB Active: 27936 kB Inactive: 323704 kB HighTotal: 131008 kB HighFree: 79576 kB LowTotal: 903652 kB LowFree: 582340 kB SwapTotal: 2097892 kB SwapFree: 2096480 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5116 kB Slab: 15500 kB Committed_AS: 63592 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 19:22:56 (client local time) WITH STATUS 10 IN 1200.42 SECONDS stats: 16612 7 1200.42 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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 20564 53488 | 6169 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/8975 c -- var.elim.: 2000/8975 c -- var.elim.: 3000/8975 c -- var.elim.: 4000/8975 c -- var.elim.: 5000/8975 c -- var.elim.: 6000/8975 c -- var.elim.: 7000/8975 c -- var.elim.: 8000/8975 c -- var.elim.: 8975/8975 c -- var.elim.: 139/139 c -- subsuming c -- var.elim.: 89/89 c -- var.elim.: 86/86 c | 0 | 20490 53248 | -- 0 -- -- | -- | -74/-171 c | 0 | 20490 53248 | 8196 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 0.515921 s) c ============================================================================== c [1mFound solution: 9485[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 7920 maxlim: 1183268 bits: 21/21 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 24 | 75815 250842 | 22744 24 2670 111.2 | 0.000 % | c -- subsuming c -- var.elim.: 1000/8525 c -- var.elim.: 2000/8525 c -- var.elim.: 3000/8525 c -- var.elim.: 4000/8525 c -- var.elim.: 5000/8525 c -- var.elim.: 6000/8525 c -- var.elim.: 7000/8525 c -- var.elim.: 8000/8525 c -- var.elim.: 8525/8525 c -- var.elim.: 22/22 c | 24 | 74329 244892 | -- 24 -- -- | -- | -1459/-5819 c | 24 | 74329 244892 | 29731 24 2670 111.2 | 0.000 % | c ============================================================================== c (current CPU-time: 3.16452 s) c ============================================================================== c [1mFound solution: 7373[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1185380 bits: 21/21 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 32 | 74372 245079 | 22311 32 3822 119.4 | 0.000 % | c -- subsuming c -- var.elim.: 35/35 c -- var.elim.: 21/21 c | 32 | 74337 244905 | -- 32 -- -- | -- | -19/-61 c | 32 | 74337 244905 | 29734 32 3822 119.4 | 0.000 % | c ============================================================================== c (current CPU-time: 4.66229 s) c ============================================================================== c [1mFound solution: 7303[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1185450 bits: 21/21 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 40 | 74362 245032 | 22308 40 4020 100.5 | 0.000 % | c -- subsuming c -- var.elim.: 30/30 c -- var.elim.: 18/18 c | 40 | 74357 245070 | -- 40 -- -- | -- | -5/43 c | 40 | 74357 245070 | 29742 40 4020 100.5 | 0.000 % | c ============================================================================== c (current CPU-time: 6.17706 s) c ============================================================================== c [1mFound solution: 6939[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1185814 bits: 21/21 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 60 | 74386 245211 | 22315 60 5555 92.6 | 0.000 % | c -- subsuming c -- var.elim.: 31/31 c -- var.elim.: 13/13 c | 60 | 74368 245070 | -- 60 -- -- | -- | -6/-10 c | 60 | 74368 245070 | 29747 60 5555 92.6 | 0.000 % | c | 160 | 74368 245070 | 32721 160 13685 85.5 | 1.535 % | c | 310 | 74368 245070 | 35994 310 72941 235.3 | 1.535 % | c | 535 | 74368 245070 | 39593 535 174006 325.2 | 1.535 % | c ============================================================================== c (current CPU-time: 11.0633 s) c ============================================================================== c [1mFound solution: 6605[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1186148 bits: 21/21 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 787 | 74394 245190 | 22318 787 195076 247.9 | 1.535 % | c -- subsuming c -- var.elim.: 31/31 c -- var.elim.: 14/14 c | 787 | 74388 245180 | -- 787 -- -- | -- | -6/-5 c | 787 | 74388 245180 | 29755 787 195076 247.9 | 1.535 % | c | 889 | 74388 245180 | 32730 889 217869 245.1 | 1.565 % | c | 1041 | 74388 245180 | 36003 1041 289623 278.2 | 1.565 % | c | 1267 | 74388 245180 | 39604 1267 421021 332.3 | 1.565 % | c ============================================================================== c (current CPU-time: 14.6168 s) c ============================================================================== c [1mFound solution: 6051[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1186702 bits: 21/21 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1304 | 74400 245269 | 22319 1304 423466 324.7 | 1.565 % | c -- subsuming c -- var.elim.: 17/17 c -- var.elim.: 12/12 c | 1304 | 74387 245175 | -- 1304 -- -- | -- | -7/-27 c | 1304 | 74387 245175 | 29754 1304 423466 324.7 | 1.565 % | c ============================================================================== c (current CPU-time: 16.1975 s) c ============================================================================== c [1mFound solution: 5111[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1187642 bits: 21/21 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1322 | 74405 245281 | 22321 1322 424561 321.2 | 1.565 % | c -- subsuming c -- var.elim.: 22/22 c -- var.elim.: 13/13 c | 1322 | 74392 245203 | -- 1322 -- -- | -- | -4/-3 c | 1322 | 74392 245203 | 29756 1322 424561 321.2 | 1.565 % | c | 1422 | 74392 245203 | 32732 1422 513647 361.2 | 1.652 % | c | 1573 | 74392 245203 | 36005 1573 533037 338.9 | 1.652 % | c | 1799 | 74392 245203 | 39606 1799 677054 376.4 | 1.652 % | c ============================================================================== c (current CPU-time: 20.2789 s) c ============================================================================== c [1mFound solution: 4588[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1188165 bits: 21/21 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1872 | 74413 245300 | 22323 1872 715296 382.1 | 1.652 % | c -- subsuming c -- var.elim.: 487/487 c -- var.elim.: 35/35 c | 1872 | 72796 238753 | -- 1872 -- -- | -- | -10/-865 c | 1872 | 72796 238753 | 29118 1834 713716 389.2 | 1.652 % | c | 1979 | 72796 238753 | 32030 1941 725118 373.6 | 2.972 % | c | 2130 | 72796 238753 | 35233 2092 753016 360.0 | 2.972 % | c | 2355 | 72796 238753 | 38756 2317 824527 355.9 | 2.972 % | c | 2692 | 72796 238753 | 42632 2654 876997 330.4 | 2.972 % | c | 3198 | 72796 238753 | 46895 3160 987776 312.6 | 2.972 % | c | 3957 | 72796 238753 | 51585 3919 1303486 332.6 | 2.972 % | c | 5098 | 72796 238753 | 56743 5060 2082990 411.7 | 2.972 % | c | 6807 | 72796 238753 | 62417 6769 3138315 463.6 | 2.972 % | c ============================================================================== c (current CPU-time: 41.1157 s) c ============================================================================== c [1mFound solution: 3579[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 5026 maxlim: 1185476 bits: 21/21 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 7025 | 107755 363557 | 32326 6987 3169525 453.6 | 2.972 % | c -- subsuming c -- var.elim.: 1000/6998 c -- var.elim.: 2000/6998 c -- var.elim.: 3000/6998 c -- var.elim.: 4000/6998 c -- var.elim.: 5000/6998 c -- var.elim.: 6000/6998 c -- var.elim.: 6998/6998 c -- var.elim.: 79/79 c | 7025 | 106409 358285 | -- 6987 -- -- | -- | -1265/-4914 c | 7025 | 106409 358285 | 42563 6825 3037532 445.1 | 2.972 % | c | 7125 | 106409 358285 | 46819 6925 3047198 440.0 | 3.237 % | c | 7278 | 106409 358285 | 51501 7078 3114086 440.0 | 3.237 % | c | 7504 | 106409 358285 | 56652 7304 3253460 445.4 | 3.237 % | c | 7842 | 106409 358285 | 62317 7642 3366629 440.5 | 3.237 % | c | 8351 | 106409 358285 | 68549 8151 3751806 460.3 | 3.237 % | c | 9111 | 106409 358285 | 75404 8911 4322060 485.0 | 3.237 % | c | 10252 | 106345 358040 | 82894 10048 4911057 488.8 | 3.260 % | c | 11960 | 106345 358040 | 91183 11756 6588634 560.4 | 3.260 % | c | 14522 | 106345 358040 | 100302 14318 8165270 570.3 | 3.260 % | c | 18371 | 106204 357526 | 110186 18158 10845871 597.3 | 3.324 % | c | 24139 | 106204 357526 | 121204 23926 16243260 678.9 | 3.324 % | c | 32788 | 105431 354871 | 132355 32574 30915058 949.1 | 3.804 % | c | 45763 | 105431 354871 | 145590 45549 50244390 1103.1 | 3.804 % | c | 65231 | 105431 354871 | 160149 65017 78862660 1213.0 | 3.804 % | 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_bit0 -CL000545_bit0 -CL000546_bit0 -CL000547_bit0 -CL000548_bit0 -CL000549_bit0 -CL000550_bit0 -CL000551_bit0 -CL000552_bit0 -CL000553_bit0 -CL000554_bit0 -CL000555_bit0 -CL000556_bit0 -CL000557_bit0 -CL000558_bit0 -CL000559_bit0 -CL000560_bit0 -CL000561_bit0 -CL000562_bit0 -CL000563_bit0 -CL000564_bit0 -CL000565_bit0 -CL000566_bit0 -CL000567_bit0 -CL000568_bit0 -CL000569_bit0 -CL000570_bit0 -CL000571_bit0 -CL000572_bit0 -CL000573_bit0 -CL000574_bit0 -CL000575_bit0 -CL000576_bit0 -CL000577_bit0 -CL000578_bit0 -CL000579_bit0 -CL000580_bit0 -CL000581_bit0 -CL000582_bit0 -CL000583_bit0 -CL000584_bit0 -CL000585_bit0 -CL000586_bit0 -CL000587_bit0 -CL000588_bit0 -CL000589_bit0 -CL000590_bit0 -CL000591_bit0 -CL000592_bit0 -CL000593_bit0 -CL000594_bit0 -CL000595_bit0 -CL000596_bit0 -CL000597_bit0 -CL000598_bit0 -CL000599_bit0 -CL000600_bit0 -CL000601_bit0 -CL000602_bit0 -CL000603_bit0 -CL000604_bit0 -CL000605_bit0 -CL000606_bit0 -CL000607_bit0 -CL000608_bit0 -CL000609_bit0 -CL000610_bit0 -CL000611_bit0 -CL000612_bit0 -CL000613_bit0 -CL000614_bit0 -CL000615_bit0 -CL000616_bit0 -CL000617_bit0 -CL000618_bit0 -CL000619_bit0 -CL000620_bit0 -CL000621_bit0 -CL000622_bit0 -CL000623_bit0 -CL000624_bit0 -CL000625_bit0 -CL000626_bit0 -CL000627_bit0 -CL000628_bit0 -CL000629_bit0 -CL000630_bit0 -CL000631_bit0 -CL000632_bit0 -CL000633_bit0 -CL000634_bit0 -CL000635_bit0 -CL000636_bit0 -CL000637_bit0 -CL000638_bit0 -CL000639_bit0 -CL000640_bit0 -CL000641_bit0 -CL000642_bit0 -CL000643_bit0 -CL000644_bit0 -CL000645_bit0 -CL000646_bit0 -CL000647_bit0 -CL000648_bit0 -CL000649_bit0 -CL000650_bit0 -CL000651_bit0 -CL000652_bit0 -CL000653_bit0 -CL000654_b#### 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.97 0.93 2/54 11078 Raw data (stat): 11078 (runsolver) R 11077 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547447420 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+10.0003 s] Raw data (loadavg): 0.93 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 9070 0 0 0 974 24 0 0 25 0 1 0 547447420 31862784 6255 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7779 6255 603 41 0 7738 0 vsize: 31116 [startup+20.0011 s] Raw data (loadavg): 0.94 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 11196 0 0 0 1968 30 0 0 25 0 1 0 547447420 34385920 6848 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8395 6848 603 41 0 8354 0 vsize: 33580 [startup+30.002 s] Raw data (loadavg): 0.95 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 12633 0 0 0 2964 34 0 0 25 0 1 0 547447420 36847616 7446 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8996 7446 603 41 0 8955 0 vsize: 35984 [startup+40.0014 s] Raw data (loadavg): 0.96 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 14417 0 0 0 3960 38 0 0 25 0 1 0 547447420 44232704 9230 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10799 9230 603 41 0 10758 0 vsize: 43196 [startup+50.0022 s] Raw data (loadavg): 0.96 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 16324 0 0 0 4956 42 0 0 25 0 1 0 547447420 48730112 10540 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11897 10540 603 41 0 11856 0 vsize: 47588 [startup+60.0022 s] Raw data (loadavg): 0.97 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 17249 0 0 0 5954 44 0 0 25 0 1 0 547447420 52555776 11465 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12831 11465 603 41 0 12790 0 vsize: 51324 [startup+70.0026 s] Raw data (loadavg): 0.97 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 18026 0 0 0 6953 46 0 0 25 0 1 0 547447420 55713792 12242 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13602 12242 603 41 0 13561 0 vsize: 54408 [startup+80.0033 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 19601 0 0 0 7949 50 0 0 25 0 1 0 547447420 62152704 13817 4294967295 134512640 134672761 3221224544 3221223648 134603706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15174 13817 603 41 0 15133 0 vsize: 60696 [startup+90.0034 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 20646 0 0 0 8947 52 0 0 25 0 1 0 547447420 66473984 14862 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16229 14862 603 41 0 16188 0 vsize: 64916 [startup+100.004 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 21387 0 0 0 9945 54 0 0 25 0 1 0 547447420 69488640 15603 4294967295 134512640 134672761 3221224544 3221223688 134616247 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16965 15603 603 41 0 16924 0 vsize: 67860 [startup+110.004 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 22083 0 0 0 10944 56 0 0 25 0 1 0 547447420 72245248 16299 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17638 16299 603 41 0 17597 0 vsize: 70552 [startup+120.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 23002 0 0 0 11942 58 0 0 25 0 1 0 547447420 76148736 17218 4294967295 134512640 134672761 3221224544 3221223728 134615617 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18591 17218 603 41 0 18550 0 vsize: 74364 [startup+130.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 23845 0 0 0 12940 60 0 0 25 0 1 0 547447420 79536128 18061 4294967295 134512640 134672761 3221224544 3221223728 134615835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19418 18061 603 41 0 19377 0 vsize: 77672 [startup+140.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 24912 0 0 0 13937 63 0 0 25 0 1 0 547447420 83959808 19128 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20498 19128 603 41 0 20457 0 vsize: 81992 [startup+150.005 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11078 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 25999 0 0 0 14934 67 0 0 25 0 1 0 547447420 88371200 20215 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21575 20215 603 41 0 21534 0 vsize: 86300 [startup+160.004 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 27026 0 0 0 15932 68 0 0 25 0 1 0 547447420 92602368 21242 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22608 21242 603 41 0 22567 0 vsize: 90432 [startup+170.005 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 27929 0 0 0 16930 71 0 0 25 0 1 0 547447420 96272384 22145 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23504 22145 603 41 0 23463 0 vsize: 94016 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 28697 0 0 0 17928 73 0 0 25 0 1 0 547447420 99405824 22913 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24269 22913 603 41 0 24228 0 vsize: 97076 [startup+190.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 29424 0 0 0 18926 75 0 0 25 0 1 0 547447420 102391808 23640 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24998 23640 603 41 0 24957 0 vsize: 99992 [startup+200.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 30408 0 0 0 19924 78 0 0 25 0 1 0 547447420 106381312 24624 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25972 24624 603 41 0 25931 0 vsize: 103888 [startup+210.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 31813 0 0 0 20921 81 0 0 25 0 1 0 547447420 112226304 26029 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27399 26029 603 41 0 27358 0 vsize: 109596 [startup+220.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 32869 0 0 0 21919 83 0 0 25 0 1 0 547447420 116527104 27085 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28449 27085 603 41 0 28408 0 vsize: 113796 [startup+230.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 34018 0 0 0 22917 85 0 0 25 0 1 0 547447420 121257984 28234 4294967295 134512640 134672761 3221224544 3221223728 134615683 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29604 28234 603 41 0 29563 0 vsize: 118416 [startup+240.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 35278 0 0 0 23915 88 0 0 25 0 1 0 547447420 126316544 29494 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30839 29494 603 41 0 30798 0 vsize: 123356 [startup+250.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 36600 0 0 0 24913 90 0 0 25 0 1 0 547447420 131780608 30816 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32173 30816 603 41 0 32132 0 vsize: 128692 [startup+260.009 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 37948 0 0 0 25910 93 0 0 25 0 1 0 547447420 137297920 32164 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33520 32164 603 41 0 33479 0 vsize: 134080 [startup+270.01 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 38964 0 0 0 26908 95 0 0 25 0 1 0 547447420 141467648 33180 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34538 33180 603 41 0 34497 0 vsize: 138152 [startup+280.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 40041 0 0 0 27906 97 0 0 25 0 1 0 547447420 145915904 34257 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35624 34257 603 41 0 35583 0 vsize: 142496 [startup+290.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 41271 0 0 0 28904 100 0 0 25 0 1 0 547447420 150843392 35487 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 36827 35487 603 41 0 36786 0 vsize: 147308 [startup+300.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 42517 0 0 0 29901 103 0 0 25 0 1 0 547447420 156053504 36733 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 38099 36733 603 41 0 38058 0 vsize: 152396 [startup+310.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 42951 0 0 0 30900 104 0 0 25 0 1 0 547447420 157728768 37167 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 38508 37167 603 41 0 38467 0 vsize: 154032 [startup+320.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 43805 0 0 0 31899 105 0 0 25 0 1 0 547447420 161333248 38021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39388 38021 603 41 0 39347 0 vsize: 157552 [startup+330.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 44383 0 0 0 32898 106 0 0 25 0 1 0 547447420 163799040 38599 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 39990 38599 603 41 0 39949 0 vsize: 159960 [startup+340.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 45179 0 0 0 33897 108 0 0 25 0 1 0 547447420 166973440 39395 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 40765 39395 603 41 0 40724 0 vsize: 163060 [startup+350.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 45940 0 0 0 34895 110 0 0 25 0 1 0 547447420 170168320 40156 4294967295 134512640 134672761 3221224544 3221223728 134616014 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 41545 40156 603 41 0 41504 0 vsize: 166180 [startup+360.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 46656 0 0 0 35893 112 0 0 25 0 1 0 547447420 173051904 40872 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 42249 40872 603 41 0 42208 0 vsize: 168996 [startup+370.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 47349 0 0 0 36891 114 0 0 25 0 1 0 547447420 175853568 41565 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 42933 41565 603 41 0 42892 0 vsize: 171732 [startup+380.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 48090 0 0 0 37889 116 0 0 25 0 1 0 547447420 178913280 42306 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 43680 42306 603 41 0 43639 0 vsize: 174720 [startup+390.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 48792 0 0 0 38887 119 0 0 25 0 1 0 547447420 181772288 43008 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 44378 43008 603 41 0 44337 0 vsize: 177512 [startup+400.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 49520 0 0 0 39885 121 0 0 25 0 1 0 547447420 184745984 43736 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 45104 43736 603 41 0 45063 0 vsize: 180416 [startup+410.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 50217 0 0 0 40884 122 0 0 25 0 1 0 547447420 187596800 44433 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 45800 44433 603 41 0 45759 0 vsize: 183200 [startup+420.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 51018 0 0 0 41883 123 0 0 25 0 1 0 547447420 190951424 45234 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 46619 45234 603 41 0 46578 0 vsize: 186476 [startup+430.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 51908 0 0 0 42881 125 0 0 25 0 1 0 547447420 194543616 46124 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 47496 46124 603 41 0 47455 0 vsize: 189984 [startup+440.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 52680 0 0 0 43879 127 0 0 25 0 1 0 547447420 197685248 46896 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 48263 46896 603 41 0 48222 0 vsize: 193052 [startup+450.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 53830 0 0 0 44877 129 0 0 25 0 1 0 547447420 202477568 48046 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 49433 48046 603 41 0 49392 0 vsize: 197732 [startup+460.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 54797 0 0 0 45876 130 0 0 25 0 1 0 547447420 206471168 49013 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 50408 49013 603 41 0 50367 0 vsize: 201632 [startup+470.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 55990 0 0 0 46874 132 0 0 25 0 1 0 547447420 211283968 50206 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 51583 50206 603 41 0 51542 0 vsize: 206332 [startup+480.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 56813 0 0 0 47872 134 0 0 25 0 1 0 547447420 214671360 51029 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 52410 51029 603 41 0 52369 0 vsize: 209640 [startup+490.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 57681 0 0 0 48871 136 0 0 25 0 1 0 547447420 218251264 51897 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 53284 51897 603 41 0 53243 0 vsize: 213136 [startup+500.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 58578 0 0 0 49870 137 0 0 25 0 1 0 547447420 221925376 52794 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 54181 52794 603 41 0 54140 0 vsize: 216724 [startup+510.012 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 59446 0 0 0 50868 140 0 0 25 0 1 0 547447420 225439744 53662 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 55039 53662 603 41 0 54998 0 vsize: 220156 [startup+520.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 60306 0 0 0 51866 141 0 0 25 0 1 0 547447420 229003264 54522 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 55909 54522 603 41 0 55868 0 vsize: 223636 [startup+530.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 61508 0 0 0 52864 143 0 0 25 0 1 0 547447420 233906176 55724 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 57106 55724 603 41 0 57065 0 vsize: 228424 [startup+540.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 62504 0 0 0 53863 145 0 0 25 0 1 0 547447420 237973504 56720 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 58099 56720 603 41 0 58058 0 vsize: 232396 [startup+550.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 63289 0 0 0 54862 146 0 0 25 0 1 0 547447420 241242112 57505 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 58897 57505 603 41 0 58856 0 vsize: 235588 [startup+560.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 63895 0 0 0 55860 148 0 0 25 0 1 0 547447420 243728384 58111 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 59504 58111 603 41 0 59463 0 vsize: 238016 [startup+570.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 64806 0 0 0 56858 150 0 0 25 0 1 0 547447420 247422976 59022 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 60406 59022 603 41 0 60365 0 vsize: 241624 [startup+580.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 65767 0 0 0 57857 152 0 0 25 0 1 0 547447420 251305984 59983 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 61354 59983 603 41 0 61313 0 vsize: 245416 [startup+590.013 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 66835 0 0 0 58855 154 0 0 25 0 1 0 547447420 255672320 61051 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 62420 61051 603 41 0 62379 0 vsize: 249680 [startup+600.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 67752 0 0 0 59853 156 0 0 25 0 1 0 547447420 259493888 61968 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 63353 61968 603 41 0 63312 0 vsize: 253412 [startup+610.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 68577 0 0 0 60851 158 0 0 25 0 1 0 547447420 262844416 62793 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 64171 62793 603 41 0 64130 0 vsize: 256684 [startup+620.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 69329 0 0 0 61851 158 0 0 25 0 1 0 547447420 265895936 63545 4294967295 134512640 134672761 3221224544 3221223728 134615538 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 64916 63545 603 41 0 64875 0 vsize: 259664 [startup+630.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 70341 0 0 0 62849 160 0 0 25 0 1 0 547447420 270086144 64557 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 65939 64557 603 41 0 65898 0 vsize: 263756 [startup+640.014 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 71313 0 0 0 63847 163 0 0 25 0 1 0 547447420 274014208 65529 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66898 65529 603 41 0 66857 0 vsize: 267592 [startup+650.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 72603 0 0 0 64845 165 0 0 25 0 1 0 547447420 279400448 66819 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68213 66819 603 41 0 68172 0 vsize: 272852 [startup+660.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 73694 0 0 0 65842 168 0 0 25 0 1 0 547447420 283865088 67910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 69303 67910 603 41 0 69262 0 vsize: 277212 [startup+670.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 74615 0 0 0 66840 170 0 0 25 0 1 0 547447420 287559680 68831 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 70205 68831 603 41 0 70164 0 vsize: 280820 [startup+680.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 75887 0 0 0 67838 173 0 0 25 0 1 0 547447420 292786176 70103 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 71481 70103 603 41 0 71440 0 vsize: 285924 [startup+690.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 76802 0 0 0 68836 175 0 0 25 0 1 0 547447420 296517632 71018 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 72392 71018 603 41 0 72351 0 vsize: 289568 [startup+700.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 77808 0 0 0 69835 176 0 0 25 0 1 0 547447420 300666880 72024 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 73405 72024 603 41 0 73364 0 vsize: 293620 [startup+710.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 78757 0 0 0 70832 179 0 0 25 0 1 0 547447420 304578560 72973 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 74360 72973 603 41 0 74319 0 vsize: 297440 [startup+720.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 79531 0 0 0 71830 181 0 0 25 0 1 0 547447420 307695616 73747 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 75121 73747 603 41 0 75080 0 vsize: 300484 [startup+730.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 80265 0 0 0 72828 184 0 0 25 0 1 0 547447420 310730752 74481 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 75862 74481 603 41 0 75821 0 vsize: 303448 [startup+740.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 81279 0 0 0 73825 186 0 0 25 0 1 0 547447420 314843136 75495 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 76866 75495 603 41 0 76825 0 vsize: 307464 [startup+750.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 82369 0 0 0 74824 188 0 0 25 0 1 0 547447420 319328256 76585 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 77961 76585 603 41 0 77920 0 vsize: 311844 [startup+760.015 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 83474 0 0 0 75822 190 0 0 25 0 1 0 547447420 323866624 77690 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 79069 77690 603 41 0 79028 0 vsize: 316276 [startup+770.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 84802 0 0 0 76820 192 0 0 25 0 1 0 547447420 329347072 79018 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 80407 79018 603 41 0 80366 0 vsize: 321628 [startup+780.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 85917 0 0 0 77817 195 0 0 25 0 1 0 547447420 333844480 80133 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 81505 80133 603 41 0 81464 0 vsize: 326020 [startup+790.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 86827 0 0 0 78816 196 0 0 25 0 1 0 547447420 337645568 81043 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 82433 81043 603 41 0 82392 0 vsize: 329732 [startup+800.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 87732 0 0 0 79814 198 0 0 25 0 1 0 547447420 341258240 81948 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83315 81948 603 41 0 83274 0 vsize: 333260 [startup+810.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 88381 0 0 0 80813 200 0 0 25 0 1 0 547447420 343916544 82597 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 83964 82597 603 41 0 83923 0 vsize: 335856 [startup+820.026 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 89140 0 0 0 81813 201 0 0 25 0 1 0 547447420 347049984 83356 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 84729 83356 603 41 0 84688 0 vsize: 338916 [startup+830.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 90212 0 0 0 82812 203 0 0 25 0 1 0 547447420 351526912 84428 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 85822 84428 603 41 0 85781 0 vsize: 343288 [startup+840.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 91114 0 0 0 83809 206 0 0 25 0 1 0 547447420 355143680 85330 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 86705 85330 603 41 0 86664 0 vsize: 346820 [startup+850.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 91707 0 0 0 84808 207 0 0 25 0 1 0 547447420 357617664 85923 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 87309 85923 603 41 0 87268 0 vsize: 349236 [startup+860.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 92043 0 0 0 85808 207 0 0 25 0 1 0 547447420 359014400 86259 4294967295 134512640 134672761 3221224544 3221223688 134616356 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 87650 86259 603 41 0 87609 0 vsize: 350600 [startup+870.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 92169 0 0 0 86808 208 0 0 25 0 1 0 547447420 359796736 86385 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 87841 86385 603 41 0 87800 0 vsize: 351364 [startup+880.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 92529 0 0 0 87807 209 0 0 25 0 1 0 547447420 361238528 86745 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 88193 86745 603 41 0 88152 0 vsize: 352772 [startup+890.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 92961 0 0 0 88807 209 0 0 25 0 1 0 547447420 363098112 87177 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 88647 87177 603 41 0 88606 0 vsize: 354588 [startup+900.032 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 93678 0 0 0 89806 210 0 0 25 0 1 0 547447420 366018560 87894 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 89360 87894 603 41 0 89319 0 vsize: 357440 [startup+910.032 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 94449 0 0 0 90804 212 0 0 25 0 1 0 547447420 369192960 88665 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 90135 88665 603 41 0 90094 0 vsize: 360540 [startup+920.032 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 94510 0 0 0 91805 212 0 0 25 0 1 0 547447420 369459200 88726 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 90200 88726 603 41 0 90159 0 vsize: 360800 [startup+930.033 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 95358 0 0 0 92803 214 0 0 25 0 1 0 547447420 372813824 89574 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 91019 89574 603 41 0 90978 0 vsize: 364076 [startup+940.033 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 96177 0 0 0 93802 215 0 0 25 0 1 0 547447420 376188928 90393 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 91843 90393 603 41 0 91802 0 vsize: 367372 [startup+950.033 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 96666 0 0 0 94801 216 0 0 25 0 1 0 547447420 378265600 90882 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 92350 90882 603 41 0 92309 0 vsize: 369400 [startup+960.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 97371 0 0 0 95801 217 0 0 25 0 1 0 547447420 381128704 91587 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 93049 91587 603 41 0 93008 0 vsize: 372196 [startup+970.035 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 97835 0 0 0 96800 218 0 0 25 0 1 0 547447420 383062016 92051 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 93521 92051 603 41 0 93480 0 vsize: 374084 [startup+980.036 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 98462 0 0 0 97798 219 0 0 25 0 1 0 547447420 385540096 92678 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 94126 92678 603 41 0 94085 0 vsize: 376504 [startup+990.035 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 99228 0 0 0 98797 221 0 0 25 0 1 0 547447420 388665344 93444 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 94889 93444 603 41 0 94848 0 vsize: 379556 [startup+1000.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 99671 0 0 0 99796 222 0 0 25 0 1 0 547447420 390496256 93887 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 95336 93887 603 41 0 95295 0 vsize: 381344 [startup+1010.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 100178 0 0 0 100795 223 0 0 25 0 1 0 547447420 392568832 94394 4294967295 134512640 134672761 3221224544 3221223584 134612827 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 95842 94394 603 41 0 95801 0 vsize: 383368 [startup+1020.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 100663 0 0 0 101795 224 0 0 25 0 1 0 547447420 394641408 94879 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 96348 94879 603 41 0 96307 0 vsize: 385392 [startup+1030.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 101316 0 0 0 102793 226 0 0 25 0 1 0 547447420 397230080 95532 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 96980 95532 603 41 0 96939 0 vsize: 387920 [startup+1040.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 101916 0 0 0 103791 228 0 0 25 0 1 0 547447420 399695872 96132 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 97582 96132 603 41 0 97541 0 vsize: 390328 [startup+1050.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 102535 0 0 0 104790 229 0 0 25 0 1 0 547447420 402276352 96751 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 98212 96751 603 41 0 98171 0 vsize: 392848 [startup+1060.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 103033 0 0 0 105789 230 0 0 25 0 1 0 547447420 404238336 97249 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 98691 97249 603 41 0 98650 0 vsize: 394764 [startup+1070.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 103492 0 0 0 106788 232 0 0 25 0 1 0 547447420 406192128 97708 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 99168 97708 603 41 0 99127 0 vsize: 396672 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 104287 0 0 0 107786 233 0 0 25 0 1 0 547447420 409423872 98503 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 99957 98503 603 41 0 99916 0 vsize: 399828 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 104896 0 0 0 108785 235 0 0 25 0 1 0 547447420 411926528 99112 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 100568 99112 603 41 0 100527 0 vsize: 402272 [startup+1100.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 105315 0 0 0 109785 235 0 0 25 0 1 0 547447420 413638656 99531 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 100986 99531 603 41 0 100945 0 vsize: 403944 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 105711 0 0 0 110784 236 0 0 25 0 1 0 547447420 415240192 99927 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 101377 99927 603 41 0 101336 0 vsize: 405508 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 106108 0 0 0 111783 237 0 0 25 0 1 0 547447420 416952320 100324 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 101795 100324 603 41 0 101754 0 vsize: 407180 [startup+1130.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 106418 0 0 0 112783 238 0 0 25 0 1 0 547447420 418127872 100634 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 102082 100634 603 41 0 102041 0 vsize: 408328 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 106610 0 0 0 113782 238 0 0 25 0 1 0 547447420 418918400 100826 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 102275 100826 603 41 0 102234 0 vsize: 409100 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 107038 0 0 0 114781 239 0 0 25 0 1 0 547447420 420745216 101254 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 102721 101254 603 41 0 102680 0 vsize: 410884 [startup+1160.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 107454 0 0 0 115780 241 0 0 25 0 1 0 547447420 422449152 101670 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 103137 101670 603 41 0 103096 0 vsize: 412548 [startup+1170.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 108155 0 0 0 116779 242 0 0 25 0 1 0 547447420 425271296 102371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 103826 102371 603 41 0 103785 0 vsize: 415304 [startup+1180.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 108675 0 0 0 117778 244 0 0 25 0 1 0 547447420 427360256 102891 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 104336 102891 603 41 0 104295 0 vsize: 417344 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 109179 0 0 0 118777 245 0 0 25 0 1 0 547447420 429436928 103395 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 104843 103395 603 41 0 104802 0 vsize: 419372 [startup+1200.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 11080 Raw data (stat): 11078 (minisat+) R 11077 27565 27564 0 -1 0 109869 0 0 0 119775 246 0 0 25 0 1 0 547447420 432250880 104085 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 105530 104085 603 41 0 105489 0 vsize: 422120 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.24 s] Raw data (loadavg): 0.99 0.97 0.93 1/54 11080 Raw data (stat): 11078 (minisat+) Z 11077 27565 27564 0 -1 12 109870 0 0 0 119775 266 0 0 25 0 1 0 547447420 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.24 CPU time (s): 1200.42 CPU user time (s): 1197.76 CPU system time (s): 2.66259 CPU usage (%): 100.015 Max. virtual memory (Kb): 422120 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####