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/miplib/normalized-mps-v2-13-7-fixnet3.opb
MD5SUM	d5b458ca51c84d53d4ddd22dc72bb5f7
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	16410049
Optimality of the best value was proved	NO
Number of terms in the objective function	9830
Biggest coefficient in the objective function	52428800
Number of bits for the biggest coefficient in the objective function	26
Sum of the numbers in the objective function	23652414692
Number of bits of the sum of numbers in the objective function	35
Biggest number in a constraint	52428800
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	23652414692
Number of bits of the biggest sum of numbers	35
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.25
Number of variables	9890
Total number of constraints	978
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	378
Number of constraints which are nor clauses,nor cardinality constraints	600
Minimum length of a constraint	1
Maximum length of a constraint	1072
Trace number 19283

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        519432 kB
Buffers:         31460 kB
Cached:         462972 kB
SwapCached:        744 kB
Active:          96536 kB
Inactive:       399860 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        519180 kB
SwapTotal:     2097892 kB
SwapFree:      2096220 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            13096 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:59:53 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 16819 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 700 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssss
c ---[ 593]---> Adder-cost: 84   maxlim: 68348   bits: 18/17
c ---[ 591]---> Adder-cost: 896   maxlim: 492249   bits: 20/19
c ---[ 589]---> Adder-cost: 224   maxlim: 140282   bits: 19/18
c ---[ 587]---> Adder-cost: 1068   maxlim: 306133   bits: 20/19
c ---[ 585]---> Adder-cost: 536   maxlim: 216300   bits: 19/18
c ---[ 583]---> Adder-cost: 958   maxlim: 434137   bits: 20/19
c ---[ 581]---> Adder-cost: 518   maxlim: 272114   bits: 20/19
c ---[ 579]---> Adder-cost: 824   maxlim: 289249   bits: 20/19
c ---[ 577]---> Adder-cost: 620   maxlim: 346857   bits: 20/19
c ---[ 575]---> Adder-cost: 868   maxlim: 359136   bits: 20/19
c ---[ 573]---> Adder-cost: 657   maxlim: 219625   bits: 19/18
c ---[ 571]---> Adder-cost: 342   maxlim: 75000   bits: 18/17
c ---[ 569]---> Adder-cost: 1288   maxlim: 642508   bits: 20/20
c ---[ 567]---> Adder-cost: 512   maxlim: 285163   bits: 19/19
c ---[ 565]---> Adder-cost: 519   maxlim: 215791   bits: 19/18
c ---[ 563]---> Adder-cost: 468   maxlim: 216816   bits: 19/18
c ---[ 561]---> Adder-cost: 191   maxlim: 70139   bits: 18/17
c ---[ 559]---> Adder-cost: 1230   maxlim: 826322   bits: 21/20
c ---[ 557]---> Adder-cost: 1152   maxlim: 575183   bits: 20/20
c ---[ 555]---> Adder-cost: 390   maxlim: 79860   bits: 18/17
c ---[ 553]---> Adder-cost: 66   maxlim: 1280   bits: 12/11
c ---[ 551]---> Adder-cost: 60   maxlim: 640   bits: 11/10
c ---[ 549]---> Adder-cost: 98   maxlim: 768   bits: 11/10
c ---[ 547]---> Adder-cost: 69   maxlim: 256   bits: 10/9
c ---[ 545]---> Adder-cost: 66   maxlim: 1408   bits: 12/11
c ---[ 543]---> Adder-cost: 39   maxlim: 768   bits: 11/10
c ---[ 541]---> Adder-cost: 35   maxlim: 384   bits: 10/9
c ---[ 539]---> Adder-cost: 117   maxlim: 768   bits: 11/10
c ---[ 537]---> Adder-cost: 66   maxlim: 1920   bits: 12/11
c ---[ 535]---> Adder-cost: 124   maxlim: 384   bits: 10/9
c ---[ 533]---> Adder-cost: 93   maxlim: 128   bits: 9/8
c ---[ 531]---> Adder-cost: 98   maxlim: 512   bits: 11/10
c ---[ 529]---> Adder-cost: 43   maxlim: 1280   bits: 12/11
c ---[ 527]---> Adder-cost: 66   maxlim: 1408   bits: 12/11
c ---[ 525]---> Adder-cost: 117   maxlim: 768   bits: 11/10
c ---[ 523]---> Adder-cost: 117   maxlim: 640   bits: 11/10
c ---[ 521]---> Adder-cost: 60   maxlim: 640   bits: 11/10
c ---[ 519]---> Adder-cost: 54   maxlim: 256   bits: 10/9
c ---[ 517]---> Adder-cost: 93   maxlim: 3584   bits: 13/12
c ---[ 515]---> Adder-cost: 117   maxlim: 512   bits: 11/10
c ---[ 513]---> Adder-cost: 153   maxlim: 768   bits: 11/10
c ---[ 511]---> Adder-cost: 98   maxlim: 640   bits: 11/10
c ---[ 509]---> Adder-cost: 39   maxlim: 768   bits: 11/10
c ---[ 507]---> Adder-cost: 93   maxlim: 128   bits: 9/8
c ---[ 505]---> Adder-cost: 98   maxlim: 896   bits: 11/10
c ---[ 503]---> Adder-cost: 60   maxlim: 512   bits: 11/10
c ---[ 501]---> Adder-cost: 77   maxlim: 640   bits: 11/10
c ---[ 499]---> Adder-cost: 66   maxlim: 1408   bits: 12/11
c ---[ 497]---> Adder-cost: 88   maxlim: 384   bits: 10/9
c ---[ 495]---> Adder-cost: 85   maxlim: 1152   bits: 12/11
c ---[ 493]---> Adder-cost: 60   maxlim: 512   bits: 11/10
c ---[ 491]---> Adder-cost: 60   maxlim: 640   bits: 11/10
c ---[ 489]---> Adder-cost: 54   maxlim: 384   bits: 10/9
c ---[ 487]---> Adder-cost: 66   maxlim: 1152   bits: 12/11
c ---[ 485]---> Adder-cost: 60   maxlim: 640   bits: 11/10
c ---[ 483]---> Adder-cost: 93   maxlim: 128   bits: 9/8
c ---[ 481]---> Adder-cost: 77   maxlim: 512   bits: 11/10
c ---[ 479]---> Adder-cost: 98   maxlim: 640   bits: 11/10
c ---[ 477]---> Adder-cost: 93   maxlim: 2048   bits: 13/12
c ---[ 475]---> Adder-cost: 43   maxlim: 1152   bits: 12/11
c ---[ 473]---> Adder-cost: 60   maxlim: 896   bits: 11/10
c ---[ 471]---> Adder-cost: 152   maxlim: 1664   bits: 12/11
c ---[ 469]---> Adder-cost: 85   maxlim: 1024   bits: 12/11
c ---[ 467]---> Adder-cost: 117   maxlim: 512   bits: 11/10
c ---[ 465]---> Adder-cost: 117   maxlim: 640   bits: 11/10
c ---[ 463]---> Adder-cost: 108   maxlim: 1408   bits: 12/11
c ---[ 461]---> Adder-cost: 85   maxlim: 1536   bits: 12/11
c ---[ 459]---> Adder-cost: 105   maxlim: 384   bits: 10/9
c ---[ 457]---> Adder-cost: 77   maxlim: 640   bits: 11/10
c ---[ 455]---> Adder-cost: 98   maxlim: 512   bits: 11/10
c ---[ 453]---> Adder-cost: 85   maxlim: 1280   bits: 12/11
c ---[ 451]---> Adder-cost: 39   maxlim: 768   bits: 11/10
c ---[ 449]---> Adder-cost: 108   maxlim: 1024   bits: 12/11
c ---[ 447]---> Adder-cost: 60   maxlim: 768   bits: 11/10
c ---[ 445]---> Adder-cost: 60   maxlim: 768   bits: 11/10
c ---[ 443]---> Adder-cost: 60   maxlim: 768   bits: 11/10
c ---[ 441]---> Adder-cost: 18   maxlim: 256   bits: 10/9
c ---[ 439]---> Adder-cost: 78   maxlim: 128   bits: 9/8
c ---[ 437]---> Adder-cost: 60   maxlim: 512   bits: 11/10
c ---[ 435]---> Adder-cost: 69   maxlim: 256   bits: 10/9
c ---[ 433]---> Adder-cost: 192   maxlim: 1024   bits: 12/11
c ---[ 431]---> Adder-cost: 78   maxlim: 128   bits: 9/8
c ---[ 429]---> Adder-cost: 60   maxlim: 640   bits: 11/10
c ---[ 427]---> Adder-cost: 60   maxlim: 640   bits: 11/10
c ---[ 425]---> Adder-cost: 66   maxlim: 1280   bits: 12/11
c ---[ 423]---> Adder-cost: 98   maxlim: 896   bits: 11/10
c ---[ 421]---> Adder-cost: 88   maxlim: 384   bits: 10/9
c ---[ 419]---> Adder-cost: 117   maxlim: 896   bits: 11/10
c ---[ 417]---> Adder-cost: 54   maxlim: 384   bits: 10/9
c ---[ 415]---> Adder-cost: 98   maxlim: 512   bits: 11/10
c ---[ 413]---> Adder-cost: 60   maxlim: 896   bits: 11/10
c ---[ 411]---> Adder-cost: 66   maxlim: 1792   bits: 12/11
c ---[ 409]---> Adder-cost: 66   maxlim: 1152   bits: 12/11
c ---[ 407]---> Adder-cost: 98   maxlim: 768   bits: 11/10
c ---[ 405]---> Adder-cost: 98   maxlim: 640   bits: 11/10
c ---[ 403]---> Adder-cost: 85   maxlim: 1024   bits: 12/11
c ---[ 401]---> Adder-cost: 61   maxlim: 128   bits: 9/8
c ---[ 399]---> Adder-cost: 117   maxlim: 640   bits: 11/10
c ---[ 397]---> Adder-cost: 54   maxlim: 256   bits: 10/9
c ---[ 395]---> Adder-cost: 77   maxlim: 768   bits: 11/10
c ---[ 394]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 393]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 392]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 391]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 390]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 389]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 388]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 387]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 386]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 385]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 384]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 383]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 382]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 381]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 380]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 379]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 378]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 377]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 376]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 375]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 374]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 373]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 372]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 371]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 370]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 369]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 368]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 367]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 366]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 365]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[ 364]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 363]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 362]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 361]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 360]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 359]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 358]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 357]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 356]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 355]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 354]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 353]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 352]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 351]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 350]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 349]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 348]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 347]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 346]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 345]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 344]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 343]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 342]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 341]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 340]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 339]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 338]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 337]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 336]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 335]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 334]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 333]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 332]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 331]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 330]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 329]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 328]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 327]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 326]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 325]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[ 324]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 323]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 322]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 321]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 320]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 319]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 318]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 317]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 316]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 315]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 314]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 313]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 312]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 311]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 310]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 309]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 308]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 307]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 306]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 305]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 304]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 303]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 302]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 301]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 300]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 299]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 298]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 297]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 296]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 295]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 294]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 293]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 292]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 291]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 290]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 289]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 288]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 287]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 286]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 285]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 284]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 283]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 282]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 281]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 280]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 279]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 278]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 277]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 276]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 275]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 274]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 273]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 272]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 271]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 270]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 269]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 268]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 267]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 266]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 265]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 264]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 263]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 262]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 261]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 260]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 259]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 258]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 257]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 256]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 255]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 254]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 253]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 252]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 251]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 250]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 249]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 248]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 247]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 246]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 245]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 244]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 243]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 242]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 241]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 240]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 239]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 238]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 237]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 236]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 235]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 234]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 233]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 232]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 231]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 230]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 229]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 228]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 227]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 226]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 225]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 224]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 223]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 222]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 221]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 220]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 219]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 218]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 217]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 216]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 215]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 214]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 213]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 212]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 211]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 210]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 209]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 208]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 207]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 206]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 205]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 204]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 203]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 202]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 201]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 200]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 199]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 198]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 197]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 196]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 195]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 194]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 193]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 192]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[ 191]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 190]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 189]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 188]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 187]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 186]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 185]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 184]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 183]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 182]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 181]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 180]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 179]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 178]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 177]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 176]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 175]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 174]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 173]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 172]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 171]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 170]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 169]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 168]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 167]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 166]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 165]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 164]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 163]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 162]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 161]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 160]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 159]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 158]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 157]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 156]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 155]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 154]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 153]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 152]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 151]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 150]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 149]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 148]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 147]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 146]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 145]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 144]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[ 143]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 142]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 141]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 140]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 139]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 138]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 137]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 136]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 135]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 134]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 133]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 132]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 131]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 130]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 129]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 128]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[ 127]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 126]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 125]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 124]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 123]---> Adder-cost: 18   maxlim: 510   bits: 10/9
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: 18   maxlim: 510   bits: 10/9
c ---[ 118]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 117]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 116]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 115]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 114]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 113]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 112]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[ 111]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[ 110]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 109]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 108]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 107]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 106]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 105]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 104]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 103]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[ 102]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[ 101]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[ 100]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  99]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  98]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  97]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  96]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  95]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  94]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  93]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  92]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  91]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  90]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  89]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  88]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  87]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  86]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  85]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  84]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  83]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  82]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  81]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  80]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  79]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  78]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  77]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  76]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  75]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[  74]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  73]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  72]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  71]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  70]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  69]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  68]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  67]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  66]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  65]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  64]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  63]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  62]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  61]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  60]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  59]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  58]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  57]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  56]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  55]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  54]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  53]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  52]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  51]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  50]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  49]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  48]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  47]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  46]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  45]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  44]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  43]---> Adder-cost: 16   maxlim: 254   bits: 9/8
c ---[  42]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  41]---> Adder-cost: 24   maxlim: 4094   bits: 13/12
c ---[  40]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  39]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  38]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  37]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  36]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  35]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  34]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  33]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  32]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  31]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  30]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  29]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  28]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  27]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  26]---> Adder-cost: 18   maxlim: 510   bits: 10/9
c ---[  25]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[  24]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  23]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  22]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  21]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  20]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  19]---> Adder-cost: 20   maxlim: 1022   bits: 11/10
c ---[  18]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  17]---> Adder-cost: 22   maxlim: 2046   bits: 12/11
c ---[  16]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[  15]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[  14]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[  13]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[  12]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[  11]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[  10]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   9]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   8]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   7]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   6]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   5]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   4]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   3]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   2]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   1]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ---[   0]---> Adder-cost: 22   maxlim: 1534   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  181321   664173 |   60440       0        0     nan |  0.000 % |
c |       104 |  181321   664173 |   66484     104      689     6.6 | 26.171 % |
c |       254 |  181321   664173 |   73132     254     1258     5.0 | 26.171 % |
c |       479 |  181313   664147 |   80445     478     2635     5.5 | 26.174 % |
c |       816 |  181313   664147 |   88490     815     4343     5.3 | 26.174 % |
c |      1322 |  181313   664147 |   97339    1321    10523     8.0 | 26.174 % |
c |      2082 |  181269   664009 |  107073    2080    14450     6.9 | 26.197 % |
c |      3221 |  181269   664009 |  117780    3219    19579     6.1 | 26.197 % |
c |      4929 |  181261   663983 |  129558    4926    30033     6.1 | 26.199 % |
c |      7491 |  181253   663957 |  142514    7487    44125     5.9 | 26.202 % |
c |     11335 |  181237   663905 |  156765   11329    66064     5.8 | 26.207 % |
c |     17101 |  181237   663905 |  172442   17095   108102     6.3 | 26.207 % |
c |     25750 |  181221   663853 |  189686   25742   170512     6.6 | 26.211 % |
c |     38725 |  181205   663805 |  208655   38715   306439     7.9 | 26.218 % |
c |     58186 |  181197   663783 |  229520   58175   757654    13.0 | 26.223 % |
c |     87378 |  181189   663757 |  252472   87366  1115211    12.8 | 26.225 % |
c |    131167 |  181157   663653 |  277720  131150  2250067    17.2 | 26.235 % |
c |    196851 |  181133   663575 |  305492  196831  3244085    16.5 | 26.242 % |
c |    295377 |  181119   663531 |  336041  295355  8435151    28.6 | 26.246 % |
c |    443166 |  181071   663375 |  369645  130638  1749988    13.4 | 26.261 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.79 0.92 0.93 2/54 10642
Raw data (stat): 10642 (runsolver) R 10641 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547320345 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.82 0.93 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 4899 0 0 0 987 12 0 0 25 0 1 0 547320345 22507520 4679 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5495 4679 603 41 0 5454 0
vsize: 21980
[startup+20.0003 s]
Raw data (loadavg): 0.85 0.93 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 5030 0 0 0 1986 13 0 0 25 0 1 0 547320345 23085056 4810 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5636 4810 603 41 0 5595 0
vsize: 22544
[startup+30.0013 s]
Raw data (loadavg): 0.87 0.93 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 5129 0 0 0 2986 13 0 0 25 0 1 0 547320345 23355392 4909 4294967295 134512640 134672761 3221224544 3221223668 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5702 4909 603 41 0 5661 0
vsize: 22808
[startup+40.0009 s]
Raw data (loadavg): 0.89 0.93 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 5221 0 0 0 3985 14 0 0 25 0 1 0 547320345 23756800 5001 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5800 5001 603 41 0 5759 0
vsize: 23200
[startup+50.0011 s]
Raw data (loadavg): 0.91 0.93 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 5345 0 0 0 4984 15 0 0 25 0 1 0 547320345 24424448 5125 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5963 5125 603 41 0 5922 0
vsize: 23852
[startup+60.0011 s]
Raw data (loadavg): 0.92 0.94 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 5466 0 0 0 5983 16 0 0 25 0 1 0 547320345 24825856 5246 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6061 5246 603 41 0 6020 0
vsize: 24244
[startup+70.0017 s]
Raw data (loadavg): 0.93 0.94 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 5553 0 0 0 6983 17 0 0 25 0 1 0 547320345 25231360 5333 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6160 5333 603 41 0 6119 0
vsize: 24640
[startup+80.0019 s]
Raw data (loadavg): 0.94 0.94 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 5627 0 0 0 7982 17 0 0 25 0 1 0 547320345 25501696 5407 4294967295 134512640 134672761 3221224544 3221223668 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6226 5407 603 41 0 6185 0
vsize: 24904
[startup+90.0015 s]
Raw data (loadavg): 0.95 0.94 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 6113 0 0 0 8981 19 0 0 25 0 1 0 547320345 27394048 5893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6688 5893 603 41 0 6647 0
vsize: 26752
[startup+100.003 s]
Raw data (loadavg): 0.96 0.94 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 6219 0 0 0 9981 19 0 0 25 0 1 0 547320345 27803648 5999 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6788 5999 603 41 0 6747 0
vsize: 27152
[startup+110.003 s]
Raw data (loadavg): 0.96 0.94 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 6318 0 0 0 10980 20 0 0 25 0 1 0 547320345 28471296 6098 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6951 6098 603 41 0 6910 0
vsize: 27804
[startup+120.002 s]
Raw data (loadavg): 0.97 0.94 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 6404 0 0 0 11979 21 0 0 25 0 1 0 547320345 28876800 6184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7050 6184 603 41 0 7009 0
vsize: 28200
[startup+130.002 s]
Raw data (loadavg): 0.97 0.95 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 6516 0 0 0 12979 22 0 0 25 0 1 0 547320345 29282304 6296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7149 6296 603 41 0 7108 0
vsize: 28596
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 6648 0 0 0 13978 22 0 0 25 0 1 0 547320345 29822976 6428 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7281 6428 603 41 0 7240 0
vsize: 29124
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 6786 0 0 0 14978 23 0 0 25 0 1 0 547320345 30359552 6566 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7412 6566 603 41 0 7371 0
vsize: 29648
[startup+160.003 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 7068 0 0 0 15976 24 0 0 25 0 1 0 547320345 31436800 6848 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7675 6848 603 41 0 7634 0
vsize: 30700
[startup+170.002 s]
Raw data (loadavg): 0.98 0.95 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 7466 0 0 0 16975 26 0 0 25 0 1 0 547320345 33050624 7246 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8069 7246 603 41 0 8028 0
vsize: 32276
[startup+180.002 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 7804 0 0 0 17974 27 0 0 25 0 1 0 547320345 34398208 7584 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8398 7584 603 41 0 8357 0
vsize: 33592
[startup+190.003 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 7934 0 0 0 18974 27 0 0 25 0 1 0 547320345 34938880 7714 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8530 7714 603 41 0 8489 0
vsize: 34120
[startup+200.003 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 8012 0 0 0 19973 28 0 0 25 0 1 0 547320345 35205120 7792 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8595 7792 603 41 0 8554 0
vsize: 34380
[startup+210.003 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 8305 0 0 0 20972 29 0 0 25 0 1 0 547320345 36417536 8085 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8891 8085 603 41 0 8850 0
vsize: 35564
[startup+220.003 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 8358 0 0 0 21971 30 0 0 25 0 1 0 547320345 36552704 8138 4294967295 134512640 134672761 3221224544 3221223696 134565094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8924 8138 603 41 0 8883 0
vsize: 35696
[startup+230.003 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 8409 0 0 0 22970 31 0 0 25 0 1 0 547320345 36818944 8189 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8989 8189 603 41 0 8948 0
vsize: 35956
[startup+240.003 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 8465 0 0 0 23970 31 0 0 25 0 1 0 547320345 37478400 8245 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9150 8245 603 41 0 9109 0
vsize: 36600
[startup+250.003 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 8512 0 0 0 24970 31 0 0 25 0 1 0 547320345 37748736 8292 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9216 8292 603 41 0 9175 0
vsize: 36864
[startup+260.004 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 8777 0 0 0 25969 32 0 0 25 0 1 0 547320345 38830080 8557 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9480 8557 603 41 0 9439 0
vsize: 37920
[startup+270.003 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 8834 0 0 0 26969 32 0 0 25 0 1 0 547320345 38961152 8614 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9512 8614 603 41 0 9471 0
vsize: 38048
[startup+280.003 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 9067 0 0 0 27969 33 0 0 25 0 1 0 547320345 39907328 8847 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9743 8847 603 41 0 9702 0
vsize: 38972
[startup+290.003 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 9192 0 0 0 28969 33 0 0 25 0 1 0 547320345 40448000 8972 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9875 8972 603 41 0 9834 0
vsize: 39500
[startup+300.003 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 9263 0 0 0 29969 33 0 0 25 0 1 0 547320345 40718336 9043 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9941 9043 603 41 0 9900 0
vsize: 39764
[startup+310.003 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 9434 0 0 0 30969 34 0 0 25 0 1 0 547320345 41394176 9214 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10106 9214 603 41 0 10065 0
vsize: 40424
[startup+320.002 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 9660 0 0 0 31968 34 0 0 25 0 1 0 547320345 42340352 9440 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10337 9440 603 41 0 10296 0
vsize: 41348
[startup+330.003 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 9764 0 0 0 32968 34 0 0 25 0 1 0 547320345 42745856 9544 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10436 9544 603 41 0 10395 0
vsize: 41744
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 9839 0 0 0 33968 35 0 0 25 0 1 0 547320345 43016192 9619 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10502 9619 603 41 0 10461 0
vsize: 42008
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 9899 0 0 0 34968 35 0 0 25 0 1 0 547320345 43151360 9679 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10535 9679 603 41 0 10494 0
vsize: 42140
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 9954 0 0 0 35968 35 0 0 25 0 1 0 547320345 43421696 9734 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10601 9734 603 41 0 10560 0
vsize: 42404
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 10018 0 0 0 36968 35 0 0 25 0 1 0 547320345 43692032 9798 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10667 9798 603 41 0 10626 0
vsize: 42668
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 10099 0 0 0 37968 35 0 0 25 0 1 0 547320345 43958272 9879 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10732 9879 603 41 0 10691 0
vsize: 42928
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 10215 0 0 0 38968 35 0 0 25 0 1 0 547320345 44498944 9995 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10864 9995 603 41 0 10823 0
vsize: 43456
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 10556 0 0 0 39967 36 0 0 25 0 1 0 547320345 45838336 10336 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11191 10336 603 41 0 11150 0
vsize: 44764
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 10645 0 0 0 40967 37 0 0 25 0 1 0 547320345 46108672 10425 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11257 10425 603 41 0 11216 0
vsize: 45028
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 10726 0 0 0 41967 37 0 0 25 0 1 0 547320345 46514176 10506 4294967295 134512640 134672761 3221224544 3221223712 134561415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11356 10506 603 41 0 11315 0
vsize: 45424
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 10796 0 0 0 42967 37 0 0 25 0 1 0 547320345 46784512 10576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11422 10576 603 41 0 11381 0
vsize: 45688
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 10881 0 0 0 43966 38 0 0 25 0 1 0 547320345 47054848 10661 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11488 10661 603 41 0 11447 0
vsize: 45952
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 11076 0 0 0 44966 38 0 0 25 0 1 0 547320345 47865856 10856 4294967295 134512640 134672761 3221224544 3221223712 134564689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11686 10856 603 41 0 11645 0
vsize: 46744
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 11178 0 0 0 45966 39 0 0 25 0 1 0 547320345 48267264 10958 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11784 10958 603 41 0 11743 0
vsize: 47136
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 11632 0 0 0 46965 40 0 0 25 0 1 0 547320345 50016256 11412 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12211 11412 603 41 0 12170 0
vsize: 48844
[startup+480.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 11705 0 0 0 47964 40 0 0 25 0 1 0 547320345 50421760 11485 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12310 11485 603 41 0 12269 0
vsize: 49240
[startup+490.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 11772 0 0 0 48964 41 0 0 25 0 1 0 547320345 50692096 11552 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11552 603 41 0 12335 0
vsize: 49504
[startup+500.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 11840 0 0 0 49964 41 0 0 25 0 1 0 547320345 50962432 11620 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12442 11620 603 41 0 12401 0
vsize: 49768
[startup+510.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 12148 0 0 0 50963 42 0 0 25 0 1 0 547320345 52178944 11928 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12739 11928 603 41 0 12698 0
vsize: 50956
[startup+520 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 12994 0 0 0 51961 44 0 0 25 0 1 0 547320345 56582144 12774 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13814 12774 603 41 0 13773 0
vsize: 55256
[startup+530.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 13702 0 0 0 52960 46 0 0 25 0 1 0 547320345 59424768 13482 4294967295 134512640 134672761 3221224544 3221223648 134555091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14508 13482 603 41 0 14467 0
vsize: 58032
[startup+540.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 14322 0 0 0 53958 48 0 0 25 0 1 0 547320345 61997056 14102 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15136 14102 603 41 0 15095 0
vsize: 60544
[startup+550.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 14918 0 0 0 54957 49 0 0 25 0 1 0 547320345 64450560 14698 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15735 14698 603 41 0 15694 0
vsize: 62940
[startup+560.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 15417 0 0 0 55956 51 0 0 25 0 1 0 547320345 66506752 15197 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16237 15197 603 41 0 16196 0
vsize: 64948
[startup+570.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 15912 0 0 0 56954 52 0 0 25 0 1 0 547320345 68526080 15692 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16730 15692 603 41 0 16689 0
vsize: 66920
[startup+580.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 16381 0 0 0 57953 53 0 0 25 0 1 0 547320345 70414336 16161 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17191 16161 603 41 0 17150 0
vsize: 68764
[startup+590.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 16457 0 0 0 58952 54 0 0 25 0 1 0 547320345 70819840 16237 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17290 16237 603 41 0 17249 0
vsize: 69160
[startup+600.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 16510 0 0 0 59952 54 0 0 25 0 1 0 547320345 70955008 16290 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17323 16290 603 41 0 17282 0
vsize: 69292
[startup+610.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 16565 0 0 0 60952 54 0 0 25 0 1 0 547320345 71225344 16345 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17389 16345 603 41 0 17348 0
vsize: 69556
[startup+620.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 16611 0 0 0 61952 54 0 0 25 0 1 0 547320345 71360512 16391 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17422 16391 603 41 0 17381 0
vsize: 69688
[startup+630.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 16657 0 0 0 62952 54 0 0 25 0 1 0 547320345 71495680 16437 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17455 16437 603 41 0 17414 0
vsize: 69820
[startup+640.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 16728 0 0 0 63952 55 0 0 25 0 1 0 547320345 71761920 16508 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17520 16508 603 41 0 17479 0
vsize: 70080
[startup+650.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 16795 0 0 0 64952 55 0 0 25 0 1 0 547320345 72032256 16575 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17586 16575 603 41 0 17545 0
vsize: 70344
[startup+660.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 16860 0 0 0 65951 56 0 0 25 0 1 0 547320345 72302592 16640 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17652 16640 603 41 0 17611 0
vsize: 70608
[startup+670.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 16918 0 0 0 66951 56 0 0 25 0 1 0 547320345 72572928 16698 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17718 16698 603 41 0 17677 0
vsize: 70872
[startup+680.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 16990 0 0 0 67951 56 0 0 25 0 1 0 547320345 72843264 16770 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17784 16770 603 41 0 17743 0
vsize: 71136
[startup+690.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17033 0 0 0 68951 57 0 0 25 0 1 0 547320345 72978432 16813 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17817 16813 603 41 0 17776 0
vsize: 71268
[startup+700.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17079 0 0 0 69951 57 0 0 25 0 1 0 547320345 73248768 16859 4294967295 134512640 134672761 3221224544 3221223668 134565980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17883 16859 603 41 0 17842 0
vsize: 71532
[startup+710.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17131 0 0 0 70951 57 0 0 25 0 1 0 547320345 73379840 16911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17915 16911 603 41 0 17874 0
vsize: 71660
[startup+720.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17173 0 0 0 71951 57 0 0 25 0 1 0 547320345 73515008 16953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17948 16953 603 41 0 17907 0
vsize: 71792
[startup+730.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17226 0 0 0 72951 57 0 0 25 0 1 0 547320345 73789440 17006 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18015 17006 603 41 0 17974 0
vsize: 72060
[startup+740.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17287 0 0 0 73951 58 0 0 25 0 1 0 547320345 74055680 17067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18080 17067 603 41 0 18039 0
vsize: 72320
[startup+750.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17335 0 0 0 74951 58 0 0 25 0 1 0 547320345 74190848 17115 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18113 17115 603 41 0 18072 0
vsize: 72452
[startup+760.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17400 0 0 0 75951 58 0 0 25 0 1 0 547320345 74461184 17180 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18179 17180 603 41 0 18138 0
vsize: 72716
[startup+770.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17458 0 0 0 76950 59 0 0 25 0 1 0 547320345 74731520 17238 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18245 17238 603 41 0 18204 0
vsize: 72980
[startup+780.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17527 0 0 0 77950 59 0 0 25 0 1 0 547320345 75001856 17307 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18311 17307 603 41 0 18270 0
vsize: 73244
[startup+790.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17614 0 0 0 78950 59 0 0 25 0 1 0 547320345 75268096 17394 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18376 17394 603 41 0 18335 0
vsize: 73504
[startup+800.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 79950 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+810.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 80950 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+820.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 81950 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+830.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 82951 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+840.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 83951 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+850.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 84951 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+860.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 85951 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+870.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 86951 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+880.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 87952 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+890.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 88952 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+900.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 89952 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+910.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 90952 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+920.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 91952 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+930.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 92952 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+940.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 93952 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+950.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 94953 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+960.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 95953 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+970.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 96953 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134564738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+980.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 97953 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+990.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 98953 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 99954 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 100954 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 101954 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 102954 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 103954 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 104954 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 105954 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 106954 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 107954 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 108955 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 109955 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 110955 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 111955 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 112956 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1140 s]
Raw data (loadavg): 1.15 1.00 0.94 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17662 0 0 0 113956 60 0 0 25 0 1 0 547320345 75534336 17442 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17442 603 41 0 18400 0
vsize: 73764
[startup+1150 s]
Raw data (loadavg): 1.12 1.00 0.94 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17663 0 0 0 114956 60 0 0 25 0 1 0 547320345 75534336 17443 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17443 603 41 0 18400 0
vsize: 73764
[startup+1160 s]
Raw data (loadavg): 1.10 1.00 0.94 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17663 0 0 0 115956 60 0 0 25 0 1 0 547320345 75534336 17443 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17443 603 41 0 18400 0
vsize: 73764
[startup+1170 s]
Raw data (loadavg): 1.09 1.00 0.94 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17663 0 0 0 116956 60 0 0 25 0 1 0 547320345 75534336 17443 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17443 603 41 0 18400 0
vsize: 73764
[startup+1180 s]
Raw data (loadavg): 1.07 1.00 0.94 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17663 0 0 0 117957 60 0 0 25 0 1 0 547320345 75534336 17443 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17443 603 41 0 18400 0
vsize: 73764
[startup+1190 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17663 0 0 0 118957 60 0 0 25 0 1 0 547320345 75534336 17443 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17443 603 41 0 18400 0
vsize: 73764
[startup+1200.01 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 10642
Raw data (stat): 10642 (minisat+) R 10641 28099 28098 0 -1 0 17663 0 0 0 119957 60 0 0 25 0 1 0 547320345 75534336 17443 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18441 17443 603 41 0 18400 0
vsize: 73764
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.05 1.00 0.94 1/54 10642
Raw data (stat): 10642 (minisat+) Z 10641 28099 28098 0 -1 12 17665 0 0 0 119957 63 0 0 25 0 1 0 547320345 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: 0
Real time (s): 1200.04
CPU time (s): 1200.21
CPU user time (s): 1199.58
CPU system time (s): 0.637903
CPU usage (%): 100.015
Max. virtual memory (Kb): 73764
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####