Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-greenbea.opb |
MD5SUM | 44cf829c3f56aa0e06d9c19014e5de34 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 10788 |
Biggest coefficient in the objective function | 524288000000 |
Number of bits for the biggest coefficient in the objective function | 39 |
Sum of the numbers in the objective function | 20280599220360 |
Number of bits of the sum of numbers in the objective function | 45 |
Biggest number in a constraint | 524288000000 |
Number of bits of the biggest number in a constraint | 39 |
Biggest sum of numbers in a constraint | 23881563011625 |
Number of bits of the biggest sum of numbers | 45 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 104437 |
Total number of constraints | 2675 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 2675 |
Minimum length of a constraint | 8 |
Maximum length of a constraint | 4913 |
LAUNCH ON wulflinc29 THE 2005-09-20 02:46:44 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3163 boxname=wulflinc29 idbench=819 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 44cf829c3f56aa0e06d9c19014e5de34 /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-greenbea.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-greenbea.opb IDLAUNCH: 3163 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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.020 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 860332 kB Buffers: 36412 kB Cached: 105848 kB SwapCached: 676 kB Active: 40280 kB Inactive: 104444 kB HighTotal: 131008 kB HighFree: 25928 kB LowTotal: 903652 kB LowFree: 834404 kB SwapTotal: 2097892 kB SwapFree: 2096528 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5664 kB Slab: 23944 kB Committed_AS: 64140 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 03:06:55 (client local time) WITH STATUS 0 IN 1208.6 SECONDS stats: 3163 7 1208.6 0
c Parsing PB file... c Converting 4200 PB-constraints to clauses... c -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ###################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################### c -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssss c ---[4247]---> BDD-cost: 17 c ---[4242]---> BDD-cost: 15 c ---[4241]---> BDD-cost: 14 c ---[4240]---> BDD-cost: 18 c ---[4239]---> BDD-cost: 15 c ---[4237]---> BDD-cost: 14 c ---[4236]---> BDD-cost: 16 c ---[4235]---> BDD-cost: 13 c ---[4234]---> BDD-cost: 13 c ---[4233]---> BDD-cost: 11 c ---[4232]---> BDD-cost: 13 c ---[4230]---> BDD-cost: 13 c ---[4229]---> BDD-cost: 14 c ---[4227]---> BDD-cost: 12 c ---[4226]---> BDD-cost: 8 c ---[4225]---> BDD-cost: 12 c ---[4224]---> BDD-cost: 12 c ---[4223]---> BDD-cost: 9 c ---[4221]---> BDD-cost: 13 c ---[4218]---> BDD-cost: 10 c ---[4217]---> BDD-cost: 15 c ---[4214]---> BDD-cost: 9 c ---[4213]---> BDD-cost: 16 c ---[4212]---> BDD-cost: 12 c ---[4211]---> BDD-cost: 14 c ---[4210]---> BDD-cost: 14 c ---[4209]---> BDD-cost: 12 c ---[4208]---> BDD-cost: 15 c ---[4207]---> BDD-cost: 12 c ---[4206]---> BDD-cost: 13 c ---[4205]---> BDD-cost: 8 c ---[4203]---> BDD-cost: 12 c ---[4202]---> BDD-cost: 11 c ---[4201]---> BDD-cost: 10 c ---[4200]---> BDD-cost: 12 c ---[4199]---> BDD-cost: 14 c ---[4196]---> BDD-cost: 19 c ---[4195]---> BDD-cost: 13 c ---[4194]---> BDD-cost: 16 c ---[4192]---> BDD-cost: 16 c ---[4190]---> BDD-cost: 17 c ---[4189]---> BDD-cost: 15 c ---[4188]---> BDD-cost: 15 c ---[4187]---> BDD-cost: 13 c ---[4186]---> BDD-cost: 17 c ---[4185]---> BDD-cost: 16 c ---[4184]---> BDD-cost: 16 c ---[4183]---> BDD-cost: 15 c ---[4182]---> BDD-cost: 14 c ---[4181]---> BDD-cost: 7 c ---[4180]---> BDD-cost: 11 c ---[4179]---> BDD-cost: 15 c ---[4178]---> BDD-cost: 7 c ---[4177]---> BDD-cost: 12 c ---[4176]---> BDD-cost: 12 c ---[4175]---> BDD-cost: 8 c ---[4174]---> BDD-cost: 11 c ---[4173]---> BDD-cost: 14 c ---[4170]---> BDD-cost: 17 c ---[4169]---> BDD-cost: 20 c ---[4168]---> BDD-cost: 14 c ---[4167]---> BDD-cost: 13 c ---[4166]---> BDD-cost: 17 c ---[4164]---> BDD-cost: 9 c ---[4163]---> BDD-cost: 17 c ---[4162]---> BDD-cost: 11 c ---[4161]---> BDD-cost: 18 c ---[4160]---> BDD-cost: 15 c ---[4159]---> BDD-cost: 16 c ---[4158]---> BDD-cost: 16 c ---[4157]---> BDD-cost: 16 c ---[4155]---> BDD-cost: 17 c ---[4154]---> BDD-cost: 15 c ---[4153]---> BDD-cost: 15 c ---[4152]---> BDD-cost: 7 c ---[4151]---> BDD-cost: 11 c ---[4149]---> BDD-cost: 7 c ---[4148]---> BDD-cost: 14 c ---[4147]---> BDD-cost: 13 c ---[4146]---> BDD-cost: 7 c ---[4145]---> BDD-cost: 12 c ---[4142]---> BDD-cost: 14 c ---[4141]---> BDD-cost: 15 c ---[4140]---> BDD-cost: 19 c ---[4139]---> BDD-cost: 16 c ---[4138]---> BDD-cost: 16 c ---[4136]---> BDD-cost: 15 c ---[4135]---> BDD-cost: 17 c ---[4134]---> BDD-cost: 11 c ---[4133]---> BDD-cost: 16 c ---[4132]---> BDD-cost: 16 c ---[4130]---> BDD-cost: 15 c ---[4128]---> BDD-cost: 15 c ---[4127]---> BDD-cost: 15 c ---[4126]---> BDD-cost: 16 c ---[4125]---> BDD-cost: 16 c ---[4124]---> BDD-cost: 12 c ---[4123]---> BDD-cost: 16 c ---[4122]---> BDD-cost: 15 c ---[4121]---> BDD-cost: 12 c ---[4120]---> BDD-cost: 12 c ---[4119]---> BDD-cost: 11 c ---[4117]---> BDD-cost: 12 c ---[4116]---> BDD-cost: 11 c ---[4115]---> BDD-cost: 12 c ---[4114]---> BDD-cost: 11 c ---[4113]---> BDD-cost: 12 c ---[4112]---> BDD-cost: 12 c ---[4111]---> BDD-cost: 12 c ---[4110]---> BDD-cost: 13 c ---[4109]---> BDD-cost: 12 c ---[4108]---> BDD-cost: 15 c ---[4107]---> BDD-cost: 19 c ---[4104]---> BDD-cost: 15 c ---[4103]---> BDD-cost: 15 c ---[4100]---> BDD-cost: 16 c ---[4099]---> BDD-cost: 15 c ---[4098]---> BDD-cost: 16 c ---[4097]---> BDD-cost: 16 c ---[4096]---> BDD-cost: 17 c ---[4094]---> BDD-cost: 14 c ---[4093]---> BDD-cost: 13 c ---[4092]---> BDD-cost: 14 c ---[4091]---> BDD-cost: 12 c ---[4089]---> BDD-cost: 11 c ---[4087]---> BDD-cost: 12 c ---[4086]---> BDD-cost: 14 c ---[4085]---> BDD-cost: 13 c ---[4084]---> BDD-cost: 12 c ---[4083]---> BDD-cost: 15 c ---[4082]---> BDD-cost: 12 c ---[4080]---> BDD-cost: 11 c ---[4079]---> BDD-cost: 11 c ---[4077]---> BDD-cost: 10 c ---[4072]---> BDD-cost: 12 c ---[4071]---> BDD-cost: 16 c ---[4069]---> BDD-cost: 14 c ---[4067]---> BDD-cost: 13 c ---[4066]---> BDD-cost: 15 c ---[4064]---> BDD-cost: 16 c ---[4063]---> BDD-cost: 10 c ---[4061]---> BDD-cost: 16 c ---[4060]---> BDD-cost: 16 c ---[4059]---> BDD-cost: 16 c ---[4057]---> BDD-cost: 13 c ---[4056]---> BDD-cost: 18 c ---[4055]---> BDD-cost: 14 c ---[4054]---> BDD-cost: 12 c ---[4053]---> BDD-cost: 11 c ---[4052]---> BDD-cost: 13 c ---[4051]---> BDD-cost: 7 c ---[4050]---> BDD-cost: 14 c ---[4049]---> BDD-cost: 13 c ---[4048]---> BDD-cost: 9 c ---[4047]---> BDD-cost: 9 c ---[4046]---> BDD-cost: 13 c ---[4045]---> BDD-cost: 14 c ---[4044]---> BDD-cost: 17 c ---[4042]---> BDD-cost: 11 c ---[4041]---> BDD-cost: 12 c ---[4040]---> BDD-cost: 15 c ---[4039]---> BDD-cost: 19 c ---[4036]---> BDD-cost: 15 c ---[4035]---> BDD-cost: 16 c ---[4034]---> BDD-cost: 18 c ---[4032]---> BDD-cost: 18 c ---[4031]---> BDD-cost: 13 c ---[4030]---> BDD-cost: 18 c ---[4027]---> BDD-cost: 16 c ---[4026]---> BDD-cost: 15 c ---[4025]---> BDD-cost: 18 c ---[4024]---> BDD-cost: 17 c ---[4022]---> BDD-cost: 12 c ---[4021]---> BDD-cost: 15 c ---[4020]---> BDD-cost: 7 c ---[4019]---> BDD-cost: 15 c ---[4018]---> BDD-cost: 13 c ---[4017]---> BDD-cost: 12 c ---[4016]---> BDD-cost: 11 c ---[4015]---> BDD-cost: 13 c ---[4014]---> BDD-cost: 19 c ---[4013]---> BDD-cost: 16 c ---[4010]---> BDD-cost: 16 c ---[4009]---> BDD-cost: 18 c ---[4008]---> BDD-cost: 14 c ---[4007]---> BDD-cost: 15 c ---[4006]---> BDD-cost: 15 c ---[4005]---> BDD-cost: 16 c ---[4003]---> BDD-cost: 16 c ---[4002]---> BDD-cost: 10 c ---[4001]---> BDD-cost: 15 c ---[4000]---> BDD-cost: 15 c ---[3998]---> BDD-cost: 12 c ---[3997]---> BDD-cost: 13 c ---[3996]---> BDD-cost: 17 c ---[3994]---> BDD-cost: 11 c ---[3993]---> BDD-cost: 11 c ---[3992]---> BDD-cost: 10 c ---[3991]---> BDD-cost: 7 c ---[3990]---> BDD-cost: 13 c ---[3989]---> BDD-cost: 11 c ---[3988]---> BDD-cost: 8 c ---[3987]---> BDD-cost: 9 c ---[3986]---> BDD-cost: 11 c ---[3980]---> BDD-cost: 17 c ---[3979]---> BDD-cost: 13 c ---[3977]---> BDD-cost: 12 c ---[3975]---> BDD-cost: 15 c ---[3973]---> BDD-cost: 11 c ---[3972]---> BDD-cost: 7 c ---[3971]---> BDD-cost: 8 c ---[3970]---> BDD-cost: 13 c ---[3969]---> BDD-cost: 11 c ---[3968]---> BDD-cost: 14 c ---[3966]---> BDD-cost: 11 c ---[3965]---> BDD-cost: 10 c ---[3963]---> BDD-cost: 9 c ---[3961]---> BDD-cost: 13 c ---[3958]---> BDD-cost: 17 c ---[3956]---> Sorter-cost: 1853 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3954]---> Adder-cost: 593 maxlim: 310528 bits: 20/19 c ---[3952]---> Adder-cost: 926 maxlim: 1250687 bits: 22/21 c ---[3950]---> Adder-cost: 593 maxlim: 297600 bits: 20/19 c ---[3948]---> Sorter-cost: 3378 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3946]---> Adder-cost: 529 maxlim: 108800 bits: 18/17 c ---[3944]---> Sorter-cost: 3248 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3942]---> Sorter-cost: 2120 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3940]---> Sorter-cost: 3164 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3938]---> Adder-cost: 300 maxlim: 97664 bits: 18/17 c ---[3936]---> BDD-cost: 172 c ---[3934]---> Adder-cost: 300 maxlim: 78976 bits: 18/17 c ---[3932]---> Sorter-cost: 372 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3930]---> BDD-cost: 70 c ---[3928]---> Sorter-cost: 3164 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3926]---> Adder-cost: 593 maxlim: 453888 bits: 20/19 c ---[3924]---> Adder-cost: 593 maxlim: 299136 bits: 20/19 c ---[3922]---> BDD-cost: 58 c ---[3920]---> Sorter-cost: 1562 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3918]---> Adder-cost: 561 maxlim: 248192 bits: 19/18 c ---[3916]---> Sorter-cost: 1087 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3914]---> Adder-cost: 593 maxlim: 321152 bits: 20/19 c ---[3912]---> BDD-cost: 85 c ---[3910]---> Sorter-cost: 2874 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3908]---> Adder-cost: 353 maxlim: 219648 bits: 19/18 c ---[3906]---> Sorter-cost: 2946 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3904]---> Sorter-cost: 3380 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3902]---> Sorter-cost: 473 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3900]---> Adder-cost: 375 maxlim: 60160 bits: 17/16 c ---[3898]---> BDD-cost: 75 c ---[3896]---> Adder-cost: 318 maxlim: 131712 bits: 19/18 c ---[3894]---> Sorter-cost: 1087 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3892]---> Sorter-cost: 1385 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3890]---> Sorter-cost: 2120 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3888]---> BDD-cost: 75 c ---[3886]---> Sorter-cost: 1844 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3884]---> Sorter-cost: 1844 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3882]---> BDD-cost: 170 c ---[3880]---> BDD-cost: 58 c ---[3878]---> BDD-cost: 58 c ---[3876]---> Adder-cost: 293 maxlim: 20224 bits: 16/15 c ---[3874]---> BDD-cost: 50 c ---[3872]---> BDD-cost: 314 c ---[3862]---> BDD-cost: 167 c ---[3860]---> BDD-cost: 314 c ---[3858]---> BDD-cost: 314 c ---[3856]---> BDD-cost: 90 c ---[3854]---> BDD-cost: 90 c ---[3852]---> BDD-cost: 50 c ---[3850]---> BDD-cost: 50 c ---[3840]---> Adder-cost: 404 maxlim: 2557996273 bits: 33/32 c ---[3838]---> Adder-cost: 404 maxlim: 2557996273 bits: 33/32 c ---[3836]---> Adder-cost: 404 maxlim: 2557996273 bits: 33/32 c ---[3828]---> Sorter-cost: 1999 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 2 c ---[3826]---> Sorter-cost: 4718 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3824]---> Sorter-cost: 4748 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3822]---> Sorter-cost: 4702 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3820]---> Sorter-cost: 4702 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3816]---> Sorter-cost: 2732 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[3808]---> Sorter-cost: 3056 Base: 2 2 2 2 2 5 5 5 2 2 2 2 7 2 2 2 c ---[3806]---> Sorter-cost: 4317 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3804]---> Sorter-cost: 4269 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3802]---> Sorter-cost: 4269 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3800]---> Sorter-cost: 4269 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3796]---> Sorter-cost: 3658 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 c ---[3788]---> Sorter-cost: 1577 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 2 c ---[3786]---> Sorter-cost: 3148 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 c ---[3784]---> Sorter-cost: 3178 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 c ---[3782]---> Sorter-cost: 3130 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 c ---[3780]---> Sorter-cost: 3130 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 c ---[3776]---> Sorter-cost: 1872 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 c ---[3768]---> Sorter-cost: 2957 Base: 2 2 2 2 5 5 2 2 2 2 2 2 5 7 2 2 2 c ---[3766]---> Sorter-cost: 4645 Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 c ---[3764]---> Sorter-cost: 4597 Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 2 c ---[3762]---> Sorter-cost: 4597 Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 2 c ---[3760]---> Sorter-cost: 4597 Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 2 c ---[3756]---> Sorter-cost: 3580 Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 5 2 7 2 2 c ---[3748]---> Sorter-cost: 3056 Base: 2 2 2 2 2 5 5 5 2 2 2 2 7 2 2 2 c ---[3746]---> Sorter-cost: 4287 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3744]---> Sorter-cost: 4317 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3742]---> Sorter-cost: 4269 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3740]---> Sorter-cost: 4269 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3736]---> Sorter-cost: 3658 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 c ---[3726]---> BDD-cost: 53 c ---[3724]---> BDD-cost: 53 c ---[3720]---> Sorter-cost: 2016 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 2 2 c ---[3718]---> Sorter-cost: 3242 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[3716]---> Sorter-cost: 3196 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 c ---[3714]---> Sorter-cost: 3196 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 c ---[3712]---> Sorter-cost: 3196 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 c ---[3708]---> Sorter-cost: 2296 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 7 2 2 c ---[3700]---> BDD-cost: 595 c ---[3698]---> Sorter-cost: 3899 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3696]---> Sorter-cost: 3929 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3694]---> Sorter-cost: 3881 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3692]---> Sorter-cost: 3881 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3688]---> Sorter-cost: 3755 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[3680]---> Sorter-cost: 2658 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3678]---> Sorter-cost: 4342 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3676]---> Sorter-cost: 4362 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3674]---> Sorter-cost: 4362 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3672]---> Sorter-cost: 4362 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3668]---> Sorter-cost: 3084 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3660]---> Sorter-cost: 2861 Base: 2 2 2 2 2 2 2 2 2 5 2 2 3 7 2 2 2 2 2 2 c ---[3658]---> Sorter-cost: 4620 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2 c ---[3656]---> Sorter-cost: 4640 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2 c ---[3654]---> Sorter-cost: 4640 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2 c ---[3652]---> Sorter-cost: 4640 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2 c ---[3648]---> Sorter-cost: 3187 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3640]---> BDD-cost: 596 c ---[3638]---> Sorter-cost: 3506 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3636]---> Sorter-cost: 3458 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3634]---> Sorter-cost: 3458 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3632]---> Sorter-cost: 3458 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3628]---> Sorter-cost: 3165 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 7 c ---[3620]---> Sorter-cost: 2658 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3618]---> Sorter-cost: 4342 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3616]---> Sorter-cost: 4362 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3614]---> Sorter-cost: 4362 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3612]---> Sorter-cost: 4362 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3608]---> Sorter-cost: 3084 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3600]---> Sorter-cost: 2705 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[3598]---> BDD-cost: 148 c ---[3594]---> Sorter-cost: 2627 Base: 2 2 2 2 2 2 2 2 2 3 3 3 2 2 2 2 2 2 2 c ---[3592]---> Sorter-cost: 4226 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3590]---> Sorter-cost: 4226 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3588]---> Sorter-cost: 4226 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3586]---> Sorter-cost: 4226 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3582]---> Sorter-cost: 2999 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[3574]---> Sorter-cost: 4674 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 3 2 3 11 2 2 2 c ---[3572]---> Adder-cost: 548 maxlim: 163444290 bits: 29/28 c ---[3570]---> Adder-cost: 666 maxlim: 2615146050 bits: 32/32 c ---[3568]---> Adder-cost: 666 maxlim: 2615146050 bits: 32/32 c ---[3566]---> Adder-cost: 468 maxlim: 1307573025 bits: 32/31 c ---[3564]---> Sorter-cost: 4674 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 3 2 3 11 2 2 2 c ---[3562]---> BDD-cost: 447 c ---[3560]---> Adder-cost: 516 maxlim: 140770970 bits: 29/28 c ---[3558]---> Adder-cost: 544 maxlim: 375389850 bits: 30/29 c ---[3556]---> Adder-cost: 516 maxlim: 140770970 bits: 29/28 c ---[3554]---> BDD-cost: 254 c ---[3552]---> Sorter-cost: 1999 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[3550]---> Sorter-cost: 1999 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[3548]---> Sorter-cost: 1999 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[3546]---> Adder-cost: 390 maxlim: 1301281575 bits: 32/31 c ---[3544]---> Adder-cost: 456 maxlim: 162657870 bits: 29/28 c ---[3542]---> Adder-cost: 560 maxlim: 2602563150 bits: 32/32 c ---[3540]---> Adder-cost: 560 maxlim: 2602563150 bits: 32/32 c ---[3538]---> Adder-cost: 390 maxlim: 1301281575 bits: 32/31 c ---[3536]---> Adder-cost: 370 maxlim: 650640167 bits: 31/30 c ---[3534]---> BDD-cost: 450 c ---[3532]---> Adder-cost: 358 maxlim: 161480550 bits: 28/28 c ---[3530]---> Adder-cost: 358 maxlim: 161480550 bits: 28/28 c ---[3528]---> Adder-cost: 358 maxlim: 161480550 bits: 28/28 c ---[3526]---> Adder-cost: 330 maxlim: 162659111 bits: 29/28 c ---[3524]---> Sorter-cost: 5540 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 c ---[3522]---> BDD-cost: 181 c ---[3520]---> Sorter-cost: 3779 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 c ---[3518]---> Sorter-cost: 3779 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 c ---[3516]---> BDD-cost: 615 c ---[3512]---> BDD-cost: 154 c ---[3510]---> Sorter-cost: 3405 Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3508]---> Sorter-cost: 3405 Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3506]---> Sorter-cost: 3114 Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[3502]---> Sorter-cost: 5380 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 c ---[3500]---> BDD-cost: 154 c ---[3498]---> Sorter-cost: 3650 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2 c ---[3496]---> Sorter-cost: 3650 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2 c ---[3494]---> Sorter-cost: 3650 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2 c ---[3492]---> Sorter-cost: 3650 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2 c ---[3490]---> BDD-cost: 288 c ---[3488]---> Sorter-cost: 3502 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2 c ---[3486]---> Sorter-cost: 4188 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2 c ---[3484]---> BDD-cost: 278 c ---[3482]---> Sorter-cost: 4188 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2 c ---[3480]---> Sorter-cost: 4188 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2 c ---[3478]---> Sorter-cost: 4188 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2 c ---[3476]---> BDD-cost: 463 c ---[3474]---> Sorter-cost: 3748 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2 c ---[3472]---> Sorter-cost: 2140 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 c ---[3470]---> Sorter-cost: 3598 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 2 c ---[3468]---> Sorter-cost: 4750 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 c ---[3466]---> Sorter-cost: 4946 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 3 2 2 c ---[3464]---> Sorter-cost: 2140 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 c ---[3462]---> Sorter-cost: 2140 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 c ---[3460]---> Sorter-cost: 1814 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 c ---[3458]---> Sorter-cost: 1604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 c ---[3450]---> Sorter-cost: 3521 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 3 3 2 2 c ---[3448]---> Adder-cost: 392 maxlim: 15007286 bits: 25/24 c ---[3446]---> Adder-cost: 510 maxlim: 480247350 bits: 30/29 c ---[3444]---> Adder-cost: 510 maxlim: 480247350 bits: 30/29 c ---[3442]---> Sorter-cost: 3521 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 3 3 2 2 c ---[3440]---> Sorter-cost: 3264 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 c ---[3438]---> Sorter-cost: 2793 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 3 3 2 2 c ---[3436]---> Sorter-cost: 2778 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 c ---[3434]---> Sorter-cost: 1368 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 c ---[3432]---> Sorter-cost: 1368 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 c ---[3430]---> Sorter-cost: 1368 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 c ---[3428]---> Sorter-cost: 5758 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 c ---[3426]---> BDD-cost: 173 c ---[3424]---> Adder-cost: 406 maxlim: 2778196813 bits: 33/32 c ---[3422]---> Adder-cost: 406 maxlim: 2778196813 bits: 33/32 c ---[3420]---> BDD-cost: 607 c ---[3416]---> BDD-cost: 172 c ---[3412]---> Sorter-cost: 6191 Base: 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3410]---> BDD-cost: 286 c ---[3408]---> Adder-cost: 490 maxlim: 1601174025 bits: 32/31 c ---[3406]---> Adder-cost: 490 maxlim: 1601174025 bits: 32/31 c ---[3404]---> Adder-cost: 490 maxlim: 1601174025 bits: 32/31 c ---[3402]---> Adder-cost: 490 maxlim: 1601174025 bits: 32/31 c ---[3400]---> BDD-cost: 421 c ---[3398]---> Sorter-cost: 5086 Base: 2 2 2 2 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 c ---[3396]---> Sorter-cost: 3252 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2 c ---[3394]---> BDD-cost: 451 c ---[3392]---> Sorter-cost: 3252 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2 c ---[3390]---> Sorter-cost: 3252 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2 c ---[3388]---> Sorter-cost: 3252 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2 c ---[3386]---> Sorter-cost: 2610 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2 c ---[3384]---> Sorter-cost: 3036 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2 c ---[3382]---> Sorter-cost: 3602 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 3 c ---[3380]---> Adder-cost: 598 maxlim: 14032030650 bits: 35/34 c ---[3378]---> Adder-cost: 598 maxlim: 14032030650 bits: 35/34 c ---[3376]---> Sorter-cost: 4093 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2 2 2 c ---[3374]---> Sorter-cost: 3849 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2 2 2 c ---[3372]---> BDD-cost: 131 c ---[3370]---> Sorter-cost: 3210 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 c ---[3368]---> Sorter-cost: 3524 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 c ---[3366]---> Sorter-cost: 3210 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 c ---[3364]---> BDD-cost: 105 c ---[3356]---> Adder-cost: 384 maxlim: 7049569725 bits: 34/33 c ---[3354]---> Adder-cost: 634 maxlim: 14099139450 bits: 35/34 c ---[3352]---> Adder-cost: 634 maxlim: 14099139450 bits: 35/34 c ---[3350]---> Adder-cost: 384 maxlim: 7049569725 bits: 34/33 c ---[3348]---> Adder-cost: 364 maxlim: 3524781501 bits: 33/32 c ---[3346]---> BDD-cost: 131 c ---[3344]---> Sorter-cost: 5682 Base: 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3342]---> Sorter-cost: 5682 Base: 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3340]---> Sorter-cost: 5682 Base: 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3338]---> BDD-cost: 340 c ---[3336]---> Sorter-cost: 6568 Base: 2 2 2 2 2 5 5 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3334]---> Sorter-cost: 3886 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 3 2 2 2 c ---[3332]---> Sorter-cost: 3886 Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 3 2 2 2 c ---[3330]---> Sorter-cost: 3456 Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 c ---[3328]---> BDD-cost: 152 c ---[3326]---> BDD-cost: 373 c ---[3324]---> Sorter-cost: 4232 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 c ---[3322]---> Sorter-cost: 4232 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 c ---[3320]---> Sorter-cost: 3956 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 c ---[3316]---> Adder-cost: 514 maxlim: 488635950 bits: 30/29 c ---[3314]---> Adder-cost: 514 maxlim: 488635950 bits: 30/29 c ---[3312]---> Adder-cost: 514 maxlim: 488635950 bits: 30/29 c ---[3310]---> Sorter-cost: 2118 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[3308]---> Sorter-cost: 2118 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[3306]---> Sorter-cost: 2118 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[3304]---> BDD-cost: 758 c ---[3302]---> BDD-cost: 754 c ---[3300]---> Sorter-cost: 2265 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 c ---[3298]---> Sorter-cost: 2265 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 c ---[3296]---> Sorter-cost: 2265 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 c ---[3294]---> Sorter-cost: 2491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 7 2 2 c ---[3292]---> Sorter-cost: 2491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 7 2 2 c ---[3290]---> Sorter-cost: 2491 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 7 2 2 c ---[3288]---> Sorter-cost: 1000 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3286]---> Sorter-cost: 1000 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3284]---> Sorter-cost: 1000 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3282]---> Sorter-cost: 4366 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3280]---> Sorter-cost: 3277 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2 c ---[3278]---> Sorter-cost: 3277 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2 c ---[3276]---> Sorter-cost: 3501 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2 c ---[3274]---> Sorter-cost: 3277 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2 c ---[3272]---> Sorter-cost: 3277 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2 c ---[3270]---> BDD-cost: 595 c ---[3268]---> BDD-cost: 530 c ---[3266]---> Sorter-cost: 3151 Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 c ---[3264]---> Sorter-cost: 1392 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[3262]---> Sorter-cost: 1478 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[3260]---> Sorter-cost: 1535 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[3258]---> Sorter-cost: 1478 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[3256]---> Sorter-cost: 1535 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[3254]---> Sorter-cost: 1134 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[3252]---> Sorter-cost: 1191 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[3250]---> Sorter-cost: 5317 Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3248]---> Sorter-cost: 4100 Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 7 2 2 2 c ---[3246]---> Sorter-cost: 4142 Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 c ---[3244]---> Sorter-cost: 4142 Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 c ---[3242]---> Sorter-cost: 3745 Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 c ---[3240]---> Sorter-cost: 3745 Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 c ---[3238]---> BDD-cost: 581 c ---[3236]---> BDD-cost: 529 c ---[3234]---> Sorter-cost: 3523 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 c ---[3232]---> Sorter-cost: 2102 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3 c ---[3230]---> Sorter-cost: 2210 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3 c ---[3228]---> Sorter-cost: 2234 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 c ---[3226]---> Sorter-cost: 2210 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3 c ---[3224]---> Sorter-cost: 2234 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 c ---[3222]---> Sorter-cost: 1778 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3 c ---[3220]---> Sorter-cost: 1802 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 c ---[3218]---> Sorter-cost: 4684 Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3216]---> Sorter-cost: 2644 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3214]---> Sorter-cost: 2644 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3212]---> Sorter-cost: 2879 Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3210]---> Sorter-cost: 2644 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3208]---> Sorter-cost: 2644 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3206]---> Sorter-cost: 2039 Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3204]---> Sorter-cost: 1871 Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[3202]---> Sorter-cost: 6062 Base: 2 2 2 2 2 2 2 2 2 5 2 5 2 2 5 2 2 2 2 2 2 2 2 2 c ---[3200]---> Sorter-cost: 3284 Base: 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 3 c ---[3198]---> Sorter-cost: 3561 Base: 2 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 3 c ---[3196]---> Sorter-cost: 3832 Base: 2 2 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 2 c ---[3194]---> Sorter-cost: 3561 Base: 2 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 3 c ---[3192]---> Sorter-cost: 3832 Base: 2 2 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 2 c ---[3190]---> Sorter-cost: 2300 Base: 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 3 c ---[3188]---> Sorter-cost: 2756 Base: 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 2 c ---[3186]---> Sorter-cost: 5559 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3184]---> Sorter-cost: 3987 Base: 2 2 2 2 2 2 2 2 2 5 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[3182]---> Sorter-cost: 4024 Base: 2 2 2 2 2 2 2 2 2 5 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[3180]---> Sorter-cost: 4024 Base: 2 2 2 2 2 2 2 2 2 5 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[3178]---> Sorter-cost: 3727 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[3176]---> Sorter-cost: 3727 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[3174]---> Sorter-cost: 3052 Base: 2 2 2 2 2 2 5 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[3172]---> Sorter-cost: 2776 Base: 2 2 2 2 2 2 5 2 2 5 2 2 2 2 2 2 2 2 2 c ---[3170]---> Sorter-cost: 6731 Base: 2 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3168]---> Sorter-cost: 3761 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 3 c ---[3166]---> Sorter-cost: 4035 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 3 c ---[3164]---> Sorter-cost: 4126 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 2 2 c ---[3162]---> Sorter-cost: 4035 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 3 c ---[3160]---> Sorter-cost: 4126 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 2 2 c ---[3158]---> Sorter-cost: 2939 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 3 c ---[3156]---> Sorter-cost: 3030 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 2 2 c ---[3154]---> Sorter-cost: 3706 Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3152]---> Sorter-cost: 3706 Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3150]---> Sorter-cost: 3706 Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3148]---> Sorter-cost: 3580 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3146]---> Sorter-cost: 3580 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3144]---> Sorter-cost: 3580 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3142]---> Sorter-cost: 3798 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2 c ---[3140]---> Sorter-cost: 3798 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2 c ---[3138]---> Sorter-cost: 3798 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2 c ---[3136]---> Sorter-cost: 4211 Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3134]---> Sorter-cost: 4211 Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3132]---> Sorter-cost: 4211 Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3130]---> Sorter-cost: 5069 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3128]---> Sorter-cost: 3088 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3126]---> Sorter-cost: 3389 Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3124]---> Sorter-cost: 3088 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3122]---> Sorter-cost: 3696 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3120]---> Sorter-cost: 3696 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3118]---> Sorter-cost: 3696 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3116]---> Sorter-cost: 3172 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2 2 2 c ---[3114]---> Sorter-cost: 1456 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[3112]---> Sorter-cost: 1456 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[3110]---> Sorter-cost: 1370 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[3108]---> Sorter-cost: 2101 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2 c ---[3106]---> Sorter-cost: 2101 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2 c ---[3104]---> Sorter-cost: 2101 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2 c ---[3102]---> Sorter-cost: 3791 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 c ---[3100]---> Sorter-cost: 2107 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 c ---[3098]---> Sorter-cost: 2101 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2 c ---[3096]---> Sorter-cost: 2107 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 c ---[3094]---> Sorter-cost: 1542 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[3092]---> Sorter-cost: 1542 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[3090]---> Sorter-cost: 1542 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[3088]---> Sorter-cost: 5054 Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3086]---> Sorter-cost: 2867 Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 3 2 2 2 3 c ---[3084]---> Sorter-cost: 2935 Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 c ---[3082]---> Sorter-cost: 2867 Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 3 2 2 2 3 c ---[3080]---> Sorter-cost: 2935 Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 c ---[3078]---> Sorter-cost: 2935 Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 c ---[3076]---> Sorter-cost: 2935 Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 c ---[3074]---> Adder-cost: 1048 maxlim: 22769277786 bits: 35/35 c ---[3072]---> Adder-cost: 1048 maxlim: 22769277786 bits: 35/35 c ---[3070]---> Adder-cost: 1048 maxlim: 22769277786 bits: 35/35 c ---[3068]---> Adder-cost: 1868 maxlim: 1273684285 bits: 32/31 c ---[3066]---> Adder-cost: 2325 maxlim: 1783847576 bits: 32/31 c ---[3064]---> Adder-cost: 2055 maxlim: 1724964795 bits: 32/31 c ---[3062]---> Sorter-cost: 2144 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3060]---> Sorter-cost: 6043 Base: 11 11 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 3 c ---[3058]---> Adder-cost: 544 maxlim: 761265450 bits: 31/30 c ---[3056]---> Sorter-cost: 6043 Base: 11 11 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 3 c ---[3054]---> Adder-cost: 544 maxlim: 761265450 bits: 31/30 c ---[3052]---> Adder-cost: 544 maxlim: 761265450 bits: 31/30 c ---[3050]---> Adder-cost: 544 maxlim: 761265450 bits: 31/30 c ---[3048]---> Adder-cost: 346 maxlim: 80740198 bits: 28/27 c ---[3046]---> Sorter-cost: 4195 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 3 2 c ---[3044]---> Adder-cost: 364 maxlim: 161480550 bits: 29/28 c ---[3042]---> Adder-cost: 364 maxlim: 161480550 bits: 29/28 c ---[3040]---> Adder-cost: 364 maxlim: 161480550 bits: 29/28 c ---[3038]---> Sorter-cost: 3199 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 11 2 2 2 2 c ---[3036]---> Adder-cost: 307 maxlim: 122158871 bits: 28/27 c ---[3034]---> Adder-cost: 325 maxlim: 244317975 bits: 29/28 c ---[3032]---> Adder-cost: 307 maxlim: 122158871 bits: 28/27 c ---[3030]---> Adder-cost: 325 maxlim: 244317975 bits: 29/28 c ---[3028]---> Adder-cost: 325 maxlim: 244317975 bits: 29/28 c ---[3026]---> Adder-cost: 325 maxlim: 244317975 bits: 29/28 c ---[3024]---> Sorter-cost: 2602 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 c ---[3022]---> Sorter-cost: 2602 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 c ---[3020]---> Sorter-cost: 2602 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 c ---[3018]---> Sorter-cost: 3051 Base: 2 2 2 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3016]---> Sorter-cost: 3584 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 3 2 2 2 c ---[3006]---> Sorter-cost: 3810 Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 c ---[3004]---> Sorter-cost: 4239 Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[3002]---> Sorter-cost: 4239 Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[3000]---> BDD-cost: 388 c ---[2998]---> BDD-cost: 388 c ---[2988]---> BDD-cost: 212 c ---[2986]---> BDD-cost: 212 c ---[2976]---> Sorter-cost: 4072 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2974]---> Sorter-cost: 4163 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2972]---> Sorter-cost: 4163 Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2970]---> Sorter-cost: 2881 Base: 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 c ---[2968]---> Sorter-cost: 3830 Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3 c ---[2966]---> Sorter-cost: 3844 Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2964]---> Sorter-cost: 3844 Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2962]---> Sorter-cost: 3817 Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3 c ---[2960]---> Sorter-cost: 3844 Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2958]---> Sorter-cost: 3844 Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2956]---> Sorter-cost: 4249 Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2954]---> Sorter-cost: 3817 Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3 c ---[2952]---> Sorter-cost: 3844 Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2950]---> Sorter-cost: 3844 Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2948]---> Sorter-cost: 6254 Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2946]---> Sorter-cost: 2693 Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2944]---> Sorter-cost: 3888 Base: 2 2 5 5 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2942]---> Sorter-cost: 6254 Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2940]---> Sorter-cost: 3461 Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3 c ---[2938]---> Sorter-cost: 3473 Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2936]---> Sorter-cost: 3473 Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2934]---> BDD-cost: 389 c ---[2932]---> Sorter-cost: 4239 Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[2908]---> Sorter-cost: 5511 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2906]---> Sorter-cost: 5339 Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[2904]---> Sorter-cost: 5480 Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 3 5 2 c ---[2894]---> Sorter-cost: 2986 Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2892]---> Sorter-cost: 3420 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2890]---> Sorter-cost: 2929 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[2888]---> Sorter-cost: 3817 Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2886]---> Sorter-cost: 3934 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2884]---> Sorter-cost: 3365 Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2882]---> Sorter-cost: 3263 Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 5 2 c ---[2880]---> BDD-cost: 370 c ---[2878]---> Sorter-cost: 3866 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 5 2 2 2 2 2 2 c ---[2876]---> Sorter-cost: 3866 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 5 2 2 2 2 2 2 c ---[2874]---> Sorter-cost: 3684 Base: 2 2 2 2 5 5 5 2 2 2 2 2 5 2 2 2 2 2 2 c ---[2870]---> BDD-cost: 133 c ---[2866]---> Sorter-cost: 3117 Base: 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2864]---> Sorter-cost: 1880 Base: 2 5 5 5 2 2 2 2 2 2 2 c ---[2862]---> Sorter-cost: 2828 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 c ---[2860]---> Sorter-cost: 3165 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[2858]---> Sorter-cost: 1339 Base: 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 c ---[2856]---> Sorter-cost: 2247 Base: 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[2854]---> Sorter-cost: 2075 Base: 2 5 5 5 2 2 2 2 2 2 2 c ---[2852]---> Sorter-cost: 1880 Base: 2 5 5 5 2 2 2 2 2 2 2 c ---[2850]---> Sorter-cost: 2828 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 c ---[2848]---> Sorter-cost: 3165 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[2846]---> Sorter-cost: 2806 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 c ---[2844]---> Sorter-cost: 5284 Base: 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[2842]---> BDD-cost: 171 c ---[2840]---> Sorter-cost: 3874 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 c ---[2838]---> Sorter-cost: 3874 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 c ---[2836]---> Sorter-cost: 2253 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 c ---[2834]---> Sorter-cost: 3129 Base: 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2 c ---[2832]---> Sorter-cost: 3587 Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 c ---[2830]---> BDD-cost: 171 c ---[2828]---> Sorter-cost: 3874 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 c ---[2826]---> Sorter-cost: 3874 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 c ---[2824]---> Sorter-cost: 3864 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 c ---[2822]---> Sorter-cost: 1420 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ---[2820]---> Sorter-cost: 2034 Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 5 2 c ---[2818]---> Adder-cost: 280 maxlim: 17301471 bits: 26/25 c ---[2816]---> Adder-cost: 280 maxlim: 17301471 bits: 26/25 c ---[2814]---> Sorter-cost: 2727 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 5 2 c ---[2
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/4588/stat): 4588 (minisat+_script) R 4587 4588 19818 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855037271 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/4588/statm): 174 3 169 147 0 27 0 [pid=4588] 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=4589 New process pid=4590 New process pid=4591 execve syscall for /bin/sed executable One traced child (pid=4590) 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=4591) exited with status: 0 One traced child (pid=4589) exited with status: 0 New process pid=4592 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-greenbea.opb [startup+10.0035 s] Raw data (loadavg): 0.84 0.94 0.90 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 13980 0 0 0 841 76 0 0 25 0 1 0 1855037276 60293120 13677 4294967295 134512640 135094434 3221224432 3221223248 134580024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 14720 13677 145 145 0 14575 0 [pid=4592] vsize: 58880 Current children cumulated CPU time (s) 9.18 Current children cumulated vsize (Kb) 61004 [startup+20.0043 s] Raw data (loadavg): 0.87 0.94 0.90 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 14547 0 0 0 1838 78 0 0 25 0 1 0 1855037276 57880576 13110 4294967295 134512640 135094434 3221224432 3221220752 134677284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4592/statm): 14131 13110 145 145 0 13986 0 [pid=4592] vsize: 56524 Current children cumulated CPU time (s) 19.17 Current children cumulated vsize (Kb) 58648 [startup+30.0051 s] Raw data (loadavg): 0.89 0.94 0.90 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 14988 0 0 0 2835 79 0 0 25 0 1 0 1855037276 57942016 13125 4294967295 134512640 135094434 3221224432 3221220988 134677228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4592/statm): 14146 13125 145 145 0 14001 0 [pid=4592] vsize: 56584 Current children cumulated CPU time (s) 29.15 Current children cumulated vsize (Kb) 58708 [startup+40.0059 s] Raw data (loadavg): 0.90 0.94 0.90 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 15419 0 0 0 3833 81 0 0 25 0 1 0 1855037276 57966592 13131 4294967295 134512640 135094434 3221224432 3221220928 134676532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4592/statm): 14152 13131 145 145 0 14007 0 [pid=4592] vsize: 56608 Current children cumulated CPU time (s) 39.15 Current children cumulated vsize (Kb) 58732 [startup+50.0066 s] Raw data (loadavg): 0.92 0.95 0.90 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 15419 0 0 0 4833 81 0 0 25 0 1 0 1855037276 57966592 13131 4294967295 134512640 135094434 3221224432 3221221104 134600175 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4592/statm): 14152 13131 145 145 0 14007 0 [pid=4592] vsize: 56608 Current children cumulated CPU time (s) 49.15 Current children cumulated vsize (Kb) 58732 [startup+60.0074 s] Raw data (loadavg): 0.93 0.95 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 15701 0 0 0 5832 82 0 0 25 0 1 0 1855037276 59539456 13413 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4592/statm): 14536 13413 145 145 0 14391 0 [pid=4592] vsize: 58144 Current children cumulated CPU time (s) 59.15 Current children cumulated vsize (Kb) 60268 [startup+70.0082 s] Raw data (loadavg): 0.94 0.95 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 15849 0 0 0 6831 83 0 0 25 0 1 0 1855037276 61112320 13519 4294967295 134512640 135094434 3221224432 3221220832 134676328 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4592/statm): 14920 13519 145 145 0 14775 0 [pid=4592] vsize: 59680 Current children cumulated CPU time (s) 69.15 Current children cumulated vsize (Kb) 61804 [startup+80.009 s] Raw data (loadavg): 0.95 0.95 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 16010 0 0 0 7831 84 0 0 25 0 1 0 1855037276 61308928 13638 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 14968 13638 145 145 0 14823 0 [pid=4592] vsize: 59872 Current children cumulated CPU time (s) 79.16 Current children cumulated vsize (Kb) 61996 [startup+90.0098 s] Raw data (loadavg): 0.96 0.95 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18294 0 0 0 8821 91 0 0 25 0 1 0 1855037276 66363392 14972 4294967295 134512640 135094434 3221224432 3221222512 134600301 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 16202 14972 145 145 0 16057 0 [pid=4592] vsize: 64808 Current children cumulated CPU time (s) 89.13 Current children cumulated vsize (Kb) 66932 [startup+100.011 s] Raw data (loadavg): 0.96 0.95 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18359 0 0 0 9821 91 0 0 25 0 1 0 1855037276 66363392 15037 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 16202 15037 145 145 0 16057 0 [pid=4592] vsize: 64808 Current children cumulated CPU time (s) 99.13 Current children cumulated vsize (Kb) 66932 [startup+110.011 s] Raw data (loadavg): 0.97 0.95 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18415 0 0 0 10821 91 0 0 25 0 1 0 1855037276 66363392 15093 4294967295 134512640 135094434 3221224432 3221221072 134518677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 16202 15093 145 145 0 16057 0 [pid=4592] vsize: 64808 Current children cumulated CPU time (s) 109.13 Current children cumulated vsize (Kb) 66932 [startup+120.012 s] Raw data (loadavg): 0.97 0.95 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18468 0 0 0 11821 91 0 0 25 0 1 0 1855037276 66363392 15146 4294967295 134512640 135094434 3221224432 3221220960 134783376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 16202 15146 145 145 0 16057 0 [pid=4592] vsize: 64808 Current children cumulated CPU time (s) 119.13 Current children cumulated vsize (Kb) 66932 [startup+130.013 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18538 0 0 0 12821 91 0 0 25 0 1 0 1855037276 69509120 15216 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 16970 15216 145 145 0 16825 0 [pid=4592] vsize: 67880 Current children cumulated CPU time (s) 129.13 Current children cumulated vsize (Kb) 70004 [startup+140.014 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18709 0 0 0 13821 92 0 0 25 0 1 0 1855037276 69509120 15304 4294967295 134512640 135094434 3221224432 3221221888 134676328 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 16970 15304 145 145 0 16825 0 [pid=4592] vsize: 67880 Current children cumulated CPU time (s) 139.14 Current children cumulated vsize (Kb) 70004 [startup+150.014 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18838 0 0 0 14821 92 0 0 25 0 1 0 1855037276 69509120 15350 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 16970 15350 145 145 0 16825 0 [pid=4592] vsize: 67880 Current children cumulated CPU time (s) 149.14 Current children cumulated vsize (Kb) 70004 [startup+160.015 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 19663 0 0 0 15816 95 0 0 25 0 1 0 1855037276 70254592 15563 4294967295 134512640 135094434 3221224432 3221220576 134600232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 17152 15563 145 145 0 17007 0 [pid=4592] vsize: 68608 Current children cumulated CPU time (s) 159.12 Current children cumulated vsize (Kb) 70732 [startup+170.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 19663 0 0 0 16816 95 0 0 25 0 1 0 1855037276 70254592 15563 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 17152 15563 145 145 0 17007 0 [pid=4592] vsize: 68608 Current children cumulated CPU time (s) 169.12 Current children cumulated vsize (Kb) 70732 [startup+180.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 20007 0 0 0 17815 95 0 0 25 0 1 0 1855037276 70311936 15585 4294967295 134512640 135094434 3221224432 3221220992 134677086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 17166 15585 145 145 0 17021 0 [pid=4592] vsize: 68664 Current children cumulated CPU time (s) 179.11 Current children cumulated vsize (Kb) 70788 [startup+190.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 20136 0 0 0 18815 96 0 0 25 0 1 0 1855037276 70311936 15589 4294967295 134512640 135094434 3221224432 3221219344 134677239 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 17166 15589 145 145 0 17021 0 [pid=4592] vsize: 68664 Current children cumulated CPU time (s) 189.12 Current children cumulated vsize (Kb) 70788 [startup+200.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 20261 0 0 0 19815 96 0 0 25 0 1 0 1855037276 70311936 15589 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 17166 15589 145 145 0 17021 0 [pid=4592] vsize: 68664 Current children cumulated CPU time (s) 199.12 Current children cumulated vsize (Kb) 70788 [startup+210.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 21718 0 0 0 20812 99 0 0 25 0 1 0 1855037276 73011200 16262 4294967295 134512640 135094434 3221224432 3221220672 134677065 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 17825 16262 145 145 0 17680 0 [pid=4592] vsize: 71300 Current children cumulated CPU time (s) 209.12 Current children cumulated vsize (Kb) 73424 [startup+220.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 22650 0 0 0 21808 102 0 0 25 0 1 0 1855037276 72998912 16287 4294967295 134512640 135094434 3221224432 3221220576 134677284 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 17822 16287 145 145 0 17677 0 [pid=4592] vsize: 71288 Current children cumulated CPU time (s) 219.11 Current children cumulated vsize (Kb) 73412 [startup+230.019 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 23181 0 0 0 22806 104 0 0 25 0 1 0 1855037276 72912896 16275 4294967295 134512640 135094434 3221224432 3221222864 134600186 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 17801 16275 145 145 0 17656 0 [pid=4592] vsize: 71204 Current children cumulated CPU time (s) 229.11 Current children cumulated vsize (Kb) 73328 [startup+240.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 25941 0 0 0 23790 113 0 0 25 0 1 0 1855037276 72953856 16293 4294967295 134512640 135094434 3221224432 3221220564 134600238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4592/statm): 17811 16293 145 145 0 17666 0 [pid=4592] vsize: 71244 Current children cumulated CPU time (s) 239.04 Current children cumulated vsize (Kb) 73368 [startup+250.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 27293 0 0 0 24783 117 0 0 25 0 1 0 1855037276 75235328 16860 4294967295 134512640 135094434 3221224432 3221220576 134676586 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 18368 16860 145 145 0 18223 0 [pid=4592] vsize: 73472 Current children cumulated CPU time (s) 249.01 Current children cumulated vsize (Kb) 75596 [startup+260.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 27818 0 0 0 25781 118 0 0 25 0 1 0 1855037276 75313152 16890 4294967295 134512640 135094434 3221224432 3221220576 134600151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 18387 16890 145 145 0 18242 0 [pid=4592] vsize: 73548 Current children cumulated CPU time (s) 259 Current children cumulated vsize (Kb) 75672 [startup+270.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 29181 0 0 0 26777 122 0 0 25 0 1 0 1855037276 75313152 16932 4294967295 134512640 135094434 3221224432 3221220220 134600233 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4592/statm): 18387 16932 145 145 0 18242 0 [pid=4592] vsize: 73548 Current children cumulated CPU time (s) 269 Current children cumulated vsize (Kb) 75672 [startup+280.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 29528 0 0 0 27777 123 0 0 25 0 1 0 1855037276 75313152 16948 4294967295 134512640 135094434 3221224432 3221221340 134677378 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 18387 16948 145 145 0 18242 0 [pid=4592] vsize: 73548 Current children cumulated CPU time (s) 279.01 Current children cumulated vsize (Kb) 75672 [startup+290.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 30045 0 0 0 28776 124 0 0 25 0 1 0 1855037276 75313152 16969 4294967295 134512640 135094434 3221224432 3221219872 134600269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 18387 16969 145 145 0 18242 0 [pid=4592] vsize: 73548 Current children cumulated CPU time (s) 289.01 Current children cumulated vsize (Kb) 75672 [startup+300.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 30304 0 0 0 29775 125 0 0 25 0 1 0 1855037276 75313152 16980 4294967295 134512640 135094434 3221224432 3221221280 134600267 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 18387 16980 145 145 0 18242 0 [pid=4592] vsize: 73548 Current children cumulated CPU time (s) 299.01 Current children cumulated vsize (Kb) 75672 [startup+310.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 30919 0 0 0 30774 126 0 0 25 0 1 0 1855037276 75313152 17015 4294967295 134512640 135094434 3221224432 3221220080 134780815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 18387 17015 145 145 0 18242 0 [pid=4592] vsize: 73548 Current children cumulated CPU time (s) 309.01 Current children cumulated vsize (Kb) 75672 [startup+320.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 31109 0 0 0 31774 126 0 0 25 0 1 0 1855037276 75313152 17039 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 18387 17039 145 145 0 18242 0 [pid=4592] vsize: 73548 Current children cumulated CPU time (s) 319.01 Current children cumulated vsize (Kb) 75672 [startup+330.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 31368 0 0 0 32773 127 0 0 25 0 1 0 1855037276 75313152 17132 4294967295 134512640 135094434 3221224432 3221220740 134600238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 18387 17132 145 145 0 18242 0 [pid=4592] vsize: 73548 Current children cumulated CPU time (s) 329.01 Current children cumulated vsize (Kb) 75672 [startup+340.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 31421 0 0 0 33773 127 0 0 25 0 1 0 1855037276 75313152 17185 4294967295 134512640 135094434 3221224432 3221221152 134677233 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 18387 17185 145 145 0 18242 0 [pid=4592] vsize: 73548 Current children cumulated CPU time (s) 339.01 Current children cumulated vsize (Kb) 75672 [startup+350.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34003 0 0 0 34761 135 0 0 25 0 1 0 1855037276 79347712 18200 4294967295 134512640 135094434 3221224432 3221220120 134676334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 19372 18200 145 145 0 19227 0 [pid=4592] vsize: 77488 Current children cumulated CPU time (s) 348.97 Current children cumulated vsize (Kb) 79612 [startup+360.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34344 0 0 0 35760 135 0 0 25 0 1 0 1855037276 79347712 18211 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 19372 18211 145 145 0 19227 0 [pid=4592] vsize: 77488 Current children cumulated CPU time (s) 358.96 Current children cumulated vsize (Kb) 79612 [startup+370.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34677 0 0 0 36760 136 0 0 25 0 1 0 1855037276 79347712 18214 4294967295 134512640 135094434 3221224432 3221219400 134676461 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 19372 18214 145 145 0 19227 0 [pid=4592] vsize: 77488 Current children cumulated CPU time (s) 368.97 Current children cumulated vsize (Kb) 79612 [startup+380.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34691 0 0 0 37760 136 0 0 25 0 1 0 1855037276 79347712 18228 4294967295 134512640 135094434 3221224432 3221220912 134600241 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 19372 18228 145 145 0 19227 0 [pid=4592] vsize: 77488 Current children cumulated CPU time (s) 378.97 Current children cumulated vsize (Kb) 79612 [startup+390.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34704 0 0 0 38760 136 0 0 25 0 1 0 1855037276 79347712 18241 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 19372 18241 145 145 0 19227 0 [pid=4592] vsize: 77488 Current children cumulated CPU time (s) 388.97 Current children cumulated vsize (Kb) 79612 [startup+400.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34704 0 0 0 39760 136 0 0 25 0 1 0 1855037276 79347712 18241 4294967295 134512640 135094434 3221224432 3221220560 134600246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 19372 18241 145 145 0 19227 0 [pid=4592] vsize: 77488 Current children cumulated CPU time (s) 398.97 Current children cumulated vsize (Kb) 79612 [startup+410.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34707 0 0 0 40761 136 0 0 25 0 1 0 1855037276 79347712 18244 4294967295 134512640 135094434 3221224432 3221221632 134677340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 19372 18244 145 145 0 19227 0 [pid=4592] vsize: 77488 Current children cumulated CPU time (s) 408.98 Current children cumulated vsize (Kb) 79612 [startup+420.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34710 0 0 0 41761 136 0 0 25 0 1 0 1855037276 79347712 18247 4294967295 134512640 135094434 3221224432 3221220732 134676240 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 19372 18247 145 145 0 19227 0 [pid=4592] vsize: 77488 Current children cumulated CPU time (s) 418.98 Current children cumulated vsize (Kb) 79612 [startup+430.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34713 0 0 0 42761 136 0 0 25 0 1 0 1855037276 79347712 18250 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 19372 18250 145 145 0 19227 0 [pid=4592] vsize: 77488 Current children cumulated CPU time (s) 428.98 Current children cumulated vsize (Kb) 79612 [startup+440.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34738 0 0 0 43761 136 0 0 25 0 1 0 1855037276 79347712 18275 4294967295 134512640 135094434 3221224432 3221221176 134677084 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4592/statm): 19372 18275 145 145 0 19227 0 [pid=4592] vsize: 77488 Current children cumulated CPU time (s) 438.98 Current children cumulated vsize (Kb) 79612 [startup+450.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 36601 0 0 0 44753 141 0 0 25 0 1 0 1855037276 81379328 18819 4294967295 134512640 135094434 3221224432 3221219344 134600314 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 19868 18819 145 145 0 19723 0 [pid=4592] vsize: 79472 Current children cumulated CPU time (s) 448.95 Current children cumulated vsize (Kb) 81596 [startup+460.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 38303 0 0 0 45749 145 0 0 25 0 1 0 1855037276 81502208 18872 4294967295 134512640 135094434 3221224432 3221221632 134676503 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 19898 18872 145 145 0 19753 0 [pid=4592] vsize: 79592 Current children cumulated CPU time (s) 458.95 Current children cumulated vsize (Kb) 81716 [startup+470.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 39660 0 0 0 46746 148 0 0 25 0 1 0 1855037276 87793664 18909 4294967295 134512640 135094434 3221224432 3221221104 134600301 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21434 18909 145 145 0 21289 0 [pid=4592] vsize: 85736 Current children cumulated CPU time (s) 468.95 Current children cumulated vsize (Kb) 87860 [startup+480.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 40921 0 0 0 47742 152 0 0 25 0 1 0 1855037276 87797760 18920 4294967295 134512640 135094434 3221224432 3221220192 134676245 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21435 18920 145 145 0 21290 0 [pid=4592] vsize: 85740 Current children cumulated CPU time (s) 478.95 Current children cumulated vsize (Kb) 87864 [startup+490.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 40921 0 0 0 48742 152 0 0 25 0 1 0 1855037276 87797760 18920 4294967295 134512640 135094434 3221224432 3221221964 134676240 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21435 18920 145 145 0 21290 0 [pid=4592] vsize: 85740 Current children cumulated CPU time (s) 488.95 Current children cumulated vsize (Kb) 87864 [startup+500.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 42198 0 0 0 49739 155 0 0 25 0 1 0 1855037276 87732224 18915 4294967295 134512640 135094434 3221224432 3221220848 134677056 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21419 18915 145 145 0 21274 0 [pid=4592] vsize: 85676 Current children cumulated CPU time (s) 498.95 Current children cumulated vsize (Kb) 87800 [startup+510.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 42198 0 0 0 50739 155 0 0 25 0 1 0 1855037276 87732224 18915 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21419 18915 145 145 0 21274 0 [pid=4592] vsize: 85676 Current children cumulated CPU time (s) 508.95 Current children cumulated vsize (Kb) 87800 [startup+520.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 42696 0 0 0 51738 156 0 0 25 0 1 0 1855037276 87732224 18918 4294967295 134512640 135094434 3221224432 3221221104 134676598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21419 18918 145 145 0 21274 0 [pid=4592] vsize: 85676 Current children cumulated CPU time (s) 518.95 Current children cumulated vsize (Kb) 87800 [startup+530.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 43191 0 0 0 52737 157 0 0 25 0 1 0 1855037276 87732224 18918 4294967295 134512640 135094434 3221224432 3221220144 134676376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21419 18918 145 145 0 21274 0 [pid=4592] vsize: 85676 Current children cumulated CPU time (s) 528.95 Current children cumulated vsize (Kb) 87800 [startup+540.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 43365 0 0 0 53737 157 0 0 25 0 1 0 1855037276 87732224 18927 4294967295 134512640 135094434 3221224432 3221220752 134677327 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21419 18927 145 145 0 21274 0 [pid=4592] vsize: 85676 Current children cumulated CPU time (s) 538.95 Current children cumulated vsize (Kb) 87800 [startup+550.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 44060 0 0 0 54735 159 0 0 25 0 1 0 1855037276 87732224 18962 4294967295 134512640 135094434 3221224432 3221220320 134677059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21419 18962 145 145 0 21274 0 [pid=4592] vsize: 85676 Current children cumulated CPU time (s) 548.95 Current children cumulated vsize (Kb) 87800 [startup+560.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 44078 0 0 0 55735 159 0 0 25 0 1 0 1855037276 87732224 18980 4294967295 134512640 135094434 3221224432 3221221260 134677150 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21419 18980 145 145 0 21274 0 [pid=4592] vsize: 85676 Current children cumulated CPU time (s) 558.95 Current children cumulated vsize (Kb) 87800 [startup+570.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 44090 0 0 0 56736 159 0 0 25 0 1 0 1855037276 87732224 18992 4294967295 134512640 135094434 3221224432 3221221012 134677077 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21419 18992 145 145 0 21274 0 [pid=4592] vsize: 85676 Current children cumulated CPU time (s) 568.96 Current children cumulated vsize (Kb) 87800 [startup+580.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 44101 0 0 0 57736 159 0 0 25 0 1 0 1855037276 87732224 19003 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21419 19003 145 145 0 21274 0 [pid=4592] vsize: 85676 Current children cumulated CPU time (s) 578.96 Current children cumulated vsize (Kb) 87800 [startup+590.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 44137 0 0 0 58736 159 0 0 25 0 1 0 1855037276 87732224 19039 4294967295 134512640 135094434 3221224432 3221220928 134676510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 21419 19039 145 145 0 21274 0 [pid=4592] vsize: 85676 Current children cumulated CPU time (s) 588.96 Current children cumulated vsize (Kb) 87800 [startup+600.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) T 4588 4588 19818 0 -1 0 45328 0 0 0 59733 162 0 0 25 0 1 0 1855037276 90431488 19735 4294967295 134512640 135094434 3221224432 3221209308 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/4592/statm): 22078 19735 145 145 0 21933 0 [pid=4592] vsize: 88312 Current children cumulated CPU time (s) 598.96 Current children cumulated vsize (Kb) 90436 [startup+610.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 69602 0 0 0 60599 241 0 0 25 0 1 0 1855037276 122236928 27506 4294967295 134512640 135094434 3221224432 3221221456 134599950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4592/statm): 29843 27506 145 145 0 29698 0 [pid=4592] vsize: 119372 Current children cumulated CPU time (s) 608.41 Current children cumulated vsize (Kb) 121496 [startup+620.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 69687 0 0 0 61599 241 0 0 25 0 1 0 1855037276 122236928 27591 4294967295 134512640 135094434 3221224432 3221221376 134519050 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 29843 27591 145 145 0 29698 0 [pid=4592] vsize: 119372 Current children cumulated CPU time (s) 618.41 Current children cumulated vsize (Kb) 121496 [startup+630.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 69771 0 0 0 62599 241 0 0 25 0 1 0 1855037276 122236928 27675 4294967295 134512640 135094434 3221224432 3221220032 134600241 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 29843 27675 145 145 0 29698 0 [pid=4592] vsize: 119372 Current children cumulated CPU time (s) 628.41 Current children cumulated vsize (Kb) 121496 [startup+640.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 69808 0 0 0 63599 241 0 0 25 0 1 0 1855037276 122236928 27712 4294967295 134512640 135094434 3221224432 3221220636 134677228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 29843 27712 145 145 0 29698 0 [pid=4592] vsize: 119372 Current children cumulated CPU time (s) 638.41 Current children cumulated vsize (Kb) 121496 [startup+650.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72524 0 0 0 64592 248 0 0 25 0 1 0 1855037276 127639552 29110 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29110 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 648.41 Current children cumulated vsize (Kb) 126772 [startup+660.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72605 0 0 0 65593 248 0 0 25 0 1 0 1855037276 127639552 29191 4294967295 134512640 135094434 3221224432 3221220672 134677138 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29191 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 658.42 Current children cumulated vsize (Kb) 126772 [startup+670.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72625 0 0 0 66593 248 0 0 25 0 1 0 1855037276 127639552 29211 4294967295 134512640 135094434 3221224432 3221220024 134676989 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29211 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 668.42 Current children cumulated vsize (Kb) 126772 [startup+680.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72636 0 0 0 67593 248 0 0 25 0 1 0 1855037276 127639552 29222 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29222 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 678.42 Current children cumulated vsize (Kb) 126772 [startup+690.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72664 0 0 0 68593 249 0 0 25 0 1 0 1855037276 127639552 29250 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29250 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 688.43 Current children cumulated vsize (Kb) 126772 [startup+700.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72689 0 0 0 69593 249 0 0 25 0 1 0 1855037276 127639552 29275 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29275 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 698.43 Current children cumulated vsize (Kb) 126772 [startup+710.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72724 0 0 0 70593 249 0 0 25 0 1 0 1855037276 127639552 29310 4294967295 134512640 135094434 3221224432 3221221104 134600151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29310 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 708.43 Current children cumulated vsize (Kb) 126772 [startup+720.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72764 0 0 0 71593 249 0 0 25 0 1 0 1855037276 127639552 29350 4294967295 134512640 135094434 3221224432 3221221600 134518676 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29350 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 718.43 Current children cumulated vsize (Kb) 126772 [startup+730.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72794 0 0 0 72593 249 0 0 25 0 1 0 1855037276 127639552 29380 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29380 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 728.43 Current children cumulated vsize (Kb) 126772 [startup+740.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72818 0 0 0 73594 249 0 0 25 0 1 0 1855037276 127639552 29404 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29404 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 738.44 Current children cumulated vsize (Kb) 126772 [startup+750.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72850 0 0 0 74594 249 0 0 25 0 1 0 1855037276 127639552 29436 4294967295 134512640 135094434 3221224432 3221220576 134600215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29436 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 748.44 Current children cumulated vsize (Kb) 126772 [startup+760.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72913 0 0 0 75594 249 0 0 25 0 1 0 1855037276 127639552 29499 4294967295 134512640 135094434 3221224432 3221218288 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29499 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 758.44 Current children cumulated vsize (Kb) 126772 [startup+770.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72969 0 0 0 76594 249 0 0 25 0 1 0 1855037276 127639552 29555 4294967295 134512640 135094434 3221224432 3221220672 134676321 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29555 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 768.44 Current children cumulated vsize (Kb) 126772 [startup+780.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73027 0 0 0 77594 250 0 0 25 0 1 0 1855037276 127639552 29613 4294967295 134512640 135094434 3221224432 3221220736 134600162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29613 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 778.45 Current children cumulated vsize (Kb) 126772 [startup+790.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73132 0 0 0 78594 250 0 0 25 0 1 0 1855037276 127639552 29718 4294967295 134512640 135094434 3221224432 3221221456 134677366 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29718 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 788.45 Current children cumulated vsize (Kb) 126772 [startup+800.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73193 0 0 0 79594 250 0 0 25 0 1 0 1855037276 127639552 29779 4294967295 134512640 135094434 3221224432 3221221000 134676334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29779 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 798.45 Current children cumulated vsize (Kb) 126772 [startup+810.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73221 0 0 0 80594 250 0 0 25 0 1 0 1855037276 127639552 29807 4294967295 134512640 135094434 3221224432 3221220472 134677084 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29807 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 808.45 Current children cumulated vsize (Kb) 126772 [startup+820.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73221 0 0 0 81594 250 0 0 25 0 1 0 1855037276 127639552 29807 4294967295 134512640 135094434 3221224432 3221220652 134676331 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29807 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 818.45 Current children cumulated vsize (Kb) 126772 [startup+830.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73221 0 0 0 82595 250 0 0 25 0 1 0 1855037276 127639552 29807 4294967295 134512640 135094434 3221224432 3221221952 134676245 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29807 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 828.46 Current children cumulated vsize (Kb) 126772 [startup+840.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73221 0 0 0 83595 250 0 0 25 0 1 0 1855037276 127639552 29807 4294967295 134512640 135094434 3221224432 3221222160 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29807 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 838.46 Current children cumulated vsize (Kb) 126772 [startup+850.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73249 0 0 0 84595 250 0 0 25 0 1 0 1855037276 127639552 29835 4294967295 134512640 135094434 3221224432 3221220048 134677354 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29835 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 848.46 Current children cumulated vsize (Kb) 126772 [startup+860.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73249 0 0 0 85595 250 0 0 25 0 1 0 1855037276 127639552 29835 4294967295 134512640 135094434 3221224432 3221220672 134676999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29835 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 858.46 Current children cumulated vsize (Kb) 126772 [startup+870.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73249 0 0 0 86596 250 0 0 25 0 1 0 1855037276 127639552 29835 4294967295 134512640 135094434 3221224432 3221221200 134677021 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29835 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 868.47 Current children cumulated vsize (Kb) 126772 [startup+880.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73254 0 0 0 87596 250 0 0 25 0 1 0 1855037276 127639552 29840 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29840 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 878.47 Current children cumulated vsize (Kb) 126772 [startup+890.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73254 0 0 0 88596 250 0 0 25 0 1 0 1855037276 127639552 29840 4294967295 134512640 135094434 3221224432 3221220320 134676273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29840 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 888.47 Current children cumulated vsize (Kb) 126772 [startup+900.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73254 0 0 0 89596 250 0 0 25 0 1 0 1855037276 127639552 29840 4294967295 134512640 135094434 3221224432 3221221088 134600246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29840 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 898.47 Current children cumulated vsize (Kb) 126772 [startup+910.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73254 0 0 0 90597 250 0 0 25 0 1 0 1855037276 127639552 29840 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29840 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 908.48 Current children cumulated vsize (Kb) 126772 [startup+920.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73259 0 0 0 91597 250 0 0 25 0 1 0 1855037276 127639552 29845 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29845 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 918.48 Current children cumulated vsize (Kb) 126772 [startup+930.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73293 0 0 0 92597 250 0 0 25 0 1 0 1855037276 127639552 29879 4294967295 134512640 135094434 3221224432 3221221808 134600267 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29879 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 928.48 Current children cumulated vsize (Kb) 126772 [startup+940.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73314 0 0 0 93597 250 0 0 25 0 1 0 1855037276 127639552 29900 4294967295 134512640 135094434 3221224432 3221220144 134677065 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29900 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 938.48 Current children cumulated vsize (Kb) 126772 [startup+950.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73314 0 0 0 94598 250 0 0 25 0 1 0 1855037276 127639552 29900 4294967295 134512640 135094434 3221224432 3221221808 134600232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29900 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 948.49 Current children cumulated vsize (Kb) 126772 [startup+960.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 95598 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221220556 134676988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 958.49 Current children cumulated vsize (Kb) 126772 [startup+970.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 96598 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221219616 134677059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 968.49 Current children cumulated vsize (Kb) 126772 [startup+980.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 97598 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221221808 134677248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 978.49 Current children cumulated vsize (Kb) 126772 [startup+990.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 98599 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221219968 134676273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 988.5 Current children cumulated vsize (Kb) 126772 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 99599 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 998.5 Current children cumulated vsize (Kb) 126772 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 100599 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221221924 134784900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 1008.5 Current children cumulated vsize (Kb) 126772 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 101599 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 1018.5 Current children cumulated vsize (Kb) 126772 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73321 0 0 0 102600 250 0 0 25 0 1 0 1855037276 127639552 29907 4294967295 134512640 135094434 3221224432 3221220288 134676336 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29907 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 1028.51 Current children cumulated vsize (Kb) 126772 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73321 0 0 0 103600 250 0 0 25 0 1 0 1855037276 127639552 29907 4294967295 134512640 135094434 3221224432 3221221632 134600232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29907 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 1038.51 Current children cumulated vsize (Kb) 126772 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73348 0 0 0 104600 250 0 0 25 0 1 0 1855037276 127639552 29934 4294967295 134512640 135094434 3221224432 3221221280 134676471 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29934 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 1048.51 Current children cumulated vsize (Kb) 126772 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73385 0 0 0 105600 250 0 0 25 0 1 0 1855037276 127639552 29971 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 29971 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 1058.51 Current children cumulated vsize (Kb) 126772 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73460 0 0 0 106600 250 0 0 25 0 1 0 1855037276 127639552 30046 4294967295 134512640 135094434 3221224432 3221220108 134676460 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 30046 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 1068.51 Current children cumulated vsize (Kb) 126772 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73549 0 0 0 107601 250 0 0 25 0 1 0 1855037276 127639552 30135 4294967295 134512640 135094434 3221224432 3221221096 134600234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 31162 30135 145 145 0 31017 0 [pid=4592] vsize: 124648 Current children cumulated CPU time (s) 1078.52 Current children cumulated vsize (Kb) 126772 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73595 0 0 0 108599 251 0 0 25 0 1 0 1855037276 140222464 30181 4294967295 134512640 135094434 3221224432 3221220752 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4592/statm): 34234 30181 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1088.51 Current children cumulated vsize (Kb) 139060 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73632 0 0 0 109598 252 0 0 25 0 1 0 1855037276 140222464 30218 4294967295 134512640 135094434 3221224432 3221222336 134677300 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30218 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1098.51 Current children cumulated vsize (Kb) 139060 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73726 0 0 0 110598 252 0 0 25 0 1 0 1855037276 140222464 30312 4294967295 134512640 135094434 3221224432 3221221080 134600694 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30312 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1108.51 Current children cumulated vsize (Kb) 139060 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73801 0 0 0 111598 253 0 0 25 0 1 0 1855037276 140222464 30387 4294967295 134512640 135094434 3221224432 3221220848 134677035 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30387 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1118.52 Current children cumulated vsize (Kb) 139060 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73835 0 0 0 112598 253 0 0 25 0 1 0 1855037276 140222464 30421 4294967295 134512640 135094434 3221224432 3221221256 134677149 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30421 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1128.52 Current children cumulated vsize (Kb) 139060 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74002 0 0 0 113598 253 0 0 25 0 1 0 1855037276 140222464 30588 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30588 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1138.52 Current children cumulated vsize (Kb) 139060 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74065 0 0 0 114597 254 0 0 25 0 1 0 1855037276 140222464 30651 4294967295 134512640 135094434 3221224432 3221220752 134677248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30651 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1148.52 Current children cumulated vsize (Kb) 139060 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74081 0 0 0 115598 254 0 0 25 0 1 0 1855037276 140222464 30667 4294967295 134512640 135094434 3221224432 3221222512 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30667 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1158.53 Current children cumulated vsize (Kb) 139060 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74125 0 0 0 116598 254 0 0 25 0 1 0 1855037276 140222464 30711 4294967295 134512640 135094434 3221224432 3221220648 134676334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30711 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1168.53 Current children cumulated vsize (Kb) 139060 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74141 0 0 0 117598 254 0 0 25 0 1 0 1855037276 140222464 30727 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30727 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1178.53 Current children cumulated vsize (Kb) 139060 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74167 0 0 0 118598 254 0 0 25 0 1 0 1855037276 140222464 30753 4294967295 134512640 135094434 3221224432 3221221072 134518662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30753 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1188.53 Current children cumulated vsize (Kb) 139060 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74223 0 0 0 119599 254 0 0 25 0 1 0 1855037276 140222464 30809 4294967295 134512640 135094434 3221224432 3221221104 134676552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30809 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1198.54 Current children cumulated vsize (Kb) 139060 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74273 0 0 0 120599 254 0 0 25 0 1 0 1855037276 140222464 30859 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30859 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1208.54 Current children cumulated vsize (Kb) 139060 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4592 Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4588/statm): 531 226 485 147 0 384 0 [pid=4588] vsize: 2124 Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74273 0 0 0 120599 254 0 0 25 0 1 0 1855037276 140222464 30859 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4592/statm): 34234 30859 145 145 0 34089 0 [pid=4592] vsize: 136936 Current children cumulated CPU time (s) 1208.54 Current children cumulated vsize (Kb) 139060 Sending SIGTERM to -4588 Sleeping 2 seconds One traced child (pid=4588) ended because it received signal 15 (SIGTERM) One traced child (pid=4592) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.16 CPU time (s): 1208.6 CPU user time (s): 1205.99 CPU system time (s): 2.6076 CPU usage (%): 99.8712 Max. virtual memory (cumulated for all children) (Kb): 139060
ERROR: no interpretation found !