Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-mod011.opb
MD5SUMaffd575590f5a6117d93002dff93565b
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 212680
Biggest coefficient in the objective function 38252041742581760
Number of bits for the biggest coefficient in the objective function 56
Sum of the numbers in the objective function 82366741301042724864
Number of bits of the sum of numbers in the objective function 67
Biggest number in a constraint 38252041742581760
Number of bits of the biggest number in a constraint 56
Biggest sum of numbers in a constraint 82366741301042724864
Number of bits of the biggest sum of numbers67
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables309773
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 constraint24690

Trace number 4495

Launcher Data

LAUNCH ON wulflinc10 THE 2005-09-19 17:42:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2955 boxname=wulflinc10 idbench=611 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  affd575590f5a6117d93002dff93565b  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-mod011.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-mod011.opb
IDLAUNCH: 2955
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        814196 kB
Buffers:         37588 kB
Cached:         155168 kB
SwapCached:        228 kB
Active:          89476 kB
Inactive:       106228 kB
HighTotal:      131008 kB
HighFree:        18200 kB
LowTotal:       903652 kB
LowFree:        795996 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6272 kB
Slab:            19204 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:03:00 (client local time) WITH STATUS 0 IN 1207.59 SECONDS
stats: 2955 7 1207.59 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 10962] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 10347 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ###############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[10799]---> BDD-cost:   16
c ---[10798]---> BDD-cost:   17
c ---[10797]---> BDD-cost:   15
c ---[10796]---> BDD-cost:   17
c ---[10795]---> BDD-cost:   14
c ---[10794]---> BDD-cost:   12
c ---[10793]---> BDD-cost:   16
c ---[10792]---> BDD-cost:   13
c ---[10791]---> BDD-cost:   18
c ---[10790]---> BDD-cost:   14
c ---[10789]---> BDD-cost:   11
c ---[10787]---> BDD-cost:   13
c ---[10786]---> BDD-cost:   17
c ---[10785]---> BDD-cost:   14
c ---[10784]---> BDD-cost:   19
c ---[10783]---> BDD-cost:   19
c ---[10782]---> BDD-cost:   20
c ---[10781]---> BDD-cost:   20
c ---[10780]---> BDD-cost:   21
c ---[10779]---> BDD-cost:   16
c ---[10778]---> BDD-cost:   17
c ---[10776]---> BDD-cost:   17
c ---[10775]---> BDD-cost:   15
c ---[10774]---> BDD-cost:   19
c ---[10773]---> BDD-cost:   17
c ---[10772]---> BDD-cost:   18
c ---[10771]---> BDD-cost:   15
c ---[10769]---> BDD-cost:   14
c ---[10768]---> BDD-cost:   16
c ---[10767]---> BDD-cost:   13
c ---[10766]---> BDD-cost:   14
c ---[10765]---> BDD-cost:   18
c ---[10764]---> BDD-cost:   20
c ---[10763]---> BDD-cost:   13
c ---[10762]---> BDD-cost:   14
c ---[10761]---> BDD-cost:   14
c ---[10759]---> BDD-cost:   15
c ---[10757]---> BDD-cost:   19
c ---[10756]---> BDD-cost:   18
c ---[10755]---> BDD-cost:   17
c ---[10753]---> BDD-cost:   16
c ---[10752]---> BDD-cost:   16
c ---[10751]---> BDD-cost:   19
c ---[10749]---> BDD-cost:   14
c ---[10748]---> BDD-cost:   17
c ---[10747]---> BDD-cost:   16
c ---[10746]---> BDD-cost:   14
c ---[10745]---> BDD-cost:   15
c ---[10744]---> BDD-cost:   14
c ---[10743]---> BDD-cost:   15
c ---[10742]---> BDD-cost:   14
c ---[10741]---> BDD-cost:   18
c ---[10740]---> BDD-cost:   17
c ---[10739]---> BDD-cost:   16
c ---[10738]---> BDD-cost:   16
c ---[10737]---> BDD-cost:   15
c ---[10736]---> BDD-cost:   10
c ---[10735]---> BDD-cost:   11
c ---[10734]---> BDD-cost:   10
c ---[10733]---> BDD-cost:   16
c ---[10732]---> BDD-cost:   16
c ---[10731]---> BDD-cost:   17
c ---[10730]---> BDD-cost:   13
c ---[10729]---> BDD-cost:   17
c ---[10728]---> BDD-cost:   18
c ---[10727]---> BDD-cost:   17
c ---[10724]---> BDD-cost:   20
c ---[10723]---> BDD-cost:   20
c ---[10722]---> BDD-cost:   18
c ---[10721]---> BDD-cost:   15
c ---[10720]---> BDD-cost:   17
c ---[10719]---> BDD-cost:   18
c ---[10718]---> BDD-cost:   18
c ---[10716]---> BDD-cost:   16
c ---[10714]---> BDD-cost:   21
c ---[10713]---> BDD-cost:   18
c ---[10712]---> BDD-cost:   15
c ---[10711]---> BDD-cost:   16
c ---[10708]---> BDD-cost:   19
c ---[10707]---> BDD-cost:   17
c ---[10706]---> BDD-cost:   18
c ---[10705]---> BDD-cost:   16
c ---[10704]---> BDD-cost:   18
c ---[10703]---> BDD-cost:   15
c ---[10702]---> BDD-cost:   17
c ---[10701]---> BDD-cost:   19
c ---[10700]---> BDD-cost:   17
c ---[10699]---> BDD-cost:   20
c ---[10698]---> BDD-cost:   17
c ---[10695]---> BDD-cost:   19
c ---[10694]---> BDD-cost:   17
c ---[10693]---> BDD-cost:   19
c ---[10692]---> BDD-cost:   16
c ---[10691]---> BDD-cost:   14
c ---[10690]---> BDD-cost:   17
c ---[10689]---> BDD-cost:   18
c ---[10687]---> BDD-cost:   18
c ---[10686]---> BDD-cost:   19
c ---[10685]---> BDD-cost:   18
c ---[10683]---> BDD-cost:   14
c ---[10682]---> BDD-cost:   19
c ---[10680]---> BDD-cost:   17
c ---[10679]---> BDD-cost:   19
c ---[10678]---> BDD-cost:   19
c ---[10677]---> BDD-cost:   18
c ---[10675]---> BDD-cost:   13
c ---[10674]---> BDD-cost:   19
c ---[10673]---> BDD-cost:   17
c ---[10672]---> BDD-cost:   19
c ---[10671]---> BDD-cost:   18
c ---[10670]---> BDD-cost:   17
c ---[10669]---> BDD-cost:   18
c ---[10668]---> BDD-cost:   17
c ---[10667]---> BDD-cost:   18
c ---[10666]---> BDD-cost:   16
c ---[10665]---> BDD-cost:   18
c ---[10664]---> BDD-cost:   17
c ---[10663]---> BDD-cost:   16
c ---[10662]---> BDD-cost:   15
c ---[10661]---> BDD-cost:   18
c ---[10660]---> BDD-cost:   17
c ---[10658]---> BDD-cost:   16
c ---[10657]---> BDD-cost:   15
c ---[10656]---> BDD-cost:   18
c ---[10655]---> BDD-cost:   12
c ---[10654]---> BDD-cost:   17
c ---[10653]---> BDD-cost:   15
c ---[10651]---> BDD-cost:   17
c ---[10647]---> BDD-cost:   15
c ---[10646]---> BDD-cost:   16
c ---[10645]---> BDD-cost:   17
c ---[10644]---> BDD-cost:   16
c ---[10643]---> BDD-cost:   19
c ---[10642]---> BDD-cost:   18
c ---[10641]---> BDD-cost:   13
c ---[10640]---> BDD-cost:   19
c ---[10639]---> BDD-cost:   18
c ---[10637]---> BDD-cost:   15
c ---[10636]---> BDD-cost:   14
c ---[10635]---> BDD-cost:   13
c ---[10634]---> BDD-cost:   15
c ---[10633]---> BDD-cost:   19
c ---[10632]---> BDD-cost:   19
c ---[10631]---> BDD-cost:   20
c ---[10629]---> BDD-cost:   19
c ---[10628]---> BDD-cost:   17
c ---[10627]---> BDD-cost:   17
c ---[10626]---> BDD-cost:   18
c ---[10624]---> BDD-cost:   16
c ---[10623]---> BDD-cost:   15
c ---[10622]---> BDD-cost:   19
c ---[10621]---> BDD-cost:   14
c ---[10620]---> BDD-cost:   16
c ---[10618]---> BDD-cost:   18
c ---[10617]---> BDD-cost:   19
c ---[10616]---> BDD-cost:   20
c ---[10615]---> BDD-cost:   19
c ---[10614]---> BDD-cost:   21
c ---[10613]---> BDD-cost:   19
c ---[10612]---> BDD-cost:   15
c ---[10611]---> BDD-cost:   14
c ---[10610]---> BDD-cost:   15
c ---[10609]---> BDD-cost:   18
c ---[10608]---> BDD-cost:   14
c ---[10607]---> BDD-cost:   17
c ---[10606]---> BDD-cost:   16
c ---[10604]---> BDD-cost:   16
c ---[10603]---> BDD-cost:   16
c ---[10602]---> BDD-cost:   14
c ---[10600]---> BDD-cost:   12
c ---[10598]---> BDD-cost:   14
c ---[10597]---> BDD-cost:   18
c ---[10596]---> BDD-cost:   13
c ---[10595]---> BDD-cost:   12
c ---[10594]---> BDD-cost:   15
c ---[10593]---> BDD-cost:   14
c ---[10592]---> BDD-cost:   12
c ---[10591]---> BDD-cost:   13
c ---[10590]---> BDD-cost:   16
c ---[10589]---> BDD-cost:   17
c ---[10588]---> BDD-cost:   16
c ---[10587]---> BDD-cost:   14
c ---[10586]---> BDD-cost:   17
c ---[10583]---> BDD-cost:   18
c ---[10582]---> BDD-cost:   20
c ---[10581]---> BDD-cost:   17
c ---[10580]---> BDD-cost:   18
c ---[10578]---> BDD-cost:   20
c ---[10577]---> BDD-cost:   19
c ---[10576]---> BDD-cost:   16
c ---[10575]---> BDD-cost:   15
c ---[10574]---> BDD-cost:   18
c ---[10573]---> BDD-cost:   13
c ---[10572]---> BDD-cost:   17
c ---[10571]---> BDD-cost:   17
c ---[10569]---> BDD-cost:   15
c ---[10568]---> BDD-cost:   17
c ---[10567]---> BDD-cost:   17
c ---[10566]---> BDD-cost:   18
c ---[10565]---> BDD-cost:   15
c ---[10564]---> BDD-cost:   13
c ---[10563]---> BDD-cost:   18
c ---[10562]---> BDD-cost:   14
c ---[10561]---> BDD-cost:   17
c ---[10560]---> BDD-cost:   17
c ---[10559]---> BDD-cost:   15
c ---[10558]---> BDD-cost:   18
c ---[10557]---> BDD-cost:   18
c ---[10556]---> BDD-cost:   16
c ---[10555]---> BDD-cost:   13
c ---[10552]---> BDD-cost:   15
c ---[10551]---> BDD-cost:   16
c ---[10548]---> BDD-cost:   13
c ---[10545]---> BDD-cost:   17
c ---[10544]---> BDD-cost:   16
c ---[10542]---> BDD-cost:   17
c ---[10541]---> BDD-cost:   17
c ---[10539]---> BDD-cost:   18
c ---[10538]---> BDD-cost:   16
c ---[10537]---> BDD-cost:   15
c ---[10536]---> BDD-cost:   17
c ---[10535]---> BDD-cost:   15
c ---[10533]---> BDD-cost:   16
c ---[10532]---> BDD-cost:   19
c ---[10531]---> BDD-cost:   18
c ---[10530]---> BDD-cost:   15
c ---[10529]---> BDD-cost:   16
c ---[10528]---> BDD-cost:   17
c ---[10527]---> BDD-cost:   20
c ---[10526]---> BDD-cost:   17
c ---[10525]---> BDD-cost:   15
c ---[10524]---> BDD-cost:   14
c ---[10523]---> BDD-cost:   12
c ---[10521]---> BDD-cost:   16
c ---[10520]---> BDD-cost:   19
c ---[10518]---> BDD-cost:   21
c ---[10517]---> BDD-cost:   15
c ---[10516]---> BDD-cost:   18
c ---[10515]---> BDD-cost:   16
c ---[10510]---> BDD-cost:   17
c ---[10509]---> BDD-cost:   16
c ---[10508]---> BDD-cost:   15
c ---[10507]---> BDD-cost:   16
c ---[10506]---> BDD-cost:   15
c ---[10505]---> BDD-cost:   17
c ---[10504]---> BDD-cost:   15
c ---[10503]---> BDD-cost:   11
c ---[10502]---> BDD-cost:   15
c ---[10501]---> BDD-cost:   17
c ---[10500]---> BDD-cost:   19
c ---[10499]---> BDD-cost:   17
c ---[10497]---> BDD-cost:   15
c ---[10496]---> BDD-cost:   15
c ---[10495]---> BDD-cost:   18
c ---[10494]---> BDD-cost:   16
c ---[10493]---> BDD-cost:   16
c ---[10492]---> BDD-cost:   16
c ---[10491]---> BDD-cost:   19
c ---[10490]---> BDD-cost:   17
c ---[10489]---> BDD-cost:   20
c ---[10488]---> BDD-cost:   17
c ---[10487]---> BDD-cost:   19
c ---[10486]---> BDD-cost:   18
c ---[10485]---> BDD-cost:   16
c ---[10484]---> BDD-cost:   13
c ---[10483]---> BDD-cost:   18
c ---[10482]---> BDD-cost:   19
c ---[10481]---> BDD-cost:   17
c ---[10480]---> BDD-cost:   17
c ---[10479]---> BDD-cost:   17
c ---[10478]---> BDD-cost:   15
c ---[10476]---> BDD-cost:   11
c ---[10475]---> BDD-cost:   13
c ---[10473]---> BDD-cost:   14
c ---[10472]---> BDD-cost:   16
c ---[10471]---> BDD-cost:   17
c ---[10469]---> BDD-cost:   15
c ---[10468]---> BDD-cost:   15
c ---[10466]---> BDD-cost:   17
c ---[10464]---> BDD-cost:   17
c ---[10463]---> BDD-cost:   15
c ---[10462]---> BDD-cost:   11
c ---[10461]---> BDD-cost:   16
c ---[10460]---> BDD-cost:   19
c ---[10459]---> BDD-cost:   18
c ---[10458]---> BDD-cost:   16
c ---[10457]---> BDD-cost:   15
c ---[10455]---> BDD-cost:   17
c ---[10454]---> BDD-cost:   14
c ---[10453]---> BDD-cost:   17
c ---[10452]---> BDD-cost:   15
c ---[10451]---> BDD-cost:   14
c ---[10450]---> BDD-cost:   15
c ---[10449]---> BDD-cost:   18
c ---[10448]---> BDD-cost:   16
c ---[10447]---> BDD-cost:   10
c ---[10446]---> BDD-cost:   15
c ---[10444]---> BDD-cost:   17
c ---[10443]---> BDD-cost:   14
c ---[10441]---> BDD-cost:   12
c ---[10440]---> BDD-cost:   16
c ---[10439]---> BDD-cost:   18
c ---[10437]---> BDD-cost:   17
c ---[10436]---> BDD-cost:   14
c ---[10435]---> BDD-cost:   13
c ---[10434]---> BDD-cost:   15
c ---[10433]---> BDD-cost:   17
c ---[10432]---> BDD-cost:   18
c ---[10428]---> BDD-cost:   13
c ---[10427]---> BDD-cost:   18
c ---[10426]---> BDD-cost:   17
c ---[10424]---> BDD-cost:   18
c ---[10423]---> BDD-cost:   19
c ---[10421]---> BDD-cost:   19
c ---[10420]---> BDD-cost:   15
c ---[10419]---> BDD-cost:   15
c ---[10418]---> BDD-cost:   15
c ---[10416]---> BDD-cost:   17
c ---[10414]---> BDD-cost:   13
c ---[10412]---> BDD-cost:   16
c ---[10411]---> BDD-cost:   17
c ---[10410]---> BDD-cost:   16
c ---[10409]---> BDD-cost:   13
c ---[10408]---> BDD-cost:   15
c ---[10407]---> BDD-cost:   15
c ---[10406]---> BDD-cost:   18
c ---[10402]---> BDD-cost:   17
c ---[10401]---> BDD-cost:   19
c ---[10400]---> BDD-cost:   18
c ---[10399]---> BDD-cost:   15
c ---[10398]---> BDD-cost:   13
c ---[10396]---> BDD-cost:   17
c ---[10395]---> BDD-cost:   19
c ---[10394]---> BDD-cost:   17
c ---[10393]---> BDD-cost:   12
c ---[10392]---> BDD-cost:   12
c ---[10390]---> BDD-cost:   17
c ---[10389]---> BDD-cost:   17
c ---[10388]---> BDD-cost:   20
c ---[10385]---> BDD-cost:   16
c ---[10383]---> BDD-cost:   10
c ---[10382]---> BDD-cost:   13
c ---[10381]---> BDD-cost:   19
c ---[10380]---> BDD-cost:   17
c ---[10379]---> BDD-cost:   17
c ---[10378]---> BDD-cost:   13
c ---[10376]---> BDD-cost:   16
c ---[10375]---> BDD-cost:   18
c ---[10374]---> BDD-cost:   17
c ---[10373]---> BDD-cost:   14
c ---[10372]---> BDD-cost:   14
c ---[10371]---> BDD-cost:   18
c ---[10370]---> BDD-cost:   15
c ---[10369]---> BDD-cost:   15
c ---[10367]---> BDD-cost:   16
c ---[10366]---> BDD-cost:   18
c ---[10365]---> BDD-cost:   15
c ---[10364]---> BDD-cost:   17
c ---[10363]---> BDD-cost:   14
c ---[10362]---> BDD-cost:   16
c ---[10361]---> BDD-cost:   16
c ---[10360]---> BDD-cost:   18
c ---[10359]---> BDD-cost:   17
c ---[10358]---> BDD-cost:   14
c ---[10357]---> BDD-cost:   16
c ---[10356]---> BDD-cost:   15
c ---[10355]---> BDD-cost:   18
c ---[10354]---> BDD-cost:   17
c ---[10353]---> BDD-cost:   17
c ---[10352]---> BDD-cost:   14
c ---[10351]---> BDD-cost:   15
c ---[10350]---> BDD-cost:   18
c ---[10349]---> BDD-cost:   17
c ---[10348]---> BDD-cost:   15
c ---[10346]---> BDD-cost:   18
c ---[10345]---> BDD-cost:   19
c ---[10344]---> BDD-cost:   11
c ---[10343]---> BDD-cost:   11
c ---[10342]---> BDD-cost:   18
c ---[10341]---> BDD-cost:   21
c ---[10340]---> BDD-cost:   16
c ---[10339]---> BDD-cost:   19
c ---[10337]---> BDD-cost:   19
c ---[10336]---> BDD-cost:   15
c ---[10334]---> BDD-cost:   17
c ---[10333]---> BDD-cost:   20
c ---[10332]---> BDD-cost:   18
c ---[10331]---> BDD-cost:   10
c ---[10329]---> BDD-cost:   18
c ---[10328]---> BDD-cost:   20
c ---[10327]---> BDD-cost:   18
c ---[10326]---> BDD-cost:   18
c ---[10325]---> BDD-cost:   14
c ---[10324]---> BDD-cost:   18
c ---[10323]---> BDD-cost:   20
c ---[10322]---> BDD-cost:   18
c ---[10321]---> BDD-cost:   19
c ---[10320]---> BDD-cost:   17
c ---[10319]---> BDD-cost:   15
c ---[10318]---> BDD-cost:   16
c ---[10312]---> BDD-cost:   12
c ---[10310]---> BDD-cost:   15
c ---[10309]---> BDD-cost:   18
c ---[10306]---> BDD-cost:   17
c ---[10304]---> BDD-cost:   15
c ---[10303]---> BDD-cost:   14
c ---[10302]---> BDD-cost:   16
c ---[10301]---> BDD-cost:   20
c ---[10300]---> BDD-cost:   17
c ---[10299]---> BDD-cost:   18
c ---[10298]---> BDD-cost:   13
c ---[10297]---> BDD-cost:   14
c ---[10296]---> BDD-cost:   14
c ---[10295]---> BDD-cost:   15
c ---[10294]---> BDD-cost:   18
c ---[10293]---> BDD-cost:   18
c ---[10292]---> BDD-cost:   17
c ---[10291]---> BDD-cost:   14
c ---[10290]---> BDD-cost:   12
c ---[10287]---> BDD-cost:   15
c ---[10286]---> BDD-cost:   18
c ---[10285]---> BDD-cost:   16
c ---[10284]---> BDD-cost:   14
c ---[10283]---> BDD-cost:   13
c ---[10282]---> BDD-cost:   13
c ---[10281]---> BDD-cost:   15
c ---[10280]---> BDD-cost:   19
c ---[10279]---> BDD-cost:   19
c ---[10278]---> BDD-cost:   19
c ---[10277]---> BDD-cost:   17
c ---[10274]---> BDD-cost:   17
c ---[10273]---> BDD-cost:   20
c ---[10272]---> BDD-cost:   16
c ---[10270]---> BDD-cost:   11
c ---[10269]---> BDD-cost:   14
c ---[10268]---> BDD-cost:   19
c ---[10267]---> BDD-cost:   17
c ---[10266]---> BDD-cost:   14
c ---[10265]---> BDD-cost:   12
c ---[10264]---> BDD-cost:   15
c ---[10263]---> BDD-cost:   19
c ---[10262]---> BDD-cost:   17
c ---[10260]---> BDD-cost:   13
c ---[10259]---> BDD-cost:   13
c ---[10258]---> BDD-cost:   13
c ---[10255]---> BDD-cost:   19
c ---[10254]---> BDD-cost:   17
c ---[10253]---> BDD-cost:   17
c ---[10252]---> BDD-cost:   14
c ---[10250]---> BDD-cost:   20
c ---[10249]---> BDD-cost:   18
c ---[10248]---> BDD-cost:   16
c ---[10247]---> BDD-cost:   14
c ---[10246]---> BDD-cost:   16
c ---[10244]---> BDD-cost:   10
c ---[10243]---> BDD-cost:   13
c ---[10242]---> BDD-cost:   17
c ---[10241]---> BDD-cost:   19
c ---[10240]---> BDD-cost:   19
c ---[10237]---> BDD-cost:   16
c ---[10236]---> BDD-cost:   16
c ---[10235]---> BDD-cost:   18
c ---[10231]---> BDD-cost:   15
c ---[10230]---> BDD-cost:   17
c ---[10229]---> BDD-cost:   17
c ---[10228]---> BDD-cost:   17
c ---[10227]---> BDD-cost:   14
c ---[10225]---> BDD-cost:   19
c ---[10222]---> BDD-cost:   18
c ---[10220]---> BDD-cost:   17
c ---[10219]---> BDD-cost:   17
c ---[10218]---> BDD-cost:   18
c ---[10217]---> BDD-cost:   17
c ---[10216]---> BDD-cost:   14
c ---[10214]---> BDD-cost:   16
c ---[10213]---> BDD-cost:   19
c ---[10212]---> BDD-cost:   15
c ---[10211]---> BDD-cost:   16
c ---[10210]---> BDD-cost:   13
c ---[10209]---> BDD-cost:   10
c ---[10208]---> BDD-cost:   15
c ---[10207]---> BDD-cost:   18
c ---[10206]---> BDD-cost:   18
c ---[10205]---> BDD-cost:   12
c ---[10204]---> BDD-cost:   17
c ---[10203]---> BDD-cost:   16
c ---[10202]---> BDD-cost:   14
c ---[10198]---> BDD-cost:   18
c ---[10197]---> BDD-cost:   18
c ---[10196]---> BDD-cost:   20
c ---[10195]---> BDD-cost:   16
c ---[10194]---> BDD-cost:   16
c ---[10193]---> BDD-cost:   20
c ---[10191]---> BDD-cost:   17
c ---[10190]---> BDD-cost:   16
c ---[10189]---> BDD-cost:   14
c ---[10188]---> BDD-cost:   15
c ---[10187]---> BDD-cost:   18
c ---[10186]---> BDD-cost:   17
c ---[10185]---> BDD-cost:   15
c ---[10184]---> BDD-cost:   14
c ---[10181]---> BDD-cost:   15
c ---[10180]---> BDD-cost:   17
c ---[10179]---> BDD-cost:   19
c ---[10177]---> BDD-cost:   20
c ---[10175]---> BDD-cost:   19
c ---[10174]---> BDD-cost:   10
c ---[10173]---> BDD-cost:   19
c ---[10172]---> BDD-cost:   15
c ---[10171]---> BDD-cost:   14
c ---[10170]---> BDD-cost:   15
c ---[10169]---> BDD-cost:   18
c ---[10168]---> BDD-cost:   16
c ---[10167]---> BDD-cost:   13
c ---[10166]---> BDD-cost:   17
c ---[10165]---> BDD-cost:   19
c ---[10164]---> BDD-cost:   16
c ---[10163]---> BDD-cost:   15
c ---[10162]---> BDD-cost:   11
c ---[10161]---> BDD-cost:   15
c ---[10160]---> BDD-cost:   19
c ---[10159]---> BDD-cost:   19
c ---[10158]---> BDD-cost:   19
c ---[10157]---> BDD-cost:   15
c ---[10156]---> BDD-cost:   19
c ---[10154]---> BDD-cost:   17
c ---[10153]---> BDD-cost:   18
c ---[10152]---> BDD-cost:   17
c ---[10151]---> BDD-cost:   15
c ---[10150]---> BDD-cost:   13
c ---[10149]---> BDD-cost:   16
c ---[10148]---> BDD-cost:   20
c ---[10147]---> BDD-cost:   12
c ---[10146]---> BDD-cost:   18
c ---[10145]---> BDD-cost:   16
c ---[10144]---> BDD-cost:   13
c ---[10143]---> BDD-cost:   14
c ---[10140]---> BDD-cost:   17
c ---[10139]---> BDD-cost:   14
c ---[10138]---> BDD-cost:   14
c ---[10137]---> BDD-cost:   10
c ---[10136]---> BDD-cost:   15
c ---[10135]---> BDD-cost:   18
c ---[10134]---> BDD-cost:   14
c ---[10133]---> BDD-cost:   16
c ---[10132]---> BDD-cost:   19
c ---[10131]---> BDD-cost:   11
c ---[10129]---> BDD-cost:   17
c ---[10128]---> BDD-cost:   16
c ---[10127]---> BDD-cost:   15
c ---[10126]---> BDD-cost:   16
c ---[10125]---> BDD-cost:   17
c ---[10123]---> BDD-cost:   20
c ---[10122]---> BDD-cost:   14
c ---[10120]---> BDD-cost:   15
c ---[10119]---> BDD-cost:   17
c ---[10118]---> BDD-cost:   19
c ---[10116]---> BDD-cost:   14
c ---[10115]---> BDD-cost:   12
c ---[10113]---> BDD-cost:   19
c ---[10111]---> BDD-cost:   15
c ---[10110]---> BDD-cost:   15
c ---[10109]---> BDD-cost:   17
c ---[10108]---> BDD-cost:   18
c ---[10107]---> BDD-cost:   17
c ---[10105]---> BDD-cost:   14
c ---[10103]---> BDD-cost:   16
c ---[10102]---> BDD-cost:   19
c ---[10101]---> BDD-cost:   17
c ---[10100]---> BDD-cost:   18
c ---[10099]---> BDD-cost:   14
c ---[10098]---> BDD-cost:   13
c ---[10097]---> BDD-cost:   16
c ---[10096]---> BDD-cost:   18
c ---[10094]---> BDD-cost:   16
c ---[10093]---> BDD-cost:   16
c ---[10092]---> BDD-cost:   19
c ---[10091]---> BDD-cost:   13
c ---[10090]---> BDD-cost:   19
c ---[10089]---> BDD-cost:   15
c ---[10088]---> BDD-cost:   21
c ---[10087]---> BDD-cost:   15
c ---[10086]---> BDD-cost:   21
c ---[10085]---> BDD-cost:   17
c ---[10084]---> BDD-cost:   14
c ---[10082]---> BDD-cost:   18
c ---[10081]---> BDD-cost:   18
c ---[10080]---> BDD-cost:   15
c ---[10077]---> BDD-cost:   18
c ---[10076]---> BDD-cost:   17
c ---[10074]---> BDD-cost:   13
c ---[10072]---> BDD-cost:   15
c ---[10071]---> BDD-cost:   18
c ---[10069]---> BDD-cost:   13
c ---[10068]---> BDD-cost:   18
c ---[10067]---> BDD-cost:   14
c ---[10065]---> BDD-cost:   19
c ---[10064]---> BDD-cost:   16
c ---[10062]---> BDD-cost:   17
c ---[10061]---> BDD-cost:   18
c ---[10060]---> BDD-cost:   13
c ---[10058]---> BDD-cost:   15
c ---[10057]---> BDD-cost:   18
c ---[10056]---> BDD-cost:   17
c ---[10054]---> BDD-cost:   18
c ---[10053]---> BDD-cost:   17
c ---[10052]---> BDD-cost:   17
c ---[10048]---> BDD-cost:   16
c ---[10047]---> BDD-cost:   15
c ---[10046]---> BDD-cost:   18
c ---[10045]---> BDD-cost:   15
c ---[10044]---> BDD-cost:   18
c ---[10043]---> BDD-cost:   16
c ---[10042]---> BDD-cost:   17
c ---[10041]---> BDD-cost:   14
c ---[10040]---> BDD-cost:   16
c ---[10039]---> BDD-cost:   16
c ---[10038]---> BDD-cost:   18
c ---[10037]---> BDD-cost:   17
c ---[10035]---> BDD-cost:   13
c ---[10034]---> BDD-cost:   17
c ---[10033]---> BDD-cost:   16
c ---[10032]---> BDD-cost:   18
c ---[10031]---> BDD-cost:   15
c ---[10030]---> BDD-cost:   16
c ---[10029]---> BDD-cost:   17
c ---[10028]---> BDD-cost:   15
c ---[10027]---> BDD-cost:   17
c ---[10025]---> BDD-cost:   15
c ---[10024]---> BDD-cost:   18
c ---[10023]---> BDD-cost:   16
c ---[10022]---> BDD-cost:   17
c ---[10021]---> BDD-cost:   14
c ---[10020]---> BDD-cost:   15
c ---[10019]---> BDD-cost:   17
c ---[10018]---> BDD-cost:   16
c ---[10017]---> BDD-cost:   18
c ---[10016]---> BDD-cost:   12
c ---[10015]---> BDD-cost:   15
c ---[10013]---> BDD-cost:   18
c ---[10012]---> BDD-cost:   15
c ---[10011]---> BDD-cost:   17
c ---[10010]---> BDD-cost:   14
c ---[10008]---> BDD-cost:   16
c ---[10007]---> BDD-cost:   18
c ---[10006]---> BDD-cost:   13
c ---[10003]---> BDD-cost:   17
c ---[10001]---> BDD-cost:   15
c ---[10000]---> BDD-cost:   13
c ---[9999]---> BDD-cost:   15
c ---[9998]---> BDD-cost:   17
c ---[9997]---> BDD-cost:   18
c ---[9996]---> BDD-cost:   18
c ---[9995]---> BDD-cost:   16
c ---[9994]---> BDD-cost:   13
c ---[9993]---> BDD-cost:   19
c ---[9992]---> BDD-cost:   16
c ---[9991]---> BDD-cost:   17
c ---[9990]---> BDD-cost:   19
c ---[9989]---> BDD-cost:   16
c ---[9988]---> BDD-cost:   19
c ---[9987]---> BDD-cost:   14
c ---[9984]---> BDD-cost:   19
c ---[9983]---> BDD-cost:   16
c ---[9982]---> BDD-cost:   17
c ---[9981]---> BDD-cost:   13
c ---[9980]---> BDD-cost:   16
c ---[9978]---> BDD-cost:   17
c ---[9977]---> BDD-cost:   13
c ---[9976]---> BDD-cost:   11
c ---[9975]---> BDD-cost:   16
c ---[9974]---> BDD-cost:   17
c ---[9972]---> BDD-cost:   18
c ---[9971]---> BDD-cost:   16
c ---[9970]---> BDD-cost:   13
c ---[9969]---> BDD-cost:   17
c ---[9968]---> BDD-cost:   16
c ---[9967]---> BDD-cost:   19
c ---[9966]---> BDD-cost:   19
c ---[9964]---> BDD-cost:   12
c ---[9963]---> BDD-cost:   14
c ---[9962]---> BDD-cost:   17
c ---[9961]---> BDD-cost:   18
c ---[9960]---> BDD-cost:   20
c ---[9959]---> BDD-cost:   16
c ---[9958]---> BDD-cost:   15
c ---[9957]---> BDD-cost:   13
c ---[9956]---> BDD-cost:   16
c ---[9955]---> BDD-cost:   18
c ---[9954]---> BDD-cost:   19
c ---[9953]---> BDD-cost:   16
c ---[9951]---> BDD-cost:   15
c ---[9950]---> BDD-cost:   17
c ---[9948]---> BDD-cost:   18
c ---[9947]---> BDD-cost:   16
c ---[9946]---> BDD-cost:   15
c ---[9945]---> BDD-cost:   16
c ---[9944]---> BDD-cost:   19
c ---[9942]---> BDD-cost:   18
c ---[9941]---> BDD-cost:   15
c ---[9940]---> BDD-cost:   15
c ---[9938]---> BDD-cost:   18
c ---[9936]---> BDD-cost:   17
c ---[9935]---> BDD-cost:   15
c ---[9933]---> BDD-cost:   13
c ---[9932]---> BDD-cost:   15
c ---[9931]---> BDD-cost:   17
c ---[9930]---> BDD-cost:   18
c ---[9929]---> BDD-cost:   17
c ---[9928]---> BDD-cost:   16
c ---[9927]---> BDD-cost:   15
c ---[9926]---> BDD-cost:   19
c ---[9919]---> BDD-cost:   22
c ---[9918]---> BDD-cost:   21
c ---[9917]---> BDD-cost:   21
c ---[9916]---> BDD-cost:   21
c ---[9915]---> BDD-cost:   21
c ---[9914]---> BDD-cost:   21
c ---[9913]---> BDD-cost:   21
c ---[9912]---> BDD-cost:   23
c ---[9911]---> BDD-cost:   21
c ---[9904]---> BDD-cost:   23
c ---[9903]---> BDD-cost:   22
c ---[9902]---> BDD-cost:   22
c ---[9901]---> BDD-cost:   22
c ---[9900]---> BDD-cost:   22
c ---[9899]---> BDD-cost:   22
c ---[9898]---> BDD-cost:   22
c ---[9897]---> BDD-cost:   24
c ---[9896]---> BDD-cost:   21
c ---[9889]---> BDD-cost:   24
c ---[9888]---> BDD-cost:   22
c ---[9887]---> BDD-cost:   22
c ---[9886]---> BDD-cost:   22
c ---[9885]---> BDD-cost:   22
c ---[9884]---> BDD-cost:   22
c ---[9883]---> BDD-cost:   22
c ---[9882]---> BDD-cost:   25
c ---[9876]---> BDD-cost:   22
c ---[9875]---> BDD-cost:   21
c ---[9874]---> BDD-cost:   21
c ---[9873]---> BDD-cost:   21
c ---[9872]---> BDD-cost:   21
c ---[9871]---> BDD-cost:   21
c ---[9870]---> BDD-cost:   23
c ---[9869]---> BDD-cost:   21
c ---[9863]---> BDD-cost:   23
c ---[9862]---> BDD-cost:   22
c ---[9861]---> BDD-cost:   22
c ---[9860]---> BDD-cost:   22
c ---[9859]---> BDD-cost:   22
c ---[9858]---> BDD-cost:   22
c ---[9857]---> BDD-cost:   24
c ---[9856]---> BDD-cost:   21
c ---[9850]---> BDD-cost:   24
c ---[9849]---> BDD-cost:   22
c ---[9848]---> BDD-cost:   22
c ---[9847]---> BDD-cost:   22
c ---[9846]---> BDD-cost:   22
c ---[9845]---> BDD-cost:   22
c ---[9838]---> BDD-cost:   21
c ---[9837]---> BDD-cost:   21
c ---[9836]---> BDD-cost:   21
c ---[9835]---> BDD-cost:   21
c ---[9827]---> BDD-cost:   22
c ---[9826]---> BDD-cost:   22
c ---[9825]---> BDD-cost:   22
c ---[9824]---> BDD-cost:   22
c ---[9816]---> BDD-cost:   22
c ---[9815]---> BDD-cost:   22
c ---[9814]---> BDD-cost:   22
c ---[9813]---> BDD-cost:   22
c ---[9812]---> BDD-cost:   24
c ---[9806]---> BDD-cost:   22
c ---[9805]---> BDD-cost:   21
c ---[9804]---> BDD-cost:   21
c ---[9802]---> BDD-cost:   21
c ---[9801]---> BDD-cost:   21
c ---[9800]---> BDD-cost:   23
c ---[9799]---> BDD-cost:   21
c ---[9793]---> BDD-cost:   23
c ---[9792]---> BDD-cost:   22
c ---[9791]---> BDD-cost:   22
c ---[9789]---> BDD-cost:   22
c ---[9788]---> BDD-cost:   22
c ---[9787]---> BDD-cost:   24
c ---[9786]---> BDD-cost:   21
c ---[9780]---> BDD-cost:   24
c ---[9779]---> BDD-cost:   22
c ---[9778]---> BDD-cost:   22
c ---[9776]---> BDD-cost:   22
c ---[9775]---> BDD-cost:   22
c ---[9766]---> BDD-cost:   22
c ---[9765]---> BDD-cost:   21
c ---[9764]---> BDD-cost:   21
c ---[9763]---> BDD-cost:   21
c ---[9762]---> BDD-cost:   21
c ---[9761]---> BDD-cost:   21
c ---[9760]---> BDD-cost:   21
c ---[9759]---> BDD-cost:   21
c ---[9758]---> BDD-cost:   23
c ---[9757]---> BDD-cost:   21
c ---[9749]---> BDD-cost:   23
c ---[9748]---> BDD-cost:   22
c ---[9747]---> BDD-cost:   22
c ---[9746]---> BDD-cost:   22
c ---[9745]---> BDD-cost:   22
c ---[9744]---> BDD-cost:   22
c ---[9743]---> BDD-cost:   22
c ---[9742]---> BDD-cost:   22
c ---[9741]---> BDD-cost:   24
c ---[9740]---> BDD-cost:   21
c ---[9732]---> BDD-cost:   24
c ---[9731]---> BDD-cost:   22
c ---[9730]---> BDD-cost:   22
c ---[9729]---> BDD-cost:   22
c ---[9728]---> BDD-cost:   22
c ---[9727]---> BDD-cost:   22
c ---[9726]---> BDD-cost:   22
c ---[9725]---> BDD-cost:   22
c ---[9724]---> BDD-cost:   25
c ---[9717]---> BDD-cost:   22
c ---[9716]---> BDD-cost:   21
c ---[9715]---> BDD-cost:   21
c ---[9714]---> BDD-cost:   21
c ---[9713]---> BDD-cost:   21
c ---[9712]---> BDD-cost:   21
c ---[9711]---> BDD-cost:   21
c ---[9710]---> BDD-cost:   23
c ---[9709]---> BDD-cost:   21
c ---[9702]---> BDD-cost:   23
c ---[9701]---> BDD-cost:   22
c ---[9700]---> BDD-cost:   22
c ---[9699]---> BDD-cost:   22
c ---[9698]---> BDD-cost:   22
c ---[9697]---> BDD-cost:   22
c ---[9696]---> BDD-cost:   22
c ---[9695]---> BDD-cost:   24
c ---[9694]---> BDD-cost:   21
c ---[9687]---> BDD-cost:   24
c ---[9686]---> BDD-cost:   22
c ---[9685]---> BDD-cost:   22
c ---[9684]---> BDD-cost:   22
c ---[9683]---> BDD-cost:   22
c ---[9682]---> BDD-cost:   22
c ---[9681]---> BDD-cost:   22
c ---[9680]---> BDD-cost:   25
c ---[9673]---> BDD-cost:   22
c ---[9672]---> BDD-cost:   21
c ---[9671]---> BDD-cost:   21
c ---[9670]---> BDD-cost:   21
c ---[9669]---> BDD-cost:   21
c ---[9668]---> BDD-cost:   21
c ---[9667]---> BDD-cost:   21
c ---[9666]---> BDD-cost:   23
c ---[9665]---> BDD-cost:   21
c ---[9658]---> BDD-cost:   23
c ---[9657]---> BDD-cost:   22
c ---[9656]---> BDD-cost:   22
c ---[9655]---> BDD-cost:   22
c ---[9654]---> BDD-cost:   22
c ---[9653]---> BDD-cost:   22
c ---[9652]---> BDD-cost:   22
c ---[9651]---> BDD-cost:   24
c ---[9650]---> BDD-cost:   21
c ---[9643]---> BDD-cost:   24
c ---[9642]---> BDD-cost:   22
c ---[9641]---> BDD-cost:   22
c ---[9640]---> BDD-cost:   22
c ---[9639]---> BDD-cost:   22
c ---[9638]---> BDD-cost:   22
c ---[9637]---> BDD-cost:   22
c ---[9636]---> BDD-cost:   25
c ---[9630]---> BDD-cost:   21
c ---[9629]---> BDD-cost:   21
c ---[9628]---> BDD-cost:   21
c ---[9627]---> BDD-cost:   21
c ---[9619]---> BDD-cost:   22
c ---[9618]---> BDD-cost:   22
c ---[9617]---> BDD-cost:   22
c ---[9616]---> BDD-cost:   22
c ---[9608]---> BDD-cost:   22
c ---[9607]---> BDD-cost:   22
c ---[9606]---> BDD-cost:   22
c ---[9605]---> BDD-cost:   22
c ---[9604]---> BDD-cost:   24
c ---[9597]---> BDD-cost:   22
c ---[9596]---> BDD-cost:   21
c ---[9595]---> BDD-cost:   21
c ---[9594]---> BDD-cost:   21
c ---[9593]---> BDD-cost:   21
c ---[9592]---> BDD-cost:   21
c ---[9591]---> BDD-cost:   21
c ---[9590]---> BDD-cost:   23
c ---[9589]---> BDD-cost:   21
c ---[9582]---> BDD-cost:   23
c ---[9581]---> BDD-cost:   22
c ---[9580]---> BDD-cost:   22
c ---[9579]---> BDD-cost:   22
c ---[9578]---> BDD-cost:   22
c ---[9577]---> BDD-cost:   22
c ---[9576]---> BDD-cost:   22
c ---[9575]---> BDD-cost:   24
c ---[9574]---> BDD-cost:   21
c ---[9567]---> BDD-cost:   24
c ---[9566]---> BDD-cost:   22
c ---[9565]---> BDD-cost:   22
c ---[9564]---> BDD-cost:   22
c ---[9563]---> BDD-cost:   22
c ---[9562]---> BDD-cost:   22
c ---[9561]---> BDD-cost:   22
c ---[9560]---> BDD-cost:   25
c ---[9554]---> BDD-cost:   21
c ---[9553]---> BDD-cost:   21
c ---[9552]---> BDD-cost:   21
c ---[9551]---> BDD-cost:   21
c ---[9543]---> BDD-cost:   22
c ---[9542]---> BDD-cost:   22
c ---[9541]---> BDD-cost:   22
c ---[9540]---> BDD-cost:   22
c ---[9532]---> BDD-cost:   22
c ---[9531]---> BDD-cost:   22
c ---[9530]---> BDD-cost:   22
c ---[9529]---> BDD-cost:   22
c ---[9528]---> BDD-cost:   24
c ---[9522]---> BDD-cost:   21
c ---[9521]---> BDD-cost:   21
c ---[9520]---> BDD-cost:   21
c ---[9519]---> BDD-cost:   21
c ---[9511]---> BDD-cost:   22
c ---[9510]---> BDD-cost:   22
c ---[9509]---> BDD-cost:   22
c ---[9508]---> BDD-cost:   22
c ---[9500]---> BDD-cost:   22
c ---[9499]---> BDD-cost:   22
c ---[9498]---> BDD-cost:   22
c ---[9497]---> BDD-cost:   22
c ---[9496]---> BDD-cost:   24
c ---[9489]---> BDD-cost:   21
c ---[9488]---> BDD-cost:   21
c ---[9487]---> BDD-cost:   21
c ---[9478]---> BDD-cost:   22
c ---[9477]---> BDD-cost:   22
c ---[9476]---> BDD-cost:   22
c ---[9467]---> BDD-cost:   22
c ---[9466]---> BDD-cost:   22
c ---[9465]---> BDD-cost:   22
c ---[9464]---> BDD-cost:   24
c ---[9456]---> BDD-cost:   22
c ---[9455]---> BDD-cost:   21
c ---[9454]---> BDD-cost:   21
c ---[9453]---> BDD-cost:   21
c ---[9452]---> BDD-cost:   21
c ---[9451]---> BDD-cost:   21
c ---[9450]---> BDD-cost:   21
c ---[9449]---> BDD-cost:   21
c ---[9448]---> BDD-cost:   23
c ---[9447]---> BDD-cost:   21
c ---[9439]---> BDD-cost:   23
c ---[9438]---> BDD-cost:   22
c ---[9437]---> BDD-cost:   22
c ---[9436]---> BDD-cost:   22
c ---[9435]---> BDD-cost:   22
c ---[9434]---> BDD-cost:   22
c ---[9433]---> BDD-cost:   22
c ---[9432]---> BDD-cost:   22
c ---[9431]---> BDD-cost:   24
c ---[9430]---> BDD-cost:   21
c ---[9422]---> BDD-cost:   24
c ---[9421]---> BDD-cost:   22
c ---[9420]---> BDD-cost:   22
c ---[9419]---> BDD-cost:   22
c ---[9418]---> BDD-cost:   22
c ---[9417]---> BDD-cost:   22
c ---[9416]---> BDD-cost:   22
c ---[9415]---> BDD-cost:   22
c ---[9414]---> BDD-cost:   25
c ---[9408]---> BDD-cost:   22
c ---[9407]---> BDD-cost:   21
c ---[9406]---> BDD-cost:   21
c ---[9405]---> BDD-cost:   21
c ---[9404]---> BDD-cost:   21
c ---[9403]---> BDD-cost:   21
c ---[9402]---> BDD-cost:   23
c ---[9401]---> BDD-cost:   21
c ---[9395]---> BDD-cost:   23
c ---[9394]---> BDD-cost:   22
c ---[9393]---> BDD-cost:   22
c ---[9392]---> BDD-cost:   22
c ---[9391]---> BDD-cost:   22
c ---[9390]---> BDD-cost:   22
c ---[9389]---> BDD-cost:   24
c ---[9388]---> BDD-cost:   21
c ---[9382]---> BDD-cost:   24
c ---[9381]---> BDD-cost:   22
c ---[9380]---> BDD-cost:   22
c ---[9379]---> BDD-cost:   22
c ---[9378]---> BDD-cost:   22
c ---[9377]---> BDD-cost:   22
c ---[9376]---> BDD-cost:   25
c ---[9369]---> BDD-cost:   22
c ---[9368]---> BDD-cost:   21
c ---[9367]---> BDD-cost:   21
c ---[9366]---> BDD-cost:   21
c ---[9365]---> BDD-cost:   21
c ---[9364]---> BDD-cost:   21
c ---[9363]---> BDD-cost:   21
c ---[9362]---> BDD-cost:   23
c ---[9361]---> BDD-cost:   21
c ---[9354]---> BDD-cost:   23
c ---[9353]---> BDD-cost:   22
c ---[9352]---> BDD-cost:   22
c ---[9351]---> BDD-cost:   22
c ---[9350]---> BDD-cost:   22
c ---[9349]---> BDD-cost:   22
c ---[9348]---> BDD-cost:   22
c ---[9347]---> BDD-cost:   24
c ---[9346]---> BDD-cost:   21
c ---[9339]---> BDD-cost:   24
c ---[9338]---> BDD-cost:   22
c ---[9337]---> BDD-cost:   22
c ---[9336]---> BDD-c

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/7197/stat): 7197 (minisat+_script) R 7196 7197 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1793592856 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/7197/statm): 174 3 169 147 0 27 0
[pid=7197] 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=7198
New process pid=7199
New process pid=7200
execve syscall for /bin/sed executable
One traced child (pid=7199) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=7200) exited with status: 0
One traced child (pid=7198) exited with status: 0
New process pid=7201
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-mod011.opb
One traced child (pid=7201) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=7202
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-mod011.opb

[startup+10.0037 s]
Raw data (loadavg): 1.09 1.01 0.73 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) T 7197 7197 22582 0 -1 0 11268 0 3 0 867 49 0 0 25 0 1 0 1793592881 45027328 10221 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/7202/statm): 10993 10221 162 162 0 10831 0
[pid=7202] vsize: 43972
Current children cumulated CPU time (s) 9.2
Current children cumulated vsize (Kb) 46100

[startup+20.0043 s]
Raw data (loadavg): 1.08 1.01 0.73 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 13533 0 3 0 1844 62 0 0 25 0 1 0 1793592881 49127424 11524 4294967295 134512640 135167914 3221224448 3221222652 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 11994 11524 162 162 0 11832 0
[pid=7202] vsize: 47976
Current children cumulated CPU time (s) 19.1
Current children cumulated vsize (Kb) 50104

[startup+30.0049 s]
Raw data (loadavg): 1.06 1.01 0.73 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 16332 0 3 0 2809 79 0 0 25 0 1 0 1793592881 78020608 14323 4294967295 134512640 135167914 3221224448 3221222736 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7202/statm): 19048 14323 162 162 0 18886 0
[pid=7202] vsize: 76192
Current children cumulated CPU time (s) 28.92
Current children cumulated vsize (Kb) 78320

[startup+40.0065 s]
Raw data (loadavg): 1.05 1.01 0.73 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 19445 0 3 0 3769 97 0 0 25 0 1 0 1793592881 89751552 17436 4294967295 134512640 135167914 3221224448 3221223152 134607966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7202/statm): 21912 17436 162 162 0 21750 0
[pid=7202] vsize: 87648
Current children cumulated CPU time (s) 38.7
Current children cumulated vsize (Kb) 89776

[startup+50.008 s]
Raw data (loadavg): 1.05 1.01 0.73 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 22522 0 3 0 4732 113 0 0 25 0 1 0 1793592881 101527552 20513 4294967295 134512640 135167914 3221224448 3221221728 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 24787 20513 162 162 0 24625 0
[pid=7202] vsize: 99148
Current children cumulated CPU time (s) 48.49
Current children cumulated vsize (Kb) 101276

[startup+60.0086 s]
Raw data (loadavg): 1.04 1.01 0.74 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 26170 0 3 0 5690 132 0 0 25 0 1 0 1793592881 111964160 23097 4294967295 134512640 135167914 3221224448 3221222424 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7202/statm): 27335 23097 162 162 0 27173 0
[pid=7202] vsize: 109340
Current children cumulated CPU time (s) 58.26
Current children cumulated vsize (Kb) 111468

[startup+70.0091 s]
Raw data (loadavg): 1.03 1.00 0.74 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 29328 0 3 0 6652 149 0 0 25 0 1 0 1793592881 120885248 25302 4294967295 134512640 135167914 3221224448 3221223136 134581202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 29513 25302 162 162 0 29351 0
[pid=7202] vsize: 118052
Current children cumulated CPU time (s) 68.05
Current children cumulated vsize (Kb) 120180

[startup+80.0097 s]
Raw data (loadavg): 1.03 1.00 0.74 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 32421 0 3 0 7615 167 0 0 25 0 1 0 1793592881 130007040 27545 4294967295 134512640 135167914 3221224448 3221222688 134845109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7202/statm): 31740 27545 162 162 0 31578 0
[pid=7202] vsize: 126960
Current children cumulated CPU time (s) 77.86
Current children cumulated vsize (Kb) 129088

[startup+90.0103 s]
Raw data (loadavg): 1.02 1.00 0.74 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 37729 0 3 0 8571 189 0 0 25 0 1 0 1793592881 151576576 32853 4294967295 134512640 135167914 3221224448 3221223296 134594196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7202/statm): 37006 32853 162 162 0 36844 0
[pid=7202] vsize: 148024
Current children cumulated CPU time (s) 87.64
Current children cumulated vsize (Kb) 150152

[startup+100.011 s]
Raw data (loadavg): 1.02 1.00 0.74 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 37730 0 3 0 9571 190 0 0 25 0 1 0 1793592881 151576576 32854 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 37006 32854 162 162 0 36844 0
[pid=7202] vsize: 148024
Current children cumulated CPU time (s) 97.65
Current children cumulated vsize (Kb) 150152

[startup+110.011 s]
Raw data (loadavg): 1.02 1.00 0.75 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 37730 0 3 0 10571 190 0 0 25 0 1 0 1793592881 151576576 32854 4294967295 134512640 135167914 3221224448 3221223280 134596373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 37006 32854 162 162 0 36844 0
[pid=7202] vsize: 148024
Current children cumulated CPU time (s) 107.65
Current children cumulated vsize (Kb) 150152

[startup+120.013 s]
Raw data (loadavg): 1.01 1.00 0.75 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 37730 0 3 0 11571 190 0 0 25 0 1 0 1793592881 151576576 32854 4294967295 134512640 135167914 3221224448 3221223276 134691200 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 37006 32854 162 162 0 36844 0
[pid=7202] vsize: 148024
Current children cumulated CPU time (s) 117.65
Current children cumulated vsize (Kb) 150152

[startup+130.014 s]
Raw data (loadavg): 1.01 1.00 0.75 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 37730 0 3 0 12571 190 0 0 25 0 1 0 1793592881 151576576 32854 4294967295 134512640 135167914 3221224448 3221223204 134697063 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 37006 32854 162 162 0 36844 0
[pid=7202] vsize: 148024
Current children cumulated CPU time (s) 127.65
Current children cumulated vsize (Kb) 150152

[startup+140.014 s]
Raw data (loadavg): 1.01 1.00 0.75 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 37730 0 3 0 13572 190 0 0 25 0 1 0 1793592881 151576576 32854 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 37006 32854 162 162 0 36844 0
[pid=7202] vsize: 148024
Current children cumulated CPU time (s) 137.66
Current children cumulated vsize (Kb) 150152

[startup+150.016 s]
Raw data (loadavg): 1.01 1.00 0.75 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 37730 0 3 0 14572 190 0 0 25 0 1 0 1793592881 151576576 32854 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 37006 32854 162 162 0 36844 0
[pid=7202] vsize: 148024
Current children cumulated CPU time (s) 147.66
Current children cumulated vsize (Kb) 150152

[startup+160.015 s]
Raw data (loadavg): 1.00 1.00 0.76 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 37731 0 3 0 15572 190 0 0 25 0 1 0 1793592881 151580672 32855 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 37007 32855 162 162 0 36845 0
[pid=7202] vsize: 148028
Current children cumulated CPU time (s) 157.66
Current children cumulated vsize (Kb) 150156

[startup+170.016 s]
Raw data (loadavg): 1.00 1.00 0.76 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 37731 0 3 0 16572 190 0 0 25 0 1 0 1793592881 151580672 32855 4294967295 134512640 135167914 3221224448 3221223280 134596340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 37007 32855 162 162 0 36845 0
[pid=7202] vsize: 148028
Current children cumulated CPU time (s) 167.66
Current children cumulated vsize (Kb) 150156

[startup+180.016 s]
Raw data (loadavg): 1.00 1.00 0.76 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 37740 0 3 0 17572 190 0 0 25 0 1 0 1793592881 151597056 32864 4294967295 134512640 135167914 3221224448 3221223296 134594169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 37011 32864 162 162 0 36849 0
[pid=7202] vsize: 148044
Current children cumulated CPU time (s) 177.66
Current children cumulated vsize (Kb) 150172

[startup+190.018 s]
Raw data (loadavg): 1.00 1.00 0.76 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 38237 0 3 0 18570 192 0 0 25 0 1 0 1793592881 146178048 31545 4294967295 134512640 135167914 3221224448 3219240240 134625625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 35688 31545 162 162 0 35526 0
[pid=7202] vsize: 142752
Current children cumulated CPU time (s) 187.66
Current children cumulated vsize (Kb) 144880

[startup+200.019 s]
Raw data (loadavg): 1.00 1.00 0.76 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 41447 0 3 0 19555 201 0 0 25 0 1 0 1793592881 158552064 34425 4294967295 134512640 135167914 3221224448 3221207920 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 38709 34425 162 162 0 38547 0
[pid=7202] vsize: 154836
Current children cumulated CPU time (s) 197.6
Current children cumulated vsize (Kb) 156964

[startup+210.019 s]
Raw data (loadavg): 1.00 1.00 0.77 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 20508 221 0 0 25 0 1 0 1793592881 178102272 39198 4294967295 134512640 135167914 3221224448 3221223216 134623708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7202/statm): 43482 39198 162 162 0 43320 0
[pid=7202] vsize: 173928
Current children cumulated CPU time (s) 207.33
Current children cumulated vsize (Kb) 176056

[startup+220.021 s]
Raw data (loadavg): 1.00 1.00 0.77 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 21507 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221218272 134843420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 217.33
Current children cumulated vsize (Kb) 170784

[startup+230.021 s]
Raw data (loadavg): 1.00 1.00 0.77 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 22506 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219376 134629445 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 227.32
Current children cumulated vsize (Kb) 170784

[startup+240.023 s]
Raw data (loadavg): 1.00 1.00 0.77 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 23507 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221218928 134843426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 237.33
Current children cumulated vsize (Kb) 170784

[startup+250.023 s]
Raw data (loadavg): 1.00 1.00 0.77 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 24507 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221218768 134695274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 247.33
Current children cumulated vsize (Kb) 170784

[startup+260.024 s]
Raw data (loadavg): 1.00 1.00 0.78 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 25507 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221218584 134842997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 257.33
Current children cumulated vsize (Kb) 170784

[startup+270.024 s]
Raw data (loadavg): 1.00 1.00 0.78 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 26507 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221218384 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 267.33
Current children cumulated vsize (Kb) 170784

[startup+280.025 s]
Raw data (loadavg): 1.00 1.00 0.78 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 27507 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221218576 134696656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 277.33
Current children cumulated vsize (Kb) 170784

[startup+290.027 s]
Raw data (loadavg): 1.00 1.00 0.78 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 28508 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221218960 134522468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 287.34
Current children cumulated vsize (Kb) 170784

[startup+300.027 s]
Raw data (loadavg): 1.00 1.00 0.78 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 29508 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219264 134844720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 297.34
Current children cumulated vsize (Kb) 170784

[startup+310.027 s]
Raw data (loadavg): 1.00 1.00 0.79 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 30508 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219692 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 307.34
Current children cumulated vsize (Kb) 170784

[startup+320.027 s]
Raw data (loadavg): 1.00 1.00 0.79 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 31508 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221218912 134845933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 317.34
Current children cumulated vsize (Kb) 170784

[startup+330.028 s]
Raw data (loadavg): 1.00 1.00 0.79 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 32509 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219304 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 327.35
Current children cumulated vsize (Kb) 170784

[startup+340.027 s]
Raw data (loadavg): 1.00 1.00 0.79 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 33509 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219552 134629183 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 337.35
Current children cumulated vsize (Kb) 170784

[startup+350.028 s]
Raw data (loadavg): 1.00 1.00 0.79 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 34509 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219088 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 347.35
Current children cumulated vsize (Kb) 170784

[startup+360.029 s]
Raw data (loadavg): 1.00 1.00 0.79 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 35509 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219744 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 357.35
Current children cumulated vsize (Kb) 170784

[startup+370.029 s]
Raw data (loadavg): 1.00 1.00 0.80 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 36509 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219616 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 367.35
Current children cumulated vsize (Kb) 170784

[startup+380.03 s]
Raw data (loadavg): 1.00 1.00 0.80 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 37509 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219168 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 377.35
Current children cumulated vsize (Kb) 170784

[startup+390.03 s]
Raw data (loadavg): 1.00 1.00 0.80 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 38510 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219644 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 387.36
Current children cumulated vsize (Kb) 170784

[startup+400.031 s]
Raw data (loadavg): 1.00 1.00 0.80 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 39510 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219952 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 397.36
Current children cumulated vsize (Kb) 170784

[startup+410.031 s]
Raw data (loadavg): 1.00 1.00 0.80 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 40510 222 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219456 134723225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 407.36
Current children cumulated vsize (Kb) 170784

[startup+420.032 s]
Raw data (loadavg): 1.00 1.00 0.81 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 41510 223 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219340 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 417.37
Current children cumulated vsize (Kb) 170784

[startup+430.033 s]
Raw data (loadavg): 1.00 1.00 0.81 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 42510 223 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219040 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 427.37
Current children cumulated vsize (Kb) 170784

[startup+440.032 s]
Raw data (loadavg): 1.00 1.00 0.81 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 43511 223 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219836 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 437.38
Current children cumulated vsize (Kb) 170784

[startup+450.033 s]
Raw data (loadavg): 1.00 1.00 0.81 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 44510 224 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220348 134842996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 447.38
Current children cumulated vsize (Kb) 170784

[startup+460.035 s]
Raw data (loadavg): 1.00 1.00 0.81 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 45510 224 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219872 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 457.38
Current children cumulated vsize (Kb) 170784

[startup+470.036 s]
Raw data (loadavg): 1.00 1.00 0.82 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 46510 224 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220384 134849163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 467.38
Current children cumulated vsize (Kb) 170784

[startup+480.036 s]
Raw data (loadavg): 1.00 1.00 0.82 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 47510 225 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219312 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 477.39
Current children cumulated vsize (Kb) 170784

[startup+490.037 s]
Raw data (loadavg): 1.00 1.00 0.82 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 48510 225 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219604 134843117 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 487.39
Current children cumulated vsize (Kb) 170784

[startup+500.038 s]
Raw data (loadavg): 1.00 1.00 0.82 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 49510 225 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219440 134843160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 497.39
Current children cumulated vsize (Kb) 170784

[startup+510.038 s]
Raw data (loadavg): 1.00 1.00 0.82 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 50510 225 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220384 134694489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 507.39
Current children cumulated vsize (Kb) 170784

[startup+520.039 s]
Raw data (loadavg): 1.00 1.00 0.82 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 51510 225 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220160 134696188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 517.39
Current children cumulated vsize (Kb) 170784

[startup+530.039 s]
Raw data (loadavg): 1.00 1.00 0.82 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 52510 225 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219796 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 527.39
Current children cumulated vsize (Kb) 170784

[startup+540.039 s]
Raw data (loadavg): 1.00 1.00 0.82 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 53510 226 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219676 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 537.4
Current children cumulated vsize (Kb) 170784

[startup+550.039 s]
Raw data (loadavg): 1.00 1.00 0.83 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 54510 226 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220208 134843139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 547.4
Current children cumulated vsize (Kb) 170784

[startup+560.04 s]
Raw data (loadavg): 1.00 1.00 0.83 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 55510 226 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219856 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 557.4
Current children cumulated vsize (Kb) 170784

[startup+570.04 s]
Raw data (loadavg): 1.00 1.00 0.83 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 56510 226 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220336 134696572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 567.4
Current children cumulated vsize (Kb) 170784

[startup+580.041 s]
Raw data (loadavg): 1.00 1.00 0.83 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 57511 226 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220496 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 577.41
Current children cumulated vsize (Kb) 170784

[startup+590.041 s]
Raw data (loadavg): 1.00 1.00 0.83 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 58511 226 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220356 134845880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 587.41
Current children cumulated vsize (Kb) 170784

[startup+600.041 s]
Raw data (loadavg): 1.00 1.00 0.83 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 59511 226 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220192 134522821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 597.41
Current children cumulated vsize (Kb) 170784

[startup+610.041 s]
Raw data (loadavg): 1.00 1.00 0.83 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 60511 226 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220304 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 607.41
Current children cumulated vsize (Kb) 170784

[startup+620.041 s]
Raw data (loadavg): 1.00 1.00 0.83 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 61511 226 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220672 134696738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 617.41
Current children cumulated vsize (Kb) 170784

[startup+630.042 s]
Raw data (loadavg): 1.00 1.00 0.83 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 62511 226 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219792 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 627.41
Current children cumulated vsize (Kb) 170784

[startup+640.041 s]
Raw data (loadavg): 1.00 1.00 0.83 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 63511 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220156 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 637.42
Current children cumulated vsize (Kb) 170784

[startup+650.042 s]
Raw data (loadavg): 1.00 1.00 0.83 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 64511 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220368 134522355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 647.42
Current children cumulated vsize (Kb) 170784

[startup+660.042 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 65512 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220496 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 657.43
Current children cumulated vsize (Kb) 170784

[startup+670.042 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 66512 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220572 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 667.43
Current children cumulated vsize (Kb) 170784

[startup+680.043 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 67512 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220224 134849143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 677.43
Current children cumulated vsize (Kb) 170784

[startup+690.042 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 68512 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219968 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 687.43
Current children cumulated vsize (Kb) 170784

[startup+700.043 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 69512 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220912 134843081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 697.43
Current children cumulated vsize (Kb) 170784

[startup+710.043 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 70512 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220588 134693552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 707.43
Current children cumulated vsize (Kb) 170784

[startup+720.044 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 71513 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219808 134696578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 717.44
Current children cumulated vsize (Kb) 170784

[startup+730.045 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 72513 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221219824 134718191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 727.44
Current children cumulated vsize (Kb) 170784

[startup+740.044 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 73513 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221592 134849087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 737.44
Current children cumulated vsize (Kb) 170784

[startup+750.045 s]
Raw data (loadavg): 1.00 1.00 0.84 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 74513 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220164 134723220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 747.44
Current children cumulated vsize (Kb) 170784

[startup+760.044 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 75513 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220848 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 757.44
Current children cumulated vsize (Kb) 170784

[startup+770.046 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 76514 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221232 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 767.45
Current children cumulated vsize (Kb) 170784

[startup+780.046 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 77514 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220412 134522361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 777.45
Current children cumulated vsize (Kb) 170784

[startup+790.046 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 78514 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220408 134693737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 787.45
Current children cumulated vsize (Kb) 170784

[startup+800.047 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 79514 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220480 134845911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 797.45
Current children cumulated vsize (Kb) 170784

[startup+810.047 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 80514 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220940 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 807.45
Current children cumulated vsize (Kb) 170784

[startup+820.048 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 81515 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221036 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 817.46
Current children cumulated vsize (Kb) 170784

[startup+830.048 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 82515 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220208 134849122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 827.46
Current children cumulated vsize (Kb) 170784

[startup+840.048 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 83515 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220672 134844718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 837.46
Current children cumulated vsize (Kb) 170784

[startup+850.048 s]
Raw data (loadavg): 1.00 1.00 0.85 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 84515 227 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220576 134843030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 847.46
Current children cumulated vsize (Kb) 170784

[startup+860.049 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 85515 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220560 134694511 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 857.47
Current children cumulated vsize (Kb) 170784

[startup+870.051 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 86515 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221376 134845906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 867.47
Current children cumulated vsize (Kb) 170784

[startup+880.051 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 87516 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220544 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 877.48
Current children cumulated vsize (Kb) 170784

[startup+890.052 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 88516 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220656 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 887.48
Current children cumulated vsize (Kb) 170784

[startup+900.052 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 89516 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220528 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 897.48
Current children cumulated vsize (Kb) 170784

[startup+910.052 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 90516 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220524 134723206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 907.48
Current children cumulated vsize (Kb) 170784

[startup+920.052 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 91517 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220880 134695302 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 917.49
Current children cumulated vsize (Kb) 170784

[startup+930.053 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 92517 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220556 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 927.49
Current children cumulated vsize (Kb) 170784

[startup+940.052 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 93517 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220928 134693566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 937.49
Current children cumulated vsize (Kb) 170784

[startup+950.053 s]
Raw data (loadavg): 1.00 1.00 0.86 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 94517 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220928 134693576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 947.49
Current children cumulated vsize (Kb) 170784

[startup+960.053 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 95517 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221200 134845930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 957.49
Current children cumulated vsize (Kb) 170784

[startup+970.053 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 96517 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221080 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 967.49
Current children cumulated vsize (Kb) 170784

[startup+980.054 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 97518 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220848 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 977.5
Current children cumulated vsize (Kb) 170784

[startup+990.053 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 98518 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220672 134845901 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 987.5
Current children cumulated vsize (Kb) 170784

[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 99518 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220732 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 997.5
Current children cumulated vsize (Kb) 170784

[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 100518 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220784 134845915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1007.5
Current children cumulated vsize (Kb) 170784

[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 101518 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220700 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1017.5
Current children cumulated vsize (Kb) 170784

[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 102518 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220032 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1027.5
Current children cumulated vsize (Kb) 170784

[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 103519 228 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221708 134844675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1037.51
Current children cumulated vsize (Kb) 170784

[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 104518 229 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221036 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1047.51
Current children cumulated vsize (Kb) 170784

[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.87 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 105517 230 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221120 134629345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1057.51
Current children cumulated vsize (Kb) 170784

[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 106517 230 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221632 134693582 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1067.51
Current children cumulated vsize (Kb) 170784

[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 107517 231 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221096 134722513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1077.52
Current children cumulated vsize (Kb) 170784

[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 108518 231 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220784 134629451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1087.53
Current children cumulated vsize (Kb) 170784

[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 109517 231 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220760 134693801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1097.52
Current children cumulated vsize (Kb) 170784

[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 110517 231 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220508 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1107.52
Current children cumulated vsize (Kb) 170784

[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 111518 231 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220960 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1117.53
Current children cumulated vsize (Kb) 170784

[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 112518 231 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221200 134696342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1127.53
Current children cumulated vsize (Kb) 170784

[startup+1140.06 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 113518 231 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220168 134723290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1137.53
Current children cumulated vsize (Kb) 170784

[startup+1150.06 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 114518 231 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220704 134695298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1147.53
Current children cumulated vsize (Kb) 170784

[startup+1160.06 s]
Raw data (loadavg): 1.00 1.00 0.88 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 115518 232 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221222176 134631219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1157.54
Current children cumulated vsize (Kb) 170784

[startup+1170.06 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 116518 232 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221632 134849110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1167.54
Current children cumulated vsize (Kb) 170784

[startup+1180.06 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 117519 232 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221088 134849148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1177.55
Current children cumulated vsize (Kb) 170784

[startup+1190.06 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 118519 232 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221276 134849056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1187.55
Current children cumulated vsize (Kb) 170784

[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 119519 232 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221220576 134696565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1197.55
Current children cumulated vsize (Kb) 170784

[startup+1210.06 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 120519 232 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221960 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1207.55
Current children cumulated vsize (Kb) 170784



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 1.00 1.00 0.89 2/57 7202
Raw data (/proc/7197/stat): 7197 (minisat+_script) S 7196 7197 22582 0 -1 0 314 328 0 2 0 1 1 2 17 0 1 0 1793592856 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/7197/statm): 532 234 485 147 0 385 0
[pid=7197] vsize: 2128
Raw data (/proc/7202/stat): 7202 (minisat+_bignum) R 7197 7197 22582 0 -1 0 46879 0 3 0 120519 232 0 0 25 0 1 0 1793592881 172703744 37880 4294967295 134512640 135167914 3221224448 3221221596 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/7202/statm): 42164 37880 162 162 0 42002 0
[pid=7202] vsize: 168656
Current children cumulated CPU time (s) 1207.55
Current children cumulated vsize (Kb) 170784

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1207.59
CPU user time (s): 1205.2
CPU system time (s): 2.39764
CPU usage (%): 99.7895
Max. virtual memory (cumulated for all children) (Kb): 176056

Verifier Data

ERROR: no interpretation found !