Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-msc98-ip.opb |
MD5SUM | 7d35d9573399ce415b4927ac319735bc |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 2147483647 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 7440 |
Biggest coefficient in the objective function | 233453000000000000 |
Number of bits for the biggest coefficient in the objective function | 58 |
Sum of the numbers in the objective function | 7418790514839784695 |
Number of bits of the sum of numbers in the objective function | 63 |
Biggest number in a constraint | 233453000000000000 |
Number of bits of the biggest number in a constraint | 58 |
Biggest sum of numbers in a constraint | 7418790514839784695 |
Number of bits of the biggest sum of numbers | 63 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1274.48 |
Number of variables | 33385 |
Total number of constraints | 36969 |
Number of constraints which are clauses | 5133 |
Number of constraints which are cardinality constraints (but not clauses) | 20819 |
Number of constraints which are nor clauses,nor cardinality constraints | 11017 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 1209 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc24 THE 2005-05-25 22:32:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22552 boxname=wulflinc24 idbench=1368 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 7d35d9573399ce415b4927ac319735bc /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-msc98-ip.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-msc98-ip.opb IDLAUNCH: 22552 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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: 906920 kB Buffers: 25484 kB Cached: 79708 kB SwapCached: 616 kB Active: 25140 kB Inactive: 82152 kB HighTotal: 131008 kB HighFree: 73220 kB LowTotal: 903652 kB LowFree: 833700 kB SwapTotal: 2097892 kB SwapFree: 2096416 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5160 kB Slab: 14556 kB Committed_AS: 63660 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 22:53:27 (client local time) WITH STATUS 152 IN 1229.88 SECONDS stats: 22552 7 1229.88 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c PARSE ERROR! [line 21147] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 20863 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################ c -- Clauses(.)/Splits(s): s......sssssssssssssssssssss....................................sssssssssssss......................................ssssssssssss................................sssss...................................sssssssssssssss....................................sssssssssssssss...................................ssssss..................................sssssss..............................................................sss...............................sss...............................s..............................sssssssssss.................................ssssssssssssssssss...............................sss..............................s.................................ssssssssss................................ssssssssssssssssssss...............................sssssssssss................................ssssssssssssssss..............................ssss................................sss..............................ss...............................s..............................s..............................s..........................s............s........................s..........................................................................................s...............................................................................................................................................sssssss.......sss........s..............................sss...............................s...............................s....................................ssss......................s.......................s............s...............ss...........................................................ssssss...............................ss..............................ss..........................s...........................ss..................................................s.................................................s.............................................................................................s.....sssss..ss...............s.........................................................................sss.........................................................ss...................................................................ss...................s........s.............................................................................................................ss.....................ssssss..................................s............................................ssssssssssssssssss...............................s..............................................................................................sssssssssssss................................ssssssssssssssssss................................ssssssssss..............................s.................................................sss.................ss.......................................................................sssssssss.............................ssss......................................ssssssssssssss....................ss..........sssssssssss.................ssssss............ssssssssssssssssssssss..........................sssss.................sssssssssssss..........s...sss...........s................s..................................s................s................s..................ssssssssss....ssssssssssssssss..s.ss..ssss........s...................s..............ssssssssssssssssss............ss.........................s.....ssssssssssssssss..............s........sss............ssssssssss...............................ssssssssssssssssssssssssssssss..........................................sssssssss..........sss.........ssss.............ssss..........s....ss......sssssssss.........................sssssssss..........ssss.....sssssssssssssssssssssss.......s..................ssss.............sss.......ssss......s....................sssssssssssssssssssss..................................sssssssssssssssss....................................ssssssssss.................................ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss......................................................................................................................................................sssss..........................ss...............................s...........................ss.........................................ss.......................................sssssssssssss.................................ssss.......................................ssss..............................................sssss................................................ssss....................................sssss................................s........................ssssssssssss....................................ssssssss......................................sss.....................................ssssss...................................sss..........................................................................ssssssss.................................sss................................sssssssss...................................sss...............................sssssss..............................ss....................................sssssssssssssssssss.........................................sssss..................................ssssssss.....................................sss........................................sssssss................................s................................s...............................sss............................................................................................ssss.............................................................ssssssssssssssssssssssssss...........................sssssssssssssssssssss..............................sssssssssssssssssssssss..............................sssssssssssss..............................ssss..............................sss............................sssssssss..............................ssss.......................................................s.......................................s.......................................ss................................................................................................................................................................ssssssssssssssss....................................sss.....................................ssssssss..................................sss.......................... c ---[21783]---> BDD-cost: 7 c ---[21782]---> BDD-cost: 11 c ---[21781]---> BDD-cost: 12 c ---[21780]---> BDD-cost: 14 c ---[21779]---> BDD-cost: 11 c ---[21778]---> BDD-cost: 12 c ---[21777]---> BDD-cost: 14 c ---[21776]---> BDD-cost: 11 c ---[21775]---> BDD-cost: 12 c ---[21774]---> BDD-cost: 14 c ---[21773]---> BDD-cost: 11 c ---[21772]---> BDD-cost: 12 c ---[21771]---> BDD-cost: 14 c ---[21770]---> BDD-cost: 11 c ---[21769]---> BDD-cost: 12 c ---[21768]---> BDD-cost: 14 c ---[21767]---> BDD-cost: 11 c ---[21766]---> BDD-cost: 12 c ---[21765]---> BDD-cost: 14 c ---[21764]---> BDD-cost: 11 c ---[21763]---> BDD-cost: 12 c ---[21762]---> BDD-cost: 14 c ---[21761]---> BDD-cost: 11 c ---[21760]---> BDD-cost: 12 c ---[21759]---> BDD-cost: 14 c ---[21758]---> BDD-cost: 11 c ---[21757]---> BDD-cost: 12 c ---[21756]---> BDD-cost: 14 c ---[21755]---> BDD-cost: 11 c ---[21754]---> BDD-cost: 12 c ---[21753]---> BDD-cost: 14 c ---[21752]---> BDD-cost: 11 c ---[21751]---> BDD-cost: 12 c ---[21750]---> BDD-cost: 14 c ---[21749]---> BDD-cost: 11 c ---[21748]---> BDD-cost: 12 c ---[21747]---> BDD-cost: 14 c ---[21746]---> BDD-cost: 11 c ---[21745]---> BDD-cost: 12 c ---[21744]---> BDD-cost: 14 c ---[21743]---> BDD-cost: 11 c ---[21742]---> BDD-cost: 12 c ---[21741]---> BDD-cost: 14 c ---[21740]---> BDD-cost: 11 c ---[21739]---> BDD-cost: 12 c ---[21738]---> BDD-cost: 14 c ---[21737]---> BDD-cost: 11 c ---[21736]---> BDD-cost: 12 c ---[21735]---> BDD-cost: 14 c ---[21734]---> BDD-cost: 11 c ---[21733]---> BDD-cost: 12 c ---[21732]---> BDD-cost: 14 c ---[21731]---> BDD-cost: 11 c ---[21730]---> BDD-cost: 12 c ---[21729]---> BDD-cost: 14 c ---[21728]---> BDD-cost: 11 c ---[21727]---> BDD-cost: 12 c ---[21726]---> BDD-cost: 14 c ---[21725]---> BDD-cost: 11 c ---[21724]---> BDD-cost: 12 c ---[21723]---> BDD-cost: 14 c ---[21722]---> BDD-cost: 11 c ---[21721]---> BDD-cost: 12 c ---[21720]---> BDD-cost: 14 c ---[21719]---> BDD-cost: 11 c ---[21718]---> BDD-cost: 12 c ---[21717]---> BDD-cost: 14 c ---[21716]---> BDD-cost: 11 c ---[21715]---> BDD-cost: 12 c ---[21714]---> BDD-cost: 14 c ---[21713]---> BDD-cost: 7 c ---[21712]---> BDD-cost: 11 c ---[21711]---> BDD-cost: 12 c ---[21710]---> BDD-cost: 14 c ---[21709]---> BDD-cost: 11 c ---[21708]---> BDD-cost: 12 c ---[21707]---> BDD-cost: 14 c ---[21706]---> BDD-cost: 11 c ---[21705]---> BDD-cost: 12 c ---[21704]---> BDD-cost: 14 c ---[21703]---> BDD-cost: 11 c ---[21702]---> BDD-cost: 12 c ---[21701]---> BDD-cost: 14 c ---[21700]---> BDD-cost: 11 c ---[21699]---> BDD-cost: 12 c ---[21698]---> BDD-cost: 14 c ---[21697]---> BDD-cost: 11 c ---[21696]---> BDD-cost: 12 c ---[21695]---> BDD-cost: 14 c ---[21694]---> BDD-cost: 11 c ---[21693]---> BDD-cost: 12 c ---[21692]---> BDD-cost: 14 c ---[21691]---> BDD-cost: 11 c ---[21690]---> BDD-cost: 12 c ---[21689]---> BDD-cost: 14 c ---[21688]---> BDD-cost: 11 c ---[21687]---> BDD-cost: 12 c ---[21686]---> BDD-cost: 14 c ---[21685]---> BDD-cost: 11 c ---[21684]---> BDD-cost: 12 c ---[21683]---> BDD-cost: 14 c ---[21682]---> BDD-cost: 11 c ---[21681]---> BDD-cost: 12 c ---[21680]---> BDD-cost: 14 c ---[21679]---> BDD-cost: 11 c ---[21678]---> BDD-cost: 12 c ---[21677]---> BDD-cost: 14 c ---[21676]---> BDD-cost: 11 c ---[21675]---> BDD-cost: 12 c ---[21674]---> BDD-cost: 14 c ---[21673]---> BDD-cost: 11 c ---[21672]---> BDD-cost: 12 c ---[21671]---> BDD-cost: 14 c ---[21670]---> BDD-cost: 11 c ---[21669]---> BDD-cost: 12 c ---[21668]---> BDD-cost: 14 c ---[21667]---> BDD-cost: 11 c ---[21666]---> BDD-cost: 12 c ---[21665]---> BDD-cost: 14 c ---[21664]---> BDD-cost: 11 c ---[21663]---> BDD-cost: 12 c ---[21662]---> BDD-cost: 14 c ---[21661]---> BDD-cost: 11 c ---[21660]---> BDD-cost: 12 c ---[21659]---> BDD-cost: 14 c ---[21658]---> BDD-cost: 11 c ---[21657]---> BDD-cost: 12 c ---[21656]---> BDD-cost: 14 c ---[21655]---> BDD-cost: 11 c ---[21654]---> BDD-cost: 12 c ---[21653]---> BDD-cost: 14 c ---[21652]---> BDD-cost: 11 c ---[21651]---> BDD-cost: 12 c ---[21650]---> BDD-cost: 14 c ---[21649]---> BDD-cost: 11 c ---[21648]---> BDD-cost: 12 c ---[21647]---> BDD-cost: 14 c ---[21646]---> BDD-cost: 11 c ---[21645]---> BDD-cost: 12 c ---[21644]---> BDD-cost: 14 c ---[21643]---> BDD-cost: 11 c ---[21642]---> BDD-cost: 12 c ---[21641]---> BDD-cost: 14 c ---[21640]---> BDD-cost: 11 c ---[21639]---> BDD-cost: 12 c ---[21638]---> BDD-cost: 14 c ---[21637]---> BDD-cost: 11 c ---[21636]---> BDD-cost: 12 c ---[21635]---> BDD-cost: 14 c ---[21634]---> BDD-cost: 11 c ---[21633]---> BDD-cost: 12 c ---[21632]---> BDD-cost: 14 c ---[21631]---> BDD-cost: 11 c ---[21630]---> BDD-cost: 12 c ---[21629]---> BDD-cost: 14 c ---[21628]---> BDD-cost: 11 c ---[21627]---> BDD-cost: 12 c ---[21626]---> BDD-cost: 14 c ---[21625]---> BDD-cost: 11 c ---[21624]---> BDD-cost: 12 c ---[21623]---> BDD-cost: 14 c ---[21622]---> BDD-cost: 11 c ---[21621]---> BDD-cost: 12 c ---[21620]---> BDD-cost: 14 c ---[21619]---> BDD-cost: 11 c ---[21618]---> BDD-cost: 12 c ---[21617]---> BDD-cost: 14 c ---[21616]---> BDD-cost: 11 c ---[21615]---> BDD-cost: 12 c ---[21614]---> BDD-cost: 14 c ---[21613]---> BDD-cost: 11 c ---[21612]---> BDD-cost: 12 c ---[21611]---> BDD-cost: 14 c ---[21610]---> BDD-cost: 11 c ---[21609]---> BDD-cost: 12 c ---[21608]---> BDD-cost: 14 c ---[21607]---> BDD-cost: 11 c ---[21606]---> BDD-cost: 12 c ---[21605]---> BDD-cost: 14 c ---[21604]---> BDD-cost: 11 c ---[21603]---> BDD-cost: 12 c ---[21602]---> BDD-cost: 14 c ---[21601]---> BDD-cost: 11 c ---[21600]---> BDD-cost: 12 c ---[21599]---> BDD-cost: 14 c ---[21598]---> BDD-cost: 11 c ---[21597]---> BDD-cost: 12 c ---[21596]---> BDD-cost: 14 c ---[21595]---> BDD-cost: 11 c ---[21594]---> BDD-cost: 12 c ---[21593]---> BDD-cost: 14 c ---[21592]---> BDD-cost: 11 c ---[21591]---> BDD-cost: 12 c ---[21590]---> BDD-cost: 14 c ---[21589]---> BDD-cost: 11 c ---[21588]---> BDD-cost: 12 c ---[21587]---> BDD-cost: 14 c ---[21586]---> BDD-cost: 11 c ---[21585]---> BDD-cost: 12 c ---[21584]---> BDD-cost: 14 c ---[21583]---> BDD-cost: 11 c ---[21582]---> BDD-cost: 12 c ---[21581]---> BDD-cost: 14 c ---[21580]---> BDD-cost: 11 c ---[21579]---> BDD-cost: 12 c ---[21578]---> BDD-cost: 14 c ---[21577]---> BDD-cost: 11 c ---[21576]---> BDD-cost: 12 c ---[21575]---> BDD-cost: 14 c ---[21574]---> BDD-cost: 11 c ---[21573]---> BDD-cost: 12 c ---[21572]---> BDD-cost: 14 c ---[21571]---> BDD-cost: 11 c ---[21570]---> BDD-cost: 12 c ---[21569]---> BDD-cost: 14 c ---[21568]---> BDD-cost: 11 c ---[21567]---> BDD-cost: 12 c ---[21566]---> BDD-cost: 14 c ---[21565]---> BDD-cost: 11 c ---[21564]---> BDD-cost: 12 c ---[21563]---> BDD-cost: 14 c ---[21562]---> BDD-cost: 11 c ---[21561]---> BDD-cost: 12 c ---[21560]---> BDD-cost: 14 c ---[21559]---> BDD-cost: 11 c ---[21558]---> BDD-cost: 12 c ---[21557]---> BDD-cost: 14 c ---[21556]---> BDD-cost: 11 c ---[21555]---> BDD-cost: 12 c ---[21554]---> BDD-cost: 14 c ---[21553]---> BDD-cost: 11 c ---[21552]---> BDD-cost: 12 c ---[21551]---> BDD-cost: 14 c ---[21550]---> BDD-cost: 11 c ---[21549]---> BDD-cost: 12 c ---[21548]---> BDD-cost: 14 c ---[21547]---> BDD-cost: 11 c ---[21546]---> BDD-cost: 12 c ---[21545]---> BDD-cost: 14 c ---[21544]---> BDD-cost: 11 c ---[21543]---> BDD-cost: 12 c ---[21542]---> BDD-cost: 14 c ---[21541]---> BDD-cost: 11 c ---[21540]---> BDD-cost: 12 c ---[21539]---> BDD-cost: 14 c ---[21538]---> BDD-cost: 11 c ---[21537]---> BDD-cost: 12 c ---[21536]---> BDD-cost: 14 c ---[21535]---> BDD-cost: 11 c ---[21534]---> BDD-cost: 12 c ---[21533]---> BDD-cost: 14 c ---[21532]---> BDD-cost: 11 c ---[21531]---> BDD-cost: 12 c ---[21530]---> BDD-cost: 14 c ---[21529]---> BDD-cost: 11 c ---[21528]---> BDD-cost: 12 c ---[21527]---> BDD-cost: 14 c ---[21526]---> BDD-cost: 11 c ---[21525]---> BDD-cost: 12 c ---[21524]---> BDD-cost: 14 c ---[21523]---> BDD-cost: 11 c ---[21522]---> BDD-cost: 12 c ---[21521]---> BDD-cost: 14 c ---[21520]---> BDD-cost: 11 c ---[21519]---> BDD-cost: 12 c ---[21518]---> BDD-cost: 14 c ---[21517]---> BDD-cost: 11 c ---[21516]---> BDD-cost: 12 c ---[21515]---> BDD-cost: 14 c ---[21514]---> BDD-cost: 11 c ---[21513]---> BDD-cost: 12 c ---[21512]---> BDD-cost: 14 c ---[21511]---> BDD-cost: 11 c ---[21510]---> BDD-cost: 12 c ---[21509]---> BDD-cost: 14 c ---[21508]---> BDD-cost: 11 c ---[21507]---> BDD-cost: 12 c ---[21506]---> BDD-cost: 14 c ---[21505]---> BDD-cost: 11 c ---[21504]---> BDD-cost: 12 c ---[21503]---> BDD-cost: 14 c ---[21502]---> BDD-cost: 11 c ---[21501]---> BDD-cost: 12 c ---[21500]---> BDD-cost: 14 c ---[21499]---> BDD-cost: 11 c ---[21498]---> BDD-cost: 12 c ---[21497]---> BDD-cost: 14 c ---[21496]---> BDD-cost: 11 c ---[21495]---> BDD-cost: 12 c ---[21494]---> BDD-cost: 14 c ---[21493]---> BDD-cost: 11 c ---[21492]---> BDD-cost: 12 c ---[21491]---> BDD-cost: 14 c ---[21490]---> BDD-cost: 11 c ---[21489]---> BDD-cost: 12 c ---[21488]---> BDD-cost: 14 c ---[21487]---> BDD-cost: 11 c ---[21486]---> BDD-cost: 12 c ---[21485]---> BDD-cost: 14 c ---[21484]---> BDD-cost: 11 c ---[21483]---> BDD-cost: 12 c ---[21482]---> BDD-cost: 14 c ---[21481]---> BDD-cost: 11 c ---[21480]---> BDD-cost: 12 c ---[21479]---> BDD-cost: 14 c ---[21478]---> BDD-cost: 11 c ---[21477]---> BDD-cost: 12 c ---[21476]---> BDD-cost: 14 c ---[21475]---> BDD-cost: 11 c ---[21474]---> BDD-cost: 12 c ---[21473]---> BDD-cost: 14 c ---[21472]---> BDD-cost: 11 c ---[21471]---> BDD-cost: 12 c ---[21470]---> BDD-cost: 14 c ---[21469]---> BDD-cost: 11 c ---[21468]---> BDD-cost: 12 c ---[21467]---> BDD-cost: 14 c ---[21466]---> BDD-cost: 11 c ---[21465]---> BDD-cost: 12 c ---[21464]---> BDD-cost: 14 c ---[21463]---> BDD-cost: 11 c ---[21462]---> BDD-cost: 12 c ---[21461]---> BDD-cost: 14 c ---[21460]---> BDD-cost: 11 c ---[21459]---> BDD-cost: 12 c ---[21458]---> BDD-cost: 14 c ---[21457]---> BDD-cost: 11 c ---[21456]---> BDD-cost: 12 c ---[21455]---> BDD-cost: 14 c ---[21454]---> BDD-cost: 11 c ---[21453]---> BDD-cost: 12 c ---[21452]---> BDD-cost: 14 c ---[21451]---> BDD-cost: 11 c ---[21450]---> BDD-cost: 12 c ---[21449]---> BDD-cost: 14 c ---[21448]---> BDD-cost: 11 c ---[21447]---> BDD-cost: 12 c ---[21446]---> BDD-cost: 14 c ---[21445]---> BDD-cost: 11 c ---[21444]---> BDD-cost: 12 c ---[21443]---> BDD-cost: 14 c ---[21442]---> BDD-cost: 11 c ---[21441]---> BDD-cost: 12 c ---[21440]---> BDD-cost: 14 c ---[21439]---> BDD-cost: 11 c ---[21438]---> BDD-cost: 12 c ---[21437]---> BDD-cost: 14 c ---[21436]---> BDD-cost: 11 c ---[21435]---> BDD-cost: 12 c ---[21434]---> BDD-cost: 14 c ---[21433]---> BDD-cost: 11 c ---[21432]---> BDD-cost: 12 c ---[21431]---> BDD-cost: 14 c ---[21430]---> BDD-cost: 11 c ---[21429]---> BDD-cost: 12 c ---[21428]---> BDD-cost: 14 c ---[21427]---> BDD-cost: 11 c ---[21426]---> BDD-cost: 12 c ---[21425]---> BDD-cost: 14 c ---[21424]---> BDD-cost: 11 c ---[21423]---> BDD-cost: 12 c ---[21422]---> BDD-cost: 14 c ---[21421]---> BDD-cost: 11 c ---[21420]---> BDD-cost: 12 c ---[21419]---> BDD-cost: 14 c ---[21418]---> BDD-cost: 11 c ---[21417]---> BDD-cost: 12 c ---[21416]---> BDD-cost: 14 c ---[21415]---> BDD-cost: 11 c ---[21414]---> BDD-cost: 12 c ---[21413]---> BDD-cost: 14 c ---[21412]---> BDD-cost: 11 c ---[21411]---> BDD-cost: 12 c ---[21410]---> BDD-cost: 14 c ---[21409]---> BDD-cost: 11 c ---[21408]---> BDD-cost: 12 c ---[21407]---> BDD-cost: 14 c ---[21406]---> BDD-cost: 11 c ---[21405]---> BDD-cost: 12 c ---[21404]---> BDD-cost: 14 c ---[21403]---> BDD-cost: 11 c ---[21402]---> BDD-cost: 12 c ---[21401]---> BDD-cost: 14 c ---[21400]---> BDD-cost: 11 c ---[21399]---> BDD-cost: 12 c ---[21398]---> BDD-cost: 14 c ---[21397]---> BDD-cost: 11 c ---[21396]---> BDD-cost: 12 c ---[21395]---> BDD-cost: 14 c ---[21394]---> BDD-cost: 11 c ---[21393]---> BDD-cost: 12 c ---[21392]---> BDD-cost: 14 c ---[21391]---> BDD-cost: 11 c ---[21390]---> BDD-cost: 12 c ---[21389]---> BDD-cost: 14 c ---[21388]---> BDD-cost: 11 c ---[21387]---> BDD-cost: 12 c ---[21386]---> BDD-cost: 14 c ---[21385]---> BDD-cost: 11 c ---[21384]---> BDD-cost: 12 c ---[21383]---> BDD-cost: 14 c ---[21382]---> BDD-cost: 11 c ---[21381]---> BDD-cost: 12 c ---[21380]---> BDD-cost: 14 c ---[21379]---> BDD-cost: 11 c ---[21378]---> BDD-cost: 12 c ---[21377]---> BDD-cost: 14 c ---[21376]---> BDD-cost: 11 c ---[21375]---> BDD-cost: 12 c ---[21374]---> BDD-cost: 14 c ---[21373]---> BDD-cost: 11 c ---[21372]---> BDD-cost: 12 c ---[21371]---> BDD-cost: 14 c ---[21370]---> BDD-cost: 11 c ---[21369]---> BDD-cost: 12 c ---[21368]---> BDD-cost: 14 c ---[21367]---> BDD-cost: 11 c ---[21366]---> BDD-cost: 12 c ---[21365]---> BDD-cost: 14 c ---[21364]---> BDD-cost: 11 c ---[21363]---> BDD-cost: 12 c ---[21362]---> BDD-cost: 14 c ---[21361]---> BDD-cost: 11 c ---[21360]---> BDD-cost: 12 c ---[21359]---> BDD-cost: 14 c ---[21358]---> BDD-cost: 11 c ---[21357]---> BDD-cost: 12 c ---[21356]---> BDD-cost: 14 c ---[21355]---> BDD-cost: 11 c ---[21354]---> BDD-cost: 12 c ---[21353]---> BDD-cost: 14 c ---[21352]---> BDD-cost: 11 c ---[21351]---> BDD-cost: 12 c ---[21350]---> BDD-cost: 14 c ---[21349]---> BDD-cost: 11 c ---[21348]---> BDD-cost: 12 c ---[21347]---> BDD-cost: 14 c ---[21346]---> BDD-cost: 11 c ---[21345]---> BDD-cost: 12 c ---[21344]---> BDD-cost: 14 c ---[21343]---> BDD-cost: 11 c ---[21342]---> BDD-cost: 12 c ---[21341]---> BDD-cost: 14 c ---[21340]---> BDD-cost: 11 c ---[21339]---> BDD-cost: 12 c ---[21338]---> BDD-cost: 14 c ---[21337]---> BDD-cost: 11 c ---[21336]---> BDD-cost: 12 c ---[21335]---> BDD-cost: 14 c ---[21334]---> BDD-cost: 11 c ---[21333]---> BDD-cost: 12 c ---[21332]---> BDD-cost: 14 c ---[21331]---> BDD-cost: 11 c ---[21330]---> BDD-cost: 12 c ---[21329]---> BDD-cost: 14 c ---[21328]---> BDD-cost: 11 c ---[21327]---> BDD-cost: 12 c ---[21326]---> BDD-cost: 14 c ---[21325]---> BDD-cost: 11 c ---[21324]---> BDD-cost: 12 c ---[21323]---> BDD-cost: 14 c ---[21322]---> BDD-cost: 11 c ---[21321]---> BDD-cost: 12 c ---[21320]---> BDD-cost: 14 c ---[21319]---> BDD-cost: 11 c ---[21318]---> BDD-cost: 12 c ---[21317]---> BDD-cost: 14 c ---[21316]---> BDD-cost: 11 c ---[21315]---> BDD-cost: 12 c ---[21314]---> BDD-cost: 14 c ---[21313]---> BDD-cost: 11 c ---[21312]---> BDD-cost: 12 c ---[21311]---> BDD-cost: 14 c ---[21310]---> BDD-cost: 11 c ---[21309]---> BDD-cost: 12 c ---[21308]---> BDD-cost: 14 c ---[21307]---> BDD-cost: 11 c ---[21306]---> BDD-cost: 12 c ---[21305]---> BDD-cost: 14 c ---[21304]---> BDD-cost: 11 c ---[21303]---> BDD-cost: 12 c ---[21302]---> BDD-cost: 14 c ---[21301]---> BDD-cost: 11 c ---[21300]---> BDD-cost: 12 c ---[21299]---> BDD-cost: 14 c ---[21298]---> BDD-cost: 11 c ---[21297]---> BDD-cost: 12 c ---[21296]---> BDD-cost: 14 c ---[21295]---> BDD-cost: 11 c ---[21294]---> BDD-cost: 12 c ---[21293]---> BDD-cost: 14 c ---[21292]---> BDD-cost: 11 c ---[21291]---> BDD-cost: 12 c ---[21290]---> BDD-cost: 14 c ---[21289]---> BDD-cost: 11 c ---[21288]---> BDD-cost: 12 c ---[21287]---> BDD-cost: 14 c ---[21286]---> BDD-cost: 11 c ---[21285]---> BDD-cost: 12 c ---[21284]---> BDD-cost: 14 c ---[21283]---> BDD-cost: 11 c ---[21282]---> BDD-cost: 12 c ---[21281]---> BDD-cost: 14 c ---[21280]---> BDD-cost: 11 c ---[21279]---> BDD-cost: 12 c ---[21278]---> BDD-cost: 14 c ---[21277]---> BDD-cost: 11 c ---[21276]---> BDD-cost: 12 c ---[21275]---> BDD-cost: 14 c ---[21274]---> BDD-cost: 11 c ---[21273]---> BDD-cost: 12 c ---[21272]---> BDD-cost: 14 c ---[21271]---> BDD-cost: 11 c ---[21270]---> BDD-cost: 12 c ---[21269]---> BDD-cost: 14 c ---[21268]---> BDD-cost: 11 c ---[21267]---> BDD-cost: 12 c ---[21266]---> BDD-cost: 14 c ---[21265]---> BDD-cost: 11 c ---[21264]---> BDD-cost: 12 c ---[21263]---> BDD-cost: 14 c ---[21262]---> BDD-cost: 11 c ---[21261]---> BDD-cost: 12 c ---[21260]---> BDD-cost: 14 c ---[21259]---> BDD-cost: 11 c ---[21258]---> BDD-cost: 12 c ---[21257]---> BDD-cost: 14 c ---[21256]---> BDD-cost: 11 c ---[21255]---> BDD-cost: 12 c ---[21254]---> BDD-cost: 14 c ---[21253]---> BDD-cost: 11 c ---[21252]---> BDD-cost: 12 c ---[21251]---> BDD-cost: 14 c ---[21250]---> BDD-cost: 11 c ---[21249]---> BDD-cost: 12 c ---[21248]---> BDD-cost: 14 c ---[21247]---> BDD-cost: 11 c ---[21246]---> BDD-cost: 12 c ---[21245]---> BDD-cost: 14 c ---[21244]---> BDD-cost: 11 c ---[21243]---> BDD-cost: 12 c ---[21242]---> BDD-cost: 14 c ---[21241]---> BDD-cost: 11 c ---[21240]---> BDD-cost: 12 c ---[21239]---> BDD-cost: 14 c ---[21238]---> BDD-cost: 11 c ---[21237]---> BDD-cost: 12 c ---[21236]---> BDD-cost: 14 c ---[21235]---> BDD-cost: 11 c ---[21234]---> BDD-cost: 12 c ---[21233]---> BDD-cost: 14 c ---[21232]---> BDD-cost: 11 c ---[21231]---> BDD-cost: 12 c ---[21230]---> BDD-cost: 14 c ---[21229]---> BDD-cost: 11 c ---[21228]---> BDD-cost: 12 c ---[21227]---> BDD-cost: 14 c ---[21226]---> BDD-cost: 11 c ---[21225]---> BDD-cost: 12 c ---[21224]---> BDD-cost: 14 c ---[21223]---> BDD-cost: 11 c ---[21222]---> BDD-cost: 12 c ---[21221]---> BDD-cost: 14 c ---[21220]---> BDD-cost: 11 c ---[21219]---> BDD-cost: 12 c ---[21218]---> BDD-cost: 14 c ---[21217]---> BDD-cost: 11 c ---[21216]---> BDD-cost: 12 c ---[21215]---> BDD-cost: 14 c ---[21214]---> BDD-cost: 11 c ---[21213]---> BDD-cost: 12 c ---[21212]---> BDD-cost: 14 c ---[21211]---> BDD-cost: 11 c ---[21210]---> BDD-cost: 12 c ---[21209]---> BDD-cost: 14 c ---[21208]---> BDD-cost: 11 c ---[21207]---> BDD-cost: 12 c ---[21206]---> BDD-cost: 14 c ---[21205]---> BDD-cost: 11 c ---[21204]---> BDD-cost: 12 c ---[21203]---> BDD-cost: 14 c ---[21202]---> BDD-cost: 11 c ---[21201]---> BDD-cost: 12 c ---[21200]---> BDD-cost: 14 c ---[21199]---> BDD-cost: 11 c ---[21198]---> BDD-cost: 12 c ---[21197]---> BDD-cost: 14 c ---[21196]---> BDD-cost: 11 c ---[21195]---> BDD-cost: 12 c ---[21194]---> BDD-cost: 14 c ---[21193]---> BDD-cost: 11 c ---[21192]---> BDD-cost: 12 c ---[21191]---> BDD-cost: 14 c ---[21190]---> BDD-cost: 11 c ---[21189]---> BDD-cost: 12 c ---[21188]---> BDD-cost: 14 c ---[21187]---> BDD-cost: 11 c ---[21186]---> BDD-cost: 12 c ---[21185]---> BDD-cost: 14 c ---[21184]---> BDD-cost: 11 c ---[21183]---> BDD-cost: 12 c ---[21182]---> BDD-cost: 14 c ---[21181]---> BDD-cost: 11 c ---[21180]---> BDD-cost: 12 c ---[21179]---> BDD-cost: 14 c ---[21178]---> BDD-cost: 11 c ---[21177]---> BDD-cost: 12 c ---[21176]---> BDD-cost: 14 c ---[21175]---> BDD-cost: 11 c ---[21174]---> BDD-cost: 12 c ---[21173]---> BDD-cost: 14 c ---[21172]---> BDD-cost: 11 c ---[21171]---> BDD-cost: 12 c ---[21170]---> BDD-cost: 14 c ---[21169]---> BDD-cost: 11 c ---[21168]---> BDD-cost: 12 c ---[21167]---> BDD-cost: 14 c ---[21166]---> BDD-cost: 11 c ---[21165]---> BDD-cost: 12 c ---[21164]---> BDD-cost: 14 c ---[21163]---> BDD-cost: 11 c ---[21162]---> BDD-cost: 12 c ---[21161]---> BDD-cost: 14 c ---[21160]---> BDD-cost: 11 c ---[21159]---> BDD-cost: 12 c ---[21158]---> BDD-cost: 14 c ---[21157]---> BDD-cost: 11 c ---[21156]---> BDD-cost: 12 c ---[21155]---> BDD-cost: 14 c ---[21154]---> BDD-cost: 11 c ---[21153]---> BDD-cost: 12 c ---[21152]---> BDD-cost: 14 c ---[21151]---> BDD-cost: 11 c ---[21150]---> BDD-cost: 12 c ---[21149]---> BDD-cost: 14 c ---[21148]---> BDD-cost: 11 c ---[21147]---> BDD-cost: 12 c ---[21146]---> BDD-cost: 14 c ---[21145]---> BDD-cost: 11 c ---[21144]---> BDD-cost: 12 c ---[21143]---> BDD-cost: 14 c ---[21142]---> BDD-cost: 11 c ---[21141]---> BDD-cost: 12 c ---[21140]---> BDD-cost: 14 c ---[21139]---> BDD-cost: 11 c ---[21138]---> BDD-cost: 12 c ---[21137]---> BDD-cost: 14 c ---[21136]---> BDD-cost: 11 c ---[21135]---> BDD-cost: 12 c ---[21134]---> BDD-cost: 14 c ---[21133]---> BDD-cost: 11 c ---[21132]---> BDD-cost: 12 c ---[21131]---> BDD-cost: 14 c ---[21130]---> BDD-cost: 11 c ---[21129]---> BDD-cost: 12 c ---[21128]---> BDD-cost: 14 c ---[21127]---> BDD-cost: 11 c ---[21126]---> BDD-cost: 12 c ---[21125]---> BDD-cost: 14 c ---[21124]---> BDD-cost: 11 c ---[21123]---> BDD-cost: 12 c ---[21122]---> BDD-cost: 14 c ---[21121]---> BDD-cost: 11 c ---[21120]---> BDD-cost: 12 c ---[21119]---> BDD-cost: 14 c ---[21118]---> BDD-cost: 11 c ---[21117]---> BDD-cost: 12 c ---[21116]---> BDD-cost: 14 c ---[21115]---> BDD-cost: 11 c ---[21114]---> BDD-cost: 12 c ---[21113]---> BDD-cost: 14 c ---[21112]---> BDD-cost: 11 c ---[21111]---> BDD-cost: 12 c ---[21110]---> BDD-cost: 14 c ---[21109]---> BDD-cost: 11 c ---[21108]---> BDD-cost: 12 c ---[21107]---> BDD-cost: 14 c ---[21106]---> BDD-cost: 11 c ---[21105]---> BDD-cost: 12 c ---[21104]---> BDD-cost: 14 c ---[21103]---> BDD-cost: 11 c ---[21102]---> BDD-cost: 12 c ---[21101]---> BDD-cost: 14 c ---[21100]---> BDD-cost: 11 c ---[21099]---> BDD-cost: 12 c ---[21098]---> BDD-cost: 14 c ---[21097]---> BDD-cost: 11 c ---[21096]---> BDD-cost: 12 c ---[21095]---> BDD-cost: 14 c ---[21094]---> BDD-cost: 11 c ---[21093]---> BDD-cost: 12 c ---[21092]---> BDD-cost: 14 c ---[21091]---> BDD-cost: 11 c ---[21090]---> BDD-cost: 12 c ---[21089]---> BDD-cost: 14 c ---[21088]---> BDD-cost: 11 c ---[21087]---> BDD-cost: 12 c ---[21086]---> BDD-cost: 14 c ---[21085]---> BDD-cost: 11 c ---[21084]---> BDD-cost: 12 c ---[21083]---> BDD-cost: 14 c ---[21082]---> BDD-cost: 11 c ---[21081]---> BDD-cost: 12 c ---[21080]---> BDD-cost: 14 c ---[21079]---> BDD-cost: 11 c ---[21078]---> BDD-cost: 12 c ---[21077]---> BDD-cost: 14 c ---[21076]---> BDD-cost: 11 c ---[21075]---> BDD-cost: 12 c ---[21074]---> BDD-cost: 14 c ---[21073]---> BDD-cost: 11 c ---[21072]---> BDD-cost: 12 c ---[21071]---> BDD-cost: 14 c ---[21070]---> BDD-cost: 11 c ---[21069]---> BDD-cost: 12 c ---[21068]---> BDD-cost: 14 c ---[21067]---> BDD-cost: 11 c ---[21066]---> BDD-cost: 12 c ---[21065]---> BDD-cost: 14 c ---[21064]---> BDD-cost: 11 c ---[21063]---> BDD-cost: 12 c ---[21062]---> BDD-cost: 14 c ---[21061]---> BDD-cost: 11 c ---[21060]---> BDD-cost: 12 c ---[21059]---> BDD-cost: 14 c ---[21058]---> BDD-cost: 11 c ---[21057]---> BDD-cost: 12 c ---[21056]---> BDD-cost: 14 c ---[21055]---> BDD-cost: 11 c ---[21054]---> BDD-cost: 12 c ---[21053]---> BDD-cost: 14 c ---[21052]---> BDD-cost: 11 c ---[21051]---> BDD-cost: 12 c ---[21050]---> BDD-cost: 14 c ---[21049]---> BDD-cost: 11 c ---[21048]---> BDD-cost: 12 c ---[21047]---> BDD-cost: 14 c ---[21046]---> BDD-cost: 11 c ---[21045]---> BDD-cost: 12 c ---[21044]---> BDD-cost: 14 c ---[21043]---> BDD-cost: 11 c ---[21042]---> BDD-cost: 12 c ---[21041]---> BDD-cost: 14 c ---[21040]---> BDD-cost: 11 c ---[21039]---> BDD-cost: 12 c ---[21038]---> BDD-cost: 14 c ---[21037]---> BDD-cost: 11 c ---[21036]---> BDD-cost: 12 c ---[21035]---> BDD-cost: 14 c ---[21034]---> BDD-cost: 11 c ---[21033]---> BDD-cost: 12 c ---[21032]---> BDD-cost: 14 c ---[21031]---> BDD-cost: 11 c ---[21030]---> BDD-cost: 12 c ---[21029]---> BDD-cost: 14 c ---[21028]---> BDD-cost: 11 c ---[21027]---> BDD-cost: 12 c ---[21026]---> BDD-cost: 14 c ---[21025]---> BDD-cost: 11 c ---[21024]---> BDD-cost: 12 c ---[21023]---> BDD-cost: 14 c ---[21022]---> BDD-cost: 11 c ---[21021]---> BDD-cost: 12 c ---[21020]---> BDD-cost: 14 c ---[21019]---> BDD-cost: 11 c ---[21018]---> BDD-cost: 12 c ---[21017]---> BDD-cost: 14 c ---[21016]---> BDD-cost: 11 c ---[21015]---> BDD-cost: 12 c ---[21014]---> BDD-cost: 14 c ---[21013]---> BDD-cost: 11 c ---[21012]---> BDD-cost: 12 c ---[21011]---> BDD-cost: 14 c ---[21010]---> BDD-cost: 11 c ---[21009]---> BDD-cost: 12 c ---[21008]---> BDD-cost: 14 c ---[21007]---> BDD-cost: 11 c ---[21006]---> BDD-cost: 12 c ---[21005]---> BDD-cost: 14 c ---[21004]---> BDD-cost: 11 c ---[21003]---> BDD-cost: 12 c ---[21002]---> BDD-cost: 14 c ---[21001]---> BDD-cost: 11 c ---[21000]---> BDD-cost: 12 c ---[20999]---> BDD-cost: 14 c ---[20998]---> BDD-cost: 11 c ---[20997]---> BDD-cost: 12 c ---[20996]---> BDD-cost: 14 c ---[20995]---> BDD-cost: 11 c ---[20994]---> BDD-cost: 12 c ---[20993]---> BDD-cost: 14 c ---[20992]---> BDD-cost: 11 c ---[20991]---> BDD-cost: 12 c ---[20990]---> BDD-cost: 14 c ---[20989]---> BDD-cost: 11 c ---[20988]---> BDD-cost: 12 c ---[20987]---> BDD-cost: 14 c ---[20986]---> BDD-cost: 11 c ---[20985]---> BDD-cost: 12 c ---[20984]---> BDD-cost: 14 c ---[20983]---> BDD-cost: 11 c ---[20982]---> BDD-cost: 12 c ---[20981]---> BDD-cost: 14 c ---[20980]---> BDD-cost: 11 c ---[20979]---> BDD-cost: 12 c ---[20978]---> BDD-cost: 14 c ---[20977]---> BDD-cost: 11 c ---[20976]---> BDD-cost: 12 c ---[20975]---> BDD-cost: 14 c ---[20974]---> BDD-cost: 11 c ---[20973]---> BDD-cost: 12 c ---[20972]---> BDD-cost: 14 c ---[20971]---> BDD-cost: 11 c ---[20970]---> BDD-cost: 12 c ---[20969]---> BDD-cost: 14 c ---[20968]---> BDD-cost: 11 c ---[20967]---> BDD-cost: 12 c ---[20966]---> BDD-cost: 14 c ---[20965]---> BDD-cost: 11 c ---[20964]---> BDD-cost: 12 c ---[20963]---> BDD-cost: 14 c ---[20962]---> BDD-cost: 11 c ---[20961]---> BDD-cost: 12 c ---[20960]---> BDD-cost: 14 c ---[20959]---> BDD-cost: 11 c ---[20958]---> BDD-cost: 12 c ---[20957]---> BDD-cost: 14 c ---[20956]---> BDD-cost: 11 c ---[20955]---> BDD-cost: 12 c ---[20954]---> BDD-cost: 14 c ---[20899]---> BDD-cost: 20 c ---[20897]---> BDD-cost: 3 c ---[20896]---> Sorter-cost: 3228 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[20895]---> BDD-cost: 3 c ---[20890]---> BDD-cost: 11 c ---[20889]---> BDD-cost: 7 c ---[20887]---> BDD-cost: 7 c ---[20886]---> BDD-cost: 5 c ---[20885]---> BDD-cost: 5 c ---[20884]---> BDD-cost: 3 c ---[20883]---> BDD-cost: 7 c ---[20882]---> BDD-cost: 7 c ---[20880]---> Sorter-cost: 505 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20879]---> BDD-cost: 5 c ---[20878]---> Sorter-cost: 326 Base: 2 2 2 2 2 2 2 2 2 2 3 c ---[20877]---> Sorter-cost: 279 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20876]---> BDD-cost: 24 c ---[20875]---> Sorter-cost: 371 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20874]---> Sorter-cost: 356 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20873]---> BDD-cost: 3 c ---[20872]---> Sorter-cost: 310 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[20871]---> Sorter-cost: 218 Base: 2 2 2 2 2 2 2 2 2 3 c ---[20870]---> Sorter-cost: 389 Base: 2 2 2 2 2 2 2 2 2 2 11 c ---[20868]---> Sorter-cost: 315 Base: 2 2 2 2 2 2 2 2 2 13 c ---[20867]---> Sorter-cost: 754 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[20866]---> Sorter-cost: 213 Base: 2 2 2 2 2 2 2 2 2 2 c ---[20865]---> Sorter-cost: 703 Base: 2 2 2 2 2 2 2 2 2 2 2 3 c ---[20863]---> BDD-cost: 6 c ---[20862]---> BDD-cost: 3 c ---[20851]---> BDD-cost: 3 c ---[20849]---> BDD-cost: 133 c ---[20848]---> BDD-cost: 29 c ---[20844]---> BDD-cost: 13 c ---[20843]---> Sorter-cost: 358 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20840]---> BDD-cost: 3 c ---[20839]---> BDD-cost: 36 c ---[20837]---> Sorter-cost: 374 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20836]---> BDD-cost: 14 c ---[20835]---> BDD-cost: 30 c ---[20832]---> BDD-cost: 6 c ---[20829]---> BDD-cost: 3 c ---[20818]---> BDD-cost: 3 c ---[20807]---> BDD-cost: 3 c ---[20798]---> BDD-cost: 3 c ---[20797]---> BDD-cost: 7 c ---[20796]---> BDD-cost: 3 c ---[20793]---> BDD-cost: 5 c ---[20789]---> BDD-cost: 11 c ---[20788]---> BDD-cost: 5 c ---[20786]---> BDD-cost: 5 c ---[20785]---> Sorter-cost: 3185 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[20784]---> BDD-cost: 3 c ---[20783]---> BDD-cost: 7 c ---[20782]---> BDD-cost: 7 c ---[20781]---> BDD-cost: 5 c ---[20780]---> BDD-cost: 6 c ---[20779]---> Sorter-cost: 412 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20777]---> Sorter-cost: 212 Base: 2 2 2 2 2 2 2 2 2 2 c ---[20776]---> Sorter-cost: 230 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[20775]---> Sorter-cost: 307 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20774]---> Sorter-cost: 679 Base: 2 2 2 2 2 2 2 2 2 2 3 c ---[20773]---> BDD-cost: 3 c ---[20772]---> Sorter-cost: 366 Base: 2 2 2 2 2 2 2 2 2 3 c ---[20771]---> Sorter-cost: 536 Base: 2 2 2 2 2 2 2 2 2 2 3 c ---[20770]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20769]---> BDD-cost: 13 c ---[20768]---> Sorter-cost: 993 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20767]---> Sorter-cost: 210 Base: 2 2 2 2 2 2 2 2 2 3 c ---[20766]---> Sorter-cost: 227 Base: 2 2 2 2 2 2 2 2 2 3 c ---[20764]---> BDD-cost: 74 c ---[20763]---> Sorter-cost: 658 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20762]---> BDD-cost: 3 c ---[20761]---> BDD-cost: 72 c ---[20760]---> BDD-cost: 6 c ---[20759]---> BDD-cost: 6 c ---[20757]---> BDD-cost: 70 c ---[20756]---> BDD-cost: 81 c ---[20755]---> BDD-cost: 55 c ---[20754]---> BDD-cost: 56 c ---[20752]---> BDD-cost: 46 c ---[20751]---> BDD-cost: 3 c ---[20749]---> BDD-cost: 13 c ---[20747]---> Sorter-cost: 655 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20746]---> BDD-cost: 17 c ---[20742]---> BDD-cost: 72 c ---[20740]---> BDD-cost: 3 c ---[20739]---> BDD-cost: 55 c ---[20738]---> BDD-cost: 16 c ---[20737]---> BDD-cost: 117 c ---[20733]---> BDD-cost: 72 c ---[20729]---> BDD-cost: 3 c ---[20718]---> BDD-cost: 3 c ---[20707]---> BDD-cost: 3 c ---[20699]---> BDD-cost: 5 c ---[20697]---> BDD-cost: 5 c ---[20696]---> BDD-cost: 3 c ---[20695]---> BDD-cost: 5 c ---[20694]---> BDD-cost: 5 c ---[20693]---> BDD-cost: 5 c ---[20692]---> BDD-cost: 5 c ---[20691]---> BDD-cost: 5 c ---[20689]---> BDD-cost: 11 c ---[20685]---> BDD-cost: 3 c ---[20683]---> BDD-cost: 8 c ---[20680]---> BDD-cost: 5 c ---[20679]---> BDD-cost: 25 c ---[20678]---> Sorter-cost: 419 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20677]---> BDD-cost: 5 c ---[20676]---> Sorter-cost: 225 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20675]---> Sorter-cost: 240 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20674]---> Sorter-cost: 3185 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[20673]---> BDD-cost: 3 c ---[20671]---> BDD-cost: 20 c ---[20670]---> Sorter-cost: 368 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20669]---> BDD-cost: 25 c ---[20668]---> Sorter-cost: 233 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20667]---> Sorter-cost: 51 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20666]---> Sorter-cost: 321 Base: 2 2 2 2 2 2 2 2 2 2 3 c ---[20664]---> BDD-cost: 30 c ---[20663]---> Sorter-cost: 318 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20662]---> BDD-cost: 3 c ---[20661]---> Sorter-cost: 46 Base: 2 2 2 2 2 2 2 2 2 3 c ---[20660]---> Sorter-cost: 225 Base: 2 2 2 2 2 2 2 2 2 2 c ---[20659]---> Sorter-cost: 230 Base: 2 2 2 2 2 2 2 2 2 2 c ---[20658]---> Sorter-cost: 703 Base: 2 2 2 2 2 2 2 2 2 2 2 3 c ---[20657]---> Sorter-cost: 704 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20656]---> Sorter-cost: 623 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20655]---> BDD-cost: 14 c ---[20654]---> BDD-cost: 14 c ---[20652]---> BDD-cost: 112 c ---[20651]---> BDD-cost: 3 c ---[20650]---> BDD-cost: 6 c ---[20649]---> Sorter-cost: 849 Base: 2 2 2 2 2 2 2 2 3 5 c ---[20646]---> BDD-cost: 41 c ---[20643]---> BDD-cost: 8 c ---[20642]---> BDD-cost: 11 c ---[20640]---> BDD-cost: 3 c ---[20639]---> BDD-cost: 6 c ---[20637]---> BDD-cost: 91 c ---[20636]---> BDD-cost: 6 c ---[20635]---> BDD-cost: 25 c ---[20634]---> Sorter-cost: 279 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20633]---> Sorter-cost: 238 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20632]---> Sorter-cost: 275 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20631]---> BDD-cost: 51 c ---[20629]---> BDD-cost: 3 c ---[20628]---> Sorter-cost: 460 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20627]---> Sorter-cost: 432 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20626]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20625]---> BDD-cost: 6 c ---[20618]---> BDD-cost: 3 c ---[20607]---> BDD-cost: 3 c ---[20596]---> BDD-cost: 3 c ---[20588]---> BDD-cost: 8 c ---[20586]---> BDD-cost: 5 c ---[20585]---> BDD-cost: 3 c ---[20584]---> BDD-cost: 5 c ---[20583]---> BDD-cost: 9 c ---[20582]---> BDD-cost: 3 c ---[20581]---> BDD-cost: 5 c ---[20580]---> BDD-cost: 10 c ---[20579]---> BDD-cost: 18 c ---[20578]---> BDD-cost: 10 c ---[20577]---> BDD-cost: 16 c ---[20575]---> Sorter-cost: 243 Base: 2 2 2 2 2 2 2 2 2 7 c ---[20574]---> BDD-cost: 3 c ---[20573]---> BDD-cost: 66 c ---[20572]---> Sorter-cost: 267 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20571]---> Sorter-cost: 250 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20570]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 11 c ---[20569]---> Sorter-cost: 359 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20568]---> Sorter-cost: 521 Base: 2 2 2 2 2 2 2 2 2 2 2 3 c ---[20567]---> Sorter-cost: 192 Base: 2 2 2 2 2 2 2 2 2 3 c ---[20566]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 5 c ---[20565]---> Sorter-cost: 617 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20564]---> BDD-cost: 75 c ---[20563]---> Sorter-cost: 3185 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[20562]---> BDD-cost: 3 c ---[20561]---> Sorter-cost: 366 Base: 2 2 2 2 2 2 2 2 2 3 c ---[20560]---> BDD-cost: 5 c ---[20558]---> BDD-cost: 63 c ---[20556]---> BDD-cost: 4 c ---[20555]---> Sorter-cost: 601 Base: 2 2 2 2 2 2 2 2 2 2 3 c ---[20554]---> BDD-cost: 4 c ---[20553]---> BDD-cost: 29 c ---[20551]---> BDD-cost: 3 c ---[20550]---> BDD-cost: 11 c ---[20549]---> BDD-cost: 11 c ---[20548]---> BDD-cost: 72 c ---[20547]---> BDD-cost: 20 c ---[20546]---> Sorter-cost: 241 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20545]---> BDD-cost: 8 c ---[20543]---> BDD-cost: 37 c ---[20542]---> BDD-cost: 3 c ---[20541]---> BDD-cost: 6 c ---[20540]---> BDD-cost: 3 c ---[20539]---> BDD-cost: 6 c ---[20538]---> Sorter-cost: 430 Base: 2 2 2 2 2 2 2 2 2 3 5 c ---[20537]---> Sorter-cost: 507 Base: 2 2 2 2 2 2 2 2 2 3 5 c ---[20536]---> BDD-cost: 29 c ---[20535]---> Sorter-cost: 312 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20534]---> Sorter-cost: 320 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20533]---> Sorter-cost: 155 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20532]---> BDD-cost: 90 c ---[20531]---> Sorter-cost: 420 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20530]---> BDD-cost: 99 c ---[20529]---> BDD-cost: 3 c ---[20528]---> BDD-cost: 58 c ---[20518]---> BDD-cost: 3 c ---[20507]---> BDD-cost: 3 c ---[20496]---> BDD-cost: 3 c ---[20494]---> BDD-cost: 8 c ---[20493]---> BDD-cost: 5 c ---[20492]---> BDD-cost: 5 c ---[20491]---> BDD-cost: 7 c ---[20490]---> BDD-cost: 5 c ---[20487]---> BDD-cost: 3 c ---[20485]---> BDD-cost: 3 c ---[20484]---> BDD-cost: 8 c ---[20482]---> BDD-cost: 7 c ---[20481]---> BDD-cost: 9 c ---[20479]---> BDD-cost: 9 c ---[20478]---> BDD-cost: 13 c ---[20477]---> Sorter-cost: 456 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20476]---> BDD-cost: 70 c ---[20475]---> BDD-cost: 83 c ---[20474]---> BDD-cost: 3 c ---[20473]---> BDD-cost: 46 c ---[20472]---> BDD-cost: 10 c ---[20471]---> BDD-cost: 13 c ---[20468]---> BDD-cost: 13 c ---[20466]---> BDD-cost: 13 c ---[20464]---> BDD-cost: 25 c ---[20463]---> BDD-cost: 3 c ---[20462]---> BDD-cost: 62 c ---[20460]---> BDD-cost: 61 c ---[20459]---> Sorter-cost: 434 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20458]---> BDD-cost: 22 c ---[20457]---> Sorter-cost: 351 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20452]---> Sorter-cost: 3185 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[20451]---> BDD-cost: 3 c ---[20448]---> BDD-cost: 13 c ---[20446]---> BDD-cost: 13 c ---[20445]---> BDD-cost: 38 c ---[20444]---> Sorter-cost: 328 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20441]---> BDD-cost: 26 c ---[20440]---> BDD-cost: 3 c ---[20429]---> BDD-cost: 3 c ---[20418]---> BDD-cost: 3 c ---[20407]---> BDD-cost: 3 c ---[20405]---> BDD-cost: 13 c ---[20404]---> BDD-cost: 7 c ---[20403]---> BDD-cost: 11 c ---[20402]---> BDD-cost: 9 c ---[20401]---> BDD-cost: 11 c ---[20400]---> BDD-cost: 5 c ---[20399]---> BDD-cost: 8 c ---[20397]---> BDD-cost: 3 c ---[20396]---> BDD-cost: 3 c ---[20395]---> BDD-cost: 8 c ---[20394]---> BDD-cost: 5 c ---[20393]---> BDD-cost: 5 c ---[20392]---> BDD-cost: 5 c ---[20389]---> BDD-cost: 5 c ---[20387]---> BDD-cost: 8 c ---[20385]---> BDD-cost: 3 c ---[20383]---> BDD-cost: 8 c ---[20382]---> BDD-cost: 5 c ---[20381]---> BDD-cost: 5 c ---[20380]---> Sorter-cost: 473 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[20379]---> BDD-cost: 54 c ---[20378]---> BDD-cost: 34 c ---[20374]---> BDD-cost: 3 c ---[20372]---> BDD-cost: 5 c ---[20371]---> BDD-cost: 28 c ---[20370]---> Sorter-cost: 255 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20369]---> Sorter-cost: 670 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20364]---> BDD-cost: 35 c ---[20363]---> BDD-cost: 3 c ---[20362]---> BDD-cost: 25 c ---[20361]---> BDD-cost: 20 c ---[20358]---> BDD-cost: 5 c ---[20353]---> BDD-cost: 39 c ---[20352]---> BDD-cost: 3 c ---[20351]---> BDD-cost: 34 c ---[20349]---> BDD-cost: 14 c ---[20348]---> BDD-cost: 12 c ---[20347]---> BDD-cost: 32 c ---[20346]---> BDD-cost: 107 c ---[20345]---> Sorter-cost: 378 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20344]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20341]---> Sorter-cost: 3185 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[20340]---> BDD-cost: 3 c ---[20329]---> BDD-cost: 3 c ---[20318]---> BDD-cost: 3 c ---[20308]---> BDD-cost: 5 c ---[20307]---> BDD-cost: 3 c ---[20305]---> BDD-cost: 8 c ---[20304]---> BDD-cost: 9 c ---[20302]---> BDD-cost: 8 c ---[20301]---> BDD-cost: 7 c ---[20300]---> BDD-cost: 5 c ---[20299]---> BDD-cost: 5 c ---[20298]---> BDD-cost: 5 c ---[20297]---> BDD-cost: 5 c ---[20296]---> BDD-cost: 3 c ---[20294]---> BDD-cost: 9 c ---[20293]---> BDD-cost: 5 c ---[20292]---> BDD-cost: 5 c ---[20290]---> BDD-cost: 5 c ---[20289]---> BDD-cost: 51 c ---[20288]---> BDD-cost: 8 c ---[20287]---> BDD-cost: 41 c ---[20286]---> Sorter-cost: 371 Base: 2 2 2 2 2 2 2 2 2 2 2 3 c ---[20285]---> BDD-cost: 3 c ---[20284]---> BDD-cost: 19 c ---[20282]---> BDD-cost: 15 c ---[20281]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20277]---> BDD-cost: 35 c ---[20275]---> BDD-cost: 12 c ---[20274]---> BDD-cost: 3 c ---[20273]---> BDD-cost: 11 c ---[20272]---> BDD-cost: 4 c ---[20271]---> BDD-cost: 38 c ---[20270]---> BDD-cost: 4 c ---[20269]---> BDD-cost: 7 c ---[20263]---> BDD-cost: 3 c ---[20252]---> BDD-cost: 3 c ---[20241]---> BDD-cost: 3 c ---[20234]---> BDD-cost: 9 c ---[20233]---> BDD-cost: 8 c ---[20231]---> BDD-cost: 5 c ---[20230]---> Sorter-cost: 3185 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[20229]---> BDD-cost: 3 c ---[20227]---> BDD-cost: 5 c ---[20226]---> BDD-cost: 8 c ---[20225]---> BDD-cost: 9 c ---[20224]---> BDD-cost: 7 c ---[20223]---> BDD-cost: 5 c ---[20222]---> BDD-cost: 5 c ---[20221]---> BDD-cost: 5 c ---[20220]---> BDD-cost: 11 c ---[20218]---> BDD-cost: 3 c ---[20216]---> BDD-cost: 5 c ---[20215]---> BDD-cost: 6 c ---[20214]---> BDD-cost: 5 c ---[20213]---> BDD-cost: 5 c ---[20212]---> BDD-cost: 5 c ---[20211]---> BDD-cost: 41 c ---[20210]---> BDD-cost: 74 c ---[20208]---> BDD-cost: 16 c ---[20207]---> BDD-cost: 3 c ---[20206]---> BDD-cost: 6 c ---[20203]---> BDD-cost: 19 c ---[20202]---> BDD-cost: 14 c ---[20200]---> BDD-cost: 10 c ---[20197]---> BDD-cost: 10 c ---[20196]---> BDD-cost: 3 c ---[20185]---> BDD-cost: 3 c ---[20174]---> BDD-cost: 3 c ---[20163]---> BDD-cost: 3 c ---[20161]---> BDD-cost: 5 c ---[20160]---> BDD-cost: 3 c ---[20159]---> BDD-cost: 5 c ---[20158]---> BDD-cost: 3 c ---[20157]---> BDD-cost: 7 c ---[20156]---> BDD-cost: 5 c ---[20155]---> BDD-cost: 5 c ---[20154]---> BDD-cost: 5 c ---[20153]---> BDD-cost: 5 c ---[20152]---> BDD-cost: 3 c ---[20151]---> BDD-cost: 6 c ---[20150]---> BDD-cost: 5 c ---[20148]---> BDD-cost: 8 c ---[20147]---> BDD-cost: 72 c ---[20146]---> Sorter-cost: 195 Base: 2 2 2 2 2 2 2 2 2 2 c ---[20145]---> BDD-cost: 14 c ---[20144]---> BDD-cost: 17 c ---[20141]---> BDD-cost: 3 c ---[20130]---> BDD-cost: 3 c ---[20119]---> Sorter-cost: 3185 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[20118]---> BDD-cost: 3 c ---[20109]---> BDD-cost: 6 c ---[20108]---> BDD-cost: 17 c ---[20107]---> BDD-cost: 3 c ---[20106]---> BDD-cost: 9 c ---[20105]---> BDD-cost: 5 c ---[20104]---> BDD-cost: 5 c ---[20102]---> BDD-cost: 5 c ---[20101]---> BDD-cost: 5 c ---[20100]---> BDD-cost: 5 c ---[20099]---> BDD-cost: 9 c ---[20098]---> BDD-cost: 3 c ---[20097]---> BDD-cost: 3 c ---[20096]---> BDD-cost: 3 c ---[20095]---> BDD-cost: 5 c ---[20094]---> BDD-cost: 3 c ---[20093]---> BDD-cost: 5 c ---[20092]---> BDD-cost: 8 c ---[20091]---> BDD-cost: 9 c ---[20090]---> BDD-cost: 3 c ---[20089]---> BDD-cost: 16 c ---[20088]---> Sorter-cost: 243 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20086]---> Sorter-cost: 273 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20085]---> BDD-cost: 3 c ---[20084]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[20083]---> BDD-cost: 27 c ---[20082]---> BDD-cost: 84 c ---[20081]---> BDD-cost: 13 c ---[20080]---> BDD-cost: 31 c ---[20078]---> BDD-cost: 12 c ---[20077]---> BDD-cost: 9 c ---[20076]---> BDD-cost: 4 c ---[20075]---> BDD-cost: 18 c ---[20074]---> BDD-cost: 3 c ---[20073]---> BDD-cost: 5 c ---[20072]---> BDD-cost: 25 c ---[20071]---> Sorter-cost: 191 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20070]---> Sorter-cost: 478 Base: 2 2 2 2 2 2 2 2 2 2 2 3 c ---[20069]---> Sorter-cost: 315 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[20068]---> BDD-cost: 107 c ---[20066]---> BDD-cost: 17 c ---[20063]---> BDD-cost: 3 c ---[20052]---> BDD-cost: 3 c ---[20041]---> BDD-cost: 3 c ---[20032]---> BDD-cost: 8 c ---[20030]---> BDD-cost: 3 c ---[20029]---> BDD-cost: 5 c ---[20028]---> BDD-cost: 5 c ---[20027]---> BDD-cost: 5 c ---[20026]---> BDD-cost: 5 c ---[20025]---> BDD-cost: 5 c ---[20024]---> BDD-cost: 5 c ---[20023]---> BDD-cost: 3 c ---[20022]---> BDD-cost: 9 c ---[20021]---> BDD-cost: 5 c ---[20020]---> BDD-cost: 11 c ---[20019]---> BDD-cost: 3 c ---[20018]---> BDD-cost: 68 c ---[20017]---> Sorter-cost: 205 Base: 2 2 2 2 2 2 2 2 2 3 c ---[20016]---> BDD-cost: 69 c ---[20014]---> BDD-cost: 6 c ---[20013]---> BDD-cost: 45 c ---[20011]---> Sorter-cost: 344 Base: 2 2 2 2 2 2 2 2 2 2 2 3 c ---[20010]---> BDD-cost: 35 c ---[20008]---> Sorter-cost: 3185 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[20007]---> BDD-cost: 3 c ---[19996]---> BDD-cost: 3 c ---[19985]---> BDD-cost: 3 c ---[19974]---> BDD-cost: 3 c ---[19973]---> BDD-cost: 9 c ---[19972]---> BDD-cost: 3 c ---[19971]---> BDD-cost: 5 c ---[19970]---> BDD-cost: 9 c ---[19968]---> BDD-cost: 5 c ---[19967]---> Sorter-cost: 175 Base: 2 2 2 2 2 2 2 2 2 2 c ---[19966]---> Sorter-cost: 171 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19965]---> BDD-cost: 50 c ---[19964]---> BDD-cost: 14 c ---[19963]---> BDD-cost: 3 c ---[19961]---> Sorter-cost: 213 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19952]---> BDD-cost: 3 c ---[19941]---> BDD-cost: 3 c ---[19930]---> BDD-cost: 3 c ---[19927]---> BDD-cost: 5 c ---[19926]---> BDD-cost: 5 c ---[19925]---> BDD-cost: 63 c ---[19923]---> Sorter-cost: 603 Base: 2 2 2 2 2 2 2 2 2 2 3 c ---[19922]---> Sorter-cost: 523 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19921]---> BDD-cost: 3 c ---[19920]---> BDD-cost: 14 c ---[19919]---> BDD-cost: 3 c ---[19917]---> Sorter-cost: 352 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19916]---> BDD-cost: 88 c ---[19915]---> BDD-cost: 5 c ---[19913]---> BDD-cost: 33 c ---[19912]---> Sorter-cost: 246 Base: 2 2 2 2 2 2 2 2 2 3 c ---[19911]---> Sorter-cost: 225 Base: 2 2 2 2 2 2 2 2 2 3 c ---[19910]---> BDD-cost: 7 c ---[19908]---> BDD-cost: 3 c ---[19905]---> BDD-cost: 49 c ---[19904]---> BDD-cost: 10 c ---[19902]---> BDD-cost: 43 c ---[19901]---> BDD-cost: 68 c ---[19900]---> BDD-cost: 49 c ---[19899]---> BDD-cost: 86 c ---[19897]---> Sorter-cost: 3185 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[19896]---> BDD-cost: 3 c ---[19895]---> BDD-cost: 51 c ---[19893]---> BDD-cost: 51 c ---[19891]---> BDD-cost: 68 c ---[19890]---> BDD-cost: 82 c ---[19889]---> Sorter-cost: 465 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19888]---> Sorter-cost: 626 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19887]---> Sorter-cost: 162 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19885]---> BDD-cost: 3 c ---[19884]---> Sorter-cost: 609 Base: 2 2 2 2 2 2 2 2 2 2 2 3 c ---[19883]---> BDD-cost: 88 c ---[19882]---> BDD-cost: 48 c ---[19874]---> BDD-cost: 3 c ---[19863]---> BDD-cost: 3 c ---[19852]---> BDD-cost: 3 c ---[19848]---> BDD-cost: 5 c ---[19844]---> BDD-cost: 48 c ---[19843]---> BDD-cost: 3 c ---[19842]---> Sorter-cost: 654 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[19841]---> BDD-cost: 3 c ---[19840]---> Sorter-cost: 328 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19839]---> BDD-cost: 43 c ---[19838]---> Sorter-cost: 276 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19837]---> Sorter-cost: 437 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19836]---> Sorter-cost: 243 Base: 2 2 2 2 2 2 2 2 2 2 c ---[19835]---> BDD-cost: 26 c ---[19834]---> Sorter-cost: 513 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19833]---> Sorter-cost: 297 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19832]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 3 c ---[19830]---> BDD-cost: 3 c ---[19829]---> Sorter-cost: 243 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19828]---> BDD-cost: 5 c ---[19826]---> BDD-cost: 50 c ---[19825]---> Sorter-cost: 246 Base: 2 2 2 2 2 2 2 2 2 3 c ---[19824]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19823]---> BDD-cost: 33 c ---[19822]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[19821]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 2 2 3 5 c ---[19820]---> Sorter-cost: 189 Base: 2 2 2 2 2 2 2 2 2 3 c ---[19819]---> BDD-cost: 3 c ---[19818]---> Sorter-cost: 202 Base: 2 2 2 2 2 2 2 2 2 2 c ---[19817]---> BDD-cost: 6 c ---[19812]---> BDD-cost: 5 c ---[19811]---> BDD-cost: 49 c ---[19810]---> BDD-cost: 10 c ---[19808]---> BDD-cost: 3 c ---[19807]---> BDD-cost: 18 c ---[19806]---> BDD-cost: 20 c ---[19805]---> BDD-cost: 43 c ---[19803]---> Sorter-cost: 345 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19802]---> BDD-cost: 74 c ---[19800]---> BDD-cost: 8 c ---[19799]---> Sorter-cost: 284 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19797]---> BDD-cost: 3 c ---[19796]---> BDD-cost: 114 c ---[19792]---> BDD-cost: 116 c ---[19789]---> BDD-cost: 18 c ---[19785]---> BDD-cost: 20 c ---[19784]---> Sorter-cost: 3185 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[19783]---> BDD-cost: 3 c ---[19772]---> BDD-cost: 3 c ---[19761]---> BDD-cost: 3 c ---[19750]---> BDD-cost: 3 c ---[19748]---> BDD-cost: 5 c ---[19747]---> BDD-cost: 9 c ---[19745]---> BDD-cost: 5 c ---[19744]---> BDD-cost: 5 c ---[19743]---> BDD-cost: 90 c ---[19742]---> Sorter-cost: 477 Base: 2 2 2 2 2 2 2 2 2 2 3 c ---[19741]---> Sorter-cost: 343 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19740]---> Sorter-cost: 310 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19739]---> BDD-cost: 3 c ---[19738]---> Sorter-cost: 375 Base: 2 2 2 2 2 2 2 2 2 2 3 c ---[19737]---> BDD-cost: 80 c ---[19736]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19735]---> Sorter-cost: 685 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19734]---> BDD-cost: 75 c ---[19733]---> Sorter-cost: 528 Base: 2 2 2 2 2 2 2 2 2 3 5 c ---[19729]---> BDD-cost: 49 c ---[19728]---> BDD-cost: 3 c ---[19727]---> BDD-cost: 4 c ---[19726]---> BDD-cost: 90 c ---[19725]---> BDD-cost: 24 c ---[19724]---> BDD-cost: 9 c ---[19723]---> Sorter-cost: 622 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19722]---> Sorter-cost: 298 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19721]---> BDD-cost: 65 c ---[19720]---> Sorter-cost: 456 Base: 2 2 2 2 2 2 2 2 2 2 2 3 c ---[19719]---> BDD-cost: 53 c ---[19718]---> Sorter-cost: 233 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19717]---> BDD-cost: 3 c ---[19706]---> BDD-cost: 3 c ---[19695]---> BDD-cost: 3 c ---[19684]---> BDD-cost: 3 c ---[19683]---> BDD-cost: 8 c ---[19682]---> BDD-cost: 3 c ---[19681]---> BDD-cost: 5 c ---[19680]---> BDD-cost: 5 c ---[19679]---> Sorter-cost: 208 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19678]---> Sorter-cost: 204 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[19677]---> BDD-cost: 7 c ---[19676]---> BDD-cost: 5 c ---[19675]---> BDD-cost: 7 c ---[19673]---> Sorter-cost: 3185 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[19672]---> BDD-cost: 3 c ---[19671]---> BDD-cost: 12 c ---[19661]---> BDD-cost: 3 c ---[19650]---> BDD-cost: 3 c ---[19639]---> BDD-cost: 3 c ---[19635]---> BDD-cost: 8 c ---[19633]---> BDD-cost: 5 c ---[19632]---> BDD-cost: 3 c ---[19631]---> Sorter-cost: 288 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19630]---> Sorter-cost: 413 Base: 2 2 2 2 2 2 2 2 2 2 2 5 c ---[19629]---> Sorter-cost: 254 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19628]---> BDD-cost: 3 c ---[19627]---> Sorter-cost: 155 Base: 2 2 2 2 2 2 2 2 2 3 c ---[19626]---> Sorter-cost: 224 Base: 2 2 2 2 2 2 2 2 2 2 c ---[19625]---> Sorter-cost: 364 Base: 2 2 2 2 2 2 2 2 2 2 2 5 c ---[19624]---> BDD-cost: 9 c ---[19620]---> BDD-cost: 16 c ---[19619]---> BDD-cost: 13 c ---[19617]---> BDD-cost: 3 c ---[19616]---> BDD-cost: 55 c ---[19614]---> Sorter-cost: 270 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19611]---> BDD-cost: 91 c ---[19610]---> Sorter-cost: 272 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19609]---> BDD-cost: 75 c ---[19608]---> BDD-cost: 88 c ---[19606]---> BDD-cost: 3 c ---[19605]---> BDD-cost: 17 c ---[19604]---> BDD-cost: 6 c ---[19601]---> BDD-cost: 88 c ---[19595]---> BDD-cost: 3 c ---[19584]---> BDD-cost: 3 c ---[19573]---> BDD-cost: 3 c ---[19566]---> BDD-cost: 5 c ---[19565]---> BDD-cost: 5 c ---[19564]---> BDD-cost: 1 c ---[19563]---> BDD-cost: 5 c ---[19562]---> Sorter-cost: 3184 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[19561]---> BDD-cost: 3 c ---[19559]---> BDD-cost: 8 c ---[19558]---> BDD-cost: 11 c ---[19557]---> BDD-cost: 3 c ---[19556]---> BDD-cost: 5 c ---[19554]---> BDD-cost: 21 c ---[19553]---> BDD-cost: 35 c ---[19552]---> Sorter-cost: 347 Base: 2 2 2 2 2 2 2 2 2 2 3 c ---[19550]---> BDD-cost: 3 c ---[19549]---> BDD-cost: 18 c ---[19539]---> BDD-cost: 3 c ---[19537]---> BDD-cost: 4 c ---[19530]---> BDD-cost: 5 c ---[19529]---> Sorter-cost: 534 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[19528]---> BDD-cost: 3 c ---[19526]---> BDD-cost: 125 c ---[19525]---> BDD-cost: 13 c ---[19524]---> BDD-cost: 7 c ---[19523]---> BDD-cost: 15 c ---[19522]---> BDD-cost: 34 c ---[19520]---> BDD-cost: 49 c ---[19517]---> BDD-cost: 3 c ---[19506]---> BDD-cost: 3 c ---[19495]---> BDD-cost: 3 c ---[19485]---> BDD-cost: 3 c ---[19484]---> BDD-cost: 3 c ---[19483]---> BDD-cost: 5 c ---[19482]---> BDD-cost: 5 c ---[19481]---> BDD-cost: 3 c ---[19480]---> BDD-cost: 3 c ---[19479]---> BDD-cost: 1 c ---[19478]---> BDD-cost: 45 c ---[19477]---> Sorter-cost: 327 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19476]---> BDD-cost: 49 c ---[19475]---> Sorter-cost: 465 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19474]---> BDD-cost: 25 c ---[19473]---> BDD-cost: 3 c ---[19472]---> BDD-cost: 56 c ---[19468]---> BDD-cost: 11 c ---[19466]---> BDD-cost: 72 c ---[19465]---> BDD-cost: 4 c ---[19464]---> BDD-cost: 30 c ---[19462]---> BDD-cost: 3 c ---[19460]---> BDD-cost: 44 c ---[19459]---> BDD-cost: 75 c ---[19458]---> BDD-cost: 15 c ---[19457]---> BDD-cost: 68 c ---[19455]---> BDD-cost: 82 c ---[19454]---> BDD-cost: 72 c ---[19453]---> BDD-cost: 9 c ---[19452]---> BDD-cost: 60 c ---[19451]---> Sorter-cost: 3185 Base: 2 2 2 2 2 2 2 5 2 3 3 3 3 2 5 3 2 c ---[19450]---> BDD-cost: 3 c ---[19449]---> Sorter-cost: 395 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19447]---> Sorter-cost: 675 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19446]---> Sorter-cost: 197 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19444]---> Sorter-cost: 406 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19443]---> BDD-cost: 51 c ---[19441]---> BDD-cost: 24 c ---[19439]---> BDD-cost: 3 c ---[19428]---> BDD-cost: 3 c ---[19417]---> BDD-cost: 3 c ---[19406]---> BDD-cost: 3 c ---[19404]---> BDD-cost: 5 c ---[19403]---> BDD-cost: 5 c ---[19399]---> BDD-cost: 90 c ---[19398]---> BDD-cost: 55 c ---[19397]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[19396]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[19395]---> BDD-cost: 3 c ---[19394]---> BDD-cost: 54 c ---[19393]---> BDD-cost: 34 c ---[19392]---> Sorter-c/oldhome/oroussel/solvers/minisat+_script: line 16: 25827 CPU time limit exceeded $XDIR/minisat+_bignum_static* "$@" #### 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.95 2/54 25822 Raw data (stat): 25822 (runsolver) R 25821 4613 4612 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842505839 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.99996 s] Raw data (loadavg): 0.93 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+20.0009 s] Raw data (loadavg): 0.94 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+30.0001 s] Raw data (loadavg): 0.95 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+40.0009 s] Raw data (loadavg): 0.96 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+50.0009 s] Raw data (loadavg): 0.96 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+60.0003 s] Raw data (loadavg): 0.97 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+69.9999 s] Raw data (loadavg): 0.97 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+79.9999 s] Raw data (loadavg): 0.98 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+90.0003 s] Raw data (loadavg): 0.98 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+100 s] Raw data (loadavg): 0.98 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+110 s] Raw data (loadavg): 0.98 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+120 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+130 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+140 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+150 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+160 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+170 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+180 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+190.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+200.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+210 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+220 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+230.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+240.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+250 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+260.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+270.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+280.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+290.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+300.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+310.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+320.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+330 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+340.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+350 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+360 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+370.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+380.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+390.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+400.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+410.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+420.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+430.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+440.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+450.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+460 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+470.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+480.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+490.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+500.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+510.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+520.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+530.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+540.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+550.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+560.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+570.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+580.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+590.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+600.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+610.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+620.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+630.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+640.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+650.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+660.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+670.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+680.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+690.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+700.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+710.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+720.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+730.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+740.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+750.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+760.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+770.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+780.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+790.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+800.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+810.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+820.004 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+830.004 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+840.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+850.004 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+860.004 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+870.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+880.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+890.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+900.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+910.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+920.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+930.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+940.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+950.007 s] Raw data (loadavg): 0.99 0.97 0.95 3/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+960.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+970.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+980.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+990.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1000.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1010.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1020.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1030.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1040.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1050.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1060.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1070.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1080.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1090.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1100.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1110.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1120.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1130.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1140.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1150.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1160.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1170.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1180.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1190.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1200.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1210.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1220.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1229.73 s] Raw data (loadavg): 0.99 0.97 0.95 1/53 25827 Raw data (stat): 25822 (minisat+_script) S 25821 4613 4612 0 -1 0 300 331 0 0 0 0 2 1 19 0 1 0 842505839 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 0 Child status: 152 Real time (s): 1229.73 CPU time (s): 1229.88 CPU user time (s): 1229.45 CPU system time (s): 0.434933 CPU usage (%): 100.013 Max. virtual memory (Kb): 2128 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####