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/miplib3/normalized-mps-v2-13-7-10teams.opb
MD5SUM	130bea0863cb3f92addf09aabe15daa3
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	912
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.97
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 18375

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 14:36:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18145 boxname=wulflinc28 idbench=1396 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  130bea0863cb3f92addf09aabe15daa3  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-10teams.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-10teams.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-10teams.opb
IDLAUNCH: 18145
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        521392 kB
Buffers:         32080 kB
Cached:         454084 kB
SwapCached:        104 kB
Active:         193168 kB
Inactive:       295408 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        521140 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            19020 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:56:10 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 18145 7 1200.3 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 ---[ 328]---> Adder-cost: 76   maxlim: 39   bits: 6/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 ---[ 306]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 304]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 302]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 300]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 298]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 296]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 294]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 292]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 290]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 288]---> Adder-cost: 76   maxlim: 39   bits: 6/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 ---[ 268]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 266]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 264]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 262]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 260]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 258]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 256]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 254]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 252]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 250]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 249]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 248]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 247]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 246]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 245]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 244]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 243]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 242]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 241]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 240]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 239]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 238]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 237]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 236]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 235]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 234]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 233]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 232]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 231]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 230]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 229]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 228]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 227]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 226]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 225]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 224]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 223]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 222]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 221]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 220]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 219]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 218]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 217]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 216]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 215]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 214]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 213]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 212]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 211]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 210]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 209]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 208]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 207]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 206]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 205]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 204]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 203]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 202]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 201]---> Adder-cost: 126   maxlim: 61   bits: 7/6
c ---[ 200]---> Adder-cost: 126   maxlim: 62   bits: 7/6
c ---[ 199]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 198]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 197]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 196]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 195]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 194]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 193]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 192]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 191]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 190]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 189]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 188]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 187]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 186]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 185]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 184]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 183]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 182]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 181]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 180]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 179]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 178]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 177]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 176]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 175]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 174]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 173]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 172]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 171]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 170]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 169]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 168]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 167]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 166]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 165]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 164]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 163]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 162]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 161]---> Adder-cost: 64   maxlim: 38   bits: 6/6
c ---[ 160]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 158]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 156]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 154]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 152]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 150]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 148]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 146]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 144]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 142]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 140]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 138]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 136]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 134]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 132]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 130]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 128]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 126]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 124]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 122]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 120]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 118]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 116]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 114]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 112]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 110]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 108]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 106]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[ 104]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 102]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[ 100]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[  98]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  96]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  94]---> Adder-cost: 64   maxlim: 39   bits: 6/6
c ---[  92]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  90]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  88]---> Adder-cost: 64   maxlim: 39   bits: 6/6
c ---[  86]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  84]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  82]---> Adder-cost: 64   maxlim: 39   bits: 6/6
c ---[  80]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  78]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  76]---> Adder-cost: 60   maxlim: 39   bits: 6/6
c ---[  74]---> Adder-cost: 64   maxlim: 39   bits: 6/6
c ---[  72]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  70]---> Adder-cost: 60   maxlim: 39   bits: 6/6
c ---[  68]---> Adder-cost: 64   maxlim: 39   bits: 6/6
c ---[  66]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  64]---> Adder-cost: 60   maxlim: 39   bits: 6/6
c ---[  62]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  60]---> Adder-cost: 60   maxlim: 39   bits: 6/6
c ---[  58]---> Adder-cost: 64   maxlim: 39   bits: 6/6
c ---[  56]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  54]---> Adder-cost: 60   maxlim: 39   bits: 6/6
c ---[  52]---> Adder-cost: 64   maxlim: 39   bits: 6/6
c ---[  50]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  48]---> Adder-cost: 60   maxlim: 39   bits: 6/6
c ---[  46]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  44]---> Adder-cost: 60   maxlim: 39   bits: 6/6
c ---[  42]---> Adder-cost: 64   maxlim: 39   bits: 6/6
c ---[  40]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  38]---> Adder-cost: 60   maxlim: 39   bits: 6/6
c ---[  36]---> Adder-cost: 64   maxlim: 39   bits: 6/6
c ---[  34]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  32]---> Adder-cost: 60   maxlim: 39   bits: 6/6
c ---[  30]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  28]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  26]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[  24]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  22]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  20]---> Adder-cost: 72   maxlim: 39   bits: 6/6
c ---[  18]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  16]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  14]---> Adder-cost: 60   maxlim: 39   bits: 6/6
c ---[  12]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[  10]---> Adder-cost: 64   maxlim: 39   bits: 6/6
c ---[   8]---> Adder-cost: 60   maxlim: 39   bits: 6/6
c ---[   6]---> Adder-cost: 68   maxlim: 39   bits: 6/6
c ---[   4]---> Adder-cost: 64   maxlim: 39   bits: 6/6
c ---[   2]---> Adder-cost: 60   maxlim: 39   bits: 6/6
c ---[   0]---> Adder-cost: 68   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 |  110489   391599 |   41110       8       16     2.0 | 12.848 % |
c |       250 |  108505   384593 |   45221      34       69     2.0 | 14.606 % |
c |       475 |  107560   381295 |   49743     171      413     2.4 | 15.369 % |
c |       812 |  106622   378090 |   54717     382     1045     2.7 | 16.102 % |
c |      1318 |  105473   374178 |   60189     725     2746     3.8 | 16.999 % |
c |      2080 |  104512   370886 |   66208    1360     6376     4.7 | 17.801 % |
c |      3219 |  103523   367444 |   72829    2345    18869     8.0 | 18.554 % |
c |      4927 |  101713   361198 |   80112    3781    43889    11.6 | 20.030 % |
c |      7489 |   99249   352764 |   88123    5986    84771    14.2 | 22.055 % |
c |     11336 |   94435   336069 |   96935    9149   153118    16.7 | 25.973 % |
c |     17102 |   89148   317933 |  106629   14101   324409    23.0 | 30.253 % |
c |     25752 |   83391   298231 |  117292   21801   555265    25.5 | 35.082 % |
c |     38727 |   77351   277487 |  129021   33918  1017102    30.0 | 40.144 % |
c |     58188 |   73086   262880 |  141923   52673  2141651    40.7 | 43.814 % |
c ==============================================================================
c [1mFound solution: 1048[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 7748   maxlim: 38952   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75975 |  124980   448608 |   41660   70075  4329451    61.8 | 43.814 % |
c |     76076 |  124950   448509 |   45826   32240  1808782    56.1 | 33.103 % |
c |     76226 |  124950   448509 |   50408   32390  1830640    56.5 | 33.103 % |
c |     76451 |  124909   448376 |   55449   32610  1844540    56.6 | 33.132 % |
c |     76788 |  124833   448116 |   60994   32936  1872958    56.9 | 33.178 % |
c |     77294 |  124833   448116 |   67093   33442  1950376    58.3 | 33.178 % |
c |     78054 |  124717   447723 |   73803   34183  2013095    58.9 | 33.246 % |
c |     79193 |  124571   447225 |   81183   35306  2160952    61.2 | 33.339 % |
c |     80901 |  124538   447116 |   89301   37008  2477722    67.0 | 33.357 % |
c |     83463 |  124221   446067 |   98232   39519  2838723    71.8 | 33.554 % |
c |     87309 |  123898   444957 |  108055   43322  3448877    79.6 | 33.758 % |
c |     93075 |  123598   443944 |  118860   49038  4620799    94.2 | 33.941 % |
c |    101725 |  123205   442620 |  130746   57625  6426931   111.5 | 34.177 % |
c ==============================================================================
c [1mFound solution: 1000[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39000   bits: 16/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107321 |  122864   441499 |   40954   63171  7793269   123.4 | 34.177 % |
c |    107422 |  122864   441499 |   45049   31687  2420424    76.4 | 34.407 % |
c |    107572 |  122864   441499 |   49554   31837  2456443    77.2 | 34.407 % |
c |    107797 |  122816   441335 |   54509   32054  2473366    77.2 | 34.425 % |
c |    108134 |  122816   441335 |   59960   32391  2532139    78.2 | 34.425 % |
c |    108641 |  122791   441254 |   65956   32894  2591264    78.8 | 34.443 % |
c |    109400 |  122782   441225 |   72552   33652  2761302    82.1 | 34.450 % |
c |    110541 |  122705   440966 |   79807   34781  2916305    83.8 | 34.496 % |
c |    112252 |  122613   440640 |   87788   36480  3189853    87.4 | 34.553 % |
c |    114814 |  122588   440557 |   96567   39035  3824583    98.0 | 34.564 % |
c |    118658 |  122338   439727 |  106224   42834  4554621   106.3 | 34.718 % |
c |    124425 |  122076   438836 |  116846   48559  5628272   115.9 | 34.872 % |
c |    133075 |  121433   436670 |  128531   57109  7340725   128.5 | 35.240 % |
c |    146052 |  121038   435340 |  141384   70021 10501290   150.0 | 35.469 % |
c |    165516 |  120523   433634 |  155522   89389 15951703   178.5 | 35.777 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x10212_bit0 -x10312_bit0 -x20312_bit0 x10412_bit0 -x20412_bit0 -x30412_bit0 -x10512_bit0 -x20512_bit0 -x30512_bit0 -x40512_bit0 -x10612_bit0 -x20612_bit0 -x30612_bit0 -x40612_bit0 -x50612_bit0 -x10712_bit0 -x20712_bit0 -x30712_bit0 -x40712_bit0 -x50712_bit0 -x60712_bit0 -x10812_bit0 -x20812_bit0 -x30812_bit0 -x40812_bit0 -x50812_bit0 -x60812_bit0 -x70812_bit0 -x10912_bit0 -x20912_bit0 -x30912_bit0 -x40912_bit0 -x50912_bit0 -x60912_bit0 -x70912_bit0 -x80912_bit0 -x11012_bit0 -x21012_bit0 -x31012_bit0 -x41012_bit0 -x51012_bit0 -x61012_bit0 -x71012_bit0 -x81012_bit0 -x91012_bit0 -x10222_bit0 -x10322_bit0 -x20322_bit0 -x10422_bit0 -x20422_bit0 -x30422_bit0 -x10522_bit0 -x20522_bit0 -x30522_bit0 -x40522_bit0 -x10622_bit0 -x20622_bit0 -x30622_bit0 -x40622_bit0 -x50622_bit0 -x10722_bit0 -x20722_bit0 -x30722_bit0 -x40722_bit0 -x50722_bit0 -x60722_bit0 -x10822_bit0 -x20822_bit0 -x30822_bit0 -x40822_bit0 -x50822_bit0 -x60822_bit0 -x70822_bit0 -x10922_bit0 -x20922_bit0 -x30922_bit0 -x40922_bit0 -x50922_bit0 -x60922_bit0 x70922_bit0 -x80922_bit0 -x11022_bit0 -x21022_bit0 -x31022_bit0 -x41022_bit0 -x51022_bit0 -x61022_bit0 -x71022_bit0 -x81022_bit0 -x91022_bit0 -x10232_bit0 -x10332_bit0 -x20332_bit0 -x10432_bit0 -x20432_bit0 -x30432_bit0 -x10532_bit0 -x20532_bit0 -x30532_bit0 -x40532_bit0 -x10632_bit0 -x20632_bit0 -x30632_bit0 -x40632_bit0 -x50632_bit0 -x10732_bit0 -x20732_bit0 -x30732_bit0 -x40732_bit0 -x50732_bit0 -x60732_bit0 -x10832_bit0 -x20832_bit0 -x30832_bit0 -x40832_bit0 -x50832_bit0 -x60832_bit0 -x70832_bit0 -x10932_bit0 -x20932_bit0 -x30932_bit0 -x40932_bit0 -x50932_bit0 -x60932_bit0 -x70932_bit0 -x80932_bit0 -x11032_bit0 -x21032_bit0 -x31032_bit0 -x41032_bit0 -x51032_bit0 -x61032_bit0 -x71032_bit0 x81032_bit0 -x91032_bit0 -x10242_bit0 -x10342_bit0 -x20342_bit0 -x10442_bit0 -x20442_bit0 -x30442_bit0 -x10542_bit0 x20542_bit0 -x30542_bit0 -x40542_bit0 -x10642_bit0 -x20642_bit0 -x30642_bit0 -x40642_bit0 -x50642_bit0 -x10742_bit0 -x20742_bit0 -x30742_bit0 -x40742_bit0 -x50742_bit0 -x60742_bit0 -x10842_bit0 -x20842_bit0 -x30842_bit0 -x40842_bit0 -x50842_bit0 -x60842_bit0 -x70842_bit0 -x10942_bit0 -x20942_bit0 -x30942_bit0 -x40942_bit0 -x50942_bit0 -x60942_bit0 -x70942_bit0 -x80942_bit0 -x11042_bit0 -x21042_bit0 -x31042_bit0 -x41042_bit0 -x51042_bit0 -x61042_bit0 -x71042_bit0 -x81042_bit0 -x91042_bit0 -x10252_bit0 -x10352_bit0 -x20352_bit0 -x10452_bit0 -x20452_bit0 -x30452_bit0 -x10552_bit0 -x20552_bit0 -x30552_bit0 -x40552_bit0 -x10652_bit0 -x20652_bit0 x30652_bit0 -x40652_bit0 -x50652_bit0 -x10752_bit0 -x20752_bit0 -x30752_bit0 -x40752_bit0 -x50752_bit0 -x60752_bit0 -x10852_bit0 -x20852_bit0 -x30852_bit0 -x40852_bit0 -x50852_bit0 -x60852_bit0 -x70852_bit0 -x10952_bit0 -x20952_bit0 -x30952_bit0 -x40952_bit0 -x50952_bit0 -x60952_bit0 -x70952_bit0 -x80952_bit0 -x11052_bit0 -x21052_bit0 -x31052_bit0 -x41052_bit0 -x51052_bit0 -x61052_bit0 -x71052_bit0 -x81052_bit0 -x91052_bit0 -x10213_bit0 -x10313_bit0 -x20313_bit0 -x10413_bit0 -x20413_bit0 -x30413_bit0 -x10513_bit0 -x20513_bit0 -x30513_bit0 -x40513_bit0 -x10613_bit0 -x20613_bit0 -x30613_bit0 -x40613_bit0 -x50613_bit0 -x10713_bit0 -x20713_bit0 -x30713_bit0 -x40713_bit0 -x50713_bit0 x60713_bit0 -x10813_bit0 -x20813_bit0 -x30813_bit0 -x40813_bit0 -x50813_bit0 -x60813_bit0 -x70813_bit0 -x10913_bit0 -x20913_bit0 -x30913_bit0 -x40913_bit0 -x50913_bit0 -x60913_bit0 -x70913_bit0 -x80913_bit0 -x11013_bit0 -x21013_bit0 -x31013_bit0 -x41013_bit0 -x51013_bit0 -x61013_bit0 -x71013_bit0 -x81013_bit0 -x91013_bit0 -x10223_bit0 -x10323_bit0 -x20323_bit0 -x10423_bit0 -x20423_bit0 -x30423_bit0 -x10523_bit0 -x20523_bit0 -x30523_bit0 -x40523_bit0 -x10623_bit0 -x20623_bit0 -x30623_bit0 -x40623_bit0 -x50623_bit0 -x10723_bit0 -x20723_bit0 -x30723_bit0 -x40723_bit0 -x50723_bit0 -x60723_bit0 -x10823_bit0 x20823_bit0 -x30823_bit0 -x40823_bit0 -x50823_bit0 -x60823_bit0 -x70823_bit0 -x10923_bit0 -x20923_bit0 -x30923_bit0 -x40923_bit0 -x50923_bit0 -x60923_bit0 -x70923_bit0 -x80923_bit0 -x11023_bit0 -x21023_bit0 -x31023_bit0 -x41023_bit0 -x51023_bit0 -x61023_bit0 -x71023_bit0 -x81023_bit0 -x91023_bit0 -x10233_bit0 -x10333_bit0 -x20333_bit0 -x10433_bit0 -x20433_bit0 -x30433_bit0 -x10533_bit0 -x20533_bit0 -x30533_bit0 -x40533_bit0 -x10633_bit0 -x20633_bit0 -x30633_bit0 -x40633_bit0 -x50633_bit0 -x10733_bit0 -x20733_bit0 -x30733_bit0 -x40733_bit0 -x50733_bit0 -x60733_bit0 -x10833_bit0 -x20833_bit0 -x30833_bit0 -x40833_bit0 -x50833_bit0 -x60833_bit0 -x70833_bit0 x10933_bit0 -x20933_bit0 -x30933_bit0 -x40933_bit0 -x50933_bit0 -x60933_bit0 -x70933_bit0 -x80933_bit0 -x11033_bit0 -x21033_bit0 -x31033_bit0 -x41033_bit0 -x51033_bit0 -x61033_bit0 -x71033_bit0 -x81033_bit0 -x91033_bit0 -x10243_bit0 -x10343_bit0 -x20343_bit0 -x10443_bit0 -x20443_bit0 -x30443_bit0 -x10543_bit0 -x20543_bit0 -x30543_bit0 -x40543_bit0 -x10643_bit0 -x20643_bit0 -x30643_bit0 -x40643_bit0 -x50643_bit0 -x10743_bit0 -x20743_bit0 -x30743_bit0 -x40743_bit0 -x50743_bit0 -x60743_bit0 -x10843_bit0 -x20843_bit0 -x30843_bit0 -x40843_bit0 -x50843_bit0 -x60843_bit0 -x70843_bit0 -x10943_bit0 -x20943_bit0 -x30943_bit0 -x40943_bit0 -x50943_bit0 -x60943_bit0 -x70943_bit0 -x80943_bit0 -x11043_bit0 -x21043_bit0 x31043_bit0 -x41043_bit0 -x51043_bit0 -x61043_bit0 -x71043_bit0 -x81043_bit0 -x91043_bit0 -x10253_bit0 -x10353_bit0 -x20353_bit0 -x10453_bit0 -x20453_bit0 -x30453_bit0 -x10553_bit0 -x20553_bit0 -x30553_bit0 x40553_bit0 -x10653_bit0 -x20653_bit0 -x30653_bit0 -x40653_bit0 -x50653_bit0 -x10753_bit0 -x20753_bit0 -x30753_bit0 -x40753_bit0 -x50753_bit0 -x60753_bit0 -x10853_bit0 -x20853_bit0 -x30853_bit0 -x40853_bit0 -x50853_bit0 -x60853_bit0 -x70853_bit0 -x10953_bit0 -x20953_bit0 -x30953_bit0 -x40953_bit0 -x50953_bit0 -x60953_bit0 -x70953_bit0 -x80953_bit0 -x11053_bit0 -x21053_bit0 -x31053_bit0 -x41053_bit0 -x51053_bit0 -x61053_bit0 -x71053_bit0 -x81053_bit0 -x91053_bit0 -x10214_bit0 -x10314_bit0 -x20314_bit0 -x10414_bit0 -x20414_bit0 -x30414_bit0 -x10514_bit0 -x20514_bit0 -x30514_bit0 -x40514_bit0 -x10614_bit0 -x20614_bit0 -x30614_bit0 -x40614_bit0 -x50614_bit0 -x10714_bit0 -x20714_bit0 -x30714_bit0 -x40714_bit0 -x50714_bit0 -x60714_bit0 -x10814_bit0 -x20814_bit0 -x30814_bit0 -x40814_bit0 -x50814_bit0 -x60814_bit0 -x70814_bit0 -x10914_bit0 -x20914_bit0 -x30914_bit0 -x40914_bit0 -x50914_bit0 -x60914_bit0 -x70914_bit0 -x80914_bit0 -x11014_bit0 -x21014_bit0 -x31014_bit0 x41014_bit0 -x51014_bit0 -x61014_bit0 -x71014_bit0 -x81014_bit0 -x91014_bit0 -x10224_bit0 -x10324_bit0 -x20324_bit0 -x10424_bit0 -x20424_bit0 -x30424_bit0 -x10524_bit0 -x20524_bit0 -x30524_bit0 -x40524_bit0 x10624_bit0 -x20624_bit0 -x30624_bit0 -x40624_bit0 -x50624_bit0 -x10724_bit0 -x20724_bit0 -x30724_bit0 -x40724_bit0 -x50724_bit0 -x60724_bit0 -x10824_bit0 -x20824_bit0 -x30824_bit0 -x40824_bit0 -x50824_bit0 -x60824_bit0 -x70824_bit0 -x10924_bit0 -x20924_bit0 -x30924_bit0 -x40924_bit0 -x50924_bit0 -x60924_bit0 -x70924_bit0 -x80924_bit0 -x11024_bit0 -x21024_bit0 -x31024_bit0 -x41024_bit0 -x51024_bit0 -x61024_bit0 -x71024_bit0 -x81024_bit0 -x91024_bit0 -x10234_bit0 -x10334_bit0 -x20334_bit0 -x10434_bit0 -x20434_bit0 -x30434_bit0 -x10534_bit0 -x20534_bit0 -x30534_bit0 -x40534_bit0 -x10634_bit0 -x20634_bit0 -x30634_bit0 -x40634_bit0 -x50634_bit0 -x10734_bit0 -x20734_bit0 -x30734_bit0 -x40734_bit0 -x50734_bit0 -x60734_bit0 -x10834_bit0 -x20834_bit0 -x30834_bit0 -x40834_bit0 x50834_bit0 -x60834_bit0 -x70834_bit0 -x10934_bit0 -x20934_bit0 -x30934_bit0 -x40934_bit0 -x50934_bit0 -x60934_bit0 -x70934_bit0 -x80934_bit0 -x11034_bit0 -x21034_bit0 -x31034_bit0 -x41034_bit0 -x51034_bit0 -x61034_bit0 -x71034_bit0 -x81034_bit0 -x91034_bit0 -x10244_bit0 -x10344_bit0 -x20344_bit0 -x10444_bit0 -x20444_bit0 -x30444_bit0 -x10544_bit0 -x20544_bit0 -x30544_bit0 -x40544_bit0 -x10644_bit0 -x20644_bit0 -x30644_bit0 -x40644_bit0 -x50644_bit0 -x10744_bit0 -x20744_bit0 -x30744_bit0 -x40744_bit0 -x50744_bit0 -x60744_bit0 -x10844_bit0 -x20844_bit0 -x30844_bit0 -x40844_bit0 -x50844_bit0 -x60844_bit0 -x70844_bit0 -x10944_bit0 -x20944_bit0 x30944_bit0 -x40944_bit0 -x50944_bit0 -x60944_bit0 -x70944_bit0 -x80944_bit0 -x11044_bit0 -x21044_bit0 -x31044_bit0 -x41044_bit0 -x51044_bit0 -x61044_bit0 -x71044_bit0 -x81044_bit0 -x91044_bit0 -x10254_bit0 -x10354_bit0 -x20354_bit0 -x10454_bit0 -x20454_bit0 -x30454_bit0 -x10554_bit0 -x20554_bit0 -x30554_bit0 -x40554_bit0 -x10654_bit0 -x20654_bit0 -x30654_bit0 -x40654_bit0 -x50654_bit0 -x10754_bit0 x20754_bit0 -x30754_bit0 -x40754_bit0 -x50754_bit0 -x60754_bit0 -x10854_bit0 -x20854_bit0 -x30854_bit0 -x40854_bit0 -x50854_bit0 -x60854_bit0 -x70854_bit0 -x10954_bit0 -x20954_bit0 -x30954_bit0 -x40954_bit0 -x50954_bit0 -x60954_bit0 -x70954_bit0 -x80954_bit0 -x11054_bit0 -x21054_bit0 -x31054_bit0 -x41054_bit0 -x51054_bit0 -x61054_bit0 -x71054_bit0 -x81054_bit0 -x91054_bit0 -x10215_bit0 -x10315_bit0 -x20315_bit0 -x10415_bit0 -x20415_bit0 -x30415_bit0 -x10515_bit0 -x20515_bit0 -x30515_bit0 -x40515_bit0 -x10615_bit0 -x20615_bit0 -x30615_bit0 -x40615_bit0 -x50615_bit0 -x10715_bit0 -x20715_bit0 -x30715_bit0 -x40715_bit0 x50715_bit0 -x60715_bit0 -x10815_bit0 -x20815_bit0 -x30815_bit0 -x40815_bit0 -x50815_bit0 -x60815_bit0 -x70815_bit0 -x10915_bit0 -x20915_bit0 -x30915_bit0 -x40915_bit0 -x50915_bit0 -x60915_bit0 -x70915_bit0 -x80915_bit0 -x11015_bit0 -x21015_bit0 -x31015_bit0 -x41015_bit0 -x51015_bit0 -x61015_bit0 -x71015_bit0 -x81015_bit0 -x91015_bit0 -x10225_bit0 -x10325_bit0 -x20325_bit0 -x10425_bit0 -x20425_bit0 -x30425_bit0 -x10525_bit0 -x20525_bit0 -x30525_bit0 -x40525_bit0 -x10625_bit0 -x20625_bit0 -x30625_bit0 -x40625_bit0 -x50625_bit0 -x10725_bit0 -x20725_bit0 -x30725_bit0 -x40725_bit0 -x50725_bit0 -x60725_bit0 -x10825_bit0 -x20825_bit0 x30825_bit0 -x40825_bit0 -x50825_bit0 -x60825_bit0 -x70825_bit0 -x10925_bit0 -x20925_bit0 -x30925_bit0 -x40925_bit0 -x50925_bit0 -x60925_bit0 -x70925_bit0 -x80925_bit0 -x11025_bit0 -x21025_bit0 -x31025_bit0 -x41025_bit0 -x51025_bit0 -x61025_bit0 -x71025_bit0 -x81025_bit0 -x91025_bit0 -x10235_bit0 -x10335_bit0 -x20335_bit0 -x10435_bit0 -x20435_bit0 -x30435_bit0 -x10535_bit0 -x20535_bit0 -x30535_bit0 -x40535_bit0 -x10635_bit0 -x20635_bit0 -x30635_bit0 -x40635_bit0 -x50635_bit0 -x10735_bit0 -x20735_bit0 -x30735_bit0 -x40735_bit0 -x50735_bit0 -x60735_bit0 -x10835_bit0 -x20835_bit0 -x30835_bit0 -x40835_bit0 -x50835_bit0 -x60835_bit0 -x70835_bit0 -x10935_bit0 -x20935_bit0 -x30935_bit0 -x40935_bit0 -x50935_bit0 -x60935_bit0 -x70935_bit0 -x80935_bit0 x11035_bit0 -x21035_bit0 -x31035_bit0 -x41035_bit0 -x51035_bit0 -x61035_bit0 -x71035_bit0 -x81035_bit0 -x91035_bit0 -x10245_bit0 -x10345_bit0 -x20345_bit0 -x10445_bit0 -x20445_bit0 -x30445_bit0 -x10545_bit0 -x20545_bit0 -x30545_bit0 -x40545_bit0 -x10645_bit0 -x20645_bit0 -x30645_bit0 x40645_bit0 -x50645_bit0 -x10745_bit0 -x20745_bit0 -x30745_bit0 -x40745_bit0 -x50745_bit0 -x60745_bit0 -x10845_bit0 -x20845_bit0 -x30845_bit0 -x40845_bit0 -x50845_bit0 -x60845_bit0 -x70845_bit0 -x10945_bit0 -x20945_bit0 -x30945_bit0 -x40945_bit0 -x50945_bit0 -x60945_bit0 -x70945_bit0 -x80945_bit0 -x11045_bit0 -x21045_bit0 -x31045_bit0 -x41045_bit0 -x51045_bit0 -x61045_bit0 -x71045_bit0 -x81045_bit0 -x91045_bit0 -x10255_bit0 -x10355_bit0 -x20355_bit0 -x10455_bit0 -x20455_bit0 -x30455_bit0 -x10555_bit0 -x20555_bit0 -x30555_bit0 -x40555_bit0 -x10655_bit0 -x20655_bit0 -x30655_bit0 -x40655_bit0 -x50655_bit0 -x10755_bit0 -x20755_bit0 -x30755_bit0 -x40755_bit0 -x50755_bit0 -x60755_bit0 -x10855_bit0 -x20855_bit0 -x30855_bit0 -x40855_bit0 -x50855_bit0 -x60855_bit0 -x70855_bit0 -x10955_bit0 x20955_bit0 -x30955_bit0 -x40955_bit0 -x50955_bit0 -x60955_bit0 -x70955_bit0 -x80955_bit0 -x11055_bit0 -x21055_bit0 -x31055_bit0 -x41055_bit0 -x51055_bit0 -x61055_bit0 -x71055_bit0 -x81055_bit0 -x91055_bit0 -x10216_bit0 -x10316_bit0 -x20316_bit0 -x10416_bit0 -x20416_bit0 -x30416_bit0 -x10516_bit0 -x20516_bit0 -x30516_bit0 -x40516_bit0 -x10616_bit0 -x20616_bit0 -x30616_bit0 -x40616_bit0 -x50616_bit0 -x10716_bit0 -x20716_bit0 -x30716_bit0 -x40716_bit0 -x50716_bit0 -x60716_bit0 -x10816_bit0 -x20816_bit0 -x30816_bit0 -x40816_bit0 -x50816_bit0 -x60816_bit0 -x70816_bit0 -x10916_bit0 -x20916_bit0 -x30916_bit0 -x40916_bit0 -x50916_bit0 x60916_bit0 -x70916_bit0 -x80916_bit0 -x11016_bit0 -x21016_bit0 -x31016_bit0 -x41016_bit0 -x51016_bit0 -x61016_bit0 -x71016_bit0 -x81016_bit0 -x91016_bit0 -x10226_bit0 -x10326_bit0 -x20326_bit0 -x10426_bit0 -x20426_bit0 -x30426_bit0 -x10526_bit0 -x20526_bit0 -x30526_bit0 -x40526_bit0 -x10626_bit0 -x20626_bit0 -x30626_bit0 -x40626_bit0 -x50626_bit0 -x10726_bit0 -x20726_bit0 -x30726_bit0 -x40726_bit0 -x50726_bit0 -x60726_bit0 -x10826_bit0 -x20826_bit0 -x30826_bit0 -x40826_bit0 -x50826_bit0 -x60826_bit0 -x70826_bit0 -x10926_bit0 -x20926_bit0 -x30926_bit0 -x40926_bit0 -x50926_bit0 -x60926_bit0 -x70926_bit0 -x80926_bit0 -x11026_bit0 -x21026_bit0 -x31026_bit0 -x41026_bit0 x51026_bit0 -x61026_bit0 -x71026_bit0 -x81026_bit0 -x91026_bit0 -x10236_bit0 -x10336_bit0 x20336_bit0 -x10436_bit0 -x20436_bit0 -x30436_bit0 -x10536_bit0 -x20536_bit0 -x30536_bit0 -x40536_bit0 -x10636_bit0 -x20636_bit0 -x30636_bit0 -x40636_bit0 -x50636_bit0 -x10736_bit0 -x20736_bit0 -x30736_bit0 -x40736_bit0 -x50736_bit0 -x60736_bit0 -x10836_bit0 -x20836_bit0 -x30836_bit0 -x40836_bit0 -x50836_bit0 -x60836_bit0 -x70836_bit0 -x10936_bit0 -x20936_bit0 -x30936_bit0 -x40936_bit0 -x50936_bit0 -x60936_bit0 -x70936_bit0 -x80936_bit0 -x11036_bit0 -x21036_bit0 -x31036_bit0 -x41036_bit0 -x51036_bit0 -x61036_bit0 -x71036_bit0 -x81036_bit0 -x91036_bit0 -x10246_bit0 -x10346_bit0 -x20346_bit0 -x10446_bit0 -x20446_bit0 -x30446_bit0 -x10546_bit0 -x20546_bit0 -x30546_bit0 -x40546_bit0 -x10646_bit0 -x20646_bit0 -x30646_bit0 -x40646_bit0 -x50646_bit0 x10746_bit0 -x20746_bit0 -x30746_bit0 -x40746_bit0 -x50746_bit0 -x60746_bit0 -x10846_bit0 -x20846_bit0 -x30846_bit0 -x40846_bit0 -x50846_bit0 -x60846_bit0 -x70846_bit0 -x10946_bit0 -x20946_bit0 -x30946_bit0 -x40946_bit0 -x50946_bit0 -x60946_bit0 -x70946_bit0 -x80946_bit0 -x11046_bit0 -x21046_bit0 -x31046_bit0 -x41046_bit0 -x51046_bit0 -x61046_bit0 -x71046_bit0 -x81046_bit0 -x91046_bit0 -x10256_bit0 -x10356_bit0 -x20356_bit0 -x10456_bit0 -x20456_bit0 -x30456_bit0 -x10556_bit0 -x20556_bit0 -x30556_bit0 -x40556_bit0 -x10656_bit0 -x20656_bit0 -x30656_bit0 -x40656_bit0 -x50656_bit0 -x10756_bit0 -x20756_bit0 -x30756_bit0 -x40756_bit0 -x50756_bit0 -x60756_bit0 -x10856_bit0 -x20856_bit0 -x30856_bit0 x40856_bit0 -x50856_bit0 -x60856_bit0 -x70856_bit0 -x10956_bit0 -x20956_bit0 -x30956_bit0 -x40956_bit0 -x50956_bit0 -x60956_bit0 -x70956_bit0 -x80956_bit0 -x11056_bit0 -x21056_bit0 -x31056_bit0 -x41056_bit0 -x51056_bit0 -x61056_bit0 -x71056_bit0 -x81056_bit0 -x91056_bit0 -x10217_bit0 -x10317_bit0 -x20317_bit0 -x10417_bit0 -x20417_bit0 -x30417_bit0 -x10517_bit0 -x20517_bit0 -x30517_bit0 -x40517_bit0 -x10617_bit0 -x20617_bit0 -x30617_bit0 -x40617_bit0 -x50617_bit0 -x10717_bit0 -x20717_bit0 -x30717_bit0 -x40717_bit0 -x50717_bit0 -x60717_bit0 -x10817_bit0 -x20817_bit0 -x30817_bit0 -x40817_bit0 -x50817_bit0 -x60817_bit0 -x70817_bit0 -x10917_bit0 -x20917_bit0 -x30917_bit0 -x40917_bit0 -x50917_bit0 -x60917_bit0 -x70917_bit0 x80917_bit0 -x11017_bit0 -x21017_bit0 -x31017_bit0 -x41017_bit0 -x51017_bit0 -x61017_bit0 -x71017_bit0 -x81017_bit0 -x91017_bit0 -x10227_bit0 -x10327_bit0 -x20327_bit0 -x10427_bit0 x20427_bit0 -x30427_bit0 -x10527_bit0 -x20527_bit0 -x30527_bit0 -x40527_bit0 -x10627_bit0 -x20627_bit0 -x30627_bit0 -x40627_bit0 -x50627_bit0 -x10727_bit0 -x20727_bit0 -x30727_bit0 -x40727_bit0 -x50727_bit0 -x60727_bit0 -x10827_bit0 -x20827_bit0 -x30827_bit0 -x40827_bit0 -x50827_bit0 -x60827_bit0 -x70827_bit0 -x10927_bit0 -x20927_bit0 -x30927_bit0 -x40927_bit0 -x50927_bit0 -x60927_bit0 -x70927_bit0 -x80927_bit0 -x11027_bit0 -x21027_bit0 -x31027_bit0 -x41027_bit0 -x51027_bit0 -x61027_bit0 -x71027_bit0 -x81027_bit0 -x91027_bit0 -x10237_bit0 -x10337_bit0 -x20337_bit0 -x10437_bit0 -x20437_bit0 -x30437_bit0 -x10537_bit0 -x20537_bit0 -x30537_bit0 -x40537_bit0 -x10637_bit0 -x20637_bit0 -x30637_bit0 -x40637_bit0 -x50637_bit0 -x10737_bit0 -x20737_bit0 x30737_bit0 -x40737_bit0 -x50737_bit0 -x60737_bit0 -x10837_bit0 -x20837_bit0 -x30837_bit0 -x40837_bit0 -x50837_bit0 -x60837_bit0 -x70837_bit0 -x10937_bit0 -x20937_bit0 -x30937_bit0 -x40937_bit0 -x50937_bit0 -x60937_bit0 -x70937_bit0 -x80937_bit0 -x11037_bit0 -x21037_bit0 -x31037_bit0 -x41037_bit0 -x51037_bit0 -x61037_bit0 -x71037_bit0 -x81037_bit0 -x91037_bit0 -x10247_bit0 -x10347_bit0 -x20347_bit0 -x10447_bit0 -x20447_bit0 -x30447_bit0 x10547_bit0 -x20547_bit0 -x30547_bit0 -x40547_bit0 -x10647_bit0 -x20647_bit0 -x30647_bit0 -x40647_bit0 -x50647_bit0 -x10747_bit0 -x20747_bit0 -x30747_bit0 -x40747_bit0 -x50747_bit0 -x60747_bit0 -x10847_bit0 -x20847_bit0 -x30847_bit0 -x40847_bit0 -x50847_bit0 -x60847_bit0 -x70847_bit0 -x10947_bit0 -x20947_bit0 -x30947_bit0 -x40947_bit0 -x50947_bit0 -x60947_bit0 -x70947_bit0 -x80947_bit0 -x11047_bit0 -x21047_bit0 -x31047_bit0 -x41047_bit0 -x51047_bit0 -x61047_bit0 -x71047_bit0 -x81047_bit0 -x91047_bit0 -x10257_bit0 -x10357_bit0 -x20357_bit0 -x10457_bit0 -x20457_bit0 -x30457_bit0 -x10557_bit0 -x20557_bit0 -x30557_bit0 -x40557_bit0 -x10657_bit0 -x20657_bit0 -x30657_bit0 -x40657_bit0 -x50657_bit0 -x10757_bit0 -x20757_bit0 -x30757_bit0 -x40757_bit0 -x50757_bit0 -x60757_bit0 -x10857_bit0 -x20857_bit0 -x30857_bit0 -x40857_bit0 -x50857_bit0 -x60857_bit0 -x70857_bit0 -x10957_bit0 -x20957_bit0 -x30957_bit0 -x40957_bit0 -x50957_bit0 -x60957_bit0 -x70957_bit0 -x80957_bit0 -x11057_bit0 -x21057_bit0 -x31057_bit0 -x41057_bit0 -x51057_bit0 x61057_bit0 -x71057_bit0 -x81057_bit0 -x91057_bit0 -x10218_bit0 -x10318_bit0 -x20318_bit0 -x10418_bit0 -x20418_bit0 -x30418_bit0 -x10518_bit0 -x20518_bit0 -x30518_bit0 -x40518_bit0 -x10618_bit0 -x20618_bit0 -x30618_bit0 -x40618_bit0 -x50618_bit0 -x10718_bit0 -x20718_bit0 -x30718_bit0 -x40718_bit0 -x50718_bit0 -x60718_bit0 -x10818_bit0 -x20818_bit0 -x30818_bit0 -x40818_bit0 -x50818_bit0 -x60818_bit0 -x70818_bit0 -x10918_bit0 -x20918_bit0 -x30918_bit0 -x40918_bit0 -x50918_bit0 -x60918_bit0 -x70918_bit0 -x80918_bit0 -x11018_bit0 x21018_bit0 -x31018_bit0 -x41018_bit0 -x51018_bit0 -x61018_bit0 -x71018_bit0 -x81018_bit0 -x91018_bit0 -x10228_bit0 -x10328_bit0 -x20328_bit0 -x10428_bit0 -x20428_bit0 -x30428_bit0 -x10528_bit0 -x20528_bit0 -x30528_bit0 -x40528_bit0 -x10628_bit0 -x20628_bit0 -x30628_bit0 -x40628_bit0 -x50628_bit0 -x10728_bit0 -x20728_bit0 -x30728_bit0 -x40728_bit0 -x50728_bit0 -x60728_bit0 -x10828_bit0 -x20828_bit0 -x30828_bit0 -x40828_bit0 -x50828_bit0 -x60828_bit0 -x70828_bit0 -x10928_bit0 -x20928_bit0 -x30928_bit0 -x40928_bit0 x50928_bit0 -x60928_bit0 -x70928_bit0 -x80928_bit0 -x11028_bit0 -x21028_bit0 -x31028_bit0 -x41028_bit0 -x51028_bit0 -x61028_bit0 -x71028_bit0 -x81028_bit0 -x91028_bit0 -x10238_bit0 -x10338_bit0 -x20338_bit0 -x10438_bit0 -x20438_bit0 -x30438_bit0 -x10538_bit0 -x20538_bit0 -x30538_bit0 -x40538_bit0 -x10638_bit0 -x20638_bit0 -x30638_bit0 -x40638_bit0 -x50638_bit0 -x10738_bit0 -x20738_bit0 -x30738_bit0 x40738_bit0 -x50738_bit0 -x60738_bit0 -x10838_bit0 -x20838_bit0 -x30838_bit0 -x40838_bit0 -x50838_bit0 -x60838_bit0 -x70838_bit0 -x10938_bit0 -x20938_bit0 -x30938_bit0 -x40938_bit0 -x50938_bit0 -x60938_bit0 -x70938_bit0 -x80938_bit0 -x11038_bit0 -x21038_bit0 -x31038_bit0 -x41038_bit0 -x51038_bit0 -x61038_bit0 -x71038_bit0 -x81038_bit0 -x91038_bit0 -x10248_bit0 -x10348_bit0 -x20348_bit0 -x10448_bit0 -x20448_bit0 -x30448_bit0 -x10548_bit0 -x20548_bit0 -x30548_bit0 -x40548_bit0 -x10648_bit0 -x20648_bit0 -x30648_bit0 -x40648_bit0 -x50648_bit0 -x10748_bit0 -x20748_bit0 -x30748_bit0 -x40748_bit0 -x50748_bit0 -x60748_bit0 -x10848_bit0 -x20848_bit0 -x30848_bit0 -x40848_bit0 -x50848_bit0 x60848_bit0 -x70848_bit0 -x10948_bit0 -x20948_bit0 -x30948_bit0 -x40948_bit0 -x50948_bit0 -x60948_bit0 -x70948_bit0 -x80948_bit0 -x11048_bit0 -x21048_bit0 -x31048_bit0 -x41048_bit0 -x51048_bit0 -x61048_bit0 -x71048_bit0 -x81048_bit0 -x91048_bit0 -x10258_bit0 x10358_bit0 -x20358_bit0 -x10458_bit0 -x20458_bit0 -x30458_bit0 -x10558_bit0 -x20558_bit0 -x30558_bit0 -x40558_bit0 -x10658_bit0 -x20658_bit0 -x30658_bit0 -x40658_bit0 -x50658_bit0 -x10758_bit0 -x20758_bit0 -x30758_bit0 -x40758_bit0 -x50758_bit0 -x60758_bit0 -x10858_bit0 -x20858_bit0 -x30858_bit0 -x40858_bit0 -x50858_bit0 -x60858_bit0 -x70858_bit0 -x10958_bit0 -x20958_bit0 -x30958_bit0 -x40958_bit0 -x50958_bit0 -x60958_bit0 -x70958_bit0 -x80958_bit0 -x11058_bit0 -x21058_bit0 -x31058_bit0 -x41058_bit0 -x51058_bit0 -x61058_bit0 -x71058_bit0 -x81058_bit0 -x91058_bit0 #### 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.79 0.94 0.91 2/54 28054
Raw data (stat): 28054 (runsolver) R 28053 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545852115 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.82 0.94 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 2524 0 0 0 993 5 0 0 25 0 1 0 545852115 12500992 2441 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3052 2441 603 41 0 3011 0
vsize: 12208
[startup+20.0003 s]
Raw data (loadavg): 0.85 0.94 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 2554 0 0 0 1993 5 0 0 25 0 1 0 545852115 12636160 2471 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3085 2471 603 41 0 3044 0
vsize: 12340
[startup+30.0014 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 2580 0 0 0 2992 6 0 0 25 0 1 0 545852115 12636160 2497 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3085 2497 603 41 0 3044 0
vsize: 12340
[startup+40.0012 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 2632 0 0 0 3991 7 0 0 25 0 1 0 545852115 12898304 2549 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3149 2549 603 41 0 3108 0
vsize: 12596
[startup+50.0014 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 2648 0 0 0 4991 7 0 0 25 0 1 0 545852115 13033472 2565 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3182 2565 603 41 0 3141 0
vsize: 12728
[startup+60.0014 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 2724 0 0 0 5990 8 0 0 25 0 1 0 545852115 13357056 2641 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3261 2641 603 41 0 3220 0
vsize: 13044
[startup+70.0019 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 2851 0 0 0 6990 8 0 0 25 0 1 0 545852115 13754368 2768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3358 2768 603 41 0 3317 0
vsize: 13432
[startup+80.0023 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 2935 0 0 0 7990 8 0 0 25 0 1 0 545852115 14159872 2852 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3457 2852 603 41 0 3416 0
vsize: 13828
[startup+90.0022 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 3043 0 0 0 8990 9 0 0 25 0 1 0 545852115 14643200 2960 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3575 2960 603 41 0 3534 0
vsize: 14300
[startup+100.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 3119 0 0 0 9990 9 0 0 25 0 1 0 545852115 14913536 3036 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3641 3036 603 41 0 3600 0
vsize: 14564
[startup+110.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 3208 0 0 0 10990 9 0 0 25 0 1 0 545852115 15314944 3125 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3739 3125 603 41 0 3698 0
vsize: 14956
[startup+120.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 3333 0 0 0 11990 10 0 0 25 0 1 0 545852115 15851520 3250 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3250 603 41 0 3829 0
vsize: 15480
[startup+130.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 3478 0 0 0 12990 10 0 0 25 0 1 0 545852115 16392192 3395 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4002 3395 603 41 0 3961 0
vsize: 16008
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 3628 0 0 0 13989 11 0 0 25 0 1 0 545852115 16928768 3545 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4133 3545 603 41 0 4092 0
vsize: 16532
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 3766 0 0 0 14989 11 0 0 25 0 1 0 545852115 17731584 3683 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4329 3683 603 41 0 4288 0
vsize: 17316
[startup+160.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 3911 0 0 0 15988 11 0 0 25 0 1 0 545852115 18268160 3828 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4460 3828 603 41 0 4419 0
vsize: 17840
[startup+170.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 4114 0 0 0 16988 12 0 0 25 0 1 0 545852115 19079168 4031 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4658 4031 603 41 0 4617 0
vsize: 18632
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 4262 0 0 0 17988 13 0 0 25 0 1 0 545852115 19619840 4179 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4790 4179 603 41 0 4749 0
vsize: 19160
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 4491 0 0 0 18987 14 0 0 25 0 1 0 545852115 20561920 4408 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5020 4408 603 41 0 4979 0
vsize: 20080
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 4675 0 0 0 19986 14 0 0 25 0 1 0 545852115 21368832 4592 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5217 4592 603 41 0 5176 0
vsize: 20868
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 4917 0 0 0 20985 15 0 0 25 0 1 0 545852115 22310912 4834 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5447 4834 603 41 0 5406 0
vsize: 21788
[startup+220.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 5108 0 0 0 21984 16 0 0 25 0 1 0 545852115 23121920 5025 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5645 5025 603 41 0 5604 0
vsize: 22580
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 5335 0 0 0 22983 16 0 0 25 0 1 0 545852115 24059904 5252 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5874 5252 603 41 0 5833 0
vsize: 23496
[startup+240.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 5580 0 0 0 23983 17 0 0 25 0 1 0 545852115 25006080 5497 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6105 5497 603 41 0 6064 0
vsize: 24420
[startup+250.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 5852 0 0 0 24983 18 0 0 25 0 1 0 545852115 26083328 5769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6368 5769 603 41 0 6327 0
vsize: 25472
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 6184 0 0 0 25982 19 0 0 25 0 1 0 545852115 27422720 6101 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6695 6101 603 41 0 6654 0
vsize: 26780
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 6422 0 0 0 26981 19 0 0 25 0 1 0 545852115 28491776 6339 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6956 6339 603 41 0 6915 0
vsize: 27824
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 6637 0 0 0 27981 20 0 0 25 0 1 0 545852115 29294592 6554 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7152 6554 603 41 0 7111 0
vsize: 28608
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 6966 0 0 0 28980 21 0 0 25 0 1 0 545852115 30892032 6883 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7542 6883 603 41 0 7501 0
vsize: 30168
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 7362 0 0 0 29979 22 0 0 25 0 1 0 545852115 32497664 7279 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7934 7279 603 41 0 7893 0
vsize: 31736
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 8334 0 0 0 30976 26 0 0 25 0 1 0 545852115 36057088 8251 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8803 8251 603 41 0 8762 0
vsize: 35212
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 8334 0 0 0 31976 26 0 0 25 0 1 0 545852115 36057088 8251 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8803 8251 603 41 0 8762 0
vsize: 35212
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 8335 0 0 0 32976 26 0 0 25 0 1 0 545852115 36057088 8252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8803 8252 603 41 0 8762 0
vsize: 35212
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 8335 0 0 0 33976 26 0 0 25 0 1 0 545852115 36057088 8252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8803 8252 603 41 0 8762 0
vsize: 35212
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 8335 0 0 0 34976 26 0 0 25 0 1 0 545852115 36057088 8252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8803 8252 603 41 0 8762 0
vsize: 35212
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 8335 0 0 0 35976 26 0 0 25 0 1 0 545852115 36057088 8252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8803 8252 603 41 0 8762 0
vsize: 35212
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 8336 0 0 0 36976 26 0 0 25 0 1 0 545852115 36057088 8253 4294967295 134512640 134672761 3221224544 3221223616 1074718851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8803 8253 603 41 0 8762 0
vsize: 35212
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 8336 0 0 0 37976 26 0 0 25 0 1 0 545852115 36057088 8253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8803 8253 603 41 0 8762 0
vsize: 35212
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 8336 0 0 0 38976 26 0 0 25 0 1 0 545852115 36057088 8253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8803 8253 603 41 0 8762 0
vsize: 35212
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 8655 0 0 0 39976 27 0 0 25 0 1 0 545852115 37400576 8572 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9131 8572 603 41 0 9090 0
vsize: 36524
[startup+410.004 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 8891 0 0 0 40975 28 0 0 25 0 1 0 545852115 38338560 8808 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9360 8808 603 41 0 9319 0
vsize: 37440
[startup+420.004 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 9183 0 0 0 41974 29 0 0 25 0 1 0 545852115 39546880 9100 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9655 9100 603 41 0 9614 0
vsize: 38620
[startup+430.005 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 9651 0 0 0 42974 30 0 0 25 0 1 0 545852115 41406464 9568 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10109 9568 603 41 0 10068 0
vsize: 40436
[startup+440.004 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 10020 0 0 0 43973 30 0 0 25 0 1 0 545852115 42995712 9937 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9937 603 41 0 10456 0
vsize: 41988
[startup+450.005 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 10286 0 0 0 44972 32 0 0 25 0 1 0 545852115 44060672 10203 4294967295 134512640 134672761 3221224544 3221223648 134560424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10757 10203 603 41 0 10716 0
vsize: 43028
[startup+460.011 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 10642 0 0 0 45973 32 0 0 25 0 1 0 545852115 45543424 10559 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11119 10559 603 41 0 11078 0
vsize: 44476
[startup+470.012 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 10977 0 0 0 46972 33 0 0 25 0 1 0 545852115 46882816 10894 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11446 10894 603 41 0 11405 0
vsize: 45784
[startup+480.014 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 11293 0 0 0 47971 34 0 0 25 0 1 0 545852115 48095232 11210 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11742 11210 603 41 0 11701 0
vsize: 46968
[startup+490.019 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 11659 0 0 0 48971 35 0 0 25 0 1 0 545852115 49692672 11576 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12132 11576 603 41 0 12091 0
vsize: 48528
[startup+500.018 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 49970 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+510.018 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 50970 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+520.022 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 51970 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+530.023 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 52970 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+540.023 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 53971 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+550.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 54971 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+560.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 55971 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+570.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 56971 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+580.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 57971 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+590.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 58971 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+600.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 59971 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+610.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 60972 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+620.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 61972 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+630.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 62972 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+640.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 63972 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+650.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 64972 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+660.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12008 0 0 0 65972 36 0 0 25 0 1 0 545852115 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11925 603 41 0 12438 0
vsize: 49916
[startup+670.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12386 0 0 0 66971 38 0 0 25 0 1 0 545852115 52727808 12303 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12873 12303 603 41 0 12832 0
vsize: 51492
[startup+680.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 12824 0 0 0 67971 39 0 0 25 0 1 0 545852115 54444032 12741 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13292 12741 603 41 0 13251 0
vsize: 53168
[startup+690.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 13159 0 0 0 68969 40 0 0 25 0 1 0 545852115 55779328 13076 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13618 13076 603 41 0 13577 0
vsize: 54472
[startup+700.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 13433 0 0 0 69969 40 0 0 25 0 1 0 545852115 56991744 13350 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13914 13350 603 41 0 13873 0
vsize: 55656
[startup+710.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 13771 0 0 0 70969 41 0 0 25 0 1 0 545852115 58322944 13688 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14239 13688 603 41 0 14198 0
vsize: 56956
[startup+720.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 14095 0 0 0 71968 42 0 0 25 0 1 0 545852115 59666432 14012 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14567 14012 603 41 0 14526 0
vsize: 58268
[startup+730.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 14505 0 0 0 72967 43 0 0 25 0 1 0 545852115 61374464 14422 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14984 14422 603 41 0 14943 0
vsize: 59936
[startup+740.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 14799 0 0 0 73966 44 0 0 25 0 1 0 545852115 62586880 14716 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15280 14716 603 41 0 15239 0
vsize: 61120
[startup+750.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 15151 0 0 0 74966 44 0 0 25 0 1 0 545852115 64053248 15068 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15638 15068 603 41 0 15597 0
vsize: 62552
[startup+760.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 15606 0 0 0 75965 45 0 0 25 0 1 0 545852115 65925120 15523 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16095 15523 603 41 0 16054 0
vsize: 64380
[startup+770.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 16016 0 0 0 76965 46 0 0 25 0 1 0 545852115 67518464 15933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16484 15933 603 41 0 16443 0
vsize: 65936
[startup+780.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 16299 0 0 0 77964 47 0 0 25 0 1 0 545852115 68722688 16216 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16778 16216 603 41 0 16737 0
vsize: 67112
[startup+790.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 16666 0 0 0 78963 48 0 0 25 0 1 0 545852115 70180864 16583 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17134 16583 603 41 0 17093 0
vsize: 68536
[startup+800.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 16888 0 0 0 79962 49 0 0 25 0 1 0 545852115 71122944 16805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17364 16805 603 41 0 17323 0
vsize: 69456
[startup+810.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 17099 0 0 0 80962 49 0 0 25 0 1 0 545852115 71917568 17016 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17558 17016 603 41 0 17517 0
vsize: 70232
[startup+820.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 17394 0 0 0 81961 50 0 0 25 0 1 0 545852115 73113600 17311 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17850 17311 603 41 0 17809 0
vsize: 71400
[startup+830.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 17769 0 0 0 82960 52 0 0 25 0 1 0 545852115 74719232 17686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18242 17686 603 41 0 18201 0
vsize: 72968
[startup+840.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 18019 0 0 0 83960 52 0 0 25 0 1 0 545852115 75653120 17936 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18470 17936 603 41 0 18429 0
vsize: 73880
[startup+850.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 18295 0 0 0 84960 53 0 0 25 0 1 0 545852115 76849152 18212 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18762 18212 603 41 0 18721 0
vsize: 75048
[startup+860.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 18674 0 0 0 85959 53 0 0 25 0 1 0 545852115 78323712 18591 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19122 18591 603 41 0 19081 0
vsize: 76488
[startup+870.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 19241 0 0 0 86959 55 0 0 25 0 1 0 545852115 80719872 19158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19707 19158 603 41 0 19666 0
vsize: 78828
[startup+880.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 19516 0 0 0 87959 55 0 0 25 0 1 0 545852115 81776640 19433 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19965 19433 603 41 0 19924 0
vsize: 79860
[startup+890.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 19774 0 0 0 88959 56 0 0 25 0 1 0 545852115 82841600 19691 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20225 19691 603 41 0 20184 0
vsize: 80900
[startup+900.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 20012 0 0 0 89959 57 0 0 25 0 1 0 545852115 83906560 19929 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20485 19929 603 41 0 20444 0
vsize: 81940
[startup+910.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 20390 0 0 0 90958 58 0 0 25 0 1 0 545852115 85360640 20307 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20840 20307 603 41 0 20799 0
vsize: 83360
[startup+920.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 20633 0 0 0 91956 59 0 0 25 0 1 0 545852115 86421504 20550 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21099 20550 603 41 0 21058 0
vsize: 84396
[startup+930.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 20968 0 0 0 92955 60 0 0 25 0 1 0 545852115 87744512 20885 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21422 20885 603 41 0 21381 0
vsize: 85688
[startup+940.051 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 21214 0 0 0 93953 62 0 0 25 0 1 0 545852115 88813568 21131 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21683 21131 603 41 0 21642 0
vsize: 86732
[startup+950.055 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 21505 0 0 0 94953 62 0 0 25 0 1 0 545852115 90005504 21422 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21974 21422 603 41 0 21933 0
vsize: 87896
[startup+960.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 21737 0 0 0 95953 63 0 0 25 0 1 0 545852115 90947584 21654 4294967295 134512640 134672761 3221224544 3221223648 134560352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22204 21654 603 41 0 22163 0
vsize: 88816
[startup+970.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 21958 0 0 0 96953 64 0 0 25 0 1 0 545852115 91758592 21875 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22402 21875 603 41 0 22361 0
vsize: 89608
[startup+980.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 22213 0 0 0 97952 65 0 0 25 0 1 0 545852115 92835840 22130 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22665 22130 603 41 0 22624 0
vsize: 90660
[startup+990.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 22506 0 0 0 98952 65 0 0 25 0 1 0 545852115 94040064 22423 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22959 22423 603 41 0 22918 0
vsize: 91836
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 22870 0 0 0 99950 67 0 0 25 0 1 0 545852115 95494144 22787 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23314 22787 603 41 0 23273 0
vsize: 93256
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 23274 0 0 0 100950 68 0 0 25 0 1 0 545852115 97210368 23191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23733 23191 603 41 0 23692 0
vsize: 94932
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 23589 0 0 0 101949 68 0 0 25 0 1 0 545852115 98402304 23506 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24024 23506 603 41 0 23983 0
vsize: 96096
[startup+1030.08 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 23884 0 0 0 102951 68 0 0 25 0 1 0 545852115 99598336 23801 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24316 23801 603 41 0 24275 0
vsize: 97264
[startup+1040.08 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 24201 0 0 0 103950 69 0 0 25 0 1 0 545852115 100941824 24118 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24644 24118 603 41 0 24603 0
vsize: 98576
[startup+1050.09 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 24433 0 0 0 104950 70 0 0 25 0 1 0 545852115 101879808 24350 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24873 24350 603 41 0 24832 0
vsize: 99492
[startup+1060.09 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 24680 0 0 0 105949 71 0 0 25 0 1 0 545852115 102948864 24597 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25134 24597 603 41 0 25093 0
vsize: 100536
[startup+1070.09 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 24919 0 0 0 106949 72 0 0 25 0 1 0 545852115 103890944 24836 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25364 24836 603 41 0 25323 0
vsize: 101456
[startup+1080.09 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 25251 0 0 0 107948 73 0 0 25 0 1 0 545852115 105238528 25168 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25693 25168 603 41 0 25652 0
vsize: 102772
[startup+1090.09 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 25487 0 0 0 108948 74 0 0 25 0 1 0 545852115 106180608 25404 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25923 25404 603 41 0 25882 0
vsize: 103692
[startup+1100.09 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 25701 0 0 0 109947 74 0 0 25 0 1 0 545852115 107106304 25618 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26149 25618 603 41 0 26108 0
vsize: 104596
[startup+1110.09 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 25939 0 0 0 110947 75 0 0 25 0 1 0 545852115 108040192 25856 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26377 25856 603 41 0 26336 0
vsize: 105508
[startup+1120.09 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 26289 0 0 0 111946 76 0 0 25 0 1 0 545852115 109498368 26206 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26733 26206 603 41 0 26692 0
vsize: 106932
[startup+1130.09 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 26605 0 0 0 112945 77 0 0 25 0 1 0 545852115 110706688 26522 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27028 26522 603 41 0 26987 0
vsize: 108112
[startup+1140.09 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 26845 0 0 0 113944 78 0 0 25 0 1 0 545852115 111771648 26762 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27288 26762 603 41 0 27247 0
vsize: 109152
[startup+1150.09 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 27120 0 0 0 114944 78 0 0 25 0 1 0 545852115 112836608 27037 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27548 27037 603 41 0 27507 0
vsize: 110192
[startup+1160.09 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 27321 0 0 0 115943 79 0 0 25 0 1 0 545852115 113639424 27238 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27744 27238 603 41 0 27703 0
vsize: 110976
[startup+1170.09 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 27593 0 0 0 116942 80 0 0 25 0 1 0 545852115 114851840 27510 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28040 27510 603 41 0 27999 0
vsize: 112160
[startup+1180.09 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 27889 0 0 0 117942 81 0 0 25 0 1 0 545852115 116060160 27806 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28335 27806 603 41 0 28294 0
vsize: 113340
[startup+1190.09 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 28246 0 0 0 118942 81 0 0 25 0 1 0 545852115 117538816 28163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28696 28163 603 41 0 28655 0
vsize: 114784
[startup+1200.09 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28054
Raw data (stat): 28054 (minisat+) R 28053 10614 10613 0 -1 0 28496 0 0 0 119941 82 0 0 25 0 1 0 545852115 118476800 28413 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28925 28413 603 41 0 28884 0
vsize: 115700
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.01 1.00 0.93 1/54 28054
Raw data (stat): 28054 (minisat+) Z 28053 10614 10613 0 -1 12 28499 0 0 0 119941 87 0 0 25 0 1 0 545852115 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.15
CPU time (s): 1200.3
CPU user time (s): 1199.42
CPU system time (s): 0.877866
CPU usage (%): 100.013
Max. virtual memory (Kb): 115700
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####