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

Nameweb/uclid_pb_benchmarks/normalized-cache.inv14.ucl.opb
MD5SUM5b41c3eb79e4b3bf301d25b20a1c7b76
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
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 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 33
Number of bits of the biggest number in a constraint 6
Biggest sum of numbers in a constraint 126
Number of bits of the biggest sum of numbers7
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables62704
Total number of constraints187107
Number of constraints which are clauses186603
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints504
Minimum length of a constraint1
Maximum length of a constraint11

Trace number 2278

Launcher Data

LAUNCH ON wulflinc15 THE 2005-09-18 18:31:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2653 boxname=wulflinc15 idbench=309 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5b41c3eb79e4b3bf301d25b20a1c7b76  /oldhome/oroussel/tmp/wulflinc15/normalized-cache.inv14.ucl.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-cache.inv14.ucl.opb
IDLAUNCH: 2653
/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:        911104 kB
Buffers:         33672 kB
Cached:          60564 kB
SwapCached:        692 kB
Active:          53804 kB
Inactive:        43076 kB
HighTotal:      131008 kB
HighFree:        67284 kB
LowTotal:       903652 kB
LowFree:        843820 kB
SwapTotal:     2097136 kB
SwapFree:      2095920 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            20860 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:51:58 (client local time) WITH STATUS 0 IN 1209.61 SECONDS
stats: 2653 7 1209.61 0

Solver Data

c Parsing PB file...
c Converting 187106 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[187096]---> BDD-cost:    1
c ---[187091]---> BDD-cost:    1
c ---[187086]---> BDD-cost:    1
c ---[187081]---> BDD-cost:    1
c ---[187076]---> BDD-cost:    1
c ---[187071]---> BDD-cost:    1
c ---[187063]---> BDD-cost:    1
c ---[187058]---> BDD-cost:    1
c ---[187053]---> BDD-cost:    1
c ---[187042]---> BDD-cost:    1
c ---[187037]---> BDD-cost:    1
c ---[187023]---> BDD-cost:    1
c ---[187018]---> BDD-cost:    1
c ---[187013]---> BDD-cost:    1
c ---[186978]---> BDD-cost:    1
c ---[186943]---> BDD-cost:    1
c ---[186935]---> BDD-cost:    1
c ---[186846]---> BDD-cost:    1
c ---[186832]---> BDD-cost:    1
c ---[186818]---> BDD-cost:    1
c ---[186768]---> BDD-cost:    1
c ---[186745]---> BDD-cost:    1
c ---[186740]---> BDD-cost:    1
c ---[186735]---> BDD-cost:    1
c ---[186730]---> BDD-cost:    1
c ---[186650]---> BDD-cost:    1
c ---[186582]---> BDD-cost:    1
c ---[186574]---> BDD-cost:    1
c ---[186371]---> BDD-cost:    1
c ---[186351]---> BDD-cost:    1
c ---[186283]---> BDD-cost:    1
c ---[186263]---> BDD-cost:    1
c ---[186243]---> BDD-cost:    1
c ---[186178]---> BDD-cost:    1
c ---[186101]---> BDD-cost:    1
c ---[186063]---> BDD-cost:    1
c ---[186058]---> BDD-cost:    1
c ---[186053]---> BDD-cost:    1
c ---[186048]---> BDD-cost:    1
c ---[186043]---> BDD-cost:    1
c ---[185897]---> BDD-cost:    1
c ---[185886]---> BDD-cost:    1
c ---[185767]---> BDD-cost:    1
c ---[185723]---> BDD-cost:    1
c ---[185376]---> BDD-cost:    1
c ---[185350]---> BDD-cost:    1
c ---[185222]---> BDD-cost:    1
c ---[185196]---> BDD-cost:    1
c ---[185110]---> BDD-cost:    1
c ---[185084]---> BDD-cost:    1
c ---[185058]---> BDD-cost:    1
c ---[184993]---> BDD-cost:    1
c ---[184856]---> BDD-cost:    1
c ---[184719]---> BDD-cost:    1
c ---[184228]---> BDD-cost:    1
c ---[184196]---> BDD-cost:    1
c ---[183990]---> BDD-cost:    1
c ---[183958]---> BDD-cost:    1
c ---[183803]---> BDD-cost:    1
c ---[183771]---> BDD-cost:    1
c ---[183667]---> BDD-cost:    1
c ---[183635]---> BDD-cost:    1
c ---[183603]---> BDD-cost:    1
c ---[183508]---> BDD-cost:    1
c ---[183482]---> BDD-cost:    1
c ---[183174]---> BDD-cost:    1
c ---[182812]---> BDD-cost:    1
c ---[182795]---> BDD-cost:    1
c ---[182790]---> BDD-cost:    1
c ---[182785]---> BDD-cost:    1
c ---[182780]---> BDD-cost:    1
c ---[182775]---> BDD-cost:    1
c ---[182755]---> BDD-cost:    1
c ---[182621]---> BDD-cost:    1
c ---[182616]---> BDD-cost:    1
c ---[182614]---> BDD-cost:    1
c ---[182612]---> BDD-cost:    1
c ---[182610]---> BDD-cost:    1
c ---[182608]---> BDD-cost:    1
c ---[182606]---> BDD-cost:    1
c ---[182604]---> BDD-cost:    1
c ---[182602]---> BDD-cost:    1
c ---[181988]---> BDD-cost:    1
c ---[181986]---> BDD-cost:    1
c ---[181984]---> BDD-cost:    1
c ---[181982]---> BDD-cost:    1
c ---[181980]---> BDD-cost:    1
c ---[181978]---> BDD-cost:    1
c ---[181973]---> BDD-cost:    1
c ---[181722]---> BDD-cost:    1
c ---[181681]---> BDD-cost:    1
c ---[181640]---> BDD-cost:    1
c ---[181599]---> BDD-cost:    1
c ---[181516]---> BDD-cost:    1
c ---[181337]---> BDD-cost:    1
c ---[181035]---> BDD-cost:    1
c ---[180952]---> BDD-cost:    1
c ---[180734]---> BDD-cost:    1
c ---[180705]---> BDD-cost:    1
c ---[180517]---> BDD-cost:    1
c ---[180464]---> BDD-cost:    1
c ---[180462]---> BDD-cost:    1
c ---[180460]---> BDD-cost:    1
c ---[179747]---> BDD-cost:    1
c ---[179742]---> BDD-cost:    1
c ---[179704]---> BDD-cost:    1
c ---[179402]---> BDD-cost:    1
c ---[179364]---> BDD-cost:    1
c ---[179122]---> BDD-cost:    1
c ---[179084]---> BDD-cost:    1
c ---[178902]---> BDD-cost:    1
c ---[178864]---> BDD-cost:    1
c ---[178742]---> BDD-cost:    1
c ---[178704]---> BDD-cost:    1
c ---[178666]---> BDD-cost:    1
c ---[177197]---> BDD-cost:    1
c ---[177138]---> BDD-cost:    1
c ---[177133]---> BDD-cost:    1
c ---[177128]---> BDD-cost:    1
c ---[177111]---> BDD-cost:    1
c ---[177106]---> BDD-cost:    1
c ---[177068]---> BDD-cost:    1
c ---[177063]---> BDD-cost:    1
c ---[177031]---> BDD-cost:    1
c ---[176996]---> BDD-cost:    1
c ---[175581]---> BDD-cost:    1
c ---[175579]---> BDD-cost:    1
c ---[175553]---> BDD-cost:    1
c ---[175551]---> BDD-cost:    1
c ---[175549]---> BDD-cost:    1
c ---[175547]---> BDD-cost:    1
c ---[175545]---> BDD-cost:    1
c ---[175543]---> BDD-cost:    1
c ---[175538]---> BDD-cost:    1
c ---[175191]---> BDD-cost:    1
c ---[175132]---> BDD-cost:    1
c ---[175082]---> BDD-cost:    1
c ---[175032]---> BDD-cost:    1
c ---[174247]---> BDD-cost:    1
c ---[173807]---> BDD-cost:    1
c ---[173757]---> BDD-cost:    1
c ---[173482]---> BDD-cost:    1
c ---[173423]---> BDD-cost:    1
c ---[173421]---> BDD-cost:    1
c ---[173419]---> BDD-cost:    1
c ---[172964]---> BDD-cost:    1
c ---[172455]---> BDD-cost:    1
c ---[172450]---> BDD-cost:    1
c ---[172406]---> BDD-cost:    1
c ---[171990]---> BDD-cost:    1
c ---[171985]---> BDD-cost:    1
c ---[171941]---> BDD-cost:    1
c ---[171594]---> BDD-cost:    1
c ---[171550]---> BDD-cost:    1
c ---[171272]---> BDD-cost:    1
c ---[171228]---> BDD-cost:    1
c ---[171019]---> BDD-cost:    1
c ---[170975]---> BDD-cost:    1
c ---[170835]---> BDD-cost:    1
c ---[170791]---> BDD-cost:    1
c ---[170747]---> BDD-cost:    1
c ---[167703]---> BDD-cost:    1
c ---[167581]---> BDD-cost:    1
c ---[167576]---> BDD-cost:    1
c ---[167571]---> BDD-cost:    1
c ---[167554]---> BDD-cost:    1
c ---[167549]---> BDD-cost:    1
c ---[167505]---> BDD-cost:    1
c ---[167500]---> BDD-cost:    1
c ---[167498]---> BDD-cost:    1
c ---[167460]---> BDD-cost:    1
c ---[167455]---> BDD-cost:    1
c ---[167402]---> BDD-cost:    1
c ---[167397]---> BDD-cost:    1
c ---[167353]---> BDD-cost:    1
c ---[164348]---> BDD-cost:    1
c ---[164346]---> BDD-cost:    1
c ---[164293]---> BDD-cost:    1
c ---[164291]---> BDD-cost:    1
c ---[164289]---> BDD-cost:    1
c ---[164287]---> BDD-cost:    1
c ---[164285]---> BDD-cost:    1
c ---[164283]---> BDD-cost:    1
c ---[164278]---> BDD-cost:    1
c ---[164141]---> BDD-cost:    1
c ---[164058]---> BDD-cost:    1
c ---[163669]---> BDD-cost:    1
c ---[163583]---> BDD-cost:    1
c ---[163524]---> BDD-cost:    1
c ---[163465]---> BDD-cost:    1
c ---[162119]---> BDD-cost:    1
c ---[161613]---> BDD-cost:    1
c ---[161521]---> BDD-cost:    1
c ---[161141]---> BDD-cost:    1
c ---[161073]---> BDD-cost:    1
c ---[161071]---> BDD-cost:    1
c ---[161069]---> BDD-cost:    1
c ---[160473]---> BDD-cost:    1
c ---[159820]---> BDD-cost:    1
c ---[159815]---> BDD-cost:    1
c ---[159765]---> BDD-cost:    1
c ---[159217]---> BDD-cost:    1
c ---[159212]---> BDD-cost:    1
c ---[159162]---> BDD-cost:    1
c ---[158692]---> BDD-cost:    1
c ---[158687]---> BDD-cost:    1
c ---[158637]---> BDD-cost:    1
c ---[158245]---> BDD-cost:    1
c ---[158195]---> BDD-cost:    1
c ---[157881]---> BDD-cost:    1
c ---[157831]---> BDD-cost:    1
c ---[157595]---> BDD-cost:    1
c ---[157545]---> BDD-cost:    1
c ---[157387]---> BDD-cost:    1
c ---[157337]---> BDD-cost:    1
c ---[157287]---> BDD-cost:    1
c ---[151969]---> BDD-cost:    1
c ---[151643]---> BDD-cost:    1
c ---[151638]---> BDD-cost:    1
c ---[151633]---> BDD-cost:    1
c ---[151595]---> BDD-cost:    1
c ---[151590]---> BDD-cost:    1
c ---[151540]---> BDD-cost:    1
c ---[151535]---> BDD-cost:    1
c ---[151533]---> BDD-cost:    1
c ---[151489]---> BDD-cost:    1
c ---[151484]---> BDD-cost:    1
c ---[151482]---> BDD-cost:    1
c ---[151444]---> BDD-cost:    1
c ---[151439]---> BDD-cost:    1
c ---[151365]---> BDD-cost:    1
c ---[151360]---> BDD-cost:    1
c ---[151355]---> BDD-cost:    1
c ---[151302]---> BDD-cost:    1
c ---[145993]---> BDD-cost:    1
c ---[145991]---> BDD-cost:    1
c ---[145854]---> BDD-cost:    1
c ---[145852]---> BDD-cost:    1
c ---[145850]---> BDD-cost:    1
c ---[145848]---> BDD-cost:    1
c ---[145846]---> BDD-cost:    1
c ---[145844]---> BDD-cost:    1
c ---[145839]---> BDD-cost:    1
c ---[145675]---> BDD-cost:    1
c ---[145553]---> BDD-cost:    1
c ---[145032]---> BDD-cost:    1
c ---[144910]---> BDD-cost:    1
c ---[144842]---> BDD-cost:    1
c ---[144774]---> BDD-cost:    1
c ---[142681]---> BDD-cost:    1
c ---[141821]---> BDD-cost:    1
c ---[141648]---> BDD-cost:    1
c ---[141145]---> BDD-cost:    1
c ---[141068]---> BDD-cost:    1
c ---[141066]---> BDD-cost:    1
c ---[141064]---> BDD-cost:    1
c ---[140312]---> BDD-cost:    1
c ---[139497]---> BDD-cost:    1
c ---[139492]---> BDD-cost:    1
c ---[139436]---> BDD-cost:    1
c ---[138738]---> BDD-cost:    1
c ---[138733]---> BDD-cost:    1
c ---[138677]---> BDD-cost:    1
c ---[138066]---> BDD-cost:    1
c ---[138061]---> BDD-cost:    1
c ---[138005]---> BDD-cost:    1
c ---[137481]---> BDD-cost:    1
c ---[137476]---> BDD-cost:    1
c ---[137420]---> BDD-cost:    1
c ---[136983]---> BDD-cost:    1
c ---[136927]---> BDD-cost:    1
c ---[136577]---> BDD-cost:    1
c ---[136521]---> BDD-cost:    1
c ---[136258]---> BDD-cost:    1
c ---[136202]---> BDD-cost:    1
c ---[136026]---> BDD-cost:    1
c ---[135970]---> BDD-cost:    1
c ---[135914]---> BDD-cost:    1
c ---[127482]---> BDD-cost:    1
c ---[126862]---> BDD-cost:    1
c ---[126830]---> BDD-cost:    1
c ---[126819]---> BDD-cost:    1
c ---[126727]---> BDD-cost:    1
c ---[126569]---> BDD-cost:    1
c ---[126564]---> BDD-cost:    1
c ---[126508]---> BDD-cost:    1
c ---[126503]---> BDD-cost:    1
c ---[126501]---> BDD-cost:    1
c ---[126451]---> BDD-cost:    1
c ---[126446]---> BDD-cost:    1
c ---[126444]---> BDD-cost:    1
c ---[126400]---> BDD-cost:    1
c ---[126395]---> BDD-cost:    1
c ---[126393]---> BDD-cost:    1
c ---[126355]---> BDD-cost:    1
c ---[126350]---> BDD-cost:    1
c ---[126285]---> BDD-cost:    1
c ---[126250]---> BDD-cost:    1
c ---[126245]---> BDD-cost:    1
c ---[126240]---> BDD-cost:    1
c ---[126235]---> BDD-cost:    1
c ---[126173]---> BDD-cost:    1
c ---[117711]---> BDD-cost:    1
c ---[117709]---> BDD-cost:    1
c ---[117371]---> BDD-cost:    1
c ---[117369]---> BDD-cost:    1
c ---[117367]---> BDD-cost:    1
c ---[117365]---> BDD-cost:    1
c ---[117363]---> BDD-cost:    1
c ---[117361]---> BDD-cost:    1
c ---[117356]---> BDD-cost:    1
c ---[117165]---> BDD-cost:    1
c ---[116992]---> BDD-cost:    1
c ---[116324]---> BDD-cost:    1
c ---[116157]---> BDD-cost:    1
c ---[116080]---> BDD-cost:    1
c ---[116003]---> BDD-cost:    1
c ---[112950]---> BDD-cost:    1
c ---[111556]---> BDD-cost:    1
c ---[111287]---> BDD-cost:    1
c ---[110643]---> BDD-cost:    1
c ---[110557]---> BDD-cost:    1
c ---[110555]---> BDD-cost:    1
c ---[110553]---> BDD-cost:    1
c ---[109627]---> BDD-cost:    1
c ---[108632]---> BDD-cost:    1
c ---[108627]---> BDD-cost:    1
c ---[108565]---> BDD-cost:    1
c ---[107699]---> BDD-cost:    1
c ---[107694]---> BDD-cost:    1
c ---[107632]---> BDD-cost:    1
c ---[106862]---> BDD-cost:    1
c ---[106857]---> BDD-cost:    1
c ---[106795]---> BDD-cost:    1
c ---[106121]---> BDD-cost:    1
c ---[106116]---> BDD-cost:    1
c ---[106054]---> BDD-cost:    1
c ---[105476]---> BDD-cost:    1
c ---[105471]---> BDD-cost:    1
c ---[105409]---> BDD-cost:    1
c ---[104927]---> BDD-cost:    1
c ---[104865]---> BDD-cost:    1
c ---[104479]---> BDD-cost:    1
c ---[104417]---> BDD-cost:    1
c ---[104127]---> BDD-cost:    1
c ---[104065]---> BDD-cost:    1
c ---[103871]---> BDD-cost:    1
c ---[103809]---> BDD-cost:    1
c ---[103747]---> BDD-cost:    1
c ---[91226]---> BDD-cost:    1
c ---[90327]---> BDD-cost:    1
c ---[90322]---> BDD-cost:    1
c ---[90281]---> BDD-cost:    1
c ---[90270]---> BDD-cost:    1
c ---[89398]---> BDD-cost:    1
c ---[88847]---> BDD-cost:    1
c ---[88842]---> BDD-cost:    1
c ---[88780]---> BDD-cost:    1
c ---[88775]---> BDD-cost:    1
c ---[88773]---> BDD-cost:    1
c ---[88717]---> BDD-cost:    1
c ---[88712]---> BDD-cost:    1
c ---[88710]---> BDD-cost:    1
c ---[88660]---> BDD-cost:    1
c ---[88655]---> BDD-cost:    1
c ---[88653]---> BDD-cost:    1
c ---[88609]---> BDD-cost:    1
c ---[88604]---> BDD-cost:    1
c ---[88602]---> BDD-cost:    1
c ---[88564]---> BDD-cost:    1
c ---[88559]---> BDD-cost:    1
c ---[88479]---> BDD-cost:    1
c ---[88477]---> BDD-cost:    1
c ---[88433]---> BDD-cost:    1
c ---[88428]---> BDD-cost:    1
c ---[88423]---> BDD-cost:    1
c ---[88418]---> BDD-cost:    1
c ---[88413]---> BDD-cost:    1
c ---[88342]---> BDD-cost:    1
c ---[75743]---> BDD-cost:    1
c ---[75741]---> BDD-cost:    1
c ---[74998]---> BDD-cost:    1
c ---[74996]---> BDD-cost:    1
c ---[74994]---> BDD-cost:    1
c ---[74992]---> BDD-cost:    1
c ---[74990]---> BDD-cost:    1
c ---[74988]---> BDD-cost:    1
c ---[74983]---> BDD-cost:    1
c ---[74765]---> BDD-cost:    1
c ---[74526]---> BDD-cost:    1
c ---[73696]---> BDD-cost:    1
c ---[73475]---> BDD-cost:    1
c ---[73389]---> BDD-cost:    1
c ---[73303]---> BDD-cost:    1
c ---[69050]---> BDD-cost:    1
c ---[66864]---> BDD-cost:    1
c ---[66481]---> BDD-cost:    1
c ---[65678]---> BDD-cost:    1
c ---[65583]---> BDD-cost:    1
c ---[65581]---> BDD-cost:    1
c ---[65579]---> BDD-cost:    1
c ---[64461]---> BDD-cost:    1
c ---[63268]---> BDD-cost:    1
c ---[63263]---> BDD-cost:    1
c ---[63195]---> BDD-cost:    1
c ---[62143]---> BDD-cost:    1
c ---[62138]---> BDD-cost:    1
c ---[62070]---> BDD-cost:    1
c ---[61123]---> BDD-cost:    1
c ---[61118]---> BDD-cost:    1
c ---[61050]---> BDD-cost:    1
c ---[60208]---> BDD-cost:    1
c ---[60203]---> BDD-cost:    1
c ---[60135]---> BDD-cost:    1
c ---[59398]---> BDD-cost:    1
c ---[59393]---> BDD-cost:    1
c ---[59325]---> BDD-cost:    1
c ---[58693]---> BDD-cost:    1
c ---[58688]---> BDD-cost:    1
c ---[58620]---> BDD-cost:    1
c ---[58093]---> BDD-cost:    1
c ---[58025]---> BDD-cost:    1
c ---[57603]---> BDD-cost:    1
c ---[57535]---> BDD-cost:    1
c ---[57218]---> BDD-cost:    1
c ---[57150]---> BDD-cost:    1
c ---[56938]---> BDD-cost:    1
c ---[56870]---> BDD-cost:    1
c ---[56802]---> BDD-cost:    1
c ---[39082]---> BDD-cost:    1
c ---[38117]---> BDD-cost:    1
c ---[38112]---> BDD-cost:    1
c ---[38107]---> BDD-cost:    1
c ---[38057]---> BDD-cost:    1
c ---[38046]---> BDD-cost:    1
c ---[34243]---> BDD-cost:    1
c ---[32576]---> BDD-cost:    1
c ---[32571]---> BDD-cost:    1
c ---[32503]---> BDD-cost:    1
c ---[32498]---> BDD-cost:    1
c ---[32496]---> BDD-cost:    1
c ---[32434]---> BDD-cost:    1
c ---[32429]---> BDD-cost:    1
c ---[32427]---> BDD-cost:    1
c ---[32371]---> BDD-cost:    1
c ---[32366]---> BDD-cost:    1
c ---[32364]---> BDD-cost:    1
c ---[32314]---> BDD-cost:    1
c ---[32309]---> BDD-cost:    1
c ---[32307]---> BDD-cost:    1
c ---[32263]---> BDD-cost:    1
c ---[32258]---> BDD-cost:    1
c ---[32256]---> BDD-cost:    1
c ---[32218]---> BDD-cost:    1
c ---[32213]---> BDD-cost:    1
c ---[32118]---> BDD-cost:    1
c ---[32116]---> BDD-cost:    1
c ---[32114]---> BDD-cost:    1
c ---[32061]---> BDD-cost:    1
c ---[32056]---> BDD-cost:    1
c ---[32051]---> BDD-cost:    1
c ---[32046]---> BDD-cost:    1
c ---[32041]---> BDD-cost:    1
c ---[32036]---> BDD-cost:    1
c ---[31956]---> BDD-cost:    1
c ---[14101]---> BDD-cost:    1
c ---[14099]---> BDD-cost:    1
c ---[12657]---> BDD-cost:    1
c ---[12655]---> BDD-cost:    1
c ---[12653]---> BDD-cost:    1
c ---[12651]---> BDD-cost:    1
c ---[12649]---> BDD-cost:    1
c ---[12647]---> BDD-cost:    1
c ---[12642]---> BDD-cost:    1
c ---[12397]---> BDD-cost:    1
c ---[12077]---> BDD-cost:    1
c ---[11070]---> BDD-cost:    1
c ---[10786]---> BDD-cost:    1
c ---[10691]---> BDD-cost:    1
c ---[10596]---> BDD-cost:    1
c ---[4876]---> BDD-cost:    1
c ---[2597]---> BDD-cost:    1
c ---[2314]---> BDD-cost:    1
c ---[2309]---> BDD-cost:    1
c ---[2304]---> BDD-cost:    1
c ---[2299]---> BDD-cost:    1
c ---[2294]---> BDD-cost:    1
c ---[2289]---> BDD-cost:    1
c ---[2284]---> BDD-cost:    1
c ---[2279]---> BDD-cost:    1
c ---[2274]---> BDD-cost:    1
c ---[2269]---> BDD-cost:    1
c ---[2264]---> BDD-cost:    1
c ---[2259]---> BDD-cost:    1
c ---[2254]---> BDD-cost:    1
c ---[2249]---> BDD-cost:    1
c ---[ 503]---> BDD-cost:   14
c ---[ 502]---> BDD-cost:   14
c ---[ 501]---> BDD-cost:    1
c ---[ 500]---> BDD-cost:    1
c ---[ 499]---> BDD-cost:   14
c ---[ 498]---> BDD-cost:   14
c ---[ 497]---> BDD-cost:    1
c ---[ 496]---> BDD-cost:    1
c ---[ 495]---> BDD-cost:   14
c ---[ 494]---> BDD-cost:   14
c ---[ 493]---> BDD-cost:    1
c ---[ 492]---> BDD-cost:    1
c ---[ 491]---> BDD-cost:   14
c ---[ 490]---> BDD-cost:   14
c ---[ 489]---> BDD-cost:    1
c ---[ 488]---> BDD-cost:    1
c ---[ 487]---> BDD-cost:   14
c ---[ 486]---> BDD-cost:   14
c ---[ 485]---> BDD-cost:    1
c ---[ 484]---> BDD-cost:    1
c ---[ 483]---> BDD-cost:   14
c ---[ 482]---> BDD-cost:   14
c ---[ 481]---> BDD-cost:    1
c ---[ 480]---> BDD-cost:    1
c ---[ 479]---> BDD-cost:   14
c ---[ 478]---> BDD-cost:   14
c ---[ 477]---> BDD-cost:    1
c ---[ 476]---> BDD-cost:    1
c ---[ 475]---> BDD-cost:   14
c ---[ 474]---> BDD-cost:   14
c ---[ 473]---> BDD-cost:    1
c ---[ 472]---> BDD-cost:    1
c ---[ 471]---> BDD-cost:   14
c ---[ 470]---> BDD-cost:   14
c ---[ 469]---> BDD-cost:    1
c ---[ 468]---> BDD-cost:    1
c ---[ 467]---> BDD-cost:   14
c ---[ 466]---> BDD-cost:   14
c ---[ 465]---> BDD-cost:    1
c ---[ 464]---> BDD-cost:    1
c ---[ 463]---> BDD-cost:   14
c ---[ 462]---> BDD-cost:   14
c ---[ 461]---> BDD-cost:    1
c ---[ 460]---> BDD-cost:    1
c ---[ 459]---> BDD-cost:   14
c ---[ 458]---> BDD-cost:   14
c ---[ 457]---> BDD-cost:    1
c ---[ 456]---> BDD-cost:    1
c ---[ 455]---> BDD-cost:   14
c ---[ 454]---> BDD-cost:   14
c ---[ 453]---> BDD-cost:    1
c ---[ 452]---> BDD-cost:    1
c ---[ 451]---> BDD-cost:   14
c ---[ 450]---> BDD-cost:   14
c ---[ 449]---> BDD-cost:    1
c ---[ 448]---> BDD-cost:    1
c ---[ 447]---> BDD-cost:   14
c ---[ 446]---> BDD-cost:   14
c ---[ 445]---> BDD-cost:    1
c ---[ 444]---> BDD-cost:    1
c ---[ 443]---> BDD-cost:   14
c ---[ 442]---> BDD-cost:   14
c ---[ 441]---> BDD-cost:    1
c ---[ 440]---> BDD-cost:    1
c ---[ 439]---> BDD-cost:   14
c ---[ 438]---> BDD-cost:   14
c ---[ 437]---> BDD-cost:    1
c ---[ 436]---> BDD-cost:    1
c ---[ 435]---> BDD-cost:   14
c ---[ 434]---> BDD-cost:   14
c ---[ 433]---> BDD-cost:    1
c ---[ 432]---> BDD-cost:    1
c ---[ 431]---> BDD-cost:   14
c ---[ 430]---> BDD-cost:   14
c ---[ 429]---> BDD-cost:    1
c ---[ 428]---> BDD-cost:    1
c ---[ 427]---> BDD-cost:   14
c ---[ 426]---> BDD-cost:   14
c ---[ 425]---> BDD-cost:    1
c ---[ 424]---> BDD-cost:    1
c ---[ 423]---> BDD-cost:   14
c ---[ 422]---> BDD-cost:   14
c ---[ 421]---> BDD-cost:    1
c ---[ 420]---> BDD-cost:    1
c ---[ 419]---> BDD-cost:   14
c ---[ 418]---> BDD-cost:   14
c ---[ 417]---> BDD-cost:    1
c ---[ 416]---> BDD-cost:    1
c ---[ 415]---> BDD-cost:   14
c ---[ 414]---> BDD-cost:   14
c ---[ 413]---> BDD-cost:    1
c ---[ 412]---> BDD-cost:    1
c ---[ 411]---> BDD-cost:   14
c ---[ 410]---> BDD-cost:   14
c ---[ 409]---> BDD-cost:    1
c ---[ 408]---> BDD-cost:    1
c ---[ 407]---> BDD-cost:   14
c ---[ 406]---> BDD-cost:   14
c ---[ 405]---> BDD-cost:    1
c ---[ 404]---> BDD-cost:    1
c ---[ 403]---> BDD-cost:   14
c ---[ 402]---> BDD-cost:   14
c ---[ 401]---> BDD-cost:    1
c ---[ 400]---> BDD-cost:    1
c ---[ 399]---> BDD-cost:   14
c ---[ 398]---> BDD-cost:   14
c ---[ 397]---> BDD-cost:    1
c ---[ 396]---> BDD-cost:    1
c ---[ 395]---> BDD-cost:   14
c ---[ 394]---> BDD-cost:   14
c ---[ 393]---> BDD-cost:    1
c ---[ 392]---> BDD-cost:    1
c ---[ 391]---> BDD-cost:   14
c ---[ 390]---> BDD-cost:   14
c ---[ 389]---> BDD-cost:    1
c ---[ 388]---> BDD-cost:    1
c ---[ 387]---> BDD-cost:   14
c ---[ 386]---> BDD-cost:   14
c ---[ 385]---> BDD-cost:    1
c ---[ 384]---> BDD-cost:    1
c ---[ 383]---> BDD-cost:   14
c ---[ 382]---> BDD-cost:   14
c ---[ 381]---> BDD-cost:    1
c ---[ 380]---> BDD-cost:    1
c ---[ 379]---> BDD-cost:   14
c ---[ 378]---> BDD-cost:   14
c ---[ 377]---> BDD-cost:    1
c ---[ 376]---> BDD-cost:    1
c ---[ 375]---> BDD-cost:   14
c ---[ 374]---> BDD-cost:   14
c ---[ 373]---> BDD-cost:    1
c ---[ 372]---> BDD-cost:    1
c ---[ 371]---> BDD-cost:   14
c ---[ 370]---> BDD-cost:   14
c ---[ 369]---> BDD-cost:    1
c ---[ 368]---> BDD-cost:    1
c ---[ 367]---> BDD-cost:   14
c ---[ 366]---> BDD-cost:   14
c ---[ 365]---> BDD-cost:    1
c ---[ 364]---> BDD-cost:    1
c ---[ 363]---> BDD-cost:   14
c ---[ 362]---> BDD-cost:   14
c ---[ 361]---> BDD-cost:    1
c ---[ 360]---> BDD-cost:    1
c ---[ 359]---> BDD-cost:   14
c ---[ 358]---> BDD-cost:   14
c ---[ 357]---> BDD-cost:    1
c ---[ 356]---> BDD-cost:    1
c ---[ 355]---> BDD-cost:   14
c ---[ 354]---> BDD-cost:   14
c ---[ 353]---> BDD-cost:    1
c ---[ 352]---> BDD-cost:    1
c ---[ 351]---> BDD-cost:   14
c ---[ 350]---> BDD-cost:   14
c ---[ 349]---> BDD-cost:    1
c ---[ 348]---> BDD-cost:    1
c ---[ 347]---> BDD-cost:   14
c ---[ 346]---> BDD-cost:   14
c ---[ 345]---> BDD-cost:    1
c ---[ 344]---> BDD-cost:    1
c ---[ 343]---> BDD-cost:   14
c ---[ 342]---> BDD-cost:   14
c ---[ 341]---> BDD-cost:    1
c ---[ 340]---> BDD-cost:    1
c ---[ 339]---> BDD-cost:   14
c ---[ 338]---> BDD-cost:   14
c ---[ 337]---> BDD-cost:    1
c ---[ 336]---> BDD-cost:    1
c ---[ 335]---> BDD-cost:   14
c ---[ 334]---> BDD-cost:   14
c ---[ 333]---> BDD-cost:    1
c ---[ 332]---> BDD-cost:    1
c ---[ 331]---> BDD-cost:   14
c ---[ 330]---> BDD-cost:   14
c ---[ 329]---> BDD-cost:    1
c ---[ 328]---> BDD-cost:    1
c ---[ 327]---> BDD-cost:   14
c ---[ 326]---> BDD-cost:   14
c ---[ 325]---> BDD-cost:    1
c ---[ 324]---> BDD-cost:    1
c ---[ 323]---> BDD-cost:   14
c ---[ 322]---> BDD-cost:   14
c ---[ 321]---> BDD-cost:    1
c ---[ 320]---> BDD-cost:    1
c ---[ 319]---> BDD-cost:   14
c ---[ 318]---> BDD-cost:   14
c ---[ 317]---> BDD-cost:    1
c ---[ 316]---> BDD-cost:    1
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:    1
c ---[ 312]---> BDD-cost:    1
c ---[ 311]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 305]---> BDD-cost:    1
c ---[ 304]---> BDD-cost:    1
c ---[ 303]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   14
c ---[ 301]---> BDD-cost:    1
c ---[ 300]---> BDD-cost:    1
c ---[ 299]---> BDD-cost:   14
c ---[ 298]---> BDD-cost:   14
c ---[ 297]---> BDD-cost:    1
c ---[ 296]---> BDD-cost:    1
c ---[ 295]---> BDD-cost:   14
c ---[ 294]---> BDD-cost:   14
c ---[ 293]---> BDD-cost:    1
c ---[ 292]---> BDD-cost:    1
c ---[ 291]---> BDD-cost:   14
c ---[ 290]---> BDD-cost:   14
c ---[ 289]---> BDD-cost:    1
c ---[ 288]---> BDD-cost:    1
c ---[ 287]---> BDD-cost:   14
c ---[ 286]---> BDD-cost:   14
c ---[ 285]---> BDD-cost:    1
c ---[ 284]---> BDD-cost:    1
c ---[ 283]---> BDD-cost:   14
c ---[ 282]---> BDD-cost:   14
c ---[ 281]---> BDD-cost:    1
c ---[ 280]---> BDD-cost:    1
c ---[ 279]---> BDD-cost:   14
c ---[ 278]---> BDD-cost:   14
c ---[ 277]---> BDD-cost:    1
c ---[ 276]---> BDD-cost:    1
c ---[ 275]---> BDD-cost:   14
c ---[ 274]---> BDD-cost:   14
c ---[ 273]---> BDD-cost:    1
c ---[ 272]---> BDD-cost:    1
c ---[ 271]---> BDD-cost:   14
c ---[ 270]---> BDD-cost:   14
c ---[ 269]---> BDD-cost:    1
c ---[ 268]---> BDD-cost:    1
c ---[ 267]---> BDD-cost:   14
c ---[ 266]---> BDD-cost:   14
c ---[ 265]---> BDD-cost:    1
c ---[ 264]---> BDD-cost:    1
c ---[ 263]---> BDD-cost:   14
c ---[ 262]---> BDD-cost:   14
c ---[ 261]---> BDD-cost:    1
c ---[ 260]---> BDD-cost:    1
c ---[ 259]---> BDD-cost:   14
c ---[ 258]---> BDD-cost:   14
c ---[ 257]---> BDD-cost:    1
c ---[ 256]---> BDD-cost:    1
c ---[ 255]---> BDD-cost:   14
c ---[ 254]---> BDD-cost:   14
c ---[ 253]---> BDD-cost:    1
c ---[ 252]---> BDD-cost:    1
c ---[ 251]---> BDD-cost:   14
c ---[ 250]---> BDD-cost:   14
c ---[ 249]---> BDD-cost:    1
c ---[ 248]---> BDD-cost:    1
c ---[ 247]---> BDD-cost:   14
c ---[ 246]---> BDD-cost:   14
c ---[ 245]---> BDD-cost:    1
c ---[ 244]---> BDD-cost:    1
c ---[ 243]---> BDD-cost:   14
c ---[ 242]---> BDD-cost:   14
c ---[ 241]---> BDD-cost:    1
c ---[ 240]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:   14
c ---[ 238]---> BDD-cost:   14
c ---[ 237]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 235]---> BDD-cost:   14
c ---[ 234]---> BDD-cost:   14
c ---[ 233]---> BDD-cost:    1
c ---[ 232]---> BDD-cost:    1
c ---[ 231]---> BDD-cost:   14
c ---[ 230]---> BDD-cost:   14
c ---[ 229]---> BDD-cost:    1
c ---[ 228]---> BDD-cost:    1
c ---[ 227]---> BDD-cost:   14
c ---[ 226]---> BDD-cost:   14
c ---[ 225]---> BDD-cost:    1
c ---[ 224]---> BDD-cost:    1
c ---[ 223]---> BDD-cost:   14
c ---[ 222]---> BDD-cost:   14
c ---[ 221]---> BDD-cost:    1
c ---[ 220]---> BDD-cost:    1
c ---[ 219]---> BDD-cost:   14
c ---[ 218]---> BDD-cost:   14
c ---[ 217]---> BDD-cost:    1
c ---[ 216]---> BDD-cost:    1
c ---[ 215]---> BDD-cost:   14
c ---[ 214]---> BDD-cost:   14
c ---[ 213]---> BDD-cost:    1
c ---[ 212]---> BDD-cost:    1
c ---[ 211]---> BDD-cost:   14
c ---[ 210]---> BDD-cost:   14
c ---[ 209]---> BDD-cost:    1
c ---[ 208]---> BDD-cost:    1
c ---[ 207]---> BDD-cost:   14
c ---[ 206]---> BDD-cost:   14
c ---[ 205]---> BDD-cost:    1
c ---[ 204]---> BDD-cost:    1
c ---[ 203]---> BDD-cost:   14
c ---[ 202]---> BDD-cost:   14
c ---[ 201]---> BDD-cost:    1
c ---[ 200]---> BDD-cost:    1
c ---[ 199]---> BDD-cost:   14
c ---[ 198]---> BDD-cost:   14
c ---[ 197]---> BDD-cost:    1
c ---[ 196]---> BDD-cost:    1
c ---[ 195]---> BDD-cost:   14
c ---[ 194]---> BDD-cost:   14
c ---[ 193]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 191]---> BDD-cost:   14
c ---[ 190]---> BDD-cost:   14
c ---[ 189]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 187]---> BDD-cost:   14
c ---[ 186]---> BDD-cost:   14
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:    1
c ---[ 183]---> BDD-cost:   14
c ---[ 182]---> BDD-cost:   14
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:   14
c ---[ 178]---> BDD-cost:   14
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:   14
c ---[ 174]---> BDD-cost:   14
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:   14
c ---[ 170]---> BDD-cost:   14
c ---[ 169]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:   14
c ---[ 166]---> BDD-cost:   14
c ---[ 165]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> BDD-cost:   14
c ---[ 162]---> BDD-cost:   14
c ---[ 161]---> BDD-cost:    1
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost:   14
c ---[ 158]---> BDD-cost:   14
c ---[ 157]---> BDD-cost:    1
c ---[ 156]---> BDD-cost:    1
c ---[ 155]---> BDD-cost:   14
c ---[ 154]---> BDD-cost:   14
c ---[ 153]---> BDD-cost:    1
c ---[ 152]---> BDD-cost:    1
c ---[ 151]---> BDD-cost:   14
c ---[ 150]---> BDD-cost:   14
c ---[ 149]---> BDD-cost:    1
c ---[ 148]---> BDD-cost:    1
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   14
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:    1
c ---[ 143]---> BDD-cost:   14
c ---[ 142]---> BDD-cost:   14
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:   14
c ---[ 138]---> BDD-cost:   14
c ---[ 137]---> BDD-cost:    1
c ---[ 136]---> BDD-cost:    1
c ---[ 135]---> BDD-cost:   14
c ---[ 134]---> BDD-cost:   14
c ---[ 133]---> BDD-cost:    1
c ---[ 132]---> BDD-cost:    1
c ---[ 131]---> BDD-cost:   14
c ---[ 130]---> BDD-cost:   14
c ---[ 129]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:   14
c ---[ 126]---> BDD-cost:   14
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:   14
c ---[ 122]---> BDD-cost:   14
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:   14
c ---[ 118]---> BDD-cost:   14
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:   14
c ---[ 114]---> BDD-cost:   14
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:   14
c ---[ 110]---> BDD-cost:   14
c ---[ 109]---> BDD-cost:    1
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:   14
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[ 103]---> BDD-cost:   14
c ---[ 102]---> BDD-cost:   14
c ---[ 101]---> BDD-cost:    1
c ---[ 100]---> BDD-cost:    1
c ---[  99]---> BDD-cost:   14
c ---[  98]---> BDD-cost:   14
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  95]---> BDD-cost:   14
c ---[  94]---> BDD-cost:   14
c ---[  93]---> BDD-cost:    1
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:   14
c ---[  90]---> BDD-cost:   14
c ---[  89]---> BDD-cost:    1
c ---[  88]---> BDD-cost:    1
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   14
c ---[  85]---> BDD-cost:    1
c ---[  84]---> BDD-cost:    1
c ---[  83]---> BDD-cost:   14
c ---[  82]---> BDD-cost:   14
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:    1
c ---[  79]---> BDD-cost:   14
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   14
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:   14
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:   14
c ---[  66]---> BDD-cost:   14
c ---[  65]---> BDD-cost:    1
c ---[  64]---> BDD-cost:    1
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   14
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:   14
c ---[  50]---> BDD-cost:   14
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:   14
c ---[  46]---> BDD-cost:   14
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:   14
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:   14
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   14
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:   14
c ---[  14]---> BDD-cost:   14
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  199800   471219 |   66600       0        0     nan |  0.000 % |
c |       100 |  199800   471219 |   73260     100     4635    46.4 |  1.589 % |
c |       250 |  199687   470959 |   80586     248    24911   100.4 |  1.641 % |
c |       475 |  199687   470959 |   88644     473    81038   171.3 |  1.641 % |
c |       812 |  195737   462240 |   97509     798   102244   128.1 |  2.865 % |
c |      1320 |  195697   462149 |  107259    1302   143363   110.1 |  2.875 % |
c |      2080 |  194117   458824 |  117985    2050   205322   100.2 |  3.108 % |
c |      3219 |  193892   458308 |  129784    3183   387077   121.6 |  3.214 % |
c |      4927 |  193860   458239 |  142763    4885   603691   123.6 |  3.231 % |
c |      7489 |  193860   458239 |  157039    7447  1143240   153.5 |  3.231 % |
c |     11334 |  192448   454970 |  172743   11283  1831327   162.3 |  3.907 % |
c |     17100 |  192245   454503 |  190017   17043  2659394   156.0 |  4.004 % |
c |     25750 |  191600   453023 |  209019   25676  4058629   158.1 |  4.307 % |
c |     38724 |  184883   438192 |  229921   38577  5658276   146.7 |  6.381 % |
c |     58189 |  184746   437875 |  252913   58038  8063413   138.9 |  6.450 % |

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/10934/stat): 10934 (minisat+_script) R 10933 10934 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785199422 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/10934/statm): 174 3 169 147 0 27 0
[pid=10934] 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=10935
New process pid=10936
New process pid=10937
execve syscall for /bin/sed executable
One traced child (pid=10936) 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=10937) exited with status: 0
One traced child (pid=10935) exited with status: 0
New process pid=10938
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-cache.inv14.ucl.opb

[startup+10.0037 s]
Raw data (loadavg): 0.93 0.96 0.98 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 872 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 9.4
Current children cumulated vsize (Kb) 69324

[startup+20.0045 s]
Raw data (loadavg): 0.94 0.96 0.98 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 1872 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 19.4
Current children cumulated vsize (Kb) 69324

[startup+30.0053 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 2871 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 29.39
Current children cumulated vsize (Kb) 69324

[startup+40.0061 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 3871 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 39.39
Current children cumulated vsize (Kb) 69324

[startup+50.0069 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 4871 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 49.39
Current children cumulated vsize (Kb) 69324

[startup+60.0067 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 5871 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 59.39
Current children cumulated vsize (Kb) 69324

[startup+70.0076 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 6871 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 69.39
Current children cumulated vsize (Kb) 69324

[startup+80.0084 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 7872 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 79.4
Current children cumulated vsize (Kb) 69324

[startup+90.0092 s]
Raw data (loadavg): 1.05 0.98 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 8872 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 89.4
Current children cumulated vsize (Kb) 69324

[startup+100.01 s]
Raw data (loadavg): 1.05 0.98 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 9872 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134557662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 99.4
Current children cumulated vsize (Kb) 69324

[startup+110.011 s]
Raw data (loadavg): 1.04 0.98 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 10872 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 109.4
Current children cumulated vsize (Kb) 69324

[startup+120.012 s]
Raw data (loadavg): 1.03 0.98 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 11872 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 119.4
Current children cumulated vsize (Kb) 69324

[startup+130.012 s]
Raw data (loadavg): 1.03 0.98 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 12873 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 129.41
Current children cumulated vsize (Kb) 69324

[startup+140.013 s]
Raw data (loadavg): 1.02 0.98 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 13873 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223120 134556513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 139.41
Current children cumulated vsize (Kb) 69324

[startup+150.014 s]
Raw data (loadavg): 1.02 0.98 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 14873 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 149.41
Current children cumulated vsize (Kb) 69324

[startup+160.014 s]
Raw data (loadavg): 1.02 0.98 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 15873 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 159.41
Current children cumulated vsize (Kb) 69324

[startup+170.015 s]
Raw data (loadavg): 1.01 0.98 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 16874 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 169.42
Current children cumulated vsize (Kb) 69324

[startup+180.016 s]
Raw data (loadavg): 1.01 0.98 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 17874 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 179.42
Current children cumulated vsize (Kb) 69324

[startup+190.016 s]
Raw data (loadavg): 1.01 0.98 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 18874 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 189.42
Current children cumulated vsize (Kb) 69324

[startup+200.017 s]
Raw data (loadavg): 1.01 0.98 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 19874 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 199.42
Current children cumulated vsize (Kb) 69324

[startup+210.017 s]
Raw data (loadavg): 1.08 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 20875 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 209.43
Current children cumulated vsize (Kb) 69324

[startup+220.018 s]
Raw data (loadavg): 1.07 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 21875 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 219.43
Current children cumulated vsize (Kb) 69324

[startup+230.019 s]
Raw data (loadavg): 1.06 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 22875 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 229.43
Current children cumulated vsize (Kb) 69324

[startup+240.019 s]
Raw data (loadavg): 1.05 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 23875 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 239.43
Current children cumulated vsize (Kb) 69324

[startup+250.02 s]
Raw data (loadavg): 1.04 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 24876 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 249.44
Current children cumulated vsize (Kb) 69324

[startup+260.02 s]
Raw data (loadavg): 1.03 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 25876 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 259.44
Current children cumulated vsize (Kb) 69324

[startup+270.021 s]
Raw data (loadavg): 1.03 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 26876 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 269.44
Current children cumulated vsize (Kb) 69324

[startup+280.022 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 27876 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 279.44
Current children cumulated vsize (Kb) 69324

[startup+290.024 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 28877 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134557587 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 289.45
Current children cumulated vsize (Kb) 69324

[startup+300.024 s]
Raw data (loadavg): 1.02 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 29877 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 299.45
Current children cumulated vsize (Kb) 69324

[startup+310.024 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 30877 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 309.45
Current children cumulated vsize (Kb) 69324

[startup+320.025 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 31877 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223040 134556834 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 319.45
Current children cumulated vsize (Kb) 69324

[startup+330.026 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 32877 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 329.45
Current children cumulated vsize (Kb) 69324

[startup+340.027 s]
Raw data (loadavg): 1.01 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 33877 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 339.45
Current children cumulated vsize (Kb) 69324

[startup+350.027 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 34877 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 349.45
Current children cumulated vsize (Kb) 69324

[startup+360.028 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 35878 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 359.46
Current children cumulated vsize (Kb) 69324

[startup+370.029 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 36878 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 369.46
Current children cumulated vsize (Kb) 69324

[startup+380.03 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 37878 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 379.46
Current children cumulated vsize (Kb) 69324

[startup+390.031 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 38878 67 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 389.46
Current children cumulated vsize (Kb) 69324

[startup+400.032 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 39878 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 399.47
Current children cumulated vsize (Kb) 69324

[startup+410.032 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 40878 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 409.47
Current children cumulated vsize (Kb) 69324

[startup+420.033 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 41878 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 419.47
Current children cumulated vsize (Kb) 69324

[startup+430.034 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 42878 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223040 134556834 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 429.47
Current children cumulated vsize (Kb) 69324

[startup+440.035 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 43878 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 439.47
Current children cumulated vsize (Kb) 69324

[startup+450.036 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 44879 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 449.48
Current children cumulated vsize (Kb) 69324

[startup+460.036 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 45879 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 459.48
Current children cumulated vsize (Kb) 69324

[startup+470.037 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 46879 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 469.48
Current children cumulated vsize (Kb) 69324

[startup+480.038 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 47879 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223040 134551920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 479.48
Current children cumulated vsize (Kb) 69324

[startup+490.039 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 48879 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 489.48
Current children cumulated vsize (Kb) 69324

[startup+500.04 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 49879 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 499.48
Current children cumulated vsize (Kb) 69324

[startup+510.04 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 50880 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 509.49
Current children cumulated vsize (Kb) 69324

[startup+520.04 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 51880 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134558184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 519.49
Current children cumulated vsize (Kb) 69324

[startup+530.041 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 52880 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 529.49
Current children cumulated vsize (Kb) 69324

[startup+540.042 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 53880 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134558295 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 539.49
Current children cumulated vsize (Kb) 69324

[startup+550.043 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 54881 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 549.5
Current children cumulated vsize (Kb) 69324

[startup+560.044 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 55881 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 559.5
Current children cumulated vsize (Kb) 69324

[startup+570.044 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 56881 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 569.5
Current children cumulated vsize (Kb) 69324

[startup+580.045 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 57881 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 579.5
Current children cumulated vsize (Kb) 69324

[startup+590.047 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 58882 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 589.51
Current children cumulated vsize (Kb) 69324

[startup+600.048 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 59882 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 599.51
Current children cumulated vsize (Kb) 69324

[startup+610.048 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 60882 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 609.51
Current children cumulated vsize (Kb) 69324

[startup+620.049 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 61882 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 619.51
Current children cumulated vsize (Kb) 69324

[startup+630.049 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 62883 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 629.52
Current children cumulated vsize (Kb) 69324

[startup+640.05 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 63883 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134558153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 639.52
Current children cumulated vsize (Kb) 69324

[startup+650.051 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 64883 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 649.52
Current children cumulated vsize (Kb) 69324

[startup+660.051 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 65883 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 659.52
Current children cumulated vsize (Kb) 69324

[startup+670.052 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 66883 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 669.52
Current children cumulated vsize (Kb) 69324

[startup+680.053 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 67883 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 679.52
Current children cumulated vsize (Kb) 69324

[startup+690.053 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 68883 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 689.52
Current children cumulated vsize (Kb) 69324

[startup+700.054 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 69884 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 699.53
Current children cumulated vsize (Kb) 69324

[startup+710.055 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 70884 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 709.53
Current children cumulated vsize (Kb) 69324

[startup+720.056 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 71884 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 719.53
Current children cumulated vsize (Kb) 69324

[startup+730.057 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 72884 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 729.53
Current children cumulated vsize (Kb) 69324

[startup+740.058 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 73885 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 739.54
Current children cumulated vsize (Kb) 69324

[startup+750.059 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 74885 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 749.54
Current children cumulated vsize (Kb) 69324

[startup+760.059 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 75885 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 759.54
Current children cumulated vsize (Kb) 69324

[startup+770.061 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 76885 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 769.54
Current children cumulated vsize (Kb) 69324

[startup+780.062 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 77886 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 779.55
Current children cumulated vsize (Kb) 69324

[startup+790.062 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16290 0 0 0 78886 68 0 0 25 0 1 0 1785199426 68812800 15765 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15765 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 789.55
Current children cumulated vsize (Kb) 69324

[startup+800.063 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 79886 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 799.55
Current children cumulated vsize (Kb) 69324

[startup+810.064 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 80887 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 809.56
Current children cumulated vsize (Kb) 69324

[startup+820.065 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 81887 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223040 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 819.56
Current children cumulated vsize (Kb) 69324

[startup+830.066 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 82887 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 829.56
Current children cumulated vsize (Kb) 69324

[startup+840.067 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 83887 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 839.56
Current children cumulated vsize (Kb) 69324

[startup+850.067 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 84887 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223120 134555323 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 849.56
Current children cumulated vsize (Kb) 69324

[startup+860.068 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 85887 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223040 134557168 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 859.56
Current children cumulated vsize (Kb) 69324

[startup+870.069 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 86887 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 869.56
Current children cumulated vsize (Kb) 69324

[startup+880.07 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 87887 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223056 134782400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 879.56
Current children cumulated vsize (Kb) 69324

[startup+890.071 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 88887 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 889.56
Current children cumulated vsize (Kb) 69324

[startup+900.072 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 89888 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 899.57
Current children cumulated vsize (Kb) 69324

[startup+910.072 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 90888 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 909.57
Current children cumulated vsize (Kb) 69324

[startup+920.073 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 91888 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 919.57
Current children cumulated vsize (Kb) 69324

[startup+930.074 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 92889 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 929.58
Current children cumulated vsize (Kb) 69324

[startup+940.076 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 93889 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 939.58
Current children cumulated vsize (Kb) 69324

[startup+950.077 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 94889 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 949.58
Current children cumulated vsize (Kb) 69324

[startup+960.076 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 95889 68 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 959.58
Current children cumulated vsize (Kb) 69324

[startup+970.077 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 96889 69 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 969.59
Current children cumulated vsize (Kb) 69324

[startup+980.078 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 97890 69 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 979.6
Current children cumulated vsize (Kb) 69324

[startup+990.079 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 98890 69 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 989.6
Current children cumulated vsize (Kb) 69324

[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 99890 69 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223040 134557275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 999.6
Current children cumulated vsize (Kb) 69324

[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 100890 69 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 1009.6
Current children cumulated vsize (Kb) 69324

[startup+1020.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 101891 69 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 1019.61
Current children cumulated vsize (Kb) 69324

[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 102891 69 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 1029.61
Current children cumulated vsize (Kb) 69324

[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 103890 69 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 1039.6
Current children cumulated vsize (Kb) 69324

[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 104890 69 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 1049.6
Current children cumulated vsize (Kb) 69324

[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16293 0 0 0 105890 69 0 0 25 0 1 0 1785199426 68812800 15768 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16800 15768 145 145 0 16655 0
[pid=10938] vsize: 67200
Current children cumulated CPU time (s) 1059.6
Current children cumulated vsize (Kb) 69324

[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16334 0 0 0 106890 69 0 0 25 0 1 0 1785199426 68980736 15809 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16841 15809 145 145 0 16696 0
[pid=10938] vsize: 67364
Current children cumulated CPU time (s) 1069.6
Current children cumulated vsize (Kb) 69488

[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16376 0 0 0 107890 70 0 0 25 0 1 0 1785199426 69177344 15851 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16889 15851 145 145 0 16744 0
[pid=10938] vsize: 67556
Current children cumulated CPU time (s) 1079.61
Current children cumulated vsize (Kb) 69680

[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16422 0 0 0 108889 70 0 0 25 0 1 0 1785199426 69410816 15897 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 16946 15897 145 145 0 16801 0
[pid=10938] vsize: 67784
Current children cumulated CPU time (s) 1089.6
Current children cumulated vsize (Kb) 69908

[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16480 0 0 0 109889 70 0 0 25 0 1 0 1785199426 69685248 15955 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17013 15955 145 145 0 16868 0
[pid=10938] vsize: 68052
Current children cumulated CPU time (s) 1099.6
Current children cumulated vsize (Kb) 70176

[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16554 0 0 0 110888 71 0 0 25 0 1 0 1785199426 69976064 16029 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17084 16029 145 145 0 16939 0
[pid=10938] vsize: 68336
Current children cumulated CPU time (s) 1109.6
Current children cumulated vsize (Kb) 70460

[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16591 0 0 0 111887 71 0 0 25 0 1 0 1785199426 70123520 16066 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17120 16066 145 145 0 16975 0
[pid=10938] vsize: 68480
Current children cumulated CPU time (s) 1119.59
Current children cumulated vsize (Kb) 70604

[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16629 0 0 0 112887 71 0 0 25 0 1 0 1785199426 70275072 16104 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17157 16104 145 145 0 17012 0
[pid=10938] vsize: 68628
Current children cumulated CPU time (s) 1129.59
Current children cumulated vsize (Kb) 70752

[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16655 0 0 0 113887 71 0 0 25 0 1 0 1785199426 70381568 16130 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17183 16130 145 145 0 17038 0
[pid=10938] vsize: 68732
Current children cumulated CPU time (s) 1139.59
Current children cumulated vsize (Kb) 70856

[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16727 0 0 0 114886 72 0 0 25 0 1 0 1785199426 70725632 16202 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17267 16202 145 145 0 17122 0
[pid=10938] vsize: 69068
Current children cumulated CPU time (s) 1149.59
Current children cumulated vsize (Kb) 71192

[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16796 0 0 0 115885 72 0 0 25 0 1 0 1785199426 71000064 16271 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17334 16271 145 145 0 17189 0
[pid=10938] vsize: 69336
Current children cumulated CPU time (s) 1159.58
Current children cumulated vsize (Kb) 71460

[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16843 0 0 0 116884 72 0 0 25 0 1 0 1785199426 71192576 16318 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17381 16318 145 145 0 17236 0
[pid=10938] vsize: 69524
Current children cumulated CPU time (s) 1169.57
Current children cumulated vsize (Kb) 71648

[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16881 0 0 0 117884 73 0 0 25 0 1 0 1785199426 71348224 16356 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17419 16356 145 145 0 17274 0
[pid=10938] vsize: 69676
Current children cumulated CPU time (s) 1179.58
Current children cumulated vsize (Kb) 71800

[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 16935 0 0 0 118884 73 0 0 25 0 1 0 1785199426 71565312 16410 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17472 16410 145 145 0 17327 0
[pid=10938] vsize: 69888
Current children cumulated CPU time (s) 1189.58
Current children cumulated vsize (Kb) 72012

[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 17015 0 0 0 119883 73 0 0 25 0 1 0 1785199426 72151040 16490 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17615 16490 145 145 0 17470 0
[pid=10938] vsize: 70460
Current children cumulated CPU time (s) 1199.57
Current children cumulated vsize (Kb) 72584

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 17016 0 0 0 120884 73 0 0 25 0 1 0 1785199426 72151040 16491 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17615 16491 145 145 0 17470 0
[pid=10938] vsize: 70460
Current children cumulated CPU time (s) 1209.58
Current children cumulated vsize (Kb) 72584



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 10938
Raw data (/proc/10934/stat): 10934 (minisat+_script) S 10933 10934 31778 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1785199422 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/10934/statm): 531 226 485 147 0 384 0
[pid=10934] vsize: 2124
Raw data (/proc/10938/stat): 10938 (minisat+_64-bit) R 10934 10934 31778 0 -1 0 17016 0 0 0 120884 73 0 0 25 0 1 0 1785199426 72151040 16491 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/10938/statm): 17615 16491 145 145 0 17470 0
[pid=10938] vsize: 70460
Current children cumulated CPU time (s) 1209.58
Current children cumulated vsize (Kb) 72584

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1209.61
CPU user time (s): 1208.84
CPU system time (s): 0.768883
CPU usage (%): 99.957
Max. virtual memory (cumulated for all children) (Kb): 72584

Verifier Data

ERROR: no interpretation found !