PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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	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.54
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 21474

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 23:58:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13153 boxname=wulflinc5 idbench=1012 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  130bea0863cb3f92addf09aabe15daa3  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-10teams.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-10teams.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-10teams.opb
IDLAUNCH: 13153
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
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:        563992 kB
Buffers:         30732 kB
Cached:         418848 kB
SwapCached:        444 kB
Active:          92064 kB
Inactive:       359656 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        563740 kB
SwapTotal:     2097136 kB
SwapFree:      2095948 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5200 kB
Slab:            13300 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 00:18:49 (client local time) WITH STATUS 10 IN 1200.51 SECONDS
stats: 13153 7 1200.51 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.92 0.95 0.91 2/54 5405
Raw data (stat): 5405 (runsolver) R 5404 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491002579 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0013 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 5405
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 2525 0 0 0 993 6 0 0 25 0 1 0 491002579 12500992 2442 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3052 2442 603 41 0 3011 0
vsize: 12208
[startup+20.002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 5405
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 2554 0 0 0 1992 6 0 0 25 0 1 0 491002579 12636160 2471 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3085 2471 603 41 0 3044 0
vsize: 12340
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5405
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 2581 0 0 0 2992 6 0 0 25 0 1 0 491002579 12636160 2498 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3085 2498 603 41 0 3044 0
vsize: 12340
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5405
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 2633 0 0 0 3992 7 0 0 25 0 1 0 491002579 12898304 2550 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3149 2550 603 41 0 3108 0
vsize: 12596
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5405
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 2653 0 0 0 4992 7 0 0 25 0 1 0 491002579 13033472 2570 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3182 2570 603 41 0 3141 0
vsize: 12728
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5405
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 2731 0 0 0 5991 8 0 0 25 0 1 0 491002579 13357056 2648 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3261 2648 603 41 0 3220 0
vsize: 13044
[startup+70.0042 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5405
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 2854 0 0 0 6991 8 0 0 25 0 1 0 491002579 13889536 2771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3391 2771 603 41 0 3350 0
vsize: 13564
[startup+80.0128 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 5443
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 2941 0 0 0 7985 15 0 0 25 0 1 0 491002579 14159872 2858 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3457 2858 603 41 0 3416 0
vsize: 13828
[startup+90.0129 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5458
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 3047 0 0 0 8984 16 0 0 25 0 1 0 491002579 14643200 2964 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3575 2964 603 41 0 3534 0
vsize: 14300
[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5458
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 3124 0 0 0 9984 16 0 0 25 0 1 0 491002579 14913536 3041 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3641 3041 603 41 0 3600 0
vsize: 14564
[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5458
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 3210 0 0 0 10984 16 0 0 25 0 1 0 491002579 15314944 3127 4294967295 134512640 134672761 3221224544 3221223696 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3739 3127 603 41 0 3698 0
vsize: 14956
[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5458
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 3338 0 0 0 11984 16 0 0 25 0 1 0 491002579 15851520 3255 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3255 603 41 0 3829 0
vsize: 15480
[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5458
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 3486 0 0 0 12984 16 0 0 25 0 1 0 491002579 16392192 3403 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4002 3403 603 41 0 3961 0
vsize: 16008
[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5458
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 3631 0 0 0 13984 17 0 0 25 0 1 0 491002579 17063936 3548 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4166 3548 603 41 0 4125 0
vsize: 16664
[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5458
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 3766 0 0 0 14984 17 0 0 25 0 1 0 491002579 17731584 3683 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 3919 0 0 0 15983 18 0 0 25 0 1 0 491002579 18268160 3836 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4460 3836 603 41 0 4419 0
vsize: 17840
[startup+170.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 4118 0 0 0 16983 18 0 0 25 0 1 0 491002579 19079168 4035 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4658 4035 603 41 0 4617 0
vsize: 18632
[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 4285 0 0 0 17983 19 0 0 25 0 1 0 491002579 19755008 4202 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4823 4202 603 41 0 4782 0
vsize: 19292
[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 4502 0 0 0 18982 19 0 0 25 0 1 0 491002579 20697088 4419 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5053 4419 603 41 0 5012 0
vsize: 20212
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 4692 0 0 0 19982 20 0 0 25 0 1 0 491002579 21368832 4609 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5217 4609 603 41 0 5176 0
vsize: 20868
[startup+210.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 4927 0 0 0 20981 21 0 0 25 0 1 0 491002579 22310912 4844 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5447 4844 603 41 0 5406 0
vsize: 21788
[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 5123 0 0 0 21981 21 0 0 25 0 1 0 491002579 23121920 5040 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5645 5040 603 41 0 5604 0
vsize: 22580
[startup+230.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 5342 0 0 0 22980 22 0 0 25 0 1 0 491002579 24059904 5259 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5874 5259 603 41 0 5833 0
vsize: 23496
[startup+240.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 5600 0 0 0 23980 23 0 0 25 0 1 0 491002579 25137152 5517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6137 5517 603 41 0 6096 0
vsize: 24548
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 5874 0 0 0 24979 24 0 0 25 0 1 0 491002579 26214400 5791 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6400 5791 603 41 0 6359 0
vsize: 25600
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 6234 0 0 0 25978 25 0 0 25 0 1 0 491002579 27693056 6151 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6761 6151 603 41 0 6720 0
vsize: 27044
[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 6461 0 0 0 26977 26 0 0 25 0 1 0 491002579 28626944 6378 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6989 6378 603 41 0 6948 0
vsize: 27956
[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 6679 0 0 0 27977 26 0 0 25 0 1 0 491002579 29425664 6596 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7184 6596 603 41 0 7143 0
vsize: 28736
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 6989 0 0 0 28976 27 0 0 25 0 1 0 491002579 31027200 6906 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7575 6906 603 41 0 7534 0
vsize: 30300
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 7388 0 0 0 29976 28 0 0 25 0 1 0 491002579 32632832 7305 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7967 7305 603 41 0 7926 0
vsize: 31868
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 8334 0 0 0 30973 30 0 0 25 0 1 0 491002579 36057088 8251 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8803 8251 603 41 0 8762 0
vsize: 35212
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 8334 0 0 0 31972 31 0 0 25 0 1 0 491002579 36057088 8251 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 8335 0 0 0 32972 31 0 0 25 0 1 0 491002579 36057088 8252 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 8335 0 0 0 33973 31 0 0 25 0 1 0 491002579 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 8335 0 0 0 34973 31 0 0 25 0 1 0 491002579 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 8335 0 0 0 35973 31 0 0 25 0 1 0 491002579 36057088 8252 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 8336 0 0 0 36973 31 0 0 25 0 1 0 491002579 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+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 8336 0 0 0 37973 31 0 0 25 0 1 0 491002579 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 8341 0 0 0 38973 31 0 0 25 0 1 0 491002579 36057088 8258 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8803 8258 603 41 0 8762 0
vsize: 35212
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5460
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 8673 0 0 0 39972 32 0 0 25 0 1 0 491002579 37400576 8590 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9131 8590 603 41 0 9090 0
vsize: 36524
[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 8908 0 0 0 40974 33 0 0 25 0 1 0 491002579 38338560 8825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9360 8825 603 41 0 9319 0
vsize: 37440
[startup+420.032 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 9224 0 0 0 41973 33 0 0 25 0 1 0 491002579 39673856 9141 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9686 9141 603 41 0 9645 0
vsize: 38744
[startup+430.046 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 9698 0 0 0 42973 35 0 0 25 0 1 0 491002579 41676800 9615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10175 9615 603 41 0 10134 0
vsize: 40700
[startup+440.046 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 10036 0 0 0 43973 35 0 0 25 0 1 0 491002579 42995712 9953 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10497 9953 603 41 0 10456 0
vsize: 41988
[startup+450.048 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 10326 0 0 0 44973 36 0 0 25 0 1 0 491002579 44191744 10243 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10789 10243 603 41 0 10748 0
vsize: 43156
[startup+460.059 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 10657 0 0 0 45973 37 0 0 25 0 1 0 491002579 45543424 10574 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11119 10574 603 41 0 11078 0
vsize: 44476
[startup+470.059 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 11006 0 0 0 46972 38 0 0 25 0 1 0 491002579 47017984 10923 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11479 10923 603 41 0 11438 0
vsize: 45916
[startup+480.059 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 11318 0 0 0 47972 38 0 0 25 0 1 0 491002579 48230400 11235 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11775 11235 603 41 0 11734 0
vsize: 47100
[startup+490.06 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 11696 0 0 0 48971 39 0 0 25 0 1 0 491002579 49827840 11613 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12165 11613 603 41 0 12124 0
vsize: 48660
[startup+500.06 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 49971 40 0 0 25 0 1 0 491002579 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.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 50971 40 0 0 25 0 1 0 491002579 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+520.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 51971 40 0 0 25 0 1 0 491002579 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+530.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 52971 40 0 0 25 0 1 0 491002579 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134561201 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.066 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 53972 40 0 0 25 0 1 0 491002579 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+550.067 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 54972 40 0 0 25 0 1 0 491002579 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.067 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 55972 40 0 0 25 0 1 0 491002579 51113984 11925 4294967295 134512640 134672761 3221224544 3221223728 134559354 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.067 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 56972 40 0 0 25 0 1 0 491002579 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134560852 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.066 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 57972 40 0 0 25 0 1 0 491002579 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134561188 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.066 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 58973 40 0 0 25 0 1 0 491002579 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+600.066 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 59973 40 0 0 25 0 1 0 491002579 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.067 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 60973 40 0 0 25 0 1 0 491002579 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+620.066 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 61973 40 0 0 25 0 1 0 491002579 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+630.066 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 62973 40 0 0 25 0 1 0 491002579 51113984 11925 4294967295 134512640 134672761 3221224544 3221223744 134557895 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.067 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 63973 40 0 0 25 0 1 0 491002579 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134560876 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.067 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 64974 40 0 0 25 0 1 0 491002579 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+660.067 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12008 0 0 0 65974 40 0 0 25 0 1 0 491002579 51113984 11925 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.067 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12464 0 0 0 66973 41 0 0 25 0 1 0 491002579 52998144 12381 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12939 12381 603 41 0 12898 0
vsize: 51756
[startup+680.067 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 12861 0 0 0 67972 42 0 0 25 0 1 0 491002579 54579200 12778 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13325 12778 603 41 0 13284 0
vsize: 53300
[startup+690.067 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 13186 0 0 0 68971 43 0 0 25 0 1 0 491002579 55914496 13103 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13651 13103 603 41 0 13610 0
vsize: 54604
[startup+700.066 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 13453 0 0 0 69971 44 0 0 25 0 1 0 491002579 56991744 13370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13914 13370 603 41 0 13873 0
vsize: 55656
[startup+710.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 13831 0 0 0 70970 44 0 0 25 0 1 0 491002579 58593280 13748 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14305 13748 603 41 0 14264 0
vsize: 57220
[startup+720.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 14146 0 0 0 71970 45 0 0 25 0 1 0 491002579 59920384 14063 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14629 14063 603 41 0 14588 0
vsize: 58516
[startup+730.067 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 14524 0 0 0 72969 46 0 0 25 0 1 0 491002579 61509632 14441 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15017 14441 603 41 0 14976 0
vsize: 60068
[startup+740.075 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 14845 0 0 0 73970 46 0 0 25 0 1 0 491002579 62722048 14762 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15313 14762 603 41 0 15272 0
vsize: 61252
[startup+750.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 15209 0 0 0 74969 48 0 0 25 0 1 0 491002579 64188416 15126 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15671 15126 603 41 0 15630 0
vsize: 62684
[startup+760.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 15676 0 0 0 75967 49 0 0 25 0 1 0 491002579 66191360 15593 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16160 15593 603 41 0 16119 0
vsize: 64640
[startup+770.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 16060 0 0 0 76967 50 0 0 25 0 1 0 491002579 67788800 15977 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16550 15977 603 41 0 16509 0
vsize: 66200
[startup+780.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 16371 0 0 0 77966 51 0 0 25 0 1 0 491002579 68980736 16288 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16841 16288 603 41 0 16800 0
vsize: 67364
[startup+790.075 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 16724 0 0 0 78966 51 0 0 25 0 1 0 491002579 70451200 16641 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17200 16641 603 41 0 17159 0
vsize: 68800
[startup+800.075 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 16910 0 0 0 79966 51 0 0 25 0 1 0 491002579 71258112 16827 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17397 16827 603 41 0 17356 0
vsize: 69588
[startup+810.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 17124 0 0 0 80965 52 0 0 25 0 1 0 491002579 72048640 17041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17590 17041 603 41 0 17549 0
vsize: 70360
[startup+820.077 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 17476 0 0 0 81965 53 0 0 25 0 1 0 491002579 73519104 17393 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17949 17393 603 41 0 17908 0
vsize: 71796
[startup+830.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 17837 0 0 0 82964 54 0 0 25 0 1 0 491002579 74985472 17754 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18307 17754 603 41 0 18266 0
vsize: 73228
[startup+840.083 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 18065 0 0 0 83964 54 0 0 25 0 1 0 491002579 75915264 17982 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18534 17982 603 41 0 18493 0
vsize: 74136
[startup+850.187 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 18368 0 0 0 84974 55 0 0 25 0 1 0 491002579 77115392 18285 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18827 18285 603 41 0 18786 0
vsize: 75308
[startup+860.187 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 18808 0 0 0 85973 56 0 0 25 0 1 0 491002579 78987264 18725 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19284 18725 603 41 0 19243 0
vsize: 77136
[startup+870.19 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 19317 0 0 0 86973 57 0 0 25 0 1 0 491002579 80986112 19234 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19772 19234 603 41 0 19731 0
vsize: 79088
[startup+880.198 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 19595 0 0 0 87973 58 0 0 25 0 1 0 491002579 82178048 19512 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20063 19512 603 41 0 20022 0
vsize: 80252
[startup+890.198 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 19820 0 0 0 88973 58 0 0 25 0 1 0 491002579 83107840 19737 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20290 19737 603 41 0 20249 0
vsize: 81160
[startup+900.212 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 20088 0 0 0 89974 59 0 0 25 0 1 0 491002579 84168704 20005 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20549 20005 603 41 0 20508 0
vsize: 82196
[startup+910.231 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 20463 0 0 0 90974 59 0 0 25 0 1 0 491002579 85749760 20380 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20935 20380 603 41 0 20894 0
vsize: 83740
[startup+920.24 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 20660 0 0 0 91974 60 0 0 25 0 1 0 491002579 86556672 20577 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21132 20577 603 41 0 21091 0
vsize: 84528
[startup+930.239 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 21030 0 0 0 92973 61 0 0 25 0 1 0 491002579 88014848 20947 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21488 20947 603 41 0 21447 0
vsize: 85952
[startup+940.24 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 21250 0 0 0 93973 62 0 0 25 0 1 0 491002579 88948736 21167 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21716 21167 603 41 0 21675 0
vsize: 86864
[startup+950.24 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 21593 0 0 0 94972 63 0 0 25 0 1 0 491002579 90275840 21510 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22040 21510 603 41 0 21999 0
vsize: 88160
[startup+960.241 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 21810 0 0 0 95972 63 0 0 25 0 1 0 491002579 91217920 21727 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22270 21727 603 41 0 22229 0
vsize: 89080
[startup+970.241 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 22027 0 0 0 96972 63 0 0 25 0 1 0 491002579 92028928 21944 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22468 21944 603 41 0 22427 0
vsize: 89872
[startup+980.241 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 22272 0 0 0 97972 64 0 0 25 0 1 0 491002579 93102080 22189 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22730 22189 603 41 0 22689 0
vsize: 90920
[startup+990.241 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 22589 0 0 0 98971 64 0 0 25 0 1 0 491002579 94310400 22506 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23025 22506 603 41 0 22984 0
vsize: 92100
[startup+1000.24 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 23007 0 0 0 99971 65 0 0 25 0 1 0 491002579 96022528 22924 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23443 22924 603 41 0 23402 0
vsize: 93772
[startup+1010.24 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 23387 0 0 0 100970 66 0 0 25 0 1 0 491002579 97607680 23304 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23830 23304 603 41 0 23789 0
vsize: 95320
[startup+1020.24 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 23666 0 0 0 101969 67 0 0 25 0 1 0 491002579 98807808 23583 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24123 23583 603 41 0 24082 0
vsize: 96492
[startup+1030.24 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 23961 0 0 0 102969 67 0 0 25 0 1 0 491002579 100003840 23878 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24415 23878 603 41 0 24374 0
vsize: 97660
[startup+1040.24 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 24241 0 0 0 103969 68 0 0 25 0 1 0 491002579 101076992 24158 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24677 24158 603 41 0 24636 0
vsize: 98708
[startup+1050.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 24520 0 0 0 104969 69 0 0 25 0 1 0 491002579 102277120 24437 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24970 24437 603 41 0 24929 0
vsize: 99880
[startup+1060.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 24733 0 0 0 105969 69 0 0 25 0 1 0 491002579 103088128 24650 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25168 24650 603 41 0 25127 0
vsize: 100672
[startup+1070.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 25020 0 0 0 106968 70 0 0 25 0 1 0 491002579 104296448 24937 4294967295 134512640 134672761 3221224544 3221223648 134559824 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25463 24937 603 41 0 25422 0
vsize: 101852
[startup+1080.26 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 25345 0 0 0 107968 71 0 0 25 0 1 0 491002579 105639936 25262 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25791 25262 603 41 0 25750 0
vsize: 103164
[startup+1090.28 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 25564 0 0 0 108969 72 0 0 25 0 1 0 491002579 106582016 25481 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26021 25481 603 41 0 25980 0
vsize: 104084
[startup+1100.28 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 25749 0 0 0 109968 72 0 0 25 0 1 0 491002579 107237376 25666 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26181 25666 603 41 0 26140 0
vsize: 104724
[startup+1110.28 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 26068 0 0 0 110968 73 0 0 25 0 1 0 491002579 108572672 25985 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26507 25985 603 41 0 26466 0
vsize: 106028
[startup+1120.28 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 26389 0 0 0 111968 74 0 0 25 0 1 0 491002579 109899776 26306 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26831 26306 603 41 0 26790 0
vsize: 107324
[startup+1130.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 26693 0 0 0 112968 75 0 0 25 0 1 0 491002579 111099904 26610 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27124 26610 603 41 0 27083 0
vsize: 108496
[startup+1140.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 26936 0 0 0 113967 76 0 0 25 0 1 0 491002579 112164864 26853 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27384 26853 603 41 0 27343 0
vsize: 109536
[startup+1150.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 27201 0 0 0 114966 77 0 0 25 0 1 0 491002579 113242112 27118 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27647 27118 603 41 0 27606 0
vsize: 110588
[startup+1160.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 27398 0 0 0 115966 78 0 0 25 0 1 0 491002579 114044928 27315 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27843 27315 603 41 0 27802 0
vsize: 111372
[startup+1170.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 27691 0 0 0 116965 79 0 0 25 0 1 0 491002579 115253248 27608 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28138 27608 603 41 0 28097 0
vsize: 112552
[startup+1180.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 28046 0 0 0 117965 79 0 0 25 0 1 0 491002579 116727808 27963 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28498 27963 603 41 0 28457 0
vsize: 113992
[startup+1190.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 28343 0 0 0 118964 80 0 0 25 0 1 0 491002579 117809152 28260 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28762 28260 603 41 0 28721 0
vsize: 115048
[startup+1200.29 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5462
Raw data (stat): 5405 (minisat+) R 5404 24215 24214 0 -1 0 28519 0 0 0 119964 81 0 0 25 0 1 0 491002579 118611968 28436 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28958 28436 603 41 0 28917 0
vsize: 115832
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.36 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 5462
Raw data (stat): 5405 (minisat+) Z 5404 24215 24214 0 -1 12 28522 0 0 0 119964 86 0 0 25 0 1 0 491002579 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.36
CPU time (s): 1200.51
CPU user time (s): 1199.64
CPU system time (s): 0.865868
CPU usage (%): 100.013
Max. virtual memory (Kb): 115832
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####