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-fixnet4.opb
MD5SUM	c6a26aa8aefc43a120ecaff31b506c53
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4227509
Optimality of the best value was proved	NO
Number of terms in the objective function	9638
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	2427493442
Number of bits of the sum of numbers in the objective function	32
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	2427493442
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.06
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 19233

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-21 18:24:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16832 boxname=wulflinc26 idbench=1295 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c6a26aa8aefc43a120ecaff31b506c53  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-fixnet4.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-fixnet4.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-fixnet4.opb
IDLAUNCH: 16832
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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:        619272 kB
Buffers:         32580 kB
Cached:         354884 kB
SwapCached:         68 kB
Active:          77788 kB
Inactive:       312576 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        619020 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6880 kB
Slab:            19408 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:44:32 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 16832 7 1200.18 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     1257     4.9 | 26.171 % |
c |       479 |  181321   664173 |   80445     479     3996     8.3 | 26.171 % |
c |       816 |  181321   664173 |   88490     816     5866     7.2 | 26.171 % |
c |      1324 |  181321   664173 |   97339    1324     7943     6.0 | 26.171 % |
c |      2083 |  181321   664173 |  107073    2083    11778     5.7 | 26.171 % |
c |      3222 |  181321   664173 |  117780    3222    18101     5.6 | 26.171 % |
c |      4930 |  181261   663983 |  129558    4927    28338     5.8 | 26.199 % |
c |      7492 |  181247   663939 |  142514    7487    43500     5.8 | 26.204 % |
c |     11336 |  181239   663913 |  156765   11330    67587     6.0 | 26.207 % |
c |     17102 |  181223   663861 |  172442   17094   103797     6.1 | 26.211 % |
c |     25751 |  181215   663835 |  189686   25742   165445     6.4 | 26.214 % |
c |     38728 |  181207   663813 |  208655   38718   326389     8.4 | 26.218 % |
c |     58189 |  181175   663709 |  229520   58175   487738     8.4 | 26.228 % |
c |     87381 |  181167   663683 |  252472   87366  1920472    22.0 | 26.230 % |
c |    131171 |  181127   663557 |  277720  131151  2514069    19.2 | 26.244 % |
c |    196855 |  181111   663505 |  305492  196833  3789703    19.3 | 26.249 % |
c |    295382 |  181071   663375 |  336041  295355  5292056    17.9 | 26.261 % |
c |    443171 |  181071   663375 |  369645  121340  1779018    14.7 | 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.73 0.92 0.91 2/54 4102
Raw data (stat): 4102 (runsolver) R 4101 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547222770 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+9.99928 s]
Raw data (loadavg): 0.77 0.92 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 4885 0 0 0 986 12 0 0 25 0 1 0 547222770 22368256 4665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5461 4665 603 41 0 5420 0
vsize: 21844
[startup+20.0004 s]
Raw data (loadavg): 0.81 0.93 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 5008 0 0 0 1986 12 0 0 25 0 1 0 547222770 22908928 4788 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5593 4788 603 41 0 5552 0
vsize: 22372
[startup+30.0011 s]
Raw data (loadavg): 0.84 0.93 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 5113 0 0 0 2986 13 0 0 25 0 1 0 547222770 23339008 4893 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5698 4893 603 41 0 5657 0
vsize: 22792
[startup+40.0013 s]
Raw data (loadavg): 0.86 0.93 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 5201 0 0 0 3985 13 0 0 25 0 1 0 547222770 23744512 4981 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5797 4981 603 41 0 5756 0
vsize: 23188
[startup+50.0024 s]
Raw data (loadavg): 0.88 0.93 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 5292 0 0 0 4984 14 0 0 25 0 1 0 547222770 24014848 5072 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5863 5072 603 41 0 5822 0
vsize: 23452
[startup+60.0021 s]
Raw data (loadavg): 0.90 0.93 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 5481 0 0 0 5982 16 0 0 25 0 1 0 547222770 24948736 5261 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6091 5261 603 41 0 6050 0
vsize: 24364
[startup+70.0024 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 5560 0 0 0 6982 16 0 0 25 0 1 0 547222770 25219072 5340 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6157 5340 603 41 0 6116 0
vsize: 24628
[startup+80.0025 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 5629 0 0 0 7982 17 0 0 25 0 1 0 547222770 25485312 5409 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6222 5409 603 41 0 6181 0
vsize: 24888
[startup+90.0032 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 5727 0 0 0 8981 18 0 0 25 0 1 0 547222770 25886720 5507 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6320 5507 603 41 0 6279 0
vsize: 25280
[startup+100.003 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 5808 0 0 0 9981 18 0 0 25 0 1 0 547222770 26157056 5588 4294967295 134512640 134672761 3221224544 3221223668 134566007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5588 603 41 0 6345 0
vsize: 25544
[startup+110.004 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 5888 0 0 0 10980 19 0 0 25 0 1 0 547222770 26427392 5668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6452 5668 603 41 0 6411 0
vsize: 25808
[startup+120.004 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 6243 0 0 0 11979 20 0 0 25 0 1 0 547222770 28172288 6023 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6878 6023 603 41 0 6837 0
vsize: 27512
[startup+130.004 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 7116 0 0 0 12977 23 0 0 25 0 1 0 547222770 31682560 6896 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7735 6896 603 41 0 7694 0
vsize: 30940
[startup+140.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 7582 0 0 0 13975 24 0 0 25 0 1 0 547222770 33583104 7362 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8199 7362 603 41 0 8158 0
vsize: 32796
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 7656 0 0 0 14975 25 0 0 25 0 1 0 547222770 33853440 7436 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8265 7436 603 41 0 8224 0
vsize: 33060
[startup+160.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 7715 0 0 0 15974 25 0 0 25 0 1 0 547222770 34123776 7495 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8331 7495 603 41 0 8290 0
vsize: 33324
[startup+170.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 7784 0 0 0 16974 26 0 0 25 0 1 0 547222770 34394112 7564 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8397 7564 603 41 0 8356 0
vsize: 33588
[startup+180.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8062 0 0 0 17972 27 0 0 25 0 1 0 547222770 35475456 7842 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8661 7842 603 41 0 8620 0
vsize: 34644
[startup+190.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8147 0 0 0 18972 28 0 0 25 0 1 0 547222770 35885056 7927 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8761 7927 603 41 0 8720 0
vsize: 35044
[startup+200.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8315 0 0 0 19971 29 0 0 25 0 1 0 547222770 36425728 8095 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8893 8095 603 41 0 8852 0
vsize: 35572
[startup+210.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8363 0 0 0 20971 29 0 0 25 0 1 0 547222770 36696064 8143 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8959 8143 603 41 0 8918 0
vsize: 35836
[startup+220.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8431 0 0 0 21970 30 0 0 25 0 1 0 547222770 36966400 8211 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9025 8211 603 41 0 8984 0
vsize: 36100
[startup+230.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8543 0 0 0 22970 31 0 0 25 0 1 0 547222770 37371904 8323 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9124 8323 603 41 0 9083 0
vsize: 36496
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8603 0 0 0 23969 31 0 0 25 0 1 0 547222770 37642240 8383 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9190 8383 603 41 0 9149 0
vsize: 36760
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8679 0 0 0 24969 31 0 0 25 0 1 0 547222770 38436864 8459 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9384 8459 603 41 0 9343 0
vsize: 37536
[startup+260.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8719 0 0 0 25969 32 0 0 25 0 1 0 547222770 38572032 8499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9417 8499 603 41 0 9376 0
vsize: 37668
[startup+270.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8787 0 0 0 26969 32 0 0 25 0 1 0 547222770 38842368 8567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9483 8567 603 41 0 9442 0
vsize: 37932
[startup+280.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8840 0 0 0 27968 33 0 0 25 0 1 0 547222770 39108608 8620 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9548 8620 603 41 0 9507 0
vsize: 38192
[startup+290.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8890 0 0 0 28967 33 0 0 25 0 1 0 547222770 39239680 8670 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9580 8670 603 41 0 9539 0
vsize: 38320
[startup+300.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 8951 0 0 0 29967 34 0 0 25 0 1 0 547222770 39510016 8731 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9646 8731 603 41 0 9605 0
vsize: 38584
[startup+310.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 9304 0 0 0 30965 36 0 0 25 0 1 0 547222770 40857600 9084 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9975 9084 603 41 0 9934 0
vsize: 39900
[startup+320.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 9363 0 0 0 31965 36 0 0 25 0 1 0 547222770 41127936 9143 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10041 9143 603 41 0 10000 0
vsize: 40164
[startup+330.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 9417 0 0 0 32964 37 0 0 25 0 1 0 547222770 41398272 9197 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10107 9197 603 41 0 10066 0
vsize: 40428
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 9465 0 0 0 33964 38 0 0 25 0 1 0 547222770 41533440 9245 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10140 9245 603 41 0 10099 0
vsize: 40560
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 9501 0 0 0 34963 38 0 0 25 0 1 0 547222770 41668608 9281 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10173 9281 603 41 0 10132 0
vsize: 40692
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 9556 0 0 0 35963 38 0 0 25 0 1 0 547222770 41803776 9336 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10206 9336 603 41 0 10165 0
vsize: 40824
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 9610 0 0 0 36963 39 0 0 25 0 1 0 547222770 42074112 9390 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10272 9390 603 41 0 10231 0
vsize: 41088
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 9669 0 0 0 37962 39 0 0 25 0 1 0 547222770 42344448 9449 4294967295 134512640 134672761 3221224544 3221223712 134564767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10338 9449 603 41 0 10297 0
vsize: 41352
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 9765 0 0 0 38962 40 0 0 25 0 1 0 547222770 42745856 9545 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10436 9545 603 41 0 10395 0
vsize: 41744
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 10526 0 0 0 39959 43 0 0 25 0 1 0 547222770 45707264 10306 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11159 10306 603 41 0 11118 0
vsize: 44636
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 10591 0 0 0 40959 43 0 0 25 0 1 0 547222770 45977600 10371 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11225 10371 603 41 0 11184 0
vsize: 44900
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 10642 0 0 0 41958 44 0 0 25 0 1 0 547222770 46247936 10422 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11291 10422 603 41 0 11250 0
vsize: 45164
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 10704 0 0 0 42958 44 0 0 25 0 1 0 547222770 46383104 10484 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11324 10484 603 41 0 11283 0
vsize: 45296
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 10744 0 0 0 43958 45 0 0 25 0 1 0 547222770 46653440 10524 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11390 10524 603 41 0 11349 0
vsize: 45560
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 10797 0 0 0 44957 46 0 0 25 0 1 0 547222770 46788608 10577 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11423 10577 603 41 0 11382 0
vsize: 45692
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 10847 0 0 0 45957 46 0 0 25 0 1 0 547222770 47054848 10627 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11488 10627 603 41 0 11447 0
vsize: 45952
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 10893 0 0 0 46957 47 0 0 25 0 1 0 547222770 47190016 10673 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11521 10673 603 41 0 11480 0
vsize: 46084
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 10947 0 0 0 47956 47 0 0 25 0 1 0 547222770 47321088 10727 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11553 10727 603 41 0 11512 0
vsize: 46212
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 11013 0 0 0 48956 47 0 0 25 0 1 0 547222770 47591424 10793 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11619 10793 603 41 0 11578 0
vsize: 46476
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 11072 0 0 0 49956 48 0 0 25 0 1 0 547222770 47861760 10852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11685 10852 603 41 0 11644 0
vsize: 46740
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 11129 0 0 0 50955 48 0 0 25 0 1 0 547222770 48128000 10909 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11750 10909 603 41 0 11709 0
vsize: 47000
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 11189 0 0 0 51955 49 0 0 25 0 1 0 547222770 48259072 10969 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 11254 0 0 0 52955 49 0 0 25 0 1 0 547222770 48529408 11034 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11848 11034 603 41 0 11807 0
vsize: 47392
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 11310 0 0 0 53954 50 0 0 25 0 1 0 547222770 48795648 11090 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11913 11090 603 41 0 11872 0
vsize: 47652
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 11534 0 0 0 54954 50 0 0 25 0 1 0 547222770 49741824 11314 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12144 11314 603 41 0 12103 0
vsize: 48576
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 11681 0 0 0 55953 51 0 0 25 0 1 0 547222770 50282496 11461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12276 11461 603 41 0 12235 0
vsize: 49104
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 11770 0 0 0 56953 52 0 0 25 0 1 0 547222770 50552832 11550 4294967295 134512640 134672761 3221224544 3221223712 134561415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12342 11550 603 41 0 12301 0
vsize: 49368
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 11857 0 0 0 57952 52 0 0 25 0 1 0 547222770 50954240 11637 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12440 11637 603 41 0 12399 0
vsize: 49760
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 11969 0 0 0 58952 53 0 0 25 0 1 0 547222770 51355648 11749 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12538 11749 603 41 0 12497 0
vsize: 50152
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 12037 0 0 0 59951 54 0 0 25 0 1 0 547222770 51625984 11817 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12604 11817 603 41 0 12563 0
vsize: 50416
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 12148 0 0 0 60951 54 0 0 25 0 1 0 547222770 52031488 11928 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12703 11928 603 41 0 12662 0
vsize: 50812
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 12262 0 0 0 61950 55 0 0 25 0 1 0 547222770 53616640 12042 4294967295 134512640 134672761 3221224544 3221223728 134558957 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13090 12042 603 41 0 13049 0
vsize: 52360
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 12369 0 0 0 62950 56 0 0 25 0 1 0 547222770 54022144 12149 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13189 12149 603 41 0 13148 0
vsize: 52756
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 12480 0 0 0 63949 57 0 0 25 0 1 0 547222770 54427648 12260 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13288 12260 603 41 0 13247 0
vsize: 53152
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 12550 0 0 0 64949 57 0 0 25 0 1 0 547222770 54697984 12330 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13354 12330 603 41 0 13313 0
vsize: 53416
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 12619 0 0 0 65948 57 0 0 25 0 1 0 547222770 54968320 12399 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13420 12399 603 41 0 13379 0
vsize: 53680
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 12740 0 0 0 66948 58 0 0 25 0 1 0 547222770 55504896 12520 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13551 12520 603 41 0 13510 0
vsize: 54204
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 12950 0 0 0 67946 59 0 0 25 0 1 0 547222770 56315904 12730 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13749 12730 603 41 0 13708 0
vsize: 54996
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 13267 0 0 0 68945 61 0 0 25 0 1 0 547222770 57528320 13047 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14045 13047 603 41 0 14004 0
vsize: 56180
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 13427 0 0 0 69944 62 0 0 25 0 1 0 547222770 58200064 13207 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14209 13207 603 41 0 14168 0
vsize: 56836
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 13546 0 0 0 70944 62 0 0 25 0 1 0 547222770 58740736 13326 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14341 13326 603 41 0 14300 0
vsize: 57364
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 13683 0 0 0 71943 64 0 0 25 0 1 0 547222770 59281408 13463 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14473 13463 603 41 0 14432 0
vsize: 57892
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 14409 0 0 0 72941 66 0 0 25 0 1 0 547222770 62107648 14189 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15163 14189 603 41 0 15122 0
vsize: 60652
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 15452 0 0 0 73939 68 0 0 25 0 1 0 547222770 66416640 15232 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16215 15232 603 41 0 16174 0
vsize: 64860
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 16415 0 0 0 74935 72 0 0 25 0 1 0 547222770 70295552 16195 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17162 16195 603 41 0 17121 0
vsize: 68648
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 17290 0 0 0 75934 73 0 0 25 0 1 0 547222770 73961472 17070 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18057 17070 603 41 0 18016 0
vsize: 72228
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 17760 0 0 0 76932 75 0 0 25 0 1 0 547222770 75874304 17540 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18524 17540 603 41 0 18483 0
vsize: 74096
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18147 0 0 0 77930 77 0 0 25 0 1 0 547222770 77488128 17927 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18918 17927 603 41 0 18877 0
vsize: 75672
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 78929 78 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223652 134554691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 79929 79 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 80929 79 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 81929 79 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223728 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+830.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 82928 80 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 83928 80 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 84928 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 85928 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 86928 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 87928 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 88928 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 89928 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 90929 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 91929 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 92929 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 93929 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+950.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 94929 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560770 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 95929 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 96930 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 97930 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 98930 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 99930 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 100930 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 101930 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 102931 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 103931 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223668 134566133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 104930 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 105930 81 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 106930 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223648 134555314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 107929 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 108930 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 109930 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 110930 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 111930 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 112930 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 113930 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 114931 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 115931 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 116931 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 117931 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 118931 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4102
Raw data (stat): 4102 (minisat+) R 4101 22612 22611 0 -1 0 18647 0 0 0 119931 82 0 0 25 0 1 0 547222770 79503360 18427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19410 18427 603 41 0 19369 0
vsize: 77640
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4102
Raw data (stat): 4102 (minisat+) Z 4101 22612 22611 0 -1 12 18649 0 0 0 119932 86 0 0 25 0 1 0 547222770 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.06
CPU time (s): 1200.18
CPU user time (s): 1199.32
CPU system time (s): 0.862868
CPU usage (%): 100.01
Max. virtual memory (Kb): 77640
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####