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/miplib3/normalized-mps-v2-13-7-fixnet6.opb
MD5SUM	5efced6eaf647505ade406591fd69d4e
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	1216.42
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 18233

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        652200 kB
Buffers:         22972 kB
Cached:         337152 kB
SwapCached:          4 kB
Active:         169932 kB
Inactive:       193012 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        651948 kB
SwapTotal:     2097136 kB
SwapFree:      2097128 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            13848 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:22:44 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 18353 7 1200.22 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.75 0.92 0.90 2/54 7973
Raw data (stat): 7973 (runsolver) R 7972 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487430330 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.79 0.92 0.90 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 4918 0 0 0 986 12 0 0 25 0 1 0 487430330 22564864 4698 4294967295 134512640 134672761 3221224544 3221223808 134562262 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.0013 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 5038 0 0 0 1985 13 0 0 25 0 1 0 487430330 23121920 4818 4294967295 134512640 134672761 3221224544 3221223668 134566049 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.0013 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 5128 0 0 0 2984 13 0 0 25 0 1 0 487430330 23392256 4908 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5711 4908 603 41 0 5670 0
vsize: 22844
[startup+40.0009 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 5212 0 0 0 3984 14 0 0 25 0 1 0 487430330 23797760 4992 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.89 0.93 0.90 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 5363 0 0 0 4984 14 0 0 25 0 1 0 487430330 24461312 5143 4294967295 134512640 134672761 3221224544 3221223712 134561215 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.91 0.93 0.90 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 5476 0 0 0 5984 14 0 0 25 0 1 0 487430330 24866816 5256 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6071 5256 603 41 0 6030 0
vsize: 24284
[startup+70.0019 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 5557 0 0 0 6984 14 0 0 25 0 1 0 487430330 25272320 5337 4294967295 134512640 134672761 3221224544 3221223700 134564777 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.93 0.94 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 5729 0 0 0 7983 15 0 0 25 0 1 0 487430330 25948160 5509 4294967295 134512640 134672761 3221224544 3221223728 134558771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6335 5509 603 41 0 6294 0
vsize: 25340
[startup+90.0021 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 5867 0 0 0 8983 16 0 0 25 0 1 0 487430330 26484736 5647 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6466 5647 603 41 0 6425 0
vsize: 25864
[startup+100.002 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 5944 0 0 0 9983 16 0 0 25 0 1 0 487430330 26755072 5724 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6532 5724 603 41 0 6491 0
vsize: 26128
[startup+110.003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 6057 0 0 0 10982 16 0 0 25 0 1 0 487430330 27418624 5837 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.96 0.94 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 6155 0 0 0 11981 17 0 0 25 0 1 0 487430330 27824128 5935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6793 5935 603 41 0 6752 0
vsize: 27172
[startup+130.003 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 6231 0 0 0 12981 17 0 0 25 0 1 0 487430330 28094464 6011 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6859 6011 603 41 0 6818 0
vsize: 27436
[startup+140.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 6325 0 0 0 13981 18 0 0 25 0 1 0 487430330 28495872 6105 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6957 6105 603 41 0 6916 0
vsize: 27828
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 6389 0 0 0 14981 18 0 0 25 0 1 0 487430330 28766208 6169 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7023 6169 603 41 0 6982 0
vsize: 28092
[startup+160.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 6479 0 0 0 15981 18 0 0 25 0 1 0 487430330 29036544 6259 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7089 6259 603 41 0 7048 0
vsize: 28356
[startup+170.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 6593 0 0 0 16981 18 0 0 25 0 1 0 487430330 29573120 6373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7220 6373 603 41 0 7179 0
vsize: 28880
[startup+180.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 6653 0 0 0 17981 19 0 0 25 0 1 0 487430330 29708288 6433 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7253 6433 603 41 0 7212 0
vsize: 29012
[startup+190.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 6907 0 0 0 18980 19 0 0 25 0 1 0 487430330 30789632 6687 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7517 6687 603 41 0 7476 0
vsize: 30068
[startup+200.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 6998 0 0 0 19980 20 0 0 25 0 1 0 487430330 31059968 6778 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7583 6778 603 41 0 7542 0
vsize: 30332
[startup+210.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 7092 0 0 0 20980 20 0 0 25 0 1 0 487430330 31461376 6872 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7681 6872 603 41 0 7640 0
vsize: 30724
[startup+220.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7973
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 7684 0 0 0 21979 22 0 0 25 0 1 0 487430330 33890304 7464 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8274 7464 603 41 0 8233 0
vsize: 33096
[startup+230.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 7865 0 0 0 22978 22 0 0 25 0 1 0 487430330 34562048 7645 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8438 7645 603 41 0 8397 0
vsize: 33752
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 7918 0 0 0 23978 23 0 0 25 0 1 0 487430330 34828288 7698 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8503 7698 603 41 0 8462 0
vsize: 34012
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 8029 0 0 0 24978 23 0 0 25 0 1 0 487430330 35758080 7809 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8730 7809 603 41 0 8689 0
vsize: 34920
[startup+260.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 8077 0 0 0 25978 23 0 0 25 0 1 0 487430330 35893248 7857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8763 7857 603 41 0 8722 0
vsize: 35052
[startup+270.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 8125 0 0 0 26978 23 0 0 25 0 1 0 487430330 36163584 7905 4294967295 134512640 134672761 3221224544 3221223708 134564531 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8829 7905 603 41 0 8788 0
vsize: 35316
[startup+280.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 8194 0 0 0 27978 23 0 0 25 0 1 0 487430330 36433920 7974 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8895 7974 603 41 0 8854 0
vsize: 35580
[startup+290.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 8426 0 0 0 28977 24 0 0 25 0 1 0 487430330 37380096 8206 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9126 8206 603 41 0 9085 0
vsize: 36504
[startup+300.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 8598 0 0 0 29977 25 0 0 25 0 1 0 487430330 38051840 8378 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9290 8378 603 41 0 9249 0
vsize: 37160
[startup+310.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 8659 0 0 0 30977 25 0 0 25 0 1 0 487430330 38187008 8439 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9323 8439 603 41 0 9282 0
vsize: 37292
[startup+320.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 8730 0 0 0 31977 25 0 0 25 0 1 0 487430330 38457344 8510 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9389 8510 603 41 0 9348 0
vsize: 37556
[startup+330.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 8796 0 0 0 32977 25 0 0 25 0 1 0 487430330 38727680 8576 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9455 8576 603 41 0 9414 0
vsize: 37820
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 8894 0 0 0 33977 26 0 0 25 0 1 0 487430330 39133184 8674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9554 8674 603 41 0 9513 0
vsize: 38216
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9001 0 0 0 34977 26 0 0 25 0 1 0 487430330 39538688 8781 4294967295 134512640 134672761 3221224544 3221223680 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9653 8781 603 41 0 9612 0
vsize: 38612
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9052 0 0 0 35977 26 0 0 25 0 1 0 487430330 39809024 8832 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9719 8832 603 41 0 9678 0
vsize: 38876
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9110 0 0 0 36977 26 0 0 25 0 1 0 487430330 39944192 8890 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9752 8890 603 41 0 9711 0
vsize: 39008
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9219 0 0 0 37977 27 0 0 25 0 1 0 487430330 40484864 8999 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9884 8999 603 41 0 9843 0
vsize: 39536
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9375 0 0 0 38976 27 0 0 25 0 1 0 487430330 41021440 9155 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10015 9155 603 41 0 9974 0
vsize: 40060
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9483 0 0 0 39976 27 0 0 25 0 1 0 487430330 41426944 9263 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10114 9263 603 41 0 10073 0
vsize: 40456
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9537 0 0 0 40976 27 0 0 25 0 1 0 487430330 41697280 9317 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10180 9317 603 41 0 10139 0
vsize: 40720
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9615 0 0 0 41976 28 0 0 25 0 1 0 487430330 41967616 9395 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10246 9395 603 41 0 10205 0
vsize: 40984
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9684 0 0 0 42976 28 0 0 25 0 1 0 487430330 42237952 9464 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10312 9464 603 41 0 10271 0
vsize: 41248
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9736 0 0 0 43976 28 0 0 25 0 1 0 487430330 42508288 9516 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10378 9516 603 41 0 10337 0
vsize: 41512
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9795 0 0 0 44976 28 0 0 25 0 1 0 487430330 42643456 9575 4294967295 134512640 134672761 3221224544 3221223484 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10411 9575 603 41 0 10370 0
vsize: 41644
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9857 0 0 0 45976 29 0 0 25 0 1 0 487430330 42909696 9637 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10476 9637 603 41 0 10435 0
vsize: 41904
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 9927 0 0 0 46976 29 0 0 25 0 1 0 487430330 43180032 9707 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10542 9707 603 41 0 10501 0
vsize: 42168
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10020 0 0 0 47975 29 0 0 25 0 1 0 487430330 43585536 9800 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10641 9800 603 41 0 10600 0
vsize: 42564
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10063 0 0 0 48976 29 0 0 25 0 1 0 487430330 43720704 9843 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10674 9843 603 41 0 10633 0
vsize: 42696
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10117 0 0 0 49976 29 0 0 25 0 1 0 487430330 43986944 9897 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10739 9897 603 41 0 10698 0
vsize: 42956
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10179 0 0 0 50975 30 0 0 25 0 1 0 487430330 44257280 9959 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10805 9959 603 41 0 10764 0
vsize: 43220
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10256 0 0 0 51975 30 0 0 25 0 1 0 487430330 44527616 10036 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10871 10036 603 41 0 10830 0
vsize: 43484
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10312 0 0 0 52975 30 0 0 25 0 1 0 487430330 44662784 10092 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10904 10092 603 41 0 10863 0
vsize: 43616
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10359 0 0 0 53975 30 0 0 25 0 1 0 487430330 44933120 10139 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10970 10139 603 41 0 10929 0
vsize: 43880
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10579 0 0 0 54975 31 0 0 25 0 1 0 487430330 45735936 10359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11166 10359 603 41 0 11125 0
vsize: 44664
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10633 0 0 0 55975 31 0 0 25 0 1 0 487430330 46006272 10413 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11232 10413 603 41 0 11191 0
vsize: 44928
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10678 0 0 0 56975 31 0 0 25 0 1 0 487430330 46141440 10458 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11265 10458 603 41 0 11224 0
vsize: 45060
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10739 0 0 0 57975 31 0 0 25 0 1 0 487430330 46411776 10519 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11331 10519 603 41 0 11290 0
vsize: 45324
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10801 0 0 0 58975 32 0 0 25 0 1 0 487430330 46682112 10581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11397 10581 603 41 0 11356 0
vsize: 45588
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10892 0 0 0 59975 32 0 0 25 0 1 0 487430330 46952448 10672 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11463 10672 603 41 0 11422 0
vsize: 45852
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 10980 0 0 0 60975 32 0 0 25 0 1 0 487430330 47357952 10760 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11562 10760 603 41 0 11521 0
vsize: 46248
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 11091 0 0 0 61975 33 0 0 25 0 1 0 487430330 47763456 10871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11661 10871 603 41 0 11620 0
vsize: 46644
[startup+630.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 11144 0 0 0 62975 33 0 0 25 0 1 0 487430330 48033792 10924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11727 10924 603 41 0 11686 0
vsize: 46908
[startup+640.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 11207 0 0 0 63974 33 0 0 25 0 1 0 487430330 48304128 10987 4294967295 134512640 134672761 3221224544 3221223484 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11793 10987 603 41 0 11752 0
vsize: 47172
[startup+650.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 11327 0 0 0 64974 34 0 0 25 0 1 0 487430330 49754112 11107 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12147 11107 603 41 0 12106 0
vsize: 48588
[startup+660.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 11432 0 0 0 65974 34 0 0 25 0 1 0 487430330 50159616 11212 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12246 11212 603 41 0 12205 0
vsize: 48984
[startup+670.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 11860 0 0 0 66973 35 0 0 25 0 1 0 487430330 51916800 11640 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12675 11640 603 41 0 12634 0
vsize: 50700
[startup+680.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 12264 0 0 0 67973 36 0 0 25 0 1 0 487430330 53534720 12044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13070 12044 603 41 0 13029 0
vsize: 52280
[startup+690.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 12647 0 0 0 68972 37 0 0 25 0 1 0 487430330 55156736 12427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13466 12427 603 41 0 13425 0
vsize: 53864
[startup+700.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 12929 0 0 0 69969 38 0 0 25 0 1 0 487430330 56238080 12709 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13730 12709 603 41 0 13689 0
vsize: 54920
[startup+710.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 12993 0 0 0 70970 38 0 0 25 0 1 0 487430330 56508416 12773 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13796 12773 603 41 0 13755 0
vsize: 55184
[startup+720.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 13442 0 0 0 71969 39 0 0 25 0 1 0 487430330 58261504 13222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14224 13222 603 41 0 14183 0
vsize: 56896
[startup+730.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 14080 0 0 0 72967 41 0 0 25 0 1 0 487430330 60813312 13860 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14847 13860 603 41 0 14806 0
vsize: 59388
[startup+740.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 14183 0 0 0 73967 41 0 0 25 0 1 0 487430330 61218816 13963 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14946 13963 603 41 0 14905 0
vsize: 59784
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 14304 0 0 0 74967 41 0 0 25 0 1 0 487430330 61755392 14084 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15077 14084 603 41 0 15036 0
vsize: 60308
[startup+760.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 14381 0 0 0 75967 41 0 0 25 0 1 0 487430330 62025728 14161 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15143 14161 603 41 0 15102 0
vsize: 60572
[startup+770.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 14545 0 0 0 76967 42 0 0 25 0 1 0 487430330 62701568 14325 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15308 14325 603 41 0 15267 0
vsize: 61232
[startup+780.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 14603 0 0 0 77967 42 0 0 25 0 1 0 487430330 62971904 14383 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15374 14383 603 41 0 15333 0
vsize: 61496
[startup+790.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 14653 0 0 0 78967 42 0 0 25 0 1 0 487430330 63102976 14433 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15406 14433 603 41 0 15365 0
vsize: 61624
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 79965 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223552 134565852 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 80965 45 0 0 25 0 1 0 487430330 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+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 81965 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134561207 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 82965 45 0 0 25 0 1 0 487430330 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+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 83965 45 0 0 25 0 1 0 487430330 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+850.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 84965 45 0 0 25 0 1 0 487430330 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+860.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 85966 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134561382 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 86966 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560871 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 87966 45 0 0 25 0 1 0 487430330 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.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 88966 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223696 134565086 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 89966 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223680 134565092 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 90966 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223680 134560590 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 91967 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223668 134566118 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 92967 45 0 0 25 0 1 0 487430330 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+940.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 93967 45 0 0 25 0 1 0 487430330 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+950.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 94967 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560892 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 95967 45 0 0 25 0 1 0 487430330 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+970.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 96967 45 0 0 25 0 1 0 487430330 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+980.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 97968 45 0 0 25 0 1 0 487430330 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+990.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 98968 45 0 0 25 0 1 0 487430330 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+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 99968 45 0 0 25 0 1 0 487430330 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+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 100968 45 0 0 25 0 1 0 487430330 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+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 101968 45 0 0 25 0 1 0 487430330 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+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 102969 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223668 134566043 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 103969 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560876 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 104969 45 0 0 25 0 1 0 487430330 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+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 105969 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134561008 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 106969 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223712 134560999 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 107970 45 0 0 25 0 1 0 487430330 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+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 108970 45 0 0 25 0 1 0 487430330 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+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 109970 45 0 0 25 0 1 0 487430330 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+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 110971 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223668 134566043 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 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 111971 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223668 134566049 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 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 112971 45 0 0 25 0 1 0 487430330 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+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 113972 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223668 134566043 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 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 114972 45 0 0 25 0 1 0 487430330 66187264 15208 4294967295 134512640 134672761 3221224544 3221223696 134565092 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 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 115972 45 0 0 25 0 1 0 487430330 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 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 116972 45 0 0 25 0 1 0 487430330 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+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 117972 45 0 0 25 0 1 0 487430330 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+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 118973 45 0 0 25 0 1 0 487430330 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 7975
Raw data (stat): 7973 (minisat+) R 7972 22932 22931 0 -1 0 15428 0 0 0 119973 45 0 0 25 0 1 0 487430330 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
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 7975
Raw data (stat): 7973 (minisat+) Z 7972 22932 22931 0 -1 12 15430 0 0 0 119973 48 0 0 25 0 1 0 487430330 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.22
CPU user time (s): 1199.73
CPU system time (s): 0.481926
CPU usage (%): 100.014
Max. virtual memory (Kb): 64636
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####