| Name | web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-2.opb |
| MD5SUM | 5e8935802e4aa1a1ac8f2a923d842947 |
| Bench Category | optimization, small integers (OPTSMALLINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 26439 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 6892 |
| Biggest coefficient in the objective function | 667 |
| Number of bits for the biggest coefficient in the objective function | 10 |
| Sum of the numbers in the objective function | 371779 |
| Number of bits of the sum of numbers in the objective function | 19 |
| Biggest number in a constraint | 667 |
| Number of bits of the biggest number in a constraint | 10 |
| Biggest sum of numbers in a constraint | 371779 |
| Number of bits of the biggest sum of numbers | 19 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1262.02 |
| Number of variables | 8405 |
| Total number of constraints | 19071 |
| Number of constraints which are clauses | 9918 |
| Number of constraints which are cardinality constraints (but not clauses) | 9153 |
| Number of constraints which are nor clauses,nor cardinality constraints | 0 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 351 |
LAUNCH ON wulflinc20 THE 2005-09-18 19:05:30 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2725 boxname=wulflinc20 idbench=381 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 5e8935802e4aa1a1ac8f2a923d842947 /oldhome/oroussel/tmp/wulflinc20/normalized-ss97-2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-ss97-2.opb IDLAUNCH: 2725 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 911192 kB Buffers: 35412 kB Cached: 59024 kB SwapCached: 832 kB Active: 67468 kB Inactive: 29624 kB HighTotal: 131008 kB HighFree: 68628 kB LowTotal: 903652 kB LowFree: 842564 kB SwapTotal: 2097892 kB SwapFree: 2096604 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5732 kB Slab: 20700 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 19:25:40 (client local time) WITH STATUS 0 IN 1205.27 SECONDS stats: 2725 7 1205.27 0
c Parsing PB file... c Converting 11366 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################ c -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................. c ---[11365]---> Adder-cost: 686 maxlim: 311 bits: 9/9 c ---[11364]---> Adder-cost: 686 maxlim: 311 bits: 9/9 c ---[11363]---> Adder-cost: 686 maxlim: 311 bits: 9/9 c ---[11362]---> Adder-cost: 686 maxlim: 311 bits: 9/9 c ---[11361]---> Adder-cost: 686 maxlim: 311 bits: 9/9 c ---[11360]---> Adder-cost: 686 maxlim: 311 bits: 9/9 c ---[11359]---> Adder-cost: 686 maxlim: 311 bits: 9/9 c ---[11358]---> Adder-cost: 686 maxlim: 311 bits: 9/9 c ---[11357]---> Adder-cost: 686 maxlim: 311 bits: 9/9 c ---[11356]---> Adder-cost: 686 maxlim: 311 bits: 9/9 c ---[11355]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11354]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11353]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11352]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11351]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11350]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11349]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11348]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11347]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11346]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11345]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11344]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11343]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11342]---> Adder-cost: 688 maxlim: 321 bits: 9/9 c ---[11341]---> Adder-cost: 46 maxlim: 26 bits: 6/5 c ---[11340]---> Adder-cost: 46 maxlim: 26 bits: 6/5 c ---[11339]---> Adder-cost: 46 maxlim: 26 bits: 6/5 c ---[11338]---> Adder-cost: 46 maxlim: 26 bits: 6/5 c ---[11337]---> Adder-cost: 46 maxlim: 26 bits: 6/5 c ---[11336]---> Adder-cost: 46 maxlim: 26 bits: 6/5 c ---[11335]---> Adder-cost: 46 maxlim: 26 bits: 6/5 c ---[11334]---> Adder-cost: 46 maxlim: 26 bits: 6/5 c ---[11333]---> Adder-cost: 46 maxlim: 26 bits: 6/5 c ---[11332]---> Adder-cost: 46 maxlim: 26 bits: 6/5 c ---[11331]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11330]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11329]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11328]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11327]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11326]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11325]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11324]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11323]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11322]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11321]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11320]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11319]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11318]---> Adder-cost: 9 maxlim: 21 bits: 6/5 c ---[11316]---> BDD-cost: 17 c ---[11314]---> BDD-cost: 25 c ---[11312]---> BDD-cost: 17 c ---[11310]---> BDD-cost: 25 c ---[11308]---> BDD-cost: 17 c ---[11306]---> BDD-cost: 25 c ---[11304]---> BDD-cost: 17 c ---[11302]---> BDD-cost: 25 c ---[11300]---> BDD-cost: 17 c ---[11298]---> BDD-cost: 25 c ---[11296]---> BDD-cost: 17 c ---[11294]---> BDD-cost: 25 c ---[11292]---> BDD-cost: 17 c ---[11290]---> BDD-cost: 25 c ---[11288]---> BDD-cost: 17 c ---[11286]---> BDD-cost: 25 c ---[11284]---> BDD-cost: 17 c ---[11282]---> BDD-cost: 25 c ---[11280]---> BDD-cost: 17 c ---[11278]---> BDD-cost: 25 c ---[11276]---> BDD-cost: 17 c ---[11274]---> BDD-cost: 25 c ---[11272]---> BDD-cost: 17 c ---[11270]---> BDD-cost: 25 c ---[11268]---> BDD-cost: 17 c ---[11266]---> BDD-cost: 25 c ---[11264]---> BDD-cost: 17 c ---[11262]---> BDD-cost: 25 c ---[11260]---> BDD-cost: 17 c ---[11258]---> BDD-cost: 25 c ---[11256]---> BDD-cost: 17 c ---[11254]---> BDD-cost: 25 c ---[11252]---> BDD-cost: 17 c ---[11250]---> BDD-cost: 25 c ---[11248]---> BDD-cost: 17 c ---[11246]---> BDD-cost: 25 c ---[11244]---> BDD-cost: 17 c ---[11242]---> BDD-cost: 25 c ---[11240]---> BDD-cost: 17 c ---[11238]---> BDD-cost: 25 c ---[11236]---> BDD-cost: 17 c ---[11234]---> BDD-cost: 25 c ---[11232]---> BDD-cost: 17 c ---[11230]---> BDD-cost: 25 c ---[11228]---> BDD-cost: 17 c ---[11226]---> BDD-cost: 25 c ---[11224]---> BDD-cost: 17 c ---[11222]---> BDD-cost: 25 c ---[11220]---> BDD-cost: 17 c ---[11218]---> BDD-cost: 25 c ---[11216]---> BDD-cost: 17 c ---[11214]---> BDD-cost: 25 c ---[11212]---> BDD-cost: 17 c ---[11210]---> BDD-cost: 25 c ---[11208]---> BDD-cost: 17 c ---[11206]---> BDD-cost: 25 c ---[11204]---> BDD-cost: 17 c ---[11202]---> BDD-cost: 25 c ---[11200]---> BDD-cost: 17 c ---[11198]---> BDD-cost: 25 c ---[11196]---> BDD-cost: 17 c ---[11194]---> BDD-cost: 25 c ---[11192]---> BDD-cost: 17 c ---[11190]---> BDD-cost: 25 c ---[11188]---> BDD-cost: 17 c ---[11186]---> BDD-cost: 25 c ---[11184]---> BDD-cost: 17 c ---[11182]---> BDD-cost: 25 c ---[11180]---> BDD-cost: 17 c ---[11178]---> BDD-cost: 25 c ---[11176]---> BDD-cost: 17 c ---[11174]---> BDD-cost: 25 c ---[11172]---> BDD-cost: 17 c ---[11170]---> BDD-cost: 25 c ---[11168]---> BDD-cost: 17 c ---[11166]---> BDD-cost: 25 c ---[11164]---> BDD-cost: 17 c ---[11162]---> BDD-cost: 25 c ---[11160]---> BDD-cost: 17 c ---[11158]---> BDD-cost: 25 c ---[11156]---> BDD-cost: 17 c ---[11154]---> BDD-cost: 25 c ---[11152]---> BDD-cost: 17 c ---[11150]---> BDD-cost: 25 c ---[11148]---> BDD-cost: 17 c ---[11146]---> BDD-cost: 25 c ---[11144]---> BDD-cost: 17 c ---[11142]---> BDD-cost: 25 c ---[11140]---> BDD-cost: 17 c ---[11138]---> BDD-cost: 25 c ---[11136]---> BDD-cost: 17 c ---[11134]---> BDD-cost: 25 c ---[11132]---> BDD-cost: 17 c ---[11130]---> BDD-cost: 25 c ---[11128]---> BDD-cost: 17 c ---[11126]---> BDD-cost: 25 c ---[11124]---> BDD-cost: 17 c ---[11122]---> BDD-cost: 25 c ---[11120]---> BDD-cost: 17 c ---[11118]---> BDD-cost: 25 c ---[11116]---> BDD-cost: 17 c ---[11114]---> BDD-cost: 25 c ---[11112]---> BDD-cost: 17 c ---[11110]---> BDD-cost: 25 c ---[11108]---> BDD-cost: 17 c ---[11106]---> BDD-cost: 25 c ---[11104]---> BDD-cost: 17 c ---[11102]---> BDD-cost: 25 c ---[11100]---> BDD-cost: 25 c ---[11098]---> BDD-cost: 17 c ---[11096]---> BDD-cost: 25 c ---[11094]---> BDD-cost: 17 c ---[11092]---> BDD-cost: 25 c ---[11090]---> BDD-cost: 17 c ---[11088]---> BDD-cost: 25 c ---[11086]---> BDD-cost: 17 c ---[11084]---> BDD-cost: 25 c ---[11082]---> BDD-cost: 17 c ---[11080]---> BDD-cost: 25 c ---[11078]---> BDD-cost: 17 c ---[11076]---> BDD-cost: 25 c ---[11074]---> BDD-cost: 17 c ---[11072]---> BDD-cost: 25 c ---[11070]---> BDD-cost: 25 c ---[11068]---> BDD-cost: 17 c ---[11066]---> BDD-cost: 25 c ---[11064]---> BDD-cost: 17 c ---[11062]---> BDD-cost: 25 c ---[11060]---> BDD-cost: 17 c ---[11058]---> BDD-cost: 25 c ---[11056]---> BDD-cost: 17 c ---[11054]---> BDD-cost: 25 c ---[11052]---> BDD-cost: 17 c ---[11050]---> BDD-cost: 25 c ---[11048]---> BDD-cost: 17 c ---[11046]---> BDD-cost: 25 c ---[11044]---> BDD-cost: 17 c ---[11042]---> BDD-cost: 25 c ---[11040]---> BDD-cost: 17 c ---[11038]---> BDD-cost: 25 c ---[11036]---> BDD-cost: 17 c ---[11034]---> BDD-cost: 25 c ---[11032]---> BDD-cost: 17 c ---[11030]---> BDD-cost: 25 c ---[11028]---> BDD-cost: 17 c ---[11026]---> BDD-cost: 25 c ---[11024]---> BDD-cost: 17 c ---[11022]---> BDD-cost: 25 c ---[11020]---> BDD-cost: 17 c ---[11018]---> BDD-cost: 25 c ---[11016]---> BDD-cost: 17 c ---[11014]---> BDD-cost: 25 c ---[11012]---> BDD-cost: 17 c ---[11010]---> BDD-cost: 25 c ---[11008]---> BDD-cost: 25 c ---[11006]---> BDD-cost: 17 c ---[11004]---> BDD-cost: 25 c ---[11002]---> BDD-cost: 17 c ---[11000]---> BDD-cost: 25 c ---[10998]---> BDD-cost: 17 c ---[10996]---> BDD-cost: 25 c ---[10994]---> BDD-cost: 17 c ---[10992]---> BDD-cost: 25 c ---[10990]---> BDD-cost: 17 c ---[10988]---> BDD-cost: 25 c ---[10986]---> BDD-cost: 17 c ---[10984]---> BDD-cost: 25 c ---[10982]---> BDD-cost: 17 c ---[10980]---> BDD-cost: 25 c ---[10978]---> BDD-cost: 17 c ---[10976]---> BDD-cost: 25 c ---[10974]---> BDD-cost: 17 c ---[10972]---> BDD-cost: 25 c ---[10970]---> BDD-cost: 17 c ---[10968]---> BDD-cost: 25 c ---[10966]---> BDD-cost: 17 c ---[10964]---> BDD-cost: 25 c ---[10962]---> BDD-cost: 17 c ---[10960]---> BDD-cost: 25 c ---[10958]---> BDD-cost: 17 c ---[10956]---> BDD-cost: 25 c ---[10954]---> BDD-cost: 17 c ---[10952]---> BDD-cost: 25 c ---[10950]---> BDD-cost: 17 c ---[10948]---> BDD-cost: 25 c ---[10946]---> BDD-cost: 17 c ---[10944]---> BDD-cost: 25 c ---[10942]---> BDD-cost: 17 c ---[10940]---> BDD-cost: 25 c ---[10938]---> BDD-cost: 17 c ---[10936]---> BDD-cost: 25 c ---[10934]---> BDD-cost: 17 c ---[10932]---> BDD-cost: 25 c ---[10930]---> BDD-cost: 17 c ---[10928]---> BDD-cost: 25 c ---[10926]---> BDD-cost: 17 c ---[10924]---> BDD-cost: 25 c ---[10922]---> BDD-cost: 17 c ---[10920]---> BDD-cost: 25 c ---[10918]---> BDD-cost: 17 c ---[10916]---> BDD-cost: 25 c ---[10914]---> BDD-cost: 17 c ---[10912]---> BDD-cost: 25 c ---[10910]---> BDD-cost: 17 c ---[10908]---> BDD-cost: 25 c ---[10906]---> BDD-cost: 25 c ---[10904]---> BDD-cost: 17 c ---[10902]---> BDD-cost: 25 c ---[10900]---> BDD-cost: 17 c ---[10898]---> BDD-cost: 25 c ---[10896]---> BDD-cost: 17 c ---[10894]---> BDD-cost: 25 c ---[10892]---> BDD-cost: 17 c ---[10890]---> BDD-cost: 25 c ---[10888]---> BDD-cost: 17 c ---[10886]---> BDD-cost: 25 c ---[10884]---> BDD-cost: 17 c ---[10882]---> BDD-cost: 25 c ---[10880]---> BDD-cost: 17 c ---[10878]---> BDD-cost: 25 c ---[10876]---> BDD-cost: 17 c ---[10874]---> BDD-cost: 25 c ---[10872]---> BDD-cost: 17 c ---[10870]---> BDD-cost: 25 c ---[10868]---> BDD-cost: 17 c ---[10866]---> BDD-cost: 25 c ---[10864]---> BDD-cost: 17 c ---[10862]---> BDD-cost: 25 c ---[10860]---> BDD-cost: 17 c ---[10858]---> BDD-cost: 25 c ---[10856]---> BDD-cost: 17 c ---[10854]---> BDD-cost: 25 c ---[10852]---> BDD-cost: 17 c ---[10850]---> BDD-cost: 25 c ---[10848]---> BDD-cost: 17 c ---[10846]---> BDD-cost: 25 c ---[10844]---> BDD-cost: 17 c ---[10842]---> BDD-cost: 25 c ---[10840]---> BDD-cost: 17 c ---[10838]---> BDD-cost: 25 c ---[10836]---> BDD-cost: 17 c ---[10834]---> BDD-cost: 25 c ---[10832]---> BDD-cost: 17 c ---[10830]---> BDD-cost: 25 c ---[10828]---> BDD-cost: 17 c ---[10826]---> BDD-cost: 25 c ---[10824]---> BDD-cost: 17 c ---[10822]---> BDD-cost: 25 c ---[10820]---> BDD-cost: 17 c ---[10818]---> BDD-cost: 25 c ---[10816]---> BDD-cost: 17 c ---[10814]---> BDD-cost: 25 c ---[10812]---> BDD-cost: 17 c ---[10810]---> BDD-cost: 25 c ---[10808]---> BDD-cost: 17 c ---[10806]---> BDD-cost: 25 c ---[10804]---> BDD-cost: 17 c ---[10802]---> BDD-cost: 25 c ---[10800]---> BDD-cost: 17 c ---[10798]---> BDD-cost: 25 c ---[10796]---> BDD-cost: 17 c ---[10794]---> BDD-cost: 25 c ---[10792]---> BDD-cost: 17 c ---[10790]---> BDD-cost: 25 c ---[10788]---> BDD-cost: 17 c ---[10786]---> BDD-cost: 25 c ---[10784]---> BDD-cost: 17 c ---[10782]---> BDD-cost: 25 c ---[10780]---> BDD-cost: 17 c ---[10778]---> BDD-cost: 25 c ---[10776]---> BDD-cost: 17 c ---[10774]---> BDD-cost: 25 c ---[10772]---> BDD-cost: 17 c ---[10770]---> BDD-cost: 25 c ---[10768]---> BDD-cost: 17 c ---[10766]---> BDD-cost: 25 c ---[10764]---> BDD-cost: 17 c ---[10762]---> BDD-cost: 25 c ---[10760]---> BDD-cost: 17 c ---[10758]---> BDD-cost: 25 c ---[10756]---> BDD-cost: 17 c ---[10754]---> BDD-cost: 25 c ---[10752]---> BDD-cost: 17 c ---[10750]---> BDD-cost: 25 c ---[10748]---> BDD-cost: 17 c ---[10746]---> BDD-cost: 25 c ---[10744]---> BDD-cost: 17 c ---[10742]---> BDD-cost: 25 c ---[10740]---> BDD-cost: 17 c ---[10738]---> BDD-cost: 25 c ---[10736]---> BDD-cost: 17 c ---[10734]---> BDD-cost: 25 c ---[10732]---> BDD-cost: 17 c ---[10730]---> BDD-cost: 25 c ---[10728]---> BDD-cost: 17 c ---[10726]---> BDD-cost: 25 c ---[10724]---> BDD-cost: 17 c ---[10722]---> BDD-cost: 25 c ---[10720]---> BDD-cost: 17 c ---[10718]---> BDD-cost: 25 c ---[10716]---> BDD-cost: 17 c ---[10714]---> BDD-cost: 25 c ---[10712]---> BDD-cost: 17 c ---[10710]---> BDD-cost: 25 c ---[10708]---> BDD-cost: 17 c ---[10706]---> BDD-cost: 25 c ---[10704]---> BDD-cost: 17 c ---[10702]---> BDD-cost: 25 c ---[10700]---> BDD-cost: 17 c ---[10698]---> BDD-cost: 25 c ---[10696]---> BDD-cost: 17 c ---[10694]---> BDD-cost: 25 c ---[10692]---> BDD-cost: 17 c ---[10690]---> BDD-cost: 25 c ---[10688]---> BDD-cost: 17 c ---[10686]---> BDD-cost: 25 c ---[10684]---> BDD-cost: 17 c ---[10682]---> BDD-cost: 25 c ---[10680]---> BDD-cost: 17 c ---[10678]---> BDD-cost: 25 c ---[10676]---> BDD-cost: 17 c ---[10674]---> BDD-cost: 25 c ---[10672]---> BDD-cost: 17 c ---[10670]---> BDD-cost: 25 c ---[10668]---> BDD-cost: 17 c ---[10666]---> BDD-cost: 25 c ---[10664]---> BDD-cost: 17 c ---[10662]---> BDD-cost: 25 c ---[10660]---> BDD-cost: 17 c ---[10658]---> BDD-cost: 25 c ---[10656]---> BDD-cost: 17 c ---[10654]---> BDD-cost: 25 c ---[10652]---> BDD-cost: 17 c ---[10650]---> BDD-cost: 25 c ---[10648]---> BDD-cost: 17 c ---[10646]---> BDD-cost: 25 c ---[10644]---> BDD-cost: 17 c ---[10642]---> BDD-cost: 25 c ---[10640]---> BDD-cost: 17 c ---[10638]---> BDD-cost: 25 c ---[10636]---> BDD-cost: 17 c ---[10634]---> BDD-cost: 25 c ---[10632]---> BDD-cost: 17 c ---[10630]---> BDD-cost: 25 c ---[10628]---> BDD-cost: 17 c ---[10626]---> BDD-cost: 25 c ---[10624]---> BDD-cost: 17 c ---[10622]---> BDD-cost: 25 c ---[10620]---> BDD-cost: 25 c ---[10618]---> BDD-cost: 17 c ---[10616]---> BDD-cost: 25 c ---[10614]---> BDD-cost: 17 c ---[10612]---> BDD-cost: 25 c ---[10610]---> BDD-cost: 17 c ---[10608]---> BDD-cost: 25 c ---[10606]---> BDD-cost: 17 c ---[10604]---> BDD-cost: 25 c ---[10602]---> BDD-cost: 17 c ---[10600]---> BDD-cost: 25 c ---[10598]---> BDD-cost: 17 c ---[10596]---> BDD-cost: 25 c ---[10594]---> BDD-cost: 17 c ---[10592]---> BDD-cost: 25 c ---[10590]---> BDD-cost: 17 c ---[10588]---> BDD-cost: 17 c ---[10586]---> BDD-cost: 25 c ---[10584]---> BDD-cost: 17 c ---[10582]---> BDD-cost: 25 c ---[10580]---> BDD-cost: 17 c ---[10578]---> BDD-cost: 25 c ---[10576]---> BDD-cost: 17 c ---[10574]---> BDD-cost: 25 c ---[10572]---> BDD-cost: 17 c ---[10570]---> BDD-cost: 25 c ---[10568]---> BDD-cost: 17 c ---[10566]---> BDD-cost: 25 c ---[10564]---> BDD-cost: 17 c ---[10562]---> BDD-cost: 25 c ---[10560]---> BDD-cost: 17 c ---[10558]---> BDD-cost: 25 c ---[10556]---> BDD-cost: 17 c ---[10554]---> BDD-cost: 25 c ---[10552]---> BDD-cost: 17 c ---[10550]---> BDD-cost: 25 c ---[10548]---> BDD-cost: 17 c ---[10546]---> BDD-cost: 25 c ---[10544]---> BDD-cost: 17 c ---[10542]---> BDD-cost: 25 c ---[10540]---> BDD-cost: 17 c ---[10538]---> BDD-cost: 25 c ---[10536]---> BDD-cost: 17 c ---[10534]---> BDD-cost: 25 c ---[10532]---> BDD-cost: 17 c ---[10530]---> BDD-cost: 25 c ---[10528]---> BDD-cost: 17 c ---[10526]---> BDD-cost: 25 c ---[10524]---> BDD-cost: 17 c ---[10522]---> BDD-cost: 25 c ---[10520]---> BDD-cost: 17 c ---[10518]---> BDD-cost: 25 c ---[10516]---> BDD-cost: 17 c ---[10514]---> BDD-cost: 25 c ---[10512]---> BDD-cost: 17 c ---[10510]---> BDD-cost: 25 c ---[10508]---> BDD-cost: 17 c ---[10506]---> BDD-cost: 25 c ---[10504]---> BDD-cost: 17 c ---[10502]---> BDD-cost: 25 c ---[10500]---> BDD-cost: 17 c ---[10498]---> BDD-cost: 25 c ---[10496]---> BDD-cost: 17 c ---[10494]---> BDD-cost: 25 c ---[10492]---> BDD-cost: 17 c ---[10490]---> BDD-cost: 25 c ---[10488]---> BDD-cost: 17 c ---[10486]---> BDD-cost: 25 c ---[10484]---> BDD-cost: 17 c ---[10482]---> BDD-cost: 25 c ---[10480]---> BDD-cost: 17 c ---[10478]---> BDD-cost: 25 c ---[10476]---> BDD-cost: 17 c ---[10474]---> BDD-cost: 25 c ---[10472]---> BDD-cost: 17 c ---[10470]---> BDD-cost: 25 c ---[10468]---> BDD-cost: 17 c ---[10466]---> BDD-cost: 25 c ---[10464]---> BDD-cost: 17 c ---[10462]---> BDD-cost: 25 c ---[10460]---> BDD-cost: 17 c ---[10458]---> BDD-cost: 25 c ---[10456]---> BDD-cost: 17 c ---[10454]---> BDD-cost: 25 c ---[10452]---> BDD-cost: 17 c ---[10450]---> BDD-cost: 25 c ---[10448]---> BDD-cost: 17 c ---[10446]---> BDD-cost: 25 c ---[10444]---> BDD-cost: 17 c ---[10442]---> BDD-cost: 25 c ---[10440]---> BDD-cost: 17 c ---[10438]---> BDD-cost: 25 c ---[10436]---> BDD-cost: 17 c ---[10434]---> BDD-cost: 25 c ---[10432]---> BDD-cost: 17 c ---[10430]---> BDD-cost: 25 c ---[10428]---> BDD-cost: 17 c ---[10426]---> BDD-cost: 25 c ---[10424]---> BDD-cost: 17 c ---[10422]---> BDD-cost: 25 c ---[10420]---> BDD-cost: 17 c ---[10418]---> BDD-cost: 25 c ---[10416]---> BDD-cost: 17 c ---[10414]---> BDD-cost: 25 c ---[10412]---> BDD-cost: 17 c ---[10410]---> BDD-cost: 25 c ---[10408]---> BDD-cost: 17 c ---[10406]---> BDD-cost: 17 c ---[10404]---> BDD-cost: 25 c ---[10402]---> BDD-cost: 17 c ---[10400]---> BDD-cost: 25 c ---[10398]---> BDD-cost: 17 c ---[10396]---> BDD-cost: 25 c ---[10394]---> BDD-cost: 17 c ---[10392]---> BDD-cost: 25 c ---[10390]---> BDD-cost: 17 c ---[10388]---> BDD-cost: 25 c ---[10386]---> BDD-cost: 17 c ---[10384]---> BDD-cost: 25 c ---[10382]---> BDD-cost: 17 c ---[10380]---> BDD-cost: 25 c ---[10378]---> BDD-cost: 17 c ---[10376]---> BDD-cost: 25 c ---[10374]---> BDD-cost: 17 c ---[10372]---> BDD-cost: 25 c ---[10370]---> BDD-cost: 17 c ---[10368]---> BDD-cost: 25 c ---[10366]---> BDD-cost: 17 c ---[10364]---> BDD-cost: 25 c ---[10362]---> BDD-cost: 17 c ---[10360]---> BDD-cost: 25 c ---[10358]---> BDD-cost: 17 c ---[10356]---> BDD-cost: 25 c ---[10354]---> BDD-cost: 17 c ---[10352]---> BDD-cost: 25 c ---[10350]---> BDD-cost: 17 c ---[10348]---> BDD-cost: 25 c ---[10346]---> BDD-cost: 17 c ---[10344]---> BDD-cost: 25 c ---[10342]---> BDD-cost: 17 c ---[10340]---> BDD-cost: 25 c ---[10338]---> BDD-cost: 17 c ---[10336]---> BDD-cost: 25 c ---[10334]---> BDD-cost: 17 c ---[10332]---> BDD-cost: 25 c ---[10330]---> BDD-cost: 17 c ---[10328]---> BDD-cost: 25 c ---[10326]---> BDD-cost: 17 c ---[10324]---> BDD-cost: 25 c ---[10322]---> BDD-cost: 17 c ---[10320]---> BDD-cost: 25 c ---[10318]---> BDD-cost: 17 c ---[10316]---> BDD-cost: 25 c ---[10314]---> BDD-cost: 17 c ---[10312]---> BDD-cost: 25 c ---[10310]---> BDD-cost: 17 c ---[10308]---> BDD-cost: 25 c ---[10306]---> BDD-cost: 17 c ---[10304]---> BDD-cost: 25 c ---[10302]---> BDD-cost: 17 c ---[10300]---> BDD-cost: 25 c ---[10298]---> BDD-cost: 17 c ---[10296]---> BDD-cost: 25 c ---[10294]---> BDD-cost: 17 c ---[10292]---> BDD-cost: 25 c ---[10290]---> BDD-cost: 17 c ---[10288]---> BDD-cost: 25 c ---[10286]---> BDD-cost: 17 c ---[10284]---> BDD-cost: 25 c ---[10282]---> BDD-cost: 17 c ---[10280]---> BDD-cost: 25 c ---[10278]---> BDD-cost: 17 c ---[10276]---> BDD-cost: 25 c ---[10274]---> BDD-cost: 17 c ---[10272]---> BDD-cost: 25 c ---[10270]---> BDD-cost: 17 c ---[10268]---> BDD-cost: 25 c ---[10266]---> BDD-cost: 17 c ---[10264]---> BDD-cost: 25 c ---[10262]---> BDD-cost: 17 c ---[10260]---> BDD-cost: 25 c ---[10258]---> BDD-cost: 17 c ---[10256]---> BDD-cost: 25 c ---[10254]---> BDD-cost: 17 c ---[10252]---> BDD-cost: 25 c ---[10250]---> BDD-cost: 17 c ---[10248]---> BDD-cost: 25 c ---[10246]---> BDD-cost: 17 c ---[10244]---> BDD-cost: 25 c ---[10242]---> BDD-cost: 17 c ---[10240]---> BDD-cost: 25 c ---[10238]---> BDD-cost: 17 c ---[10236]---> BDD-cost: 25 c ---[10234]---> BDD-cost: 17 c ---[10232]---> BDD-cost: 25 c ---[10230]---> BDD-cost: 17 c ---[10228]---> BDD-cost: 25 c ---[10226]---> BDD-cost: 17 c ---[10224]---> BDD-cost: 25 c ---[10222]---> BDD-cost: 17 c ---[10220]---> BDD-cost: 25 c ---[10218]---> BDD-cost: 17 c ---[10216]---> BDD-cost: 25 c ---[10214]---> BDD-cost: 17 c ---[10212]---> BDD-cost: 25 c ---[10210]---> BDD-cost: 25 c ---[10208]---> BDD-cost: 17 c ---[10206]---> BDD-cost: 25 c ---[10204]---> BDD-cost: 17 c ---[10202]---> BDD-cost: 25 c ---[10200]---> BDD-cost: 17 c ---[10198]---> BDD-cost: 25 c ---[10196]---> BDD-cost: 17 c ---[10194]---> BDD-cost: 25 c ---[10192]---> BDD-cost: 17 c ---[10190]---> BDD-cost: 25 c ---[10188]---> BDD-cost: 17 c ---[10186]---> BDD-cost: 25 c ---[10184]---> BDD-cost: 17 c ---[10182]---> BDD-cost: 25 c ---[10180]---> BDD-cost: 17 c ---[10178]---> BDD-cost: 25 c ---[10176]---> BDD-cost: 17 c ---[10174]---> BDD-cost: 25 c ---[10172]---> BDD-cost: 17 c ---[10170]---> BDD-cost: 25 c ---[10168]---> BDD-cost: 17 c ---[10166]---> BDD-cost: 25 c ---[10164]---> BDD-cost: 17 c ---[10162]---> BDD-cost: 25 c ---[10160]---> BDD-cost: 17 c ---[10158]---> BDD-cost: 25 c ---[10156]---> BDD-cost: 17 c ---[10154]---> BDD-cost: 25 c ---[10152]---> BDD-cost: 25 c ---[10150]---> BDD-cost: 17 c ---[10148]---> BDD-cost: 25 c ---[10146]---> BDD-cost: 17 c ---[10144]---> BDD-cost: 25 c ---[10142]---> BDD-cost: 17 c ---[10140]---> BDD-cost: 25 c ---[10138]---> BDD-cost: 17 c ---[10136]---> BDD-cost: 25 c ---[10134]---> BDD-cost: 17 c ---[10132]---> BDD-cost: 25 c ---[10130]---> BDD-cost: 17 c ---[10128]---> BDD-cost: 17 c ---[10126]---> BDD-cost: 25 c ---[10124]---> BDD-cost: 17 c ---[10122]---> BDD-cost: 25 c ---[10120]---> BDD-cost: 17 c ---[10118]---> BDD-cost: 25 c ---[10116]---> BDD-cost: 17 c ---[10114]---> BDD-cost: 25 c ---[10112]---> BDD-cost: 17 c ---[10110]---> BDD-cost: 25 c ---[10108]---> BDD-cost: 17 c ---[10106]---> BDD-cost: 25 c ---[10104]---> BDD-cost: 17 c ---[10102]---> BDD-cost: 25 c ---[10100]---> BDD-cost: 17 c ---[10098]---> BDD-cost: 25 c ---[10096]---> BDD-cost: 17 c ---[10094]---> BDD-cost: 25 c ---[10092]---> BDD-cost: 17 c ---[10090]---> BDD-cost: 25 c ---[10088]---> BDD-cost: 17 c ---[10086]---> BDD-cost: 25 c ---[10084]---> BDD-cost: 17 c ---[10082]---> BDD-cost: 25 c ---[10080]---> BDD-cost: 17 c ---[10078]---> BDD-cost: 25 c ---[10076]---> BDD-cost: 17 c ---[10074]---> BDD-cost: 25 c ---[10072]---> BDD-cost: 17 c ---[10070]---> BDD-cost: 17 c ---[10068]---> BDD-cost: 25 c ---[10066]---> BDD-cost: 17 c ---[10064]---> BDD-cost: 25 c ---[10062]---> BDD-cost: 17 c ---[10060]---> BDD-cost: 25 c ---[10058]---> BDD-cost: 17 c ---[10056]---> BDD-cost: 25 c ---[10054]---> BDD-cost: 17 c ---[10052]---> BDD-cost: 25 c ---[10050]---> BDD-cost: 17 c ---[10048]---> BDD-cost: 25 c ---[10046]---> BDD-cost: 17 c ---[10044]---> BDD-cost: 25 c ---[10042]---> BDD-cost: 17 c ---[10040]---> BDD-cost: 25 c ---[10038]---> BDD-cost: 17 c ---[10036]---> BDD-cost: 25 c ---[10034]---> BDD-cost: 17 c ---[10032]---> BDD-cost: 25 c ---[10030]---> BDD-cost: 17 c ---[10028]---> BDD-cost: 25 c ---[10026]---> BDD-cost: 17 c ---[10024]---> BDD-cost: 25 c ---[10022]---> BDD-cost: 17 c ---[10020]---> BDD-cost: 25 c ---[10018]---> BDD-cost: 17 c ---[10016]---> BDD-cost: 25 c ---[10014]---> BDD-cost: 17 c ---[10012]---> BDD-cost: 25 c ---[10010]---> BDD-cost: 17 c ---[10008]---> BDD-cost: 25 c ---[10006]---> BDD-cost: 17 c ---[10004]---> BDD-cost: 25 c ---[10002]---> BDD-cost: 17 c ---[10000]---> BDD-cost: 25 c ---[9998]---> BDD-cost: 17 c ---[9996]---> BDD-cost: 25 c ---[9994]---> BDD-cost: 17 c ---[9992]---> BDD-cost: 25 c ---[9990]---> BDD-cost: 17 c ---[9988]---> BDD-cost: 25 c ---[9986]---> BDD-cost: 17 c ---[9984]---> BDD-cost: 25 c ---[9982]---> BDD-cost: 17 c ---[9980]---> BDD-cost: 25 c ---[9978]---> BDD-cost: 17 c ---[9976]---> BDD-cost: 25 c ---[9974]---> BDD-cost: 17 c ---[9972]---> BDD-cost: 25 c ---[9970]---> BDD-cost: 17 c ---[9968]---> BDD-cost: 25 c ---[9966]---> BDD-cost: 17 c ---[9964]---> BDD-cost: 25 c ---[9962]---> BDD-cost: 17 c ---[9960]---> BDD-cost: 25 c ---[9958]---> BDD-cost: 17 c ---[9956]---> BDD-cost: 25 c ---[9954]---> BDD-cost: 17 c ---[9952]---> BDD-cost: 25 c ---[9950]---> BDD-cost: 17 c ---[9948]---> BDD-cost: 25 c ---[9946]---> BDD-cost: 17 c ---[9944]---> BDD-cost: 25 c ---[9942]---> BDD-cost: 17 c ---[9940]---> BDD-cost: 25 c ---[9938]---> BDD-cost: 17 c ---[9936]---> BDD-cost: 25 c ---[9934]---> BDD-cost: 17 c ---[9932]---> BDD-cost: 25 c ---[9930]---> BDD-cost: 17 c ---[9928]---> BDD-cost: 25 c ---[9926]---> BDD-cost: 17 c ---[9924]---> BDD-cost: 25 c ---[9922]---> BDD-cost: 17 c ---[9920]---> BDD-cost: 17 c ---[9918]---> BDD-cost: 25 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 163148 532482 | 54382 0 0 nan | 0.000 % | c | 101 | 163065 532193 | 59820 88 845 9.6 | 2.413 % | c | 251 | 163030 532076 | 65802 236 4687 19.9 | 2.428 % | c | 476 | 162996 531958 | 72382 458 5330 11.6 | 2.448 % | c | 813 | 162928 531722 | 79620 786 6347 8.1 | 2.483 % | c | 1319 | 162913 531669 | 87582 1290 8281 6.4 | 2.488 % | c | 2078 | 162778 531194 | 96341 2013 10744 5.3 | 2.553 % | c | 3217 | 162672 530818 | 105975 3126 14721 4.7 | 2.608 % | c | 4925 | 162597 530553 | 116572 4817 22980 4.8 | 2.647 % | c | 7488 | 162472 530140 | 128229 7356 36896 5.0 | 2.712 % | c | 11332 | 162366 529766 | 141052 11185 65646 5.9 | 2.765 % | c | 17100 | 162104 528846 | 155158 16884 142757 8.5 | 2.894 % | c | 25749 | 162095 528817 | 170674 25532 380187 14.9 | 2.899 % | c | 38725 | 161875 528055 | 187741 38461 664055 17.3 | 3.006 % | c | 58187 | 161751 527627 | 206515 57901 1199343 20.7 | 3.069 % | c | 87379 | 161616 527167 | 227167 87062 1920374 22.1 | 3.133 % | c | 131168 | 161597 527102 | 249883 130849 3438083 26.3 | 3.143 % | c | 196852 | 161509 526798 | 274872 196513 13008984 66.2 | 3.186 % | c | 295380 | 161509 526798 | 302359 295041 45134801 153.0 | 3.186 % |
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/13396/stat): 13396 (minisat+_script) R 13395 13396 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843638755 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/13396/statm): 174 3 169 147 0 27 0 [pid=13396] 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=13397 New process pid=13398 New process pid=13399 execve syscall for /bin/sed executable One traced child (pid=13398) 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=13399) exited with status: 0 One traced child (pid=13397) exited with status: 0 New process pid=13400 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-ss97-2.opb [startup+10.0033 s] Raw data (loadavg): 0.93 0.96 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 4024 0 0 0 963 15 0 0 25 0 1 0 1843638759 18395136 3880 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 4491 3880 145 145 0 4346 0 [pid=13400] vsize: 17964 Current children cumulated CPU time (s) 9.8 Current children cumulated vsize (Kb) 20088 [startup+20.005 s] Raw data (loadavg): 0.94 0.96 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 4050 0 0 0 1962 16 0 0 25 0 1 0 1843638759 18509824 3906 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 4519 3906 145 145 0 4374 0 [pid=13400] vsize: 18076 Current children cumulated CPU time (s) 19.8 Current children cumulated vsize (Kb) 20200 [startup+30.0058 s] Raw data (loadavg): 0.95 0.96 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 4079 0 0 0 2962 16 0 0 25 0 1 0 1843638759 18620416 3935 4294967295 134512640 135094434 3221224448 3221223104 134550399 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 4546 3935 145 145 0 4401 0 [pid=13400] vsize: 18184 Current children cumulated CPU time (s) 29.8 Current children cumulated vsize (Kb) 20308 [startup+40.0065 s] Raw data (loadavg): 0.96 0.96 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 4130 0 0 0 3961 17 0 0 25 0 1 0 1843638759 18845696 3986 4294967295 134512640 135094434 3221224448 3221223096 134558258 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 4601 3986 145 145 0 4456 0 [pid=13400] vsize: 18404 Current children cumulated CPU time (s) 39.8 Current children cumulated vsize (Kb) 20528 [startup+50.0072 s] Raw data (loadavg): 0.96 0.96 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 4197 0 0 0 4959 18 0 0 25 0 1 0 1843638759 19103744 4053 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 4664 4053 145 145 0 4519 0 [pid=13400] vsize: 18656 Current children cumulated CPU time (s) 49.79 Current children cumulated vsize (Kb) 20780 [startup+60.0079 s] Raw data (loadavg): 0.97 0.96 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 4607 0 0 0 5954 21 0 0 25 0 1 0 1843638759 20799488 4463 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 5078 4463 145 145 0 4933 0 [pid=13400] vsize: 20312 Current children cumulated CPU time (s) 59.77 Current children cumulated vsize (Kb) 22436 [startup+70.0096 s] Raw data (loadavg): 0.97 0.96 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 4842 0 0 0 6951 22 0 0 25 0 1 0 1843638759 21868544 4698 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 5339 4698 145 145 0 5194 0 [pid=13400] vsize: 21356 Current children cumulated CPU time (s) 69.75 Current children cumulated vsize (Kb) 23480 [startup+80.0103 s] Raw data (loadavg): 0.98 0.96 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 5013 0 0 0 7948 23 0 0 25 0 1 0 1843638759 22544384 4869 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 5504 4869 145 145 0 5359 0 [pid=13400] vsize: 22016 Current children cumulated CPU time (s) 79.73 Current children cumulated vsize (Kb) 24140 [startup+90.0111 s] Raw data (loadavg): 0.98 0.96 0.96 1/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) T 13396 13396 2660 0 -1 0 5352 0 0 0 8943 25 0 0 25 0 1 0 1843638759 23891968 5208 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/13400/statm): 5833 5208 145 145 0 5688 0 [pid=13400] vsize: 23332 Current children cumulated CPU time (s) 89.7 Current children cumulated vsize (Kb) 25456 [startup+100.012 s] Raw data (loadavg): 0.98 0.96 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 5732 0 0 0 9936 28 0 0 25 0 1 0 1843638759 25419776 5588 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 6206 5588 145 145 0 6061 0 [pid=13400] vsize: 24824 Current children cumulated CPU time (s) 99.66 Current children cumulated vsize (Kb) 26948 [startup+110.013 s] Raw data (loadavg): 0.98 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 6035 0 0 0 10930 31 0 0 25 0 1 0 1843638759 26890240 5891 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 6565 5891 145 145 0 6420 0 [pid=13400] vsize: 26260 Current children cumulated CPU time (s) 109.63 Current children cumulated vsize (Kb) 28384 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 6376 0 0 0 11926 33 0 0 25 0 1 0 1843638759 28262400 6232 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 6900 6232 145 145 0 6755 0 [pid=13400] vsize: 27600 Current children cumulated CPU time (s) 119.61 Current children cumulated vsize (Kb) 29724 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 6416 0 0 0 12925 34 0 0 25 0 1 0 1843638759 28418048 6272 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 6938 6272 145 145 0 6793 0 [pid=13400] vsize: 27752 Current children cumulated CPU time (s) 129.61 Current children cumulated vsize (Kb) 29876 [startup+140.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 6777 0 0 0 13918 36 0 0 25 0 1 0 1843638759 29859840 6633 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 7290 6633 145 145 0 7145 0 [pid=13400] vsize: 29160 Current children cumulated CPU time (s) 139.56 Current children cumulated vsize (Kb) 31284 [startup+150.016 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 7427 0 0 0 14909 41 0 0 25 0 1 0 1843638759 32473088 7283 4294967295 134512640 135094434 3221224448 3221223104 134558123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 7928 7283 145 145 0 7783 0 [pid=13400] vsize: 31712 Current children cumulated CPU time (s) 149.52 Current children cumulated vsize (Kb) 33836 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 7853 0 0 0 15901 44 0 0 25 0 1 0 1843638759 34177024 7709 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 8344 7709 145 145 0 8199 0 [pid=13400] vsize: 33376 Current children cumulated CPU time (s) 159.47 Current children cumulated vsize (Kb) 35500 [startup+170.018 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 8065 0 0 0 16898 46 0 0 25 0 1 0 1843638759 35012608 7921 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 8548 7921 145 145 0 8403 0 [pid=13400] vsize: 34192 Current children cumulated CPU time (s) 169.46 Current children cumulated vsize (Kb) 36316 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 8437 0 0 0 17891 50 0 0 25 0 1 0 1843638759 36507648 8293 4294967295 134512640 135094434 3221224448 3221223040 134557137 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 8913 8293 145 145 0 8768 0 [pid=13400] vsize: 35652 Current children cumulated CPU time (s) 179.43 Current children cumulated vsize (Kb) 37776 [startup+190.019 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 8732 0 0 0 18886 52 0 0 25 0 1 0 1843638759 38215680 8588 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 9330 8588 145 145 0 9185 0 [pid=13400] vsize: 37320 Current children cumulated CPU time (s) 189.4 Current children cumulated vsize (Kb) 39444 [startup+200.02 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 9204 0 0 0 19877 55 0 0 25 0 1 0 1843638759 40128512 9060 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 9797 9060 145 145 0 9652 0 [pid=13400] vsize: 39188 Current children cumulated CPU time (s) 199.34 Current children cumulated vsize (Kb) 41312 [startup+210.021 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 9750 0 0 0 20866 60 0 0 25 0 1 0 1843638759 42352640 9606 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 10340 9606 145 145 0 10195 0 [pid=13400] vsize: 41360 Current children cumulated CPU time (s) 209.28 Current children cumulated vsize (Kb) 43484 [startup+220.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 10276 0 0 0 21854 65 0 0 25 0 1 0 1843638759 44498944 10132 4294967295 134512640 135094434 3221224448 3221223040 134556964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 10864 10132 145 145 0 10719 0 [pid=13400] vsize: 43456 Current children cumulated CPU time (s) 219.21 Current children cumulated vsize (Kb) 45580 [startup+230.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 10795 0 0 0 22843 70 0 0 25 0 1 0 1843638759 46616576 10651 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 11381 10651 145 145 0 11236 0 [pid=13400] vsize: 45524 Current children cumulated CPU time (s) 229.15 Current children cumulated vsize (Kb) 47648 [startup+240.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 11326 0 0 0 23834 74 0 0 25 0 1 0 1843638759 48779264 11182 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 11909 11182 145 145 0 11764 0 [pid=13400] vsize: 47636 Current children cumulated CPU time (s) 239.1 Current children cumulated vsize (Kb) 49760 [startup+250.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 11798 0 0 0 24827 77 0 0 25 0 1 0 1843638759 50708480 11654 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 12380 11654 145 145 0 12235 0 [pid=13400] vsize: 49520 Current children cumulated CPU time (s) 249.06 Current children cumulated vsize (Kb) 51644 [startup+260.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 12292 0 0 0 25819 81 0 0 25 0 1 0 1843638759 52723712 12148 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 12872 12148 145 145 0 12727 0 [pid=13400] vsize: 51488 Current children cumulated CPU time (s) 259.02 Current children cumulated vsize (Kb) 53612 [startup+270.027 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 12766 0 0 0 26810 85 0 0 25 0 1 0 1843638759 54673408 12622 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 13348 12622 145 145 0 13203 0 [pid=13400] vsize: 53392 Current children cumulated CPU time (s) 268.97 Current children cumulated vsize (Kb) 55516 [startup+280.028 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 13222 0 0 0 27801 89 0 0 25 0 1 0 1843638759 56541184 13078 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 13804 13078 145 145 0 13659 0 [pid=13400] vsize: 55216 Current children cumulated CPU time (s) 278.92 Current children cumulated vsize (Kb) 57340 [startup+290.029 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 13686 0 0 0 28793 92 0 0 25 0 1 0 1843638759 58429440 13542 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 14265 13542 145 145 0 14120 0 [pid=13400] vsize: 57060 Current children cumulated CPU time (s) 288.87 Current children cumulated vsize (Kb) 59184 [startup+300.03 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 14121 0 0 0 29786 96 0 0 25 0 1 0 1843638759 60203008 13977 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 14698 13977 145 145 0 14553 0 [pid=13400] vsize: 58792 Current children cumulated CPU time (s) 298.84 Current children cumulated vsize (Kb) 60916 [startup+310.031 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 14575 0 0 0 30778 98 0 0 25 0 1 0 1843638759 62078976 14431 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 15156 14431 145 145 0 15011 0 [pid=13400] vsize: 60624 Current children cumulated CPU time (s) 308.78 Current children cumulated vsize (Kb) 62748 [startup+320.032 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 15023 0 0 0 31771 102 0 0 25 0 1 0 1843638759 63922176 14879 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 15606 14879 145 145 0 15461 0 [pid=13400] vsize: 62424 Current children cumulated CPU time (s) 318.75 Current children cumulated vsize (Kb) 64548 [startup+330.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 15426 0 0 0 32763 105 0 0 25 0 1 0 1843638759 65552384 15282 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 16004 15282 145 145 0 15859 0 [pid=13400] vsize: 64016 Current children cumulated CPU time (s) 328.7 Current children cumulated vsize (Kb) 66140 [startup+340.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 15832 0 0 0 33755 108 0 0 25 0 1 0 1843638759 67215360 15688 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 16410 15688 145 145 0 16265 0 [pid=13400] vsize: 65640 Current children cumulated CPU time (s) 338.65 Current children cumulated vsize (Kb) 67764 [startup+350.035 s] Raw data (loadavg): 0.99 0.97 0.96 1/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) T 13396 13396 2660 0 -1 0 16243 0 0 0 34749 111 0 0 25 0 1 0 1843638759 68882432 16099 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/13400/statm): 16817 16099 145 145 0 16672 0 [pid=13400] vsize: 67268 Current children cumulated CPU time (s) 348.62 Current children cumulated vsize (Kb) 69392 [startup+360.036 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 16619 0 0 0 35743 113 0 0 25 0 1 0 1843638759 70418432 16475 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 17192 16475 145 145 0 17047 0 [pid=13400] vsize: 68768 Current children cumulated CPU time (s) 358.58 Current children cumulated vsize (Kb) 70892 [startup+370.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 17040 0 0 0 36736 116 0 0 25 0 1 0 1843638759 72151040 16896 4294967295 134512640 135094434 3221224448 3221223040 134557269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 17615 16896 145 145 0 17470 0 [pid=13400] vsize: 70460 Current children cumulated CPU time (s) 368.54 Current children cumulated vsize (Kb) 72584 [startup+380.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 17438 0 0 0 37728 119 0 0 25 0 1 0 1843638759 73846784 17294 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 18029 17294 145 145 0 17884 0 [pid=13400] vsize: 72116 Current children cumulated CPU time (s) 378.49 Current children cumulated vsize (Kb) 74240 [startup+390.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 17937 0 0 0 38723 122 0 0 25 0 1 0 1843638759 75874304 17793 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 18524 17793 145 145 0 18379 0 [pid=13400] vsize: 74096 Current children cumulated CPU time (s) 388.47 Current children cumulated vsize (Kb) 76220 [startup+400.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 18476 0 0 0 39714 125 0 0 25 0 1 0 1843638759 78036992 18332 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 19052 18332 145 145 0 18907 0 [pid=13400] vsize: 76208 Current children cumulated CPU time (s) 398.41 Current children cumulated vsize (Kb) 78332 [startup+410.039 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 18889 0 0 0 40709 128 0 0 25 0 1 0 1843638759 79695872 18745 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 19457 18745 145 145 0 19312 0 [pid=13400] vsize: 77828 Current children cumulated CPU time (s) 408.39 Current children cumulated vsize (Kb) 79952 [startup+420.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 19182 0 0 0 41703 130 0 0 25 0 1 0 1843638759 80875520 19038 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 19745 19038 145 145 0 19600 0 [pid=13400] vsize: 78980 Current children cumulated CPU time (s) 418.35 Current children cumulated vsize (Kb) 81104 [startup+430.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 19518 0 0 0 42696 133 0 0 25 0 1 0 1843638759 82231296 19374 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 20076 19374 145 145 0 19931 0 [pid=13400] vsize: 80304 Current children cumulated CPU time (s) 428.31 Current children cumulated vsize (Kb) 82428 [startup+440.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 20234 0 0 0 43683 138 0 0 25 0 1 0 1843638759 85151744 20090 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 20789 20090 145 145 0 20644 0 [pid=13400] vsize: 83156 Current children cumulated CPU time (s) 438.23 Current children cumulated vsize (Kb) 85280 [startup+450.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 20900 0 0 0 44670 143 0 0 25 0 1 0 1843638759 87871488 20756 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 21453 20756 145 145 0 21308 0 [pid=13400] vsize: 85812 Current children cumulated CPU time (s) 448.15 Current children cumulated vsize (Kb) 87936 [startup+460.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 21525 0 0 0 45659 148 0 0 25 0 1 0 1843638759 90415104 21381 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 22074 21381 145 145 0 21929 0 [pid=13400] vsize: 88296 Current children cumulated CPU time (s) 458.09 Current children cumulated vsize (Kb) 90420 [startup+470.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 22156 0 0 0 46648 153 0 0 25 0 1 0 1843638759 92987392 22012 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 22702 22012 145 145 0 22557 0 [pid=13400] vsize: 90808 Current children cumulated CPU time (s) 468.03 Current children cumulated vsize (Kb) 92932 [startup+480.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 22817 0 0 0 47638 157 0 0 25 0 1 0 1843638759 95686656 22673 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 23361 22673 145 145 0 23216 0 [pid=13400] vsize: 93444 Current children cumulated CPU time (s) 477.97 Current children cumulated vsize (Kb) 95568 [startup+490.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 23444 0 0 0 48627 162 0 0 25 0 1 0 1843638759 98246656 23300 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 23986 23300 145 145 0 23841 0 [pid=13400] vsize: 95944 Current children cumulated CPU time (s) 487.91 Current children cumulated vsize (Kb) 98068 [startup+500.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 24123 0 0 0 49616 167 0 0 25 0 1 0 1843638759 101019648 23979 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 24663 23979 145 145 0 24518 0 [pid=13400] vsize: 98652 Current children cumulated CPU time (s) 497.85 Current children cumulated vsize (Kb) 100776 [startup+510.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 24809 0 0 0 50606 170 0 0 25 0 1 0 1843638759 103817216 24665 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 25346 24665 145 145 0 25201 0 [pid=13400] vsize: 101384 Current children cumulated CPU time (s) 507.78 Current children cumulated vsize (Kb) 103508 [startup+520.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 25449 0 0 0 51597 173 0 0 25 0 1 0 1843638759 106438656 25305 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 25986 25305 145 145 0 25841 0 [pid=13400] vsize: 103944 Current children cumulated CPU time (s) 517.72 Current children cumulated vsize (Kb) 106068 [startup+530.049 s] Raw data (loadavg): 0.99 0.97 0.96 1/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) T 13396 13396 2660 0 -1 0 26049 0 0 0 52589 177 0 0 25 0 1 0 1843638759 108892160 25905 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/13400/statm): 26585 25905 145 145 0 26440 0 [pid=13400] vsize: 106340 Current children cumulated CPU time (s) 527.68 Current children cumulated vsize (Kb) 108464 [startup+540.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 26694 0 0 0 53578 181 0 0 25 0 1 0 1843638759 111538176 26550 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 27231 26550 145 145 0 27086 0 [pid=13400] vsize: 108924 Current children cumulated CPU time (s) 537.61 Current children cumulated vsize (Kb) 111048 [startup+550.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 27330 0 0 0 54567 184 0 0 25 0 1 0 1843638759 114130944 27186 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 27864 27186 145 145 0 27719 0 [pid=13400] vsize: 111456 Current children cumulated CPU time (s) 547.53 Current children cumulated vsize (Kb) 113580 [startup+560.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 27967 0 0 0 55556 188 0 0 25 0 1 0 1843638759 116744192 27823 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 28502 27823 145 145 0 28357 0 [pid=13400] vsize: 114008 Current children cumulated CPU time (s) 557.46 Current children cumulated vsize (Kb) 116132 [startup+570.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 28555 0 0 0 56545 192 0 0 25 0 1 0 1843638759 119148544 28411 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 29089 28411 145 145 0 28944 0 [pid=13400] vsize: 116356 Current children cumulated CPU time (s) 567.39 Current children cumulated vsize (Kb) 118480 [startup+580.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 29118 0 0 0 57536 196 0 0 25 0 1 0 1843638759 121450496 28974 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 29651 28974 145 145 0 29506 0 [pid=13400] vsize: 118604 Current children cumulated CPU time (s) 577.34 Current children cumulated vsize (Kb) 120728 [startup+590.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 29650 0 0 0 58526 200 0 0 25 0 1 0 1843638759 123625472 29506 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 30182 29506 145 145 0 30037 0 [pid=13400] vsize: 120728 Current children cumulated CPU time (s) 587.28 Current children cumulated vsize (Kb) 122852 [startup+600.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 30206 0 0 0 59516 204 0 0 25 0 1 0 1843638759 125906944 30062 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 30739 30062 145 145 0 30594 0 [pid=13400] vsize: 122956 Current children cumulated CPU time (s) 597.22 Current children cumulated vsize (Kb) 125080 [startup+610.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 30742 0 0 0 60508 206 0 0 25 0 1 0 1843638759 128110592 30598 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 31277 30598 145 145 0 31132 0 [pid=13400] vsize: 125108 Current children cumulated CPU time (s) 607.16 Current children cumulated vsize (Kb) 127232 [startup+620.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) T 13396 13396 2660 0 -1 0 31265 0 0 0 61500 210 0 0 25 0 1 0 1843638759 130260992 31121 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/13400/statm): 31802 31121 145 145 0 31657 0 [pid=13400] vsize: 127208 Current children cumulated CPU time (s) 617.12 Current children cumulated vsize (Kb) 129332 [startup+630.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 31884 0 0 0 62491 214 0 0 25 0 1 0 1843638759 132784128 31740 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 32418 31740 145 145 0 32273 0 [pid=13400] vsize: 129672 Current children cumulated CPU time (s) 627.07 Current children cumulated vsize (Kb) 131796 [startup+640.058 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 32421 0 0 0 63483 217 0 0 25 0 1 0 1843638759 135032832 32277 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 32967 32277 145 145 0 32822 0 [pid=13400] vsize: 131868 Current children cumulated CPU time (s) 637.02 Current children cumulated vsize (Kb) 133992 [startup+650.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 32924 0 0 0 64474 221 0 0 25 0 1 0 1843638759 137076736 32780 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 33466 32780 145 145 0 33321 0 [pid=13400] vsize: 133864 Current children cumulated CPU time (s) 646.97 Current children cumulated vsize (Kb) 135988 [startup+660.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) T 13396 13396 2660 0 -1 0 33461 0 0 0 65463 225 0 0 25 0 1 0 1843638759 139268096 33317 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/13400/statm): 34001 33317 145 145 0 33856 0 [pid=13400] vsize: 136004 Current children cumulated CPU time (s) 656.9 Current children cumulated vsize (Kb) 138128 [startup+670.061 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 34041 0 0 0 66454 228 0 0 25 0 1 0 1843638759 141639680 33897 4294967295 134512640 135094434 3221224448 3221223040 134556843 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 34580 33897 145 145 0 34435 0 [pid=13400] vsize: 138320 Current children cumulated CPU time (s) 666.84 Current children cumulated vsize (Kb) 140444 [startup+680.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 34593 0 0 0 67446 232 0 0 25 0 1 0 1843638759 143900672 34449 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 35132 34449 145 145 0 34987 0 [pid=13400] vsize: 140528 Current children cumulated CPU time (s) 676.8 Current children cumulated vsize (Kb) 142652 [startup+690.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 35170 0 0 0 68437 235 0 0 25 0 1 0 1843638759 146284544 35026 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 35714 35026 145 145 0 35569 0 [pid=13400] vsize: 142856 Current children cumulated CPU time (s) 686.74 Current children cumulated vsize (Kb) 144980 [startup+700.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 35705 0 0 0 69429 238 0 0 25 0 1 0 1843638759 148504576 35561 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 36256 35561 145 145 0 36111 0 [pid=13400] vsize: 145024 Current children cumulated CPU time (s) 696.69 Current children cumulated vsize (Kb) 147148 [startup+710.064 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 36221 0 0 0 70422 241 0 0 25 0 1 0 1843638759 150609920 36077 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 36770 36077 145 145 0 36625 0 [pid=13400] vsize: 147080 Current children cumulated CPU time (s) 706.65 Current children cumulated vsize (Kb) 149204 [startup+720.066 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 36707 0 0 0 71415 244 0 0 25 0 1 0 1843638759 152604672 36563 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 37257 36563 145 145 0 37112 0 [pid=13400] vsize: 149028 Current children cumulated CPU time (s) 716.61 Current children cumulated vsize (Kb) 151152 [startup+730.066 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 37209 0 0 0 72407 247 0 0 25 0 1 0 1843638759 155705344 37065 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 38014 37065 145 145 0 37869 0 [pid=13400] vsize: 152056 Current children cumulated CPU time (s) 726.56 Current children cumulated vsize (Kb) 154180 [startup+740.067 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 37686 0 0 0 73398 250 0 0 25 0 1 0 1843638759 157663232 37542 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 38492 37542 145 145 0 38347 0 [pid=13400] vsize: 153968 Current children cumulated CPU time (s) 736.5 Current children cumulated vsize (Kb) 156092 [startup+750.068 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 38108 0 0 0 74391 253 0 0 25 0 1 0 1843638759 159383552 37964 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 38912 37964 145 145 0 38767 0 [pid=13400] vsize: 155648 Current children cumulated CPU time (s) 746.46 Current children cumulated vsize (Kb) 157772 [startup+760.069 s] Raw data (loadavg): 1.07 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 38558 0 0 0 75383 257 0 0 25 0 1 0 1843638759 161222656 38414 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 39361 38414 145 145 0 39216 0 [pid=13400] vsize: 157444 Current children cumulated CPU time (s) 756.42 Current children cumulated vsize (Kb) 159568 [startup+770.069 s] Raw data (loadavg): 1.06 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 39059 0 0 0 76373 261 0 0 25 0 1 0 1843638759 163274752 38915 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 39862 38915 145 145 0 39717 0 [pid=13400] vsize: 159448 Current children cumulated CPU time (s) 766.36 Current children cumulated vsize (Kb) 161572 [startup+780.071 s] Raw data (loadavg): 1.05 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 39567 0 0 0 77363 265 0 0 25 0 1 0 1843638759 165347328 39423 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 40368 39423 145 145 0 40223 0 [pid=13400] vsize: 161472 Current children cumulated CPU time (s) 776.3 Current children cumulated vsize (Kb) 163596 [startup+790.072 s] Raw data (loadavg): 1.04 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 39984 0 0 0 78356 269 0 0 25 0 1 0 1843638759 167055360 39840 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 40785 39840 145 145 0 40640 0 [pid=13400] vsize: 163140 Current children cumulated CPU time (s) 786.27 Current children cumulated vsize (Kb) 165264 [startup+800.072 s] Raw data (loadavg): 1.04 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 40416 0 0 0 79349 272 0 0 25 0 1 0 1843638759 168820736 40272 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 41216 40272 145 145 0 41071 0 [pid=13400] vsize: 164864 Current children cumulated CPU time (s) 796.23 Current children cumulated vsize (Kb) 166988 [startup+810.073 s] Raw data (loadavg): 1.03 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 40803 0 0 0 80342 275 0 0 25 0 1 0 1843638759 170389504 40659 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 41599 40659 145 145 0 41454 0 [pid=13400] vsize: 166396 Current children cumulated CPU time (s) 806.19 Current children cumulated vsize (Kb) 168520 [startup+820.074 s] Raw data (loadavg): 1.03 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 41227 0 0 0 81335 278 0 0 25 0 1 0 1843638759 172130304 41083 4294967295 134512640 135094434 3221224448 3221223084 134556682 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 42024 41083 145 145 0 41879 0 [pid=13400] vsize: 168096 Current children cumulated CPU time (s) 816.15 Current children cumulated vsize (Kb) 170220 [startup+830.075 s] Raw data (loadavg): 1.02 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 41682 0 0 0 82326 282 0 0 25 0 1 0 1843638759 173998080 41538 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 42480 41538 145 145 0 42335 0 [pid=13400] vsize: 169920 Current children cumulated CPU time (s) 826.1 Current children cumulated vsize (Kb) 172044 [startup+840.075 s] Raw data (loadavg): 1.02 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 42120 0 0 0 83318 286 0 0 25 0 1 0 1843638759 175783936 41976 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 42916 41976 145 145 0 42771 0 [pid=13400] vsize: 171664 Current children cumulated CPU time (s) 836.06 Current children cumulated vsize (Kb) 173788 [startup+850.077 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 42545 0 0 0 84311 289 0 0 25 0 1 0 1843638759 177512448 42401 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 43338 42401 145 145 0 43193 0 [pid=13400] vsize: 173352 Current children cumulated CPU time (s) 846.02 Current children cumulated vsize (Kb) 175476 [startup+860.078 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 42988 0 0 0 85303 292 0 0 25 0 1 0 1843638759 179326976 42844 4294967295 134512640 135094434 3221224448 3221223040 134557297 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 43781 42844 145 145 0 43636 0 [pid=13400] vsize: 175124 Current children cumulated CPU time (s) 855.97 Current children cumulated vsize (Kb) 177248 [startup+870.08 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 43428 0 0 0 86297 295 0 0 25 0 1 0 1843638759 181141504 43284 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 44224 43284 145 145 0 44079 0 [pid=13400] vsize: 176896 Current children cumulated CPU time (s) 865.94 Current children cumulated vsize (Kb) 179020 [startup+880.08 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 43855 0 0 0 87290 298 0 0 25 0 1 0 1843638759 182882304 43711 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 44649 43711 145 145 0 44504 0 [pid=13400] vsize: 178596 Current children cumulated CPU time (s) 875.9 Current children cumulated vsize (Kb) 180720 [startup+890.081 s] Raw data (loadavg): 1.01 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 44324 0 0 0 88281 302 0 0 25 0 1 0 1843638759 184799232 44180 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 45117 44180 145 145 0 44972 0 [pid=13400] vsize: 180468 Current children cumulated CPU time (s) 885.85 Current children cumulated vsize (Kb) 182592 [startup+900.083 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 44785 0 0 0 89273 304 0 0 25 0 1 0 1843638759 186724352 44641 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 45587 44641 145 145 0 45442 0 [pid=13400] vsize: 182348 Current children cumulated CPU time (s) 895.79 Current children cumulated vsize (Kb) 184472 [startup+910.083 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 45196 0 0 0 90267 307 0 0 25 0 1 0 1843638759 188416000 45052 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 46000 45052 145 145 0 45855 0 [pid=13400] vsize: 184000 Current children cumulated CPU time (s) 905.76 Current children cumulated vsize (Kb) 186124 [startup+920.085 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 45603 0 0 0 91259 311 0 0 25 0 1 0 1843638759 190078976 45459 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 46406 45459 145 145 0 46261 0 [pid=13400] vsize: 185624 Current children cumulated CPU time (s) 915.72 Current children cumulated vsize (Kb) 187748 [startup+930.086 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 46025 0 0 0 92251 314 0 0 25 0 1 0 1843638759 191795200 45881 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 46825 45881 145 145 0 46680 0 [pid=13400] vsize: 187300 Current children cumulated CPU time (s) 925.67 Current children cumulated vsize (Kb) 189424 [startup+940.087 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 46442 0 0 0 93245 316 0 0 25 0 1 0 1843638759 193499136 46298 4294967295 134512640 135094434 3221224448 3221223040 134557131 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 47241 46298 145 145 0 47096 0 [pid=13400] vsize: 188964 Current children cumulated CPU time (s) 935.63 Current children cumulated vsize (Kb) 191088 [startup+950.087 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 46872 0 0 0 94238 319 0 0 25 0 1 0 1843638759 195256320 46728 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 47670 46728 145 145 0 47525 0 [pid=13400] vsize: 190680 Current children cumulated CPU time (s) 945.59 Current children cumulated vsize (Kb) 192804 [startup+960.088 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 47274 0 0 0 95232 322 0 0 25 0 1 0 1843638759 196943872 47130 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 48082 47130 145 145 0 47937 0 [pid=13400] vsize: 192328 Current children cumulated CPU time (s) 955.56 Current children cumulated vsize (Kb) 194452 [startup+970.09 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 47649 0 0 0 96226 325 0 0 25 0 1 0 1843638759 198479872 47505 4294967295 134512640 135094434 3221224448 3221223120 134556094 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 48457 47505 145 145 0 48312 0 [pid=13400] vsize: 193828 Current children cumulated CPU time (s) 965.53 Current children cumulated vsize (Kb) 195952 [startup+980.091 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 48056 0 0 0 97222 326 0 0 25 0 1 0 1843638759 200146944 47912 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 48864 47912 145 145 0 48719 0 [pid=13400] vsize: 195456 Current children cumulated CPU time (s) 975.5 Current children cumulated vsize (Kb) 197580 [startup+990.091 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 48542 0 0 0 98214 330 0 0 25 0 1 0 1843638759 202113024 48398 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 49344 48398 145 145 0 49199 0 [pid=13400] vsize: 197376 Current children cumulated CPU time (s) 985.46 Current children cumulated vsize (Kb) 199500 [startup+1000.09 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 48943 0 0 0 99208 333 0 0 25 0 1 0 1843638759 203743232 48799 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 49742 48799 145 145 0 49597 0 [pid=13400] vsize: 198968 Current children cumulated CPU time (s) 995.43 Current children cumulated vsize (Kb) 201092 [startup+1010.09 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 49318 0 0 0 100202 336 0 0 25 0 1 0 1843638759 205316096 49174 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 50126 49174 145 145 0 49981 0 [pid=13400] vsize: 200504 Current children cumulated CPU time (s) 1005.4 Current children cumulated vsize (Kb) 202628 [startup+1020.09 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 49721 0 0 0 101194 339 0 0 25 0 1 0 1843638759 206958592 49577 4294967295 134512640 135094434 3221224448 3221223040 134557528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 50527 49577 145 145 0 50382 0 [pid=13400] vsize: 202108 Current children cumulated CPU time (s) 1015.35 Current children cumulated vsize (Kb) 204232 [startup+1030.09 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 50161 0 0 0 102187 343 0 0 25 0 1 0 1843638759 208756736 50017 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 50966 50017 145 145 0 50821 0 [pid=13400] vsize: 203864 Current children cumulated CPU time (s) 1025.32 Current children cumulated vsize (Kb) 205988 [startup+1040.09 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 50628 0 0 0 103180 345 0 0 25 0 1 0 1843638759 210665472 50484 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 51432 50484 145 145 0 51287 0 [pid=13400] vsize: 205728 Current children cumulated CPU time (s) 1035.27 Current children cumulated vsize (Kb) 207852 [startup+1050.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 51058 0 0 0 104174 348 0 0 25 0 1 0 1843638759 212434944 50914 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 51864 50914 145 145 0 51719 0 [pid=13400] vsize: 207456 Current children cumulated CPU time (s) 1045.24 Current children cumulated vsize (Kb) 209580 [startup+1060.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 51391 0 0 0 105168 351 0 0 25 0 1 0 1843638759 213766144 51247 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13400/statm): 52189 51247 145 145 0 52044 0 [pid=13400] vsize: 208756 Current children cumulated CPU time (s) 1055.21 Current children cumulated vsize (Kb) 210880 [startup+1070.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 51746 0 0 0 106162 354 0 0 25 0 1 0 1843638759 215187456 51602 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52536 51602 145 145 0 52391 0 [pid=13400] vsize: 210144 Current children cumulated CPU time (s) 1065.18 Current children cumulated vsize (Kb) 212268 [startup+1080.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 107158 356 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1075.16 Current children cumulated vsize (Kb) 213384 [startup+1090.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 108158 356 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223100 134561543 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1085.16 Current children cumulated vsize (Kb) 213384 [startup+1100.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 109158 356 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1095.16 Current children cumulated vsize (Kb) 213384 [startup+1110.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 110158 356 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1105.16 Current children cumulated vsize (Kb) 213384 [startup+1120.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 111159 356 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1115.17 Current children cumulated vsize (Kb) 213384 [startup+1130.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 112159 356 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223088 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1125.17 Current children cumulated vsize (Kb) 213384 [startup+1140.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 113159 356 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223060 134563041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1135.17 Current children cumulated vsize (Kb) 213384 [startup+1150.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 114159 356 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1145.17 Current children cumulated vsize (Kb) 213384 [startup+1160.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 115159 356 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1155.17 Current children cumulated vsize (Kb) 213384 [startup+1170.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 116159 356 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223104 134558035 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1165.17 Current children cumulated vsize (Kb) 213384 [startup+1180.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 117159 357 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1175.18 Current children cumulated vsize (Kb) 213384 [startup+1190.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 118160 357 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1185.19 Current children cumulated vsize (Kb) 213384 [startup+1200.1 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 119160 357 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1195.19 Current children cumulated vsize (Kb) 213384 [startup+1210.11 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 120160 357 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223136 134784967 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1205.19 Current children cumulated vsize (Kb) 213384 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 1.00 0.99 0.97 2/57 13400 Raw data (/proc/13396/stat): 13396 (minisat+_script) S 13395 13396 2660 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1843638755 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13396/statm): 531 226 485 147 0 384 0 [pid=13396] vsize: 2124 Raw data (/proc/13400/stat): 13400 (minisat+_64-bit) R 13396 13396 2660 0 -1 0 52030 0 0 0 120160 357 0 0 25 0 1 0 1843638759 216330240 51886 4294967295 134512640 135094434 3221224448 3221223104 134558420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13400/statm): 52815 51886 145 145 0 52670 0 [pid=13400] vsize: 211260 Current children cumulated CPU time (s) 1205.19 Current children cumulated vsize (Kb) 213384 Sending SIGTERM to -13396 Sleeping 2 seconds One traced child (pid=13396) ended because it received signal 15 (SIGTERM) One traced child (pid=13400) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.2 CPU time (s): 1205.27 CPU user time (s): 1201.61 CPU system time (s): 3.66544 CPU usage (%): 99.5927 Max. virtual memory (cumulated for all children) (Kb): 213384
ERROR: no interpretation found !