| Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-greenbeb.opb |
| MD5SUM | 32c6aa90779c7f105af21c4a840e4d92 |
| 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 | 10569 |
| 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 | 20687385806400 |
| 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 | 104157 |
| Total number of constraints | 2676 |
| 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 | 2676 |
| Minimum length of a constraint | 8 |
| Maximum length of a constraint | 4848 |
LAUNCH ON wulflinc9 THE 2005-09-20 02:47:42 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3164 boxname=wulflinc9 idbench=820 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 32c6aa90779c7f105af21c4a840e4d92 /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-greenbeb.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-greenbeb.opb IDLAUNCH: 3164 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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 : 2 cpu MHz : 451.242 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: 855464 kB Buffers: 36936 kB Cached: 112776 kB SwapCached: 1044 kB Active: 80400 kB Inactive: 71944 kB HighTotal: 131008 kB HighFree: 22680 kB LowTotal: 903652 kB LowFree: 832784 kB SwapTotal: 2097136 kB SwapFree: 2095568 kB Dirty: 40 kB Writeback: 0 kB Mapped: 5664 kB Slab: 21260 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 03:07:53 (client local time) WITH STATUS 0 IN 1207.8 SECONDS stats: 3164 7 1207.8 0
c Parsing PB file... c Converting 4201 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: #################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################### c -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssss c ---[4255]---> BDD-cost: 17 c ---[4250]---> BDD-cost: 15 c ---[4249]---> BDD-cost: 14 c ---[4248]---> BDD-cost: 18 c ---[4247]---> BDD-cost: 15 c ---[4245]---> BDD-cost: 14 c ---[4244]---> BDD-cost: 16 c ---[4243]---> BDD-cost: 13 c ---[4242]---> BDD-cost: 13 c ---[4238]---> BDD-cost: 13 c ---[4236]---> BDD-cost: 10 c ---[4235]---> BDD-cost: 12 c ---[4234]---> BDD-cost: 8 c ---[4233]---> BDD-cost: 12 c ---[4232]---> BDD-cost: 12 c ---[4231]---> BDD-cost: 9 c ---[4229]---> BDD-cost: 13 c ---[4226]---> BDD-cost: 15 c ---[4223]---> BDD-cost: 9 c ---[4222]---> BDD-cost: 16 c ---[4221]---> BDD-cost: 12 c ---[4220]---> BDD-cost: 13 c ---[4219]---> BDD-cost: 14 c ---[4218]---> BDD-cost: 12 c ---[4217]---> BDD-cost: 15 c ---[4216]---> BDD-cost: 12 c ---[4214]---> BDD-cost: 9 c ---[4212]---> BDD-cost: 12 c ---[4211]---> BDD-cost: 11 c ---[4210]---> BDD-cost: 11 c ---[4209]---> BDD-cost: 12 c ---[4208]---> BDD-cost: 14 c ---[4205]---> BDD-cost: 19 c ---[4204]---> BDD-cost: 12 c ---[4203]---> BDD-cost: 16 c ---[4201]---> BDD-cost: 16 c ---[4200]---> BDD-cost: 10 c ---[4199]---> BDD-cost: 17 c ---[4198]---> BDD-cost: 14 c ---[4197]---> BDD-cost: 14 c ---[4195]---> BDD-cost: 17 c ---[4194]---> BDD-cost: 15 c ---[4193]---> BDD-cost: 16 c ---[4192]---> BDD-cost: 14 c ---[4191]---> BDD-cost: 13 c ---[4190]---> BDD-cost: 7 c ---[4189]---> BDD-cost: 11 c ---[4187]---> BDD-cost: 7 c ---[4186]---> BDD-cost: 13 c ---[4185]---> BDD-cost: 12 c ---[4184]---> BDD-cost: 9 c ---[4182]---> BDD-cost: 13 c ---[4181]---> BDD-cost: 12 c ---[4180]---> BDD-cost: 15 c ---[4179]---> BDD-cost: 17 c ---[4178]---> BDD-cost: 20 c ---[4177]---> BDD-cost: 14 c ---[4176]---> BDD-cost: 13 c ---[4175]---> BDD-cost: 17 c ---[4173]---> BDD-cost: 9 c ---[4172]---> BDD-cost: 17 c ---[4171]---> BDD-cost: 11 c ---[4170]---> BDD-cost: 18 c ---[4169]---> BDD-cost: 15 c ---[4167]---> BDD-cost: 16 c ---[4166]---> BDD-cost: 16 c ---[4165]---> BDD-cost: 15 c ---[4164]---> BDD-cost: 17 c ---[4161]---> BDD-cost: 7 c ---[4160]---> BDD-cost: 11 c ---[4158]---> BDD-cost: 7 c ---[4157]---> BDD-cost: 14 c ---[4156]---> BDD-cost: 13 c ---[4155]---> BDD-cost: 8 c ---[4154]---> BDD-cost: 13 c ---[4153]---> BDD-cost: 14 c ---[4152]---> BDD-cost: 13 c ---[4151]---> BDD-cost: 14 c ---[4150]---> BDD-cost: 13 c ---[4149]---> BDD-cost: 14 c ---[4148]---> BDD-cost: 15 c ---[4147]---> BDD-cost: 19 c ---[4146]---> BDD-cost: 16 c ---[4145]---> BDD-cost: 16 c ---[4143]---> BDD-cost: 15 c ---[4142]---> BDD-cost: 17 c ---[4141]---> BDD-cost: 13 c ---[4140]---> BDD-cost: 16 c ---[4139]---> BDD-cost: 16 c ---[4138]---> BDD-cost: 16 c ---[4137]---> BDD-cost: 15 c ---[4136]---> BDD-cost: 16 c ---[4134]---> BDD-cost: 15 c ---[4133]---> BDD-cost: 16 c ---[4131]---> BDD-cost: 12 c ---[4130]---> BDD-cost: 16 c ---[4129]---> BDD-cost: 15 c ---[4128]---> BDD-cost: 13 c ---[4127]---> BDD-cost: 12 c ---[4126]---> BDD-cost: 11 c ---[4125]---> BDD-cost: 11 c ---[4124]---> BDD-cost: 12 c ---[4123]---> BDD-cost: 11 c ---[4122]---> BDD-cost: 12 c ---[4121]---> BDD-cost: 11 c ---[4120]---> BDD-cost: 12 c ---[4119]---> BDD-cost: 11 c ---[4118]---> BDD-cost: 11 c ---[4117]---> BDD-cost: 12 c ---[4116]---> BDD-cost: 12 c ---[4114]---> BDD-cost: 18 c ---[4111]---> BDD-cost: 14 c ---[4110]---> BDD-cost: 15 c ---[4107]---> BDD-cost: 16 c ---[4106]---> BDD-cost: 13 c ---[4105]---> BDD-cost: 15 c ---[4104]---> BDD-cost: 16 c ---[4103]---> BDD-cost: 17 c ---[4101]---> BDD-cost: 13 c ---[4100]---> BDD-cost: 12 c ---[4098]---> BDD-cost: 10 c ---[4097]---> BDD-cost: 12 c ---[4095]---> BDD-cost: 11 c ---[4093]---> BDD-cost: 12 c ---[4092]---> BDD-cost: 14 c ---[4091]---> BDD-cost: 13 c ---[4088]---> BDD-cost: 12 c ---[4087]---> BDD-cost: 9 c ---[4083]---> BDD-cost: 10 c ---[4078]---> BDD-cost: 12 c ---[4077]---> BDD-cost: 16 c ---[4076]---> BDD-cost: 17 c ---[4075]---> BDD-cost: 14 c ---[4073]---> BDD-cost: 13 c ---[4072]---> BDD-cost: 15 c ---[4071]---> BDD-cost: 16 c ---[4070]---> BDD-cost: 10 c ---[4069]---> BDD-cost: 17 c ---[4067]---> BDD-cost: 16 c ---[4066]---> BDD-cost: 16 c ---[4064]---> BDD-cost: 13 c ---[4063]---> BDD-cost: 18 c ---[4062]---> BDD-cost: 14 c ---[4061]---> BDD-cost: 12 c ---[4060]---> BDD-cost: 12 c ---[4059]---> BDD-cost: 13 c ---[4058]---> BDD-cost: 7 c ---[4056]---> BDD-cost: 13 c ---[4055]---> BDD-cost: 9 c ---[4054]---> BDD-cost: 9 c ---[4053]---> BDD-cost: 13 c ---[4052]---> BDD-cost: 12 c ---[4051]---> BDD-cost: 17 c ---[4050]---> BDD-cost: 14 c ---[4049]---> BDD-cost: 11 c ---[4047]---> BDD-cost: 15 c ---[4046]---> BDD-cost: 19 c ---[4045]---> BDD-cost: 20 c ---[4043]---> BDD-cost: 15 c ---[4042]---> BDD-cost: 16 c ---[4041]---> BDD-cost: 18 c ---[4039]---> BDD-cost: 18 c ---[4038]---> BDD-cost: 13 c ---[4036]---> BDD-cost: 18 c ---[4035]---> BDD-cost: 15 c ---[4033]---> BDD-cost: 15 c ---[4032]---> BDD-cost: 15 c ---[4030]---> BDD-cost: 17 c ---[4029]---> BDD-cost: 14 c ---[4028]---> BDD-cost: 13 c ---[4026]---> BDD-cost: 7 c ---[4025]---> BDD-cost: 15 c ---[4024]---> BDD-cost: 13 c ---[4023]---> BDD-cost: 12 c ---[4022]---> BDD-cost: 12 c ---[4021]---> BDD-cost: 14 c ---[4020]---> BDD-cost: 12 c ---[4019]---> BDD-cost: 19 c ---[4018]---> BDD-cost: 17 c ---[4015]---> BDD-cost: 16 c ---[4014]---> BDD-cost: 18 c ---[4013]---> BDD-cost: 14 c ---[4012]---> BDD-cost: 15 c ---[4011]---> BDD-cost: 15 c ---[4010]---> BDD-cost: 16 c ---[4008]---> BDD-cost: 16 c ---[4006]---> BDD-cost: 15 c ---[4005]---> BDD-cost: 15 c ---[4002]---> BDD-cost: 13 c ---[4001]---> BDD-cost: 17 c ---[3999]---> BDD-cost: 11 c ---[3998]---> BDD-cost: 12 c ---[3997]---> BDD-cost: 10 c ---[3996]---> BDD-cost: 7 c ---[3995]---> BDD-cost: 13 c ---[3994]---> BDD-cost: 11 c ---[3993]---> BDD-cost: 7 c ---[3992]---> BDD-cost: 9 c ---[3991]---> BDD-cost: 12 c ---[3990]---> BDD-cost: 12 c ---[3987]---> BDD-cost: 11 c ---[3985]---> BDD-cost: 13 c ---[3984]---> BDD-cost: 17 c ---[3983]---> BDD-cost: 13 c ---[3981]---> BDD-cost: 11 c ---[3980]---> BDD-cost: 15 c ---[3979]---> BDD-cost: 13 c ---[3978]---> BDD-cost: 11 c ---[3977]---> BDD-cost: 7 c ---[3976]---> BDD-cost: 8 c ---[3975]---> BDD-cost: 13 c ---[3974]---> BDD-cost: 14 c ---[3973]---> BDD-cost: 11 c ---[3970]---> BDD-cost: 10 c ---[3969]---> BDD-cost: 8 c ---[3967]---> BDD-cost: 13 c ---[3965]---> BDD-cost: 16 c ---[3963]---> Sorter-cost: 1986 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3961]---> Adder-cost: 561 maxlim: 185088 bits: 19/18 c ---[3959]---> Adder-cost: 902 maxlim: 1253375 bits: 22/21 c ---[3957]---> Adder-cost: 561 maxlim: 144640 bits: 19/18 c ---[3955]---> Sorter-cost: 3380 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3953]---> Adder-cost: 529 maxlim: 83200 bits: 18/17 c ---[3951]---> Sorter-cost: 3060 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3949]---> Sorter-cost: 2120 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3947]---> Sorter-cost: 3164 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3945]---> Adder-cost: 300 maxlim: 70784 bits: 18/17 c ---[3943]---> BDD-cost: 170 c ---[3941]---> Sorter-cost: 3164 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3939]---> Sorter-cost: 350 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3937]---> BDD-cost: 65 c ---[3935]---> Sorter-cost: 3164 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3933]---> Adder-cost: 593 maxlim: 438656 bits: 20/19 c ---[3931]---> Adder-cost: 593 maxlim: 316416 bits: 20/19 c ---[3929]---> BDD-cost: 58 c ---[3927]---> Sorter-cost: 1562 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3925]---> Adder-cost: 561 maxlim: 176000 bits: 19/18 c ---[3923]---> Sorter-cost: 1020 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3921]---> Adder-cost: 561 maxlim: 220032 bits: 19/18 c ---[3917]---> Sorter-cost: 3009 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3915]---> Adder-cost: 318 maxlim: 164992 bits: 19/18 c ---[3913]---> Sorter-cost: 2948 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3911]---> Sorter-cost: 3379 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3909]---> Sorter-cost: 473 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3907]---> Adder-cost: 375 maxlim: 60160 bits: 17/16 c ---[3905]---> BDD-cost: 75 c ---[3903]---> Adder-cost: 300 maxlim: 125440 bits: 18/17 c ---[3901]---> Sorter-cost: 1087 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3899]---> Sorter-cost: 1388 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3897]---> Sorter-cost: 2121 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3895]---> BDD-cost: 75 c ---[3893]---> Sorter-cost: 1843 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3891]---> Sorter-cost: 1844 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3889]---> BDD-cost: 166 c ---[3887]---> BDD-cost: 58 c ---[3885]---> BDD-cost: 58 c ---[3883]---> Adder-cost: 293 maxlim: 27776 bits: 16/15 c ---[3881]---> BDD-cost: 24 c ---[3879]---> BDD-cost: 50 c ---[3869]---> BDD-cost: 24 c ---[3867]---> BDD-cost: 98 c ---[3865]---> BDD-cost: 50 c ---[3863]---> BDD-cost: 20 c ---[3861]---> BDD-cost: 20 c ---[3859]---> BDD-cost: 20 c ---[3857]---> BDD-cost: 20 c ---[3847]---> BDD-cost: 24 c ---[3845]---> BDD-cost: 98 c ---[3843]---> BDD-cost: 50 c ---[3835]---> Sorter-cost: 1815 Base: 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 2 c ---[3833]---> Sorter-cost: 4725 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 7 c ---[3831]---> Sorter-cost: 4718 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3829]---> Sorter-cost: 4748 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3827]---> 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 ---[3823]---> 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 ---[3815]---> Sorter-cost: 2782 Base: 2 2 2 2 5 5 5 2 2 2 2 7 2 2 2 c ---[3813]---> Sorter-cost: 4287 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3811]---> Sorter-cost: 4317 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3809]---> 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 ---[3807]---> 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 ---[3803]---> Sorter-cost: 3658 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 c ---[3795]---> Sorter-cost: 1467 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 2 c ---[3793]---> Sorter-cost: 2951 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[3791]---> Sorter-cost: 2981 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[3789]---> Sorter-cost: 2935 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 c ---[3787]---> Sorter-cost: 2935 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 c ---[3783]---> Sorter-cost: 1762 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 c ---[3775]---> BDD-cost: 507 c ---[3773]---> Sorter-cost: 4615 Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 c ---[3771]---> 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 ---[3769]---> 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 ---[3767]---> 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 ---[3763]---> Sorter-cost: 3580 Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 5 2 7 2 2 c ---[3755]---> Sorter-cost: 2782 Base: 2 2 2 2 5 5 5 2 2 2 2 7 2 2 2 c ---[3753]---> Sorter-cost: 4018 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3751]---> Sorter-cost: 4048 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3749]---> Sorter-cost: 4000 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3747]---> Sorter-cost: 4000 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3743]---> Sorter-cost: 3370 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 7 2 2 c ---[3733]---> BDD-cost: 53 c ---[3731]---> BDD-cost: 53 c ---[3727]---> Sorter-cost: 1882 Base: 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 2 2 c ---[3725]---> Sorter-cost: 3212 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[3723]---> Sorter-cost: 3242 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[3721]---> 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 ---[3719]---> 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 ---[3715]---> Sorter-cost: 2296 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 7 2 2 c ---[3707]---> BDD-cost: 330 c ---[3705]---> Sorter-cost: 3910 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 c ---[3703]---> 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 ---[3701]---> 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 ---[3699]---> 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 ---[3695]---> 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 ---[3687]---> BDD-cost: 330 c ---[3685]---> Sorter-cost: 4355 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 c ---[3683]---> 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 ---[3681]---> 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 ---[3679]---> 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 ---[3675]---> 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 ---[3667]---> BDD-cost: 342 c ---[3665]---> Sorter-cost: 4200 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2 c ---[3663]---> Sorter-cost: 4220 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2 c ---[3661]---> Sorter-cost: 4220 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2 c ---[3659]---> Sorter-cost: 4220 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2 c ---[3655]---> Sorter-cost: 2940 Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3647]---> BDD-cost: 330 c ---[3645]---> Sorter-cost: 3476 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3643]---> 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 ---[3641]---> 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 ---[3639]---> 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 ---[3635]---> 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 ---[3627]---> BDD-cost: 330 c ---[3625]---> Sorter-cost: 3946 Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3623]---> Sorter-cost: 3966 Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3621]---> Sorter-cost: 3966 Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3619]---> Sorter-cost: 3966 Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3615]---> Sorter-cost: 2863 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3607]---> Sorter-cost: 2717 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[3605]---> BDD-cost: 129 c ---[3601]---> Sorter-cost: 2385 Base: 2 2 2 2 2 2 2 2 3 3 3 2 2 2 2 2 2 2 c ---[3599]---> Sorter-cost: 4206 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3597]---> Sorter-cost: 4226 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3595]---> Sorter-cost: 4226 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3593]---> Sorter-cost: 4226 Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2 c ---[3589]---> Sorter-cost: 2999 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[3581]---> 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 ---[3579]---> Adder-cost: 548 maxlim: 163444290 bits: 29/28 c ---[3577]---> Adder-cost: 668 maxlim: 1961358914 bits: 32/31 c ---[3575]---> Adder-cost: 616 maxlim: 653784642 bits: 31/30 c ---[3573]---> Adder-cost: 468 maxlim: 1307573025 bits: 32/31 c ---[3571]---> Sorter-cost: 4211 Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 3 2 3 11 2 2 2 c ---[3569]---> BDD-cost: 447 c ---[3567]---> Adder-cost: 460 maxlim: 46923418 bits: 27/26 c ---[3565]---> Adder-cost: 544 maxlim: 375389850 bits: 30/29 c ---[3563]---> Adder-cost: 488 maxlim: 70385306 bits: 28/27 c ---[3561]---> BDD-cost: 254 c ---[3559]---> Sorter-cost: 1815 Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[3557]---> Sorter-cost: 1999 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[3555]---> Sorter-cost: 1999 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 c ---[3553]---> Adder-cost: 390 maxlim: 1301281575 bits: 32/31 c ---[3551]---> Adder-cost: 456 maxlim: 162657870 bits: 29/28 c ---[3549]---> Adder-cost: 560 maxlim: 2602563150 bits: 32/32 c ---[3547]---> Adder-cost: 512 maxlim: 650638926 bits: 31/30 c ---[3545]---> Adder-cost: 390 maxlim: 1301281575 bits: 32/31 c ---[3543]---> Adder-cost: 370 maxlim: 650640167 bits: 31/30 c ---[3541]---> BDD-cost: 450 c ---[3539]---> Adder-cost: 334 maxlim: 40370022 bits: 27/26 c ---[3537]---> Adder-cost: 358 maxlim: 161480550 bits: 28/28 c ---[3535]---> Adder-cost: 358 maxlim: 161480550 bits: 28/28 c ---[3533]---> Adder-cost: 330 maxlim: 162659111 bits: 29/28 c ---[3531]---> 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 ---[3529]---> BDD-cost: 181 c ---[3527]---> 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 ---[3525]---> BDD-cost: 615 c ---[3523]---> BDD-cost: 340 c ---[3519]---> BDD-cost: 154 c ---[3517]---> Sorter-cost: 2847 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[3515]---> 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 ---[3513]---> 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 ---[3509]---> 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 ---[3507]---> BDD-cost: 154 c ---[3505]---> 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 ---[3503]---> BDD-cost: 517 c ---[3501]---> 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 ---[3499]---> 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 ---[3497]---> BDD-cost: 288 c ---[3495]---> 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 ---[3493]---> 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 ---[3491]---> BDD-cost: 278 c ---[3489]---> 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 ---[3487]---> Sorter-cost: 3638 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 ---[3485]---> Sorter-cost: 4022 Base: 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 ---[3483]---> BDD-cost: 463 c ---[3481]---> 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 ---[3479]---> 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 ---[3477]---> Sorter-cost: 3598 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 2 c ---[3475]---> 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 ---[3473]---> Sorter-cost: 4498 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 2 c ---[3471]---> 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 ---[3469]---> Sorter-cost: 2006 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 c ---[3467]---> Sorter-cost: 1814 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 c ---[3465]---> Sorter-cost: 1604 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 c ---[3457]---> 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 ---[3455]---> Adder-cost: 392 maxlim: 15007286 bits: 25/24 c ---[3453]---> Adder-cost: 510 maxlim: 480247350 bits: 30/29 c ---[3451]---> Adder-cost: 470 maxlim: 120061494 bits: 28/27 c ---[3449]---> 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 ---[3447]---> 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 ---[3445]---> Sorter-cost: 2793 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 3 3 2 2 c ---[3443]---> 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 ---[3441]---> Sorter-cost: 1368 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 c ---[3439]---> Sorter-cost: 1368 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 c ---[3437]---> Sorter-cost: 1368 Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 c ---[3435]---> 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 ---[3433]---> BDD-cost: 173 c ---[3431]---> Adder-cost: 406 maxlim: 2778196813 bits: 33/32 c ---[3429]---> BDD-cost: 607 c ---[3427]---> BDD-cost: 333 c ---[3423]---> BDD-cost: 172 c ---[3419]---> 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 ---[3417]---> BDD-cost: 286 c ---[3415]---> Adder-cost: 490 maxlim: 1601174025 bits: 32/31 c ---[3413]---> Sorter-cost: 4380 Base: 2 2 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 c ---[3411]---> Adder-cost: 490 maxlim: 1601174025 bits: 32/31 c ---[3409]---> Adder-cost: 490 maxlim: 1601174025 bits: 32/31 c ---[3407]---> BDD-cost: 421 c ---[3405]---> 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 ---[3403]---> 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 ---[3401]---> BDD-cost: 451 c ---[3399]---> 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 ---[3397]---> Sorter-cost: 2893 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 3 c ---[3395]---> 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 ---[3393]---> 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 ---[3391]---> 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 ---[3389]---> 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 ---[3387]---> Adder-cost: 590 maxlim: 10524019642 bits: 34/34 c ---[3385]---> BDD-cost: 540 c ---[3383]---> 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 ---[3381]---> BDD-cost: 612 c ---[3379]---> BDD-cost: 131 c ---[3377]---> Sorter-cost: 2923 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 3 c ---[3375]---> 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 ---[3373]---> Sorter-cost: 2962 Base: 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 ---[3371]---> BDD-cost: 105 c ---[3363]---> Adder-cost: 384 maxlim: 7049569725 bits: 34/33 c ---[3361]---> Adder-cost: 634 maxlim: 14099139450 bits: 35/34 c ---[3359]---> BDD-cost: 540 c ---[3357]---> Adder-cost: 384 maxlim: 7049569725 bits: 34/33 c ---[3355]---> Adder-cost: 364 maxlim: 3524781501 bits: 33/32 c ---[3353]---> BDD-cost: 131 c ---[3351]---> Sorter-cost: 5168 Base: 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 c ---[3349]---> 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 ---[3347]---> 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 ---[3345]---> BDD-cost: 340 c ---[3343]---> 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 ---[3341]---> 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 ---[3339]---> BDD-cost: 510 c ---[3337]---> Sorter-cost: 3176 Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 c ---[3335]---> BDD-cost: 89 c ---[3333]---> BDD-cost: 373 c ---[3331]---> Sorter-cost: 3678 Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 c ---[3329]---> 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 ---[3327]---> 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 ---[3323]---> Adder-cost: 462 maxlim: 122158638 bits: 28/27 c ---[3321]---> Adder-cost: 514 maxlim: 488635950 bits: 30/29 c ---[3319]---> Adder-cost: 514 maxlim: 488635950 bits: 30/29 c ---[3317]---> Sorter-cost: 2118 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[3315]---> Sorter-cost: 2118 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[3313]---> Sorter-cost: 2118 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 c ---[3311]---> BDD-cost: 65 c ---[3309]---> BDD-cost: 75 c ---[3307]---> Sorter-cost: 2001 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 c ---[3305]---> 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 ---[3303]---> Sorter-cost: 2133 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 c ---[3301]---> Sorter-cost: 2223 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 7 2 2 c ---[3299]---> 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 ---[3297]---> Sorter-cost: 2357 Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 7 2 2 c ---[3295]---> Sorter-cost: 868 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3293]---> Sorter-cost: 1000 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3291]---> Sorter-cost: 1000 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3289]---> 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 ---[3287]---> 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 ---[3285]---> 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 ---[3283]---> 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 ---[3281]---> 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 ---[3279]---> Sorter-cost: 3004 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2 c ---[3277]---> BDD-cost: 595 c ---[3275]---> BDD-cost: 530 c ---[3273]---> 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 ---[3271]---> 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 ---[3269]---> 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 ---[3267]---> 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 ---[3265]---> 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 ---[3263]---> 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 ---[3261]---> Sorter-cost: 1134 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[3259]---> Sorter-cost: 1191 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[3257]---> 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 ---[3255]---> 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 ---[3253]---> 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 ---[3251]---> 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 ---[3249]---> 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 ---[3247]---> 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 ---[3245]---> BDD-cost: 581 c ---[3243]---> BDD-cost: 529 c ---[3241]---> 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 ---[3239]---> 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 ---[3237]---> 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 ---[3235]---> 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 ---[3233]---> 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 ---[3231]---> 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 ---[3229]---> Sorter-cost: 1778 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3 c ---[3227]---> Sorter-cost: 1802 Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 c ---[3225]---> 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 ---[3223]---> 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 ---[3221]---> 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 ---[3219]---> 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 ---[3217]---> 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 ---[3215]---> Sorter-cost: 2427 Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3213]---> Sorter-cost: 2039 Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3211]---> Sorter-cost: 1871 Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[3209]---> 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 ---[3207]---> 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 ---[3205]---> 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 ---[3203]---> 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 ---[3201]---> 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 ---[3199]---> 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 ---[3197]---> 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 ---[3195]---> 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 ---[3193]---> 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 ---[3191]---> 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 ---[3189]---> 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 ---[3187]---> 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 ---[3185]---> 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 ---[3183]---> 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 ---[3181]---> 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 ---[3179]---> Sorter-cost: 2776 Base: 2 2 2 2 2 2 5 2 2 5 2 2 2 2 2 2 2 2 2 c ---[3177]---> 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 ---[3175]---> 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 ---[3173]---> 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 ---[3171]---> 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 ---[3169]---> 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 ---[3167]---> 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 ---[3165]---> 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 ---[3163]---> 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 ---[3161]---> 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 ---[3159]---> 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 ---[3157]---> 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 ---[3155]---> 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 ---[3153]---> 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 ---[3151]---> 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 ---[3149]---> 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 ---[3147]---> 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 ---[3145]---> 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 ---[3143]---> 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 ---[3141]---> 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 ---[3139]---> 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 ---[3137]---> 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 ---[3135]---> 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 ---[3133]---> 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 ---[3131]---> 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 ---[3129]---> 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 ---[3127]---> 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 ---[3125]---> 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 ---[3123]---> 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 ---[3121]---> 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 ---[3119]---> 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 ---[3117]---> Sorter-cost: 1370 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 c ---[3115]---> 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 ---[3113]---> 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 ---[3111]---> 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 ---[3109]---> 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 ---[3107]---> 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 ---[3105]---> 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 ---[3103]---> 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 ---[3101]---> 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 ---[3099]---> 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 ---[3097]---> 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 ---[3095]---> 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 ---[3093]---> 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 ---[3091]---> 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 ---[3089]---> 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 ---[3087]---> 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 ---[3085]---> 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 ---[3083]---> 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 ---[3081]---> Adder-cost: 994 maxlim: 13873748826 bits: 35/34 c ---[3079]---> Adder-cost: 1010 maxlim: 14466784090 bits: 35/34 c ---[3077]---> Adder-cost: 1010 maxlim: 14466784090 bits: 35/34 c ---[3075]---> Adder-cost: 1568 maxlim: 93995325 bits: 28/27 c ---[3073]---> Adder-cost: 2013 maxlim: 485866136 bits: 30/29 c ---[3071]---> Adder-cost: 1752 maxlim: 328064955 bits: 30/29 c ---[3069]---> 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 ---[3067]---> 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 ---[3065]---> Adder-cost: 544 maxlim: 761265450 bits: 31/30 c ---[3063]---> 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 ---[3061]---> Adder-cost: 544 maxlim: 761265450 bits: 31/30 c ---[3059]---> Adder-cost: 544 maxlim: 761265450 bits: 31/30 c ---[3057]---> Adder-cost: 544 maxlim: 761265450 bits: 31/30 c ---[3055]---> Adder-cost: 346 maxlim: 80740198 bits: 28/27 c ---[3053]---> 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 ---[3051]---> Adder-cost: 364 maxlim: 161480550 bits: 29/28 c ---[3049]---> Adder-cost: 364 maxlim: 161480550 bits: 29/28 c ---[3047]---> Adder-cost: 364 maxlim: 161480550 bits: 29/28 c ---[3045]---> 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 ---[3043]---> Adder-cost: 307 maxlim: 122158871 bits: 28/27 c ---[3041]---> Adder-cost: 325 maxlim: 244317975 bits: 29/28 c ---[3039]---> Adder-cost: 307 maxlim: 122158871 bits: 28/27 c ---[3037]---> Adder-cost: 325 maxlim: 244317975 bits: 29/28 c ---[3035]---> Adder-cost: 325 maxlim: 244317975 bits: 29/28 c ---[3033]---> Adder-cost: 325 maxlim: 244317975 bits: 29/28 c ---[3031]---> Sorter-cost: 2623 Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 c ---[3029]---> 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 ---[3027]---> 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 ---[3025]---> 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 ---[3023]---> Sorter-cost: 3342 Base: 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 ---[3013]---> BDD-cost: 212 c ---[3011]---> BDD-cost: 692 c ---[3009]---> BDD-cost: 389 c ---[3007]---> BDD-cost: 27 c ---[3005]---> BDD-cost: 27 c ---[2995]---> BDD-cost: 27 c ---[2993]---> BDD-cost: 27 c ---[2983]---> 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 ---[2981]---> 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 ---[2979]---> 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 ---[2977]---> Sorter-cost: 2829 Base: 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 c ---[2975]---> 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 ---[2973]---> 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 ---[2971]---> 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 ---[2969]---> 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 ---[2967]---> 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 ---[2965]---> 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 ---[2963]---> Sorter-cost: 4197 Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2961]---> 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 ---[2959]---> 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 ---[2957]---> 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 ---[2955]---> 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 ---[2953]---> Sorter-cost: 2691 Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2951]---> Sorter-cost: 3868 Base: 2 2 5 5 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2949]---> Sorter-cost: 6234 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 ---[2947]---> 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 ---[2945]---> 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 ---[2943]---> 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 ---[2941]---> BDD-cost: 212 c ---[2939]---> BDD-cost: 389 c ---[2915]---> BDD-cost: 406 c ---[2913]---> BDD-cost: 692 c ---[2911]---> BDD-cost: 389 c ---[2901]---> Sorter-cost: 2790 Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2899]---> Sorter-cost: 3420 Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2897]---> Sorter-cost: 2677 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[2895]---> Sorter-cost: 3143 Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2893]---> Sorter-cost: 3934 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2891]---> Sorter-cost: 2986 Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2889]---> 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 ---[2887]---> BDD-cost: 370 c ---[2885]---> 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 ---[2883]---> Sorter-cost: 3684 Base: 2 2 2 2 5 5 5 2 2 2 2 2 5 2 2 2 2 2 2 c ---[2881]---> Sorter-cost: 3437 Base: 2 2 2 2 5 5 5 2 2 2 2 5 2 2 2 2 2 2 c ---[2877]---> BDD-cost: 133 c ---[2873]---> Sorter-cost: 3117 Base: 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2871]---> Sorter-cost: 1880 Base: 2 5 5 5 2 2 2 2 2 2 2 c ---[2869]---> Sorter-cost: 2828 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 c ---[2867]---> Sorter-cost: 2566 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 c ---[2865]---> Sorter-cost: 1207 Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 c ---[2863]---> Sorter-cost: 2247 Base: 2 5 5 5 2 2 2 2 2 2 2 2 2 c ---[2861]---> Sorter-cost: 2075 Base: 2 5 5 5 2 2 2 2 2 2 2 c ---[2859]---> Sorter-cost: 1880 Base: 2 5 5 5 2 2 2 2 2 2 2 c ---[2857]---> Sorter-cost: 2828 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 c ---[2855]---> Sorter-cost: 2566 Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 c ---[2853]---> Sorter-cost: 2806 Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 c ---[2851]---> 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 ---[2849]---> BDD-cost: 171 c ---[2847]---> 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 ---[2845]---> Sorter-cost: 3538 Base: 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2 c ---[2843]---> 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 ---[2841]---> Sorter-cost: 3129 Base: 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2 c ---[2839]---> Sorter-cost: 3587 Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 c ---[2837]---> BDD-cost: 171 c ---[2835]---> 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 ---[2833]---> Sorter-cost: 3538 Base: 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2 c ---[2831]---> 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 ---[2829]---> 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 ---[2827]---> Sorter-cost: 2034 Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 5 2 c ---[2825]---> Adder-cost: 280 maxlim: 17301471 bits: 26/25 c ---[2823]---> Sorter-cost: 2727 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 5 2 c ---[2821]---> Adder-cost: 236 maxlim: 4325343 bits: 24/23 c ---[2817]---> BDD-cost: 219 c ---[2813]---> Sorter-cost: 5746 Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2811]---> Adder-cost: 454 maxlim: 237502011 bits: 29/28 c ---[2809]---> BDD-cost: 205 c ---[2807]---> BDD-cost: 426 c ---[2805]---> BDD-cost: 385 c ---[2803]---> Sorter-cost: 4159 Base: 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2801]---> Sorter-cost: 5594 Base: 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2799]---> Sorter-cost: 3844 Base: 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2797]---> BDD-cost: 394 c ---[2795]---> Adder-cost: 482 maxlim: 475004475 bits: 30/29 c ---[2793]---> BDD-cost: 205 c ---[2791]---> Adder-cost: 482 maxlim: 475004475 bits: 30/29 c ---[2789]---> Sorter-cost: 4552 Base: 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2787]---> Sorter-cost: 5683 Base: 2 2 2 5 5 5 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2 c ---[2785]---> Sorter-cost: 4751 Base: 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2783]---> Sorter-cost: 4996 Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2781]---> Sorter-cost: 4632 Base: 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[2779]---> BDD-cost: 20
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/32058/stat): 32058 (minisat+_script) R 32057 32058 30740 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796826084 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/32058/statm): 174 3 169 147 0 27 0 [pid=32058] 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=32059 New process pid=32060 New process pid=32061 execve syscall for /bin/sed executable One traced child (pid=32060) 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=32061) exited with status: 0 One traced child (pid=32059) exited with status: 0 New process pid=32062 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-greenbeb.opb [startup+10.0035 s] Raw data (loadavg): 0.48 0.12 0.04 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 13879 0 0 0 835 76 0 0 25 0 1 0 1796826088 60014592 13576 4294967295 134512640 135094434 3221224432 3221223248 134580034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 14652 13576 145 145 0 14507 0 [pid=32062] vsize: 58608 Current children cumulated CPU time (s) 9.12 Current children cumulated vsize (Kb) 60732 [startup+20.0052 s] Raw data (loadavg): 0.56 0.15 0.05 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 14108 0 0 0 1834 77 0 0 25 0 1 0 1796826088 59166720 13194 4294967295 134512640 135094434 3221224432 3221220584 134781717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 14445 13194 145 145 0 14300 0 [pid=32062] vsize: 57780 Current children cumulated CPU time (s) 19.12 Current children cumulated vsize (Kb) 59904 [startup+30.0059 s] Raw data (loadavg): 0.63 0.18 0.06 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 14225 0 0 0 2833 78 0 0 25 0 1 0 1796826088 59166720 13311 4294967295 134512640 135094434 3221224432 3221220848 134676376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 14445 13311 145 145 0 14300 0 [pid=32062] vsize: 57780 Current children cumulated CPU time (s) 29.12 Current children cumulated vsize (Kb) 59904 [startup+40.0067 s] Raw data (loadavg): 0.68 0.20 0.07 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 14374 0 0 0 3833 79 0 0 25 0 1 0 1796826088 60821504 13418 4294967295 134512640 135094434 3221224432 3221219792 134676321 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 14849 13418 145 145 0 14704 0 [pid=32062] vsize: 59396 Current children cumulated CPU time (s) 39.13 Current children cumulated vsize (Kb) 61520 [startup+50.0084 s] Raw data (loadavg): 0.73 0.23 0.08 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 17483 0 0 0 4816 88 0 0 25 0 1 0 1796826088 65880064 14762 4294967295 134512640 135094434 3221224432 3221220048 134677310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 16084 14762 145 145 0 15939 0 [pid=32062] vsize: 64336 Current children cumulated CPU time (s) 49.05 Current children cumulated vsize (Kb) 66460 [startup+60.0091 s] Raw data (loadavg): 0.77 0.26 0.09 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 17547 0 0 0 5816 89 0 0 25 0 1 0 1796826088 65880064 14826 4294967295 134512640 135094434 3221224432 3221221532 134676331 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 16084 14826 145 145 0 15939 0 [pid=32062] vsize: 64336 Current children cumulated CPU time (s) 59.06 Current children cumulated vsize (Kb) 66460 [startup+70.0098 s] Raw data (loadavg): 0.81 0.28 0.10 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 17620 0 0 0 6816 89 0 0 25 0 1 0 1796826088 65880064 14899 4294967295 134512640 135094434 3221224432 3221219244 134677081 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 16084 14899 145 145 0 15939 0 [pid=32062] vsize: 64336 Current children cumulated CPU time (s) 69.06 Current children cumulated vsize (Kb) 66460 [startup+80.0106 s] Raw data (loadavg): 0.84 0.30 0.11 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 17668 0 0 0 7815 90 0 0 25 0 1 0 1796826088 65880064 14947 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 16084 14947 145 145 0 15939 0 [pid=32062] vsize: 64336 Current children cumulated CPU time (s) 79.06 Current children cumulated vsize (Kb) 66460 [startup+90.0103 s] Raw data (loadavg): 0.86 0.33 0.12 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 17753 0 0 0 8815 91 0 0 25 0 1 0 1796826088 69025792 15032 4294967295 134512640 135094434 3221224432 3221219440 134676321 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 16852 15032 145 145 0 16707 0 [pid=32062] vsize: 67408 Current children cumulated CPU time (s) 89.07 Current children cumulated vsize (Kb) 69532 [startup+100.011 s] Raw data (loadavg): 0.88 0.35 0.12 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 17848 0 0 0 9815 91 0 0 25 0 1 0 1796826088 69025792 15127 4294967295 134512640 135094434 3221224432 3221220672 134677059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 16852 15127 145 145 0 16707 0 [pid=32062] vsize: 67408 Current children cumulated CPU time (s) 99.07 Current children cumulated vsize (Kb) 69532 [startup+110.012 s] Raw data (loadavg): 0.90 0.37 0.13 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 18338 0 0 0 10813 92 0 0 25 0 1 0 1796826088 69578752 15286 4294967295 134512640 135094434 3221224432 3221221632 134676510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 16987 15286 145 145 0 16842 0 [pid=32062] vsize: 67948 Current children cumulated CPU time (s) 109.06 Current children cumulated vsize (Kb) 70072 [startup+120.012 s] Raw data (loadavg): 0.91 0.39 0.14 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 18687 0 0 0 11812 93 0 0 25 0 1 0 1796826088 69615616 15313 4294967295 134512640 135094434 3221224432 3221220496 134677049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 16996 15313 145 145 0 16851 0 [pid=32062] vsize: 67984 Current children cumulated CPU time (s) 119.06 Current children cumulated vsize (Kb) 70108 [startup+130.013 s] Raw data (loadavg): 0.93 0.41 0.15 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 18687 0 0 0 12812 93 0 0 25 0 1 0 1796826088 69615616 15313 4294967295 134512640 135094434 3221224432 3221221984 134600144 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 16996 15313 145 145 0 16851 0 [pid=32062] vsize: 67984 Current children cumulated CPU time (s) 129.06 Current children cumulated vsize (Kb) 70108 [startup+140.013 s] Raw data (loadavg): 0.94 0.43 0.16 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 19028 0 0 0 13811 94 0 0 25 0 1 0 1796826088 69664768 15332 4294967295 134512640 135094434 3221224432 3221221280 134600291 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 17008 15332 145 145 0 16863 0 [pid=32062] vsize: 68032 Current children cumulated CPU time (s) 139.06 Current children cumulated vsize (Kb) 70156 [startup+150.014 s] Raw data (loadavg): 0.95 0.45 0.17 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 19154 0 0 0 14811 94 0 0 25 0 1 0 1796826088 69664768 15333 4294967295 134512640 135094434 3221224432 3221220928 134677327 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 17008 15333 145 145 0 16863 0 [pid=32062] vsize: 68032 Current children cumulated CPU time (s) 149.06 Current children cumulated vsize (Kb) 70156 [startup+160.014 s] Raw data (loadavg): 0.95 0.46 0.18 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 19404 0 0 0 15810 95 0 0 25 0 1 0 1796826088 69664768 15333 4294967295 134512640 135094434 3221224432 3221220032 134600246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 17008 15333 145 145 0 16863 0 [pid=32062] vsize: 68032 Current children cumulated CPU time (s) 159.06 Current children cumulated vsize (Kb) 70156 [startup+170.015 s] Raw data (loadavg): 0.96 0.48 0.19 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 19956 0 0 0 16808 97 0 0 25 0 1 0 1796826088 69644288 15364 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 17003 15364 145 145 0 16858 0 [pid=32062] vsize: 68012 Current children cumulated CPU time (s) 169.06 Current children cumulated vsize (Kb) 70136 [startup+180.016 s] Raw data (loadavg): 0.97 0.50 0.19 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 20871 0 0 0 17805 99 0 0 25 0 1 0 1796826088 69656576 15382 4294967295 134512640 135094434 3221224432 3221221024 134676317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 17006 15382 145 145 0 16861 0 [pid=32062] vsize: 68024 Current children cumulated CPU time (s) 179.05 Current children cumulated vsize (Kb) 70148 [startup+190.017 s] Raw data (loadavg): 0.97 0.51 0.20 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 23606 0 0 0 18789 107 0 0 25 0 1 0 1796826088 69603328 15377 4294967295 134512640 135094434 3221224432 3221220224 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 16993 15377 145 145 0 16848 0 [pid=32062] vsize: 67972 Current children cumulated CPU time (s) 188.97 Current children cumulated vsize (Kb) 70096 [startup+200.017 s] Raw data (loadavg): 0.98 0.53 0.21 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 26305 0 0 0 19779 114 0 0 25 0 1 0 1796826088 74571776 16600 4294967295 134512640 135094434 3221224432 3221220552 134676241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 18206 16600 145 145 0 18061 0 [pid=32062] vsize: 72824 Current children cumulated CPU time (s) 198.94 Current children cumulated vsize (Kb) 74948 [startup+210.018 s] Raw data (loadavg): 0.98 0.54 0.22 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 28081 0 0 0 20775 119 0 0 25 0 1 0 1796826088 74571776 16642 4294967295 134512640 135094434 3221224432 3221219232 134676341 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 18206 16642 145 145 0 18061 0 [pid=32062] vsize: 72824 Current children cumulated CPU time (s) 208.95 Current children cumulated vsize (Kb) 74948 [startup+220.019 s] Raw data (loadavg): 0.98 0.56 0.22 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 28081 0 0 0 21775 119 0 0 25 0 1 0 1796826088 74571776 16642 4294967295 134512640 135094434 3221224432 3221220224 134676595 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 18206 16642 145 145 0 18061 0 [pid=32062] vsize: 72824 Current children cumulated CPU time (s) 218.95 Current children cumulated vsize (Kb) 74948 [startup+230.02 s] Raw data (loadavg): 0.98 0.57 0.23 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 28935 0 0 0 22772 121 0 0 25 0 1 0 1796826088 74571776 16669 4294967295 134512640 135094434 3221224432 3221220016 134781142 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 18206 16669 145 145 0 18061 0 [pid=32062] vsize: 72824 Current children cumulated CPU time (s) 228.94 Current children cumulated vsize (Kb) 74948 [startup+240.019 s] Raw data (loadavg): 0.99 0.59 0.24 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 29536 0 0 0 23771 122 0 0 25 0 1 0 1796826088 74571776 16691 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 18206 16691 145 145 0 18061 0 [pid=32062] vsize: 72824 Current children cumulated CPU time (s) 238.94 Current children cumulated vsize (Kb) 74948 [startup+250.02 s] Raw data (loadavg): 0.99 0.60 0.25 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 29809 0 0 0 24770 123 0 0 25 0 1 0 1796826088 74571776 16715 4294967295 134512640 135094434 3221224432 3221221552 134677042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 18206 16715 145 145 0 18061 0 [pid=32062] vsize: 72824 Current children cumulated CPU time (s) 248.94 Current children cumulated vsize (Kb) 74948 [startup+260.021 s] Raw data (loadavg): 0.99 0.61 0.26 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 30177 0 0 0 25769 124 0 0 25 0 1 0 1796826088 74571776 16751 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 18206 16751 145 145 0 18061 0 [pid=32062] vsize: 72824 Current children cumulated CPU time (s) 258.94 Current children cumulated vsize (Kb) 74948 [startup+270.021 s] Raw data (loadavg): 0.99 0.62 0.26 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 30277 0 0 0 26769 124 0 0 25 0 1 0 1796826088 74571776 16851 4294967295 134512640 135094434 3221224432 3221221344 134677091 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 18206 16851 145 145 0 18061 0 [pid=32062] vsize: 72824 Current children cumulated CPU time (s) 268.94 Current children cumulated vsize (Kb) 74948 [startup+280.022 s] Raw data (loadavg): 0.99 0.64 0.27 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 32518 0 0 0 27756 132 0 0 25 0 1 0 1796826088 78503936 17855 4294967295 134512640 135094434 3221224432 3221220048 134677313 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19166 17855 145 145 0 19021 0 [pid=32062] vsize: 76664 Current children cumulated CPU time (s) 278.89 Current children cumulated vsize (Kb) 78788 [startup+290.023 s] Raw data (loadavg): 0.99 0.65 0.28 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 32864 0 0 0 28755 133 0 0 25 0 1 0 1796826088 78503936 17871 4294967295 134512640 135094434 3221224432 3221221456 134600002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19166 17871 145 145 0 19021 0 [pid=32062] vsize: 76664 Current children cumulated CPU time (s) 288.89 Current children cumulated vsize (Kb) 78788 [startup+300.024 s] Raw data (loadavg): 0.99 0.66 0.29 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 33536 0 0 0 29754 135 0 0 25 0 1 0 1796826088 78503936 17883 4294967295 134512640 135094434 3221224432 3221220848 134677007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19166 17883 145 145 0 19021 0 [pid=32062] vsize: 76664 Current children cumulated CPU time (s) 298.9 Current children cumulated vsize (Kb) 78788 [startup+310.024 s] Raw data (loadavg): 0.99 0.67 0.29 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 33550 0 0 0 30754 135 0 0 25 0 1 0 1796826088 78503936 17897 4294967295 134512640 135094434 3221224432 3221221328 134676465 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19166 17897 145 145 0 19021 0 [pid=32062] vsize: 76664 Current children cumulated CPU time (s) 308.9 Current children cumulated vsize (Kb) 78788 [startup+320.025 s] Raw data (loadavg): 0.99 0.68 0.30 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 33563 0 0 0 31755 135 0 0 25 0 1 0 1796826088 78503936 17910 4294967295 134512640 135094434 3221224432 3221220656 134676328 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19166 17910 145 145 0 19021 0 [pid=32062] vsize: 76664 Current children cumulated CPU time (s) 318.91 Current children cumulated vsize (Kb) 78788 [startup+330.026 s] Raw data (loadavg): 0.99 0.69 0.31 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 33566 0 0 0 32755 135 0 0 25 0 1 0 1796826088 78503936 17913 4294967295 134512640 135094434 3221224432 3221221456 134676595 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19166 17913 145 145 0 19021 0 [pid=32062] vsize: 76664 Current children cumulated CPU time (s) 328.91 Current children cumulated vsize (Kb) 78788 [startup+340.026 s] Raw data (loadavg): 0.99 0.70 0.31 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 33579 0 0 0 33755 135 0 0 25 0 1 0 1796826088 78503936 17926 4294967295 134512640 135094434 3221224432 3221220928 134600637 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19166 17926 145 145 0 19021 0 [pid=32062] vsize: 76664 Current children cumulated CPU time (s) 338.91 Current children cumulated vsize (Kb) 78788 [startup+350.026 s] Raw data (loadavg): 0.99 0.71 0.32 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 33582 0 0 0 34755 135 0 0 25 0 1 0 1796826088 78503936 17929 4294967295 134512640 135094434 3221224432 3221221084 134676988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19166 17929 145 145 0 19021 0 [pid=32062] vsize: 76664 Current children cumulated CPU time (s) 348.91 Current children cumulated vsize (Kb) 78788 [startup+360.027 s] Raw data (loadavg): 0.99 0.72 0.33 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 33598 0 0 0 35755 135 0 0 25 0 1 0 1796826088 78503936 17945 4294967295 134512640 135094434 3221224432 3221221632 134599982 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19166 17945 145 145 0 19021 0 [pid=32062] vsize: 76664 Current children cumulated CPU time (s) 358.91 Current children cumulated vsize (Kb) 78788 [startup+370.028 s] Raw data (loadavg): 0.99 0.73 0.33 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 33972 0 0 0 36754 136 0 0 25 0 1 0 1796826088 78503936 17989 4294967295 134512640 135094434 3221224432 3221221632 134676489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19166 17989 145 145 0 19021 0 [pid=32062] vsize: 76664 Current children cumulated CPU time (s) 368.91 Current children cumulated vsize (Kb) 78788 [startup+380.029 s] Raw data (loadavg): 0.99 0.74 0.34 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 37812 0 0 0 37741 147 0 0 25 0 1 0 1796826088 80433152 18499 4294967295 134512640 135094434 3221224432 3221221456 134676489 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 19637 18499 145 145 0 19492 0 [pid=32062] vsize: 78548 Current children cumulated CPU time (s) 378.89 Current children cumulated vsize (Kb) 80672 [startup+390.029 s] Raw data (loadavg): 0.99 0.74 0.35 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 38502 0 0 0 38739 148 0 0 25 0 1 0 1796826088 80433152 18529 4294967295 134512640 135094434 3221224432 3221214128 134597156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19637 18529 145 145 0 19492 0 [pid=32062] vsize: 78548 Current children cumulated CPU time (s) 388.88 Current children cumulated vsize (Kb) 80672 [startup+400.03 s] Raw data (loadavg): 0.99 0.75 0.35 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 39798 0 0 0 39734 152 0 0 25 0 1 0 1796826088 80490496 18543 4294967295 134512640 135094434 3221224432 3221220928 134677239 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19651 18543 145 145 0 19506 0 [pid=32062] vsize: 78604 Current children cumulated CPU time (s) 398.87 Current children cumulated vsize (Kb) 80728 [startup+410.031 s] Raw data (loadavg): 0.99 0.76 0.36 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 39798 0 0 0 40735 152 0 0 25 0 1 0 1796826088 80490496 18543 4294967295 134512640 135094434 3221224432 3221221792 134600246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19651 18543 145 145 0 19506 0 [pid=32062] vsize: 78604 Current children cumulated CPU time (s) 408.88 Current children cumulated vsize (Kb) 80728 [startup+420.031 s] Raw data (loadavg): 0.99 0.77 0.37 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 41458 0 0 0 41731 156 0 0 25 0 1 0 1796826088 80490496 18554 4294967295 134512640 135094434 3221224432 3221221728 134677099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19651 18554 145 145 0 19506 0 [pid=32062] vsize: 78604 Current children cumulated CPU time (s) 418.88 Current children cumulated vsize (Kb) 80728 [startup+430.032 s] Raw data (loadavg): 0.99 0.77 0.37 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 42118 0 0 0 42729 157 0 0 25 0 1 0 1796826088 80490496 18554 4294967295 134512640 135094434 3221224432 3221220848 134677056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19651 18554 145 145 0 19506 0 [pid=32062] vsize: 78604 Current children cumulated CPU time (s) 428.87 Current children cumulated vsize (Kb) 80728 [startup+440.032 s] Raw data (loadavg): 0.99 0.78 0.38 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 42143 0 0 0 43729 157 0 0 25 0 1 0 1796826088 80490496 18579 4294967295 134512640 135094434 3221224432 3221221424 134781096 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 19651 18579 145 145 0 19506 0 [pid=32062] vsize: 78604 Current children cumulated CPU time (s) 438.87 Current children cumulated vsize (Kb) 80728 [startup+450.033 s] Raw data (loadavg): 0.99 0.79 0.38 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 42821 0 0 0 44728 159 0 0 25 0 1 0 1796826088 86781952 18597 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 21187 18597 145 145 0 21042 0 [pid=32062] vsize: 84748 Current children cumulated CPU time (s) 448.88 Current children cumulated vsize (Kb) 86872 [startup+460.033 s] Raw data (loadavg): 0.99 0.79 0.39 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 42852 0 0 0 45727 160 0 0 25 0 1 0 1796826088 86781952 18628 4294967295 134512640 135094434 3221224432 3221219344 134677257 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 21187 18628 145 145 0 21042 0 [pid=32062] vsize: 84748 Current children cumulated CPU time (s) 458.88 Current children cumulated vsize (Kb) 86872 [startup+470.033 s] Raw data (loadavg): 0.99 0.80 0.40 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 42874 0 0 0 46727 160 0 0 25 0 1 0 1796826088 86781952 18650 4294967295 134512640 135094434 3221224432 3221220928 134677271 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 21187 18650 145 145 0 21042 0 [pid=32062] vsize: 84748 Current children cumulated CPU time (s) 468.88 Current children cumulated vsize (Kb) 86872 [startup+480.034 s] Raw data (loadavg): 0.99 0.81 0.40 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 42918 0 0 0 47728 160 0 0 25 0 1 0 1796826088 86781952 18694 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 21187 18694 145 145 0 21042 0 [pid=32062] vsize: 84748 Current children cumulated CPU time (s) 478.89 Current children cumulated vsize (Kb) 86872 [startup+490.035 s] Raw data (loadavg): 0.99 0.81 0.41 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 48035 0 0 0 48697 177 0 0 25 0 1 0 1796826088 95309824 20844 4294967295 134512640 135094434 3221224432 3221220752 134600228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 23269 20844 145 145 0 23124 0 [pid=32062] vsize: 93076 Current children cumulated CPU time (s) 488.75 Current children cumulated vsize (Kb) 95200 [startup+500.036 s] Raw data (loadavg): 0.99 0.82 0.41 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 48125 0 0 0 49697 177 0 0 25 0 1 0 1796826088 95309824 20934 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 23269 20934 145 145 0 23124 0 [pid=32062] vsize: 93076 Current children cumulated CPU time (s) 498.75 Current children cumulated vsize (Kb) 95200 [startup+510.037 s] Raw data (loadavg): 0.99 0.82 0.42 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 48164 0 0 0 50696 178 0 0 25 0 1 0 1796826088 95309824 20973 4294967295 134512640 135094434 3221224432 3221219848 134600694 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 23269 20973 145 145 0 23124 0 [pid=32062] vsize: 93076 Current children cumulated CPU time (s) 508.75 Current children cumulated vsize (Kb) 95200 [startup+520.037 s] Raw data (loadavg): 0.99 0.83 0.43 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 48223 0 0 0 51696 178 0 0 25 0 1 0 1796826088 95309824 21032 4294967295 134512640 135094434 3221224432 3221220224 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 23269 21032 145 145 0 23124 0 [pid=32062] vsize: 93076 Current children cumulated CPU time (s) 518.75 Current children cumulated vsize (Kb) 95200 [startup+530.038 s] Raw data (loadavg): 0.99 0.83 0.43 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 50956 0 0 0 52689 185 0 0 25 0 1 0 1796826088 100712448 22447 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22447 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 528.75 Current children cumulated vsize (Kb) 100476 [startup+540.037 s] Raw data (loadavg): 0.99 0.84 0.44 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 50982 0 0 0 53689 185 0 0 25 0 1 0 1796826088 100712448 22473 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22473 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 538.75 Current children cumulated vsize (Kb) 100476 [startup+550.038 s] Raw data (loadavg): 0.99 0.84 0.44 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51004 0 0 0 54689 185 0 0 25 0 1 0 1796826088 100712448 22495 4294967295 134512640 135094434 3221224432 3221219852 134676988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22495 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 548.75 Current children cumulated vsize (Kb) 100476 [startup+560.039 s] Raw data (loadavg): 0.99 0.85 0.45 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51014 0 0 0 55689 185 0 0 25 0 1 0 1796826088 100712448 22505 4294967295 134512640 135094434 3221224432 3221220928 134676503 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22505 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 558.75 Current children cumulated vsize (Kb) 100476 [startup+570.039 s] Raw data (loadavg): 0.99 0.85 0.45 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51041 0 0 0 56690 185 0 0 25 0 1 0 1796826088 100712448 22532 4294967295 134512640 135094434 3221224432 3221221452 134600154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22532 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 568.76 Current children cumulated vsize (Kb) 100476 [startup+580.04 s] Raw data (loadavg): 0.99 0.86 0.46 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51080 0 0 0 57690 185 0 0 25 0 1 0 1796826088 100712448 22571 4294967295 134512640 135094434 3221224432 3221221632 134600144 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22571 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 578.76 Current children cumulated vsize (Kb) 100476 [startup+590.04 s] Raw data (loadavg): 0.99 0.86 0.46 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51122 0 0 0 58690 185 0 0 25 0 1 0 1796826088 100712448 22613 4294967295 134512640 135094434 3221224432 3221220848 134677035 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22613 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 588.76 Current children cumulated vsize (Kb) 100476 [startup+600.041 s] Raw data (loadavg): 0.99 0.86 0.47 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51154 0 0 0 59690 185 0 0 25 0 1 0 1796826088 100712448 22645 4294967295 134512640 135094434 3221224432 3221219664 134519153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22645 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 598.76 Current children cumulated vsize (Kb) 100476 [startup+610.041 s] Raw data (loadavg): 0.99 0.87 0.47 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51173 0 0 0 60690 185 0 0 25 0 1 0 1796826088 100712448 22664 4294967295 134512640 135094434 3221224432 3221221808 134676598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22664 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 608.76 Current children cumulated vsize (Kb) 100476 [startup+620.041 s] Raw data (loadavg): 0.99 0.87 0.48 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51197 0 0 0 61690 185 0 0 25 0 1 0 1796826088 100712448 22688 4294967295 134512640 135094434 3221224432 3221221280 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22688 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 618.76 Current children cumulated vsize (Kb) 100476 [startup+630.042 s] Raw data (loadavg): 0.99 0.88 0.48 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51248 0 0 0 62690 186 0 0 25 0 1 0 1796826088 100712448 22739 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22739 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 628.77 Current children cumulated vsize (Kb) 100476 [startup+640.043 s] Raw data (loadavg): 0.99 0.88 0.49 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51302 0 0 0 63691 186 0 0 25 0 1 0 1796826088 100712448 22793 4294967295 134512640 135094434 3221224432 3221221692 134676610 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22793 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 638.78 Current children cumulated vsize (Kb) 100476 [startup+650.043 s] Raw data (loadavg): 0.99 0.88 0.49 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51362 0 0 0 64691 186 0 0 25 0 1 0 1796826088 100712448 22853 4294967295 134512640 135094434 3221224432 3221220672 134676280 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22853 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 648.78 Current children cumulated vsize (Kb) 100476 [startup+660.044 s] Raw data (loadavg): 0.99 0.89 0.50 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51424 0 0 0 65691 186 0 0 25 0 1 0 1796826088 100712448 22915 4294967295 134512640 135094434 3221224432 3221217472 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 22915 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 658.78 Current children cumulated vsize (Kb) 100476 [startup+670.045 s] Raw data (loadavg): 0.99 0.89 0.50 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51534 0 0 0 66690 187 0 0 25 0 1 0 1796826088 100712448 23025 4294967295 134512640 135094434 3221224432 3221220672 134677065 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 23025 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 668.78 Current children cumulated vsize (Kb) 100476 [startup+680.045 s] Raw data (loadavg): 0.99 0.89 0.51 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 51577 0 0 0 67690 187 0 0 25 0 1 0 1796826088 100712448 23068 4294967295 134512640 135094434 3221224432 3221221600 134676245 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 23068 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 678.78 Current children cumulated vsize (Kb) 100476 [startup+690.045 s] Raw data (loadavg): 0.99 0.90 0.51 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 52247 0 0 0 68689 188 0 0 25 0 1 0 1796826088 100712448 23079 4294967295 134512640 135094434 3221224432 3221220048 134600232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 23079 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 688.78 Current children cumulated vsize (Kb) 100476 [startup+700.046 s] Raw data (loadavg): 0.99 0.90 0.52 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 52247 0 0 0 69690 188 0 0 25 0 1 0 1796826088 100712448 23079 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 23079 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 698.79 Current children cumulated vsize (Kb) 100476 [startup+710.047 s] Raw data (loadavg): 0.99 0.90 0.52 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 52247 0 0 0 70690 188 0 0 25 0 1 0 1796826088 100712448 23079 4294967295 134512640 135094434 3221224432 3221221164 134677378 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 23079 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 708.79 Current children cumulated vsize (Kb) 100476 [startup+720.046 s] Raw data (loadavg): 0.99 0.90 0.53 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 53264 0 0 0 71687 191 0 0 25 0 1 0 1796826088 100712448 23107 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 23107 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 718.79 Current children cumulated vsize (Kb) 100476 [startup+730.047 s] Raw data (loadavg): 0.99 0.91 0.53 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 53264 0 0 0 72688 191 0 0 25 0 1 0 1796826088 100712448 23107 4294967295 134512640 135094434 3221224432 3221221328 134676465 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 23107 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 728.8 Current children cumulated vsize (Kb) 100476 [startup+740.048 s] Raw data (loadavg): 0.99 0.91 0.54 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 53264 0 0 0 73688 191 0 0 25 0 1 0 1796826088 100712448 23107 4294967295 134512640 135094434 3221224432 3221221808 134676601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 23107 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 738.8 Current children cumulated vsize (Kb) 100476 [startup+750.049 s] Raw data (loadavg): 0.99 0.91 0.54 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54258 0 0 0 74685 193 0 0 25 0 1 0 1796826088 100712448 23112 4294967295 134512640 135094434 3221224432 3221220576 134600254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 23112 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 748.79 Current children cumulated vsize (Kb) 100476 [startup+760.049 s] Raw data (loadavg): 0.99 0.91 0.55 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54258 0 0 0 75685 193 0 0 25 0 1 0 1796826088 100712448 23112 4294967295 134512640 135094434 3221224432 3221221456 134600186 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 23112 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 758.79 Current children cumulated vsize (Kb) 100476 [startup+770.049 s] Raw data (loadavg): 0.99 0.92 0.55 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54258 0 0 0 76686 193 0 0 25 0 1 0 1796826088 100712448 23112 4294967295 134512640 135094434 3221224432 3221221984 134600283 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 24588 23112 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 768.8 Current children cumulated vsize (Kb) 100476 [startup+780.05 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54262 0 0 0 77685 194 0 0 25 0 1 0 1796826088 100712448 23116 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23116 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 778.8 Current children cumulated vsize (Kb) 100476 [startup+790.051 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54285 0 0 0 78684 194 0 0 25 0 1 0 1796826088 100712448 23139 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23139 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 788.79 Current children cumulated vsize (Kb) 100476 [startup+800.051 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54309 0 0 0 79684 195 0 0 25 0 1 0 1796826088 100712448 23163 4294967295 134512640 135094434 3221224432 3221220752 134677333 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23163 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 798.8 Current children cumulated vsize (Kb) 100476 [startup+810.052 s] Raw data (loadavg): 0.99 0.92 0.57 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54309 0 0 0 80684 195 0 0 25 0 1 0 1796826088 100712448 23163 4294967295 134512640 135094434 3221224432 3221220368 134676245 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23163 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 808.8 Current children cumulated vsize (Kb) 100476 [startup+820.052 s] Raw data (loadavg): 0.99 0.93 0.57 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54309 0 0 0 81683 195 0 0 25 0 1 0 1796826088 100712448 23163 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23163 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 818.79 Current children cumulated vsize (Kb) 100476 [startup+830.053 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54309 0 0 0 82683 195 0 0 25 0 1 0 1796826088 100712448 23163 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23163 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 828.79 Current children cumulated vsize (Kb) 100476 [startup+840.053 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54309 0 0 0 83683 195 0 0 25 0 1 0 1796826088 100712448 23163 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23163 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 838.79 Current children cumulated vsize (Kb) 100476 [startup+850.055 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54309 0 0 0 84683 195 0 0 25 0 1 0 1796826088 100712448 23163 4294967295 134512640 135094434 3221224432 3221219616 134677065 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23163 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 848.79 Current children cumulated vsize (Kb) 100476 [startup+860.056 s] Raw data (loadavg): 0.99 0.93 0.59 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54309 0 0 0 85683 196 0 0 25 0 1 0 1796826088 100712448 23163 4294967295 134512640 135094434 3221224432 3221221164 134677228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23163 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 858.8 Current children cumulated vsize (Kb) 100476 [startup+870.056 s] Raw data (loadavg): 0.99 0.94 0.59 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54318 0 0 0 86683 196 0 0 25 0 1 0 1796826088 100712448 23172 4294967295 134512640 135094434 3221224432 3221220448 134677375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23172 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 868.8 Current children cumulated vsize (Kb) 100476 [startup+880.056 s] Raw data (loadavg): 0.99 0.94 0.59 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54321 0 0 0 87682 196 0 0 25 0 1 0 1796826088 100712448 23175 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23175 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 878.79 Current children cumulated vsize (Kb) 100476 [startup+890.057 s] Raw data (loadavg): 0.99 0.94 0.60 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54321 0 0 0 88682 196 0 0 25 0 1 0 1796826088 100712448 23175 4294967295 134512640 135094434 3221224432 3221221648 134783385 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23175 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 888.79 Current children cumulated vsize (Kb) 100476 [startup+900.058 s] Raw data (loadavg): 0.99 0.94 0.60 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54342 0 0 0 89682 197 0 0 25 0 1 0 1796826088 100712448 23196 4294967295 134512640 135094434 3221224432 3221221792 134600246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23196 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 898.8 Current children cumulated vsize (Kb) 100476 [startup+910.058 s] Raw data (loadavg): 0.99 0.94 0.61 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54358 0 0 0 90682 197 0 0 25 0 1 0 1796826088 100712448 23212 4294967295 134512640 135094434 3221224432 3221221456 134676516 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23212 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 908.8 Current children cumulated vsize (Kb) 100476 [startup+920.059 s] Raw data (loadavg): 0.99 0.94 0.61 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54443 0 0 0 91681 198 0 0 25 0 1 0 1796826088 100712448 23297 4294967295 134512640 135094434 3221224432 3221220400 134600002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23297 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 918.8 Current children cumulated vsize (Kb) 100476 [startup+930.06 s] Raw data (loadavg): 0.99 0.94 0.61 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 54538 0 0 0 92681 198 0 0 25 0 1 0 1796826088 100712448 23392 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 24588 23392 145 145 0 24443 0 [pid=32062] vsize: 98352 Current children cumulated CPU time (s) 928.8 Current children cumulated vsize (Kb) 100476 [startup+940.061 s] Raw data (loadavg): 0.99 0.95 0.62 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 60108 0 0 0 93661 212 0 0 25 0 1 0 1796826088 104427520 24348 4294967295 134512640 135094434 3221224432 3221218964 134676244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 25495 24348 145 145 0 25350 0 [pid=32062] vsize: 101980 Current children cumulated CPU time (s) 938.74 Current children cumulated vsize (Kb) 104104 [startup+950.062 s] Raw data (loadavg): 0.99 0.95 0.62 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 60170 0 0 0 94661 212 0 0 25 0 1 0 1796826088 104427520 24410 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 25495 24410 145 145 0 25350 0 [pid=32062] vsize: 101980 Current children cumulated CPU time (s) 948.74 Current children cumulated vsize (Kb) 104104 [startup+960.063 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 60217 0 0 0 95661 213 0 0 25 0 1 0 1796826088 117010432 24457 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 28567 24457 145 145 0 28422 0 [pid=32062] vsize: 114268 Current children cumulated CPU time (s) 958.75 Current children cumulated vsize (Kb) 116392 [startup+970.064 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 60337 0 0 0 96660 214 0 0 25 0 1 0 1796826088 117010432 24577 4294967295 134512640 135094434 3221224432 3221221104 134600295 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 28567 24577 145 145 0 28422 0 [pid=32062] vsize: 114268 Current children cumulated CPU time (s) 968.75 Current children cumulated vsize (Kb) 116392 [startup+980.065 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 60460 0 0 0 97659 214 0 0 25 0 1 0 1796826088 117010432 24700 4294967295 134512640 135094434 3221224432 3221219872 134677248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 28567 24700 145 145 0 28422 0 [pid=32062] vsize: 114268 Current children cumulated CPU time (s) 978.74 Current children cumulated vsize (Kb) 116392 [startup+990.065 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 60491 0 0 0 98659 215 0 0 25 0 1 0 1796826088 117010432 24731 4294967295 134512640 135094434 3221224432 3221221456 134600310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 28567 24731 145 145 0 28422 0 [pid=32062] vsize: 114268 Current children cumulated CPU time (s) 988.75 Current children cumulated vsize (Kb) 116392 [startup+1000.07 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 60533 0 0 0 99658 216 0 0 25 0 1 0 1796826088 117010432 24773 4294967295 134512640 135094434 3221224432 3221220144 134677069 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 28567 24773 145 145 0 28422 0 [pid=32062] vsize: 114268 Current children cumulated CPU time (s) 998.75 Current children cumulated vsize (Kb) 116392 [startup+1010.07 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 60571 0 0 0 100657 216 0 0 25 0 1 0 1796826088 117010432 24811 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 28567 24811 145 145 0 28422 0 [pid=32062] vsize: 114268 Current children cumulated CPU time (s) 1008.74 Current children cumulated vsize (Kb) 116392 [startup+1020.07 s] Raw data (loadavg): 0.99 0.95 0.65 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 60621 0 0 0 101657 217 0 0 25 0 1 0 1796826088 117010432 24861 4294967295 134512640 135094434 3221224432 3221220784 134783378 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 28567 24861 145 145 0 28422 0 [pid=32062] vsize: 114268 Current children cumulated CPU time (s) 1018.75 Current children cumulated vsize (Kb) 116392 [startup+1030.07 s] Raw data (loadavg): 0.99 0.95 0.65 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 66617 0 0 0 102626 236 0 0 24 0 1 0 1796826088 130478080 28217 4294967295 134512640 135094434 3221224432 3221212432 134596848 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 31855 28217 145 145 0 31710 0 [pid=32062] vsize: 127420 Current children cumulated CPU time (s) 1028.63 Current children cumulated vsize (Kb) 129544 [startup+1040.07 s] Raw data (loadavg): 0.99 0.96 0.65 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 81733 0 0 0 103574 276 0 0 25 0 1 0 1796826088 127868928 27588 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 31218 27588 145 145 0 31073 0 [pid=32062] vsize: 124872 Current children cumulated CPU time (s) 1038.51 Current children cumulated vsize (Kb) 126996 [startup+1050.07 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 81751 0 0 0 104574 276 0 0 25 0 1 0 1796826088 127868928 27606 4294967295 134512640 135094434 3221224432 3221206788 134597107 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 31218 27606 145 145 0 31073 0 [pid=32062] vsize: 124872 Current children cumulated CPU time (s) 1048.51 Current children cumulated vsize (Kb) 126996 [startup+1060.07 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 87023 0 0 0 105556 291 0 0 25 0 1 0 1796826088 130023424 28136 4294967295 134512640 135094434 3221224432 3221221456 134600310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 31744 28136 145 145 0 31599 0 [pid=32062] vsize: 126976 Current children cumulated CPU time (s) 1058.48 Current children cumulated vsize (Kb) 129100 [startup+1070.07 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 91933 0 0 0 106541 304 0 0 25 0 1 0 1796826088 131141632 28432 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 32017 28432 145 145 0 31872 0 [pid=32062] vsize: 128068 Current children cumulated CPU time (s) 1068.46 Current children cumulated vsize (Kb) 130192 [startup+1080.07 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 96569 0 0 0 107530 316 0 0 25 0 1 0 1796826088 131141632 28454 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 32017 28454 145 145 0 31872 0 [pid=32062] vsize: 128068 Current children cumulated CPU time (s) 1078.47 Current children cumulated vsize (Kb) 130192 [startup+1090.07 s] Raw data (loadavg): 0.99 0.96 0.67 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 96569 0 0 0 108530 316 0 0 25 0 1 0 1796826088 131141632 28454 4294967295 134512640 135094434 3221224432 3221219616 134676999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 32017 28454 145 145 0 31872 0 [pid=32062] vsize: 128068 Current children cumulated CPU time (s) 1088.47 Current children cumulated vsize (Kb) 130192 [startup+1100.07 s] Raw data (loadavg): 0.99 0.96 0.67 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 98898 0 0 0 109523 322 0 0 25 0 1 0 1796826088 131141632 28476 4294967295 134512640 135094434 3221224432 3221220576 134600283 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 32017 28476 145 145 0 31872 0 [pid=32062] vsize: 128068 Current children cumulated CPU time (s) 1098.46 Current children cumulated vsize (Kb) 130192 [startup+1110.07 s] Raw data (loadavg): 0.99 0.96 0.67 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 99907 0 0 0 110521 325 0 0 25 0 1 0 1796826088 131141632 28496 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 32017 28496 145 145 0 31872 0 [pid=32062] vsize: 128068 Current children cumulated CPU time (s) 1108.47 Current children cumulated vsize (Kb) 130192 [startup+1120.07 s] Raw data (loadavg): 0.99 0.96 0.68 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 99907 0 0 0 111520 326 0 0 25 0 1 0 1796826088 131141632 28496 4294967295 134512640 135094434 3221224432 3221220752 134676552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/32062/statm): 32017 28496 145 145 0 31872 0 [pid=32062] vsize: 128068 Current children cumulated CPU time (s) 1118.47 Current children cumulated vsize (Kb) 130192 [startup+1130.07 s] Raw data (loadavg): 0.99 0.96 0.68 4/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 102229 0 0 0 112514 332 0 0 25 0 1 0 1796826088 131141632 28511 4294967295 134512640 135094434 3221224432 3221220016 134676245 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 32017 28511 145 145 0 31872 0 [pid=32062] vsize: 128068 Current children cumulated CPU time (s) 1128.47 Current children cumulated vsize (Kb) 130192 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.68 1/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) T 32058 32058 30740 0 -1 0 116880 0 0 0 113445 374 0 0 23 0 1 0 1796826088 170868736 38218 4294967295 134512640 135094434 3221224432 3221210716 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/32062/statm): 41716 38218 145 145 0 41571 0 [pid=32062] vsize: 166864 Current children cumulated CPU time (s) 1138.2 Current children cumulated vsize (Kb) 168988 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.68 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 136141 0 0 0 114332 438 0 0 25 0 1 0 1796826088 182726656 41117 4294967295 134512640 135094434 3221224432 3221220048 134676519 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 44611 41117 145 145 0 44466 0 [pid=32062] vsize: 178444 Current children cumulated CPU time (s) 1147.71 Current children cumulated vsize (Kb) 180568 [startup+1160.08 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 136141 0 0 0 115332 438 0 0 25 0 1 0 1796826088 182726656 41117 4294967295 134512640 135094434 3221224432 3221219944 134677084 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 44611 41117 145 145 0 44466 0 [pid=32062] vsize: 178444 Current children cumulated CPU time (s) 1157.71 Current children cumulated vsize (Kb) 180568 [startup+1170.08 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 146707 0 0 0 116306 464 0 0 25 0 1 0 1796826088 204324864 46410 4294967295 134512640 135094434 3221224432 3221209792 134596842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 49884 46410 145 145 0 49739 0 [pid=32062] vsize: 199536 Current children cumulated CPU time (s) 1167.71 Current children cumulated vsize (Kb) 201660 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 149356 0 0 0 117299 471 0 0 25 0 1 0 1796826088 182726656 41149 4294967295 134512640 135094434 3221224432 3221220224 134676542 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 44611 41149 145 145 0 44466 0 [pid=32062] vsize: 178444 Current children cumulated CPU time (s) 1177.71 Current children cumulated vsize (Kb) 180568 [startup+1190.08 s] Raw data (loadavg): 0.99 0.97 0.70 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 149356 0 0 0 118299 471 0 0 25 0 1 0 1796826088 182726656 41149 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 44611 41149 145 145 0 44466 0 [pid=32062] vsize: 178444 Current children cumulated CPU time (s) 1187.71 Current children cumulated vsize (Kb) 180568 [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.70 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 152015 0 0 0 119293 478 0 0 25 0 1 0 1796826088 182726656 41171 4294967295 134512640 135094434 3221224432 3221218464 134600345 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 44611 41171 145 145 0 44466 0 [pid=32062] vsize: 178444 Current children cumulated CPU time (s) 1197.72 Current children cumulated vsize (Kb) 180568 [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.70 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 152015 0 0 0 120293 478 0 0 25 0 1 0 1796826088 182726656 41171 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 44611 41171 145 145 0 44466 0 [pid=32062] vsize: 178444 Current children cumulated CPU time (s) 1207.72 Current children cumulated vsize (Kb) 180568 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.70 2/57 32062 Raw data (/proc/32058/stat): 32058 (minisat+_script) S 32057 32058 30740 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1796826084 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/32058/statm): 531 226 485 147 0 384 0 [pid=32058] vsize: 2124 Raw data (/proc/32062/stat): 32062 (minisat+_64-bit) R 32058 32058 30740 0 -1 0 152015 0 0 0 120293 478 0 0 25 0 1 0 1796826088 182726656 41171 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/32062/statm): 44611 41171 145 145 0 44466 0 [pid=32062] vsize: 178444 Current children cumulated CPU time (s) 1207.72 Current children cumulated vsize (Kb) 180568 Sending SIGTERM to -32058 Sleeping 2 seconds One traced child (pid=32058) ended because it received signal 15 (SIGTERM) One traced child (pid=32062) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.16 CPU time (s): 1207.8 CPU user time (s): 1202.94 CPU system time (s): 4.86026 CPU usage (%): 99.8047 Max. virtual memory (cumulated for all children) (Kb): 201660
ERROR: no interpretation found !