PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-pp08aCUTS.opb
MD5SUM	d1b87efc35bcd73acfc5183bbe3df4f0
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	2304
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	178464600
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	178464600
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	3288
Total number of constraints	374
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	64
Number of constraints which are nor clauses,nor cardinality constraints	310
Minimum length of a constraint	1
Maximum length of a constraint	123
Trace number 15324

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        617968 kB
Buffers:          7340 kB
Cached:         385564 kB
SwapCached:          0 kB
Active:          66216 kB
Inactive:       329588 kB
HighTotal:      131008 kB
HighFree:        30324 kB
LowTotal:       903652 kB
LowFree:        587644 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            15260 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 04:16:06 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 17911 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 374 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[ 501]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 500]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 499]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 498]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 497]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 496]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 495]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 494]---> Adder-cost: 51   maxlim: 11774   bits: 15/14
c ---[ 485]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 484]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 483]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 482]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 481]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 480]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 479]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 477]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 476]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 475]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 474]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 473]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 472]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 471]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 469]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 468]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 467]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 466]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 465]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 464]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 463]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 462]---> Adder-cost: 28   maxlim: 12286   bits: 15/14
c ---[ 461]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 460]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 459]---> Adder-cost: 30   maxlim: 20734   bits: 16/15
c ---[ 458]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 457]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 456]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 455]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 454]---> Adder-cost: 53   maxlim: 14334   bits: 15/14
c ---[ 445]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 444]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 443]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 442]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 441]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 440]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 439]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 438]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 436]---> Adder-cost: 80   maxlim: 1114110   bits: 22/21
c ---[ 434]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 433]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 432]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 431]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 430]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 429]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 428]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 427]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 426]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 425]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 424]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 422]---> Adder-cost: 160   maxlim: 2123517   bits: 23/22
c ---[ 421]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 420]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 419]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[ 418]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 417]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 416]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 415]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 414]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 413]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 412]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 410]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[ 409]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 408]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 407]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 406]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 405]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 404]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 403]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 402]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 401]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 400]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 398]---> Adder-cost: 160   maxlim: 2126077   bits: 23/22
c ---[ 397]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 396]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 395]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 394]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 393]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 392]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 391]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 386]---> Adder-cost: 160   maxlim: 2129917   bits: 23/22
c ---[ 374]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 362]---> Adder-cost: 80   maxlim: 1074942   bits: 22/21
c ---[ 350]---> Adder-cost: 80   maxlim: 1108990   bits: 22/21
c ---[ 338]---> Adder-cost: 160   maxlim: 2156285   bits: 23/22
c ---[ 326]---> Adder-cost: 160   maxlim: 2162685   bits: 23/22
c ---[ 314]---> Adder-cost: 160   maxlim: 2153725   bits: 23/22
c ---[ 312]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 300]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 288]---> Adder-cost: 160   maxlim: 2152445   bits: 23/22
c ---[ 276]---> Adder-cost: 160   maxlim: 2151165   bits: 23/22
c ---[ 264]---> Adder-cost: 80   maxlim: 1093630   bits: 22/21
c ---[ 255]---> Adder-cost: 80   maxlim: 1114110   bits: 22/21
c ---[ 253]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 251]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 249]---> Adder-cost: 160   maxlim: 2143485   bits: 23/22
c ---[ 247]---> Adder-cost: 160   maxlim: 2142205   bits: 23/22
c ---[ 245]---> Adder-cost: 160   maxlim: 2156285   bits: 23/22
c ---[ 243]---> Adder-cost: 160   maxlim: 2151165   bits: 23/22
c ---[ 241]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 239]---> Adder-cost: 80   maxlim: 1101310   bits: 22/21
c ---[ 237]---> Adder-cost: 80   maxlim: 1074942   bits: 22/21
c ---[ 235]---> Adder-cost: 160   maxlim: 2129917   bits: 23/22
c ---[ 233]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[ 231]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 229]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[ 227]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[ 225]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[ 223]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 221]---> Adder-cost: 80   maxlim: 1080062   bits: 22/21
c ---[ 219]---> Adder-cost: 80   maxlim: 1105150   bits: 22/21
c ---[ 217]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 215]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 213]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 211]---> Adder-cost: 160   maxlim: 2149885   bits: 23/22
c ---[ 209]---> Adder-cost: 160   maxlim: 2160125   bits: 23/22
c ---[ 207]---> Adder-cost: 160   maxlim: 2157565   bits: 23/22
c ---[ 205]---> Adder-cost: 80   maxlim: 1107710   bits: 22/21
c ---[ 203]---> Adder-cost: 80   maxlim: 1081342   bits: 22/21
c ---[ 201]---> Adder-cost: 160   maxlim: 2160125   bits: 23/22
c ---[ 199]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[ 197]---> Adder-cost: 160   maxlim: 2123517   bits: 23/22
c ---[ 195]---> Adder-cost: 160   maxlim: 2128637   bits: 23/22
c ---[ 193]---> Adder-cost: 160   maxlim: 2127357   bits: 23/22
c ---[ 191]---> Adder-cost: 160   maxlim: 2122237   bits: 23/22
c ---[ 189]---> Adder-cost: 160   maxlim: 2124797   bits: 23/22
c ---[ 187]---> Adder-cost: 80   maxlim: 1076222   bits: 22/21
c ---[ 185]---> Adder-cost: 80   maxlim: 1063678   bits: 22/21
c ---[ 183]---> Adder-cost: 160   maxlim: 2110973   bits: 23/22
c ---[ 181]---> Adder-cost: 160   maxlim: 2113533   bits: 23/22
c ---[ 179]---> Adder-cost: 160   maxlim: 2152445   bits: 23/22
c ---[ 177]---> Adder-cost: 160   maxlim: 2113533   bits: 23/22
c ---[ 175]---> Adder-cost: 160   maxlim: 2112253   bits: 23/22
c ---[ 173]---> Adder-cost: 160   maxlim: 2112253   bits: 23/22
c ---[ 171]---> Adder-cost: 160   maxlim: 2110973   bits: 23/22
c ---[ 169]---> Adder-cost: 80   maxlim: 1061118   bits: 22/21
c ---[ 168]---> Adder-cost: 218   maxlim: 332023   bits: 19/19
c ---[ 167]---> Adder-cost: 218   maxlim: 332023   bits: 19/19
c ---[ 166]---> Adder-cost: 218   maxlim: 332023   bits: 19/19
c ---[ 165]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[ 164]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[ 162]---> Adder-cost: 160   maxlim: 2162685   bits: 23/22
c ---[ 161]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[ 160]---> Adder-cost: 218   maxlim: 325623   bits: 19/19
c ---[ 159]---> Adder-cost: 218   maxlim: 312823   bits: 19/19
c ---[ 158]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 157]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 156]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 155]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 154]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 153]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 152]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 150]---> Adder-cost: 80   maxlim: 1101310   bits: 22/21
c ---[ 149]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 148]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 147]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 146]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 145]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 144]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 143]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 142]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 141]---> Adder-cost: 8   maxlim: 32766   bits: 16/15
c ---[ 140]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 138]---> Adder-cost: 80   maxlim: 1078782   bits: 22/21
c ---[ 137]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 136]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 135]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 134]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 133]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 132]---> Adder-cost: 10   maxlim: 65534   bits: 17/16
c ---[ 131]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 130]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 129]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 128]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 127]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 126]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 125]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 124]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 123]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 122]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 121]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 120]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 119]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[ 118]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[ 117]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 116]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 115]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 114]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 113]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 112]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 111]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 110]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 109]---> Adder-cost: 41   maxlim: 8959   bits: 15/14
c ---[ 108]---> Adder-cost: 113   maxlim: 65534   bits: 17/16
c ---[ 107]---> Adder-cost: 37   maxlim: 6399   bits: 14/13
c ---[ 106]---> Adder-cost: 113   maxlim: 65534   bits: 17/16
c ---[ 105]---> Adder-cost: 39   maxlim: 12799   bits: 15/14
c ---[ 104]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[ 103]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[ 102]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[ 101]---> Adder-cost: 35   maxlim: 10239   bits: 15/14
c ---[ 100]---> Adder-cost: 107   maxlim: 65534   bits: 17/16
c ---[  99]---> Adder-cost: 10   maxlim: 12799   bits: 15/14
c ---[  98]---> Adder-cost: 78   maxlim: 65534   bits: 17/16
c ---[  97]---> Adder-cost: 6   maxlim: 2559   bits: 13/12
c ---[  96]---> Adder-cost: 72   maxlim: 32766   bits: 16/15
c ---[  95]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  94]---> Adder-cost: 101   maxlim: 32766   bits: 16/15
c ---[  93]---> Adder-cost: 37   maxlim: 6399   bits: 14/13
c ---[  92]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  91]---> Adder-cost: 33   maxlim: 3839   bits: 13/12
c ---[  90]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  89]---> Adder-cost: 29   maxlim: 1279   bits: 12/11
c ---[  88]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  87]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  86]---> Adder-cost: 101   maxlim: 32766   bits: 16/15
c ---[  85]---> Adder-cost: 10   maxlim: 6399   bits: 14/13
c ---[  84]---> Adder-cost: 74   maxlim: 32766   bits: 16/15
c ---[  83]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[  82]---> Adder-cost: 76   maxlim: 65534   bits: 17/16
c ---[  81]---> Adder-cost: 37   maxlim: 6399   bits: 14/13
c ---[  80]---> Adder-cost: 113   maxlim: 65534   bits: 17/16
c ---[  79]---> Adder-cost: 39   maxlim: 12799   bits: 15/14
c ---[  78]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  77]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  76]---> Adder-cost: 109   maxlim: 65534   bits: 17/16
c ---[  75]---> Adder-cost: 35   maxlim: 10239   bits: 15/14
c ---[  74]---> Adder-cost: 107   maxlim: 65534   bits: 17/16
c ---[  73]---> Adder-cost: 41   maxlim: 11519   bits: 15/14
c ---[  72]---> Adder-cost: 113   maxlim: 65534   bits: 17/16
c ---[  71]---> Adder-cost: 6   maxlim: 20479   bits: 16/15
c ---[  70]---> Adder-cost: 72   maxlim: 65534   bits: 17/16
c ---[  69]---> Adder-cost: 39   maxlim: 12799   bits: 15/14
c ---[  68]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  67]---> Adder-cost: 39   maxlim: 12799   bits: 15/14
c ---[  66]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  65]---> Adder-cost: 45   maxlim: 19199   bits: 16/15
c ---[  64]---> Adder-cost: 113   maxlim: 65534   bits: 17/16
c ---[  63]---> Adder-cost: 37   maxlim: 20479   bits: 16/15
c ---[  62]---> Adder-cost: 105   maxlim: 65534   bits: 17/16
c ---[  61]---> Adder-cost: 41   maxlim: 11519   bits: 15/14
c ---[  60]---> Adder-cost: 113   maxlim: 65534   bits: 17/16
c ---[  59]---> Adder-cost: 39   maxlim: 12799   bits: 15/14
c ---[  58]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  57]---> Adder-cost: 10   maxlim: 12799   bits: 15/14
c ---[  56]---> Adder-cost: 78   maxlim: 65534   bits: 17/16
c ---[  55]---> Adder-cost: 10   maxlim: 6399   bits: 14/13
c ---[  54]---> Adder-cost: 74   maxlim: 32766   bits: 16/15
c ---[  53]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[  52]---> Adder-cost: 103   maxlim: 32766   bits: 16/15
c ---[  51]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  50]---> Adder-cost: 101   maxlim: 32766   bits: 16/15
c ---[  49]---> Adder-cost: 29   maxlim: 1279   bits: 12/11
c ---[  48]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  47]---> Adder-cost: 29   maxlim: 1279   bits: 12/11
c ---[  46]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  45]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[  44]---> Adder-cost: 103   maxlim: 32766   bits: 16/15
c ---[  43]---> Adder-cost: 6   maxlim: 1279   bits: 12/11
c ---[  42]---> Adder-cost: 74   maxlim: 32766   bits: 16/15
c ---[  41]---> Adder-cost: 12   maxlim: 8959   bits: 15/14
c ---[  40]---> Adder-cost: 80   maxlim: 65534   bits: 17/16
c ---[  39]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  38]---> Adder-cost: 109   maxlim: 65534   bits: 17/16
c ---[  37]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  36]---> Adder-cost: 109   maxlim: 65534   bits: 17/16
c ---[  35]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  34]---> Adder-cost: 109   maxlim: 65534   bits: 17/16
c ---[  33]---> Adder-cost: 39   maxlim: 12799   bits: 15/14
c ---[  32]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  31]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[  30]---> Adder-cost: 111   maxlim: 65534   bits: 17/16
c ---[  29]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  28]---> Adder-cost: 109   maxlim: 65534   bits: 17/16
c ---[  27]---> Adder-cost: 10   maxlim: 6399   bits: 14/13
c ---[  26]---> Adder-cost: 80   maxlim: 65534   bits: 17/16
c ---[  25]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[  24]---> Adder-cost: 103   maxlim: 32766   bits: 16/15
c ---[  23]---> Adder-cost: 37   maxlim: 6399   bits: 14/13
c ---[  22]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  21]---> Adder-cost: 29   maxlim: 1279   bits: 12/11
c ---[  20]---> Adder-cost: 105   maxlim: 32766   bits: 16/15
c ---[  19]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[  18]---> Adder-cost: 103   maxlim: 32766   bits: 16/15
c ---[  17]---> Adder-cost: 35   maxlim: 7679   bits: 14/13
c ---[  16]---> Adder-cost: 103   maxlim: 32766   bits: 16/15
c ---[  15]---> Adder-cost: 33   maxlim: 5119   bits: 14/13
c ---[  14]---> Adder-cost: 101   maxlim: 32766   bits: 16/15
c ---[  13]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[  12]---> Adder-cost: 70   maxlim: 32766   bits: 16/15
c ---[  11]---> Adder-cost: 6   maxlim: 1279   bits: 12/11
c ---[  10]---> Adder-cost: 68   maxlim: 16382   bits: 15/14
c ---[   9]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[   8]---> Adder-cost: 95   maxlim: 16382   bits: 15/14
c ---[   7]---> Adder-cost: 29   maxlim: 1279   bits: 12/11
c ---[   6]---> Adder-cost: 97   maxlim: 16382   bits: 15/14
c ---[   5]---> Adder-cost: 29   maxlim: 1279   bits: 12/11
c ---[   4]---> Adder-cost: 97   maxlim: 16382   bits: 15/14
c ---[   3]---> Adder-cost: 31   maxlim: 2559   bits: 13/12
c ---[   2]---> Adder-cost: 95   maxlim: 16382   bits: 15/14
c ---[   1]---> Adder-cost: 8   maxlim: 3839   bits: 13/12
c ---[   0]---> Adder-cost: 68   maxlim: 16382   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  126353   460481 |   42117       0        0     nan |  0.000 % |
c |       101 |  126353   460481 |   46328     101      496     4.9 | 20.451 % |
c |       251 |  126345   460455 |   50961     250     1223     4.9 | 20.454 % |
c |       477 |  126317   460365 |   56057     472     2238     4.7 | 20.469 % |
c |       814 |  126309   460339 |   61663     808     3625     4.5 | 20.472 % |
c |      1320 |  126285   460261 |   67829    1311     6540     5.0 | 20.483 % |
c |      2079 |  126265   460199 |   74612    2067    10396     5.0 | 20.494 % |
c |      3218 |  126195   459971 |   82074    3196    16441     5.1 | 20.526 % |
c |      4926 |  126083   459607 |   90281    4883    24732     5.1 | 20.580 % |
c |      7488 |  125880   458948 |   99309    7390    39093     5.3 | 20.685 % |
c |     11332 |  125703   458369 |  109240   11183    61676     5.5 | 20.775 % |
c |     17098 |  125625   458115 |  120164   16933   100445     5.9 | 20.815 % |
c |     25747 |  125528   457790 |  132181   25560   171572     6.7 | 20.869 % |
c |     38721 |  125391   457337 |  145399   38499   276751     7.2 | 20.945 % |
c |     58182 |  125252   456876 |  159939   57938   454377     7.8 | 21.017 % |
c |     87376 |  125090   456350 |  175933   87101   743625     8.5 | 21.103 % |
c |    131166 |  124966   455948 |  193526  130845  1426789    10.9 | 21.183 % |
c |    196850 |  124909   455763 |  212879  196520  2662585    13.5 | 21.211 % |
c |    295376 |  124774   455316 |  234167   93810  1422080    15.2 | 21.287 % |
c |    443165 |  124746   455224 |  257583   35468   274586     7.7 | 21.302 % |
c |    664848 |  124739   455201 |  283342  257150  3207713    12.5 | 21.305 % |
c |    997373 |  124732   455178 |  311676   79748   800519    10.0 | 21.309 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 1.03 0.98 0.91 2/55 1704
Raw data (stat): 1704 (runsolver) R 1703 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 419269978 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 1.03 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 3794 0 0 0 989 9 0 0 25 0 1 0 419269978 17305600 3640 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4225 3640 603 41 0 4184 0
vsize: 16900
[startup+20.0011 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 3985 0 0 0 1989 10 0 0 25 0 1 0 419269978 18116608 3831 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4423 3831 603 41 0 4382 0
vsize: 17692
[startup+30.0018 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 4161 0 0 0 2989 11 0 0 25 0 1 0 419269978 18792448 4007 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4588 4007 603 41 0 4547 0
vsize: 18352
[startup+40.0015 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 4340 0 0 0 3988 11 0 0 25 0 1 0 419269978 19595264 4186 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4784 4186 603 41 0 4743 0
vsize: 19136
[startup+50.0012 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 4503 0 0 0 4988 12 0 0 25 0 1 0 419269978 20271104 4349 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4349 603 41 0 4908 0
vsize: 19796
[startup+60.0013 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 4661 0 0 0 5987 13 0 0 25 0 1 0 419269978 20811776 4507 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5081 4507 603 41 0 5040 0
vsize: 20324
[startup+70.0019 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 4823 0 0 0 6986 13 0 0 25 0 1 0 419269978 21749760 4669 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5310 4669 603 41 0 5269 0
vsize: 21240
[startup+80.0022 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 5004 0 0 0 7986 14 0 0 25 0 1 0 419269978 22425600 4850 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5475 4850 603 41 0 5434 0
vsize: 21900
[startup+90.0019 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 5160 0 0 0 8985 15 0 0 25 0 1 0 419269978 23101440 5006 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5640 5006 603 41 0 5599 0
vsize: 22560
[startup+100.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 5439 0 0 0 9984 16 0 0 25 0 1 0 419269978 24182784 5285 4294967295 134512640 134672761 3221224544 3221223712 134561415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5904 5285 603 41 0 5863 0
vsize: 23616
[startup+110.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 5730 0 0 0 10983 17 0 0 25 0 1 0 419269978 25264128 5576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6168 5576 603 41 0 6127 0
vsize: 24672
[startup+120.003 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 6145 0 0 0 11982 19 0 0 25 0 1 0 419269978 27009024 5991 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6594 5991 603 41 0 6553 0
vsize: 26376
[startup+130.004 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 6599 0 0 0 12980 21 0 0 25 0 1 0 419269978 29274112 6445 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7147 6445 603 41 0 7106 0
vsize: 28588
[startup+140.004 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 6830 0 0 0 13979 21 0 0 25 0 1 0 419269978 30220288 6676 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7378 6676 603 41 0 7337 0
vsize: 29512
[startup+150.004 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 7059 0 0 0 14978 22 0 0 25 0 1 0 419269978 31031296 6905 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7576 6905 603 41 0 7535 0
vsize: 30304
[startup+160.004 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 7228 0 0 0 15977 24 0 0 25 0 1 0 419269978 31703040 7074 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7740 7074 603 41 0 7699 0
vsize: 30960
[startup+170.003 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 7452 0 0 0 16976 25 0 0 25 0 1 0 419269978 32649216 7298 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7971 7298 603 41 0 7930 0
vsize: 31884
[startup+180.003 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 7930 0 0 0 17974 27 0 0 25 0 1 0 419269978 34533376 7776 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8431 7776 603 41 0 8390 0
vsize: 33724
[startup+190.004 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 8374 0 0 0 18973 28 0 0 25 0 1 0 419269978 36278272 8220 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8857 8220 603 41 0 8816 0
vsize: 35428
[startup+200.003 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 8757 0 0 0 19972 29 0 0 25 0 1 0 419269978 37904384 8603 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9254 8603 603 41 0 9213 0
vsize: 37016
[startup+210.003 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9190 0 0 0 20972 30 0 0 25 0 1 0 419269978 39661568 9036 4294967295 134512640 134672761 3221224544 3221223484 1075350787 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9036 603 41 0 9642 0
vsize: 38732
[startup+220.003 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9190 0 0 0 21972 30 0 0 25 0 1 0 419269978 39661568 9036 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9036 603 41 0 9642 0
vsize: 38732
[startup+230.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1704
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9190 0 0 0 22972 30 0 0 25 0 1 0 419269978 39661568 9036 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9036 603 41 0 9642 0
vsize: 38732
[startup+240.002 s]
Raw data (loadavg): 1.00 0.98 0.91 3/58 1741
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9190 0 0 0 23971 30 0 0 25 0 1 0 419269978 39661568 9036 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9036 603 41 0 9642 0
vsize: 38732
[startup+250.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1757
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9191 0 0 0 24971 30 0 0 25 0 1 0 419269978 39661568 9037 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9037 603 41 0 9642 0
vsize: 38732
[startup+260.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1757
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9191 0 0 0 25972 30 0 0 25 0 1 0 419269978 39661568 9037 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9037 603 41 0 9642 0
vsize: 38732
[startup+270.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1757
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9192 0 0 0 26972 30 0 0 25 0 1 0 419269978 39661568 9038 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9038 603 41 0 9642 0
vsize: 38732
[startup+280.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1757
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9192 0 0 0 27972 30 0 0 25 0 1 0 419269978 39661568 9038 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9038 603 41 0 9642 0
vsize: 38732
[startup+290.001 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1757
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9193 0 0 0 28972 30 0 0 25 0 1 0 419269978 39661568 9039 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9039 603 41 0 9642 0
vsize: 38732
[startup+300.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1759
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9193 0 0 0 29971 31 0 0 25 0 1 0 419269978 39661568 9039 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9039 603 41 0 9642 0
vsize: 38732
[startup+310.002 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1761
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9193 0 0 0 30971 31 0 0 25 0 1 0 419269978 39661568 9039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9039 603 41 0 9642 0
vsize: 38732
[startup+320.003 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1761
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9193 0 0 0 31971 31 0 0 25 0 1 0 419269978 39661568 9039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9039 603 41 0 9642 0
vsize: 38732
[startup+330.003 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1761
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9193 0 0 0 32971 32 0 0 25 0 1 0 419269978 39661568 9039 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9039 603 41 0 9642 0
vsize: 38732
[startup+340.003 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1761
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9193 0 0 0 33971 32 0 0 25 0 1 0 419269978 39661568 9039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9039 603 41 0 9642 0
vsize: 38732
[startup+350.003 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 1761
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9193 0 0 0 34971 32 0 0 25 0 1 0 419269978 39661568 9039 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9039 603 41 0 9642 0
vsize: 38732
[startup+360.009 s]
Raw data (loadavg): 1.08 1.00 0.92 3/69 1778
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9193 0 0 0 35971 32 0 0 25 0 1 0 419269978 39661568 9039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9039 603 41 0 9642 0
vsize: 38732
[startup+370.01 s]
Raw data (loadavg): 1.37 1.06 0.94 3/64 1778
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9193 0 0 0 36971 33 0 0 25 0 1 0 419269978 39661568 9039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9039 603 41 0 9642 0
vsize: 38732
[startup+380.011 s]
Raw data (loadavg): 1.70 1.14 0.97 2/61 2010
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9194 0 0 0 37962 35 0 0 25 0 1 0 419269978 39661568 9040 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9040 603 41 0 9642 0
vsize: 38732
[startup+390.011 s]
Raw data (loadavg): 1.74 1.17 0.98 3/61 2043
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9194 0 0 0 38963 35 0 0 25 0 1 0 419269978 39661568 9040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9683 9040 603 41 0 9642 0
vsize: 38732
[startup+400.011 s]
Raw data (loadavg): 1.63 1.16 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9194 0 0 0 39960 38 0 0 25 0 1 0 419269978 39661568 9040 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9040 603 41 0 9642 0
vsize: 38732
[startup+410.011 s]
Raw data (loadavg): 1.53 1.16 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9194 0 0 0 40960 38 0 0 25 0 1 0 419269978 39661568 9040 4294967295 134512640 134672761 3221224544 3221223712 134564748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9040 603 41 0 9642 0
vsize: 38732
[startup+420.012 s]
Raw data (loadavg): 1.45 1.15 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9367 0 0 0 41960 39 0 0 25 0 1 0 419269978 40329216 9213 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9846 9213 603 41 0 9805 0
vsize: 39384
[startup+430.012 s]
Raw data (loadavg): 1.38 1.15 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9550 0 0 0 42959 40 0 0 25 0 1 0 419269978 41136128 9396 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10043 9396 603 41 0 10002 0
vsize: 40172
[startup+440.012 s]
Raw data (loadavg): 1.32 1.14 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9732 0 0 0 43958 40 0 0 25 0 1 0 419269978 41807872 9578 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10207 9578 603 41 0 10166 0
vsize: 40828
[startup+450.011 s]
Raw data (loadavg): 1.27 1.14 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 9860 0 0 0 44958 41 0 0 25 0 1 0 419269978 42344448 9706 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10338 9706 603 41 0 10297 0
vsize: 41352
[startup+460.019 s]
Raw data (loadavg): 1.23 1.13 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10035 0 0 0 45958 41 0 0 25 0 1 0 419269978 43020288 9881 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10503 9881 603 41 0 10462 0
vsize: 42012
[startup+470.019 s]
Raw data (loadavg): 1.19 1.13 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 46958 41 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+480.02 s]
Raw data (loadavg): 1.16 1.12 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 47958 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+490.02 s]
Raw data (loadavg): 1.14 1.12 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 48959 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+500.02 s]
Raw data (loadavg): 1.12 1.11 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 49959 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+510.019 s]
Raw data (loadavg): 1.10 1.11 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 50959 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+520.019 s]
Raw data (loadavg): 1.08 1.10 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 51959 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+530.024 s]
Raw data (loadavg): 1.07 1.10 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 52960 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+540.024 s]
Raw data (loadavg): 1.06 1.10 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 53960 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+550.023 s]
Raw data (loadavg): 1.05 1.09 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 54960 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+560.024 s]
Raw data (loadavg): 1.04 1.09 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 55960 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+570.024 s]
Raw data (loadavg): 1.03 1.09 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 56960 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+580.024 s]
Raw data (loadavg): 1.03 1.08 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 57961 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+590.024 s]
Raw data (loadavg): 1.02 1.08 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 58961 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+600.024 s]
Raw data (loadavg): 1.02 1.08 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 59961 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+610.024 s]
Raw data (loadavg): 1.02 1.07 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 60961 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+620.024 s]
Raw data (loadavg): 1.01 1.07 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 61961 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134564738 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+630.024 s]
Raw data (loadavg): 1.01 1.07 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 62962 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+640.024 s]
Raw data (loadavg): 1.01 1.07 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 63962 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+650.024 s]
Raw data (loadavg): 1.01 1.06 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 64962 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223648 134555333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+660.024 s]
Raw data (loadavg): 1.00 1.06 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 65962 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+670.023 s]
Raw data (loadavg): 1.00 1.06 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 66962 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+680.023 s]
Raw data (loadavg): 1.00 1.06 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 67962 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+690.023 s]
Raw data (loadavg): 1.00 1.05 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 68962 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+700.022 s]
Raw data (loadavg): 1.00 1.05 0.98 2/55 2080
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 69963 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+710.022 s]
Raw data (loadavg): 1.00 1.05 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10037 0 0 0 70963 42 0 0 25 0 1 0 419269978 43020288 9883 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9883 603 41 0 10462 0
vsize: 42012
[startup+720.022 s]
Raw data (loadavg): 1.00 1.05 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10086 0 0 0 71963 42 0 0 25 0 1 0 419269978 43151360 9932 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10535 9932 603 41 0 10494 0
vsize: 42140
[startup+730.022 s]
Raw data (loadavg): 1.00 1.05 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10290 0 0 0 72962 43 0 0 25 0 1 0 419269978 43962368 10136 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10733 10136 603 41 0 10692 0
vsize: 42932
[startup+740.022 s]
Raw data (loadavg): 1.00 1.04 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10490 0 0 0 73961 43 0 0 25 0 1 0 419269978 44769280 10336 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10930 10336 603 41 0 10889 0
vsize: 43720
[startup+750.022 s]
Raw data (loadavg): 1.00 1.04 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10656 0 0 0 74961 44 0 0 25 0 1 0 419269978 46489600 10502 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11350 10502 603 41 0 11309 0
vsize: 45400
[startup+760.023 s]
Raw data (loadavg): 1.00 1.04 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10799 0 0 0 75960 45 0 0 25 0 1 0 419269978 47026176 10645 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11481 10645 603 41 0 11440 0
vsize: 45924
[startup+770.023 s]
Raw data (loadavg): 1.00 1.04 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 10912 0 0 0 76961 45 0 0 25 0 1 0 419269978 47431680 10758 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11580 10758 603 41 0 11539 0
vsize: 46320
[startup+780.025 s]
Raw data (loadavg): 1.00 1.04 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11201 0 0 0 77960 46 0 0 25 0 1 0 419269978 48635904 11047 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11874 11047 603 41 0 11833 0
vsize: 47496
[startup+790.025 s]
Raw data (loadavg): 1.00 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11327 0 0 0 78959 46 0 0 25 0 1 0 419269978 49176576 11173 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11173 603 41 0 11965 0
vsize: 48024
[startup+800.024 s]
Raw data (loadavg): 1.00 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 79959 47 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+810.025 s]
Raw data (loadavg): 1.00 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 80958 47 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+820.025 s]
Raw data (loadavg): 1.00 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 81959 47 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+830.025 s]
Raw data (loadavg): 1.00 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 82959 47 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+840.027 s]
Raw data (loadavg): 1.00 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 83959 47 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+850.026 s]
Raw data (loadavg): 1.00 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 84959 47 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+860.025 s]
Raw data (loadavg): 1.00 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 85959 47 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223744 134557959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+870.026 s]
Raw data (loadavg): 1.00 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 86958 47 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+880.027 s]
Raw data (loadavg): 1.00 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 87959 47 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+890.026 s]
Raw data (loadavg): 1.00 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 88959 48 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+900.034 s]
Raw data (loadavg): 1.00 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 89959 48 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+910.042 s]
Raw data (loadavg): 1.00 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 90960 48 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+920.041 s]
Raw data (loadavg): 1.00 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 91960 48 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+930.042 s]
Raw data (loadavg): 1.07 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 92960 48 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+940.058 s]
Raw data (loadavg): 1.06 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 93961 48 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+950.057 s]
Raw data (loadavg): 1.05 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 94961 48 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+960.069 s]
Raw data (loadavg): 1.04 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 95962 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+970.069 s]
Raw data (loadavg): 1.04 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 96962 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+980.074 s]
Raw data (loadavg): 1.03 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 97963 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+990.074 s]
Raw data (loadavg): 1.02 1.03 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 98963 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+1000.07 s]
Raw data (loadavg): 1.02 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 99964 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+1010.07 s]
Raw data (loadavg): 1.02 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 100964 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+1020.07 s]
Raw data (loadavg): 1.01 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 101964 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+1030.07 s]
Raw data (loadavg): 1.01 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 102964 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+1040.07 s]
Raw data (loadavg): 1.01 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 103964 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+1050.08 s]
Raw data (loadavg): 1.01 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 104965 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+1060.08 s]
Raw data (loadavg): 1.01 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 105965 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+1070.08 s]
Raw data (loadavg): 1.00 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 106965 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+1080.08 s]
Raw data (loadavg): 1.00 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 107965 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+1090.08 s]
Raw data (loadavg): 1.00 1.02 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 108966 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+1100.08 s]
Raw data (loadavg): 1.00 1.01 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11344 0 0 0 109966 49 0 0 25 0 1 0 419269978 49176576 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12006 11190 603 41 0 11965 0
vsize: 48024
[startup+1110.08 s]
Raw data (loadavg): 1.00 1.01 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11444 0 0 0 110966 49 0 0 25 0 1 0 419269978 49582080 11290 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12105 11290 603 41 0 12064 0
vsize: 48420
[startup+1120.08 s]
Raw data (loadavg): 1.00 1.01 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11610 0 0 0 111966 49 0 0 25 0 1 0 419269978 50257920 11456 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12270 11456 603 41 0 12229 0
vsize: 49080
[startup+1130.08 s]
Raw data (loadavg): 1.00 1.01 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11711 0 0 0 112966 50 0 0 25 0 1 0 419269978 50659328 11557 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12368 11557 603 41 0 12327 0
vsize: 49472
[startup+1140.12 s]
Raw data (loadavg): 1.00 1.01 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11711 0 0 0 113970 50 0 0 25 0 1 0 419269978 50659328 11557 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12368 11557 603 41 0 12327 0
vsize: 49472
[startup+1150.14 s]
Raw data (loadavg): 1.00 1.01 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11711 0 0 0 114972 50 0 0 25 0 1 0 419269978 50659328 11557 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12368 11557 603 41 0 12327 0
vsize: 49472
[startup+1160.14 s]
Raw data (loadavg): 1.00 1.01 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11711 0 0 0 115972 50 0 0 25 0 1 0 419269978 50659328 11557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12368 11557 603 41 0 12327 0
vsize: 49472
[startup+1170.14 s]
Raw data (loadavg): 1.00 1.01 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11711 0 0 0 116972 50 0 0 25 0 1 0 419269978 50659328 11557 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12368 11557 603 41 0 12327 0
vsize: 49472
[startup+1180.14 s]
Raw data (loadavg): 1.00 1.01 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11711 0 0 0 117968 50 0 0 25 0 1 0 419269978 50659328 11557 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12368 11557 603 41 0 12327 0
vsize: 49472
[startup+1190.14 s]
Raw data (loadavg): 1.00 1.01 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11711 0 0 0 118968 50 0 0 25 0 1 0 419269978 50659328 11557 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12368 11557 603 41 0 12327 0
vsize: 49472
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.98 2/55 2082
Raw data (stat): 1704 (minisat+) R 1703 30927 30926 0 -1 0 11711 0 0 0 119968 50 0 0 25 0 1 0 419269978 50659328 11557 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12368 11557 603 41 0 12327 0
vsize: 49472
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 1.00 0.98 1/55 2082
Raw data (stat): 1704 (minisat+) Z 1703 30927 30926 0 -1 12 11713 0 0 0 119968 52 0 0 24 0 1 0 419269978 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.18
CPU time (s): 1200.21
CPU user time (s): 1199.69
CPU system time (s): 0.527919
CPU usage (%): 100.003
Max. virtual memory (Kb): 49472
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####