PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-10teams.opb
MD5SUM	1ff3cc3253012886aa21be4feac6111e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	924
Optimality of the best value was proved	NO
Number of terms in the objective function	1800
Biggest coefficient in the objective function	86
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	41700
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	86
Number of bits of the biggest number in a constraint	7
Biggest sum of numbers in a constraint	41700
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.71
Number of variables	1800
Total number of constraints	2015
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2015
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	72
Trace number 16865

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 08:48:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12386 boxname=wulflinc7 idbench=953 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1ff3cc3253012886aa21be4feac6111e  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-10teams.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-10teams.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-10teams.opb
IDLAUNCH: 12386
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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		: 451.050
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:        695336 kB
Buffers:         19052 kB
Cached:         298028 kB
SwapCached:          4 kB
Active:          71628 kB
Inactive:       248296 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        695084 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            13728 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:08:54 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 12386 7 1200.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 330 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 329]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 328]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 326]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 324]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 322]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 320]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 318]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 316]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 314]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 312]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 310]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 308]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 307]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 305]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 303]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 301]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 299]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 297]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 295]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 293]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 291]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 289]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 288]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 286]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 284]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 282]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 280]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 278]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 276]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 274]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 272]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 270]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 269]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 267]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 265]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 263]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 261]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 259]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 257]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 255]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 253]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 251]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 250]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 248]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 246]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 244]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 242]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 240]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 238]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 236]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 234]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 233]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 231]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 229]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 227]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 225]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 223]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 221]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 219]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 217]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 216]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 214]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 212]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 210]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 208]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 206]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 204]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 202]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 200]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 198]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 197]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 195]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 193]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 191]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 189]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 187]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 185]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 183]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 181]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 179]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 178]---> Adder-cost: 118   maxlim: 62   bits: 7/6
c ---[ 176]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 174]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 172]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 170]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 168]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 166]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 164]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 162]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 160]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 159]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[ 157]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 155]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 153]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 151]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 149]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 147]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 145]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 143]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 141]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 140]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[ 139]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[ 137]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 135]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 133]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 131]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 129]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 127]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 125]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 123]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 121]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 120]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[ 118]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 116]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 114]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 112]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 110]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 108]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 106]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 104]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 102]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 101]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  99]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  97]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  95]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  93]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  91]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  89]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  87]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  85]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  83]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  82]---> Adder-cost: 118   maxlim: 62   bits: 7/6
c ---[  80]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  79]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  78]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  77]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  76]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  75]---> Adder-cost: 118   maxlim: 61   bits: 7/6
c ---[  74]---> Adder-cost: 114   maxlim: 62   bits: 7/6
c ---[  73]---> Adder-cost: 118   maxlim: 61   bits: 7/6
c ---[  72]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  71]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  70]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  69]---> Adder-cost: 118   maxlim: 61   bits: 7/6
c ---[  68]---> Adder-cost: 114   maxlim: 62   bits: 7/6
c ---[  67]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  66]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  65]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  64]---> Adder-cost: 118   maxlim: 61   bits: 7/6
c ---[  63]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  62]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  61]---> Adder-cost: 114   maxlim: 62   bits: 7/6
c ---[  60]---> Adder-cost: 114   maxlim: 62   bits: 7/6
c ---[  59]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  58]---> Adder-cost: 118   maxlim: 61   bits: 7/6
c ---[  57]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  56]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  55]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  54]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  53]---> Adder-cost: 118   maxlim: 61   bits: 7/6
c ---[  52]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  51]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  50]---> Adder-cost: 114   maxlim: 62   bits: 7/6
c ---[  49]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  48]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[  47]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  46]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  45]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[  44]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  43]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  42]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[  41]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  40]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[  39]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  38]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  37]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[  36]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  35]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  34]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[  33]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  32]---> Adder-cost: 114   maxlim: 62   bits: 7/6
c ---[  31]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  30]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  29]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  28]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  27]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  26]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[  25]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  24]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  23]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  22]---> Adder-cost: 118   maxlim: 61   bits: 7/6
c ---[  21]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[  20]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  19]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  18]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[  17]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  16]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[  15]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[  14]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[  13]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  12]---> Adder-cost: 114   maxlim: 61   bits: 7/6
c ---[  11]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  10]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[   9]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[   8]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[   7]---> Adder-cost: 58   maxlim: 38   bits: 6/6
c ---[   6]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[   4]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[   2]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[   0]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  112120   397350 |   37373       0        0     nan |  0.000 % |
c |       100 |  111907   396603 |   41110      86      174     2.0 | 11.580 % |
c |       250 |  111404   394867 |   45221     172      398     2.3 | 11.976 % |
c |       475 |  110680   392358 |   49743     324      779     2.4 | 12.580 % |
c |       813 |  109653   388798 |   54717     563     1890     3.4 | 13.447 % |
c |      1320 |  107769   382196 |   60189     907     3357     3.7 | 15.067 % |
c |      2079 |  105864   375549 |   66208    1473     6202     4.2 | 16.652 % |
c |      3218 |  104574   371131 |   72829    2459    11244     4.6 | 17.766 % |
c |      4926 |  102440   363689 |   80112    3872    29583     7.6 | 19.480 % |
c |      7488 |   99440   353341 |   88123    6010    64894    10.8 | 22.031 % |
c |     11332 |   94533   336430 |   96935    9109   120851    13.3 | 25.978 % |
c |     17098 |   89037   317586 |  106629   14011   251292    17.9 | 30.391 % |
c |     25749 |   83957   300293 |  117292   21772   513018    23.6 | 34.601 % |
c |     38723 |   76907   276053 |  129021   33712   986517    29.3 | 40.525 % |
c |     58184 |   71731   258418 |  141923   52280  2410623    46.1 | 44.903 % |
c |     87378 |   69318   250251 |  156116   80971  7138749    88.2 | 46.914 % |
c ==============================================================================
c [1mFound solution: 970[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 7748   maxlim: 39030   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115658 |  122276   439667 |   40758  109026 13723174   125.9 | 46.914 % |
c |    115758 |  122276   439667 |   44833   38685  3336171    86.2 | 34.670 % |
c |    115908 |  122235   439528 |   49317   38830  3365655    86.7 | 34.688 % |
c |    116135 |  122235   439528 |   54248   39057  3408860    87.3 | 34.688 % |
c |    116477 |  122235   439528 |   59673   39399  3456047    87.7 | 34.688 % |
c |    116983 |  122235   439528 |   65641   39905  3522874    88.3 | 34.688 % |
c |    117743 |  122227   439498 |   72205   40664  3681474    90.5 | 34.692 % |
c ==============================================================================
c [1mFound solution: 952[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39048   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    118028 |  122234   439536 |   40744   40949  3723236    90.9 | 34.692 % |
c |    118131 |  122209   439455 |   44818   41047  3735451    91.0 | 34.717 % |
c |    118281 |  122209   439455 |   49300   41197  3748392    91.0 | 34.717 % |
c |    118506 |  122209   439455 |   54230   41422  3782479    91.3 | 34.717 % |
c |    118844 |  122191   439397 |   59653   41758  3814711    91.4 | 34.731 % |
c |    119351 |  122184   439374 |   65618   42263  3973845    94.0 | 34.735 % |
c |    120110 |  122118   439152 |   72180   43011  4170493    97.0 | 34.767 % |
c |    121252 |  122110   439126 |   79398   44152  4414858   100.0 | 34.770 % |
c |    122963 |  122101   439097 |   87338   45862  4707275   102.6 | 34.778 % |
c |    125527 |  122006   438779 |   96072   48412  5392904   111.4 | 34.835 % |
c |    129371 |  121758   437941 |  105679   52222  6284305   120.3 | 34.985 % |
c |    135138 |  121592   437372 |  116247   57967  7685295   132.6 | 35.092 % |
c |    143788 |  121406   436740 |  127872   66590 10099767   151.7 | 35.211 % |
c |    156762 |  120950   435186 |  140659   79497 13115167   165.0 | 35.472 % |
c |    176224 |  120447   433476 |  154725   98876 18405696   186.1 | 35.790 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x226_bit0 -x227_bit0 -x228_bit0 -x229_bit0 -x230_bit0 -x231_bit0 -x232_bit0 -x233_bit0 -x234_bit0 -x235_bit0 -x236_bit0 -x237_bit0 -x238_bit0 -x239_bit0 -x240_bit0 -x241_bit0 -x242_bit0 -x243_bit0 -x244_bit0 -x245_bit0 -x246_bit0 -x247_bit0 -x248_bit0 -x249_bit0 -x250_bit0 -x251_bit0 -x252_bit0 -x253_bit0 -x254_bit0 -x255_bit0 -x256_bit0 x257_bit0 -x258_bit0 -x259_bit0 -x260_bit0 -x261_bit0 -x262_bit0 -x263_bit0 -x264_bit0 -x265_bit0 -x266_bit0 -x267_bit0 -x268_bit0 -x269_bit0 -x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 -x275_bit0 -x276_bit0 -x277_bit0 -x278_bit0 -x279_bit0 -x280_bit0 -x281_bit0 -x282_bit0 -x283_bit0 -x284_bit0 -x285_bit0 x286_bit0 -x287_bit0 -x288_bit0 -x289_bit0 -x290_bit0 -x291_bit0 -x292_bit0 -x293_bit0 -x294_bit0 -x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 -x299_bit0 -x300_bit0 -x301_bit0 -x302_bit0 -x303_bit0 -x304_bit0 -x305_bit0 -x306_bit0 -x307_bit0 -x308_bit0 -x309_bit0 -x310_bit0 -x311_bit0 -x312_bit0 -x313_bit0 -x314_bit0 -x315_bit0 -x316_bit0 -x317_bit0 -x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 -x333_bit0 -x334_bit0 -x335_bit0 -x336_bit0 -x337_bit0 -x338_bit0 x339_bit0 -x340_bit0 -x341_bit0 -x342_bit0 -x343_bit0 -x344_bit0 -x345_bit0 -x346_bit0 -x347_bit0 -x348_bit0 -x349_bit0 -x350_bit0 -x351_bit0 -x352_bit0 -x353_bit0 -x354_bit0 -x355_bit0 -x356_bit0 -x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 -x366_bit0 -x367_bit0 x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 -x373_bit0 -x374_bit0 -x375_bit0 -x376_bit0 -x377_bit0 -x378_bit0 -x379_bit0 -x380_bit0 -x381_bit0 -x382_bit0 -x383_bit0 -x384_bit0 -x385_bit0 -x386_bit0 -x387_bit0 -x388_bit0 -x389_bit0 -x390_bit0 -x391_bit0 -x392_bit0 -x393_bit0 -x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 -x399_bit0 -x400_bit0 -x401_bit0 -x402_bit0 -x403_bit0 -x404_bit0 -x405_bit0 -x406_bit0 -x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0 -x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 -x416_bit0 -x417_bit0 -x418_bit0 -x419_bit0 -x420_bit0 -x421_bit0 -x422_bit0 -x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x427_bit0 -x428_bit0 -x429_bit0 -x430_bit0 -x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 -x436_bit0 -x437_bit0 -x438_bit0 -x439_bit0 -x440_bit0 -x441_bit0 -x442_bit0 -x443_bit0 -x444_bit0 -x445_bit0 -x446_bit0 x447_bit0 -x448_bit0 -x449_bit0 -x450_bit0 -x451_bit0 -x452_bit0 -x453_bit0 -x454_bit0 -x455_bit0 -x456_bit0 -x457_bit0 -x458_bit0 -x459_bit0 -x460_bit0 -x461_bit0 -x462_bit0 -x463_bit0 -x464_bit0 -x465_bit0 -x466_bit0 -x467_bit0 -x468_bit0 -x469_bit0 x470_bit0 -x471_bit0 -x472_bit0 -x473_bit0 -x474_bit0 -x475_bit0 -x476_bit0 -x477_bit0 -x478_bit0 -x479_bit0 -x480_bit0 -x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 -x485_bit0 -x486_bit0 -x487_bit0 -x488_bit0 -x489_bit0 -x490_bit0 -x491_bit0 -x492_bit0 -x493_bit0 -x494_bit0 -x495_bit0 -x496_bit0 -x497_bit0 -x498_bit0 -x499_bit0 -x500_bit0 -x501_bit0 -x502_bit0 -x503_bit0 -x504_bit0 -x505_bit0 -x506_bit0 x507_bit0 -x508_bit0 -x509_bit0 -x510_bit0 -x511_bit0 -x512_bit0 -x513_bit0 -x514_bit0 -x515_bit0 -x516_bit0 -x517_bit0 -x518_bit0 -x519_bit0 -x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 -x524_bit0 -x525_bit0 -x526_bit0 -x527_bit0 -x528_bit0 -x529_bit0 -x530_bit0 -x531_bit0 -x532_bit0 -x533_bit0 -x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 -x540_bit0 -x541_bit0 -x542_bit0 -x543_bit0 -x544_bit0 -x545_bit0 -x546_bit0 -x547_bit0 -x548_bit0 -x549_bit0 -x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 -x556_bit0 -x557_bit0 -x558_bit0 -x559_bit0 -x560_bit0 -x561_bit0 -x562_bit0 -x563_bit0 -x564_bit0 -x565_bit0 -x566_bit0 -x567_bit0 -x568_bit0 x569_bit0 -x570_bit0 -x571_bit0 -x572_bit0 -x573_bit0 -x574_bit0 -x575_bit0 -x576_bit0 -x577_bit0 -x578_bit0 -x579_bit0 -x580_bit0 -x581_bit0 -x582_bit0 -x583_bit0 -x584_bit0 -x585_bit0 -x586_bit0 -x587_bit0 -x588_bit0 -x589_bit0 -x590_bit0 -x591_bit0 -x592_bit0 -x593_bit0 -x594_bit0 -x595_bit0 -x596_bit0 -x597_bit0 -x598_bit0 -x599_bit0 -x600_bit0 -x601_bit0 -x602_bit0 -x603_bit0 -x604_bit0 -x605_bit0 -x606_bit0 -x607_bit0 -x608_bit0 -x609_bit0 -x610_bit0 -x611_bit0 -x612_bit0 -x613_bit0 -x614_bit0 -x615_bit0 -x616_bit0 -x617_bit0 -x618_bit0 -x619_bit0 -x620_bit0 -x621_bit0 -x622_bit0 -x623_bit0 x624_bit0 -x625_bit0 -x626_bit0 -x627_bit0 -x628_bit0 -x629_bit0 -x630_bit0 -x631_bit0 -x632_bit0 -x633_bit0 -x634_bit0 -x635_bit0 -x636_bit0 -x637_bit0 -x638_bit0 -x639_bit0 -x640_bit0 -x641_bit0 -x642_bit0 -x643_bit0 -x644_bit0 -x645_bit0 -x646_bit0 -x647_bit0 -x648_bit0 -x649_bit0 -x650_bit0 -x651_bit0 -x652_bit0 -x653_bit0 -x654_bit0 x655_bit0 -x656_bit0 -x657_bit0 -x658_bit0 -x659_bit0 -x660_bit0 -x661_bit0 -x662_bit0 -x663_bit0 -x664_bit0 -x665_bit0 -x666_bit0 -x667_bit0 -x668_bit0 -x669_bit0 -x670_bit0 -x671_bit0 -x672_bit0 -x673_bit0 -x674_bit0 -x675_bit0 -x676_bit0 -x677_bit0 -x678_bit0 -x679_bit0 -x680_bit0 -x681_bit0 -x682_bit0 -x683_bit0 -x684_bit0 -x685_bit0 -x686_bit0 -x687_bit0 -x688_bit0 -x689_bit0 -x690_bit0 -x691_bit0 -x692_bit0 -x693_bit0 -x694_bit0 -x695_bit0 -x696_bit0 -x697_bit0 -x698_bit0 -x699_bit0 -x700_bit0 -x701_bit0 -x702_bit0 -x703_bit0 -x704_bit0 x705_bit0 -x706_bit0 -x707_bit0 -x708_bit0 -x709_bit0 -x710_bit0 -x711_bit0 -x712_bit0 -x713_bit0 -x714_bit0 -x715_bit0 -x716_bit0 -x717_bit0 -x718_bit0 -x719_bit0 -x720_bit0 -x721_bit0 -x722_bit0 -x723_bit0 -x724_bit0 -x725_bit0 -x726_bit0 -x727_bit0 -x728_bit0 -x729_bit0 x730_bit0 -x731_bit0 -x732_bit0 -x733_bit0 -x734_bit0 -x735_bit0 -x736_bit0 -x737_bit0 -x738_bit0 -x739_bit0 -x740_bit0 -x741_bit0 -x742_bit0 -x743_bit0 -x744_bit0 -x745_bit0 -x746_bit0 -x747_bit0 -x748_bit0 -x749_bit0 -x750_bit0 -x751_bit0 -x752_bit0 -x753_bit0 -x754_bit0 -x755_bit0 -x756_bit0 -x757_bit0 -x758_bit0 -x759_bit0 -x760_bit0 -x761_bit0 -x762_bit0 -x763_bit0 -x764_bit0 -x765_bit0 -x766_bit0 -x767_bit0 -x768_bit0 -x769_bit0 -x770_bit0 -x771_bit0 -x772_bit0 -x773_bit0 -x774_bit0 -x775_bit0 -x776_bit0 -x777_bit0 -x778_bit0 -x779_bit0 -x780_bit0 -x781_bit0 -x782_bit0 x783_bit0 -x784_bit0 -x785_bit0 -x786_bit0 -x787_bit0 -x788_bit0 -x789_bit0 -x790_bit0 -x791_bit0 -x792_bit0 -x793_bit0 -x794_bit0 -x795_bit0 -x796_bit0 -x797_bit0 -x798_bit0 -x799_bit0 -x800_bit0 -x801_bit0 -x802_bit0 -x803_bit0 -x804_bit0 -x805_bit0 -x806_bit0 -x807_bit0 -x808_bit0 -x809_bit0 -x810_bit0 -x811_bit0 -x812_bit0 -x813_bit0 -x814_bit0 -x815_bit0 -x816_bit0 -x817_bit0 -x818_bit0 -x819_bit0 -x820_bit0 -x821_bit0 -x822_bit0 -x823_bit0 -x824_bit0 -x825_bit0 -x826_bit0 -x827_bit0 -x828_bit0 -x829_bit0 -x830_bit0 -x831_bit0 -x832_bit0 -x833_bit0 -x834_bit0 -x835_bit0 -x836_bit0 -x837_bit0 -x838_bit0 -x839_bit0 -x840_bit0 -x841_bit0 -x842_bit0 -x843_bit0 -x844_bit0 -x845_bit0 -x846_bit0 -x847_bit0 -x848_bit0 -x849_bit0 -x850_bit0 -x851_bit0 -x852_bit0 -x853_bit0 x854_bit0 -x855_bit0 -x856_bit0 -x857_bit0 -x858_bit0 -x859_bit0 -x860_bit0 -x861_bit0 -x862_bit0 -x863_bit0 -x864_bit0 -x865_bit0 x866_bit0 -x867_bit0 -x868_bit0 -x869_bit0 -x870_bit0 -x871_bit0 -x872_bit0 -x873_bit0 -x874_bit0 -x875_bit0 -x876_bit0 -x877_bit0 -x878_bit0 -x879_bit0 -x880_bit0 -x881_bit0 -x882_bit0 -x883_bit0 -x884_bit0 -x885_bit0 -x886_bit0 -x887_bit0 -x888_bit0 -x889_bit0 -x890_bit0 -x891_bit0 -x892_bit0 -x893_bit0 -x894_bit0 -x895_bit0 -x896_bit0 -x897_bit0 -x898_bit0 -x899_bit0 -x900_bit0 -x901_bit0 -x902_bit0 -x903_bit0 -x904_bit0 -x905_bit0 -x906_bit0 -x907_bit0 -x908_bit0 -x909_bit0 -x910_bit0 -x911_bit0 -x912_bit0 -x913_bit0 -x914_bit0 -x915_bit0 -x916_bit0 -x917_bit0 -x918_bit0 -x919_bit0 -x920_bit0 -x921_bit0 -x922_bit0 -x923_bit0 -x924_bit0 -x925_bit0 -x926_bit0 -x927_bit0 -x928_bit0 -x929_bit0 -x930_bit0 -x931_bit0 -x932_bit0 -x933_bit0 -x934_bit0 -x935_bit0 -x936_bit0 -x937_bit0 -x938_bit0 -x939_bit0 x940_bit0 -x941_bit0 -x942_bit0 -x943_bit0 -x944_bit0 -x945_bit0 -x946_bit0 -x947_bit0 -x948_bit0 -x949_bit0 -x950_bit0 -x951_bit0 x952_bit0 -x953_bit0 -x954_bit0 -x955_bit0 -x956_bit0 -x957_bit0 -x958_bit0 -x959_bit0 -x960_bit0 -x961_bit0 -x962_bit0 -x963_bit0 -x964_bit0 -x965_bit0 -x966_bit0 -x967_bit0 -x968_bit0 -x969_bit0 -x970_bit0 -x971_bit0 -x972_bit0 -x973_bit0 -x974_bit0 -x975_bit0 -x976_bit0 -x977_bit0 -x978_bit0 -x979_bit0 -x980_bit0 -x981_bit0 -x982_bit0 -x983_bit0 -x984_bit0 -x985_bit0 -x986_bit0 -x987_bit0 -x988_bit0 -x989_bit0 -x990_bit0 -x991_bit0 -x992_bit0 -x993_bit0 -x994_bit0 -x995_bit0 -x996_bit0 -x997_bit0 -x998_bit0 -x999_bit0 -x1000_bit0 -x1001_bit0 -x1002_bit0 -x1003_bit0 -x1004_bit0 -x1005_bit0 -x1006_bit0 -x1007_bit0 -x1008_bit0 -x1009_bit0 -x1010_bit0 -x1011_bit0 -x1012_bit0 x1013_bit0 -x1014_bit0 -x1015_bit0 -x1016_bit0 -x1017_bit0 -x1018_bit0 -x1019_bit0 -x1020_bit0 -x1021_bit0 -x1022_bit0 -x1023_bit0 -x1024_bit0 -x1025_bit0 -x1026_bit0 -x1027_bit0 -x1028_bit0 -x1029_bit0 -x1030_bit0 -x1031_bit0 -x1032_bit0 -x1033_bit0 -x1034_bit0 -x1035_bit0 -x1036_bit0 -x1037_bit0 -x1038_bit0 -x1039_bit0 -x1040_bit0 -x1041_bit0 -x1042_bit0 -x1043_bit0 -x1044_bit0 -x1045_bit0 -x1046_bit0 -x1047_bit0 -x1048_bit0 -x1049_bit0 -x1050_bit0 -x1051_bit0 -x1052_bit0 -x1053_bit0 -x1054_bit0 -x1055_bit0 x1056_bit0 -x1057_bit0 -x1058_bit0 -x1059_bit0 -x1060_bit0 -x1061_bit0 -x1062_bit0 -x1063_bit0 -x1064_bit0 -x1065_bit0 -x1066_bit0 -x1067_bit0 -x1068_bit0 -x1069_bit0 -x1070_bit0 -x1071_bit0 -x1072_bit0 -x1073_bit0 -x1074_bit0 -x1075_bit0 -x1076_bit0 -x1077_bit0 -x1078_bit0 -x1079_bit0 -x1080_bit0 -x1081_bit0 -x1082_bit0 -x1083_bit0 -x1084_bit0 -x1085_bit0 -x1086_bit0 -x1087_bit0 -x1088_bit0 -x1089_bit0 -x1090_bit0 -x1091_bit0 -x1092_bit0 -x1093_bit0 -x1094_bit0 -x1095_bit0 -x1096_bit0 -x1097_bit0 -x1098_bit0 -x1099_bit0 -x1100_bit0 -x1101_bit0 -x1102_bit0 -x1103_bit0 -x1104_bit0 -x1105_bit0 -x1106_bit0 -x1107_bit0 -x1108_bit0 -x1109_bit0 -x1110_bit0 x1111_bit0 -x1112_bit0 -x1113_bit0 -x1114_bit0 -x1115_bit0 -x1116_bit0 -x1117_bit0 -x1118_bit0 -x1119_bit0 -x1120_bit0 -x1121_bit0 -x1122_bit0 -x1123_bit0 -x1124_bit0 -x1125_bit0 -x1126_bit0 -x1127_bit0 -x1128_bit0 -x1129_bit0 -x1130_bit0 -x1131_bit0 -x1132_bit0 -x1133_bit0 -x1134_bit0 -x1135_bit0 -x1136_bit0 -x1137_bit0 x1138_bit0 -x1139_bit0 -x1140_bit0 -x1141_bit0 -x1142_bit0 -x1143_bit0 -x1144_bit0 -x1145_bit0 -x1146_bit0 -x1147_bit0 -x1148_bit0 -x1149_bit0 -x1150_bit0 -x1151_bit0 -x1152_bit0 -x1153_bit0 -x1154_bit0 -x1155_bit0 -x1156_bit0 -x1157_bit0 -x1158_bit0 -x1159_bit0 -x1160_bit0 -x1161_bit0 -x1162_bit0 -x1163_bit0 -x1164_bit0 -x1165_bit0 -x1166_bit0 -x1167_bit0 -x1168_bit0 -x1169_bit0 -x1170_bit0 -x1171_bit0 -x1172_bit0 -x1173_bit0 -x1174_bit0 -x1175_bit0 -x1176_bit0 -x1177_bit0 -x1178_bit0 -x1179_bit0 -x1180_bit0 -x1181_bit0 -x1182_bit0 -x1183_bit0 -x1184_bit0 -x1185_bit0 -x1186_bit0 -x1187_bit0 -x1188_bit0 -x1189_bit0 -x1190_bit0 -x1191_bit0 -x1192_bit0 -x1193_bit0 -x1194_bit0 -x1195_bit0 -x1196_bit0 -x1197_bit0 -x1198_bit0 -x1199_bit0 -x1200_bit0 -x1201_bit0 -x1202_bit0 -x1203_bit0 -x1204_bit0 -x1205_bit0 -x1206_bit0 -x1207_bit0 -x1208_bit0 -x1209_bit0 -x1210_bit0 -x1211_bit0 -x1212_bit0 x1213_bit0 -x1214_bit0 -x1215_bit0 -x1216_bit0 -x1217_bit0 -x1218_bit0 -x1219_bit0 x1220_bit0 -x1221_bit0 -x1222_bit0 -x1223_bit0 -x1224_bit0 -x1225_bit0 -x1226_bit0 -x1227_bit0 -x1228_bit0 -x1229_bit0 -x1230_bit0 -x1231_bit0 -x1232_bit0 -x1233_bit0 -x1234_bit0 -x1235_bit0 -x1236_bit0 -x1237_bit0 -x1238_bit0 -x1239_bit0 -x1240_bit0 -x1241_bit0 -x1242_bit0 -x1243_bit0 -x1244_bit0 -x1245_bit0 -x1246_bit0 -x1247_bit0 -x1248_bit0 -x1249_bit0 -x1250_bit0 -x1251_bit0 -x1252_bit0 -x1253_bit0 -x1254_bit0 -x1255_bit0 -x1256_bit0 -x1257_bit0 -x1258_bit0 -x1259_bit0 -x1260_bit0 -x1261_bit0 -x1262_bit0 -x1263_bit0 -x1264_bit0 -x1265_bit0 -x1266_bit0 -x1267_bit0 -x1268_bit0 -x1269_bit0 -x1270_bit0 -x1271_bit0 -x1272_bit0 -x1273_bit0 -x1274_bit0 -x1275_bit0 -x1276_bit0 -x1277_bit0 -x1278_bit0 -x1279_bit0 -x1280_bit0 -x1281_bit0 -x1282_bit0 -x1283_bit0 -x1284_bit0 -x1285_bit0 -x1286_bit0 -x1287_bit0 -x1288_bit0 -x1289_bit0 -x1290_bit0 -x1291_bit0 -x1292_bit0 x1293_bit0 -x1294_bit0 -x1295_bit0 -x1296_bit0 -x1297_bit0 -x1298_bit0 -x1299_bit0 -x1300_bit0 -x1301_bit0 -x1302_bit0 -x1303_bit0 -x1304_bit0 -x1305_bit0 -x1306_bit0 -x1307_bit0 -x1308_bit0 -x1309_bit0 -x1310_bit0 -x1311_bit0 -x1312_bit0 -x1313_bit0 -x1314_bit0 -x1315_bit0 -x1316_bit0 -x1317_bit0 -x1318_bit0 -x1319_bit0 -x1320_bit0 -x1321_bit0 -x1322_bit0 -x1323_bit0 -x1324_bit0 -x1325_bit0 -x1326_bit0 x1327_bit0 -x1328_bit0 -x1329_bit0 -x1330_bit0 -x1331_bit0 -x1332_bit0 -x1333_bit0 -x1334_bit0 -x1335_bit0 -x1336_bit0 -x1337_bit0 -x1338_bit0 -x1339_bit0 -x1340_bit0 -x1341_bit0 -x1342_bit0 -x1343_bit0 -x1344_bit0 -x1345_bit0 -x1346_bit0 -x1347_bit0 -x1348_bit0 -x1349_bit0 -x1350_bit0 -x1351_bit0 -x1352_bit0 -x1353_bit0 -x1354_bit0 -x1355_bit0 -x1356_bit0 -x1357_bit0 -x1358_bit0 -x1359_bit0 -x1360_bit0 -x1361_bit0 -x1362_bit0 -x1363_bit0 -x1364_bit0 -x1365_bit0 -x1366_bit0 -x1367_bit0 -x1368_bit0 -x1369_bit0 -x1370_bit0 -x1371_bit0 -x1372_bit0 -x1373_bit0 -x1374_bit0 -x1375_bit0 -x1376_bit0 x1377_bit0 -x1378_bit0 -x1379_bit0 -x1380_bit0 -x1381_bit0 -x1382_bit0 -x1383_bit0 -x1384_bit0 -x1385_bit0 -x1386_bit0 -x1387_bit0 -x1388_bit0 -x1389_bit0 -x1390_bit0 -x1391_bit0 -x1392_bit0 -x1393_bit0 -x1394_bit0 -x1395_bit0 -x1396_bit0 -x1397_bit0 -x1398_bit0 -x1399_bit0 -x1400_bit0 -x1401_bit0 -x1402_bit0 -x1403_bit0 -x1404_bit0 -x1405_bit0 -x1406_bit0 -x1407_bit0 -x1408_bit0 -x1409_bit0 -x1410_bit0 -x1411_bit0 -x1412_bit0 -x1413_bit0 -x1414_bit0 -x1415_bit0 -x1416_bit0 -x1417_bit0 -x1418_bit0 -x1419_bit0 -x1420_bit0 -x1421_bit0 -x1422_bit0 -x1423_bit0 -x1424_bit0 -x1425_bit0 -x1426_bit0 -x1427_bit0 -x1428_bit0 -x1429_bit0 -x1430_bit0 -x1431_bit0 -x1432_bit0 x1433_bit0 -x1434_bit0 -x1435_bit0 -x1436_bit0 -x1437_bit0 -x1438_bit0 -x1439_bit0 -x1440_bit0 -x1441_bit0 -x1442_bit0 -x1443_bit0 -x1444_bit0 -x1445_bit0 -x1446_bit0 -x1447_bit0 -x1448_bit0 -x1449_bit0 -x1450_bit0 -x1451_bit0 -x1452_bit0 -x1453_bit0 -x1454_bit0 -x1455_bit0 -x1456_bit0 -x1457_bit0 -x1458_bit0 -x1459_bit0 -x1460_bit0 -x1461_bit0 -x1462_bit0 -x1463_bit0 -x1464_bit0 -x1465_bit0 -x1466_bit0 -x1467_bit0 -x1468_bit0 -x1469_bit0 -x1470_bit0 -x1471_bit0 -x1472_bit0 -x1473_bit0 -x1474_bit0 x1475_bit0 -x1476_bit0 -x1477_bit0 -x1478_bit0 -x1479_bit0 -x1480_bit0 -x1481_bit0 -x1482_bit0 -x1483_bit0 -x1484_bit0 -x1485_bit0 -x1486_bit0 -x1487_bit0 -x1488_bit0 x1489_bit0 -x1490_bit0 -x1491_bit0 -x1492_bit0 -x1493_bit0 -x1494_bit0 -x1495_bit0 -x1496_bit0 -x1497_bit0 -x1498_bit0 -x1499_bit0 -x1500_bit0 -x1501_bit0 -x1502_bit0 -x1503_bit0 -x1504_bit0 -x1505_bit0 -x1506_bit0 -x1507_bit0 -x1508_bit0 -x1509_bit0 -x1510_bit0 -x1511_bit0 -x1512_bit0 -x1513_bit0 -x1514_bit0 -x1515_bit0 -x1516_bit0 -x1517_bit0 -x1518_bit0 -x1519_bit0 -x1520_bit0 -x1521_bit0 -x1522_bit0 -x1523_bit0 -x1524_bit0 -x1525_bit0 -x1526_bit0 -x1527_bit0 -x1528_bit0 -x1529_bit0 -x1530_bit0 -x1531_bit0 -x1532_bit0 -x1533_bit0 -x1534_bit0 -x1535_bit0 -x1536_bit0 -x1537_bit0 -x1538_bit0 x1539_bit0 -x1540_bit0 -x1541_bit0 -x1542_bit0 -x1543_bit0 -x1544_bit0 -x1545_bit0 -x1546_bit0 -x1547_bit0 -x1548_bit0 -x1549_bit0 -x1550_bit0 -x1551_bit0 -x1552_bit0 -x1553_bit0 -x1554_bit0 -x1555_bit0 -x1556_bit0 -x1557_bit0 -x1558_bit0 -x1559_bit0 -x1560_bit0 -x1561_bit0 -x1562_bit0 -x1563_bit0 -x1564_bit0 -x1565_bit0 -x1566_bit0 -x1567_bit0 -x1568_bit0 -x1569_bit0 -x1570_bit0 -x1571_bit0 -x1572_bit0 -x1573_bit0 -x1574_bit0 -x1575_bit0 -x1576_bit0 -x1577_bit0 -x1578_bit0 -x1579_bit0 -x1580_bit0 -x1581_bit0 -x1582_bit0 -x1583_bit0 -x1584_bit0 -x1585_bit0 -x1586_bit0 -x1587_bit0 -x1588_bit0 -x1589_bit0 -x1590_bit0 -x1591_bit0 -x1592_bit0 -x1593_bit0 -x1594_bit0 -x1595_bit0 -x1596_bit0 -x1597_bit0 -x1598_bit0 -x1599_bit0 -x1600_bit0 x1601_bit0 -x1602_bit0 -x1603_bit0 -x1604_bit0 -x1605_bit0 -x1606_bit0 -x1607_bit0 -x1608_bit0 -x1609_bit0 -x1610_bit0 -x1611_bit0 -x1612_bit0 -x1613_bit0 -x1614_bit0 -x1615_bit0 -x1616_bit0 -x1617_bit0 -x1618_bit0 -x1619_bit0 -x1620_bit0 -x1621_bit0 -x1622_bit0 -x1623_bit0 -x1624_bit0 -x1625_bit0 -x1626_bit0 -x1627_bit0 -x1628_bit0 -x1629_bit0 -x1630_bit0 -x1631_bit0 -x1632_bit0 -x1633_bit0 -x1634_bit0 -x1635_bit0 -x1636_bit0 -x1637_bit0 -x1638_bit0 -x1639_bit0 -x1640_bit0 -x1641_bit0 -x1642_bit0 -x1643_bit0 -x1644_bit0 -x1645_bit0 -x1646_bit0 -x1647_bit0 -x1648_bit0 -x1649_bit0 -x1650_bit0 -x1651_bit0 -x1652_bit0 -x1653_bit0 x1654_bit0 -x1655_bit0 -x1656_bit0 -x1657_bit0 -x1658_bit0 -x1659_bit0 -x1660_bit0 -x1661_bit0 -x1662_bit0 -x1663_bit0 -x1664_bit0 -x1665_bit0 -x1666_bit0 -x1667_bit0 -x1668_bit0 -x1669_bit0 -x1670_bit0 -x1671_bit0 -x1672_bit0 -x1673_bit0 -x1674_bit0 -x1675_bit0 -x1676_bit0 -x1677_bit0 -x1678_bit0 -x1679_bit0 -x1680_bit0 -x1681_bit0 -x1682_bit0 -x1683_bit0 -x1684_bit0 -x1685_bit0 -x1686_bit0 -x1687_bit0 -x1688_bit0 -x1689_bit0 -x1690_bit0 -x1691_bit0 -x1692_bit0 -x1693_bit0 -x1694_bit0 -x1695_bit0 -x1696_bit0 -x1697_bit0 -x1698_bit0 -x1699_bit0 -x1700_bit0 -x1701_bit0 x1702_bit0 -x1703_bit0 -x1704_bit0 -x1705_bit0 -x1706_bit0 -x1707_bit0 -x1708_bit0 -x1709_bit0 -x1710_bit0 -x1711_bit0 -x1712_bit0 x1713_bit0 -x1714_bit0 -x1715_bit0 -x1716_bit0 -x1717_bit0 -x1718_bit0 -x1719_bit0 -x1720_bit0 -x1721_bit0 -x1722_bit0 -x1723_bit0 -x1724_bit0 -x1725_bit0 -x1726_bit0 -x1727_bit0 -x1728_bit0 -x1729_bit0 -x1730_bit0 -x1731_bit0 -x1732_bit0 -x1733_bit0 -x1734_bit0 -x1735_bit0 -x1736_bit0 -x1737_bit0 -x1738_bit0 -x1739_bit0 -x1740_bit0 -x1741_bit0 -x1742_bit0 -x1743_bit0 -x1744_bit0 -x1745_bit0 -x1746_bit0 -x1747_bit0 -x1748_bit0 -x1749_bit0 -x1750_bit0 -x1751_bit0 -x1752_bit0 -x1753_bit0 -x1754_bit0 -x1755_bit0 -x1756_bit0 -x1757_bit0 -x1758_bit0 -x1759_bit0 -x1760_bit0 -x1761_bit0 -x1762_bit0 -x1763_bit0 -x1764_bit0 -x1765_bit0 -x1766_bit0 -x1767_bit0 -x1768_bit0 -x1769_bit0 -x1770_bit0 -x1771_bit0 -x1772_bit0 -x1773_bit0 x1774_bit0 -x1775_bit0 -x1776_bit0 -x1777_bit0 -x1778_bit0 -x1779_bit0 -x1780_bit0 -x1781_bit0 -x1782_bit0 -x1783_bit0 -x1784_bit0 -x1785_bit0 -x1786_bit0 -x1787_bit0 -x1788_bit0 -x1789_bit0 -x1790_bit0 -x1791_bit0 -x1792_bit0 -x1793_bit0 -x1794_bit0 -x1795_bit0 -x1796_bit0 -x1797_bit0 -x1798_bit0 -x1799_bit0 -x1800_bit0 -x1801_bit0 x1802_bit0 -x1803_bit0 -x1804_bit0 -x1805_bit0 -x1806_bit0 -x1807_bit0 -x1808_bit0 -x1809_bit0 -x1810_bit0 -x1811_bit0 -x1812_bit0 -x1813_bit0 -x1814_bit0 -x1815_bit0 -x1816_bit0 -x1817_bit0 -x1818_bit0 -x1819_bit0 -x1820_bit0 -x1821_bit0 -x1822_bit0 -x1823_bit0 -x1824_bit0 -x1825_bit0 -x1826_bit0 -x1827_bit0 -x1828_bit0 -x1829_bit0 -x1830_bit0 -x1831_bit0 -x1832_bit0 -x1833_bit0 -x1834_bit0 -x1835_bit0 -x1836_bit0 -x1837_bit0 -x1838_bit0 -x1839_bit0 -x1840_bit0 -x1841_bit0 -x1842_bit0 -x1843_bit0 -x1844_bit0 -x1845_bit0 -x1846_bit0 -x1847_bit0 -x1848_bit0 -x1849_bit0 -x1850_bit0 -x1851_bit0 -x1852_bit0 -x1853_bit0 -x1854_bit0 -x1855_bit0 -x1856_bit0 -x1857_bit0 -x1858_bit0 -x1859_bit0 -x1860_bit0 -x1861_bit0 -x1862_bit0 -x1863_bit0 -x1864_bit0 -x1865_bit0 -x1866_bit0 -x1867_bit0 -x1868_bit0 -x1869_bit0 -x1870_bit0 -x1871_bit0 -x1872_bit0 -x1873_bit0 -x1874_bit0 -x1875_bit0 -x1876_bit0 -x1877_bit0 -x1878_bit0 -x1879_bit0 -x1880_bit0 x1881_bit0 -x1882_bit0 -x1883_bit0 -x1884_bit0 -x1885_bit0 -x1886_bit0 -x1887_bit0 -x1888_bit0 -x1889_bit0 -x1890_bit0 -x1891_bit0 -x1892_bit0 -x1893_bit0 -x1894_bit0 -x1895_bit0 -x1896_bit0 -x1897_bit0 -x1898_bit0 -x1899_bit0 -x1900_bit0 -x1901_bit0 -x1902_bit0 -x1903_bit0 -x1904_bit0 -x1905_bit0 -x1906_bit0 -x1907_bit0 -x1908_bit0 -x1909_bit0 -x1910_bit0 -x1911_bit0 -x1912_bit0 -x1913_bit0 -x1914_bit0 -x1915_bit0 -x1916_bit0 -x1917_bit0 -x1918_bit0 -x1919_bit0 -x1920_bit0 -x1921_bit0 -x1922_bit0 -x1923_bit0 -x1924_bit0 -x1925_bit0 -x1926_bit0 -x1927_bit0 -x1928_bit0 -x1929_bit0 -x1930_bit0 x1931_bit0 -x1932_bit0 -x1933_bit0 -x1934_bit0 -x1935_bit0 -x1936_bit0 -x1937_bit0 -x1938_bit0 -x1939_bit0 -x1940_bit0 -x1941_bit0 -x1942_bit0 -x1943_bit0 -x1944_bit0 -x1945_bit0 -x1946_bit0 -x1947_bit0 -x1948_bit0 x1949_bit0 -x1950_bit0 -x1951_bit0 -x1952_bit0 -x1953_bit0 -x1954_bit0 -x1955_bit0 -x1956_bit0 -x1957_bit0 -x1958_bit0 -x1959_bit0 -x1960_bit0 -x1961_bit0 -x1962_bit0 -x1963_bit0 -x1964_bit0 -x1965_bit0 -x1966_bit0 -x1967_bit0 -x1968_bit0 -x1969_bit0 -x1970_bit0 -x1971_bit0 -x1972_bit0 -x1973_bit0 -x1974_bit0 -x1975_bit0 -x1976_bit0 -x1977_bit0 -x1978_bit0 -x1979_bit0 -x1980_bit0 -x1981_bit0 -x1982_bit0 -x1983_bit0 -x1984_bit0 -x1985_bit0 -x1986_bit0 -x1987_bit0 -x1988_bit0 -x1989_bit0 -x1990_bit0 -x1991_bit0 -x1992_bit0 -x1993_bit0 -x1994_bit0 -x1995_bit0 -x1996_bit0 x#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 1.03 0.97 0.91 2/54 3305
Raw data (stat): 3305 (runsolver) D 3304 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485547002 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 2564 0 0 0 992 6 0 0 25 0 1 0 485547002 12718080 2481 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3105 2481 603 41 0 3064 0
vsize: 12420
[startup+20.0007 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 2576 0 0 0 1991 7 0 0 25 0 1 0 485547002 12718080 2493 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3105 2493 603 41 0 3064 0
vsize: 12420
[startup+30.0003 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 2582 0 0 0 2990 7 0 0 25 0 1 0 485547002 12718080 2499 4294967295 134512640 134672761 3221224544 3221223752 134561962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3105 2499 603 41 0 3064 0
vsize: 12420
[startup+40.0002 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 2609 0 0 0 3990 7 0 0 25 0 1 0 485547002 12853248 2526 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3138 2526 603 41 0 3097 0
vsize: 12552
[startup+50.0008 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 2653 0 0 0 4990 7 0 0 25 0 1 0 485547002 12988416 2570 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3171 2570 603 41 0 3130 0
vsize: 12684
[startup+60.0011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 2685 0 0 0 5990 8 0 0 25 0 1 0 485547002 13266944 2602 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3239 2602 603 41 0 3198 0
vsize: 12956
[startup+70.0013 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 2751 0 0 0 6990 8 0 0 25 0 1 0 485547002 13402112 2668 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3272 2668 603 41 0 3231 0
vsize: 13088
[startup+80.0018 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 2822 0 0 0 7989 8 0 0 25 0 1 0 485547002 13807616 2739 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3371 2739 603 41 0 3330 0
vsize: 13484
[startup+90.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 2952 0 0 0 8989 8 0 0 25 0 1 0 485547002 14397440 2869 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3515 2869 603 41 0 3474 0
vsize: 14060
[startup+100.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 3081 0 0 0 9988 9 0 0 25 0 1 0 485547002 14794752 2998 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3612 2998 603 41 0 3571 0
vsize: 14448
[startup+110.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 3183 0 0 0 10988 10 0 0 25 0 1 0 485547002 15200256 3100 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3711 3100 603 41 0 3670 0
vsize: 14844
[startup+120.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 3266 0 0 0 11988 10 0 0 25 0 1 0 485547002 15605760 3183 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3183 603 41 0 3769 0
vsize: 15240
[startup+130.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 3376 0 0 0 12988 10 0 0 25 0 1 0 485547002 16003072 3293 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3293 603 41 0 3866 0
vsize: 15628
[startup+140.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 3511 0 0 0 13987 11 0 0 25 0 1 0 485547002 16543744 3428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4039 3428 603 41 0 3998 0
vsize: 16156
[startup+150.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 3618 0 0 0 14987 11 0 0 25 0 1 0 485547002 16936960 3535 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4135 3535 603 41 0 4094 0
vsize: 16540
[startup+160.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 3760 0 0 0 15987 11 0 0 25 0 1 0 485547002 17739776 3677 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4331 3677 603 41 0 4290 0
vsize: 17324
[startup+170.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 3838 0 0 0 16987 12 0 0 25 0 1 0 485547002 18010112 3755 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4397 3755 603 41 0 4356 0
vsize: 17588
[startup+180.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 3952 0 0 0 17987 12 0 0 25 0 1 0 485547002 18407424 3869 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4494 3869 603 41 0 4453 0
vsize: 17976
[startup+190.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 4126 0 0 0 18986 12 0 0 25 0 1 0 485547002 19214336 4043 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4691 4043 603 41 0 4650 0
vsize: 18764
[startup+200.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 4358 0 0 0 19986 13 0 0 25 0 1 0 485547002 20152320 4275 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4920 4275 603 41 0 4879 0
vsize: 19680
[startup+210.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 4486 0 0 0 20986 14 0 0 25 0 1 0 485547002 20692992 4403 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5052 4403 603 41 0 5011 0
vsize: 20208
[startup+220.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 4707 0 0 0 21985 15 0 0 25 0 1 0 485547002 21499904 4624 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5249 4624 603 41 0 5208 0
vsize: 20996
[startup+230.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 4944 0 0 0 22984 16 0 0 25 0 1 0 485547002 22441984 4861 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5479 4861 603 41 0 5438 0
vsize: 21916
[startup+240.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 5173 0 0 0 23984 16 0 0 25 0 1 0 485547002 23388160 5090 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5710 5090 603 41 0 5669 0
vsize: 22840
[startup+250.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 5528 0 0 0 24983 17 0 0 25 0 1 0 485547002 24862720 5445 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6070 5445 603 41 0 6029 0
vsize: 24280
[startup+260.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 5816 0 0 0 25983 18 0 0 25 0 1 0 485547002 26062848 5733 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6363 5733 603 41 0 6322 0
vsize: 25452
[startup+270.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 6194 0 0 0 26982 19 0 0 25 0 1 0 485547002 27529216 6111 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6721 6111 603 41 0 6680 0
vsize: 26884
[startup+280.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 6632 0 0 0 27981 20 0 0 25 0 1 0 485547002 29396992 6549 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7177 6549 603 41 0 7136 0
vsize: 28708
[startup+290.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 6864 0 0 0 28980 21 0 0 25 0 1 0 485547002 30334976 6781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7406 6781 603 41 0 7365 0
vsize: 29624
[startup+300.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 7116 0 0 0 29979 22 0 0 25 0 1 0 485547002 31277056 7033 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7636 7033 603 41 0 7595 0
vsize: 30544
[startup+310.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 7441 0 0 0 30978 23 0 0 25 0 1 0 485547002 32620544 7358 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7964 7358 603 41 0 7923 0
vsize: 31856
[startup+320.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 7773 0 0 0 31977 24 0 0 25 0 1 0 485547002 34226176 7690 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8356 7690 603 41 0 8315 0
vsize: 33424
[startup+330.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 8066 0 0 0 32977 25 0 0 25 0 1 0 485547002 35438592 7983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8652 7983 603 41 0 8611 0
vsize: 34608
[startup+340.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 8395 0 0 0 33976 25 0 0 25 0 1 0 485547002 36777984 8312 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8979 8312 603 41 0 8938 0
vsize: 35916
[startup+350.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 8754 0 0 0 34975 27 0 0 25 0 1 0 485547002 38252544 8671 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9339 8671 603 41 0 9298 0
vsize: 37356
[startup+360.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 9136 0 0 0 35974 28 0 0 25 0 1 0 485547002 39858176 9053 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9731 9053 603 41 0 9690 0
vsize: 38924
[startup+370.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 9432 0 0 0 36973 29 0 0 25 0 1 0 485547002 41062400 9349 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10025 9349 603 41 0 9984 0
vsize: 40100
[startup+380.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 9735 0 0 0 37972 30 0 0 25 0 1 0 485547002 42278912 9652 4294967295 134512640 134672761 3221224544 3221223728 134558925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10322 9652 603 41 0 10281 0
vsize: 41288
[startup+390.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 10208 0 0 0 38971 32 0 0 25 0 1 0 485547002 44146688 10125 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10778 10125 603 41 0 10737 0
vsize: 43112
[startup+400.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 10581 0 0 0 39970 33 0 0 25 0 1 0 485547002 45748224 10498 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11169 10498 603 41 0 11128 0
vsize: 44676
[startup+410.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 10771 0 0 0 40969 34 0 0 25 0 1 0 485547002 46424064 10688 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 10688 603 41 0 11293 0
vsize: 45336
[startup+420.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 11086 0 0 0 41968 35 0 0 25 0 1 0 485547002 47763456 11003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11661 11003 603 41 0 11620 0
vsize: 46644
[startup+430.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 11442 0 0 0 42967 36 0 0 25 0 1 0 485547002 49238016 11359 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12021 11359 603 41 0 11980 0
vsize: 48084
[startup+440.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 11709 0 0 0 43967 36 0 0 25 0 1 0 485547002 50311168 11626 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12283 11626 603 41 0 12242 0
vsize: 49132
[startup+450.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 12082 0 0 0 44966 37 0 0 25 0 1 0 485547002 51781632 11999 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12642 11999 603 41 0 12601 0
vsize: 50568
[startup+460.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 12414 0 0 0 45965 38 0 0 25 0 1 0 485547002 53248000 12331 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13000 12331 603 41 0 12959 0
vsize: 52000
[startup+470.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 12798 0 0 0 46964 39 0 0 25 0 1 0 485547002 54718464 12715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13359 12715 603 41 0 13318 0
vsize: 53436
[startup+480.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 13157 0 0 0 47964 40 0 0 25 0 1 0 485547002 56188928 13074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13718 13074 603 41 0 13677 0
vsize: 54872
[startup+490.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 13486 0 0 0 48963 41 0 0 25 0 1 0 485547002 57536512 13403 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14047 13403 603 41 0 14006 0
vsize: 56188
[startup+500.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 13827 0 0 0 49962 42 0 0 25 0 1 0 485547002 58994688 13744 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14403 13744 603 41 0 14362 0
vsize: 57612
[startup+510.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 14096 0 0 0 50962 43 0 0 25 0 1 0 485547002 60071936 14013 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14666 14013 603 41 0 14625 0
vsize: 58664
[startup+520.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 14433 0 0 0 51961 43 0 0 25 0 1 0 485547002 61415424 14350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14994 14350 603 41 0 14953 0
vsize: 59976
[startup+530.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 14711 0 0 0 52961 44 0 0 25 0 1 0 485547002 62595072 14628 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15282 14628 603 41 0 15241 0
vsize: 61128
[startup+540.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 14996 0 0 0 53960 45 0 0 25 0 1 0 485547002 63799296 14913 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15576 14913 603 41 0 15535 0
vsize: 62304
[startup+550.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 15336 0 0 0 54959 46 0 0 25 0 1 0 485547002 65134592 15253 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15902 15253 603 41 0 15861 0
vsize: 63608
[startup+560.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 15561 0 0 0 55958 47 0 0 25 0 1 0 485547002 66072576 15478 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16131 15478 603 41 0 16090 0
vsize: 64524
[startup+570.005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 15840 0 0 0 56957 48 0 0 25 0 1 0 485547002 67145728 15757 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16393 15757 603 41 0 16352 0
vsize: 65572
[startup+580.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 16208 0 0 0 57956 50 0 0 25 0 1 0 485547002 68624384 16125 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16754 16125 603 41 0 16713 0
vsize: 67016
[startup+590.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 16545 0 0 0 58956 51 0 0 25 0 1 0 485547002 70098944 16462 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17114 16462 603 41 0 17073 0
vsize: 68456
[startup+600.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 16975 0 0 0 59955 51 0 0 25 0 1 0 485547002 71831552 16892 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17537 16892 603 41 0 17496 0
vsize: 70148
[startup+610.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 17311 0 0 0 60955 52 0 0 25 0 1 0 485547002 73175040 17228 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17865 17228 603 41 0 17824 0
vsize: 71460
[startup+620.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18268 0 0 0 61951 56 0 0 25 0 1 0 485547002 76607488 18185 4294967295 134512640 134672761 3221224544 3221223844 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18703 18185 603 41 0 18662 0
vsize: 74812
[startup+630.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18275 0 0 0 62951 56 0 0 25 0 1 0 485547002 76607488 18192 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18703 18192 603 41 0 18662 0
vsize: 74812
[startup+640.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 63951 56 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+650.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 64951 56 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+660.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 65951 56 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+670.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 3305
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 66953 56 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+680.04 s]
Raw data (loadavg): 1.08 0.99 0.92 3/58 3351
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 67953 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+690.051 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 3358
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 68954 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+700.051 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 3358
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 69955 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+710.051 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 3358
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 70955 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+720.052 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 3358
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 71955 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+730.051 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 3358
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 72955 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+740.051 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 3358
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 73955 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+750.051 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 74955 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+760.052 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 75956 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+770.051 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 76956 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+780.05 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 77956 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+790.051 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 78956 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+800.051 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 79956 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+810.051 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 80956 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+820.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 81957 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+830.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 82957 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+840.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 83957 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+850.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 84957 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+860.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 85957 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+870.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 86957 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+880.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 87958 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+890.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 88958 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+900.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 89958 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+910.05 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 90958 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+920.05 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 91958 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+930.05 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 92958 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+940.05 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18305 0 0 0 93959 57 0 0 25 0 1 0 485547002 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18743 18222 603 41 0 18702 0
vsize: 74972
[startup+950.05 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18423 0 0 0 94958 58 0 0 25 0 1 0 485547002 77295616 18340 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18871 18340 603 41 0 18830 0
vsize: 75484
[startup+960.05 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18729 0 0 0 95958 58 0 0 25 0 1 0 485547002 78495744 18646 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19164 18646 603 41 0 19123 0
vsize: 76656
[startup+970.049 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 18982 0 0 0 96957 59 0 0 25 0 1 0 485547002 79560704 18899 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19424 18899 603 41 0 19383 0
vsize: 77696
[startup+980.049 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 19187 0 0 0 97957 60 0 0 25 0 1 0 485547002 80359424 19104 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19619 19104 603 41 0 19578 0
vsize: 78476
[startup+990.05 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 19441 0 0 0 98956 61 0 0 25 0 1 0 485547002 81420288 19358 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19878 19358 603 41 0 19837 0
vsize: 79512
[startup+1000.05 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 19740 0 0 0 99955 62 0 0 25 0 1 0 485547002 82620416 19657 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20171 19657 603 41 0 20130 0
vsize: 80684
[startup+1010.05 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 20073 0 0 0 100954 63 0 0 25 0 1 0 485547002 84066304 19990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20524 19990 603 41 0 20483 0
vsize: 82096
[startup+1020.05 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 20333 0 0 0 101953 64 0 0 25 0 1 0 485547002 85135360 20250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20785 20250 603 41 0 20744 0
vsize: 83140
[startup+1030.05 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 20597 0 0 0 102953 65 0 0 25 0 1 0 485547002 86224896 20514 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21051 20514 603 41 0 21010 0
vsize: 84204
[startup+1040.05 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 20833 0 0 0 103952 66 0 0 25 0 1 0 485547002 87150592 20750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21277 20750 603 41 0 21236 0
vsize: 85108
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3360
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 21198 0 0 0 104951 67 0 0 25 0 1 0 485547002 88625152 21115 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21637 21115 603 41 0 21596 0
vsize: 86548
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 21503 0 0 0 105950 68 0 0 25 0 1 0 485547002 89833472 21420 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21932 21420 603 41 0 21891 0
vsize: 87728
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 21865 0 0 0 106949 69 0 0 25 0 1 0 485547002 91308032 21782 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22292 21782 603 41 0 22251 0
vsize: 89168
[startup+1080.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 22138 0 0 0 107949 70 0 0 25 0 1 0 485547002 92516352 22055 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22587 22055 603 41 0 22546 0
vsize: 90348
[startup+1090.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 22377 0 0 0 108948 71 0 0 25 0 1 0 485547002 93454336 22294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22816 22294 603 41 0 22775 0
vsize: 91264
[startup+1100.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 22627 0 0 0 109948 71 0 0 25 0 1 0 485547002 94535680 22544 4294967295 134512640 134672761 3221224544 3221223648 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23080 22544 603 41 0 23039 0
vsize: 92320
[startup+1110.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 22909 0 0 0 110947 72 0 0 25 0 1 0 485547002 95612928 22826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23343 22826 603 41 0 23302 0
vsize: 93372
[startup+1120.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 23195 0 0 0 111946 73 0 0 25 0 1 0 485547002 96829440 23112 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23640 23112 603 41 0 23599 0
vsize: 94560
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 23472 0 0 0 112945 74 0 0 25 0 1 0 485547002 97898496 23389 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23901 23389 603 41 0 23860 0
vsize: 95604
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 23771 0 0 0 113944 76 0 0 25 0 1 0 485547002 99241984 23688 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24229 23688 603 41 0 24188 0
vsize: 96916
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 24044 0 0 0 114943 77 0 0 25 0 1 0 485547002 100306944 23961 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24489 23961 603 41 0 24448 0
vsize: 97956
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 24391 0 0 0 115942 78 0 0 25 0 1 0 485547002 101765120 24308 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24845 24308 603 41 0 24804 0
vsize: 99380
[startup+1170.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 24723 0 0 0 116940 79 0 0 25 0 1 0 485547002 103100416 24640 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25171 24640 603 41 0 25130 0
vsize: 100684
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 24998 0 0 0 117940 80 0 0 25 0 1 0 485547002 104161280 24915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25430 24915 603 41 0 25389 0
vsize: 101720
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 25276 0 0 0 118939 81 0 0 25 0 1 0 485547002 105345024 25193 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25719 25193 603 41 0 25678 0
vsize: 102876
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 3362
Raw data (stat): 3305 (minisat+) R 3304 22932 22931 0 -1 0 25550 0 0 0 119939 82 0 0 25 0 1 0 485547002 106541056 25467 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26011 25467 603 41 0 25970 0
vsize: 104044
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 3362
Raw data (stat): 3305 (minisat+) Z 3304 22932 22931 0 -1 12 25553 0 0 0 119939 87 0 0 25 0 1 0 485547002 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.27
CPU user time (s): 1199.39
CPU system time (s): 0.871867
CPU usage (%): 100.013
Max. virtual memory (Kb): 104044
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####