| Name | mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-msc98-ip.opb |
| MD5SUM | b16b3be9013bb805347ce7c637f88389 |
| Bench Category | optimization, big integers (OPTBIGINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 3088409400819991040 |
| 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 | 1211.45 |
| Number of variables | 36105 |
| 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 |
LAUNCH ON wulflinc4 THE 2005-09-19 03:47:03 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2926 boxname=wulflinc4 idbench=582 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b16b3be9013bb805347ce7c637f88389 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-msc98-ip.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-msc98-ip.opb IDLAUNCH: 2926 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 915484 kB Buffers: 21456 kB Cached: 72124 kB SwapCached: 872 kB Active: 30592 kB Inactive: 65524 kB HighTotal: 131008 kB HighFree: 55692 kB LowTotal: 903652 kB LowFree: 859792 kB SwapTotal: 2097136 kB SwapFree: 2095648 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5672 kB Slab: 17252 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 04:07:14 (client local time) WITH STATUS 0 IN 1209.78 SECONDS stats: 2926 7 1209.78 0
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: 10 c ---[21782]---> BDD-cost: 14 c ---[21781]---> BDD-cost: 15 c ---[21780]---> BDD-cost: 17 c ---[21779]---> BDD-cost: 14 c ---[21778]---> BDD-cost: 15 c ---[21777]---> BDD-cost: 17 c ---[21776]---> BDD-cost: 14 c ---[21775]---> BDD-cost: 15 c ---[21774]---> BDD-cost: 17 c ---[21773]---> BDD-cost: 14 c ---[21772]---> BDD-cost: 15 c ---[21771]---> BDD-cost: 17 c ---[21770]---> BDD-cost: 14 c ---[21769]---> BDD-cost: 15 c ---[21768]---> BDD-cost: 17 c ---[21767]---> BDD-cost: 14 c ---[21766]---> BDD-cost: 15 c ---[21765]---> BDD-cost: 17 c ---[21764]---> BDD-cost: 14 c ---[21763]---> BDD-cost: 15 c ---[21762]---> BDD-cost: 17 c ---[21761]---> BDD-cost: 14 c ---[21760]---> BDD-cost: 15 c ---[21759]---> BDD-cost: 17 c ---[21758]---> BDD-cost: 14 c ---[21757]---> BDD-cost: 15 c ---[21756]---> BDD-cost: 17 c ---[21755]---> BDD-cost: 14 c ---[21754]---> BDD-cost: 15 c ---[21753]---> BDD-cost: 17 c ---[21752]---> BDD-cost: 14 c ---[21751]---> BDD-cost: 15 c ---[21750]---> BDD-cost: 17 c ---[21749]---> BDD-cost: 14 c ---[21748]---> BDD-cost: 15 c ---[21747]---> BDD-cost: 17 c ---[21746]---> BDD-cost: 14 c ---[21745]---> BDD-cost: 15 c ---[21744]---> BDD-cost: 17 c ---[21743]---> BDD-cost: 14 c ---[21742]---> BDD-cost: 15 c ---[21741]---> BDD-cost: 17 c ---[21740]---> BDD-cost: 14 c ---[21739]---> BDD-cost: 15 c ---[21738]---> BDD-cost: 17 c ---[21737]---> BDD-cost: 14 c ---[21736]---> BDD-cost: 15 c ---[21735]---> BDD-cost: 17 c ---[21734]---> BDD-cost: 14 c ---[21733]---> BDD-cost: 15 c ---[21732]---> BDD-cost: 17 c ---[21731]---> BDD-cost: 14 c ---[21730]---> BDD-cost: 15 c ---[21729]---> BDD-cost: 17 c ---[21728]---> BDD-cost: 14 c ---[21727]---> BDD-cost: 15 c ---[21726]---> BDD-cost: 17 c ---[21725]---> BDD-cost: 14 c ---[21724]---> BDD-cost: 15 c ---[21723]---> BDD-cost: 17 c ---[21722]---> BDD-cost: 14 c ---[21721]---> BDD-cost: 15 c ---[21720]---> BDD-cost: 17 c ---[21719]---> BDD-cost: 14 c ---[21718]---> BDD-cost: 15 c ---[21717]---> BDD-cost: 17 c ---[21716]---> BDD-cost: 14 c ---[21715]---> BDD-cost: 15 c ---[21714]---> BDD-cost: 17 c ---[21713]---> BDD-cost: 10 c ---[21712]---> BDD-cost: 14 c ---[21711]---> BDD-cost: 15 c ---[21710]---> BDD-cost: 17 c ---[21709]---> BDD-cost: 14 c ---[21708]---> BDD-cost: 15 c ---[21707]---> BDD-cost: 17 c ---[21706]---> BDD-cost: 14 c ---[21705]---> BDD-cost: 15 c ---[21704]---> BDD-cost: 17 c ---[21703]---> BDD-cost: 14 c ---[21702]---> BDD-cost: 15 c ---[21701]---> BDD-cost: 17 c ---[21700]---> BDD-cost: 14 c ---[21699]---> BDD-cost: 15 c ---[21698]---> BDD-cost: 17 c ---[21697]---> BDD-cost: 14 c ---[21696]---> BDD-cost: 15 c ---[21695]---> BDD-cost: 17 c ---[21694]---> BDD-cost: 14 c ---[21693]---> BDD-cost: 15 c ---[21692]---> BDD-cost: 17 c ---[21691]---> BDD-cost: 14 c ---[21690]---> BDD-cost: 15 c ---[21689]---> BDD-cost: 17 c ---[21688]---> BDD-cost: 14 c ---[21687]---> BDD-cost: 15 c ---[21686]---> BDD-cost: 17 c ---[21685]---> BDD-cost: 14 c ---[21684]---> BDD-cost: 15 c ---[21683]---> BDD-cost: 17 c ---[21682]---> BDD-cost: 14 c ---[21681]---> BDD-cost: 15 c ---[21680]---> BDD-cost: 17 c ---[21679]---> BDD-cost: 14 c ---[21678]---> BDD-cost: 15 c ---[21677]---> BDD-cost: 17 c ---[21676]---> BDD-cost: 14 c ---[21675]---> BDD-cost: 15 c ---[21674]---> BDD-cost: 17 c ---[21673]---> BDD-cost: 14 c ---[21672]---> BDD-cost: 15 c ---[21671]---> BDD-cost: 17 c ---[21670]---> BDD-cost: 14 c ---[21669]---> BDD-cost: 15 c ---[21668]---> BDD-cost: 17 c ---[21667]---> BDD-cost: 14 c ---[21666]---> BDD-cost: 15 c ---[21665]---> BDD-cost: 17 c ---[21664]---> BDD-cost: 14 c ---[21663]---> BDD-cost: 15 c ---[21662]---> BDD-cost: 17 c ---[21661]---> BDD-cost: 14 c ---[21660]---> BDD-cost: 15 c ---[21659]---> BDD-cost: 17 c ---[21658]---> BDD-cost: 14 c ---[21657]---> BDD-cost: 15 c ---[21656]---> BDD-cost: 17 c ---[21655]---> BDD-cost: 14 c ---[21654]---> BDD-cost: 15 c ---[21653]---> BDD-cost: 17 c ---[21652]---> BDD-cost: 14 c ---[21651]---> BDD-cost: 15 c ---[21650]---> BDD-cost: 17 c ---[21649]---> BDD-cost: 14 c ---[21648]---> BDD-cost: 15 c ---[21647]---> BDD-cost: 17 c ---[21646]---> BDD-cost: 14 c ---[21645]---> BDD-cost: 15 c ---[21644]---> BDD-cost: 17 c ---[21643]---> BDD-cost: 14 c ---[21642]---> BDD-cost: 15 c ---[21641]---> BDD-cost: 17 c ---[21640]---> BDD-cost: 14 c ---[21639]---> BDD-cost: 15 c ---[21638]---> BDD-cost: 17 c ---[21637]---> BDD-cost: 14 c ---[21636]---> BDD-cost: 15 c ---[21635]---> BDD-cost: 17 c ---[21634]---> BDD-cost: 14 c ---[21633]---> BDD-cost: 15 c ---[21632]---> BDD-cost: 17 c ---[21631]---> BDD-cost: 14 c ---[21630]---> BDD-cost: 15 c ---[21629]---> BDD-cost: 17 c ---[21628]---> BDD-cost: 14 c ---[21627]---> BDD-cost: 15 c ---[21626]---> BDD-cost: 17 c ---[21625]---> BDD-cost: 14 c ---[21624]---> BDD-cost: 15 c ---[21623]---> BDD-cost: 17 c ---[21622]---> BDD-cost: 14 c ---[21621]---> BDD-cost: 15 c ---[21620]---> BDD-cost: 17 c ---[21619]---> BDD-cost: 14 c ---[21618]---> BDD-cost: 15 c ---[21617]---> BDD-cost: 17 c ---[21616]---> BDD-cost: 14 c ---[21615]---> BDD-cost: 15 c ---[21614]---> BDD-cost: 17 c ---[21613]---> BDD-cost: 14 c ---[21612]---> BDD-cost: 15 c ---[21611]---> BDD-cost: 17 c ---[21610]---> BDD-cost: 14 c ---[21609]---> BDD-cost: 15 c ---[21608]---> BDD-cost: 17 c ---[21607]---> BDD-cost: 14 c ---[21606]---> BDD-cost: 15 c ---[21605]---> BDD-cost: 17 c ---[21604]---> BDD-cost: 14 c ---[21603]---> BDD-cost: 15 c ---[21602]---> BDD-cost: 17 c ---[21601]---> BDD-cost: 14 c ---[21600]---> BDD-cost: 15 c ---[21599]---> BDD-cost: 17 c ---[21598]---> BDD-cost: 14 c ---[21597]---> BDD-cost: 15 c ---[21596]---> BDD-cost: 17 c ---[21595]---> BDD-cost: 14 c ---[21594]---> BDD-cost: 15 c ---[21593]---> BDD-cost: 17 c ---[21592]---> BDD-cost: 14 c ---[21591]---> BDD-cost: 15 c ---[21590]---> BDD-cost: 17 c ---[21589]---> BDD-cost: 14 c ---[21588]---> BDD-cost: 15 c ---[21587]---> BDD-cost: 17 c ---[21586]---> BDD-cost: 14 c ---[21585]---> BDD-cost: 15 c ---[21584]---> BDD-cost: 17 c ---[21583]---> BDD-cost: 14 c ---[21582]---> BDD-cost: 15 c ---[21581]---> BDD-cost: 17 c ---[21580]---> BDD-cost: 14 c ---[21579]---> BDD-cost: 15 c ---[21578]---> BDD-cost: 17 c ---[21577]---> BDD-cost: 14 c ---[21576]---> BDD-cost: 15 c ---[21575]---> BDD-cost: 17 c ---[21574]---> BDD-cost: 14 c ---[21573]---> BDD-cost: 15 c ---[21572]---> BDD-cost: 17 c ---[21571]---> BDD-cost: 14 c ---[21570]---> BDD-cost: 15 c ---[21569]---> BDD-cost: 17 c ---[21568]---> BDD-cost: 14 c ---[21567]---> BDD-cost: 15 c ---[21566]---> BDD-cost: 17 c ---[21565]---> BDD-cost: 14 c ---[21564]---> BDD-cost: 15 c ---[21563]---> BDD-cost: 17 c ---[21562]---> BDD-cost: 14 c ---[21561]---> BDD-cost: 15 c ---[21560]---> BDD-cost: 17 c ---[21559]---> BDD-cost: 14 c ---[21558]---> BDD-cost: 15 c ---[21557]---> BDD-cost: 17 c ---[21556]---> BDD-cost: 14 c ---[21555]---> BDD-cost: 15 c ---[21554]---> BDD-cost: 17 c ---[21553]---> BDD-cost: 14 c ---[21552]---> BDD-cost: 15 c ---[21551]---> BDD-cost: 17 c ---[21550]---> BDD-cost: 14 c ---[21549]---> BDD-cost: 15 c ---[21548]---> BDD-cost: 17 c ---[21547]---> BDD-cost: 14 c ---[21546]---> BDD-cost: 15 c ---[21545]---> BDD-cost: 17 c ---[21544]---> BDD-cost: 14 c ---[21543]---> BDD-cost: 15 c ---[21542]---> BDD-cost: 17 c ---[21541]---> BDD-cost: 14 c ---[21540]---> BDD-cost: 15 c ---[21539]---> BDD-cost: 17 c ---[21538]---> BDD-cost: 14 c ---[21537]---> BDD-cost: 15 c ---[21536]---> BDD-cost: 17 c ---[21535]---> BDD-cost: 14 c ---[21534]---> BDD-cost: 15 c ---[21533]---> BDD-cost: 17 c ---[21532]---> BDD-cost: 14 c ---[21531]---> BDD-cost: 15 c ---[21530]---> BDD-cost: 17 c ---[21529]---> BDD-cost: 14 c ---[21528]---> BDD-cost: 15 c ---[21527]---> BDD-cost: 17 c ---[21526]---> BDD-cost: 14 c ---[21525]---> BDD-cost: 15 c ---[21524]---> BDD-cost: 17 c ---[21523]---> BDD-cost: 14 c ---[21522]---> BDD-cost: 15 c ---[21521]---> BDD-cost: 17 c ---[21520]---> BDD-cost: 14 c ---[21519]---> BDD-cost: 15 c ---[21518]---> BDD-cost: 17 c ---[21517]---> BDD-cost: 14 c ---[21516]---> BDD-cost: 15 c ---[21515]---> BDD-cost: 17 c ---[21514]---> BDD-cost: 14 c ---[21513]---> BDD-cost: 15 c ---[21512]---> BDD-cost: 17 c ---[21511]---> BDD-cost: 14 c ---[21510]---> BDD-cost: 15 c ---[21509]---> BDD-cost: 17 c ---[21508]---> BDD-cost: 14 c ---[21507]---> BDD-cost: 15 c ---[21506]---> BDD-cost: 17 c ---[21505]---> BDD-cost: 14 c ---[21504]---> BDD-cost: 15 c ---[21503]---> BDD-cost: 17 c ---[21502]---> BDD-cost: 14 c ---[21501]---> BDD-cost: 15 c ---[21500]---> BDD-cost: 17 c ---[21499]---> BDD-cost: 14 c ---[21498]---> BDD-cost: 15 c ---[21497]---> BDD-cost: 17 c ---[21496]---> BDD-cost: 14 c ---[21495]---> BDD-cost: 15 c ---[21494]---> BDD-cost: 17 c ---[21493]---> BDD-cost: 14 c ---[21492]---> BDD-cost: 15 c ---[21491]---> BDD-cost: 17 c ---[21490]---> BDD-cost: 14 c ---[21489]---> BDD-cost: 15 c ---[21488]---> BDD-cost: 17 c ---[21487]---> BDD-cost: 14 c ---[21486]---> BDD-cost: 15 c ---[21485]---> BDD-cost: 17 c ---[21484]---> BDD-cost: 14 c ---[21483]---> BDD-cost: 15 c ---[21482]---> BDD-cost: 17 c ---[21481]---> BDD-cost: 14 c ---[21480]---> BDD-cost: 15 c ---[21479]---> BDD-cost: 17 c ---[21478]---> BDD-cost: 14 c ---[21477]---> BDD-cost: 15 c ---[21476]---> BDD-cost: 17 c ---[21475]---> BDD-cost: 14 c ---[21474]---> BDD-cost: 15 c ---[21473]---> BDD-cost: 17 c ---[21472]---> BDD-cost: 14 c ---[21471]---> BDD-cost: 15 c ---[21470]---> BDD-cost: 17 c ---[21469]---> BDD-cost: 14 c ---[21468]---> BDD-cost: 15 c ---[21467]---> BDD-cost: 17 c ---[21466]---> BDD-cost: 14 c ---[21465]---> BDD-cost: 15 c ---[21464]---> BDD-cost: 17 c ---[21463]---> BDD-cost: 14 c ---[21462]---> BDD-cost: 15 c ---[21461]---> BDD-cost: 17 c ---[21460]---> BDD-cost: 14 c ---[21459]---> BDD-cost: 15 c ---[21458]---> BDD-cost: 17 c ---[21457]---> BDD-cost: 14 c ---[21456]---> BDD-cost: 15 c ---[21455]---> BDD-cost: 17 c ---[21454]---> BDD-cost: 14 c ---[21453]---> BDD-cost: 15 c ---[21452]---> BDD-cost: 17 c ---[21451]---> BDD-cost: 14 c ---[21450]---> BDD-cost: 15 c ---[21449]---> BDD-cost: 17 c ---[21448]---> BDD-cost: 14 c ---[21447]---> BDD-cost: 15 c ---[21446]---> BDD-cost: 17 c ---[21445]---> BDD-cost: 14 c ---[21444]---> BDD-cost: 15 c ---[21443]---> BDD-cost: 17 c ---[21442]---> BDD-cost: 14 c ---[21441]---> BDD-cost: 15 c ---[21440]---> BDD-cost: 17 c ---[21439]---> BDD-cost: 14 c ---[21438]---> BDD-cost: 15 c ---[21437]---> BDD-cost: 17 c ---[21436]---> BDD-cost: 14 c ---[21435]---> BDD-cost: 15 c ---[21434]---> BDD-cost: 17 c ---[21433]---> BDD-cost: 14 c ---[21432]---> BDD-cost: 15 c ---[21431]---> BDD-cost: 17 c ---[21430]---> BDD-cost: 14 c ---[21429]---> BDD-cost: 15 c ---[21428]---> BDD-cost: 17 c ---[21427]---> BDD-cost: 14 c ---[21426]---> BDD-cost: 15 c ---[21425]---> BDD-cost: 17 c ---[21424]---> BDD-cost: 14 c ---[21423]---> BDD-cost: 15 c ---[21422]---> BDD-cost: 17 c ---[21421]---> BDD-cost: 14 c ---[21420]---> BDD-cost: 15 c ---[21419]---> BDD-cost: 17 c ---[21418]---> BDD-cost: 14 c ---[21417]---> BDD-cost: 15 c ---[21416]---> BDD-cost: 17 c ---[21415]---> BDD-cost: 14 c ---[21414]---> BDD-cost: 15 c ---[21413]---> BDD-cost: 17 c ---[21412]---> BDD-cost: 14 c ---[21411]---> BDD-cost: 15 c ---[21410]---> BDD-cost: 17 c ---[21409]---> BDD-cost: 14 c ---[21408]---> BDD-cost: 15 c ---[21407]---> BDD-cost: 17 c ---[21406]---> BDD-cost: 14 c ---[21405]---> BDD-cost: 15 c ---[21404]---> BDD-cost: 17 c ---[21403]---> BDD-cost: 14 c ---[21402]---> BDD-cost: 15 c ---[21401]---> BDD-cost: 17 c ---[21400]---> BDD-cost: 14 c ---[21399]---> BDD-cost: 15 c ---[21398]---> BDD-cost: 17 c ---[21397]---> BDD-cost: 14 c ---[21396]---> BDD-cost: 15 c ---[21395]---> BDD-cost: 17 c ---[21394]---> BDD-cost: 14 c ---[21393]---> BDD-cost: 15 c ---[21392]---> BDD-cost: 17 c ---[21391]---> BDD-cost: 14 c ---[21390]---> BDD-cost: 15 c ---[21389]---> BDD-cost: 17 c ---[21388]---> BDD-cost: 14 c ---[21387]---> BDD-cost: 15 c ---[21386]---> BDD-cost: 17 c ---[21385]---> BDD-cost: 14 c ---[21384]---> BDD-cost: 15 c ---[21383]---> BDD-cost: 17 c ---[21382]---> BDD-cost: 14 c ---[21381]---> BDD-cost: 15 c ---[21380]---> BDD-cost: 17 c ---[21379]---> BDD-cost: 14 c ---[21378]---> BDD-cost: 15 c ---[21377]---> BDD-cost: 17 c ---[21376]---> BDD-cost: 14 c ---[21375]---> BDD-cost: 15 c ---[21374]---> BDD-cost: 17 c ---[21373]---> BDD-cost: 14 c ---[21372]---> BDD-cost: 15 c ---[21371]---> BDD-cost: 17 c ---[21370]---> BDD-cost: 14 c ---[21369]---> BDD-cost: 15 c ---[21368]---> BDD-cost: 17 c ---[21367]---> BDD-cost: 14 c ---[21366]---> BDD-cost: 15 c ---[21365]---> BDD-cost: 17 c ---[21364]---> BDD-cost: 14 c ---[21363]---> BDD-cost: 15 c ---[21362]---> BDD-cost: 17 c ---[21361]---> BDD-cost: 14 c ---[21360]---> BDD-cost: 15 c ---[21359]---> BDD-cost: 17 c ---[21358]---> BDD-cost: 14 c ---[21357]---> BDD-cost: 15 c ---[21356]---> BDD-cost: 17 c ---[21355]---> BDD-cost: 14 c ---[21354]---> BDD-cost: 15 c ---[21353]---> BDD-cost: 17 c ---[21352]---> BDD-cost: 14 c ---[21351]---> BDD-cost: 15 c ---[21350]---> BDD-cost: 17 c ---[21349]---> BDD-cost: 14 c ---[21348]---> BDD-cost: 15 c ---[21347]---> BDD-cost: 17 c ---[21346]---> BDD-cost: 14 c ---[21345]---> BDD-cost: 15 c ---[21344]---> BDD-cost: 17 c ---[21343]---> BDD-cost: 14 c ---[21342]---> BDD-cost: 15 c ---[21341]---> BDD-cost: 17 c ---[21340]---> BDD-cost: 14 c ---[21339]---> BDD-cost: 15 c ---[21338]---> BDD-cost: 17 c ---[21337]---> BDD-cost: 14 c ---[21336]---> BDD-cost: 15 c ---[21335]---> BDD-cost: 17 c ---[21334]---> BDD-cost: 14 c ---[21333]---> BDD-cost: 15 c ---[21332]---> BDD-cost: 17 c ---[21331]---> BDD-cost: 14 c ---[21330]---> BDD-cost: 15 c ---[21329]---> BDD-cost: 17 c ---[21328]---> BDD-cost: 14 c ---[21327]---> BDD-cost: 15 c ---[21326]---> BDD-cost: 17 c ---[21325]---> BDD-cost: 14 c ---[21324]---> BDD-cost: 15 c ---[21323]---> BDD-cost: 17 c ---[21322]---> BDD-cost: 14 c ---[21321]---> BDD-cost: 15 c ---[21320]---> BDD-cost: 17 c ---[21319]---> BDD-cost: 14 c ---[21318]---> BDD-cost: 15 c ---[21317]---> BDD-cost: 17 c ---[21316]---> BDD-cost: 14 c ---[21315]---> BDD-cost: 15 c ---[21314]---> BDD-cost: 17 c ---[21313]---> BDD-cost: 14 c ---[21312]---> BDD-cost: 15 c ---[21311]---> BDD-cost: 17 c ---[21310]---> BDD-cost: 14 c ---[21309]---> BDD-cost: 15 c ---[21308]---> BDD-cost: 17 c ---[21307]---> BDD-cost: 14 c ---[21306]---> BDD-cost: 15 c ---[21305]---> BDD-cost: 17 c ---[21304]---> BDD-cost: 14 c ---[21303]---> BDD-cost: 15 c ---[21302]---> BDD-cost: 17 c ---[21301]---> BDD-cost: 14 c ---[21300]---> BDD-cost: 15 c ---[21299]---> BDD-cost: 17 c ---[21298]---> BDD-cost: 14 c ---[21297]---> BDD-cost: 15 c ---[21296]---> BDD-cost: 17 c ---[21295]---> BDD-cost: 14 c ---[21294]---> BDD-cost: 15 c ---[21293]---> BDD-cost: 17 c ---[21292]---> BDD-cost: 14 c ---[21291]---> BDD-cost: 15 c ---[21290]---> BDD-cost: 17 c ---[21289]---> BDD-cost: 14 c ---[21288]---> BDD-cost: 15 c ---[21287]---> BDD-cost: 17 c ---[21286]---> BDD-cost: 14 c ---[21285]---> BDD-cost: 15 c ---[21284]---> BDD-cost: 17 c ---[21283]---> BDD-cost: 14 c ---[21282]---> BDD-cost: 15 c ---[21281]---> BDD-cost: 17 c ---[21280]---> BDD-cost: 14 c ---[21279]---> BDD-cost: 15 c ---[21278]---> BDD-cost: 17 c ---[21277]---> BDD-cost: 14 c ---[21276]---> BDD-cost: 15 c ---[21275]---> BDD-cost: 17 c ---[21274]---> BDD-cost: 14 c ---[21273]---> BDD-cost: 15 c ---[21272]---> BDD-cost: 17 c ---[21271]---> BDD-cost: 14 c ---[21270]---> BDD-cost: 15 c ---[21269]---> BDD-cost: 17 c ---[21268]---> BDD-cost: 14 c ---[21267]---> BDD-cost: 15 c ---[21266]---> BDD-cost: 17 c ---[21265]---> BDD-cost: 14 c ---[21264]---> BDD-cost: 15 c ---[21263]---> BDD-cost: 17 c ---[21262]---> BDD-cost: 14 c ---[21261]---> BDD-cost: 15 c ---[21260]---> BDD-cost: 17 c ---[21259]---> BDD-cost: 14 c ---[21258]---> BDD-cost: 15 c ---[21257]---> BDD-cost: 17 c ---[21256]---> BDD-cost: 14 c ---[21255]---> BDD-cost: 15 c ---[21254]---> BDD-cost: 17 c ---[21253]---> BDD-cost: 14 c ---[21252]---> BDD-cost: 15 c ---[21251]---> BDD-cost: 17 c ---[21250]---> BDD-cost: 14 c ---[21249]---> BDD-cost: 15 c ---[21248]---> BDD-cost: 17 c ---[21247]---> BDD-cost: 14 c ---[21246]---> BDD-cost: 15 c ---[21245]---> BDD-cost: 17 c ---[21244]---> BDD-cost: 14 c ---[21243]---> BDD-cost: 15 c ---[21242]---> BDD-cost: 17 c ---[21241]---> BDD-cost: 14 c ---[21240]---> BDD-cost: 15 c ---[21239]---> BDD-cost: 17 c ---[21238]---> BDD-cost: 14 c ---[21237]---> BDD-cost: 15 c ---[21236]---> BDD-cost: 17 c ---[21235]---> BDD-cost: 14 c ---[21234]---> BDD-cost: 15 c ---[21233]---> BDD-cost: 17 c ---[21232]---> BDD-cost: 14 c ---[21231]---> BDD-cost: 15 c ---[21230]---> BDD-cost: 17 c ---[21229]---> BDD-cost: 14 c ---[21228]---> BDD-cost: 15 c ---[21227]---> BDD-cost: 17 c ---[21226]---> BDD-cost: 14 c ---[21225]---> BDD-cost: 15 c ---[21224]---> BDD-cost: 17 c ---[21223]---> BDD-cost: 14 c ---[21222]---> BDD-cost: 15 c ---[21221]---> BDD-cost: 17 c ---[21220]---> BDD-cost: 14 c ---[21219]---> BDD-cost: 15 c ---[21218]---> BDD-cost: 17 c ---[21217]---> BDD-cost: 14 c ---[21216]---> BDD-cost: 15 c ---[21215]---> BDD-cost: 17 c ---[21214]---> BDD-cost: 14 c ---[21213]---> BDD-cost: 15 c ---[21212]---> BDD-cost: 17 c ---[21211]---> BDD-cost: 14 c ---[21210]---> BDD-cost: 15 c ---[21209]---> BDD-cost: 17 c ---[21208]---> BDD-cost: 14 c ---[21207]---> BDD-cost: 15 c ---[21206]---> BDD-cost: 17 c ---[21205]---> BDD-cost: 14 c ---[21204]---> BDD-cost: 15 c ---[21203]---> BDD-cost: 17 c ---[21202]---> BDD-cost: 14 c ---[21201]---> BDD-cost: 15 c ---[21200]---> BDD-cost: 17 c ---[21199]---> BDD-cost: 14 c ---[21198]---> BDD-cost: 15 c ---[21197]---> BDD-cost: 17 c ---[21196]---> BDD-cost: 14 c ---[21195]---> BDD-cost: 15 c ---[21194]---> BDD-cost: 17 c ---[21193]---> BDD-cost: 14 c ---[21192]---> BDD-cost: 15 c ---[21191]---> BDD-cost: 17 c ---[21190]---> BDD-cost: 14 c ---[21189]---> BDD-cost: 15 c ---[21188]---> BDD-cost: 17 c ---[21187]---> BDD-cost: 14 c ---[21186]---> BDD-cost: 15 c ---[21185]---> BDD-cost: 17 c ---[21184]---> BDD-cost: 14 c ---[21183]---> BDD-cost: 15 c ---[21182]---> BDD-cost: 17 c ---[21181]---> BDD-cost: 14 c ---[21180]---> BDD-cost: 15 c ---[21179]---> BDD-cost: 17 c ---[21178]---> BDD-cost: 14 c ---[21177]---> BDD-cost: 15 c ---[21176]---> BDD-cost: 17 c ---[21175]---> BDD-cost: 14 c ---[21174]---> BDD-cost: 15 c ---[21173]---> BDD-cost: 17 c ---[21172]---> BDD-cost: 14 c ---[21171]---> BDD-cost: 15 c ---[21170]---> BDD-cost: 17 c ---[21169]---> BDD-cost: 14 c ---[21168]---> BDD-cost: 15 c ---[21167]---> BDD-cost: 17 c ---[21166]---> BDD-cost: 14 c ---[21165]---> BDD-cost: 15 c ---[21164]---> BDD-cost: 17 c ---[21163]---> BDD-cost: 14 c ---[21162]---> BDD-cost: 15 c ---[21161]---> BDD-cost: 17 c ---[21160]---> BDD-cost: 14 c ---[21159]---> BDD-cost: 15 c ---[21158]---> BDD-cost: 17 c ---[21157]---> BDD-cost: 14 c ---[21156]---> BDD-cost: 15 c ---[21155]---> BDD-cost: 17 c ---[21154]---> BDD-cost: 14 c ---[21153]---> BDD-cost: 15 c ---[21152]---> BDD-cost: 17 c ---[21151]---> BDD-cost: 14 c ---[21150]---> BDD-cost: 15 c ---[21149]---> BDD-cost: 17 c ---[21148]---> BDD-cost: 14 c ---[21147]---> BDD-cost: 15 c ---[21146]---> BDD-cost: 17 c ---[21145]---> BDD-cost: 14 c ---[21144]---> BDD-cost: 15 c ---[21143]---> BDD-cost: 17 c ---[21142]---> BDD-cost: 14 c ---[21141]---> BDD-cost: 15 c ---[21140]---> BDD-cost: 17 c ---[21139]---> BDD-cost: 14 c ---[21138]---> BDD-cost: 15 c ---[21137]---> BDD-cost: 17 c ---[21136]---> BDD-cost: 14 c ---[21135]---> BDD-cost: 15 c ---[21134]---> BDD-cost: 17 c ---[21133]---> BDD-cost: 14 c ---[21132]---> BDD-cost: 15 c ---[21131]---> BDD-cost: 17 c ---[21130]---> BDD-cost: 14 c ---[21129]---> BDD-cost: 15 c ---[21128]---> BDD-cost: 17 c ---[21127]---> BDD-cost: 14 c ---[21126]---> BDD-cost: 15 c ---[21125]---> BDD-cost: 17 c ---[21124]---> BDD-cost: 14 c ---[21123]---> BDD-cost: 15 c ---[21122]---> BDD-cost: 17 c ---[21121]---> BDD-cost: 14 c ---[21120]---> BDD-cost: 15 c ---[21119]---> BDD-cost: 17 c ---[21118]---> BDD-cost: 14 c ---[21117]---> BDD-cost: 15 c ---[21116]---> BDD-cost: 17 c ---[21115]---> BDD-cost: 14 c ---[21114]---> BDD-cost: 15 c ---[21113]---> BDD-cost: 17 c ---[21112]---> BDD-cost: 14 c ---[21111]---> BDD-cost: 15 c ---[21110]---> BDD-cost: 17 c ---[21109]---> BDD-cost: 14 c ---[21108]---> BDD-cost: 15 c ---[21107]---> BDD-cost: 17 c ---[21106]---> BDD-cost: 14 c ---[21105]---> BDD-cost: 15 c ---[21104]---> BDD-cost: 17 c ---[21103]---> BDD-cost: 14 c ---[21102]---> BDD-cost: 15 c ---[21101]---> BDD-cost: 17 c ---[21100]---> BDD-cost: 14 c ---[21099]---> BDD-cost: 15 c ---[21098]---> BDD-cost: 17 c ---[21097]---> BDD-cost: 14 c ---[21096]---> BDD-cost: 15 c ---[21095]---> BDD-cost: 17 c ---[21094]---> BDD-cost: 14 c ---[21093]---> BDD-cost: 15 c ---[21092]---> BDD-cost: 17 c ---[21091]---> BDD-cost: 14 c ---[21090]---> BDD-cost: 15 c ---[21089]---> BDD-cost: 17 c ---[21088]---> BDD-cost: 14 c ---[21087]---> BDD-cost: 15 c ---[21086]---> BDD-cost: 17 c ---[21085]---> BDD-cost: 14 c ---[21084]---> BDD-cost: 15 c ---[21083]---> BDD-cost: 17 c ---[21082]---> BDD-cost: 14 c ---[21081]---> BDD-cost: 15 c ---[21080]---> BDD-cost: 17 c ---[21079]---> BDD-cost: 14 c ---[21078]---> BDD-cost: 15 c ---[21077]---> BDD-cost: 17 c ---[21076]---> BDD-cost: 14 c ---[21075]---> BDD-cost: 15 c ---[21074]---> BDD-cost: 17 c ---[21073]---> BDD-cost: 14 c ---[21072]---> BDD-cost: 15 c ---[21071]---> BDD-cost: 17 c ---[21070]---> BDD-cost: 14 c ---[21069]---> BDD-cost: 15 c ---[21068]---> BDD-cost: 17 c ---[21067]---> BDD-cost: 14 c ---[21066]---> BDD-cost: 15 c ---[21065]---> BDD-cost: 17 c ---[21064]---> BDD-cost: 14 c ---[21063]---> BDD-cost: 15 c ---[21062]---> BDD-cost: 17 c ---[21061]---> BDD-cost: 14 c ---[21060]---> BDD-cost: 15 c ---[21059]---> BDD-cost: 17 c ---[21058]---> BDD-cost: 14 c ---[21057]---> BDD-cost: 15 c ---[21056]---> BDD-cost: 17 c ---[21055]---> BDD-cost: 14 c ---[21054]---> BDD-cost: 15 c ---[21053]---> BDD-cost: 17 c ---[21052]---> BDD-cost: 14 c ---[21051]---> BDD-cost: 15 c ---[21050]---> BDD-cost: 17 c ---[21049]---> BDD-cost: 14 c ---[21048]---> BDD-cost: 15 c ---[21047]---> BDD-cost: 17 c ---[21046]---> BDD-cost: 14 c ---[21045]---> BDD-cost: 15 c ---[21044]---> BDD-cost: 17 c ---[21043]---> BDD-cost: 14 c ---[21042]---> BDD-cost: 15 c ---[21041]---> BDD-cost: 17 c ---[21040]---> BDD-cost: 14 c ---[21039]---> BDD-cost: 15 c ---[21038]---> BDD-cost: 17 c ---[21037]---> BDD-cost: 14 c ---[21036]---> BDD-cost: 15 c ---[21035]---> BDD-cost: 17 c ---[21034]---> BDD-cost: 14 c ---[21033]---> BDD-cost: 15 c ---[21032]---> BDD-cost: 17 c ---[21031]---> BDD-cost: 14 c ---[21030]---> BDD-cost: 15 c ---[21029]---> BDD-cost: 17 c ---[21028]---> BDD-cost: 14 c ---[21027]---> BDD-cost: 15 c ---[21026]---> BDD-cost: 17 c ---[21025]---> BDD-cost: 14 c ---[21024]---> BDD-cost: 15 c ---[21023]---> BDD-cost: 17 c ---[21022]---> BDD-cost: 14 c ---[21021]---> BDD-cost: 15 c ---[21020]---> BDD-cost: 17 c ---[21019]---> BDD-cost: 14 c ---[21018]---> BDD-cost: 15 c ---[21017]---> BDD-cost: 17 c ---[21016]---> BDD-cost: 14 c ---[21015]---> BDD-cost: 15 c ---[21014]---> BDD-cost: 17 c ---[21013]---> BDD-cost: 14 c ---[21012]---> BDD-cost: 15 c ---[21011]---> BDD-cost: 17 c ---[21010]---> BDD-cost: 14 c ---[21009]---> BDD-cost: 15 c ---[21008]---> BDD-cost: 17 c ---[21007]---> BDD-cost: 14 c ---[21006]---> BDD-cost: 15 c ---[21005]---> BDD-cost: 17 c ---[21004]---> BDD-cost: 14 c ---[21003]---> BDD-cost: 15 c ---[21002]---> BDD-cost: 17 c ---[21001]---> BDD-cost: 14 c ---[21000]---> BDD-cost: 15 c ---[20999]---> BDD-cost: 17 c ---[20998]---> BDD-cost: 14 c ---[20997]---> BDD-cost: 15 c ---[20996]---> BDD-cost: 17 c ---[20995]---> BDD-cost: 14 c ---[20994]---> BDD-cost: 15 c ---[20993]---> BDD-cost: 17 c ---[20992]---> BDD-cost: 14 c ---[20991]---> BDD-cost: 15 c ---[20990]---> BDD-cost: 17 c ---[20989]---> BDD-cost: 14 c ---[20988]---> BDD-cost: 15 c ---[20987]---> BDD-cost: 17 c ---[20986]---> BDD-cost: 14 c ---[20985]---> BDD-cost: 15 c ---[20984]---> BDD-cost: 17 c ---[20983]---> BDD-cost: 14 c ---[20982]---> BDD-cost: 15 c ---[20981]---> BDD-cost: 17 c ---[20980]---> BDD-cost: 14 c ---[20979]---> BDD-cost: 15 c ---[20978]---> BDD-cost: 17 c ---[20977]---> BDD-cost: 14 c ---[20976]---> BDD-cost: 15 c ---[20975]---> BDD-cost: 17 c ---[20974]---> BDD-cost: 14 c ---[20973]---> BDD-cost: 15 c ---[20972]---> BDD-cost: 17 c ---[20971]---> BDD-cost: 14 c ---[20970]---> BDD-cost: 15 c ---[20969]---> BDD-cost: 17 c ---[20968]---> BDD-cost: 14 c ---[20967]---> BDD-cost: 15 c ---[20966]---> BDD-cost: 17 c ---[20965]---> BDD-cost: 14 c ---[20964]---> BDD-cost: 15 c ---[20963]---> BDD-cost: 17 c ---[20962]---> BDD-cost: 14 c ---[20961]---> BDD-cost: 15 c ---[20960]---> BDD-cost: 17 c ---[20959]---> BDD-cost: 14 c ---[20958]---> BDD-cost: 15 c ---[20957]---> BDD-cost: 17 c ---[20956]---> BDD-cost: 14 c ---[20955]---> BDD-cost: 15 c ---[20954]---> BDD-cost: 17 c ---[20899]---> BDD-cost: 23 c ---[20897]---> BDD-cost: 3 c ---[20896]---> Sorter-cost: 4930 Base: 2 2 2 2 2 2 2 2 5 2 2 2 3 3 3 5 3 3 2 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: 529 Base: 2 2 2 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 2 2 2 3 c ---[20877]---> Sorter-cost: 279 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20876]---> BDD-cost: 24 c ---[20875]---> Sorter-cost: 395 Base: 2 2 2 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 2 2 2 c ---[20873]---> BDD-cost: 3 c ---[20872]---> Sorter-cost: 310 Base: 2 2 2 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 2 2 2 3 c ---[20870]---> Sorter-cost: 389 Base: 2 2 2 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 2 2 2 13 c ---[20867]---> Sorter-cost: 778 Base: 2 2 2 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 2 2 2 c ---[20865]---> Sorter-cost: 763 Base: 2 2 2 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: 142 c ---[20848]---> BDD-cost: 29 c ---[20844]---> BDD-cost: 13 c ---[20843]---> Sorter-cost: 382 Base: 2 2 2 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: 398 Base: 2 2 2 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: 4916 Base: 2 2 2 2 2 2 2 2 5 2 2 2 3 3 3 5 3 3 2 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: 436 Base: 2 2 2 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 2 2 2 c ---[20776]---> Sorter-cost: 230 Base: 2 2 2 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 2 2 2 c ---[20774]---> Sorter-cost: 679 Base: 2 2 2 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 2 2 2 3 c ---[20771]---> Sorter-cost: 536 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[20770]---> Sorter-cost: 471 Base: 2 2 2 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 2 2 2 c ---[20767]---> Sorter-cost: 210 Base: 2 2 2 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 2 2 2 3 c ---[20764]---> BDD-cost: 83 c ---[20763]---> Sorter-cost: 724 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20762]---> BDD-cost: 3 c ---[20761]---> BDD-cost: 81 c ---[20760]---> BDD-cost: 6 c ---[20759]---> BDD-cost: 6 c ---[20757]---> BDD-cost: 79 c ---[20756]---> BDD-cost: 90 c ---[20755]---> BDD-cost: 55 c ---[20754]---> BDD-cost: 65 c ---[20752]---> BDD-cost: 46 c ---[20751]---> BDD-cost: 3 c ---[20749]---> BDD-cost: 13 c ---[20747]---> Sorter-cost: 721 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20746]---> BDD-cost: 17 c ---[20742]---> BDD-cost: 81 c ---[20740]---> BDD-cost: 3 c ---[20739]---> BDD-cost: 55 c ---[20738]---> BDD-cost: 16 c ---[20737]---> BDD-cost: 126 c ---[20733]---> BDD-cost: 81 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: 443 Base: 2 2 2 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 2 2 2 c ---[20675]---> Sorter-cost: 240 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20674]---> Sorter-cost: 4916 Base: 2 2 2 2 2 2 2 2 5 2 2 2 3 3 3 5 3 3 2 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 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 2 2 2 c ---[20667]---> Sorter-cost: 51 Base: 2 2 2 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 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 2 2 2 c ---[20662]---> BDD-cost: 3 c ---[20661]---> Sorter-cost: 46 Base: 2 2 2 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 2 2 2 c ---[20659]---> Sorter-cost: 230 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20658]---> Sorter-cost: 763 Base: 2 2 2 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 2 2 2 c ---[20656]---> Sorter-cost: 683 Base: 2 2 2 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: 121 c ---[20651]---> BDD-cost: 3 c ---[20650]---> BDD-cost: 6 c ---[20649]---> Sorter-cost: 915 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 c ---[20646]---> BDD-cost: 50 c ---[20643]---> BDD-cost: 8 c ---[20642]---> BDD-cost: 11 c ---[20640]---> BDD-cost: 3 c ---[20639]---> BDD-cost: 6 c ---[20637]---> BDD-cost: 100 c ---[20636]---> BDD-cost: 6 c ---[20635]---> BDD-cost: 25 c ---[20634]---> Sorter-cost: 303 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20633]---> Sorter-cost: 262 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20632]---> BDD-cost: 130 c ---[20631]---> BDD-cost: 51 c ---[20629]---> BDD-cost: 3 c ---[20628]---> Sorter-cost: 484 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20627]---> Sorter-cost: 456 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20626]---> Sorter-cost: 341 Base: 2 2 2 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 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 2 2 2 c ---[20571]---> Sorter-cost: 250 Base: 2 2 2 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 2 2 2 11 c ---[20569]---> Sorter-cost: 359 Base: 2 2 2 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 2 2 2 3 c ---[20567]---> BDD-cost: 100 c ---[20566]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 c ---[20565]---> Sorter-cost: 641 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20564]---> BDD-cost: 75 c ---[20563]---> Sorter-cost: 4916 Base: 2 2 2 2 2 2 2 2 5 2 2 2 3 3 3 5 3 3 2 2 c ---[20562]---> BDD-cost: 3 c ---[20561]---> Sorter-cost: 366 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[20560]---> BDD-cost: 5 c ---[20558]---> BDD-cost: 72 c ---[20556]---> BDD-cost: 4 c ---[20555]---> Sorter-cost: 667 Base: 2 2 2 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: 81 c ---[20547]---> BDD-cost: 20 c ---[20546]---> Sorter-cost: 241 Base: 2 2 2 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 2 2 2 3 5 c ---[20537]---> Sorter-cost: 531 Base: 2 2 2 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 2 2 2 c ---[20534]---> Sorter-cost: 320 Base: 2 2 2 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 2 2 2 c ---[20532]---> BDD-cost: 99 c ---[20531]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20530]---> BDD-cost: 108 c ---[20529]---> BDD-cost: 3 c ---[20528]---> BDD-cost: 67 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: 480 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20476]---> BDD-cost: 79 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: 458 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20458]---> BDD-cost: 22 c ---[20457]---> Sorter-cost: 375 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[20452]---> Sorter-cost: 4916 Base: 2 2 2 2 2 2 2 2 5 2 2 2 3 3 3 5 3 3 2 2 c ---[20451]---> BDD-cost: 3 c ---[20448]---> BDD-cost: 13 c ---[20446]---> BDD-cost: 13 c ---[20445]---> BDD-cost: 38 c ---[20444]---> BDD-cost: 123 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 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]--->
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/30349/stat): 30349 (minisat+_script) R 30348 30349 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788526820 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/30349/statm): 174 3 169 147 0 27 0 [pid=30349] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=30350 New process pid=30351 New process pid=30352 execve syscall for /bin/sed executable One traced child (pid=30351) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=30352) exited with status: 0 One traced child (pid=30350) exited with status: 0 New process pid=30353 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-msc98-ip.opb One traced child (pid=30353) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=30354 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-msc98-ip.opb [startup+10.0043 s] Raw data (loadavg): 0.93 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 4038 0 0 0 937 27 0 0 25 0 1 0 1788526832 18423808 3931 4294967295 134512640 135167914 3221224448 3221223264 134843139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30354/statm): 4498 3931 162 162 0 4336 0 [pid=30354] vsize: 17992 Current children cumulated CPU time (s) 9.69 Current children cumulated vsize (Kb) 20120 [startup+20.0054 s] Raw data (loadavg): 0.94 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 1908 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221219704 134693740 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 19.55 Current children cumulated vsize (Kb) 29724 [startup+30.0064 s] Raw data (loadavg): 0.95 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 2907 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220384 134849110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 29.54 Current children cumulated vsize (Kb) 29724 [startup+40.0074 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 3907 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220208 134849082 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 39.54 Current children cumulated vsize (Kb) 29724 [startup+50.0085 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 4908 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220560 134843400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 49.55 Current children cumulated vsize (Kb) 29724 [startup+60.0095 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 5908 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220224 134693561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 59.55 Current children cumulated vsize (Kb) 29724 [startup+70.0105 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 6908 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220208 134849196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 69.55 Current children cumulated vsize (Kb) 29724 [startup+80.0125 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 7908 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220936 134693553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 79.55 Current children cumulated vsize (Kb) 29724 [startup+90.0135 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 8909 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221219952 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 89.56 Current children cumulated vsize (Kb) 29724 [startup+100.015 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 9909 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220480 134845930 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 99.56 Current children cumulated vsize (Kb) 29724 [startup+110.016 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 10909 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221221376 134844736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 109.56 Current children cumulated vsize (Kb) 29724 [startup+120.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 11909 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220432 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 119.56 Current children cumulated vsize (Kb) 29724 [startup+130.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 12910 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220800 134844720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 129.57 Current children cumulated vsize (Kb) 29724 [startup+140.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 13910 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221221488 134629024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 139.57 Current children cumulated vsize (Kb) 29724 [startup+150.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 14910 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220684 134843002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 149.57 Current children cumulated vsize (Kb) 29724 [startup+160.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 15910 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221221264 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 159.57 Current children cumulated vsize (Kb) 29724 [startup+170.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 16911 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220576 134849122 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 169.58 Current children cumulated vsize (Kb) 29724 [startup+180.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 17911 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221221456 134849061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 179.58 Current children cumulated vsize (Kb) 29724 [startup+190.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 18911 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220412 134843033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 189.58 Current children cumulated vsize (Kb) 29724 [startup+200.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 19911 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220848 134844718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 199.58 Current children cumulated vsize (Kb) 29724 [startup+210.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6657 0 0 0 20912 42 0 0 25 0 1 0 1788526832 28258304 6338 4294967295 134512640 135167914 3221224448 3221220848 134696766 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 6899 6338 162 162 0 6737 0 [pid=30354] vsize: 27596 Current children cumulated CPU time (s) 209.59 Current children cumulated vsize (Kb) 29724 [startup+220.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 21911 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220176 134722532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 219.59 Current children cumulated vsize (Kb) 30184 [startup+230.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 22911 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220320 134844725 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 229.59 Current children cumulated vsize (Kb) 30184 [startup+240.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 23912 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220080 134844718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 239.6 Current children cumulated vsize (Kb) 30184 [startup+250.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 24912 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220608 134844653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 249.6 Current children cumulated vsize (Kb) 30184 [startup+260.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 25912 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220196 134845938 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 259.6 Current children cumulated vsize (Kb) 30184 [startup+270.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 26913 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220404 134523556 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 269.61 Current children cumulated vsize (Kb) 30184 [startup+280.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 27913 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220760 134693744 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 279.61 Current children cumulated vsize (Kb) 30184 [startup+290.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 28913 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220348 134849088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 289.61 Current children cumulated vsize (Kb) 30184 [startup+300.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 29913 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221221772 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 299.61 Current children cumulated vsize (Kb) 30184 [startup+310.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 30913 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220848 134844718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 309.61 Current children cumulated vsize (Kb) 30184 [startup+320.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 31914 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221221408 134720472 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 319.62 Current children cumulated vsize (Kb) 30184 [startup+330.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 32914 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220764 134849056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 329.62 Current children cumulated vsize (Kb) 30184 [startup+340.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 33914 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220784 134845888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 339.62 Current children cumulated vsize (Kb) 30184 [startup+350.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 34914 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220560 134849187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 349.62 Current children cumulated vsize (Kb) 30184 [startup+360.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 35915 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221220924 134696566 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 359.63 Current children cumulated vsize (Kb) 30184 [startup+370.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 36915 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221221088 134849102 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 369.63 Current children cumulated vsize (Kb) 30184 [startup+380.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 37915 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221221452 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 379.63 Current children cumulated vsize (Kb) 30184 [startup+390.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 38915 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221221104 134693576 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 389.63 Current children cumulated vsize (Kb) 30184 [startup+400.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 39916 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221221088 134849099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 399.64 Current children cumulated vsize (Kb) 30184 [startup+410.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6832 0 0 0 40916 43 0 0 25 0 1 0 1788526832 28729344 6439 4294967295 134512640 135167914 3221224448 3221221440 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7014 6439 162 162 0 6852 0 [pid=30354] vsize: 28056 Current children cumulated CPU time (s) 409.64 Current children cumulated vsize (Kb) 30184 [startup+420.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 41914 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221220144 134696658 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 419.63 Current children cumulated vsize (Kb) 30836 [startup+430.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 42915 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221219856 134694532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 429.64 Current children cumulated vsize (Kb) 30836 [startup+440.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 43915 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221220156 134843002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 439.64 Current children cumulated vsize (Kb) 30836 [startup+450.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 44915 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221220480 134718181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 449.64 Current children cumulated vsize (Kb) 30836 [startup+460.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 45915 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221220736 134694504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 459.64 Current children cumulated vsize (Kb) 30836 [startup+470.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 46915 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221220408 134849087 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 469.64 Current children cumulated vsize (Kb) 30836 [startup+480.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 47916 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221221024 134843010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 479.65 Current children cumulated vsize (Kb) 30836 [startup+490.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 48916 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221220732 134722208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 489.65 Current children cumulated vsize (Kb) 30836 [startup+500.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 49916 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221221116 134849088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 499.65 Current children cumulated vsize (Kb) 30836 [startup+510.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 50916 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221221124 134629227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 509.65 Current children cumulated vsize (Kb) 30836 [startup+520.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 51917 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221220880 134849122 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 519.66 Current children cumulated vsize (Kb) 30836 [startup+530.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 52917 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221221600 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 529.66 Current children cumulated vsize (Kb) 30836 [startup+540.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 53917 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221221612 134722231 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 539.66 Current children cumulated vsize (Kb) 30836 [startup+550.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 54917 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221220560 134694392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 549.66 Current children cumulated vsize (Kb) 30836 [startup+560.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 55918 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221220948 134629088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 559.67 Current children cumulated vsize (Kb) 30836 [startup+570.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 56918 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221221464 134843032 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 569.67 Current children cumulated vsize (Kb) 30836 [startup+580.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 57918 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221221200 134844706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 579.67 Current children cumulated vsize (Kb) 30836 [startup+590.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 58918 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221220736 134843139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 589.67 Current children cumulated vsize (Kb) 30836 [startup+600.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 6969 0 0 0 59918 44 0 0 25 0 1 0 1788526832 29396992 6544 4294967295 134512640 135167914 3221224448 3221221296 134629373 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7177 6544 162 162 0 7015 0 [pid=30354] vsize: 28708 Current children cumulated CPU time (s) 599.67 Current children cumulated vsize (Kb) 30836 [startup+610.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7150 0 0 0 60918 44 0 0 25 0 1 0 1788526832 29732864 6642 4294967295 134512640 135167914 3221224448 3221222828 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7259 6642 162 162 0 7097 0 [pid=30354] vsize: 29036 Current children cumulated CPU time (s) 609.67 Current children cumulated vsize (Kb) 31164 [startup+620.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 61916 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221220256 134845903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 619.66 Current children cumulated vsize (Kb) 31484 [startup+630.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 62917 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221219628 134723262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 629.67 Current children cumulated vsize (Kb) 31484 [startup+640.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 63917 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221220672 134845918 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 639.67 Current children cumulated vsize (Kb) 31484 [startup+650.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 64917 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221220320 134845933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 649.67 Current children cumulated vsize (Kb) 31484 [startup+660.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 65917 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221220540 134845940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 659.67 Current children cumulated vsize (Kb) 31484 [startup+670.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 66918 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221220400 134693576 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 669.68 Current children cumulated vsize (Kb) 31484 [startup+680.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 67918 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221220828 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 679.68 Current children cumulated vsize (Kb) 31484 [startup+690.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 68918 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221220920 134722513 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 689.68 Current children cumulated vsize (Kb) 31484 [startup+700.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 69919 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221221452 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 699.69 Current children cumulated vsize (Kb) 31484 [startup+710.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 70919 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221220832 134845927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 709.69 Current children cumulated vsize (Kb) 31484 [startup+720.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 71919 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221220736 134849122 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 719.69 Current children cumulated vsize (Kb) 31484 [startup+730.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 72919 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221221184 134845930 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 729.69 Current children cumulated vsize (Kb) 31484 [startup+740.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 73919 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221220480 134845913 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 739.69 Current children cumulated vsize (Kb) 31484 [startup+750.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 74920 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221220880 134695298 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 749.7 Current children cumulated vsize (Kb) 31484 [startup+760.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 75920 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221221468 134694320 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 759.7 Current children cumulated vsize (Kb) 31484 [startup+770.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 76920 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221221056 134843001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 769.7 Current children cumulated vsize (Kb) 31484 [startup+780.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 77921 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221220912 134849061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 779.71 Current children cumulated vsize (Kb) 31484 [startup+790.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 78921 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221221448 134722657 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 789.71 Current children cumulated vsize (Kb) 31484 [startup+800.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7291 0 0 0 79921 45 0 0 25 0 1 0 1788526832 30060544 6751 4294967295 134512640 135167914 3221224448 3221221376 134696781 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7339 6751 162 162 0 7177 0 [pid=30354] vsize: 29356 Current children cumulated CPU time (s) 799.71 Current children cumulated vsize (Kb) 31484 [startup+810.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 80920 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221220056 134849057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 809.7 Current children cumulated vsize (Kb) 31704 [startup+820.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 81921 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221220368 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 819.71 Current children cumulated vsize (Kb) 31704 [startup+830.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 82921 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221220736 134843026 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 829.71 Current children cumulated vsize (Kb) 31704 [startup+840.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 83921 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221220672 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 839.71 Current children cumulated vsize (Kb) 31704 [startup+850.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 84921 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221220400 134849061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 849.71 Current children cumulated vsize (Kb) 31704 [startup+860.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 85922 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221220704 134693570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 859.72 Current children cumulated vsize (Kb) 31704 [startup+870.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 86922 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221220912 134849102 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 869.72 Current children cumulated vsize (Kb) 31704 [startup+880.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 87922 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221220784 134629108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 879.72 Current children cumulated vsize (Kb) 31704 [startup+890.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 88922 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221220924 134722660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 889.72 Current children cumulated vsize (Kb) 31704 [startup+900.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 89923 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221221772 134844675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 899.73 Current children cumulated vsize (Kb) 31704 [startup+910.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 90923 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221220704 134722539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 909.73 Current children cumulated vsize (Kb) 31704 [startup+920.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 91923 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221221040 134696197 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 919.73 Current children cumulated vsize (Kb) 31704 [startup+930.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 92923 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221221652 134629284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 929.73 Current children cumulated vsize (Kb) 31704 [startup+940.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 93924 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221221088 134849096 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 939.74 Current children cumulated vsize (Kb) 31704 [startup+950.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 94924 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221221904 134844653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 949.74 Current children cumulated vsize (Kb) 31704 [startup+960.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 95924 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221220736 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 959.74 Current children cumulated vsize (Kb) 31704 [startup+970.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 96924 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221221616 134849092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 969.74 Current children cumulated vsize (Kb) 31704 [startup+980.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 97925 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221221200 134843064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 979.75 Current children cumulated vsize (Kb) 31704 [startup+990.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 98925 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221221024 134845930 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 989.75 Current children cumulated vsize (Kb) 31704 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7411 0 0 0 99925 45 0 0 25 0 1 0 1788526832 30285824 6838 4294967295 134512640 135167914 3221224448 3221220832 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7394 6838 162 162 0 7232 0 [pid=30354] vsize: 29576 Current children cumulated CPU time (s) 999.75 Current children cumulated vsize (Kb) 31704 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 100924 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221220764 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1009.75 Current children cumulated vsize (Kb) 32636 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 101925 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221220432 134844703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1019.76 Current children cumulated vsize (Kb) 32636 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 102925 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221219980 134723285 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1029.76 Current children cumulated vsize (Kb) 32636 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 103925 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221220848 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1039.76 Current children cumulated vsize (Kb) 32636 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.91 3/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 104925 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221220736 134843064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1049.76 Current children cumulated vsize (Kb) 32636 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 105926 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221221120 134629049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1059.77 Current children cumulated vsize (Kb) 32636 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 106926 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221221376 134843113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1069.77 Current children cumulated vsize (Kb) 32636 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 107926 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221221116 134693816 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1079.77 Current children cumulated vsize (Kb) 32636 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 108927 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221221440 134849187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1089.78 Current children cumulated vsize (Kb) 32636 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 109927 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221221312 134629108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1099.78 Current children cumulated vsize (Kb) 32636 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 110927 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221221228 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1109.78 Current children cumulated vsize (Kb) 32636 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 111927 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221220568 134722657 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1119.78 Current children cumulated vsize (Kb) 32636 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 112928 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221221244 134844632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1129.79 Current children cumulated vsize (Kb) 32636 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 113928 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221220656 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1139.79 Current children cumulated vsize (Kb) 32636 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 114928 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221220960 134629419 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1149.79 Current children cumulated vsize (Kb) 32636 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 115928 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221220688 134843400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1159.79 Current children cumulated vsize (Kb) 32636 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 116929 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221221440 134694545 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1169.8 Current children cumulated vsize (Kb) 32636 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 117929 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221220928 134693566 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1179.8 Current children cumulated vsize (Kb) 32636 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 118929 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221221744 134849108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1189.8 Current children cumulated vsize (Kb) 32636 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7507 0 0 0 119929 46 0 0 25 0 1 0 1788526832 31240192 6902 4294967295 134512640 135167914 3221224448 3221221276 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7627 6902 162 162 0 7465 0 [pid=30354] vsize: 30508 Current children cumulated CPU time (s) 1199.8 Current children cumulated vsize (Kb) 32636 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7590 0 0 0 120929 46 0 0 25 0 1 0 1788526832 31502336 6985 4294967295 134512640 135167914 3221224448 3221220304 134845901 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7691 6985 162 162 0 7529 0 [pid=30354] vsize: 30764 Current children cumulated CPU time (s) 1209.8 Current children cumulated vsize (Kb) 32892 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 30354 Raw data (/proc/30349/stat): 30349 (minisat+_script) S 30348 30349 6847 0 -1 0 314 330 0 0 0 1 2 2 19 0 1 0 1788526820 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/30349/statm): 532 234 485 147 0 385 0 [pid=30349] vsize: 2128 Raw data (/proc/30354/stat): 30354 (minisat+_bignum) R 30349 30349 6847 0 -1 0 7590 0 0 0 120929 46 0 0 25 0 1 0 1788526832 31502336 6985 4294967295 134512640 135167914 3221224448 3221220144 134844731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/30354/statm): 7691 6985 162 162 0 7529 0 [pid=30354] vsize: 30764 Current children cumulated CPU time (s) 1209.8 Current children cumulated vsize (Kb) 32892 Sending SIGTERM to -30349 Sleeping 2 seconds One traced child (pid=30349) ended because it received signal 15 (SIGTERM) One traced child (pid=30354) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.13 CPU time (s): 1209.78 CPU user time (s): 1209.3 CPU system time (s): 0.482926 CPU usage (%): 99.9709 Max. virtual memory (cumulated for all children) (Kb): 32892
ERROR: no interpretation found !