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-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-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	920
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.75
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 15520

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 04:44:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17378 boxname=wulflinc20 idbench=1337 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1ff3cc3253012886aa21be4feac6111e  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-10teams.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-10teams.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-10teams.opb
IDLAUNCH: 17378
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        874984 kB
Buffers:          3560 kB
Cached:         132672 kB
SwapCached:        516 kB
Active:          29972 kB
Inactive:       108244 kB
HighTotal:      131008 kB
HighFree:        36932 kB
LowTotal:       903652 kB
LowFree:        838052 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            15804 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:04:55 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 17378 7 1200.26 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): 0.92 0.95 0.94 2/54 28717
Raw data (stat): 28717 (runsolver) R 28716 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542298651 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.93 0.96 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 2564 0 0 0 992 6 0 0 25 0 1 0 542298651 12718080 2481 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.0015 s]
Raw data (loadavg): 0.94 0.96 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 2575 0 0 0 1991 7 0 0 25 0 1 0 542298651 12718080 2492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3105 2492 603 41 0 3064 0
vsize: 12420
[startup+30.001 s]
Raw data (loadavg): 0.95 0.96 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 2582 0 0 0 2990 7 0 0 25 0 1 0 542298651 12718080 2499 4294967295 134512640 134672761 3221224544 3221223740 134556584 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.0081 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 2609 0 0 0 3991 7 0 0 25 0 1 0 542298651 12853248 2526 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.0084 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 2653 0 0 0 4991 7 0 0 25 0 1 0 542298651 12988416 2570 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.008 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 2685 0 0 0 5991 7 0 0 25 0 1 0 542298651 13266944 2602 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.0082 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 2747 0 0 0 6991 7 0 0 25 0 1 0 542298651 13402112 2664 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3272 2664 603 41 0 3231 0
vsize: 13088
[startup+80.0085 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 2821 0 0 0 7989 8 0 0 25 0 1 0 542298651 13807616 2738 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3371 2738 603 41 0 3330 0
vsize: 13484
[startup+90.0081 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 2927 0 0 0 8989 9 0 0 25 0 1 0 542298651 14213120 2844 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3470 2844 603 41 0 3429 0
vsize: 13880
[startup+100.008 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 3072 0 0 0 9988 9 0 0 25 0 1 0 542298651 14794752 2989 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3612 2989 603 41 0 3571 0
vsize: 14448
[startup+110.008 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 3178 0 0 0 10988 10 0 0 25 0 1 0 542298651 15200256 3095 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3711 3095 603 41 0 3670 0
vsize: 14844
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 3256 0 0 0 11988 10 0 0 25 0 1 0 542298651 15605760 3173 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3173 603 41 0 3769 0
vsize: 15240
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 3370 0 0 0 12988 10 0 0 25 0 1 0 542298651 16003072 3287 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3907 3287 603 41 0 3866 0
vsize: 15628
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 3496 0 0 0 13988 11 0 0 25 0 1 0 542298651 16543744 3413 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4039 3413 603 41 0 3998 0
vsize: 16156
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 3605 0 0 0 14987 11 0 0 25 0 1 0 542298651 16936960 3522 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4135 3522 603 41 0 4094 0
vsize: 16540
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 3760 0 0 0 15987 11 0 0 25 0 1 0 542298651 17739776 3677 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 3825 0 0 0 16987 12 0 0 25 0 1 0 542298651 18010112 3742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4397 3742 603 41 0 4356 0
vsize: 17588
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 3940 0 0 0 17987 12 0 0 25 0 1 0 542298651 18407424 3857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4494 3857 603 41 0 4453 0
vsize: 17976
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 4110 0 0 0 18986 13 0 0 25 0 1 0 542298651 19079168 4027 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4658 4027 603 41 0 4617 0
vsize: 18632
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 4330 0 0 0 19985 14 0 0 25 0 1 0 542298651 20021248 4247 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4888 4247 603 41 0 4847 0
vsize: 19552
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 4481 0 0 0 20985 14 0 0 25 0 1 0 542298651 20557824 4398 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5019 4398 603 41 0 4978 0
vsize: 20076
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 4700 0 0 0 21985 15 0 0 25 0 1 0 542298651 21499904 4617 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5249 4617 603 41 0 5208 0
vsize: 20996
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 4933 0 0 0 22984 15 0 0 25 0 1 0 542298651 22441984 4850 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5479 4850 603 41 0 5438 0
vsize: 21916
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 5161 0 0 0 23984 16 0 0 25 0 1 0 542298651 23388160 5078 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5710 5078 603 41 0 5669 0
vsize: 22840
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 5487 0 0 0 24983 17 0 0 25 0 1 0 542298651 24727552 5404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6037 5404 603 41 0 5996 0
vsize: 24148
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 5764 0 0 0 25983 18 0 0 25 0 1 0 542298651 25800704 5681 4294967295 134512640 134672761 3221224544 3221223648 134559808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6299 5681 603 41 0 6258 0
vsize: 25196
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 6185 0 0 0 26982 18 0 0 25 0 1 0 542298651 27529216 6102 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6721 6102 603 41 0 6680 0
vsize: 26884
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 6589 0 0 0 27981 20 0 0 25 0 1 0 542298651 29143040 6506 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7115 6506 603 41 0 7074 0
vsize: 28460
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 6847 0 0 0 28979 22 0 0 25 0 1 0 542298651 30203904 6764 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7374 6764 603 41 0 7333 0
vsize: 29496
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 7094 0 0 0 29979 22 0 0 25 0 1 0 542298651 31277056 7011 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7636 7011 603 41 0 7595 0
vsize: 30544
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 7406 0 0 0 30978 23 0 0 25 0 1 0 542298651 32485376 7323 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7931 7323 603 41 0 7890 0
vsize: 31724
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 7737 0 0 0 31977 24 0 0 25 0 1 0 542298651 34091008 7654 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8323 7654 603 41 0 8282 0
vsize: 33292
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 8015 0 0 0 32976 25 0 0 25 0 1 0 542298651 35303424 7932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8619 7932 603 41 0 8578 0
vsize: 34476
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 8360 0 0 0 33976 26 0 0 25 0 1 0 542298651 36646912 8277 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8947 8277 603 41 0 8906 0
vsize: 35788
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 8721 0 0 0 34974 28 0 0 25 0 1 0 542298651 38121472 8638 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9307 8638 603 41 0 9266 0
vsize: 37228
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 9084 0 0 0 35973 29 0 0 25 0 1 0 542298651 39591936 9001 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9666 9001 603 41 0 9625 0
vsize: 38664
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 9419 0 0 0 36973 29 0 0 25 0 1 0 542298651 40931328 9336 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9993 9336 603 41 0 9952 0
vsize: 39972
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 9704 0 0 0 37972 30 0 0 25 0 1 0 542298651 42143744 9621 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10289 9621 603 41 0 10248 0
vsize: 41156
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 10175 0 0 0 38972 31 0 0 25 0 1 0 542298651 44011520 10092 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10745 10092 603 41 0 10704 0
vsize: 42980
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 10527 0 0 0 39971 32 0 0 25 0 1 0 542298651 45486080 10444 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11105 10444 603 41 0 11064 0
vsize: 44420
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 10750 0 0 0 40970 32 0 0 25 0 1 0 542298651 46424064 10667 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 10667 603 41 0 11293 0
vsize: 45336
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 11037 0 0 0 41969 33 0 0 25 0 1 0 542298651 47632384 10954 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11629 10954 603 41 0 11588 0
vsize: 46516
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 11393 0 0 0 42969 34 0 0 25 0 1 0 542298651 48967680 11310 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11955 11310 603 41 0 11914 0
vsize: 47820
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 11685 0 0 0 43969 35 0 0 25 0 1 0 542298651 50176000 11602 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12250 11602 603 41 0 12209 0
vsize: 49000
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 12031 0 0 0 44968 35 0 0 25 0 1 0 542298651 51646464 11948 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12609 11948 603 41 0 12568 0
vsize: 50436
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 12369 0 0 0 45967 36 0 0 25 0 1 0 542298651 52981760 12286 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12935 12286 603 41 0 12894 0
vsize: 51740
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 12755 0 0 0 46967 37 0 0 25 0 1 0 542298651 54579200 12672 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13325 12672 603 41 0 13284 0
vsize: 53300
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 13083 0 0 0 47966 38 0 0 25 0 1 0 542298651 55922688 13000 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13653 13000 603 41 0 13612 0
vsize: 54612
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 13435 0 0 0 48965 39 0 0 25 0 1 0 542298651 57401344 13352 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14014 13352 603 41 0 13973 0
vsize: 56056
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 13812 0 0 0 49965 40 0 0 25 0 1 0 542298651 58863616 13729 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14371 13729 603 41 0 14330 0
vsize: 57484
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 14075 0 0 0 50964 41 0 0 25 0 1 0 542298651 59940864 13992 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14634 13992 603 41 0 14593 0
vsize: 58536
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 14394 0 0 0 51963 41 0 0 25 0 1 0 542298651 61288448 14311 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14963 14311 603 41 0 14922 0
vsize: 59852
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 14676 0 0 0 52963 42 0 0 25 0 1 0 542298651 62459904 14593 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15249 14593 603 41 0 15208 0
vsize: 60996
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 14963 0 0 0 53962 43 0 0 25 0 1 0 542298651 63668224 14880 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15544 14880 603 41 0 15503 0
vsize: 62176
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 15278 0 0 0 54962 44 0 0 25 0 1 0 542298651 64868352 15195 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15837 15195 603 41 0 15796 0
vsize: 63348
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 15540 0 0 0 55961 44 0 0 25 0 1 0 542298651 65937408 15457 4294967295 134512640 134672761 3221224544 3221223616 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16098 15457 603 41 0 16057 0
vsize: 64392
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 15789 0 0 0 56960 45 0 0 25 0 1 0 542298651 67014656 15706 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16361 15706 603 41 0 16320 0
vsize: 65444
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 16171 0 0 0 57960 46 0 0 25 0 1 0 542298651 68489216 16088 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16721 16088 603 41 0 16680 0
vsize: 66884
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 16500 0 0 0 58959 47 0 0 25 0 1 0 542298651 69832704 16417 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17049 16417 603 41 0 17008 0
vsize: 68196
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 16931 0 0 0 59958 48 0 0 25 0 1 0 542298651 71696384 16848 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17504 16848 603 41 0 17463 0
vsize: 70016
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 17291 0 0 0 60958 48 0 0 25 0 1 0 542298651 73043968 17208 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17833 17208 603 41 0 17792 0
vsize: 71332
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 17564 0 0 0 61957 49 0 0 25 0 1 0 542298651 74235904 17481 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18124 17481 603 41 0 18083 0
vsize: 72496
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18275 0 0 0 62955 51 0 0 25 0 1 0 542298651 76607488 18192 4294967295 134512640 134672761 3221224544 3221223712 134561164 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 63956 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134561115 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.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 64956 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223716 134556639 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 65956 51 0 0 25 0 1 0 542298651 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+670.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 66956 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 67956 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560858 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 68956 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134561382 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.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 69956 51 0 0 25 0 1 0 542298651 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+710.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 70957 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134561188 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 71957 51 0 0 25 0 1 0 542298651 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+730.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 72957 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 73957 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560839 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 74957 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223668 134566037 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.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 75958 51 0 0 25 0 1 0 542298651 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+770.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 76958 51 0 0 25 0 1 0 542298651 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.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 77958 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560912 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.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 78958 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 79958 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 80959 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223616 134553549 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.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 81959 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 82959 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134561001 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.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 83959 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223648 134560174 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.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 84959 51 0 0 25 0 1 0 542298651 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+860.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 85960 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 86960 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560876 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.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 87960 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560867 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.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 88960 51 0 0 25 0 1 0 542298651 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+900.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 89960 51 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 28717
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 90962 51 0 0 25 0 1 0 542298651 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+920.067 s]
Raw data (loadavg): 1.07 0.99 0.94 3/57 28761
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 91964 52 0 0 25 0 1 0 542298651 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+930.067 s]
Raw data (loadavg): 1.06 0.99 0.94 2/54 28770
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 92958 58 0 0 25 0 1 0 542298651 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+940.067 s]
Raw data (loadavg): 1.05 0.99 0.94 2/54 28770
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18305 0 0 0 93958 58 0 0 25 0 1 0 542298651 76771328 18222 4294967295 134512640 134672761 3221224544 3221223728 134559340 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.067 s]
Raw data (loadavg): 1.04 0.99 0.94 2/54 28770
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18425 0 0 0 94957 58 0 0 25 0 1 0 542298651 77295616 18342 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18871 18342 603 41 0 18830 0
vsize: 75484
[startup+960.068 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 28770
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18747 0 0 0 95957 59 0 0 25 0 1 0 542298651 78622720 18664 4294967295 134512640 134672761 3221224544 3221223648 134560293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19195 18664 603 41 0 19154 0
vsize: 76780
[startup+970.068 s]
Raw data (loadavg): 1.03 0.99 0.94 2/54 28770
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 18982 0 0 0 96957 60 0 0 25 0 1 0 542298651 79560704 18899 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.067 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 28770
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 19196 0 0 0 97956 60 0 0 25 0 1 0 542298651 80490496 19113 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19651 19113 603 41 0 19610 0
vsize: 78604
[startup+990.068 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 19454 0 0 0 98955 62 0 0 25 0 1 0 542298651 81420288 19371 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19878 19371 603 41 0 19837 0
vsize: 79512
[startup+1000.07 s]
Raw data (loadavg): 1.02 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 19756 0 0 0 99954 63 0 0 25 0 1 0 542298651 82751488 19673 4294967295 134512640 134672761 3221224544 3221223728 134559601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20203 19673 603 41 0 20162 0
vsize: 80812
[startup+1010.07 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 20088 0 0 0 100953 64 0 0 25 0 1 0 542298651 84066304 20005 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20524 20005 603 41 0 20483 0
vsize: 82096
[startup+1020.07 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 20357 0 0 0 101953 64 0 0 25 0 1 0 542298651 85135360 20274 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20785 20274 603 41 0 20744 0
vsize: 83140
[startup+1030.07 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 20609 0 0 0 102952 65 0 0 25 0 1 0 542298651 86224896 20526 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21051 20526 603 41 0 21010 0
vsize: 84204
[startup+1040.07 s]
Raw data (loadavg): 1.01 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 20877 0 0 0 103952 66 0 0 25 0 1 0 542298651 87289856 20794 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21311 20794 603 41 0 21270 0
vsize: 85244
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 21220 0 0 0 104951 67 0 0 25 0 1 0 542298651 88760320 21137 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21670 21137 603 41 0 21629 0
vsize: 86680
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 21544 0 0 0 105951 67 0 0 25 0 1 0 542298651 90103808 21461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21998 21461 603 41 0 21957 0
vsize: 87992
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 21901 0 0 0 106950 68 0 0 25 0 1 0 542298651 91578368 21818 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22358 21818 603 41 0 22317 0
vsize: 89432
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 22164 0 0 0 107950 68 0 0 25 0 1 0 542298651 92651520 22081 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22620 22081 603 41 0 22579 0
vsize: 90480
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 22403 0 0 0 108950 69 0 0 25 0 1 0 542298651 93589504 22320 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22849 22320 603 41 0 22808 0
vsize: 91396
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 22663 0 0 0 109950 69 0 0 25 0 1 0 542298651 94662656 22580 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23111 22580 603 41 0 23070 0
vsize: 92444
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 22946 0 0 0 110949 70 0 0 25 0 1 0 542298651 95748096 22863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23376 22863 603 41 0 23335 0
vsize: 93504
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 23236 0 0 0 111948 71 0 0 25 0 1 0 542298651 96960512 23153 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23672 23153 603 41 0 23631 0
vsize: 94688
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 23484 0 0 0 112947 72 0 0 25 0 1 0 542298651 98033664 23401 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23934 23401 603 41 0 23893 0
vsize: 95736
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 23807 0 0 0 113946 73 0 0 25 0 1 0 542298651 99373056 23724 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24261 23724 603 41 0 24220 0
vsize: 97044
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 24046 0 0 0 114945 74 0 0 25 0 1 0 542298651 100306944 23963 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24489 23963 603 41 0 24448 0
vsize: 97956
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 24418 0 0 0 115945 75 0 0 25 0 1 0 542298651 101896192 24335 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24877 24335 603 41 0 24836 0
vsize: 99508
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 24754 0 0 0 116944 76 0 0 25 0 1 0 542298651 103235584 24671 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25204 24671 603 41 0 25163 0
vsize: 100816
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 25010 0 0 0 117944 76 0 0 25 0 1 0 542298651 104296448 24927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25463 24927 603 41 0 25422 0
vsize: 101852
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 25294 0 0 0 118943 77 0 0 25 0 1 0 542298651 105476096 25211 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25751 25211 603 41 0 25710 0
vsize: 103004
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.94 2/54 28772
Raw data (stat): 28717 (minisat+) R 28716 27565 27564 0 -1 0 25569 0 0 0 119943 78 0 0 25 0 1 0 542298651 106541056 25486 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26011 25486 603 41 0 25970 0
vsize: 104044
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.94 1/54 28772
Raw data (stat): 28717 (minisat+) Z 28716 27565 27564 0 -1 12 25572 0 0 0 119943 82 0 0 25 0 1 0 542298651 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.13
CPU time (s): 1200.26
CPU user time (s): 1199.43
CPU system time (s): 0.828873
CPU usage (%): 100.011
Max. virtual memory (Kb): 104044
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####