Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namemps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-bc1.opb
MD5SUM15670523760c6351fb6de07139f11abe
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
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 31
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 2147483647
Number of bits of the sum of numbers in the objective function 31
Biggest number in a constraint 1073741824000000000000000000
Number of bits of the biggest number in a constraint 90
Biggest sum of numbers in a constraint 3221975665359866705114824704
Number of bits of the biggest sum of numbers92
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables27730
Total number of constraints3627
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)336
Number of constraints which are nor clauses,nor cardinality constraints3291
Minimum length of a constraint1
Maximum length of a constraint5701

Trace number 5905

Launcher Data

LAUNCH ON wulflinc18 THE 2005-09-20 01:47:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3086 boxname=wulflinc18 idbench=742 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  15670523760c6351fb6de07139f11abe  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-bc1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-bc1.opb
IDLAUNCH: 3086
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        776552 kB
Buffers:         20396 kB
Cached:         204304 kB
SwapCached:        856 kB
Active:         116924 kB
Inactive:       110416 kB
HighTotal:      131008 kB
HighFree:         3780 kB
LowTotal:       903652 kB
LowFree:        772772 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            25180 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 02:07:25 (client local time) WITH STATUS 0 IN 1209.68 SECONDS
stats: 3086 7 1209.68 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 3471] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 4160 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[4159]---> BDD-cost:   30
c ---[4158]---> BDD-cost:   30
c ---[4157]---> BDD-cost:   30
c ---[4156]---> BDD-cost:   30
c ---[4155]---> BDD-cost:   30
c ---[4154]---> BDD-cost:   30
c ---[4153]---> BDD-cost:   30
c ---[4152]---> BDD-cost:   30
c ---[4151]---> BDD-cost:   30
c ---[4150]---> BDD-cost:   30
c ---[4149]---> BDD-cost:   30
c ---[4148]---> BDD-cost:   30
c ---[4147]---> BDD-cost:   30
c ---[4146]---> BDD-cost:   30
c ---[4145]---> BDD-cost:   30
c ---[4144]---> BDD-cost:   30
c ---[4143]---> BDD-cost:   30
c ---[4142]---> BDD-cost:   30
c ---[4141]---> BDD-cost:   30
c ---[4140]---> BDD-cost:   30
c ---[4139]---> BDD-cost:   30
c ---[4138]---> BDD-cost:   30
c ---[4137]---> BDD-cost:   30
c ---[4136]---> BDD-cost:   30
c ---[4135]---> BDD-cost:   30
c ---[4134]---> BDD-cost:   30
c ---[4133]---> BDD-cost:   30
c ---[4132]---> BDD-cost:   30
c ---[4131]---> BDD-cost:   30
c ---[4130]---> BDD-cost:   30
c ---[4129]---> BDD-cost:   30
c ---[4128]---> BDD-cost:   30
c ---[4127]---> BDD-cost:   30
c ---[4126]---> BDD-cost:   30
c ---[4125]---> BDD-cost:   30
c ---[4124]---> BDD-cost:   30
c ---[4123]---> BDD-cost:   30
c ---[4122]---> BDD-cost:   30
c ---[4121]---> BDD-cost:   30
c ---[4120]---> BDD-cost:   30
c ---[4119]---> BDD-cost:   30
c ---[4118]---> BDD-cost:   30
c ---[4117]---> BDD-cost:   30
c ---[4116]---> BDD-cost:   30
c ---[4115]---> BDD-cost:   30
c ---[4114]---> BDD-cost:   30
c ---[4113]---> BDD-cost:   30
c ---[4112]---> BDD-cost:   30
c ---[4111]---> BDD-cost:   30
c ---[4110]---> BDD-cost:   30
c ---[4109]---> BDD-cost:   30
c ---[4108]---> BDD-cost:   30
c ---[4107]---> BDD-cost:   30
c ---[4106]---> BDD-cost:   30
c ---[4105]---> BDD-cost:   30
c ---[4104]---> BDD-cost:   30
c ---[4103]---> BDD-cost:   30
c ---[4102]---> BDD-cost:   30
c ---[4101]---> BDD-cost:   30
c ---[4100]---> BDD-cost:   30
c ---[4099]---> BDD-cost:   30
c ---[4098]---> BDD-cost:   30
c ---[4097]---> BDD-cost:   30
c ---[4096]---> BDD-cost:   30
c ---[4095]---> BDD-cost:   30
c ---[4094]---> BDD-cost:   30
c ---[4093]---> BDD-cost:   30
c ---[4092]---> BDD-cost:   30
c ---[4091]---> BDD-cost:   30
c ---[4090]---> BDD-cost:   30
c ---[4089]---> BDD-cost:   30
c ---[4088]---> BDD-cost:   30
c ---[4087]---> BDD-cost:   30
c ---[4086]---> BDD-cost:   30
c ---[4085]---> BDD-cost:   30
c ---[4084]---> BDD-cost:   30
c ---[4083]---> BDD-cost:   30
c ---[4082]---> BDD-cost:   30
c ---[4081]---> BDD-cost:   30
c ---[4080]---> BDD-cost:   30
c ---[4079]---> BDD-cost:   30
c ---[4078]---> BDD-cost:   30
c ---[4077]---> BDD-cost:   30
c ---[4076]---> BDD-cost:   30
c ---[4075]---> BDD-cost:   30
c ---[4074]---> BDD-cost:   30
c ---[4073]---> BDD-cost:   30
c ---[4072]---> BDD-cost:   30
c ---[4071]---> BDD-cost:   30
c ---[4070]---> BDD-cost:   30
c ---[4069]---> BDD-cost:   30
c ---[4068]---> BDD-cost:   30
c ---[4067]---> BDD-cost:   30
c ---[4066]---> BDD-cost:   30
c ---[4065]---> BDD-cost:   30
c ---[4064]---> BDD-cost:   30
c ---[4063]---> BDD-cost:   30
c ---[4062]---> BDD-cost:   30
c ---[4061]---> BDD-cost:   30
c ---[4060]---> BDD-cost:   30
c ---[4059]---> BDD-cost:   30
c ---[4058]---> BDD-cost:   30
c ---[4057]---> BDD-cost:   30
c ---[4056]---> BDD-cost:   30
c ---[4055]---> BDD-cost:   10
c ---[4054]---> BDD-cost:   10
c ---[4053]---> BDD-cost:   10
c ---[4052]---> BDD-cost:   10
c ---[4051]---> BDD-cost:   10
c ---[4050]---> BDD-cost:   10
c ---[4049]---> BDD-cost:   30
c ---[4048]---> BDD-cost:   30
c ---[4047]---> BDD-cost:   30
c ---[4046]---> BDD-cost:   30
c ---[4045]---> BDD-cost:   30
c ---[4044]---> BDD-cost:   30
c ---[4043]---> BDD-cost:   10
c ---[4042]---> BDD-cost:   10
c ---[4041]---> BDD-cost:   10
c ---[4040]---> BDD-cost:   10
c ---[4039]---> BDD-cost:   10
c ---[4038]---> BDD-cost:   10
c ---[4037]---> BDD-cost:   30
c ---[4036]---> BDD-cost:   30
c ---[4035]---> BDD-cost:   30
c ---[4034]---> BDD-cost:   30
c ---[4033]---> BDD-cost:   30
c ---[4032]---> BDD-cost:   30
c ---[4031]---> BDD-cost:   30
c ---[4030]---> BDD-cost:   30
c ---[4029]---> BDD-cost:   10
c ---[4028]---> BDD-cost:   10
c ---[4027]---> BDD-cost:   10
c ---[4026]---> BDD-cost:   10
c ---[4025]---> BDD-cost:   10
c ---[4024]---> BDD-cost:   10
c ---[4023]---> BDD-cost:   30
c ---[4022]---> BDD-cost:   30
c ---[4021]---> BDD-cost:   30
c ---[4020]---> BDD-cost:   30
c ---[4019]---> BDD-cost:   30
c ---[4018]---> BDD-cost:   30
c ---[4017]---> BDD-cost:   10
c ---[4016]---> BDD-cost:   10
c ---[4015]---> BDD-cost:   10
c ---[4014]---> BDD-cost:   10
c ---[4013]---> BDD-cost:   10
c ---[4012]---> BDD-cost:   10
c ---[4011]---> BDD-cost:   30
c ---[4010]---> BDD-cost:   30
c ---[4009]---> BDD-cost:   30
c ---[4008]---> BDD-cost:   30
c ---[4007]---> BDD-cost:   30
c ---[4006]---> BDD-cost:   30
c ---[4005]---> BDD-cost:   30
c ---[4004]---> BDD-cost:   30
c ---[4003]---> BDD-cost:   10
c ---[4002]---> BDD-cost:   10
c ---[4001]---> BDD-cost:   10
c ---[4000]---> BDD-cost:   10
c ---[3999]---> BDD-cost:   10
c ---[3998]---> BDD-cost:   10
c ---[3997]---> BDD-cost:   30
c ---[3996]---> BDD-cost:   30
c ---[3995]---> BDD-cost:   30
c ---[3994]---> BDD-cost:   30
c ---[3993]---> BDD-cost:   30
c ---[3992]---> BDD-cost:   30
c ---[3991]---> BDD-cost:   10
c ---[3990]---> BDD-cost:   10
c ---[3989]---> BDD-cost:   10
c ---[3988]---> BDD-cost:   10
c ---[3987]---> BDD-cost:   10
c ---[3986]---> BDD-cost:   10
c ---[3985]---> BDD-cost:   30
c ---[3984]---> BDD-cost:   30
c ---[3983]---> BDD-cost:   30
c ---[3982]---> BDD-cost:   30
c ---[3981]---> BDD-cost:   30
c ---[3980]---> BDD-cost:   30
c ---[3979]---> BDD-cost:   30
c ---[3978]---> BDD-cost:   30
c ---[3977]---> BDD-cost:   10
c ---[3976]---> BDD-cost:   10
c ---[3975]---> BDD-cost:   10
c ---[3974]---> BDD-cost:   10
c ---[3973]---> BDD-cost:   10
c ---[3972]---> BDD-cost:   10
c ---[3971]---> BDD-cost:   30
c ---[3970]---> BDD-cost:   30
c ---[3969]---> BDD-cost:   30
c ---[3968]---> BDD-cost:   30
c ---[3967]---> BDD-cost:   30
c ---[3966]---> BDD-cost:   30
c ---[3965]---> BDD-cost:   10
c ---[3964]---> BDD-cost:   10
c ---[3963]---> BDD-cost:   10
c ---[3962]---> BDD-cost:   10
c ---[3961]---> BDD-cost:   10
c ---[3960]---> BDD-cost:   10
c ---[3959]---> BDD-cost:   30
c ---[3958]---> BDD-cost:   30
c ---[3957]---> BDD-cost:   30
c ---[3956]---> BDD-cost:   30
c ---[3955]---> BDD-cost:   30
c ---[3954]---> BDD-cost:   30
c ---[3953]---> BDD-cost:   30
c ---[3952]---> BDD-cost:   30
c ---[3951]---> BDD-cost:   10
c ---[3950]---> BDD-cost:   10
c ---[3949]---> BDD-cost:   10
c ---[3948]---> BDD-cost:   10
c ---[3947]---> BDD-cost:   10
c ---[3946]---> BDD-cost:   10
c ---[3945]---> BDD-cost:   30
c ---[3944]---> BDD-cost:   30
c ---[3943]---> BDD-cost:   30
c ---[3942]---> BDD-cost:   30
c ---[3941]---> BDD-cost:   30
c ---[3940]---> BDD-cost:   30
c ---[3939]---> BDD-cost:   10
c ---[3938]---> BDD-cost:   10
c ---[3937]---> BDD-cost:   10
c ---[3936]---> BDD-cost:   10
c ---[3935]---> BDD-cost:   10
c ---[3934]---> BDD-cost:   10
c ---[3933]---> BDD-cost:   30
c ---[3932]---> BDD-cost:   30
c ---[3931]---> BDD-cost:   30
c ---[3930]---> BDD-cost:   30
c ---[3929]---> BDD-cost:   30
c ---[3928]---> BDD-cost:   30
c ---[3927]---> BDD-cost:   30
c ---[3926]---> BDD-cost:   30
c ---[3925]---> BDD-cost:   10
c ---[3924]---> BDD-cost:   10
c ---[3923]---> BDD-cost:   10
c ---[3922]---> BDD-cost:   10
c ---[3921]---> BDD-cost:   10
c ---[3920]---> BDD-cost:   10
c ---[3919]---> BDD-cost:   30
c ---[3918]---> BDD-cost:   30
c ---[3917]---> BDD-cost:   30
c ---[3916]---> BDD-cost:   30
c ---[3915]---> BDD-cost:   30
c ---[3914]---> BDD-cost:   30
c ---[3913]---> BDD-cost:   10
c ---[3912]---> BDD-cost:   10
c ---[3911]---> BDD-cost:   10
c ---[3910]---> BDD-cost:   10
c ---[3909]---> BDD-cost:   10
c ---[3908]---> BDD-cost:   10
c ---[3907]---> BDD-cost:   30
c ---[3906]---> BDD-cost:   30
c ---[3905]---> BDD-cost:   30
c ---[3904]---> BDD-cost:   30
c ---[3903]---> BDD-cost:   30
c ---[3902]---> BDD-cost:   30
c ---[3901]---> BDD-cost:   30
c ---[3900]---> BDD-cost:   30
c ---[3899]---> BDD-cost:   10
c ---[3898]---> BDD-cost:   10
c ---[3897]---> BDD-cost:   10
c ---[3896]---> BDD-cost:   10
c ---[3895]---> BDD-cost:   10
c ---[3894]---> BDD-cost:   10
c ---[3893]---> BDD-cost:   30
c ---[3892]---> BDD-cost:   30
c ---[3891]---> BDD-cost:   30
c ---[3890]---> BDD-cost:   30
c ---[3889]---> BDD-cost:   30
c ---[3888]---> BDD-cost:   30
c ---[3887]---> BDD-cost:   10
c ---[3886]---> BDD-cost:   10
c ---[3885]---> BDD-cost:   10
c ---[3884]---> BDD-cost:   10
c ---[3883]---> BDD-cost:   10
c ---[3882]---> BDD-cost:   10
c ---[3881]---> BDD-cost:   30
c ---[3880]---> BDD-cost:   30
c ---[3879]---> BDD-cost:   30
c ---[3878]---> BDD-cost:   30
c ---[3877]---> BDD-cost:   30
c ---[3876]---> BDD-cost:   30
c ---[3875]---> BDD-cost:   30
c ---[3874]---> BDD-cost:   30
c ---[3873]---> BDD-cost:   10
c ---[3872]---> BDD-cost:   10
c ---[3871]---> BDD-cost:   10
c ---[3870]---> BDD-cost:   10
c ---[3869]---> BDD-cost:   10
c ---[3868]---> BDD-cost:   10
c ---[3867]---> BDD-cost:   30
c ---[3866]---> BDD-cost:   30
c ---[3865]---> BDD-cost:   30
c ---[3864]---> BDD-cost:   30
c ---[3863]---> BDD-cost:   30
c ---[3862]---> BDD-cost:   30
c ---[3861]---> BDD-cost:   10
c ---[3860]---> BDD-cost:   10
c ---[3859]---> BDD-cost:   10
c ---[3858]---> BDD-cost:   10
c ---[3857]---> BDD-cost:   10
c ---[3856]---> BDD-cost:   10
c ---[3855]---> BDD-cost:   30
c ---[3854]---> BDD-cost:   30
c ---[3853]---> BDD-cost:   30
c ---[3852]---> BDD-cost:   30
c ---[3851]---> BDD-cost:   30
c ---[3850]---> BDD-cost:   30
c ---[3849]---> BDD-cost:   30
c ---[3848]---> BDD-cost:   30
c ---[3847]---> BDD-cost:   10
c ---[3846]---> BDD-cost:   10
c ---[3845]---> BDD-cost:   10
c ---[3844]---> BDD-cost:   10
c ---[3843]---> BDD-cost:   10
c ---[3842]---> BDD-cost:   10
c ---[3841]---> BDD-cost:   30
c ---[3840]---> BDD-cost:   30
c ---[3839]---> BDD-cost:   30
c ---[3838]---> BDD-cost:   30
c ---[3837]---> BDD-cost:   30
c ---[3836]---> BDD-cost:   30
c ---[3835]---> BDD-cost:   10
c ---[3834]---> BDD-cost:   10
c ---[3833]---> BDD-cost:   10
c ---[3832]---> BDD-cost:   10
c ---[3831]---> BDD-cost:   10
c ---[3830]---> BDD-cost:   10
c ---[3829]---> BDD-cost:   30
c ---[3828]---> BDD-cost:   30
c ---[3827]---> BDD-cost:   30
c ---[3826]---> BDD-cost:   30
c ---[3825]---> BDD-cost:   30
c ---[3824]---> BDD-cost:   30
c ---[3823]---> BDD-cost:   30
c ---[3822]---> BDD-cost:   30
c ---[3821]---> BDD-cost:   10
c ---[3820]---> BDD-cost:   10
c ---[3819]---> BDD-cost:   10
c ---[3818]---> BDD-cost:   10
c ---[3817]---> BDD-cost:   10
c ---[3816]---> BDD-cost:   10
c ---[3815]---> BDD-cost:   30
c ---[3814]---> BDD-cost:   30
c ---[3813]---> BDD-cost:   30
c ---[3812]---> BDD-cost:   30
c ---[3811]---> BDD-cost:   30
c ---[3810]---> BDD-cost:   30
c ---[3809]---> BDD-cost:   30
c ---[3808]---> BDD-cost:   30
c ---[3807]---> BDD-cost:   30
c ---[3806]---> BDD-cost:   30
c ---[3805]---> BDD-cost:   10
c ---[3804]---> BDD-cost:   10
c ---[3803]---> BDD-cost:   10
c ---[3802]---> BDD-cost:   10
c ---[3801]---> BDD-cost:   10
c ---[3800]---> BDD-cost:   10
c ---[3799]---> BDD-cost:   30
c ---[3798]---> BDD-cost:   30
c ---[3797]---> BDD-cost:   30
c ---[3796]---> BDD-cost:   30
c ---[3795]---> BDD-cost:   30
c ---[3794]---> BDD-cost:   30
c ---[3793]---> BDD-cost:   30
c ---[3792]---> BDD-cost:   30
c ---[3791]---> BDD-cost:   10
c ---[3790]---> BDD-cost:   10
c ---[3789]---> BDD-cost:   10
c ---[3788]---> BDD-cost:   10
c ---[3787]---> BDD-cost:   10
c ---[3786]---> BDD-cost:   10
c ---[3785]---> BDD-cost:   30
c ---[3784]---> BDD-cost:   30
c ---[3783]---> BDD-cost:   30
c ---[3782]---> BDD-cost:   30
c ---[3781]---> BDD-cost:   30
c ---[3780]---> BDD-cost:   30
c ---[3779]---> BDD-cost:   30
c ---[3778]---> BDD-cost:   30
c ---[3777]---> BDD-cost:   30
c ---[3776]---> BDD-cost:   30
c ---[3775]---> BDD-cost:   10
c ---[3774]---> BDD-cost:   10
c ---[3773]---> BDD-cost:   10
c ---[3772]---> BDD-cost:   10
c ---[3771]---> BDD-cost:   10
c ---[3770]---> BDD-cost:   10
c ---[3769]---> BDD-cost:   30
c ---[3768]---> BDD-cost:   30
c ---[3767]---> BDD-cost:   30
c ---[3766]---> BDD-cost:   30
c ---[3765]---> BDD-cost:   30
c ---[3764]---> BDD-cost:   30
c ---[3763]---> BDD-cost:   30
c ---[3762]---> BDD-cost:   30
c ---[3761]---> BDD-cost:   10
c ---[3760]---> BDD-cost:   10
c ---[3759]---> BDD-cost:   10
c ---[3758]---> BDD-cost:   10
c ---[3757]---> BDD-cost:   10
c ---[3756]---> BDD-cost:   10
c ---[3755]---> BDD-cost:   10
c ---[3754]---> BDD-cost:   10
c ---[3753]---> BDD-cost:   10
c ---[3752]---> BDD-cost:   10
c ---[3751]---> BDD-cost:   10
c ---[3750]---> BDD-cost:   10
c ---[3749]---> BDD-cost:   10
c ---[3748]---> BDD-cost:   10
c ---[3747]---> BDD-cost:   10
c ---[3746]---> BDD-cost:   10
c ---[3745]---> BDD-cost:   10
c ---[3744]---> BDD-cost:   10
c ---[3743]---> BDD-cost:   10
c ---[3742]---> BDD-cost:   10
c ---[3741]---> BDD-cost:   10
c ---[3740]---> BDD-cost:   10
c ---[3739]---> BDD-cost:   30
c ---[3738]---> BDD-cost:   30
c ---[3737]---> BDD-cost:   30
c ---[3736]---> BDD-cost:   30
c ---[3735]---> BDD-cost:   30
c ---[3734]---> BDD-cost:   30
c ---[3733]---> BDD-cost:   30
c ---[3732]---> BDD-cost:   30
c ---[3731]---> BDD-cost:   10
c ---[3730]---> BDD-cost:   10
c ---[3729]---> BDD-cost:   10
c ---[3728]---> BDD-cost:   10
c ---[3727]---> BDD-cost:   10
c ---[3726]---> BDD-cost:   10
c ---[3725]---> BDD-cost:   10
c ---[3724]---> BDD-cost:   10
c ---[3723]---> BDD-cost:   10
c ---[3722]---> BDD-cost:   10
c ---[3721]---> BDD-cost:   10
c ---[3720]---> BDD-cost:   10
c ---[3719]---> BDD-cost:   10
c ---[3718]---> BDD-cost:   10
c ---[3717]---> BDD-cost:   10
c ---[3716]---> BDD-cost:   10
c ---[3715]---> BDD-cost:   10
c ---[3714]---> BDD-cost:   10
c ---[3713]---> BDD-cost:   10
c ---[3712]---> BDD-cost:   10
c ---[3711]---> BDD-cost:   10
c ---[3710]---> BDD-cost:   10
c ---[3709]---> BDD-cost:   30
c ---[3708]---> BDD-cost:   30
c ---[3707]---> BDD-cost:   30
c ---[3706]---> BDD-cost:   30
c ---[3705]---> BDD-cost:   30
c ---[3704]---> BDD-cost:   30
c ---[3703]---> BDD-cost:   30
c ---[3702]---> BDD-cost:   30
c ---[3701]---> BDD-cost:   10
c ---[3700]---> BDD-cost:   10
c ---[3699]---> BDD-cost:   10
c ---[3698]---> BDD-cost:   10
c ---[3697]---> BDD-cost:   10
c ---[3696]---> BDD-cost:   10
c ---[3695]---> BDD-cost:   10
c ---[3694]---> BDD-cost:   10
c ---[3693]---> BDD-cost:   10
c ---[3692]---> BDD-cost:   10
c ---[3691]---> BDD-cost:   10
c ---[3690]---> BDD-cost:   10
c ---[3689]---> BDD-cost:   10
c ---[3688]---> BDD-cost:   10
c ---[3687]---> BDD-cost:   10
c ---[3686]---> BDD-cost:   10
c ---[3685]---> BDD-cost:   10
c ---[3684]---> BDD-cost:   10
c ---[3683]---> BDD-cost:   10
c ---[3682]---> BDD-cost:   10
c ---[3681]---> BDD-cost:   10
c ---[3680]---> BDD-cost:   10
c ---[3679]---> BDD-cost:   30
c ---[3678]---> BDD-cost:   30
c ---[3677]---> BDD-cost:   30
c ---[3676]---> BDD-cost:   30
c ---[3675]---> BDD-cost:   30
c ---[3674]---> BDD-cost:   30
c ---[3673]---> BDD-cost:   30
c ---[3672]---> BDD-cost:   30
c ---[3671]---> BDD-cost:   10
c ---[3670]---> BDD-cost:   10
c ---[3669]---> BDD-cost:   10
c ---[3668]---> BDD-cost:   10
c ---[3667]---> BDD-cost:   10
c ---[3666]---> BDD-cost:   10
c ---[3665]---> BDD-cost:   10
c ---[3664]---> BDD-cost:   10
c ---[3663]---> BDD-cost:   10
c ---[3662]---> BDD-cost:   10
c ---[3661]---> BDD-cost:   10
c ---[3660]---> BDD-cost:   10
c ---[3659]---> BDD-cost:   10
c ---[3658]---> BDD-cost:   10
c ---[3657]---> BDD-cost:   10
c ---[3656]---> BDD-cost:   10
c ---[3655]---> BDD-cost:   10
c ---[3654]---> BDD-cost:   10
c ---[3653]---> BDD-cost:   10
c ---[3652]---> BDD-cost:   10
c ---[3651]---> BDD-cost:   10
c ---[3650]---> BDD-cost:   10
c ---[3649]---> BDD-cost:   30
c ---[3648]---> BDD-cost:   30
c ---[3647]---> BDD-cost:   30
c ---[3646]---> BDD-cost:   30
c ---[3645]---> BDD-cost:   30
c ---[3644]---> BDD-cost:   30
c ---[3643]---> BDD-cost:   30
c ---[3642]---> BDD-cost:   30
c ---[3641]---> BDD-cost:   10
c ---[3640]---> BDD-cost:   10
c ---[3639]---> BDD-cost:   10
c ---[3638]---> BDD-cost:   10
c ---[3637]---> BDD-cost:   10
c ---[3636]---> BDD-cost:   10
c ---[3635]---> BDD-cost:   10
c ---[3634]---> BDD-cost:   10
c ---[3633]---> BDD-cost:   10
c ---[3632]---> BDD-cost:   10
c ---[3631]---> BDD-cost:   10
c ---[3630]---> BDD-cost:   10
c ---[3629]---> BDD-cost:   10
c ---[3628]---> BDD-cost:   10
c ---[3627]---> BDD-cost:   10
c ---[3626]---> BDD-cost:   10
c ---[3625]---> BDD-cost:   10
c ---[3624]---> BDD-cost:   10
c ---[3623]---> BDD-cost:   10
c ---[3622]---> BDD-cost:   10
c ---[3621]---> BDD-cost:   10
c ---[3620]---> BDD-cost:   10
c ---[3619]---> BDD-cost:   30
c ---[3618]---> BDD-cost:   30
c ---[3617]---> BDD-cost:   30
c ---[3616]---> BDD-cost:   30
c ---[3615]---> BDD-cost:   30
c ---[3614]---> BDD-cost:   30
c ---[3613]---> BDD-cost:   30
c ---[3612]---> BDD-cost:   30
c ---[3611]---> BDD-cost:   10
c ---[3610]---> BDD-cost:   10
c ---[3609]---> BDD-cost:   10
c ---[3608]---> BDD-cost:   10
c ---[3607]---> BDD-cost:   10
c ---[3606]---> BDD-cost:   10
c ---[3605]---> BDD-cost:   10
c ---[3604]---> BDD-cost:   10
c ---[3603]---> BDD-cost:   10
c ---[3602]---> BDD-cost:   10
c ---[3601]---> BDD-cost:   10
c ---[3600]---> BDD-cost:   10
c ---[3599]---> BDD-cost:   10
c ---[3598]---> BDD-cost:   10
c ---[3597]---> BDD-cost:   10
c ---[3596]---> BDD-cost:   10
c ---[3595]---> BDD-cost:   10
c ---[3594]---> BDD-cost:   10
c ---[3593]---> BDD-cost:   10
c ---[3592]---> BDD-cost:   10
c ---[3591]---> BDD-cost:   10
c ---[3590]---> BDD-cost:   10
c ---[3589]---> BDD-cost:   30
c ---[3588]---> BDD-cost:   30
c ---[3587]---> BDD-cost:   30
c ---[3586]---> BDD-cost:   30
c ---[3585]---> BDD-cost:   30
c ---[3584]---> BDD-cost:   30
c ---[3583]---> BDD-cost:   30
c ---[3582]---> BDD-cost:   30
c ---[3581]---> BDD-cost:   10
c ---[3580]---> BDD-cost:   10
c ---[3579]---> BDD-cost:   10
c ---[3578]---> BDD-cost:   10
c ---[3577]---> BDD-cost:   10
c ---[3576]---> BDD-cost:   10
c ---[3575]---> BDD-cost:   10
c ---[3574]---> BDD-cost:   10
c ---[3573]---> BDD-cost:   10
c ---[3572]---> BDD-cost:   10
c ---[3571]---> BDD-cost:   10
c ---[3570]---> BDD-cost:   10
c ---[3569]---> BDD-cost:   10
c ---[3568]---> BDD-cost:   10
c ---[3567]---> BDD-cost:   10
c ---[3566]---> BDD-cost:   10
c ---[3565]---> BDD-cost:   10
c ---[3564]---> BDD-cost:   10
c ---[3563]---> BDD-cost:   10
c ---[3562]---> BDD-cost:   10
c ---[3561]---> BDD-cost:   10
c ---[3560]---> BDD-cost:   10
c ---[3559]---> BDD-cost:   30
c ---[3558]---> BDD-cost:   30
c ---[3557]---> BDD-cost:   30
c ---[3556]---> BDD-cost:   30
c ---[3555]---> BDD-cost:   30
c ---[3554]---> BDD-cost:   30
c ---[3553]---> BDD-cost:   30
c ---[3552]---> BDD-cost:   30
c ---[3551]---> BDD-cost:   10
c ---[3550]---> BDD-cost:   10
c ---[3549]---> BDD-cost:   10
c ---[3548]---> BDD-cost:   10
c ---[3547]---> BDD-cost:   10
c ---[3546]---> BDD-cost:   10
c ---[3545]---> BDD-cost:   10
c ---[3544]---> BDD-cost:   10
c ---[3543]---> BDD-cost:   10
c ---[3542]---> BDD-cost:   10
c ---[3541]---> BDD-cost:   10
c ---[3540]---> BDD-cost:   10
c ---[3539]---> BDD-cost:   10
c ---[3538]---> BDD-cost:   10
c ---[3537]---> BDD-cost:   10
c ---[3536]---> BDD-cost:   10
c ---[3535]---> BDD-cost:   10
c ---[3534]---> BDD-cost:   10
c ---[3533]---> BDD-cost:   10
c ---[3532]---> BDD-cost:   10
c ---[3531]---> BDD-cost:   10
c ---[3530]---> BDD-cost:   10
c ---[3529]---> BDD-cost:   30
c ---[3528]---> BDD-cost:   30
c ---[3527]---> BDD-cost:   30
c ---[3526]---> BDD-cost:   30
c ---[3525]---> BDD-cost:   30
c ---[3524]---> BDD-cost:   30
c ---[3523]---> BDD-cost:   30
c ---[3522]---> BDD-cost:   30
c ---[3521]---> BDD-cost:   30
c ---[3520]---> BDD-cost:   30
c ---[3519]---> BDD-cost:   30
c ---[3518]---> BDD-cost:   30
c ---[3517]---> BDD-cost:   30
c ---[3516]---> BDD-cost:   30
c ---[3515]---> BDD-cost:   30
c ---[3514]---> BDD-cost:   30
c ---[3513]---> BDD-cost:   30
c ---[3512]---> BDD-cost:   30
c ---[3511]---> BDD-cost:   30
c ---[3510]---> BDD-cost:   30
c ---[3509]---> BDD-cost:   30
c ---[3508]---> BDD-cost:   30
c ---[3507]---> BDD-cost:   30
c ---[3506]---> BDD-cost:   30
c ---[3505]---> BDD-cost:   30
c ---[3504]---> BDD-cost:   30
c ---[3503]---> BDD-cost:   30
c ---[3502]---> BDD-cost:   30
c ---[3501]---> BDD-cost:   30
c ---[3500]---> BDD-cost:   30
c ---[3499]---> BDD-cost:   30
c ---[3498]---> BDD-cost:   30
c ---[3497]---> BDD-cost:   30
c ---[3496]---> BDD-cost:   30
c ---[3495]---> BDD-cost:   30
c ---[3494]---> BDD-cost:   30
c ---[3493]---> BDD-cost:   30
c ---[3492]---> BDD-cost:   30
c ---[3491]---> BDD-cost:   30
c ---[3490]---> BDD-cost:   30
c ---[3489]---> BDD-cost:   30
c ---[3488]---> BDD-cost:   30
c ---[3487]---> BDD-cost:   30
c ---[3486]---> BDD-cost:   30
c ---[3485]---> BDD-cost:   30
c ---[3484]---> BDD-cost:   30
c ---[3483]---> BDD-cost:   30
c ---[3482]---> BDD-cost:   30
c ---[3481]---> BDD-cost:   30
c ---[3480]---> BDD-cost:   30
c ---[3479]---> BDD-cost:   30
c ---[3478]---> BDD-cost:   30
c ---[3477]---> BDD-cost:   30
c ---[3476]---> BDD-cost:   30
c ---[3475]---> BDD-cost:   30
c ---[3474]---> BDD-cost:   30
c ---[3473]---> BDD-cost:   30
c ---[3472]---> BDD-cost:   30
c ---[3471]---> BDD-cost:   30
c ---[3470]---> BDD-cost:   30
c ---[3469]---> BDD-cost:   30
c ---[3468]---> BDD-cost:   30
c ---[3467]---> BDD-cost:   30
c ---[3466]---> BDD-cost:   30
c ---[3465]---> BDD-cost:   30
c ---[3464]---> BDD-cost:   30
c ---[3463]---> BDD-cost:   30
c ---[3462]---> BDD-cost:   30
c ---[3461]---> BDD-cost:   30
c ---[3460]---> BDD-cost:   30
c ---[3459]---> BDD-cost:   30
c ---[3458]---> BDD-cost:   30
c ---[3457]---> BDD-cost:   30
c ---[3456]---> BDD-cost:   30
c ---[3455]---> BDD-cost:   30
c ---[3454]---> BDD-cost:   30
c ---[3453]---> BDD-cost:   30
c ---[3452]---> BDD-cost:   30
c ---[3451]---> BDD-cost:   30
c ---[3450]---> BDD-cost:   30
c ---[3449]---> BDD-cost:   30
c ---[3448]---> BDD-cost:   30
c ---[3447]---> BDD-cost:   30
c ---[3446]---> BDD-cost:   30
c ---[3445]---> BDD-cost:   30
c ---[3444]---> BDD-cost:   30
c ---[3443]---> BDD-cost:   30
c ---[3442]---> BDD-cost:   30
c ---[3441]---> BDD-cost:   30
c ---[3440]---> BDD-cost:   30
c ---[3439]---> BDD-cost:   30
c ---[3438]---> BDD-cost:   30
c ---[3437]---> BDD-cost:   30
c ---[3436]---> BDD-cost:   30
c ---[3435]---> BDD-cost:   30
c ---[3434]---> BDD-cost:   30
c ---[3433]---> BDD-cost:   30
c ---[3432]---> BDD-cost:   30
c ---[3431]---> BDD-cost:   30
c ---[3430]---> BDD-cost:   30
c ---[3429]---> BDD-cost:   30
c ---[3428]---> BDD-cost:   30
c ---[3427]---> BDD-cost:   30
c ---[3426]---> BDD-cost:   30
c ---[3425]---> BDD-cost:   30
c ---[3424]---> BDD-cost:   30
c ---[3423]---> BDD-cost:   30
c ---[3422]---> BDD-cost:   30
c ---[3421]---> BDD-cost:   30
c ---[3420]---> BDD-cost:   30
c ---[3419]---> BDD-cost:   30
c ---[3418]---> BDD-cost:   30
c ---[3417]---> BDD-cost:   30
c ---[3416]---> BDD-cost:   30
c ---[3415]---> BDD-cost:   30
c ---[3414]---> BDD-cost:   30
c ---[3413]---> BDD-cost:   30
c ---[3412]---> BDD-cost:   30
c ---[3411]---> BDD-cost:   10
c ---[3410]---> BDD-cost:   10
c ---[3409]---> BDD-cost:   10
c ---[3408]---> BDD-cost:   10
c ---[3407]---> BDD-cost:   10
c ---[3406]---> BDD-cost:   10
c ---[3405]---> BDD-cost:   10
c ---[3404]---> BDD-cost:   10
c ---[3403]---> BDD-cost:   10
c ---[3402]---> BDD-cost:   10
c ---[3401]---> BDD-cost:   10
c ---[3400]---> BDD-cost:   10
c ---[3399]---> BDD-cost:   10
c ---[3398]---> BDD-cost:   10
c ---[3397]---> BDD-cost:   10
c ---[3396]---> BDD-cost:   10
c ---[3395]---> BDD-cost:   10
c ---[3394]---> BDD-cost:   10
c ---[3393]---> BDD-cost:   10
c ---[3392]---> BDD-cost:   10
c ---[3391]---> BDD-cost:   10
c ---[3390]---> BDD-cost:   10
c ---[3389]---> BDD-cost:   10
c ---[3388]---> BDD-cost:   10
c ---[3387]---> BDD-cost:   10
c ---[3386]---> BDD-cost:   10
c ---[3385]---> BDD-cost:   10
c ---[3384]---> BDD-cost:   10
c ---[3383]---> BDD-cost:   10
c ---[3382]---> BDD-cost:   10
c ---[3381]---> BDD-cost:   10
c ---[3380]---> BDD-cost:   10
c ---[3379]---> BDD-cost:   10
c ---[3378]---> BDD-cost:   10
c ---[3377]---> BDD-cost:   10
c ---[3376]---> BDD-cost:   10
c ---[3375]---> BDD-cost:   10
c ---[3374]---> BDD-cost:   10
c ---[3373]---> BDD-cost:   10
c ---[3372]---> BDD-cost:   10
c ---[3371]---> BDD-cost:   10
c ---[3370]---> BDD-cost:   10
c ---[3369]---> BDD-cost:   10
c ---[3368]---> BDD-cost:   10
c ---[3367]---> BDD-cost:   10
c ---[3366]---> BDD-cost:   10
c ---[3365]---> BDD-cost:   10
c ---[3364]---> BDD-cost:   10
c ---[3363]---> BDD-cost:   10
c ---[3362]---> BDD-cost:   10
c ---[3361]---> BDD-cost:   10
c ---[3360]---> BDD-cost:   10
c ---[3359]---> BDD-cost:   10
c ---[3358]---> BDD-cost:   10
c ---[3357]---> BDD-cost:   10
c ---[3356]---> BDD-cost:   10
c ---[3355]---> BDD-cost:   10
c ---[3354]---> BDD-cost:   10
c ---[3353]---> BDD-cost:   10
c ---[3352]---> BDD-cost:   10
c ---[3351]---> BDD-cost:   10
c ---[3350]---> BDD-cost:   10
c ---[3349]---> BDD-cost:   10
c ---[3348]---> BDD-cost:   10
c ---[3347]---> BDD-cost:   10
c ---[3346]---> BDD-cost:   10
c ---[3345]---> BDD-cost:   10
c ---[3344]---> BDD-cost:   10
c ---[3343]---> BDD-cost:   10
c ---[3342]---> BDD-cost:   10
c ---[3341]---> BDD-cost:   10
c ---[3340]---> BDD-cost:   10
c ---[3339]---> BDD-cost:   10
c ---[3338]---> BDD-cost:   10
c ---[3337]---> BDD-cost:   10
c ---[3336]---> BDD-cost:   10
c ---[3335]---> BDD-cost:   10
c ---[3334]---> BDD-cost:   10
c ---[3333]---> BDD-cost:   10
c ---[3332]---> BDD-cost:   10
c ---[3331]---> BDD-cost:   10
c ---[3330]---> BDD-cost:   10
c ---[3329]---> BDD-cost:   10
c ---[3328]---> BDD-cost:   10
c ---[3327]---> BDD-cost:   10
c ---[3326]---> BDD-cost:   10
c ---[3325]---> BDD-cost:   10
c ---[3324]---> BDD-cost:   10
c ---[3323]---> BDD-cost:   10
c ---[3322]---> BDD-cost:   10
c ---[3321]---> BDD-cost:   10
c ---[3320]---> BDD-cost:   10
c ---[3319]---> BDD-cost:   10
c ---[3318]---> BDD-cost:   10
c ---[3317]---> BDD-cost:   10
c ---[3316]---> BDD-cost:   10
c ---[3315]---> BDD-cost:   10
c ---[3314]---> BDD-cost:   10
c ---[3313]---> BDD-cost:   10
c ---[3312]---> BDD-cost:   10
c ---[3311]---> BDD-cost:   10
c ---[3310]---> BDD-cost:   10
c ---[3309]---> BDD-cost:   10
c ---[3308]---> BDD-cost:   10
c ---[3307]---> BDD-cost:   10
c ---[3306]---> BDD-cost:   10
c ---[3305]---> BDD-cost:   10
c ---[3304]---> BDD-cost:   10
c ---[3303]---> BDD-cost:   10
c ---[3302]---> BDD-cost:   10
c ---[3301]---> BDD-cost:   10
c ---[3300]---> BDD-cost:   10
c ---[3299]---> BDD-cost:   10
c ---[3298]---> BDD-cost:   10
c ---[3297]---> BDD-cost:   10
c ---[3296]---> BDD-cost:   10
c ---[3295]---> BDD-cost:   10
c ---[3294]---> BDD-cost:   10
c ---[3293]---> BDD-cost:   10
c ---[3292]---> BDD-cost:   10
c ---[3291]---> BDD-cost:   10
c ---[3290]---> BDD-cost:   10
c ---[3289]---> BDD-cost:   10
c ---[3288]---> BDD-cost:   10
c ---[3287]---> BDD-cost:   10
c ---[3286]---> BDD-cost:   10
c ---[3285]---> BDD-cost:   10
c ---[3284]---> BDD-cost:   10
c ---[3283]---> BDD-cost:   10
c ---[3282]---> BDD-cost:   10

Watcher Data

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/27267/stat): 27267 (minisat+_script) R 27266 27267 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1854655780 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/27267/statm): 174 3 169 147 0 27 0
[pid=27267] 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=27268
New process pid=27269
New process pid=27270
execve syscall for /bin/sed executable
One traced child (pid=27269) 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=27270) exited with status: 0
One traced child (pid=27268) exited with status: 0
New process pid=27271
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-bc1.opb
One traced child (pid=27271) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=27272
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-bc1.opb

[startup+10.0043 s]
Raw data (loadavg): 1.03 0.97 0.91 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 3856 0 3 0 904 16 0 0 25 0 1 0 1854655821 13750272 3155 4294967295 134512640 135167914 3221224448 3221222508 134522361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 3357 3155 162 162 0 3195 0
[pid=27272] vsize: 13428
Current children cumulated CPU time (s) 9.52
Current children cumulated vsize (Kb) 15556

[startup+20.0062 s]
Raw data (loadavg): 1.02 0.97 0.91 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 6631 0 3 0 1873 31 0 0 25 0 1 0 1854655821 21475328 5051 4294967295 134512640 135167914 3221224448 3221220924 134693585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 5243 5051 162 162 0 5081 0
[pid=27272] vsize: 20972
Current children cumulated CPU time (s) 19.36
Current children cumulated vsize (Kb) 23100

[startup+30.0071 s]
Raw data (loadavg): 1.02 0.97 0.91 1/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 9392 0 3 0 2839 49 0 0 25 0 1 0 1854655821 29949952 7122 4294967295 134512640 135167914 3221224448 3221222556 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 7312 7122 162 162 0 7150 0
[pid=27272] vsize: 29248
Current children cumulated CPU time (s) 29.2
Current children cumulated vsize (Kb) 31376

[startup+40.0081 s]
Raw data (loadavg): 1.02 0.97 0.91 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 12176 0 3 0 3809 63 0 0 25 0 1 0 1854655821 37982208 9080 4294967295 134512640 135167914 3221224448 3221222816 134608735 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 9273 9080 162 162 0 9111 0
[pid=27272] vsize: 37092
Current children cumulated CPU time (s) 39.04
Current children cumulated vsize (Kb) 39220

[startup+50.009 s]
Raw data (loadavg): 1.01 0.97 0.91 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 15147 0 3 0 4774 78 0 0 25 0 1 0 1854655821 46833664 11237 4294967295 134512640 135167914 3221224448 3221221072 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27272/statm): 11434 11237 162 162 0 11272 0
[pid=27272] vsize: 45736
Current children cumulated CPU time (s) 48.84
Current children cumulated vsize (Kb) 47864

[startup+60.0099 s]
Raw data (loadavg): 1.09 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 18280 0 3 0 5742 96 0 0 25 0 1 0 1854655821 54595584 13130 4294967295 134512640 135167914 3221224448 3221222448 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 13329 13130 162 162 0 13167 0
[pid=27272] vsize: 53316
Current children cumulated CPU time (s) 58.7
Current children cumulated vsize (Kb) 55444

[startup+70.0109 s]
Raw data (loadavg): 1.08 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 21019 0 3 0 6710 110 0 0 25 0 1 0 1854655821 62480384 15078 4294967295 134512640 135167914 3221224448 3221223120 134849573 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27272/statm): 15254 15078 162 162 0 15092 0
[pid=27272] vsize: 61016
Current children cumulated CPU time (s) 68.52
Current children cumulated vsize (Kb) 63144

[startup+80.0128 s]
Raw data (loadavg): 1.06 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 23946 0 3 0 7681 125 0 0 25 0 1 0 1854655821 70430720 17019 4294967295 134512640 135167914 3221224448 3221223360 134572073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 17195 17019 162 162 0 17033 0
[pid=27272] vsize: 68780
Current children cumulated CPU time (s) 78.38
Current children cumulated vsize (Kb) 70908

[startup+90.0127 s]
Raw data (loadavg): 1.05 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 26953 0 3 0 8650 140 0 0 25 0 1 0 1854655821 78397440 18964 4294967295 134512640 135167914 3221224448 3221223260 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 19140 18964 162 162 0 18978 0
[pid=27272] vsize: 76560
Current children cumulated CPU time (s) 88.22
Current children cumulated vsize (Kb) 78688

[startup+100.014 s]
Raw data (loadavg): 1.04 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 29716 0 3 0 9618 154 0 0 25 0 1 0 1854655821 86568960 20959 4294967295 134512640 135167914 3221224448 3221222784 134694428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 21135 20959 162 162 0 20973 0
[pid=27272] vsize: 84540
Current children cumulated CPU time (s) 98.04
Current children cumulated vsize (Kb) 86668

[startup+110.015 s]
Raw data (loadavg): 1.04 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 32327 0 3 0 10588 167 0 0 25 0 1 0 1854655821 94347264 22857 4294967295 134512640 135167914 3221224448 3221221272 134693704 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 23034 22857 162 162 0 22872 0
[pid=27272] vsize: 92136
Current children cumulated CPU time (s) 107.87
Current children cumulated vsize (Kb) 94264

[startup+120.015 s]
Raw data (loadavg): 1.03 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 35179 0 3 0 11558 183 0 0 25 0 1 0 1854655821 102592512 24864 4294967295 134512640 135167914 3221224448 3221219840 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 25047 24864 162 162 0 24885 0
[pid=27272] vsize: 100188
Current children cumulated CPU time (s) 117.73
Current children cumulated vsize (Kb) 102316

[startup+130.016 s]
Raw data (loadavg): 1.03 0.99 0.92 1/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 37875 0 3 0 12529 198 0 0 25 0 1 0 1854655821 109871104 26645 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 26824 26645 162 162 0 26662 0
[pid=27272] vsize: 107296
Current children cumulated CPU time (s) 127.59
Current children cumulated vsize (Kb) 109424

[startup+140.017 s]
Raw data (loadavg): 1.02 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 40705 0 3 0 13497 213 0 0 25 0 1 0 1854655821 118542336 28757 4294967295 134512640 135167914 3221224448 3221222624 134845937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 28941 28757 162 162 0 28779 0
[pid=27272] vsize: 115764
Current children cumulated CPU time (s) 137.42
Current children cumulated vsize (Kb) 117892

[startup+150.018 s]
Raw data (loadavg): 1.02 0.99 0.92 1/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 43535 0 3 0 14467 227 0 0 25 0 1 0 1854655821 125902848 30562 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 30738 30562 162 162 0 30576 0
[pid=27272] vsize: 122952
Current children cumulated CPU time (s) 147.26
Current children cumulated vsize (Kb) 125080

[startup+160.019 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 46224 0 3 0 15436 241 0 0 25 0 1 0 1854655821 134266880 32596 4294967295 134512640 135167914 3221224448 3221222672 134694392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 32780 32596 162 162 0 32618 0
[pid=27272] vsize: 131120
Current children cumulated CPU time (s) 157.09
Current children cumulated vsize (Kb) 133248

[startup+170.02 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 48857 0 3 0 16408 256 0 0 25 0 1 0 1854655821 141791232 34433 4294967295 134512640 135167914 3221224448 3221222876 134691206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27272/statm): 34617 34433 162 162 0 34455 0
[pid=27272] vsize: 138468
Current children cumulated CPU time (s) 166.96
Current children cumulated vsize (Kb) 140596

[startup+180.021 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 51279 0 3 0 17380 267 0 0 25 0 1 0 1854655821 149782528 36382 4294967295 134512640 135167914 3221224448 3221221452 134722227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 36568 36382 162 162 0 36406 0
[pid=27272] vsize: 146272
Current children cumulated CPU time (s) 176.79
Current children cumulated vsize (Kb) 148400

[startup+190.021 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 54023 0 3 0 18352 281 0 0 25 0 1 0 1854655821 157736960 38326 4294967295 134512640 135167914 3221224448 3221221984 134844708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 38510 38326 162 162 0 38348 0
[pid=27272] vsize: 154040
Current children cumulated CPU time (s) 186.65
Current children cumulated vsize (Kb) 156168

[startup+200.022 s]
Raw data (loadavg): 1.01 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 56264 0 3 0 19323 294 0 0 25 0 1 0 1854655821 165019648 40112 4294967295 134512640 135167914 3221224448 3221222828 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 40288 40112 162 162 0 40126 0
[pid=27272] vsize: 161152
Current children cumulated CPU time (s) 196.49
Current children cumulated vsize (Kb) 163280

[startup+210.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 59022 0 3 0 20293 309 0 0 25 0 1 0 1854655821 172871680 42029 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 42205 42029 162 162 0 42043 0
[pid=27272] vsize: 168820
Current children cumulated CPU time (s) 206.34
Current children cumulated vsize (Kb) 170948

[startup+220.025 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 61666 0 3 0 21262 325 0 0 25 0 1 0 1854655821 180707328 43939 4294967295 134512640 135167914 3221224448 3221222636 134693600 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 44118 43939 162 162 0 43956 0
[pid=27272] vsize: 176472
Current children cumulated CPU time (s) 216.19
Current children cumulated vsize (Kb) 178600

[startup+230.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 64383 0 3 0 22231 339 0 0 25 0 1 0 1854655821 188911616 45936 4294967295 134512640 135167914 3221224448 3221221584 134516620 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 46121 45936 162 162 0 45959 0
[pid=27272] vsize: 184484
Current children cumulated CPU time (s) 226.02
Current children cumulated vsize (Kb) 186612

[startup+240.026 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 67020 0 3 0 23201 353 0 0 25 0 1 0 1854655821 195837952 47635 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 47812 47635 162 162 0 47650 0
[pid=27272] vsize: 191248
Current children cumulated CPU time (s) 235.86
Current children cumulated vsize (Kb) 193376

[startup+250.026 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 69795 0 3 0 24168 367 0 0 25 0 1 0 1854655821 204341248 49703 4294967295 134512640 135167914 3221224448 3221222636 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 49888 49703 162 162 0 49726 0
[pid=27272] vsize: 199552
Current children cumulated CPU time (s) 245.67
Current children cumulated vsize (Kb) 201680

[startup+260.027 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 72465 0 3 0 25139 382 0 0 25 0 1 0 1854655821 211845120 51543 4294967295 134512640 135167914 3221224448 3221222468 134522308 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 51720 51543 162 162 0 51558 0
[pid=27272] vsize: 206880
Current children cumulated CPU time (s) 255.53
Current children cumulated vsize (Kb) 209008

[startup+270.028 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 75180 0 3 0 26104 397 0 0 25 0 1 0 1854655821 219975680 53520 4294967295 134512640 135167914 3221224448 3221220464 134694377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27272/statm): 53705 53520 162 162 0 53543 0
[pid=27272] vsize: 214820
Current children cumulated CPU time (s) 265.33
Current children cumulated vsize (Kb) 216948

[startup+280.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 77778 0 3 0 27074 411 0 0 25 0 1 0 1854655821 227414016 55345 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 55521 55345 162 162 0 55359 0
[pid=27272] vsize: 222084
Current children cumulated CPU time (s) 275.17
Current children cumulated vsize (Kb) 224212

[startup+290.029 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 80548 0 3 0 28040 427 0 0 25 0 1 0 1854655821 235659264 57349 4294967295 134512640 135167914 3221224448 3221221276 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 57534 57349 162 162 0 57372 0
[pid=27272] vsize: 230136
Current children cumulated CPU time (s) 284.99
Current children cumulated vsize (Kb) 232264

[startup+300.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 83191 0 3 0 29008 440 0 0 25 0 1 0 1854655821 243228672 59196 4294967295 134512640 135167914 3221224448 3221220560 134612020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 59382 59196 162 162 0 59220 0
[pid=27272] vsize: 237528
Current children cumulated CPU time (s) 294.8
Current children cumulated vsize (Kb) 239656

[startup+310.031 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 85655 0 3 0 29978 456 0 0 25 0 1 0 1854655821 250691584 61028 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 61204 61028 162 162 0 61042 0
[pid=27272] vsize: 244816
Current children cumulated CPU time (s) 304.66
Current children cumulated vsize (Kb) 246944

[startup+320.031 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 88349 0 3 0 30946 470 0 0 25 0 1 0 1854655821 258781184 62994 4294967295 134512640 135167914 3221224448 3221219552 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 63179 62994 162 162 0 63017 0
[pid=27272] vsize: 252716
Current children cumulated CPU time (s) 314.48
Current children cumulated vsize (Kb) 254844

[startup+330.032 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 90853 0 3 0 31915 484 0 0 25 0 1 0 1854655821 266149888 64800 4294967295 134512640 135167914 3221224448 3221222588 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 64978 64800 162 162 0 64816 0
[pid=27272] vsize: 259912
Current children cumulated CPU time (s) 324.31
Current children cumulated vsize (Kb) 262040

[startup+340.033 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 93475 0 3 0 32887 497 0 0 18 0 1 0 1854655821 274022400 66722 4294967295 134512640 135167914 3221224448 3221222748 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 66900 66723 162 162 0 66738 0
[pid=27272] vsize: 267600
Current children cumulated CPU time (s) 334.16
Current children cumulated vsize (Kb) 269728

[startup+350.034 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 95851 0 3 0 33858 510 0 0 25 0 1 0 1854655821 281649152 68586 4294967295 134512640 135167914 3221224448 3221222784 134845927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 68762 68586 162 162 0 68600 0
[pid=27272] vsize: 275048
Current children cumulated CPU time (s) 344
Current children cumulated vsize (Kb) 277176

[startup+360.035 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 98559 0 3 0 34826 526 0 0 20 0 1 0 1854655821 289538048 70502 4294967295 134512640 135167914 3221224448 3221223120 134843153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 70688 70502 162 162 0 70526 0
[pid=27272] vsize: 282752
Current children cumulated CPU time (s) 353.84
Current children cumulated vsize (Kb) 284880

[startup+370.036 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 101042 0 3 0 35795 542 0 0 25 0 1 0 1854655821 297074688 72350 4294967295 134512640 135167914 3221224448 3221223016 134846907 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27272/statm): 72528 72350 162 162 0 72366 0
[pid=27272] vsize: 290112
Current children cumulated CPU time (s) 363.69
Current children cumulated vsize (Kb) 292240

[startup+380.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 103722 0 3 0 36763 556 0 0 25 0 1 0 1854655821 305188864 74323 4294967295 134512640 135167914 3221224448 3221222776 134693624 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27272/statm): 74509 74323 162 162 0 74347 0
[pid=27272] vsize: 298036
Current children cumulated CPU time (s) 373.51
Current children cumulated vsize (Kb) 300164

[startup+390.038 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 106006 0 3 0 37735 569 0 0 25 0 1 0 1854655821 312602624 76141 4294967295 134512640 135167914 3221224448 3221222884 134849086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 76319 76141 162 162 0 76157 0
[pid=27272] vsize: 305276
Current children cumulated CPU time (s) 383.36
Current children cumulated vsize (Kb) 307404

[startup+400.039 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 108722 0 3 0 38707 582 0 0 25 0 1 0 1854655821 320782336 78130 4294967295 134512640 135167914 3221224448 3221220204 134722660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 78316 78130 162 162 0 78154 0
[pid=27272] vsize: 313264
Current children cumulated CPU time (s) 393.21
Current children cumulated vsize (Kb) 315392

[startup+410.04 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 111245 0 3 0 39676 597 0 0 25 0 1 0 1854655821 328220672 79954 4294967295 134512640 135167914 3221224448 3221220160 134522492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 80132 79954 162 162 0 79970 0
[pid=27272] vsize: 320528
Current children cumulated CPU time (s) 403.05
Current children cumulated vsize (Kb) 322656

[startup+420.04 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 113909 0 3 0 40644 612 0 0 25 0 1 0 1854655821 336166912 81895 4294967295 134512640 135167914 3221224448 3221222556 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 82072 81895 162 162 0 81910 0
[pid=27272] vsize: 328288
Current children cumulated CPU time (s) 412.88
Current children cumulated vsize (Kb) 330416

[startup+430.041 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 116351 0 3 0 41616 625 0 0 25 0 1 0 1854655821 344133632 83840 4294967295 134512640 135167914 3221224448 3221222428 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 84017 83840 162 162 0 83855 0
[pid=27272] vsize: 336068
Current children cumulated CPU time (s) 422.73
Current children cumulated vsize (Kb) 338196

[startup+440.046 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 119018 0 3 0 42580 639 0 0 25 0 1 0 1854655821 352079872 85781 4294967295 134512640 135167914 3221224448 3221221076 134849086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 85957 85781 162 162 0 85795 0
[pid=27272] vsize: 343828
Current children cumulated CPU time (s) 432.51
Current children cumulated vsize (Kb) 345956

[startup+450.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 121610 0 3 0 43551 652 0 0 25 0 1 0 1854655821 360013824 87718 4294967295 134512640 135167914 3221224448 3221222160 134845933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 87894 87718 162 162 0 87732 0
[pid=27272] vsize: 351576
Current children cumulated CPU time (s) 442.35
Current children cumulated vsize (Kb) 353704

[startup+460.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 124207 0 3 0 44521 665 0 0 25 0 1 0 1854655821 367595520 89566 4294967295 134512640 135167914 3221224448 3221220844 134693600 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 89745 89566 162 162 0 89583 0
[pid=27272] vsize: 358980
Current children cumulated CPU time (s) 452.18
Current children cumulated vsize (Kb) 361108

[startup+470.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 126769 0 3 0 45490 679 0 0 25 0 1 0 1854655821 375701504 91547 4294967295 134512640 135167914 3221224448 3221220912 134522492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 91724 91547 162 162 0 91562 0
[pid=27272] vsize: 366896
Current children cumulated CPU time (s) 462.01
Current children cumulated vsize (Kb) 369024

[startup+480.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 129454 0 3 0 46459 696 0 0 25 0 1 0 1854655821 383918080 93554 4294967295 134512640 135167914 3221224448 3221222496 134522195 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 93730 93554 162 162 0 93568 0
[pid=27272] vsize: 374920
Current children cumulated CPU time (s) 471.87
Current children cumulated vsize (Kb) 377048

[startup+490.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137239 0 3 0 47376 733 0 0 25 0 1 0 1854655821 413872128 100871 4294967295 134512640 135167914 3221224448 3221223268 134522233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27272/statm): 101043 100871 162 162 0 100881 0
[pid=27272] vsize: 404172
Current children cumulated CPU time (s) 481.41
Current children cumulated vsize (Kb) 406300

[startup+500.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137239 0 3 0 48375 733 0 0 25 0 1 0 1854655821 413872128 100871 4294967295 134512640 135167914 3221224448 3221223296 134594254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101043 100871 162 162 0 100881 0
[pid=27272] vsize: 404172
Current children cumulated CPU time (s) 491.4
Current children cumulated vsize (Kb) 406300

[startup+510.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137239 0 3 0 49375 733 0 0 25 0 1 0 1854655821 413872128 100871 4294967295 134512640 135167914 3221224448 3221223204 134697155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101043 100871 162 162 0 100881 0
[pid=27272] vsize: 404172
Current children cumulated CPU time (s) 501.4
Current children cumulated vsize (Kb) 406300

[startup+520.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137239 0 3 0 50375 733 0 0 25 0 1 0 1854655821 413872128 100871 4294967295 134512640 135167914 3221224448 3221223268 134522188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101043 100871 162 162 0 100881 0
[pid=27272] vsize: 404172
Current children cumulated CPU time (s) 511.4
Current children cumulated vsize (Kb) 406300

[startup+530.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137240 0 3 0 51375 733 0 0 25 0 1 0 1854655821 413876224 100872 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101044 100872 162 162 0 100882 0
[pid=27272] vsize: 404176
Current children cumulated CPU time (s) 521.4
Current children cumulated vsize (Kb) 406304

[startup+540.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137240 0 3 0 52375 733 0 0 25 0 1 0 1854655821 413876224 100872 4294967295 134512640 135167914 3221224448 3221223264 134691205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101044 100872 162 162 0 100882 0
[pid=27272] vsize: 404176
Current children cumulated CPU time (s) 531.4
Current children cumulated vsize (Kb) 406304

[startup+550.053 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137240 0 3 0 53376 733 0 0 25 0 1 0 1854655821 413876224 100872 4294967295 134512640 135167914 3221224448 3221223264 134522227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101044 100872 162 162 0 100882 0
[pid=27272] vsize: 404176
Current children cumulated CPU time (s) 541.41
Current children cumulated vsize (Kb) 406304

[startup+560.054 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137240 0 3 0 54376 733 0 0 25 0 1 0 1854655821 413876224 100872 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101044 100872 162 162 0 100882 0
[pid=27272] vsize: 404176
Current children cumulated CPU time (s) 551.41
Current children cumulated vsize (Kb) 406304

[startup+570.055 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137240 0 3 0 55376 733 0 0 25 0 1 0 1854655821 413876224 100872 4294967295 134512640 135167914 3221224448 3221223264 134691205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101044 100872 162 162 0 100882 0
[pid=27272] vsize: 404176
Current children cumulated CPU time (s) 561.41
Current children cumulated vsize (Kb) 406304

[startup+580.056 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137240 0 3 0 56376 733 0 0 25 0 1 0 1854655821 413876224 100872 4294967295 134512640 135167914 3221224448 3221223208 134697190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101044 100872 162 162 0 100882 0
[pid=27272] vsize: 404176
Current children cumulated CPU time (s) 571.41
Current children cumulated vsize (Kb) 406304

[startup+590.056 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137240 0 3 0 57376 733 0 0 25 0 1 0 1854655821 413876224 100872 4294967295 134512640 135167914 3221224448 3221223296 134594196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101044 100872 162 162 0 100882 0
[pid=27272] vsize: 404176
Current children cumulated CPU time (s) 581.41
Current children cumulated vsize (Kb) 406304

[startup+600.057 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137240 0 3 0 58377 733 0 0 25 0 1 0 1854655821 413876224 100872 4294967295 134512640 135167914 3221224448 3221223216 134691401 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101044 100872 162 162 0 100882 0
[pid=27272] vsize: 404176
Current children cumulated CPU time (s) 591.42
Current children cumulated vsize (Kb) 406304

[startup+610.058 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137240 0 3 0 59377 733 0 0 25 0 1 0 1854655821 413876224 100872 4294967295 134512640 135167914 3221224448 3221223264 134522192 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101044 100872 162 162 0 100882 0
[pid=27272] vsize: 404176
Current children cumulated CPU time (s) 601.42
Current children cumulated vsize (Kb) 406304

[startup+620.059 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137240 0 3 0 60377 733 0 0 25 0 1 0 1854655821 413876224 100872 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101044 100872 162 162 0 100882 0
[pid=27272] vsize: 404176
Current children cumulated CPU time (s) 611.42
Current children cumulated vsize (Kb) 406304

[startup+630.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137240 0 3 0 61377 733 0 0 25 0 1 0 1854655821 413876224 100872 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101044 100872 162 162 0 100882 0
[pid=27272] vsize: 404176
Current children cumulated CPU time (s) 621.42
Current children cumulated vsize (Kb) 406304

[startup+640.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 62377 733 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 631.42
Current children cumulated vsize (Kb) 406308

[startup+650.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 63378 733 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 641.43
Current children cumulated vsize (Kb) 406308

[startup+660.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 64378 733 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223264 134522192 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 651.43
Current children cumulated vsize (Kb) 406308

[startup+670.063 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 65378 733 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223276 134691389 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 661.43
Current children cumulated vsize (Kb) 406308

[startup+680.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 66378 733 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223288 134596362 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 671.43
Current children cumulated vsize (Kb) 406308

[startup+690.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 67378 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 681.44
Current children cumulated vsize (Kb) 406308

[startup+700.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 68379 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 691.45
Current children cumulated vsize (Kb) 406308

[startup+710.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 69379 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 701.45
Current children cumulated vsize (Kb) 406308

[startup+720.066 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 70379 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223280 134596368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 711.45
Current children cumulated vsize (Kb) 406308

[startup+730.067 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 71379 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 721.45
Current children cumulated vsize (Kb) 406308

[startup+740.068 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 72379 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691401 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 731.45
Current children cumulated vsize (Kb) 406308

[startup+750.069 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 73379 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223280 134596368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 741.45
Current children cumulated vsize (Kb) 406308

[startup+760.07 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 74380 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223208 134697041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 751.46
Current children cumulated vsize (Kb) 406308

[startup+770.071 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 75380 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223204 134697161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 761.46
Current children cumulated vsize (Kb) 406308

[startup+780.072 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 76380 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 771.46
Current children cumulated vsize (Kb) 406308

[startup+790.072 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 77380 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 781.46
Current children cumulated vsize (Kb) 406308

[startup+800.072 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 78380 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223280 134596368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 791.46
Current children cumulated vsize (Kb) 406308

[startup+810.073 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 79381 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223288 134596334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 801.47
Current children cumulated vsize (Kb) 406308

[startup+820.073 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 80381 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223280 134596345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 811.47
Current children cumulated vsize (Kb) 406308

[startup+830.074 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 81381 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 821.47
Current children cumulated vsize (Kb) 406308

[startup+840.075 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 82381 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223276 134691200 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 831.47
Current children cumulated vsize (Kb) 406308

[startup+850.076 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 83381 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223204 134697161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 841.47
Current children cumulated vsize (Kb) 406308

[startup+860.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 84381 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 851.47
Current children cumulated vsize (Kb) 406308

[startup+870.077 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 85382 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 861.48
Current children cumulated vsize (Kb) 406308

[startup+880.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 86382 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223204 134697161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 871.48
Current children cumulated vsize (Kb) 406308

[startup+890.078 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 87382 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223296 134594254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 881.48
Current children cumulated vsize (Kb) 406308

[startup+900.079 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 88382 734 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 891.48
Current children cumulated vsize (Kb) 406308

[startup+910.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 89382 735 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691394 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 901.49
Current children cumulated vsize (Kb) 406308

[startup+920.081 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 90383 735 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 911.5
Current children cumulated vsize (Kb) 406308

[startup+930.082 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 91383 735 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 921.5
Current children cumulated vsize (Kb) 406308

[startup+940.081 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 92383 735 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 931.5
Current children cumulated vsize (Kb) 406308

[startup+950.083 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 93383 735 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223280 134596347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 941.5
Current children cumulated vsize (Kb) 406308

[startup+960.084 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 94383 735 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223276 134691389 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 951.5
Current children cumulated vsize (Kb) 406308

[startup+970.084 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 95383 735 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223276 134691200 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 961.5
Current children cumulated vsize (Kb) 406308

[startup+980.086 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 96384 735 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223264 134691205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 971.51
Current children cumulated vsize (Kb) 406308

[startup+990.086 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 97384 735 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 981.51
Current children cumulated vsize (Kb) 406308

[startup+1000.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 98384 735 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223296 134596417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 991.51
Current children cumulated vsize (Kb) 406308

[startup+1010.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137241 0 3 0 99384 735 0 0 25 0 1 0 1854655821 413880320 100873 4294967295 134512640 135167914 3221224448 3221223268 134522188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101045 100873 162 162 0 100883 0
[pid=27272] vsize: 404180
Current children cumulated CPU time (s) 1001.51
Current children cumulated vsize (Kb) 406308

[startup+1020.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137242 0 3 0 100385 735 0 0 25 0 1 0 1854655821 413884416 100874 4294967295 134512640 135167914 3221224448 3221223276 134522184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101046 100874 162 162 0 100884 0
[pid=27272] vsize: 404184
Current children cumulated CPU time (s) 1011.52
Current children cumulated vsize (Kb) 406312

[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137242 0 3 0 101385 735 0 0 25 0 1 0 1854655821 413884416 100874 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101046 100874 162 162 0 100884 0
[pid=27272] vsize: 404184
Current children cumulated CPU time (s) 1021.52
Current children cumulated vsize (Kb) 406312

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137242 0 3 0 102385 735 0 0 25 0 1 0 1854655821 413884416 100874 4294967295 134512640 135167914 3221224448 3221223204 134697152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101046 100874 162 162 0 100884 0
[pid=27272] vsize: 404184
Current children cumulated CPU time (s) 1031.52
Current children cumulated vsize (Kb) 406312

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137242 0 3 0 103385 735 0 0 25 0 1 0 1854655821 413884416 100874 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101046 100874 162 162 0 100884 0
[pid=27272] vsize: 404184
Current children cumulated CPU time (s) 1041.52
Current children cumulated vsize (Kb) 406312

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137242 0 3 0 104385 735 0 0 25 0 1 0 1854655821 413884416 100874 4294967295 134512640 135167914 3221224448 3221223204 134697155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101046 100874 162 162 0 100884 0
[pid=27272] vsize: 404184
Current children cumulated CPU time (s) 1051.52
Current children cumulated vsize (Kb) 406312

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137242 0 3 0 105386 735 0 0 25 0 1 0 1854655821 413884416 100874 4294967295 134512640 135167914 3221224448 3221223204 134697170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101046 100874 162 162 0 100884 0
[pid=27272] vsize: 404184
Current children cumulated CPU time (s) 1061.53
Current children cumulated vsize (Kb) 406312

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137242 0 3 0 106386 735 0 0 25 0 1 0 1854655821 413216768 100711 4294967295 134512640 135167914 3221224448 3221223200 134691218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 100883 100711 162 162 0 100721 0
[pid=27272] vsize: 403532
Current children cumulated CPU time (s) 1071.53
Current children cumulated vsize (Kb) 405660

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137406 0 3 0 107385 736 0 0 25 0 1 0 1854655821 413843456 100875 4294967295 134512640 135167914 3221224448 3221220400 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27272/statm): 101036 100875 162 162 0 100874 0
[pid=27272] vsize: 404144
Current children cumulated CPU time (s) 1081.53
Current children cumulated vsize (Kb) 406272

[startup+1100.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 137419 0 3 0 108385 736 0 0 25 0 1 0 1854655821 413843456 100888 4294967295 134512640 135167914 3221224448 3220646328 134722513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 101036 100888 162 162 0 100874 0
[pid=27272] vsize: 404144
Current children cumulated CPU time (s) 1091.53
Current children cumulated vsize (Kb) 406272

[startup+1110.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 139706 0 3 0 109372 743 0 0 25 0 1 0 1854655821 423211008 103175 4294967295 134512640 135167914 3221224448 3220646008 134694481 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 103323 103175 162 162 0 103161 0
[pid=27272] vsize: 413292
Current children cumulated CPU time (s) 1101.47
Current children cumulated vsize (Kb) 415420

[startup+1120.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 145287 0 3 0 110334 762 0 0 25 0 1 0 1854655821 446070784 108756 4294967295 134512640 135167914 3221224448 3220646108 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 108904 108756 162 162 0 108742 0
[pid=27272] vsize: 435616
Current children cumulated CPU time (s) 1111.28
Current children cumulated vsize (Kb) 437744

[startup+1130.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 148015 0 3 0 111303 774 0 0 25 0 1 0 1854655821 451846144 110166 4294967295 134512640 135167914 3221224448 3220649984 134696128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 110314 110166 162 162 0 110152 0
[pid=27272] vsize: 441256
Current children cumulated CPU time (s) 1121.09
Current children cumulated vsize (Kb) 443384

[startup+1140.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 150780 0 3 0 112276 786 0 0 25 0 1 0 1854655821 463171584 112931 4294967295 134512640 135167914 3221224448 3220645448 134849057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 113079 112931 162 162 0 112917 0
[pid=27272] vsize: 452316
Current children cumulated CPU time (s) 1130.94
Current children cumulated vsize (Kb) 454444

[startup+1150.1 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 153599 0 3 0 113246 799 0 0 25 0 1 0 1854655821 474718208 115750 4294967295 134512640 135167914 3221224448 3220645596 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 115898 115750 162 162 0 115736 0
[pid=27272] vsize: 463592
Current children cumulated CPU time (s) 1140.77
Current children cumulated vsize (Kb) 465720

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 160705 0 3 0 114215 820 0 0 25 0 1 0 1854655821 493023232 120219 4294967295 134512640 135167914 3221224448 3220646016 134844672 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 120367 120219 162 162 0 120205 0
[pid=27272] vsize: 481468
Current children cumulated CPU time (s) 1150.67
Current children cumulated vsize (Kb) 483596

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 163107 0 3 0 115188 831 0 0 25 0 1 0 1854655821 502861824 122621 4294967295 134512640 135167914 3221224448 3220649752 134697190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27272/statm): 122769 122621 162 162 0 122607 0
[pid=27272] vsize: 491076
Current children cumulated CPU time (s) 1160.51
Current children cumulated vsize (Kb) 493204

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 165489 0 3 0 116161 842 0 0 25 0 1 0 1854655821 512618496 125003 4294967295 134512640 135167914 3221224448 3220647040 134624231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 125151 125003 162 162 0 124989 0
[pid=27272] vsize: 500604
Current children cumulated CPU time (s) 1170.35
Current children cumulated vsize (Kb) 502732

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 168004 0 3 0 117135 852 0 0 25 0 1 0 1854655821 522919936 127518 4294967295 134512640 135167914 3221224448 3220649216 134844866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 127666 127518 162 162 0 127504 0
[pid=27272] vsize: 510664
Current children cumulated CPU time (s) 1180.19
Current children cumulated vsize (Kb) 512792

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 170595 0 3 0 118106 864 0 0 25 0 1 0 1854655821 533532672 130109 4294967295 134512640 135167914 3221224448 3220649340 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 130257 130109 162 162 0 130095 0
[pid=27272] vsize: 521028
Current children cumulated CPU time (s) 1190.02
Current children cumulated vsize (Kb) 523156

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) R 27267 27267 31027 0 -1 0 172957 0 3 0 119080 875 0 0 25 0 1 0 1854655821 543207424 132471 4294967295 134512640 135167914 3221224448 3220648512 134844708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27272/statm): 132619 132471 162 162 0 132457 0
[pid=27272] vsize: 530476
Current children cumulated CPU time (s) 1199.87
Current children cumulated vsize (Kb) 532604

[startup+1220.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 174915 0 3 0 120061 882 0 0 25 0 1 0 1854655821 551227392 134429 4294967295 134512640 135167914 3221224448 3220648092 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 134577 134429 162 162 0 134415 0
[pid=27272] vsize: 538308
Current children cumulated CPU time (s) 1209.75
Current children cumulated vsize (Kb) 540436



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1220.1 s]
Raw data (loadavg): 1.00 0.99 0.92 1/57 27272
Raw data (/proc/27267/stat): 27267 (minisat+_script) S 27266 27267 31027 0 -1 0 313 1605 1 0 0 1 25 6 18 0 1 0 1854655780 2179072 234 4294967295 134512640 135087896 3221224512 3221223400 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27267/statm): 532 234 485 147 0 385 0
[pid=27267] vsize: 2128
Raw data (/proc/27272/stat): 27272 (minisat+_bignum) T 27267 27267 31027 0 -1 0 174915 0 3 0 120061 882 0 0 25 0 1 0 1854655821 551227392 134429 4294967295 134512640 135167914 3221224448 3220648092 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/27272/statm): 134577 134429 162 162 0 134415 0
[pid=27272] vsize: 538308
Current children cumulated CPU time (s) 1209.75
Current children cumulated vsize (Kb) 540436

Sending SIGTERM to -27267
Sleeping 2 seconds
One traced child (pid=27267) ended because it received signal 15 (SIGTERM)
One traced child (pid=27272) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1220.35
CPU time (s): 1209.68
CPU user time (s): 1200.61
CPU system time (s): 9.07262
CPU usage (%): 99.1257
Max. virtual memory (cumulated for all children) (Kb): 540436

Verifier Data

ERROR: no interpretation found !