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-fixnet6.opb
MD5SUM	1b379137169731592d0d61cac8bf57af
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5123480
Optimality of the best value was proved	NO
Number of terms in the objective function	8282
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	524133752
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	524133752
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1243.61
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 19224

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        372024 kB
Buffers:         35812 kB
Cached:         603960 kB
SwapCached:        176 kB
Active:         275764 kB
Inactive:       366788 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        371772 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            14372 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:43:31 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 16845 7 1200.23 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     1302     5.1 | 26.171 % |
c |       479 |  181277   664035 |   80445     478     2491     5.2 | 26.195 % |
c |       816 |  181263   663991 |   88490     813     3951     4.9 | 26.199 % |
c |      1322 |  181263   663991 |   97339    1319     6767     5.1 | 26.199 % |
c |      2081 |  181263   663991 |  107073    2078    10750     5.2 | 26.199 % |
c |      3220 |  181263   663991 |  117780    3217    16788     5.2 | 26.199 % |
c |      4928 |  181257   663973 |  129558    4924    25733     5.2 | 26.202 % |
c |      7490 |  181249   663947 |  142514    7485    48732     6.5 | 26.204 % |
c |     11334 |  181241   663921 |  156765   11328    72364     6.4 | 26.207 % |
c |     17100 |  181225   663869 |  172442   17092   109302     6.4 | 26.211 % |
c |     25749 |  181201   663791 |  189686   25738   167475     6.5 | 26.218 % |
c |     38723 |  181193   663769 |  208655   38711   289478     7.5 | 26.223 % |
c |     58184 |  181169   663695 |  229520   58169   518644     8.9 | 26.232 % |
c |     87376 |  181161   663669 |  252472   87360   790489     9.0 | 26.235 % |
c |    131165 |  181137   663591 |  277720  131146  1791074    13.7 | 26.242 % |
c |    196850 |  181097   663461 |  305492  196826  2777506    14.1 | 26.253 % |
c |    295377 |  181065   663357 |  336041  295349  4801067    16.3 | 26.263 % |
c |    443167 |  181065   663357 |  369645  114627  1745173    15.2 | 26.263 % |
#### 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.66 0.86 0.88 2/54 22709
Raw data (stat): 22709 (runsolver) R 22708 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488994439 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99991 s]
Raw data (loadavg): 0.71 0.86 0.88 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 4918 0 0 0 985 12 0 0 25 0 1 0 488994439 22564864 4698 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5509 4698 603 41 0 5468 0
vsize: 22036
[startup+20.0002 s]
Raw data (loadavg): 0.76 0.87 0.88 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 5038 0 0 0 1984 13 0 0 25 0 1 0 488994439 23121920 4818 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5645 4818 603 41 0 5604 0
vsize: 22580
[startup+30.0002 s]
Raw data (loadavg): 0.79 0.87 0.88 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 5128 0 0 0 2982 14 0 0 25 0 1 0 488994439 23392256 4908 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5711 4908 603 41 0 5670 0
vsize: 22844
[startup+39.9998 s]
Raw data (loadavg): 0.83 0.87 0.88 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 5212 0 0 0 3982 15 0 0 25 0 1 0 488994439 23797760 4992 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5810 4992 603 41 0 5769 0
vsize: 23240
[startup+50.0009 s]
Raw data (loadavg): 0.85 0.88 0.88 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 5363 0 0 0 4982 16 0 0 25 0 1 0 488994439 24461312 5143 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5972 5143 603 41 0 5931 0
vsize: 23888
[startup+60.0012 s]
Raw data (loadavg): 0.87 0.88 0.88 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 5477 0 0 0 5981 16 0 0 25 0 1 0 488994439 24866816 5257 4294967295 134512640 134672761 3221224544 3221223696 134565132 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6071 5257 603 41 0 6030 0
vsize: 24284
[startup+70.0012 s]
Raw data (loadavg): 0.89 0.89 0.89 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 5557 0 0 0 6981 16 0 0 25 0 1 0 488994439 25272320 5337 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6170 5337 603 41 0 6129 0
vsize: 24680
[startup+80.0018 s]
Raw data (loadavg): 0.91 0.89 0.89 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 5739 0 0 0 7981 17 0 0 25 0 1 0 488994439 25948160 5519 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6335 5519 603 41 0 6294 0
vsize: 25340
[startup+90.0011 s]
Raw data (loadavg): 0.92 0.89 0.89 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 5869 0 0 0 8980 17 0 0 25 0 1 0 488994439 26484736 5649 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6466 5649 603 41 0 6425 0
vsize: 25864
[startup+100.002 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 5945 0 0 0 9980 18 0 0 25 0 1 0 488994439 26755072 5725 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6532 5725 603 41 0 6491 0
vsize: 26128
[startup+110.003 s]
Raw data (loadavg): 0.94 0.90 0.89 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 6057 0 0 0 10980 18 0 0 25 0 1 0 488994439 27418624 5837 4294967295 134512640 134672761 3221224544 3221223780 134564645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6694 5837 603 41 0 6653 0
vsize: 26776
[startup+120.003 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 6156 0 0 0 11980 18 0 0 25 0 1 0 488994439 27824128 5936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6793 5936 603 41 0 6752 0
vsize: 27172
[startup+130.003 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 6232 0 0 0 12980 18 0 0 25 0 1 0 488994439 28094464 6012 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6859 6012 603 41 0 6818 0
vsize: 27436
[startup+140.003 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 6327 0 0 0 13980 19 0 0 25 0 1 0 488994439 28495872 6107 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6957 6107 603 41 0 6916 0
vsize: 27828
[startup+150.003 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 6404 0 0 0 14980 19 0 0 25 0 1 0 488994439 28766208 6184 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7023 6184 603 41 0 6982 0
vsize: 28092
[startup+160.003 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 6480 0 0 0 15980 19 0 0 25 0 1 0 488994439 29036544 6260 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7089 6260 603 41 0 7048 0
vsize: 28356
[startup+170.003 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 6595 0 0 0 16979 20 0 0 25 0 1 0 488994439 29573120 6375 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7220 6375 603 41 0 7179 0
vsize: 28880
[startup+180.003 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 6654 0 0 0 17979 20 0 0 25 0 1 0 488994439 29708288 6434 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7253 6434 603 41 0 7212 0
vsize: 29012
[startup+190.003 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 6908 0 0 0 18979 21 0 0 25 0 1 0 488994439 30789632 6688 4294967295 134512640 134672761 3221224544 3221223760 134557683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7517 6688 603 41 0 7476 0
vsize: 30068
[startup+200.004 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 7000 0 0 0 19979 21 0 0 25 0 1 0 488994439 31059968 6780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7583 6780 603 41 0 7542 0
vsize: 30332
[startup+210.003 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 7093 0 0 0 20979 21 0 0 25 0 1 0 488994439 31461376 6873 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7681 6873 603 41 0 7640 0
vsize: 30724
[startup+220.003 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 7708 0 0 0 21977 24 0 0 25 0 1 0 488994439 34021376 7488 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8306 7488 603 41 0 8265 0
vsize: 33224
[startup+230.003 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 7866 0 0 0 22977 24 0 0 25 0 1 0 488994439 34562048 7646 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8438 7646 603 41 0 8397 0
vsize: 33752
[startup+240.002 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 7919 0 0 0 23977 24 0 0 25 0 1 0 488994439 34828288 7699 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8503 7699 603 41 0 8462 0
vsize: 34012
[startup+250.003 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 8030 0 0 0 24977 24 0 0 25 0 1 0 488994439 35758080 7810 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8730 7810 603 41 0 8689 0
vsize: 34920
[startup+260.004 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 8078 0 0 0 25977 24 0 0 25 0 1 0 488994439 35893248 7858 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 7858 603 41 0 8722 0
vsize: 35052
[startup+270.003 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 8126 0 0 0 26977 24 0 0 25 0 1 0 488994439 36163584 7906 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 7906 603 41 0 8788 0
vsize: 35316
[startup+280.003 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 8196 0 0 0 27977 25 0 0 25 0 1 0 488994439 36433920 7976 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8895 7976 603 41 0 8854 0
vsize: 35580
[startup+290.003 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 8453 0 0 0 28976 25 0 0 25 0 1 0 488994439 37380096 8233 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9126 8233 603 41 0 9085 0
vsize: 36504
[startup+300.003 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 8599 0 0 0 29976 26 0 0 25 0 1 0 488994439 38051840 8379 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9290 8379 603 41 0 9249 0
vsize: 37160
[startup+310.003 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 8661 0 0 0 30976 26 0 0 25 0 1 0 488994439 38187008 8441 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9323 8441 603 41 0 9282 0
vsize: 37292
[startup+320.003 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 8732 0 0 0 31976 26 0 0 25 0 1 0 488994439 38592512 8512 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9422 8512 603 41 0 9381 0
vsize: 37688
[startup+330.003 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 8801 0 0 0 32976 26 0 0 25 0 1 0 488994439 38727680 8581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9455 8581 603 41 0 9414 0
vsize: 37820
[startup+340.003 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 8900 0 0 0 33976 27 0 0 25 0 1 0 488994439 39133184 8680 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9554 8680 603 41 0 9513 0
vsize: 38216
[startup+350.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9004 0 0 0 34975 27 0 0 25 0 1 0 488994439 39538688 8784 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9653 8784 603 41 0 9612 0
vsize: 38612
[startup+360.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9054 0 0 0 35976 27 0 0 25 0 1 0 488994439 39809024 8834 4294967295 134512640 134672761 3221224544 3221223696 134565070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9719 8834 603 41 0 9678 0
vsize: 38876
[startup+370.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9147 0 0 0 36976 27 0 0 25 0 1 0 488994439 40214528 8927 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9818 8927 603 41 0 9777 0
vsize: 39272
[startup+380.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9221 0 0 0 37976 28 0 0 25 0 1 0 488994439 40484864 9001 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9884 9001 603 41 0 9843 0
vsize: 39536
[startup+390.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9378 0 0 0 38975 28 0 0 25 0 1 0 488994439 41021440 9158 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10015 9158 603 41 0 9974 0
vsize: 40060
[startup+400.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9486 0 0 0 39976 28 0 0 25 0 1 0 488994439 41426944 9266 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10114 9266 603 41 0 10073 0
vsize: 40456
[startup+410.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9546 0 0 0 40976 28 0 0 25 0 1 0 488994439 41697280 9326 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10180 9326 603 41 0 10139 0
vsize: 40720
[startup+420.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9618 0 0 0 41976 29 0 0 25 0 1 0 488994439 41967616 9398 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10246 9398 603 41 0 10205 0
vsize: 40984
[startup+430.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9685 0 0 0 42975 29 0 0 25 0 1 0 488994439 42237952 9465 4294967295 134512640 134672761 3221224544 3221223732 134557974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10312 9465 603 41 0 10271 0
vsize: 41248
[startup+440.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9738 0 0 0 43975 29 0 0 25 0 1 0 488994439 42508288 9518 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10378 9518 603 41 0 10337 0
vsize: 41512
[startup+450.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9798 0 0 0 44975 29 0 0 25 0 1 0 488994439 42643456 9578 4294967295 134512640 134672761 3221224544 3221223712 134564451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10411 9578 603 41 0 10370 0
vsize: 41644
[startup+460.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9866 0 0 0 45975 29 0 0 25 0 1 0 488994439 42909696 9646 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10476 9646 603 41 0 10435 0
vsize: 41904
[startup+470.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 9929 0 0 0 46975 30 0 0 25 0 1 0 488994439 43180032 9709 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10542 9709 603 41 0 10501 0
vsize: 42168
[startup+480.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10022 0 0 0 47975 30 0 0 25 0 1 0 488994439 43585536 9802 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10641 9802 603 41 0 10600 0
vsize: 42564
[startup+490.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10067 0 0 0 48975 30 0 0 25 0 1 0 488994439 43720704 9847 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10674 9847 603 41 0 10633 0
vsize: 42696
[startup+500.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10120 0 0 0 49975 30 0 0 25 0 1 0 488994439 43986944 9900 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10739 9900 603 41 0 10698 0
vsize: 42956
[startup+510.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10182 0 0 0 50975 31 0 0 25 0 1 0 488994439 44257280 9962 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10805 9962 603 41 0 10764 0
vsize: 43220
[startup+520.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10262 0 0 0 51975 31 0 0 25 0 1 0 488994439 44527616 10042 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10871 10042 603 41 0 10830 0
vsize: 43484
[startup+530.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10315 0 0 0 52975 31 0 0 25 0 1 0 488994439 44662784 10095 4294967295 134512640 134672761 3221224544 3221223712 134560819 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10904 10095 603 41 0 10863 0
vsize: 43616
[startup+540.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10364 0 0 0 53975 31 0 0 25 0 1 0 488994439 44933120 10144 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10970 10144 603 41 0 10929 0
vsize: 43880
[startup+550.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10582 0 0 0 54975 32 0 0 25 0 1 0 488994439 45735936 10362 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11166 10362 603 41 0 11125 0
vsize: 44664
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10636 0 0 0 55975 32 0 0 25 0 1 0 488994439 46006272 10416 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11232 10416 603 41 0 11191 0
vsize: 44928
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10682 0 0 0 56975 32 0 0 25 0 1 0 488994439 46141440 10462 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11265 10462 603 41 0 11224 0
vsize: 45060
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10744 0 0 0 57975 32 0 0 25 0 1 0 488994439 46411776 10524 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11331 10524 603 41 0 11290 0
vsize: 45324
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10809 0 0 0 58975 32 0 0 25 0 1 0 488994439 46682112 10589 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11397 10589 603 41 0 11356 0
vsize: 45588
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10896 0 0 0 59975 32 0 0 25 0 1 0 488994439 47087616 10676 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11496 10676 603 41 0 11455 0
vsize: 45984
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 10990 0 0 0 60975 33 0 0 25 0 1 0 488994439 47357952 10770 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11562 10770 603 41 0 11521 0
vsize: 46248
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 11096 0 0 0 61975 33 0 0 25 0 1 0 488994439 47763456 10876 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11661 10876 603 41 0 11620 0
vsize: 46644
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 11149 0 0 0 62975 33 0 0 25 0 1 0 488994439 48033792 10929 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11727 10929 603 41 0 11686 0
vsize: 46908
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 11211 0 0 0 63975 33 0 0 25 0 1 0 488994439 48304128 10991 4294967295 134512640 134672761 3221224544 3221223712 134553610 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11793 10991 603 41 0 11752 0
vsize: 47172
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 11364 0 0 0 64975 33 0 0 25 0 1 0 488994439 49889280 11144 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12180 11144 603 41 0 12139 0
vsize: 48720
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 11449 0 0 0 65975 34 0 0 25 0 1 0 488994439 50294784 11229 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12279 11229 603 41 0 12238 0
vsize: 49116
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 11906 0 0 0 66975 35 0 0 25 0 1 0 488994439 52051968 11686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12708 11686 603 41 0 12667 0
vsize: 50832
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 12311 0 0 0 67974 36 0 0 25 0 1 0 488994439 53669888 12091 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13103 12091 603 41 0 13062 0
vsize: 52412
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 12685 0 0 0 68973 37 0 0 25 0 1 0 488994439 55291904 12465 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13499 12465 603 41 0 13458 0
vsize: 53996
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 12936 0 0 0 69971 38 0 0 25 0 1 0 488994439 56238080 12716 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13730 12716 603 41 0 13689 0
vsize: 54920
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 13020 0 0 0 70972 38 0 0 25 0 1 0 488994439 56643584 12800 4294967295 134512640 134672761 3221224544 3221223712 134564493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13829 12800 603 41 0 13788 0
vsize: 55316
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 13548 0 0 0 71970 40 0 0 25 0 1 0 488994439 58658816 13328 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14321 13328 603 41 0 14280 0
vsize: 57284
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 14092 0 0 0 72969 41 0 0 25 0 1 0 488994439 60948480 13872 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14880 13872 603 41 0 14839 0
vsize: 59520
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 14191 0 0 0 73970 41 0 0 25 0 1 0 488994439 61218816 13971 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14946 13971 603 41 0 14905 0
vsize: 59784
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 14313 0 0 0 74969 41 0 0 25 0 1 0 488994439 61755392 14093 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15077 14093 603 41 0 15036 0
vsize: 60308
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 14388 0 0 0 75969 41 0 0 25 0 1 0 488994439 62025728 14168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15143 14168 603 41 0 15102 0
vsize: 60572
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 14559 0 0 0 76969 42 0 0 25 0 1 0 488994439 62701568 14339 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15308 14339 603 41 0 15267 0
vsize: 61232
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 14610 0 0 0 77969 42 0 0 25 0 1 0 488994439 62971904 14390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15374 14390 603 41 0 15333 0
vsize: 61496
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 14663 0 0 0 78969 42 0 0 25 0 1 0 488994439 63102976 14443 4294967295 134512640 134672761 3221224544 3221223648 134555539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15406 14443 603 41 0 15365 0
vsize: 61624
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 79968 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 80968 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 81968 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 82969 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 83969 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 84969 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 85969 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 86970 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 87970 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 88970 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 89970 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+910.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 90970 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 91971 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 92971 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 93971 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 94971 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 95971 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 96972 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 97972 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 98972 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 99972 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 100972 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 101972 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 102973 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 103973 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 104972 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223760 134557646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 105973 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 106973 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 107973 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 108973 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223728 134559293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 109973 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 110974 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 111974 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 112974 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 113974 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 114974 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 115974 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 116975 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 117975 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15428 0 0 0 118975 44 0 0 25 0 1 0 488994439 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16159 15208 603 41 0 16118 0
vsize: 64636
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22709
Raw data (stat): 22709 (minisat+) R 22708 30701 30700 0 -1 0 15488 0 0 0 119975 44 0 0 25 0 1 0 488994439 66457600 15268 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16225 15268 603 41 0 16184 0
vsize: 64900
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 22709
Raw data (stat): 22709 (minisat+) Z 22708 30701 30700 0 -1 12 15490 0 0 0 119975 47 0 0 25 0 1 0 488994439 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.05
CPU time (s): 1200.23
CPU user time (s): 1199.75
CPU system time (s): 0.473927
CPU usage (%): 100.014
Max. virtual memory (Kb): 64900
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####