Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-greenbea.opb |
MD5SUM | 9328ce67cb4db3dffdeb7eebb9aea072 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 15205 |
Biggest coefficient in the objective function | 536870912000000 |
Number of bits for the biggest coefficient in the objective function | 49 |
Sum of the numbers in the objective function | 11303756896327816 |
Number of bits of the sum of numbers in the objective function | 54 |
Biggest number in a constraint | 536870912000000 |
Number of bits of the biggest number in a constraint | 49 |
Biggest sum of numbers in a constraint | 24454743822989865 |
Number of bits of the biggest sum of numbers | 55 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 155427 |
Total number of constraints | 2675 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 2675 |
Minimum length of a constraint | 11 |
Maximum length of a constraint | 7267 |
LAUNCH ON wulflinc11 THE 2005-09-18 20:18:22 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2779 boxname=wulflinc11 idbench=435 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 9328ce67cb4db3dffdeb7eebb9aea072 /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-greenbea.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-greenbea.opb IDLAUNCH: 2779 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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: 895660 kB Buffers: 32844 kB Cached: 78148 kB SwapCached: 732 kB Active: 72640 kB Inactive: 40920 kB HighTotal: 131008 kB HighFree: 51072 kB LowTotal: 903652 kB LowFree: 844588 kB SwapTotal: 2097136 kB SwapFree: 2095856 kB Dirty: 12 kB Writeback: 0 kB Mapped: 5716 kB Slab: 19708 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 20:38:33 (client local time) WITH STATUS 0 IN 1208.34 SECONDS stats: 2779 7 1208.34 0
c Parsing PB file... c PARSE ERROR! [line 5409] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 4200 PB-constraints to clauses... c -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ###################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################### c -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssss c ---[4242]---> BDD-cost: 20 c ---[4237]---> BDD-cost: 18 c ---[4236]---> BDD-cost: 17 c ---[4235]---> BDD-cost: 21 c ---[4234]---> BDD-cost: 18 c ---[4232]---> BDD-cost: 17 c ---[4231]---> BDD-cost: 19 c ---[4230]---> BDD-cost: 16 c ---[4229]---> BDD-cost: 16 c ---[4228]---> BDD-cost: 14 c ---[4227]---> BDD-cost: 16 c ---[4225]---> BDD-cost: 16 c ---[4224]---> BDD-cost: 17 c ---[4222]---> BDD-cost: 15 c ---[4221]---> BDD-cost: 11 c ---[4220]---> BDD-cost: 15 c ---[4219]---> BDD-cost: 15 c ---[4218]---> BDD-cost: 12 c ---[4216]---> BDD-cost: 16 c ---[4213]---> BDD-cost: 13 c ---[4212]---> BDD-cost: 18 c ---[4209]---> BDD-cost: 12 c ---[4208]---> BDD-cost: 19 c ---[4207]---> BDD-cost: 15 c ---[4206]---> BDD-cost: 17 c ---[4205]---> BDD-cost: 17 c ---[4204]---> BDD-cost: 15 c ---[4203]---> BDD-cost: 18 c ---[4202]---> BDD-cost: 15 c ---[4201]---> BDD-cost: 16 c ---[4200]---> BDD-cost: 11 c ---[4198]---> BDD-cost: 15 c ---[4197]---> BDD-cost: 14 c ---[4196]---> BDD-cost: 13 c ---[4195]---> BDD-cost: 15 c ---[4194]---> BDD-cost: 17 c ---[4191]---> BDD-cost: 22 c ---[4190]---> BDD-cost: 16 c ---[4189]---> BDD-cost: 19 c ---[4187]---> BDD-cost: 19 c ---[4185]---> BDD-cost: 20 c ---[4184]---> BDD-cost: 18 c ---[4183]---> BDD-cost: 18 c ---[4182]---> BDD-cost: 16 c ---[4181]---> BDD-cost: 20 c ---[4180]---> BDD-cost: 19 c ---[4179]---> BDD-cost: 19 c ---[4178]---> BDD-cost: 18 c ---[4177]---> BDD-cost: 17 c ---[4176]---> BDD-cost: 10 c ---[4175]---> BDD-cost: 14 c ---[4174]---> BDD-cost: 18 c ---[4173]---> BDD-cost: 10 c ---[4172]---> BDD-cost: 15 c ---[4171]---> BDD-cost: 15 c ---[4170]---> BDD-cost: 11 c ---[4169]---> BDD-cost: 14 c ---[4168]---> BDD-cost: 17 c ---[4165]---> BDD-cost: 20 c ---[4164]---> BDD-cost: 23 c ---[4163]---> BDD-cost: 17 c ---[4162]---> BDD-cost: 16 c ---[4161]---> BDD-cost: 20 c ---[4159]---> BDD-cost: 12 c ---[4158]---> BDD-cost: 20 c ---[4157]---> BDD-cost: 14 c ---[4156]---> BDD-cost: 21 c ---[4155]---> BDD-cost: 18 c ---[4154]---> BDD-cost: 19 c ---[4153]---> BDD-cost: 19 c ---[4152]---> BDD-cost: 19 c ---[4150]---> BDD-cost: 20 c ---[4149]---> BDD-cost: 18 c ---[4148]---> BDD-cost: 18 c ---[4147]---> BDD-cost: 10 c ---[4146]---> BDD-cost: 14 c ---[4144]---> BDD-cost: 10 c ---[4143]---> BDD-cost: 17 c ---[4142]---> BDD-cost: 16 c ---[4141]---> BDD-cost: 10 c ---[4140]---> BDD-cost: 15 c ---[4137]---> BDD-cost: 17 c ---[4136]---> BDD-cost: 18 c ---[4135]---> BDD-cost: 22 c ---[4134]---> BDD-cost: 19 c ---[4133]---> BDD-cost: 19 c ---[4131]---> BDD-cost: 18 c ---[4130]---> BDD-cost: 20 c ---[4129]---> BDD-cost: 14 c ---[4128]---> BDD-cost: 19 c ---[4127]---> BDD-cost: 19 c ---[4125]---> BDD-cost: 18 c ---[4123]---> BDD-cost: 18 c ---[4122]---> BDD-cost: 18 c ---[4121]---> BDD-cost: 19 c ---[4120]---> BDD-cost: 19 c ---[4119]---> BDD-cost: 15 c ---[4118]---> BDD-cost: 19 c ---[4117]---> BDD-cost: 18 c ---[4116]---> BDD-cost: 15 c ---[4115]---> BDD-cost: 15 c ---[4114]---> BDD-cost: 14 c ---[4112]---> BDD-cost: 15 c ---[4111]---> BDD-cost: 14 c ---[4110]---> BDD-cost: 15 c ---[4109]---> BDD-cost: 14 c ---[4108]---> BDD-cost: 15 c ---[4107]---> BDD-cost: 15 c ---[4106]---> BDD-cost: 15 c ---[4105]---> BDD-cost: 16 c ---[4104]---> BDD-cost: 15 c ---[4103]---> BDD-cost: 18 c ---[4102]---> BDD-cost: 22 c ---[4099]---> BDD-cost: 18 c ---[4098]---> BDD-cost: 18 c ---[4095]---> BDD-cost: 19 c ---[4094]---> BDD-cost: 18 c ---[4093]---> BDD-cost: 19 c ---[4092]---> BDD-cost: 19 c ---[4091]---> BDD-cost: 20 c ---[4089]---> BDD-cost: 17 c ---[4088]---> BDD-cost: 16 c ---[4087]---> BDD-cost: 17 c ---[4086]---> BDD-cost: 15 c ---[4084]---> BDD-cost: 14 c ---[4082]---> BDD-cost: 15 c ---[4081]---> BDD-cost: 17 c ---[4080]---> BDD-cost: 16 c ---[4079]---> BDD-cost: 15 c ---[4078]---> BDD-cost: 18 c ---[4077]---> BDD-cost: 15 c ---[4075]---> BDD-cost: 14 c ---[4074]---> BDD-cost: 14 c ---[4072]---> BDD-cost: 13 c ---[4067]---> BDD-cost: 15 c ---[4066]---> BDD-cost: 19 c ---[4064]---> BDD-cost: 17 c ---[4062]---> BDD-cost: 16 c ---[4061]---> BDD-cost: 18 c ---[4059]---> BDD-cost: 19 c ---[4058]---> BDD-cost: 13 c ---[4056]---> BDD-cost: 19 c ---[4055]---> BDD-cost: 19 c ---[4054]---> BDD-cost: 19 c ---[4052]---> BDD-cost: 16 c ---[4051]---> BDD-cost: 21 c ---[4050]---> BDD-cost: 17 c ---[4049]---> BDD-cost: 15 c ---[4048]---> BDD-cost: 14 c ---[4047]---> BDD-cost: 16 c ---[4046]---> BDD-cost: 10 c ---[4045]---> BDD-cost: 17 c ---[4044]---> BDD-cost: 16 c ---[4043]---> BDD-cost: 12 c ---[4042]---> BDD-cost: 12 c ---[4041]---> BDD-cost: 16 c ---[4040]---> BDD-cost: 17 c ---[4039]---> BDD-cost: 20 c ---[4037]---> BDD-cost: 14 c ---[4036]---> BDD-cost: 15 c ---[4035]---> BDD-cost: 18 c ---[4034]---> BDD-cost: 22 c ---[4033]---> BDD-cost: 23 c ---[4031]---> BDD-cost: 18 c ---[4030]---> BDD-cost: 19 c ---[4029]---> BDD-cost: 21 c ---[4027]---> BDD-cost: 21 c ---[4026]---> BDD-cost: 16 c ---[4025]---> BDD-cost: 21 c ---[4022]---> BDD-cost: 19 c ---[4021]---> BDD-cost: 18 c ---[4020]---> BDD-cost: 21 c ---[4019]---> BDD-cost: 20 c ---[4017]---> BDD-cost: 15 c ---[4016]---> BDD-cost: 18 c ---[4015]---> BDD-cost: 10 c ---[4014]---> BDD-cost: 18 c ---[4013]---> BDD-cost: 16 c ---[4012]---> BDD-cost: 15 c ---[4011]---> BDD-cost: 14 c ---[4010]---> BDD-cost: 16 c ---[4009]---> BDD-cost: 22 c ---[4008]---> BDD-cost: 19 c ---[4005]---> BDD-cost: 19 c ---[4004]---> BDD-cost: 21 c ---[4003]---> BDD-cost: 17 c ---[4002]---> BDD-cost: 18 c ---[4001]---> BDD-cost: 18 c ---[4000]---> BDD-cost: 19 c ---[3998]---> BDD-cost: 19 c ---[3997]---> BDD-cost: 13 c ---[3996]---> BDD-cost: 18 c ---[3995]---> BDD-cost: 18 c ---[3993]---> BDD-cost: 15 c ---[3992]---> BDD-cost: 16 c ---[3991]---> BDD-cost: 20 c ---[3989]---> BDD-cost: 14 c ---[3988]---> BDD-cost: 14 c ---[3987]---> BDD-cost: 13 c ---[3986]---> BDD-cost: 10 c ---[3985]---> BDD-cost: 16 c ---[3984]---> BDD-cost: 14 c ---[3983]---> BDD-cost: 11 c ---[3982]---> BDD-cost: 12 c ---[3981]---> BDD-cost: 14 c ---[3975]---> BDD-cost: 20 c ---[3974]---> BDD-cost: 16 c ---[3972]---> BDD-cost: 15 c ---[3970]---> BDD-cost: 18 c ---[3968]---> BDD-cost: 14 c ---[3967]---> BDD-cost: 10 c ---[3966]---> BDD-cost: 11 c ---[3965]---> BDD-cost: 16 c ---[3964]---> BDD-cost: 14 c ---[3963]---> BDD-cost: 17 c ---[3961]---> BDD-cost: 14 c ---[3960]---> BDD-cost: 13 c ---[3958]---> BDD-cost: 12 c ---[3956]---> BDD-cost: 16 c ---[3953]---> BDD-cost: 20 c ---[3951]---> Sorter-cost: 2252 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3949]---> Adder-cost: 689 maxlim: 2484224 bits: 23/22 c ---[3947]---> Adder-cost: 1287 maxlim: 1075358719 bits: 32/31 c ---[3945]---> Adder-cost: 689 maxlim: 2380800 bits: 23/22 c ---[3943]---> Adder-cost: 354 maxlim: 585728 bits: 21/20 c ---[3941]---> Adder-cost: 625 maxlim: 870400 bits: 21/20 c ---[3939]---> Sorter-cost: 3809 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3937]---> Sorter-cost: 2519 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3935]---> Adder-cost: 336 maxlim: 437248 bits: 20/19 c ---[3933]---> Adder-cost: 354 maxlim: 781312 bits: 21/20 c ---[3931]---> BDD-cost: 214 c ---[3929]---> Adder-cost: 354 maxlim: 631808 bits: 21/20 c ---[3927]---> Sorter-cost: 441 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3925]---> BDD-cost: 85 c ---[3923]---> Adder-cost: 336 maxlim: 510976 bits: 20/19 c ---[3921]---> Adder-cost: 689 maxlim: 3631104 bits: 23/22 c ---[3919]---> Adder-cost: 689 maxlim: 2393088 bits: 23/22 c ---[3917]---> BDD-cost: 88 c ---[3915]---> Sorter-cost: 1823 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3913]---> Adder-cost: 657 maxlim: 1985536 bits: 22/21 c ---[3911]---> Sorter-cost: 1282 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3909]---> Adder-cost: 689 maxlim: 2569216 bits: 23/22 c ---[3907]---> BDD-cost: 100 c ---[3905]---> Sorter-cost: 3435 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3903]---> Adder-cost: 413 maxlim: 1757184 bits: 22/21 c ---[3901]---> Sorter-cost: 3591 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3899]---> Adder-cost: 354 maxlim: 701440 bits: 21/20 c ---[3897]---> Sorter-cost: 590 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3895]---> Adder-cost: 447 maxlim: 481280 bits: 20/19 c ---[3893]---> BDD-cost: 90 c ---[3891]---> Adder-cost: 372 maxlim: 1053696 bits: 22/21 c ---[3889]---> Sorter-cost: 1282 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3887]---> Sorter-cost: 1646 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3885]---> Sorter-cost: 2519 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[3883]---> BDD-cost: 90 c --
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/17698/stat): 17698 (minisat+_script) R 17697 17698 9854 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785844897 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/17698/statm): 174 3 169 147 0 27 0 [pid=17698] 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=17699 New process pid=17700 New process pid=17701 execve syscall for /bin/sed executable One traced child (pid=17700) 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=17701) exited with status: 0 One traced child (pid=17699) exited with status: 0 New process pid=17702 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-greenbea.opb One traced child (pid=17702) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=17703 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-greenbea.opb [startup+10.0041 s] Raw data (loadavg): 0.86 0.93 0.95 1/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) T 17698 17698 9854 0 -1 0 5251 0 3 0 926 27 0 0 25 0 1 0 1785844906 23871488 4935 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/17703/statm): 5828 4935 162 162 0 5666 0 [pid=17703] vsize: 23312 Current children cumulated CPU time (s) 9.56 Current children cumulated vsize (Kb) 25440 [startup+20.0059 s] Raw data (loadavg): 0.88 0.93 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 8119 0 3 0 1889 43 0 0 25 0 1 0 1785844906 34369536 7803 4294967295 134512640 135167914 3221224448 3221222784 134849068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 8391 7803 162 162 0 8229 0 [pid=17703] vsize: 33564 Current children cumulated CPU time (s) 19.35 Current children cumulated vsize (Kb) 35692 [startup+30.0067 s] Raw data (loadavg): 0.90 0.93 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) T 17698 17698 9854 0 -1 0 10848 0 3 0 2853 61 0 0 25 0 1 0 1785844906 44281856 10532 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/17703/statm): 10811 10532 162 162 0 10649 0 [pid=17703] vsize: 43244 Current children cumulated CPU time (s) 29.17 Current children cumulated vsize (Kb) 45372 [startup+40.0075 s] Raw data (loadavg): 0.92 0.93 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 13419 0 3 0 3818 78 0 0 25 0 1 0 1785844906 62816256 13103 4294967295 134512640 135167914 3221224448 3221219964 134845940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 15336 13103 162 162 0 15174 0 [pid=17703] vsize: 61344 Current children cumulated CPU time (s) 38.99 Current children cumulated vsize (Kb) 63472 [startup+50.0082 s] Raw data (loadavg): 0.93 0.94 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) T 17698 17698 9854 0 -1 0 15784 0 3 0 4784 92 0 0 25 0 1 0 1785844906 72056832 15429 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/17703/statm): 17592 15429 162 162 0 17430 0 [pid=17703] vsize: 70368 Current children cumulated CPU time (s) 48.79 Current children cumulated vsize (Kb) 72496 [startup+60.009 s] Raw data (loadavg): 0.94 0.94 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 18076 0 3 0 5746 109 0 0 25 0 1 0 1785844906 81072128 17682 4294967295 134512640 135167914 3221224448 3221222816 134696578 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 19793 17682 162 162 0 19631 0 [pid=17703] vsize: 79172 Current children cumulated CPU time (s) 58.58 Current children cumulated vsize (Kb) 81300 [startup+70.0088 s] Raw data (loadavg): 0.95 0.94 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 20015 0 3 0 6713 124 0 0 25 0 1 0 1785844906 88326144 19470 4294967295 134512640 135167914 3221224448 3221222780 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 21564 19470 162 162 0 21402 0 [pid=17703] vsize: 86256 Current children cumulated CPU time (s) 68.4 Current children cumulated vsize (Kb) 88384 [startup+80.0096 s] Raw data (loadavg): 0.95 0.94 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 22022 0 3 0 7677 141 0 0 25 0 1 0 1785844906 95920128 21345 4294967295 134512640 135167914 3221224448 3221221980 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 23418 21345 162 162 0 23256 0 [pid=17703] vsize: 93672 Current children cumulated CPU time (s) 78.21 Current children cumulated vsize (Kb) 95800 [startup+90.0094 s] Raw data (loadavg): 0.96 0.94 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 24839 0 3 0 8653 153 0 0 25 0 1 0 1785844906 107147264 24099 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 26159 24099 162 162 0 25997 0 [pid=17703] vsize: 104636 Current children cumulated CPU time (s) 88.09 Current children cumulated vsize (Kb) 106764 [startup+100.01 s] Raw data (loadavg): 0.97 0.94 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 24841 0 3 0 9653 153 0 0 25 0 1 0 1785844906 107147264 24101 4294967295 134512640 135167914 3221224448 3221223204 134697076 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 26159 24101 162 162 0 25997 0 [pid=17703] vsize: 104636 Current children cumulated CPU time (s) 98.09 Current children cumulated vsize (Kb) 106764 [startup+110.011 s] Raw data (loadavg): 0.97 0.95 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 24842 0 3 0 10653 153 0 0 25 0 1 0 1785844906 107147264 24102 4294967295 134512640 135167914 3221224448 3221223216 134691415 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 26159 24102 162 162 0 25997 0 [pid=17703] vsize: 104636 Current children cumulated CPU time (s) 108.09 Current children cumulated vsize (Kb) 106764 [startup+120.012 s] Raw data (loadavg): 0.98 0.95 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 24847 0 3 0 11653 153 0 0 25 0 1 0 1785844906 107147264 24107 4294967295 134512640 135167914 3221224448 3221223204 134697187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 26159 24107 162 162 0 25997 0 [pid=17703] vsize: 104636 Current children cumulated CPU time (s) 118.09 Current children cumulated vsize (Kb) 106764 [startup+130.013 s] Raw data (loadavg): 0.98 0.95 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 24850 0 3 0 12654 153 0 0 25 0 1 0 1785844906 107147264 24110 4294967295 134512640 135167914 3221224448 3221223264 134522227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 26159 24110 162 162 0 25997 0 [pid=17703] vsize: 104636 Current children cumulated CPU time (s) 128.1 Current children cumulated vsize (Kb) 106764 [startup+140.013 s] Raw data (loadavg): 0.98 0.95 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 24851 0 3 0 13654 153 0 0 25 0 1 0 1785844906 107147264 24111 4294967295 134512640 135167914 3221224448 3221223216 134691307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 26159 24111 162 162 0 25997 0 [pid=17703] vsize: 104636 Current children cumulated CPU time (s) 138.1 Current children cumulated vsize (Kb) 106764 [startup+150.014 s] Raw data (loadavg): 0.98 0.95 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 24851 0 3 0 14654 153 0 0 25 0 1 0 1785844906 107147264 24111 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 26159 24111 162 162 0 25997 0 [pid=17703] vsize: 104636 Current children cumulated CPU time (s) 148.1 Current children cumulated vsize (Kb) 106764 [startup+160.015 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 24902 0 3 0 15654 153 0 0 25 0 1 0 1785844906 103559168 23251 4294967295 134512640 135167914 3221224448 3221140224 134844860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25283 23251 162 162 0 25121 0 [pid=17703] vsize: 101132 Current children cumulated CPU time (s) 158.1 Current children cumulated vsize (Kb) 103260 [startup+170.016 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25379 0 3 0 16651 155 0 0 25 0 1 0 1785844906 104161280 23398 4294967295 134512640 135167914 3221224448 3221220080 134629448 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25430 23398 162 162 0 25268 0 [pid=17703] vsize: 101720 Current children cumulated CPU time (s) 168.09 Current children cumulated vsize (Kb) 103848 [startup+180.016 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25379 0 3 0 17651 155 0 0 25 0 1 0 1785844906 104161280 23398 4294967295 134512640 135167914 3221224448 3221220672 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25430 23398 162 162 0 25268 0 [pid=17703] vsize: 101720 Current children cumulated CPU time (s) 178.09 Current children cumulated vsize (Kb) 103848 [startup+190.017 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25379 0 3 0 18652 155 0 0 25 0 1 0 1785844906 104161280 23398 4294967295 134512640 135167914 3221224448 3221220304 134845895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25430 23398 162 162 0 25268 0 [pid=17703] vsize: 101720 Current children cumulated CPU time (s) 188.1 Current children cumulated vsize (Kb) 103848 [startup+200.018 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25379 0 3 0 19652 155 0 0 25 0 1 0 1785844906 104161280 23398 4294967295 134512640 135167914 3221224448 3221220584 134842997 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25430 23398 162 162 0 25268 0 [pid=17703] vsize: 101720 Current children cumulated CPU time (s) 198.1 Current children cumulated vsize (Kb) 103848 [startup+210.019 s] Raw data (loadavg): 0.99 0.95 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25379 0 3 0 20652 155 0 0 25 0 1 0 1785844906 104161280 23398 4294967295 134512640 135167914 3221224448 3221220296 134844674 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25430 23398 162 162 0 25268 0 [pid=17703] vsize: 101720 Current children cumulated CPU time (s) 208.1 Current children cumulated vsize (Kb) 103848 [startup+220.02 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25379 0 3 0 21652 155 0 0 25 0 1 0 1785844906 104161280 23398 4294967295 134512640 135167914 3221224448 3221220304 134845888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25430 23398 162 162 0 25268 0 [pid=17703] vsize: 101720 Current children cumulated CPU time (s) 218.1 Current children cumulated vsize (Kb) 103848 [startup+230.02 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25379 0 3 0 22653 155 0 0 25 0 1 0 1785844906 104161280 23398 4294967295 134512640 135167914 3221224448 3221221264 134849179 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25430 23398 162 162 0 25268 0 [pid=17703] vsize: 101720 Current children cumulated CPU time (s) 228.11 Current children cumulated vsize (Kb) 103848 [startup+240.021 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25379 0 3 0 23653 155 0 0 25 0 1 0 1785844906 104161280 23398 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25430 23398 162 162 0 25268 0 [pid=17703] vsize: 101720 Current children cumulated CPU time (s) 238.11 Current children cumulated vsize (Kb) 103848 [startup+250.022 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25379 0 3 0 24653 155 0 0 25 0 1 0 1785844906 104161280 23398 4294967295 134512640 135167914 3221224448 3221221664 134629196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25430 23398 162 162 0 25268 0 [pid=17703] vsize: 101720 Current children cumulated CPU time (s) 248.11 Current children cumulated vsize (Kb) 103848 [startup+260.023 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25732 0 3 0 25652 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221219616 134844682 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 258.11 Current children cumulated vsize (Kb) 103940 [startup+270.023 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25732 0 3 0 26652 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221220172 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 268.11 Current children cumulated vsize (Kb) 103940 [startup+280.023 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25732 0 3 0 27652 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221220408 134843032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 278.11 Current children cumulated vsize (Kb) 103940 [startup+290.024 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25732 0 3 0 28653 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 288.12 Current children cumulated vsize (Kb) 103940 [startup+300.025 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25732 0 3 0 29653 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221220832 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 298.12 Current children cumulated vsize (Kb) 103940 [startup+310.026 s] Raw data (loadavg): 0.99 0.96 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25732 0 3 0 30653 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221220516 134843000 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 308.12 Current children cumulated vsize (Kb) 103940 [startup+320.025 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25732 0 3 0 31653 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221220704 134720508 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 318.12 Current children cumulated vsize (Kb) 103940 [startup+330.026 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25732 0 3 0 32654 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221220656 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 328.13 Current children cumulated vsize (Kb) 103940 [startup+340.026 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25732 0 3 0 33654 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221221312 134844697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 338.13 Current children cumulated vsize (Kb) 103940 [startup+350.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25732 0 3 0 34654 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221221260 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 348.13 Current children cumulated vsize (Kb) 103940 [startup+360.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 25732 0 3 0 35654 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221215984 134843030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 358.13 Current children cumulated vsize (Kb) 103940 [startup+370.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26062 0 3 0 36654 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221220016 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 368.13 Current children cumulated vsize (Kb) 103940 [startup+380.029 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26062 0 3 0 37654 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221221376 134845913 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 378.13 Current children cumulated vsize (Kb) 103940 [startup+390.03 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26062 0 3 0 38654 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221221728 134843068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 388.13 Current children cumulated vsize (Kb) 103940 [startup+400.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26062 0 3 0 39654 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221221088 134849068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 398.13 Current children cumulated vsize (Kb) 103940 [startup+410.032 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26062 0 3 0 40655 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221221312 134844697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 408.14 Current children cumulated vsize (Kb) 103940 [startup+420.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26062 0 3 0 41655 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221221388 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 418.14 Current children cumulated vsize (Kb) 103940 [startup+430.032 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26062 0 3 0 42655 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221221376 134845921 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 428.14 Current children cumulated vsize (Kb) 103940 [startup+440.033 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26062 0 3 0 43655 156 0 0 25 0 1 0 1785844906 104255488 23421 4294967295 134512640 135167914 3221224448 3221221040 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25453 23421 162 162 0 25291 0 [pid=17703] vsize: 101812 Current children cumulated CPU time (s) 438.14 Current children cumulated vsize (Kb) 103940 [startup+450.034 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26227 0 3 0 44655 157 0 0 25 0 1 0 1785844906 104931328 23586 4294967295 134512640 135167914 3221224448 3221213308 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25618 23586 162 162 0 25456 0 [pid=17703] vsize: 102472 Current children cumulated CPU time (s) 448.15 Current children cumulated vsize (Kb) 104600 [startup+460.034 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 45653 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221218496 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 458.14 Current children cumulated vsize (Kb) 104360 [startup+470.034 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 46654 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221218648 134696177 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 468.15 Current children cumulated vsize (Kb) 104360 [startup+480.035 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 47654 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220032 134843015 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 478.15 Current children cumulated vsize (Kb) 104360 [startup+490.036 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 48654 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221219524 134849060 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 488.15 Current children cumulated vsize (Kb) 104360 [startup+500.038 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 49654 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220144 134843064 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 498.15 Current children cumulated vsize (Kb) 104360 [startup+510.038 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 50655 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220320 134696342 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 508.16 Current children cumulated vsize (Kb) 104360 [startup+520.038 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 51655 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221219504 134843130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 518.16 Current children cumulated vsize (Kb) 104360 [startup+530.039 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 52655 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220128 134845921 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 528.16 Current children cumulated vsize (Kb) 104360 [startup+540.04 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 53655 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221280 134693570 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 538.16 Current children cumulated vsize (Kb) 104360 [startup+550.041 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 54656 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220736 134843402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 548.17 Current children cumulated vsize (Kb) 104360 [startup+560.041 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 55656 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221024 134696769 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 558.17 Current children cumulated vsize (Kb) 104360 [startup+570.042 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 56656 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220520 134842997 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 568.17 Current children cumulated vsize (Kb) 104360 [startup+580.043 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 57656 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221116 134693585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 578.17 Current children cumulated vsize (Kb) 104360 [startup+590.044 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 58657 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220320 134845924 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 588.18 Current children cumulated vsize (Kb) 104360 [startup+600.045 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 59657 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220216 134849057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 598.18 Current children cumulated vsize (Kb) 104360 [startup+610.046 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 60657 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221264 134849187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 608.18 Current children cumulated vsize (Kb) 104360 [startup+620.046 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 61657 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221104 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 618.18 Current children cumulated vsize (Kb) 104360 [startup+630.047 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 62657 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221264 134843113 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 628.18 Current children cumulated vsize (Kb) 104360 [startup+640.047 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 63658 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221728 134843068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 638.19 Current children cumulated vsize (Kb) 104360 [startup+650.047 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 64658 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221056 134845881 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 648.19 Current children cumulated vsize (Kb) 104360 [startup+660.048 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 65658 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221392 134849102 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 658.19 Current children cumulated vsize (Kb) 104360 [startup+670.049 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 66658 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220800 134845927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 668.19 Current children cumulated vsize (Kb) 104360 [startup+680.05 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 67659 158 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221552 134845901 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 678.2 Current children cumulated vsize (Kb) 104360 [startup+690.051 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 68658 159 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221616 134849196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 688.2 Current children cumulated vsize (Kb) 104360 [startup+700.051 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 69658 159 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220860 134723267 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 698.2 Current children cumulated vsize (Kb) 104360 [startup+710.052 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 70658 159 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221832 134629277 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 708.2 Current children cumulated vsize (Kb) 104360 [startup+720.052 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 71659 159 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221600 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 718.21 Current children cumulated vsize (Kb) 104360 [startup+730.054 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 72659 159 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220912 134694524 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 728.21 Current children cumulated vsize (Kb) 104360 [startup+740.054 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 26662 0 3 0 73659 159 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221376 134844725 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 738.21 Current children cumulated vsize (Kb) 104360 [startup+750.055 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 74658 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221218800 134522715 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 748.21 Current children cumulated vsize (Kb) 104360 [startup+760.056 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 75658 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221219864 134722513 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 758.21 Current children cumulated vsize (Kb) 104360 [startup+770.057 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 76659 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221219728 134844697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 768.22 Current children cumulated vsize (Kb) 104360 [startup+780.058 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 77659 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221219240 134844674 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 778.22 Current children cumulated vsize (Kb) 104360 [startup+790.058 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 78659 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220352 134849122 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 788.22 Current children cumulated vsize (Kb) 104360 [startup+800.06 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 79659 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220080 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 798.22 Current children cumulated vsize (Kb) 104360 [startup+810.061 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 80660 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220672 134844715 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 808.23 Current children cumulated vsize (Kb) 104360 [startup+820.061 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 81660 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220912 134843404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 818.23 Current children cumulated vsize (Kb) 104360 [startup+830.062 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 82660 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221219952 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 828.23 Current children cumulated vsize (Kb) 104360 [startup+840.061 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 83660 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221219628 134845940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 838.23 Current children cumulated vsize (Kb) 104360 [startup+850.062 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 84661 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220736 134849082 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 848.24 Current children cumulated vsize (Kb) 104360 [startup+860.063 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 85661 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220836 134843117 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 858.24 Current children cumulated vsize (Kb) 104360 [startup+870.063 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 86661 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220056 134693783 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 868.24 Current children cumulated vsize (Kb) 104360 [startup+880.063 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 87661 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220848 134845888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 878.24 Current children cumulated vsize (Kb) 104360 [startup+890.064 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 88661 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221616 134694428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 888.24 Current children cumulated vsize (Kb) 104360 [startup+900.065 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 89662 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221068 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 898.25 Current children cumulated vsize (Kb) 104360 [startup+910.066 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 90662 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221219980 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 908.25 Current children cumulated vsize (Kb) 104360 [startup+920.066 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 91662 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221256 134845877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 918.25 Current children cumulated vsize (Kb) 104360 [startup+930.066 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 92662 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221552 134843064 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 928.25 Current children cumulated vsize (Kb) 104360 [startup+940.066 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 93662 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220736 134843160 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 938.25 Current children cumulated vsize (Kb) 104360 [startup+950.067 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 94663 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221376 134844700 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 948.26 Current children cumulated vsize (Kb) 104360 [startup+960.068 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 27240 0 3 0 95663 160 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221488 134844728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 958.26 Current children cumulated vsize (Kb) 104360 [startup+970.069 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 96661 162 0 0 25 0 1 0 1785844906 106037248 23856 4294967295 134512640 135167914 3221224448 3221215780 134624735 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25888 23856 162 162 0 25726 0 [pid=17703] vsize: 103552 Current children cumulated CPU time (s) 968.26 Current children cumulated vsize (Kb) 105680 [startup+980.069 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 97661 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220496 134844728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 978.27 Current children cumulated vsize (Kb) 104360 [startup+990.069 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 98661 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221219976 134693609 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 988.27 Current children cumulated vsize (Kb) 104360 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 99661 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220700 134844638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 998.27 Current children cumulated vsize (Kb) 104360 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 100661 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220176 134718188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 1008.27 Current children cumulated vsize (Kb) 104360 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 101662 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220576 134849108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 1018.28 Current children cumulated vsize (Kb) 104360 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 102662 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221219856 134843107 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 1028.28 Current children cumulated vsize (Kb) 104360 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 103662 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220400 134849108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 1038.28 Current children cumulated vsize (Kb) 104360 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 104662 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221036 134723240 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 1048.28 Current children cumulated vsize (Kb) 104360 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 105663 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220668 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 1058.29 Current children cumulated vsize (Kb) 104360 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 106663 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221292 134693792 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 1068.29 Current children cumulated vsize (Kb) 104360 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 107663 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221220584 134693754 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 1078.29 Current children cumulated vsize (Kb) 104360 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 108663 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221221984 134694364 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 1088.29 Current children cumulated vsize (Kb) 104360 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 109664 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221222088 134845939 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 1098.3 Current children cumulated vsize (Kb) 104360 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 28480 0 3 0 110664 163 0 0 25 0 1 0 1785844906 104685568 23526 4294967295 134512640 135167914 3221224448 3221222096 134849068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25558 23526 162 162 0 25396 0 [pid=17703] vsize: 102232 Current children cumulated CPU time (s) 1108.3 Current children cumulated vsize (Kb) 104360 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 29095 0 3 0 111662 164 0 0 25 0 1 0 1785844906 104837120 23563 4294967295 134512640 135167914 3221224448 3221218220 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25595 23563 162 162 0 25433 0 [pid=17703] vsize: 102380 Current children cumulated CPU time (s) 1118.29 Current children cumulated vsize (Kb) 104508 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 29095 0 3 0 112662 164 0 0 25 0 1 0 1785844906 104837120 23563 4294967295 134512640 135167914 3221224448 3221219008 134629228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25595 23563 162 162 0 25433 0 [pid=17703] vsize: 102380 Current children cumulated CPU time (s) 1128.29 Current children cumulated vsize (Kb) 104508 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 29095 0 3 0 113663 164 0 0 25 0 1 0 1785844906 104837120 23563 4294967295 134512640 135167914 3221224448 3221218824 134693801 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25595 23563 162 162 0 25433 0 [pid=17703] vsize: 102380 Current children cumulated CPU time (s) 1138.3 Current children cumulated vsize (Kb) 104508 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 29095 0 3 0 114663 164 0 0 25 0 1 0 1785844906 104837120 23563 4294967295 134512640 135167914 3221224448 3221219568 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25595 23563 162 162 0 25433 0 [pid=17703] vsize: 102380 Current children cumulated CPU time (s) 1148.3 Current children cumulated vsize (Kb) 104508 [startup+1160.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 29095 0 3 0 115663 164 0 0 25 0 1 0 1785844906 104837120 23563 4294967295 134512640 135167914 3221224448 3221220080 134844723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25595 23563 162 162 0 25433 0 [pid=17703] vsize: 102380 Current children cumulated CPU time (s) 1158.3 Current children cumulated vsize (Kb) 104508 [startup+1170.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 29095 0 3 0 116663 164 0 0 25 0 1 0 1785844906 104837120 23563 4294967295 134512640 135167914 3221224448 3221220032 134843130 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25595 23563 162 162 0 25433 0 [pid=17703] vsize: 102380 Current children cumulated CPU time (s) 1168.3 Current children cumulated vsize (Kb) 104508 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 29095 0 3 0 117664 164 0 0 25 0 1 0 1785844906 104837120 23563 4294967295 134512640 135167914 3221224448 3221220000 134849110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25595 23563 162 162 0 25433 0 [pid=17703] vsize: 102380 Current children cumulated CPU time (s) 1178.31 Current children cumulated vsize (Kb) 104508 [startup+1190.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 29095 0 3 0 118664 164 0 0 25 0 1 0 1785844906 104837120 23563 4294967295 134512640 135167914 3221224448 3221220460 134844638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25595 23563 162 162 0 25433 0 [pid=17703] vsize: 102380 Current children cumulated CPU time (s) 1188.31 Current children cumulated vsize (Kb) 104508 [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 29095 0 3 0 119664 164 0 0 25 0 1 0 1785844906 104837120 23563 4294967295 134512640 135167914 3221224448 3221219328 134849163 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25595 23563 162 162 0 25433 0 [pid=17703] vsize: 102380 Current children cumulated CPU time (s) 1198.31 Current children cumulated vsize (Kb) 104508 [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 29095 0 3 0 120664 164 0 0 25 0 1 0 1785844906 104837120 23563 4294967295 134512640 135167914 3221224448 3221220080 134844718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25595 23563 162 162 0 25433 0 [pid=17703] vsize: 102380 Current children cumulated CPU time (s) 1208.31 Current children cumulated vsize (Kb) 104508 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17703 Raw data (/proc/17698/stat): 17698 (minisat+_script) S 17697 17698 9854 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785844897 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17698/statm): 532 234 485 147 0 385 0 [pid=17698] vsize: 2128 Raw data (/proc/17703/stat): 17703 (minisat+_bignum) R 17698 17698 9854 0 -1 0 29095 0 3 0 120664 164 0 0 25 0 1 0 1785844906 104837120 23563 4294967295 134512640 135167914 3221224448 3221220232 134843032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17703/statm): 25595 23563 162 162 0 25433 0 [pid=17703] vsize: 102380 Current children cumulated CPU time (s) 1208.31 Current children cumulated vsize (Kb) 104508 Sending SIGTERM to -17698 Sleeping 2 seconds One traced child (pid=17698) ended because it received signal 15 (SIGTERM) One traced child (pid=17703) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.13 CPU time (s): 1208.34 CPU user time (s): 1206.65 CPU system time (s): 1.68874 CPU usage (%): 99.8515 Max. virtual memory (cumulated for all children) (Kb): 106764
ERROR: no interpretation found !