Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-mod011.opb
MD5SUM5b9b020cb595d55e8dbba526590c1088
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 144804
Biggest coefficient in the objective function 37355509514240
Number of bits for the biggest coefficient in the objective function 46
Sum of the numbers in the objective function 86052429291555573
Number of bits of the sum of numbers in the objective function 57
Biggest number in a constraint 37355509514240
Number of bits of the biggest number in a constraint 46
Biggest sum of numbers in a constraint 86052429291555573
Number of bits of the biggest sum of numbers57
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1211.57
Number of variables211663
Total number of constraints6093
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)128
Number of constraints which are nor clauses,nor cardinality constraints5965
Minimum length of a constraint1
Maximum length of a constraint16460

Trace number 6175

Launcher Data

LAUNCH ON wulflinc19 THE 2005-09-20 04:07:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3339 boxname=wulflinc19 idbench=995 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5b9b020cb595d55e8dbba526590c1088  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-mod011.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-mod011.opb
IDLAUNCH: 3339
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        900056 kB
Buffers:         15312 kB
Cached:          91076 kB
SwapCached:        848 kB
Active:          34732 kB
Inactive:        74232 kB
HighTotal:      131008 kB
HighFree:        38836 kB
LowTotal:       903652 kB
LowFree:        861220 kB
SwapTotal:     2097892 kB
SwapFree:      2096432 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5508 kB
Slab:            19992 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:27:58 (client local time) WITH STATUS 0 IN 1207.54 SECONDS
stats: 3339 7 1207.54 0

Solver Data

c Parsing PB file...
c Converting 10347 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ###############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[10788]---> BDD-cost:   13
c ---[10787]---> BDD-cost:   14
c ---[10786]---> BDD-cost:   12
c ---[10785]---> BDD-cost:   14
c ---[10784]---> BDD-cost:   11
c ---[10783]---> BDD-cost:    9
c ---[10782]---> BDD-cost:   13
c ---[10781]---> BDD-cost:   10
c ---[10780]---> BDD-cost:   15
c ---[10779]---> BDD-cost:   11
c ---[10778]---> BDD-cost:    8
c ---[10776]---> BDD-cost:   10
c ---[10775]---> BDD-cost:   14
c ---[10774]---> BDD-cost:   11
c ---[10773]---> BDD-cost:   16
c ---[10772]---> BDD-cost:   16
c ---[10771]---> BDD-cost:   17
c ---[10770]---> BDD-cost:   17
c ---[10769]---> BDD-cost:   18
c ---[10768]---> BDD-cost:   13
c ---[10767]---> BDD-cost:   14
c ---[10765]---> BDD-cost:   14
c ---[10764]---> BDD-cost:   12
c ---[10763]---> BDD-cost:   16
c ---[10762]---> BDD-cost:   14
c ---[10761]---> BDD-cost:   15
c ---[10760]---> BDD-cost:   12
c ---[10758]---> BDD-cost:   11
c ---[10757]---> BDD-cost:   13
c ---[10756]---> BDD-cost:   10
c ---[10755]---> BDD-cost:   11
c ---[10754]---> BDD-cost:   15
c ---[10753]---> BDD-cost:   17
c ---[10752]---> BDD-cost:   10
c ---[10751]---> BDD-cost:   11
c ---[10750]---> BDD-cost:   11
c ---[10748]---> BDD-cost:   12
c ---[10746]---> BDD-cost:   16
c ---[10745]---> BDD-cost:   15
c ---[10744]---> BDD-cost:   14
c ---[10742]---> BDD-cost:   13
c ---[10741]---> BDD-cost:   13
c ---[10740]---> BDD-cost:   16
c ---[10738]---> BDD-cost:   11
c ---[10737]---> BDD-cost:   14
c ---[10736]---> BDD-cost:   13
c ---[10735]---> BDD-cost:   11
c ---[10734]---> BDD-cost:   12
c ---[10733]---> BDD-cost:   11
c ---[10732]---> BDD-cost:   12
c ---[10731]---> BDD-cost:   11
c ---[10730]---> BDD-cost:   15
c ---[10729]---> BDD-cost:   14
c ---[10728]---> BDD-cost:   13
c ---[10727]---> BDD-cost:   13
c ---[10726]---> BDD-cost:   12
c ---[10725]---> BDD-cost:    7
c ---[10724]---> BDD-cost:    8
c ---[10723]---> BDD-cost:    7
c ---[10722]---> BDD-cost:   13
c ---[10721]---> BDD-cost:   13
c ---[10720]---> BDD-cost:   14
c ---[10719]---> BDD-cost:   10
c ---[10718]---> BDD-cost:   14
c ---[10717]---> BDD-cost:   15
c ---[10716]---> BDD-cost:   14
c ---[10713]---> BDD-cost:   17
c ---[10712]---> BDD-cost:   17
c ---[10711]---> BDD-cost:   15
c ---[10710]---> BDD-cost:   12
c ---[10709]---> BDD-cost:   14
c ---[10708]---> BDD-cost:   15
c ---[10707]---> BDD-cost:   15
c ---[10705]---> BDD-cost:   13
c ---[10703]---> BDD-cost:   18
c ---[10702]---> BDD-cost:   15
c ---[10701]---> BDD-cost:   12
c ---[10700]---> BDD-cost:   13
c ---[10697]---> BDD-cost:   16
c ---[10696]---> BDD-cost:   14
c ---[10695]---> BDD-cost:   15
c ---[10694]---> BDD-cost:   13
c ---[10693]---> BDD-cost:   15
c ---[10692]---> BDD-cost:   12
c ---[10691]---> BDD-cost:   14
c ---[10690]---> BDD-cost:   16
c ---[10689]---> BDD-cost:   14
c ---[10688]---> BDD-cost:   17
c ---[10687]---> BDD-cost:   14
c ---[10684]---> BDD-cost:   16
c ---[10683]---> BDD-cost:   14
c ---[10682]---> BDD-cost:   16
c ---[10681]---> BDD-cost:   13
c ---[10680]---> BDD-cost:   11
c ---[10679]---> BDD-cost:   14
c ---[10678]---> BDD-cost:   15
c ---[10676]---> BDD-cost:   15
c ---[10675]---> BDD-cost:   16
c ---[10674]---> BDD-cost:   15
c ---[10672]---> BDD-cost:   11
c ---[10671]---> BDD-cost:   16
c ---[10669]---> BDD-cost:   14
c ---[10668]---> BDD-cost:   16
c ---[10667]---> BDD-cost:   16
c ---[10666]---> BDD-cost:   15
c ---[10664]---> BDD-cost:   10
c ---[10663]---> BDD-cost:   16
c ---[10662]---> BDD-cost:   14
c ---[10661]---> BDD-cost:   16
c ---[10660]---> BDD-cost:   15
c ---[10659]---> BDD-cost:   14
c ---[10658]---> BDD-cost:   15
c ---[10657]---> BDD-cost:   14
c ---[10656]---> BDD-cost:   15
c ---[10655]---> BDD-cost:   13
c ---[10654]---> BDD-cost:   15
c ---[10653]---> BDD-cost:   14
c ---[10652]---> BDD-cost:   13
c ---[10651]---> BDD-cost:   12
c ---[10650]---> BDD-cost:   15
c ---[10649]---> BDD-cost:   14
c ---[10647]---> BDD-cost:   13
c ---[10646]---> BDD-cost:   12
c ---[10645]---> BDD-cost:   15
c ---[10644]---> BDD-cost:    9
c ---[10643]---> BDD-cost:   14
c ---[10642]---> BDD-cost:   12
c ---[10640]---> BDD-cost:   14
c ---[10636]---> BDD-cost:   12
c ---[10635]---> BDD-cost:   13
c ---[10634]---> BDD-cost:   14
c ---[10633]---> BDD-cost:   13
c ---[10632]---> BDD-cost:   16
c ---[10631]---> BDD-cost:   15
c ---[10630]---> BDD-cost:   10
c ---[10629]---> BDD-cost:   16
c ---[10628]---> BDD-cost:   15
c ---[10626]---> BDD-cost:   12
c ---[10625]---> BDD-cost:   11
c ---[10624]---> BDD-cost:   10
c ---[10623]---> BDD-cost:   12
c ---[10622]---> BDD-cost:   16
c ---[10621]---> BDD-cost:   16
c ---[10620]---> BDD-cost:   17
c ---[10618]---> BDD-cost:   16
c ---[10617]---> BDD-cost:   14
c ---[10616]---> BDD-cost:   14
c ---[10615]---> BDD-cost:   15
c ---[10613]---> BDD-cost:   13
c ---[10612]---> BDD-cost:   12
c ---[10611]---> BDD-cost:   16
c ---[10610]---> BDD-cost:   11
c ---[10609]---> BDD-cost:   13
c ---[10607]---> BDD-cost:   15
c ---[10606]---> BDD-cost:   16
c ---[10605]---> BDD-cost:   17
c ---[10604]---> BDD-cost:   16
c ---[10603]---> BDD-cost:   18
c ---[10602]---> BDD-cost:   16
c ---[10601]---> BDD-cost:   12
c ---[10600]---> BDD-cost:   11
c ---[10599]---> BDD-cost:   12
c ---[10598]---> BDD-cost:   15
c ---[10597]---> BDD-cost:   11
c ---[10596]---> BDD-cost:   14
c ---[10595]---> BDD-cost:   13
c ---[10593]---> BDD-cost:   13
c ---[10592]---> BDD-cost:   13
c ---[10591]---> BDD-cost:   11
c ---[10589]---> BDD-cost:    9
c ---[10587]---> BDD-cost:   11
c ---[10586]---> BDD-cost:   15
c ---[10585]---> BDD-cost:   10
c ---[10584]---> BDD-cost:    9
c ---[10583]---> BDD-cost:   12
c ---[10582]---> BDD-cost:   11
c ---[10581]---> BDD-cost:    9
c ---[10580]---> BDD-cost:   10
c ---[10579]---> BDD-cost:   13
c ---[10578]---> BDD-cost:   14
c ---[10577]---> BDD-cost:   13
c ---[10576]---> BDD-cost:   11
c ---[10575]---> BDD-cost:   14
c ---[10572]---> BDD-cost:   15
c ---[10571]---> BDD-cost:   17
c ---[10570]---> BDD-cost:   14
c ---[10569]---> BDD-cost:   15
c ---[10567]---> BDD-cost:   17
c ---[10566]---> BDD-cost:   16
c ---[10565]---> BDD-cost:   13
c ---[10564]---> BDD-cost:   12
c ---[10563]---> BDD-cost:   15
c ---[10562]---> BDD-cost:   10
c ---[10561]---> BDD-cost:   14
c ---[10560]---> BDD-cost:   14
c ---[10558]---> BDD-cost:   12
c ---[10557]---> BDD-cost:   14
c ---[10556]---> BDD-cost:   14
c ---[10555]---> BDD-cost:   15
c ---[10554]---> BDD-cost:   12
c ---[10553]---> BDD-cost:   10
c ---[10552]---> BDD-cost:   15
c ---[10551]---> BDD-cost:   11
c ---[10550]---> BDD-cost:   14
c ---[10549]---> BDD-cost:   14
c ---[10548]---> BDD-cost:   12
c ---[10547]---> BDD-cost:   15
c ---[10546]---> BDD-cost:   15
c ---[10545]---> BDD-cost:   13
c ---[10544]---> BDD-cost:   10
c ---[10541]---> BDD-cost:   12
c ---[10540]---> BDD-cost:   13
c ---[10537]---> BDD-cost:   10
c ---[10534]---> BDD-cost:   14
c ---[10533]---> BDD-cost:   13
c ---[10531]---> BDD-cost:   14
c ---[10530]---> BDD-cost:   14
c ---[10528]---> BDD-cost:   15
c ---[10527]---> BDD-cost:   13
c ---[10526]---> BDD-cost:   12
c ---[10525]---> BDD-cost:   14
c ---[10524]---> BDD-cost:   12
c ---[10522]---> BDD-cost:   13
c ---[10521]---> BDD-cost:   16
c ---[10520]---> BDD-cost:   15
c ---[10519]---> BDD-cost:   12
c ---[10518]---> BDD-cost:   13
c ---[10517]---> BDD-cost:   14
c ---[10516]---> BDD-cost:   17
c ---[10515]---> BDD-cost:   14
c ---[10514]---> BDD-cost:   12
c ---[10513]---> BDD-cost:   11
c ---[10512]---> BDD-cost:    9
c ---[10510]---> BDD-cost:   13
c ---[10509]---> BDD-cost:   16
c ---[10507]---> BDD-cost:   18
c ---[10506]---> BDD-cost:   12
c ---[10505]---> BDD-cost:   15
c ---[10504]---> BDD-cost:   13
c ---[10499]---> BDD-cost:   14
c ---[10498]---> BDD-cost:   13
c ---[10497]---> BDD-cost:   12
c ---[10496]---> BDD-cost:   13
c ---[10495]---> BDD-cost:   12
c ---[10494]---> BDD-cost:   14
c ---[10493]---> BDD-cost:   12
c ---[10492]---> BDD-cost:    8
c ---[10491]---> BDD-cost:   12
c ---[10490]---> BDD-cost:   14
c ---[10489]---> BDD-cost:   16
c ---[10488]---> BDD-cost:   14
c ---[10486]---> BDD-cost:   12
c ---[10485]---> BDD-cost:   12
c ---[10484]---> BDD-cost:   15
c ---[10483]---> BDD-cost:   13
c ---[10482]---> BDD-cost:   13
c ---[10481]---> BDD-cost:   13
c ---[10480]---> BDD-cost:   16
c ---[10479]---> BDD-cost:   14
c ---[10478]---> BDD-cost:   17
c ---[10477]---> BDD-cost:   14
c ---[10476]---> BDD-cost:   16
c ---[10475]---> BDD-cost:   15
c ---[10474]---> BDD-cost:   13
c ---[10473]---> BDD-cost:   10
c ---[10472]---> BDD-cost:   15
c ---[10471]---> BDD-cost:   16
c ---[10470]---> BDD-cost:   14
c ---[10469]---> BDD-cost:   14
c ---[10468]---> BDD-cost:   14
c ---[10467]---> BDD-cost:   12
c ---[10465]---> BDD-cost:    8
c ---[10464]---> BDD-cost:   10
c ---[10462]---> BDD-cost:   11
c ---[10461]---> BDD-cost:   13
c ---[10460]---> BDD-cost:   14
c ---[10458]---> BDD-cost:   12
c ---[10457]---> BDD-cost:   12
c ---[10455]---> BDD-cost:   14
c ---[10453]---> BDD-cost:   14
c ---[10452]---> BDD-cost:   12
c ---[10451]---> BDD-cost:    8
c ---[10450]---> BDD-cost:   13
c ---[10449]---> BDD-cost:   16
c ---[10448]---> BDD-cost:   15
c ---[10447]---> BDD-cost:   13
c ---[10446]---> BDD-cost:   12
c ---[10444]---> BDD-cost:   14
c ---[10443]---> BDD-cost:   11
c ---[10442]---> BDD-cost:   14
c ---[10441]---> BDD-cost:   12
c ---[10440]---> BDD-cost:   11
c ---[10439]---> BDD-cost:   12
c ---[10438]---> BDD-cost:   15
c ---[10437]---> BDD-cost:   13
c ---[10436]---> BDD-cost:    7
c ---[10435]---> BDD-cost:   12
c ---[10433]---> BDD-cost:   14
c ---[10432]---> BDD-cost:   11
c ---[10430]---> BDD-cost:    9
c ---[10429]---> BDD-cost:   13
c ---[10428]---> BDD-cost:   15
c ---[10426]---> BDD-cost:   14
c ---[10425]---> BDD-cost:   11
c ---[10424]---> BDD-cost:   10
c ---[10423]---> BDD-cost:   12
c ---[10422]---> BDD-cost:   14
c ---[10421]---> BDD-cost:   15
c ---[10417]---> BDD-cost:   10
c ---[10416]---> BDD-cost:   15
c ---[10415]---> BDD-cost:   14
c ---[10413]---> BDD-cost:   15
c ---[10412]---> BDD-cost:   16
c ---[10410]---> BDD-cost:   16
c ---[10409]---> BDD-cost:   12
c ---[10408]---> BDD-cost:   12
c ---[10407]---> BDD-cost:   12
c ---[10405]---> BDD-cost:   14
c ---[10403]---> BDD-cost:   10
c ---[10401]---> BDD-cost:   13
c ---[10400]---> BDD-cost:   14
c ---[10399]---> BDD-cost:   13
c ---[10398]---> BDD-cost:   10
c ---[10397]---> BDD-cost:   12
c ---[10396]---> BDD-cost:   12
c ---[10395]---> BDD-cost:   15
c ---[10391]---> BDD-cost:   14
c ---[10390]---> BDD-cost:   16
c ---[10389]---> BDD-cost:   15
c ---[10388]---> BDD-cost:   12
c ---[10387]---> BDD-cost:   10
c ---[10385]---> BDD-cost:   14
c ---[10384]---> BDD-cost:   16
c ---[10383]---> BDD-cost:   14
c ---[10382]---> BDD-cost:    9
c ---[10381]---> BDD-cost:    9
c ---[10379]---> BDD-cost:   14
c ---[10378]---> BDD-cost:   14
c ---[10377]---> BDD-cost:   17
c ---[10374]---> BDD-cost:   13
c ---[10372]---> BDD-cost:    7
c ---[10371]---> BDD-cost:   10
c ---[10370]---> BDD-cost:   16
c ---[10369]---> BDD-cost:   14
c ---[10368]---> BDD-cost:   14
c ---[10367]---> BDD-cost:   10
c ---[10365]---> BDD-cost:   13
c ---[10364]---> BDD-cost:   15
c ---[10363]---> BDD-cost:   14
c ---[10362]---> BDD-cost:   11
c ---[10361]---> BDD-cost:   11
c ---[10360]---> BDD-cost:   15
c ---[10359]---> BDD-cost:   12
c ---[10358]---> BDD-cost:   12
c ---[10356]---> BDD-cost:   13
c ---[10355]---> BDD-cost:   15
c ---[10354]---> BDD-cost:   12
c ---[10353]---> BDD-cost:   14
c ---[10352]---> BDD-cost:   11
c ---[10351]---> BDD-cost:   13
c ---[10350]---> BDD-cost:   13
c ---[10349]---> BDD-cost:   15
c ---[10348]---> BDD-cost:   14
c ---[10347]---> BDD-cost:   11
c ---[10346]---> BDD-cost:   13
c ---[10345]---> BDD-cost:   12
c ---[10344]---> BDD-cost:   15
c ---[10343]---> BDD-cost:   14
c ---[10342]---> BDD-cost:   14
c ---[10341]---> BDD-cost:   11
c ---[10340]---> BDD-cost:   12
c ---[10339]---> BDD-cost:   15
c ---[10338]---> BDD-cost:   14
c ---[10337]---> BDD-cost:   12
c ---[10335]---> BDD-cost:   15
c ---[10334]---> BDD-cost:   16
c ---[10333]---> BDD-cost:    8
c ---[10332]---> BDD-cost:    8
c ---[10331]---> BDD-cost:   15
c ---[10330]---> BDD-cost:   18
c ---[10329]---> BDD-cost:   13
c ---[10328]---> BDD-cost:   16
c ---[10326]---> BDD-cost:   16
c ---[10325]---> BDD-cost:   12
c ---[10323]---> BDD-cost:   14
c ---[10322]---> BDD-cost:   17
c ---[10321]---> BDD-cost:   15
c ---[10320]---> BDD-cost:    7
c ---[10318]---> BDD-cost:   15
c ---[10317]---> BDD-cost:   17
c ---[10316]---> BDD-cost:   15
c ---[10315]---> BDD-cost:   15
c ---[10314]---> BDD-cost:   11
c ---[10313]---> BDD-cost:   15
c ---[10312]---> BDD-cost:   17
c ---[10311]---> BDD-cost:   15
c ---[10310]---> BDD-cost:   16
c ---[10309]---> BDD-cost:   14
c ---[10308]---> BDD-cost:   12
c ---[10307]---> BDD-cost:   13
c ---[10301]---> BDD-cost:    9
c ---[10299]---> BDD-cost:   12
c ---[10298]---> BDD-cost:   15
c ---[10295]---> BDD-cost:   14
c ---[10293]---> BDD-cost:   12
c ---[10292]---> BDD-cost:   11
c ---[10291]---> BDD-cost:   13
c ---[10290]---> BDD-cost:   17
c ---[10289]---> BDD-cost:   14
c ---[10288]---> BDD-cost:   15
c ---[10287]---> BDD-cost:   10
c ---[10286]---> BDD-cost:   11
c ---[10285]---> BDD-cost:   11
c ---[10284]---> BDD-cost:   12
c ---[10283]---> BDD-cost:   15
c ---[10282]---> BDD-cost:   15
c ---[10281]---> BDD-cost:   14
c ---[10280]---> BDD-cost:   11
c ---[10279]---> BDD-cost:    9
c ---[10276]---> BDD-cost:   12
c ---[10275]---> BDD-cost:   15
c ---[10274]---> BDD-cost:   13
c ---[10273]---> BDD-cost:   11
c ---[10272]---> BDD-cost:   10
c ---[10271]---> BDD-cost:   10
c ---[10270]---> BDD-cost:   12
c ---[10269]---> BDD-cost:   16
c ---[10268]---> BDD-cost:   16
c ---[10267]---> BDD-cost:   16
c ---[10266]---> BDD-cost:   14
c ---[10263]---> BDD-cost:   14
c ---[10262]---> BDD-cost:   17
c ---[10261]---> BDD-cost:   13
c ---[10259]---> BDD-cost:    8
c ---[10258]---> BDD-cost:   11
c ---[10257]---> BDD-cost:   16
c ---[10256]---> BDD-cost:   14
c ---[10255]---> BDD-cost:   11
c ---[10254]---> BDD-cost:    9
c ---[10253]---> BDD-cost:   12
c ---[10252]---> BDD-cost:   16
c ---[10251]---> BDD-cost:   14
c ---[10249]---> BDD-cost:   10
c ---[10248]---> BDD-cost:   10
c ---[10247]---> BDD-cost:   10
c ---[10244]---> BDD-cost:   16
c ---[10243]---> BDD-cost:   14
c ---[10242]---> BDD-cost:   14
c ---[10241]---> BDD-cost:   11
c ---[10239]---> BDD-cost:   17
c ---[10238]---> BDD-cost:   15
c ---[10237]---> BDD-cost:   13
c ---[10236]---> BDD-cost:   11
c ---[10235]---> BDD-cost:   13
c ---[10233]---> BDD-cost:    7
c ---[10232]---> BDD-cost:   10
c ---[10231]---> BDD-cost:   14
c ---[10230]---> BDD-cost:   16
c ---[10229]---> BDD-cost:   16
c ---[10226]---> BDD-cost:   13
c ---[10225]---> BDD-cost:   13
c ---[10224]---> BDD-cost:   15
c ---[10220]---> BDD-cost:   12
c ---[10219]---> BDD-cost:   14
c ---[10218]---> BDD-cost:   14
c ---[10217]---> BDD-cost:   14
c ---[10216]---> BDD-cost:   11
c ---[10214]---> BDD-cost:   16
c ---[10211]---> BDD-cost:   15
c ---[10209]---> BDD-cost:   14
c ---[10208]---> BDD-cost:   14
c ---[10207]---> BDD-cost:   15
c ---[10206]---> BDD-cost:   14
c ---[10205]---> BDD-cost:   11
c ---[10203]---> BDD-cost:   13
c ---[10202]---> BDD-cost:   16
c ---[10201]---> BDD-cost:   12
c ---[10200]---> BDD-cost:   13
c ---[10199]---> BDD-cost:   10
c ---[10198]---> BDD-cost:    7
c ---[10197]---> BDD-cost:   12
c ---[10196]---> BDD-cost:   15
c ---[10195]---> BDD-cost:   15
c ---[10194]---> BDD-cost:    9
c ---[10193]---> BDD-cost:   14
c ---[10192]---> BDD-cost:   13
c ---[10191]---> BDD-cost:   11
c ---[10187]---> BDD-cost:   15
c ---[10186]---> BDD-cost:   15
c ---[10185]---> BDD-cost:   17
c ---[10184]---> BDD-cost:   13
c ---[10183]---> BDD-cost:   13
c ---[10182]---> BDD-cost:   17
c ---[10180]---> BDD-cost:   14
c ---[10179]---> BDD-cost:   13
c ---[10178]---> BDD-cost:   11
c ---[10177]---> BDD-cost:   12
c ---[10176]---> BDD-cost:   15
c ---[10175]---> BDD-cost:   14
c ---[10174]---> BDD-cost:   12
c ---[10173]---> BDD-cost:   11
c ---[10170]---> BDD-cost:   12
c ---[10169]---> BDD-cost:   14
c ---[10168]---> BDD-cost:   16
c ---[10166]---> BDD-cost:   17
c ---[10164]---> BDD-cost:   16
c ---[10163]---> BDD-cost:    7
c ---[10162]---> BDD-cost:   16
c ---[10161]---> BDD-cost:   12
c ---[10160]---> BDD-cost:   11
c ---[10159]---> BDD-cost:   12
c ---[10158]---> BDD-cost:   15
c ---[10157]---> BDD-cost:   13
c ---[10156]---> BDD-cost:   10
c ---[10155]---> BDD-cost:   14
c ---[10154]---> BDD-cost:   16
c ---[10153]---> BDD-cost:   13
c ---[10152]---> BDD-cost:   12
c ---[10151]---> BDD-cost:    8
c ---[10150]---> BDD-cost:   12
c ---[10149]---> BDD-cost:   16
c ---[10148]---> BDD-cost:   16
c ---[10147]---> BDD-cost:   16
c ---[10146]---> BDD-cost:   12
c ---[10145]---> BDD-cost:   16
c ---[10143]---> BDD-cost:   14
c ---[10142]---> BDD-cost:   15
c ---[10141]---> BDD-cost:   14
c ---[10140]---> BDD-cost:   12
c ---[10139]---> BDD-cost:   10
c ---[10138]---> BDD-cost:   13
c ---[10137]---> BDD-cost:   17
c ---[10136]---> BDD-cost:    9
c ---[10135]---> BDD-cost:   15
c ---[10134]---> BDD-cost:   13
c ---[10133]---> BDD-cost:   10
c ---[10132]---> BDD-cost:   11
c ---[10129]---> BDD-cost:   14
c ---[10128]---> BDD-cost:   11
c ---[10127]---> BDD-cost:   11
c ---[10126]---> BDD-cost:    7
c ---[10125]---> BDD-cost:   12
c ---[10124]---> BDD-cost:   15
c ---[10123]---> BDD-cost:   11
c ---[10122]---> BDD-cost:   13
c ---[10121]---> BDD-cost:   16
c ---[10120]---> BDD-cost:    8
c ---[10118]---> BDD-cost:   14
c ---[10117]---> BDD-cost:   13
c ---[10116]---> BDD-cost:   12
c ---[10115]---> BDD-cost:   13
c ---[10114]---> BDD-cost:   14
c ---[10112]---> BDD-cost:   17
c ---[10111]---> BDD-cost:   11
c ---[10109]---> BDD-cost:   12
c ---[10108]---> BDD-cost:   14
c ---[10107]---> BDD-cost:   16
c ---[10105]---> BDD-cost:   11
c ---[10104]---> BDD-cost:    9
c ---[10102]---> BDD-cost:   16
c ---[10100]---> BDD-cost:   12
c ---[10099]---> BDD-cost:   12
c ---[10098]---> BDD-cost:   14
c ---[10097]---> BDD-cost:   15
c ---[10096]---> BDD-cost:   14
c ---[10094]---> BDD-cost:   11
c ---[10092]---> BDD-cost:   13
c ---[10091]---> BDD-cost:   16
c ---[10090]---> BDD-cost:   14
c ---[10089]---> BDD-cost:   15
c ---[10088]---> BDD-cost:   11
c ---[10087]---> BDD-cost:   10
c ---[10086]---> BDD-cost:   13
c ---[10085]---> BDD-cost:   15
c ---[10083]---> BDD-cost:   13
c ---[10082]---> BDD-cost:   13
c ---[10081]---> BDD-cost:   16
c ---[10080]---> BDD-cost:   10
c ---[10079]---> BDD-cost:   16
c ---[10078]---> BDD-cost:   12
c ---[10077]---> BDD-cost:   18
c ---[10076]---> BDD-cost:   12
c ---[10075]---> BDD-cost:   18
c ---[10074]---> BDD-cost:   14
c ---[10073]---> BDD-cost:   11
c ---[10071]---> BDD-cost:   15
c ---[10070]---> BDD-cost:   15
c ---[10069]---> BDD-cost:   12
c ---[10066]---> BDD-cost:   15
c ---[10065]---> BDD-cost:   14
c ---[10063]---> BDD-cost:   10
c ---[10061]---> BDD-cost:   12
c ---[10060]---> BDD-cost:   15
c ---[10058]---> BDD-cost:   10
c ---[10057]---> BDD-cost:   15
c ---[10056]---> BDD-cost:   11
c ---[10054]---> BDD-cost:   16
c ---[10053]---> BDD-cost:   13
c ---[10051]---> BDD-cost:   14
c ---[10050]---> BDD-cost:   15
c ---[10049]---> BDD-cost:   10
c ---[10047]---> BDD-cost:   12
c ---[10046]---> BDD-cost:   15
c ---[10045]---> BDD-cost:   14
c ---[10043]---> BDD-cost:   15
c ---[10042]---> BDD-cost:   14
c ---[10041]---> BDD-cost:   14
c ---[10037]---> BDD-cost:   13
c ---[10036]---> BDD-cost:   12
c ---[10035]---> BDD-cost:   15
c ---[10034]---> BDD-cost:   12
c ---[10033]---> BDD-cost:   15
c ---[10032]---> BDD-cost:   13
c ---[10031]---> BDD-cost:   14
c ---[10030]---> BDD-cost:   11
c ---[10029]---> BDD-cost:   13
c ---[10028]---> BDD-cost:   13
c ---[10027]---> BDD-cost:   15
c ---[10026]---> BDD-cost:   14
c ---[10024]---> BDD-cost:   10
c ---[10023]---> BDD-cost:   14
c ---[10022]---> BDD-cost:   13
c ---[10021]---> BDD-cost:   15
c ---[10020]---> BDD-cost:   12
c ---[10019]---> BDD-cost:   13
c ---[10018]---> BDD-cost:   14
c ---[10017]---> BDD-cost:   12
c ---[10016]---> BDD-cost:   14
c ---[10014]---> BDD-cost:   12
c ---[10013]---> BDD-cost:   15
c ---[10012]---> BDD-cost:   13
c ---[10011]---> BDD-cost:   14
c ---[10010]---> BDD-cost:   11
c ---[10009]---> BDD-cost:   12
c ---[10008]---> BDD-cost:   14
c ---[10007]---> BDD-cost:   13
c ---[10006]---> BDD-cost:   15
c ---[10005]---> BDD-cost:    9
c ---[10004]---> BDD-cost:   12
c ---[10002]---> BDD-cost:   15
c ---[10001]---> BDD-cost:   12
c ---[10000]---> BDD-cost:   14
c ---[9999]---> BDD-cost:   11
c ---[9997]---> BDD-cost:   13
c ---[9996]---> BDD-cost:   15
c ---[9995]---> BDD-cost:   10
c ---[9992]---> BDD-cost:   14
c ---[9990]---> BDD-cost:   12
c ---[9989]---> BDD-cost:   10
c ---[9988]---> BDD-cost:   12
c ---[9987]---> BDD-cost:   14
c ---[9986]---> BDD-cost:   15
c ---[9985]---> BDD-cost:   15
c ---[9984]---> BDD-cost:   13
c ---[9983]---> BDD-cost:   10
c ---[9982]---> BDD-cost:   16
c ---[9981]---> BDD-cost:   13
c ---[9980]---> BDD-cost:   14
c ---[9979]---> BDD-cost:   16
c ---[9978]---> BDD-cost:   13
c ---[9977]---> BDD-cost:   16
c ---[9976]---> BDD-cost:   11
c ---[9973]---> BDD-cost:   16
c ---[9972]---> BDD-cost:   13
c ---[9971]---> BDD-cost:   14
c ---[9970]---> BDD-cost:   10
c ---[9969]---> BDD-cost:   13
c ---[9967]---> BDD-cost:   14
c ---[9966]---> BDD-cost:   10
c ---[9965]---> BDD-cost:    8
c ---[9964]---> BDD-cost:   13
c ---[9963]---> BDD-cost:   14
c ---[9961]---> BDD-cost:   15
c ---[9960]---> BDD-cost:   13
c ---[9959]---> BDD-cost:   10
c ---[9958]---> BDD-cost:   14
c ---[9957]---> BDD-cost:   13
c ---[9956]---> BDD-cost:   16
c ---[9955]---> BDD-cost:   16
c ---[9953]---> BDD-cost:    9
c ---[9952]---> BDD-cost:   11
c ---[9951]---> BDD-cost:   14
c ---[9950]---> BDD-cost:   15
c ---[9949]---> BDD-cost:   17
c ---[9948]---> BDD-cost:   13
c ---[9947]---> BDD-cost:   12
c ---[9946]---> BDD-cost:   10
c ---[9945]---> BDD-cost:   13
c ---[9944]---> BDD-cost:   15
c ---[9943]---> BDD-cost:   16
c ---[9942]---> BDD-cost:   13
c ---[9940]---> BDD-cost:   12
c ---[9939]---> BDD-cost:   14
c ---[9937]---> BDD-cost:   15
c ---[9936]---> BDD-cost:   13
c ---[9935]---> BDD-cost:   12
c ---[9934]---> BDD-cost:   13
c ---[9933]---> BDD-cost:   16
c ---[9931]---> BDD-cost:   15
c ---[9930]---> BDD-cost:   12
c ---[9929]---> BDD-cost:   12
c ---[9927]---> BDD-cost:   15
c ---[9925]---> BDD-cost:   14
c ---[9924]---> BDD-cost:   12
c ---[9922]---> BDD-cost:   10
c ---[9921]---> BDD-cost:   12
c ---[9920]---> BDD-cost:   14
c ---[9919]---> BDD-cost:   15
c ---[9918]---> BDD-cost:   14
c ---[9917]---> BDD-cost:   13
c ---[9916]---> BDD-cost:   12
c ---[9915]---> BDD-cost:   16
c ---[9908]---> BDD-cost:   19
c ---[9907]---> BDD-cost:   18
c ---[9906]---> BDD-cost:   18
c ---[9905]---> BDD-cost:   18
c ---[9904]---> BDD-cost:   18
c ---[9903]---> BDD-cost:   18
c ---[9902]---> BDD-cost:   18
c ---[9901]---> BDD-cost:   20
c ---[9900]---> BDD-cost:   18
c ---[9893]---> BDD-cost:   20
c ---[9892]---> BDD-cost:   19
c ---[9891]---> BDD-cost:   19
c ---[9890]---> BDD-cost:   19
c ---[9886]---> BDD-cost:   21
c ---[9885]---> BDD-cost:   18
c ---[9878]---> BDD-cost:   21
c ---[9877]---> BDD-cost:   19
c ---[9876]---> BDD-cost:   19
c ---[9875]---> BDD-cost:   19
c ---[9871]---> BDD-cost:   22
c ---[9865]---> BDD-cost:   19
c ---[9864]---> BDD-cost:   18
c ---[9863]---> BDD-cost:   18
c ---[9862]---> BDD-cost:   18
c ---[9861]---> BDD-cost:   18
c ---[9860]---> BDD-cost:   18
c ---[9859]---> BDD-cost:   20
c ---[9858]---> BDD-cost:   18
c ---[9852]---> BDD-cost:   20
c ---[9849]---> BDD-cost:   19
c ---[9846]---> BDD-cost:   21
c ---[9845]---> BDD-cost:   18
c ---[9839]---> BDD-cost:   21
c ---[9836]---> BDD-cost:   19
c ---[9827]---> BDD-cost:   18
c ---[9826]---> BDD-cost:   18
c ---[9825]---> BDD-cost:   18
c ---[9824]---> BDD-cost:   18
c ---[9815]---> BDD-cost:   19
c ---[9814]---> BDD-cost:   19
c ---[9813]---> BDD-cost:   19
c ---[9804]---> BDD-cost:   19
c ---[9803]---> BDD-cost:   19
c ---[9802]---> BDD-cost:   19
c ---[9801]---> BDD-cost:   21
c ---[9795]---> BDD-cost:   19
c ---[9794]---> BDD-cost:   18
c ---[9793]---> BDD-cost:   18
c ---[9791]---> BDD-cost:   18
c ---[9790]---> BDD-cost:   18
c ---[9789]---> BDD-cost:   20
c ---[9788]---> BDD-cost:   18
c ---[9782]---> BDD-cost:   20
c ---[9778]---> BDD-cost:   19
c ---[9776]---> BDD-cost:   21
c ---[9775]---> BDD-cost:   18
c ---[9769]---> BDD-cost:   21
c ---[9765]---> BDD-cost:   19
c ---[9755]---> BDD-cost:   19
c ---[9754]---> BDD-cost:   18
c ---[9753]---> BDD-cost:   18
c ---[9752]---> BDD-cost:   18
c ---[9751]---> BDD-cost:   18
c ---[9750]---> BDD-cost:   18
c ---[9749]---> BDD-cost:   18
c ---[9748]---> BDD-cost:   18
c ---[9747]---> BDD-cost:   20
c ---[9746]---> BDD-cost:   18
c ---[9738]---> BDD-cost:   20
c ---[9737]---> BDD-cost:   19
c ---[9734]---> BDD-cost:   19
c ---[9732]---> BDD-cost:   19
c ---[9730]---> BDD-cost:   21
c ---[9729]---> BDD-cost:   18
c ---[9721]---> BDD-cost:   21
c ---[9720]---> BDD-cost:   19
c ---[9717]---> BDD-cost:   19
c ---[9715]---> BDD-cost:   19
c ---[9713]---> BDD-cost:   22
c ---[9706]---> BDD-cost:   19
c ---[9705]---> BDD-cost:   18
c ---[9704]---> BDD-cost:   18
c ---[9703]---> BDD-cost:   18
c ---[9702]---> BDD-cost:   18
c ---[9701]---> BDD-cost:   18
c ---[9700]---> BDD-cost:   18
c ---[9699]---> BDD-cost:   20
c ---[9698]---> BDD-cost:   18
c ---[9691]---> BDD-cost:   20
c ---[9690]---> BDD-cost:   19
c ---[9688]---> BDD-cost:   19
c ---[9687]---> BDD-cost:   19
c ---[9686]---> BDD-cost:   19
c ---[9684]---> BDD-cost:   21
c ---[9683]---> BDD-cost:   18
c ---[9676]---> BDD-cost:   21
c ---[9675]---> BDD-cost:   19
c ---[9673]---> BDD-cost:   19
c ---[9672]---> BDD-cost:   19
c ---[9671]---> BDD-cost:   19
c ---[9669]---> BDD-cost:   22
c ---[9662]---> BDD-cost:   19
c ---[9661]---> BDD-cost:   18
c ---[9660]---> BDD-cost:   18
c ---[9659]---> BDD-cost:   18
c ---[9658]---> BDD-cost:   18
c ---[9657]---> BDD-cost:   18
c ---[9656]---> BDD-cost:   18
c ---[9655]---> BDD-cost:   20
c ---[9654]---> BDD-cost:   18
c ---[9647]---> BDD-cost:   20
c ---[9645]---> BDD-cost:   19
c ---[9642]---> BDD-cost:   19
c ---[9641]---> BDD-cost:   19
c ---[9640]---> BDD-cost:   21
c ---[9639]---> BDD-cost:   18
c ---[9632]---> BDD-cost:   21
c ---[9630]---> BDD-cost:   19
c ---[9627]---> BDD-cost:   19
c ---[9626]---> BDD-cost:   19
c ---[9625]---> BDD-cost:   22
c ---[9619]---> BDD-cost:   18
c ---[9618]---> BDD-cost:   18
c ---[9617]---> BDD-cost:   18
c ---[9616]---> BDD-cost:   18
c ---[9608]---> BDD-cost:   19
c ---[9597]---> BDD-cost:   19
c ---[9593]---> BDD-cost:   21
c ---[9586]---> BDD-cost:   19
c ---[9585]---> BDD-cost:   18
c ---[9582]---> BDD-cost:   18
c ---[9581]---> BDD-cost:   18
c ---[9580]---> BDD-cost:   18
c ---[9579]---> BDD-cost:   20
c ---[9578]---> BDD-cost:   18
c ---[9571]---> BDD-cost:   20
c ---[9567]---> BDD-cost:   19
c ---[9565]---> BDD-cost:   19
c ---[9564]---> BDD-cost:   21
c ---[9563]---> BDD-cost:   18
c ---[9556]---> BDD-cost:   21
c ---[9552]---> BDD-cost:   19
c ---[9550]---> BDD-cost:   19
c ---[9543]---> BDD-cost:   18
c ---[9542]---> BDD-cost:   18
c ---[9541]---> BDD-cost:   18
c ---[9540]---> BDD-cost:   18
c ---[9531]---> BDD-cost:   19
c ---[9530]---> BDD-cost:   19
c ---[9520]---> BDD-cost:   19
c ---[9519]---> BDD-cost:   19
c ---[9517]---> BDD-cost:   21
c ---[9510]---> BDD-cost:   18
c ---[9509]---> BDD-cost:   18
c ---[9508]---> BDD-cost:   18
c ---[9498]---> BDD-cost:   19
c ---[9497]---> BDD-cost:   19
c ---[9487]---> BDD-cost:   19
c ---[9486]---> BDD-cost:   19
c ---[9485]---> BDD-cost:   21
c ---[9478]---> BDD-cost:   18
c ---[9476]---> BDD-cost:   18
c ---[9465]---> BDD-cost:   19
c ---[9454]---> BDD-cost:   19
c ---[9445]---> BDD-cost:   19
c ---[9444]---> BDD-cost:   18
c ---[9442]---> BDD-cost:   18
c ---[9441]---> BDD-cost:   18
c ---[9439]---> BDD-cost:   18
c ---[9438]---> BDD-cost:   18
c ---[9437]---> BDD-cost:   20
c ---[9436]---> BDD-cost:   18
c ---[9428]---> BDD-cost:   20
c ---[9424]---> BDD-cost:   19
c ---[9422]---> BDD-cost:   19
c ---[9421]---> BDD-cost:   19
c ---[9420]---> BDD-cost:   21
c ---[9419]---> BDD-cost:   18
c ---[9411]---> BDD-cost:   21
c ---[9407]---> BDD-cost:   19
c ---[9405]---> BDD-cost:   19
c ---[9404]---> BDD-cost:   19
c ---[9403]---> BDD-cost:   22
c ---[9397]---> BDD-cost:   19
c ---[9396]---> BDD-cost:   18
c ---[9395]---> BDD-cost:   18
c ---[9394]---> BDD-cost:   18
c ---[9391]---> BDD-cost:   20
c ---[9390]---> BDD-cost:   18
c ---[9384]---> BDD-cost:   20
c ---[9383]---> BDD-cost:   19
c ---[9382]---> BDD-cost:   19
c ---[9378]---> BDD-cost:   21
c ---[9377]---> BDD-cost:   18
c ---[9371]---> BDD-cost:   21
c ---[9370]---> BDD-cost:   19
c ---[9369]---> BDD-cost:   19
c ---[9358]---> BDD-cost:   19
c ---[9356]---> BDD-cost:   18
c ---[9355]---> BDD-cost:   18
c ---[9354]---> BDD-cost:   18
c ---[9353]---> BDD-cost:   18
c ---[9351]---> BDD-cost:   20
c ---[9350]---> BDD-cost:   18
c ---[9343]---> BDD-cost:   20
c ---[9341]---> BDD-cost:   19
c ---[9340]---> BDD-cost:   19
c ---[9338]---> BDD-cost:   19
c ---[9336]---> BDD-cost:   21
c ---[9335]---> BDD-cost:   18
c ---[9328]---> BDD-cost:   21
c ---[9326]---> BDD-cost:   19
c ---[9325]---> BDD-cost:   19
c ---[9323]---> BDD-cost:   19
c ---[9314]---> BDD-cost:   18
c ---[9313]---> BDD-cost:   18
c ---[9312]---> BDD-cost:   18
c ---[9302]---> BDD-cost:   19
c ---[9301]---> BDD-cost:   19
c ---[9291]---> BDD-cost:   19
c ---[9290]---> BDD-cost:   19
c ---[9289]---> BDD-cost:   21
c ---[9288]---> Adder-cost: 13148   maxlim: 209736   bits: 18/18
c ---[9287]---> BDD-cost:    9
c ---[9285]---> BDD-cost:   34
c ---[9283]---> BDD-cost:   58
c ---[9281]---> BDD-cost:   58
c ---[9279]---> Adder-cost: 796   maxlim: 52428700000   bits: 37/36
c ---[9277]---> BDD-cost:   58
c ---[9275]---> BDD-cost:   58
c ---[9273]---> Adder-cost: 699   maxlim: 41724896400   bits: 36/36
c ---[9271]---> BDD-cost:  172
c ---[9269]---> BDD-cost:   58
c ---[9267]---> BDD-cost:  549
c ---[9265]---> BDD-cost:  519
c ---[9263]---> BDD-cost:   40
c ---[9261]---> BDD-cost:  172
c ---[9259]---> BDD-cost:   58
c ---[9257]---> Adder-cost: 524   maxlim: 6553587500   bits: 34/33
c ---[9255]---> BDD-cost:   40
c ---[9253]---> BDD-cost:   40
c ---[9251]---> Adder-cost: 496   maxlim: 3658818123   bits: 33/32
c ---[9250]---> BDD-cost:    9
c ---[9248]---> Sorter-

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/566/stat): 566 (minisat+_script) R 565 566 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855518257 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/566/statm): 174 3 169 147 0 27 0
[pid=566] 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=567
New process pid=568
New process pid=569
One traced child (pid=568) exited with status: 0
execve syscall for /bin/sed executable
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=569) exited with status: 0
One traced child (pid=567) exited with status: 0
New process pid=570
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-mod011.opb

[startup+10.0041 s]
Raw data (loadavg): 0.94 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 20914 0 0 0 819 97 0 0 25 0 1 0 1855518262 82919424 18086 4294967295 134512640 135094434 3221224432 3221223248 134580034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20244 18086 145 145 0 20099 0
[pid=570] vsize: 80976
Current children cumulated CPU time (s) 9.16
Current children cumulated vsize (Kb) 83100

[startup+20.005 s]
Raw data (loadavg): 0.95 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 26736 0 0 0 1789 115 0 0 25 0 1 0 1855518262 84856832 18408 4294967295 134512640 135094434 3221224432 3221218992 134677287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20717 18408 145 145 0 20572 0
[pid=570] vsize: 82868
Current children cumulated CPU time (s) 19.04
Current children cumulated vsize (Kb) 84992

[startup+30.0058 s]
Raw data (loadavg): 0.95 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 26736 0 0 0 2790 115 0 0 25 0 1 0 1855518262 84856832 18408 4294967295 134512640 135094434 3221224432 3221219696 134676519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20717 18408 145 145 0 20572 0
[pid=570] vsize: 82868
Current children cumulated CPU time (s) 29.05
Current children cumulated vsize (Kb) 84992

[startup+40.0066 s]
Raw data (loadavg): 0.96 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 26736 0 0 0 3790 115 0 0 25 0 1 0 1855518262 84856832 18408 4294967295 134512640 135094434 3221224432 3221220400 134676516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20717 18408 145 145 0 20572 0
[pid=570] vsize: 82868
Current children cumulated CPU time (s) 39.05
Current children cumulated vsize (Kb) 84992

[startup+50.0075 s]
Raw data (loadavg): 0.97 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 26736 0 0 0 4790 115 0 0 25 0 1 0 1855518262 84856832 18408 4294967295 134512640 135094434 3221224432 3221221376 134677056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20717 18408 145 145 0 20572 0
[pid=570] vsize: 82868
Current children cumulated CPU time (s) 49.05
Current children cumulated vsize (Kb) 84992

[startup+60.0084 s]
Raw data (loadavg): 0.97 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 26736 0 0 0 5790 115 0 0 25 0 1 0 1855518262 84856832 18408 4294967295 134512640 135094434 3221224432 3221220624 134677375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20717 18408 145 145 0 20572 0
[pid=570] vsize: 82868
Current children cumulated CPU time (s) 59.05
Current children cumulated vsize (Kb) 84992

[startup+70.0092 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 26736 0 0 0 6790 115 0 0 25 0 1 0 1855518262 84856832 18408 4294967295 134512640 135094434 3221224432 3221220928 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20717 18408 145 145 0 20572 0
[pid=570] vsize: 82868
Current children cumulated CPU time (s) 69.05
Current children cumulated vsize (Kb) 84992

[startup+80.0101 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 26736 0 0 0 7791 115 0 0 25 0 1 0 1855518262 84856832 18408 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20717 18408 145 145 0 20572 0
[pid=570] vsize: 82868
Current children cumulated CPU time (s) 79.06
Current children cumulated vsize (Kb) 84992

[startup+90.0109 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 26736 0 0 0 8791 115 0 0 25 0 1 0 1855518262 84856832 18408 4294967295 134512640 135094434 3221224432 3221221104 134676545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20717 18408 145 145 0 20572 0
[pid=570] vsize: 82868
Current children cumulated CPU time (s) 89.06
Current children cumulated vsize (Kb) 84992

[startup+100.012 s]
Raw data (loadavg): 0.98 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 26736 0 0 0 9791 115 0 0 25 0 1 0 1855518262 84856832 18408 4294967295 134512640 135094434 3221224432 3221221632 134599982 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20717 18408 145 145 0 20572 0
[pid=570] vsize: 82868
Current children cumulated CPU time (s) 99.06
Current children cumulated vsize (Kb) 84992

[startup+110.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 30979 0 0 0 10764 129 0 0 25 0 1 0 1855518262 84918272 18424 4294967295 134512640 135094434 3221224432 3221219264 134676301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20732 18424 145 145 0 20587 0
[pid=570] vsize: 82928
Current children cumulated CPU time (s) 108.93
Current children cumulated vsize (Kb) 85052

[startup+120.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 30979 0 0 0 11764 130 0 0 25 0 1 0 1855518262 84918272 18424 4294967295 134512640 135094434 3221224432 3221220400 134676601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20732 18424 145 145 0 20587 0
[pid=570] vsize: 82928
Current children cumulated CPU time (s) 118.94
Current children cumulated vsize (Kb) 85052

[startup+130.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 30979 0 0 0 12764 130 0 0 25 0 1 0 1855518262 84918272 18424 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20732 18424 145 145 0 20587 0
[pid=570] vsize: 82928
Current children cumulated CPU time (s) 128.94
Current children cumulated vsize (Kb) 85052

[startup+140.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 30979 0 0 0 13765 130 0 0 25 0 1 0 1855518262 84918272 18424 4294967295 134512640 135094434 3221224432 3221220552 134677149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20732 18424 145 145 0 20587 0
[pid=570] vsize: 82928
Current children cumulated CPU time (s) 138.95
Current children cumulated vsize (Kb) 85052

[startup+150.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 30979 0 0 0 14765 130 0 0 25 0 1 0 1855518262 84918272 18424 4294967295 134512640 135094434 3221224432 3221221200 134677007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20732 18424 145 145 0 20587 0
[pid=570] vsize: 82928
Current children cumulated CPU time (s) 148.95
Current children cumulated vsize (Kb) 85052

[startup+160.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 30979 0 0 0 15765 130 0 0 25 0 1 0 1855518262 84918272 18424 4294967295 134512640 135094434 3221224432 3221221184 134676328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20732 18424 145 145 0 20587 0
[pid=570] vsize: 82928
Current children cumulated CPU time (s) 158.95
Current children cumulated vsize (Kb) 85052

[startup+170.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 30979 0 0 0 16765 130 0 0 25 0 1 0 1855518262 84918272 18424 4294967295 134512640 135094434 3221224432 3221220496 134677042 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20732 18424 145 145 0 20587 0
[pid=570] vsize: 82928
Current children cumulated CPU time (s) 168.95
Current children cumulated vsize (Kb) 85052

[startup+180.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 30979 0 0 0 17765 130 0 0 25 0 1 0 1855518262 84918272 18424 4294967295 134512640 135094434 3221224432 3221221104 134600283 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20732 18424 145 145 0 20587 0
[pid=570] vsize: 82928
Current children cumulated CPU time (s) 178.95
Current children cumulated vsize (Kb) 85052

[startup+190.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 35156 0 0 0 18740 145 0 0 25 0 1 0 1855518262 84975616 18438 4294967295 134512640 135094434 3221224432 3221221100 134600233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/570/statm): 20746 18438 145 145 0 20601 0
[pid=570] vsize: 82984
Current children cumulated CPU time (s) 188.85
Current children cumulated vsize (Kb) 85108

[startup+200.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 39315 0 0 0 19717 158 0 0 25 0 1 0 1855518262 84918272 18424 4294967295 134512640 135094434 3221224432 3221219504 134600162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/570/statm): 20732 18424 145 145 0 20587 0
[pid=570] vsize: 82928
Current children cumulated CPU time (s) 198.75
Current children cumulated vsize (Kb) 85052

[startup+210.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 43158 0 0 0 20696 171 0 0 25 0 1 0 1855518262 84918272 18424 4294967295 134512640 135094434 3221224432 3221219048 134677377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20732 18424 145 145 0 20587 0
[pid=570] vsize: 82928
Current children cumulated CPU time (s) 208.67
Current children cumulated vsize (Kb) 85052

[startup+220.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 46948 0 0 0 21674 184 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221218816 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 218.58
Current children cumulated vsize (Kb) 85100

[startup+230.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 46948 0 0 0 22674 184 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 228.58
Current children cumulated vsize (Kb) 85100

[startup+240.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 46948 0 0 0 23675 184 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 238.59
Current children cumulated vsize (Kb) 85100

[startup+250.022 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 46948 0 0 0 24675 184 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221220496 134676251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 248.59
Current children cumulated vsize (Kb) 85100

[startup+260.023 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 46948 0 0 0 25675 184 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221219968 134677028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 258.59
Current children cumulated vsize (Kb) 85100

[startup+270.024 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 46948 0 0 0 26675 184 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221220672 134676259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 268.59
Current children cumulated vsize (Kb) 85100

[startup+280.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 46948 0 0 0 27675 184 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 278.59
Current children cumulated vsize (Kb) 85100

[startup+290.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 46948 0 0 0 28675 184 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221221256 134676241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 288.59
Current children cumulated vsize (Kb) 85100

[startup+300.025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 46948 0 0 0 29676 184 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221221280 134601168 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 298.6
Current children cumulated vsize (Kb) 85100

[startup+310.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 50726 0 0 0 30654 197 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221219264 134677035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 308.51
Current children cumulated vsize (Kb) 85100

[startup+320.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 50726 0 0 0 31653 198 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221220032 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 318.51
Current children cumulated vsize (Kb) 85100

[startup+330.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 50726 0 0 0 32653 198 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 328.51
Current children cumulated vsize (Kb) 85100

[startup+340.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 50726 0 0 0 33653 198 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 338.51
Current children cumulated vsize (Kb) 85100

[startup+350.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 50726 0 0 0 34653 198 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221220048 134677290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 348.51
Current children cumulated vsize (Kb) 85100

[startup+360.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 50726 0 0 0 35653 198 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221220144 134676317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 358.51
Current children cumulated vsize (Kb) 85100

[startup+370.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 50726 0 0 0 36653 199 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221221280 134600310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 368.52
Current children cumulated vsize (Kb) 85100

[startup+380.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 50726 0 0 0 37653 199 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221220736 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 378.52
Current children cumulated vsize (Kb) 85100

[startup+390.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 50726 0 0 0 38653 199 0 0 25 0 1 0 1855518262 84967424 18436 4294967295 134512640 135094434 3221224432 3221221104 134676542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20744 18436 145 145 0 20599 0
[pid=570] vsize: 82976
Current children cumulated CPU time (s) 388.52
Current children cumulated vsize (Kb) 85100

[startup+400.031 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 67000 0 0 0 39570 246 0 0 20 0 1 0 1855518262 142176256 32403 4294967295 134512640 135094434 3221224432 3221200848 134597430 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 34711 32403 145 145 0 34566 0
[pid=570] vsize: 138844
Current children cumulated CPU time (s) 398.16
Current children cumulated vsize (Kb) 140968

[startup+410.032 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 40538 260 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221218868 134676464 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 407.98
Current children cumulated vsize (Kb) 85044

[startup+420.033 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 41538 261 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221219872 134676519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 417.99
Current children cumulated vsize (Kb) 85044

[startup+430.035 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 42538 261 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221219792 134677007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 427.99
Current children cumulated vsize (Kb) 85044

[startup+440.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 43538 261 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221219520 134600225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 437.99
Current children cumulated vsize (Kb) 85044

[startup+450.036 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 44538 261 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220048 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 447.99
Current children cumulated vsize (Kb) 85044

[startup+460.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 45538 261 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 457.99
Current children cumulated vsize (Kb) 85044

[startup+470.037 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 46538 261 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 467.99
Current children cumulated vsize (Kb) 85044

[startup+480.038 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 47539 261 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220752 134600008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 478
Current children cumulated vsize (Kb) 85044

[startup+490.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 48539 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221219848 134676241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 488.01
Current children cumulated vsize (Kb) 85044

[startup+500.039 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 49539 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 498.01
Current children cumulated vsize (Kb) 85044

[startup+510.04 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 50539 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220048 134676532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 508.01
Current children cumulated vsize (Kb) 85044

[startup+520.041 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 51539 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220400 134677300 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 518.01
Current children cumulated vsize (Kb) 85044

[startup+530.042 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 52540 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220732 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 528.02
Current children cumulated vsize (Kb) 85044

[startup+540.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 53539 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 538.01
Current children cumulated vsize (Kb) 85044

[startup+550.043 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 54540 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 548.02
Current children cumulated vsize (Kb) 85044

[startup+560.044 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 55540 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 558.02
Current children cumulated vsize (Kb) 85044

[startup+570.045 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 56540 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220752 134676480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 568.02
Current children cumulated vsize (Kb) 85044

[startup+580.046 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 57540 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220928 134677366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 578.02
Current children cumulated vsize (Kb) 85044

[startup+590.047 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 58540 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221024 134677056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 588.02
Current children cumulated vsize (Kb) 85044

[startup+600.048 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 59540 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221084 134677150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 598.02
Current children cumulated vsize (Kb) 85044

[startup+610.048 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 60541 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220820 134677085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 608.03
Current children cumulated vsize (Kb) 85044

[startup+620.048 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 61541 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221524 134676335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 618.03
Current children cumulated vsize (Kb) 85044

[startup+630.05 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 62541 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221552 134676301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 628.03
Current children cumulated vsize (Kb) 85044

[startup+640.051 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 63541 262 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220928 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 638.03
Current children cumulated vsize (Kb) 85044

[startup+650.051 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 64541 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220928 134677333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 648.04
Current children cumulated vsize (Kb) 85044

[startup+660.051 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 65541 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 658.04
Current children cumulated vsize (Kb) 85044

[startup+670.052 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 66542 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220836 134677077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 668.05
Current children cumulated vsize (Kb) 85044

[startup+680.053 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 67542 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221728 134677099 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 678.05
Current children cumulated vsize (Kb) 85044

[startup+690.054 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 68542 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221280 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 688.05
Current children cumulated vsize (Kb) 85044

[startup+700.055 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 69542 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221456 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 698.05
Current children cumulated vsize (Kb) 85044

[startup+710.055 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 70543 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220912 134600162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 708.06
Current children cumulated vsize (Kb) 85044

[startup+720.056 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 71542 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221632 134600175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 718.05
Current children cumulated vsize (Kb) 85044

[startup+730.057 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 72543 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221808 134600204 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 728.06
Current children cumulated vsize (Kb) 85044

[startup+740.058 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 73543 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221280 134600019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 738.06
Current children cumulated vsize (Kb) 85044

[startup+750.059 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 74543 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221508 134676608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 748.06
Current children cumulated vsize (Kb) 85044

[startup+760.059 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 75544 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221200 134676999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 758.07
Current children cumulated vsize (Kb) 85044

[startup+770.06 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 76544 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221808 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 768.07
Current children cumulated vsize (Kb) 85044

[startup+780.061 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 69789 0 0 0 77544 263 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221432 134600694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 778.07
Current children cumulated vsize (Kb) 85044

[startup+790.062 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 78427 326 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221218288 134676589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 787.53
Current children cumulated vsize (Kb) 85044

[startup+800.063 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 79427 326 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221219404 134677228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 797.53
Current children cumulated vsize (Kb) 85044

[startup+810.063 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 80427 326 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221219168 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 807.53
Current children cumulated vsize (Kb) 85044

[startup+820.063 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 81428 326 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220320 134676349 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 817.54
Current children cumulated vsize (Kb) 85044

[startup+830.064 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 82428 326 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221219768 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 827.54
Current children cumulated vsize (Kb) 85044

[startup+840.065 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 83428 326 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221219424 134676328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 837.54
Current children cumulated vsize (Kb) 85044

[startup+850.065 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 84428 326 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 847.54
Current children cumulated vsize (Kb) 85044

[startup+860.065 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 85428 326 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220224 134600186 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 857.54
Current children cumulated vsize (Kb) 85044

[startup+870.066 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 86429 326 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220744 134600234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 867.55
Current children cumulated vsize (Kb) 85044

[startup+880.067 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 87429 326 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220656 134676328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 877.55
Current children cumulated vsize (Kb) 85044

[startup+890.068 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 88429 326 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220400 134677248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 887.55
Current children cumulated vsize (Kb) 85044

[startup+900.069 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 89429 326 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221219944 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 897.55
Current children cumulated vsize (Kb) 85044

[startup+910.069 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 90428 328 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 907.56
Current children cumulated vsize (Kb) 85044

[startup+920.07 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 91427 329 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220720 134676993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 917.56
Current children cumulated vsize (Kb) 85044

[startup+930.072 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 92427 329 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 927.56
Current children cumulated vsize (Kb) 85044

[startup+940.073 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 93427 329 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220812 134677228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 937.56
Current children cumulated vsize (Kb) 85044

[startup+950.074 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 94427 330 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220576 134600295 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 947.57
Current children cumulated vsize (Kb) 85044

[startup+960.074 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 95427 330 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220576 134601161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 957.57
Current children cumulated vsize (Kb) 85044

[startup+970.075 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 96427 330 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220752 134676601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 967.57
Current children cumulated vsize (Kb) 85044

[startup+980.076 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 97427 330 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 977.57
Current children cumulated vsize (Kb) 85044

[startup+990.077 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 98427 330 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 987.57
Current children cumulated vsize (Kb) 85044

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 99427 330 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220832 134676328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 997.57
Current children cumulated vsize (Kb) 85044

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 100428 330 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221104 134676516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1007.58
Current children cumulated vsize (Kb) 85044

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 101428 331 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220928 134600254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1017.59
Current children cumulated vsize (Kb) 85044

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 102428 331 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220560 134600167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1027.59
Current children cumulated vsize (Kb) 85044

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 103428 331 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1037.59
Current children cumulated vsize (Kb) 85044

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 104428 331 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220896 134676993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1047.59
Current children cumulated vsize (Kb) 85044

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 105428 331 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221264 134600162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1057.59
Current children cumulated vsize (Kb) 85044

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 106428 331 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220928 134676519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1067.59
Current children cumulated vsize (Kb) 85044

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 107429 331 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221156 134676464 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1077.6
Current children cumulated vsize (Kb) 85044

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 108429 332 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221248 134518676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1087.61
Current children cumulated vsize (Kb) 85044

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 109429 332 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220752 134677363 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1097.61
Current children cumulated vsize (Kb) 85044

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 110429 332 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220928 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1107.61
Current children cumulated vsize (Kb) 85044

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 111429 332 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221456 134599953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1117.61
Current children cumulated vsize (Kb) 85044

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 112430 332 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1127.62
Current children cumulated vsize (Kb) 85044

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 113429 332 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1137.61
Current children cumulated vsize (Kb) 85044

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 114430 332 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221220824 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1147.62
Current children cumulated vsize (Kb) 85044

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 88867 0 0 0 115430 332 0 0 25 0 1 0 1855518262 84910080 18422 4294967295 134512640 135094434 3221224432 3221221552 134676321 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20730 18422 145 145 0 20585 0
[pid=570] vsize: 82920
Current children cumulated CPU time (s) 1157.62
Current children cumulated vsize (Kb) 85044

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.98 0.92 1/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) T 566 566 5929 0 -1 0 90451 0 0 0 116422 336 0 0 25 0 1 0 1855518262 90046464 19676 4294967295 134512640 135094434 3221224432 3221213180 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/570/statm): 21984 19676 145 145 0 21839 0
[pid=570] vsize: 87936
Current children cumulated CPU time (s) 1167.58
Current children cumulated vsize (Kb) 90060

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 93116 0 0 0 117404 345 0 0 25 0 1 0 1855518262 84869120 18412 4294967295 134512640 135094434 3221224432 3221220224 134600612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20720 18412 145 145 0 20575 0
[pid=570] vsize: 82880
Current children cumulated CPU time (s) 1177.49
Current children cumulated vsize (Kb) 85004

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 93116 0 0 0 118403 346 0 0 25 0 1 0 1855518262 84869120 18412 4294967295 134512640 135094434 3221224432 3221220224 134600274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20720 18412 145 145 0 20575 0
[pid=570] vsize: 82880
Current children cumulated CPU time (s) 1187.49
Current children cumulated vsize (Kb) 85004

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 93116 0 0 0 119404 346 0 0 25 0 1 0 1855518262 84869120 18412 4294967295 134512640 135094434 3221224432 3221221104 134600228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20720 18412 145 145 0 20575 0
[pid=570] vsize: 82880
Current children cumulated CPU time (s) 1197.5
Current children cumulated vsize (Kb) 85004

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 93116 0 0 0 120404 346 0 0 25 0 1 0 1855518262 84869120 18412 4294967295 134512640 135094434 3221224432 3221220928 134600274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20720 18412 145 145 0 20575 0
[pid=570] vsize: 82880
Current children cumulated CPU time (s) 1207.5
Current children cumulated vsize (Kb) 85004



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.98 0.92 2/57 570
Raw data (/proc/566/stat): 566 (minisat+_script) S 565 566 5929 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1855518257 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/566/statm): 531 226 485 147 0 384 0
[pid=566] vsize: 2124
Raw data (/proc/570/stat): 570 (minisat+_64-bit) R 566 566 5929 0 -1 0 93116 0 0 0 120404 346 0 0 25 0 1 0 1855518262 84869120 18412 4294967295 134512640 135094434 3221224432 3221220928 134677354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/570/statm): 20720 18412 145 145 0 20575 0
[pid=570] vsize: 82880
Current children cumulated CPU time (s) 1207.5
Current children cumulated vsize (Kb) 85004

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1207.54
CPU user time (s): 1204.05
CPU system time (s): 3.49647
CPU usage (%): 99.7857
Max. virtual memory (cumulated for all children) (Kb): 140968

Verifier Data

ERROR: no interpretation found !