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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-bienst1.opb
MD5SUM	3be753912a1804561d804d0545fc341d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	13633395
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	9232
Total number of constraints	632
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	32
Number of constraints which are nor clauses,nor cardinality constraints	600
Minimum length of a constraint	1
Maximum length of a constraint	260
Trace number 14757

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        832972 kB
Buffers:          3248 kB
Cached:         165936 kB
SwapCached:          0 kB
Active:          40424 kB
Inactive:       131604 kB
HighTotal:      131008 kB
HighFree:        29344 kB
LowTotal:       903652 kB
LowFree:        803628 kB
SwapTotal:     2097892 kB
SwapFree:      2097824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            23940 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 01:30:44 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 19419 7 1200.33 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 732 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 731]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 730]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 729]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 728]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 727]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 726]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 725]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 724]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 723]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 722]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 721]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 720]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 719]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 718]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 717]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 716]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 715]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 714]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 713]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 712]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 711]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 710]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 709]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 708]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 707]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 706]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 705]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 704]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 702]---> Adder-cost: 336   maxlim: 121593   bits: 18/17
c ---[ 700]---> Adder-cost: 336   maxlim: 121977   bits: 18/17
c ---[ 698]---> Adder-cost: 326   maxlim: 129401   bits: 18/17
c ---[ 696]---> Adder-cost: 336   maxlim: 121337   bits: 18/17
c ---[ 694]---> Adder-cost: 336   maxlim: 121209   bits: 18/17
c ---[ 692]---> Adder-cost: 347   maxlim: 105721   bits: 18/17
c ---[ 690]---> Adder-cost: 336   maxlim: 121209   bits: 18/17
c ---[ 688]---> Adder-cost: 346   maxlim: 178425   bits: 19/18
c ---[ 686]---> Adder-cost: 346   maxlim: 178297   bits: 19/18
c ---[ 684]---> Adder-cost: 346   maxlim: 178553   bits: 19/18
c ---[ 682]---> Adder-cost: 352   maxlim: 162297   bits: 19/18
c ---[ 680]---> Adder-cost: 352   maxlim: 162681   bits: 19/18
c ---[ 678]---> Adder-cost: 352   maxlim: 162681   bits: 19/18
c ---[ 676]---> Adder-cost: 352   maxlim: 162681   bits: 19/18
c ---[ 674]---> Adder-cost: 322   maxlim: 88441   bits: 18/17
c ---[ 672]---> Adder-cost: 322   maxlim: 88953   bits: 18/17
c ---[ 670]---> Adder-cost: 322   maxlim: 88697   bits: 18/17
c ---[ 668]---> Adder-cost: 328   maxlim: 81145   bits: 18/17
c ---[ 666]---> Adder-cost: 328   maxlim: 81273   bits: 18/17
c ---[ 664]---> Adder-cost: 328   maxlim: 80505   bits: 18/17
c ---[ 662]---> Adder-cost: 328   maxlim: 80889   bits: 18/17
c ---[ 660]---> Adder-cost: 322   maxlim: 89209   bits: 18/17
c ---[ 658]---> Adder-cost: 322   maxlim: 89081   bits: 18/17
c ---[ 656]---> Adder-cost: 322   maxlim: 88185   bits: 18/17
c ---[ 654]---> Adder-cost: 328   maxlim: 81017   bits: 18/17
c ---[ 652]---> Adder-cost: 328   maxlim: 81145   bits: 18/17
c ---[ 650]---> Adder-cost: 328   maxlim: 80505   bits: 18/17
c ---[ 648]---> Adder-cost: 328   maxlim: 80761   bits: 18/17
c ---[ 646]---> Adder-cost: 334   maxlim: 130041   bits: 18/17
c ---[ 644]---> Adder-cost: 326   maxlim: 137721   bits: 18/18
c ---[ 642]---> Adder-cost: 326   maxlim: 137721   bits: 18/18
c ---[ 640]---> Adder-cost: 334   maxlim: 129913   bits: 18/17
c ---[ 638]---> Adder-cost: 345   maxlim: 113529   bits: 18/17
c ---[ 636]---> Adder-cost: 334   maxlim: 129273   bits: 18/17
c ---[ 634]---> Adder-cost: 334   maxlim: 129657   bits: 18/17
c ---[ 632]---> Adder-cost: 334   maxlim: 105849   bits: 18/17
c ---[ 630]---> Adder-cost: 322   maxlim: 113273   bits: 18/17
c ---[ 628]---> Adder-cost: 322   maxlim: 113273   bits: 18/17
c ---[ 626]---> Adder-cost: 322   maxlim: 113785   bits: 18/17
c ---[ 624]---> Adder-cost: 334   maxlim: 105337   bits: 18/17
c ---[ 622]---> Adder-cost: 334   maxlim: 104569   bits: 18/17
c ---[ 620]---> Adder-cost: 334   maxlim: 104953   bits: 18/17
c ---[ 618]---> Adder-cost: 322   maxlim: 105721   bits: 18/17
c ---[ 616]---> Adder-cost: 322   maxlim: 105337   bits: 18/17
c ---[ 614]---> Adder-cost: 322   maxlim: 105593   bits: 18/17
c ---[ 612]---> Adder-cost: 322   maxlim: 104697   bits: 18/17
c ---[ 610]---> Adder-cost: 328   maxlim: 97017   bits: 18/17
c ---[ 608]---> Adder-cost: 328   maxlim: 96761   bits: 18/17
c ---[ 606]---> Adder-cost: 328   maxlim: 97401   bits: 18/17
c ---[ 604]---> Adder-cost: 322   maxlim: 88697   bits: 18/17
c ---[ 602]---> Adder-cost: 322   maxlim: 89209   bits: 18/17
c ---[ 600]---> Adder-cost: 322   maxlim: 89081   bits: 18/17
c ---[ 598]---> Adder-cost: 322   maxlim: 89337   bits: 18/17
c ---[ 596]---> Adder-cost: 328   maxlim: 80633   bits: 18/17
c ---[ 594]---> Adder-cost: 328   maxlim: 81273   bits: 18/17
c ---[ 592]---> Adder-cost: 328   maxlim: 80121   bits: 18/17
c ---[ 591]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 590]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 589]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 588]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 587]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 586]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 585]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 584]---> Adder-cost: 36   maxlim: 65534   bits: 17/16
c ---[ 583]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 582]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 581]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 580]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 579]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 578]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 577]---> Adder-cost: 36   maxlim: 65534   bits: 17/16
c ---[ 576]---> Adder-cost: 36   maxlim: 65534   bits: 17/16
c ---[ 575]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 574]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 573]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 572]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 571]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 570]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 569]---> Adder-cost: 36   maxlim: 65534   bits: 17/16
c ---[ 568]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 567]---> Adder-cost: 36   maxlim: 65534   bits: 17/16
c ---[ 566]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 565]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 564]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 563]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 562]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 561]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 560]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 559]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 558]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 557]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 556]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 555]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 554]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 553]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 552]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 551]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 550]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 549]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 548]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 547]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 546]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 545]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 544]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 543]---> Adder-cost: 38   maxlim: 262142   bits: 19/18
c ---[ 542]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 541]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 540]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 539]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 538]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 537]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 536]---> Adder-cost: 37   maxlim: 131070   bits: 18/17
c ---[ 534]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 532]---> Adder-cost: 198   maxlim: 131071   bits: 18/17
c ---[ 530]---> Adder-cost: 198   maxlim: 131071   bits: 18/17
c ---[ 528]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 526]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 524]---> Adder-cost: 198   maxlim: 131071   bits: 18/17
c ---[ 522]---> Adder-cost: 198   maxlim: 131071   bits: 18/17
c ---[ 520]---> Adder-cost: 188   maxlim: 65535   bits: 17/16
c ---[ 518]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 516]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 514]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 512]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 510]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 508]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 506]---> Adder-cost: 188   maxlim: 65535   bits: 17/16
c ---[ 504]---> Adder-cost: 188   maxlim: 65535   bits: 17/16
c ---[ 502]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 500]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 498]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 496]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 494]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 492]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 490]---> Adder-cost: 188   maxlim: 65535   bits: 17/16
c ---[ 488]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 486]---> Adder-cost: 188   maxlim: 65535   bits: 17/16
c ---[ 484]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 482]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 480]---> Adder-cost: 196   maxlim: 131071   bits: 18/17
c ---[ 478]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 476]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 474]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 472]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 470]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 468]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 466]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 464]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 462]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 460]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 458]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 456]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 454]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 452]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 450]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 448]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 446]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 444]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 442]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 440]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 438]---> Adder-cost: 210   maxlim: 262143   bits: 19/18
c ---[ 436]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 434]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 432]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 430]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 428]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 426]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 424]---> Adder-cost: 202   maxlim: 131071   bits: 18/17
c ---[ 422]---> Adder-cost: 56   maxlim: 1148   bits: 11/11
c ---[ 420]---> Adder-cost: 56   maxlim: 1148   bits: 11/11
c ---[ 418]---> Adder-cost: 56   maxlim: 1148   bits: 11/11
c ---[ 416]---> Adder-cost: 56   maxlim: 1148   bits: 11/11
c ---[ 414]---> Adder-cost: 40   maxlim: 1021   bits: 11/10
c ---[ 412]---> Adder-cost: 40   maxlim: 1021   bits: 11/10
c ---[ 410]---> Adder-cost: 40   maxlim: 1021   bits: 11/10
c ---[ 408]---> Adder-cost: 40   maxlim: 1021   bits: 11/10
c ---[ 406]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 404]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 402]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 400]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 398]---> Adder-cost: 96   maxlim: 1529   bits: 11/11
c ---[ 396]---> Adder-cost: 96   maxlim: 1529   bits: 11/11
c ---[ 394]---> Adder-cost: 96   maxlim: 1529   bits: 11/11
c ---[ 392]---> Adder-cost: 96   maxlim: 1529   bits: 11/11
c ---[ 391]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 390]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 389]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 388]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 387]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 386]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 385]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 384]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 383]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 382]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 381]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 380]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 379]---> Adder-cost: 2   maxlim: 16382   bits: 15/14
c ---[ 378]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 377]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 376]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 375]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 374]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 373]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 372]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 371]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 370]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 369]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 368]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 367]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 366]---> Adder-cost: 90   maxlim: 16382   bits: 15/14
c ---[ 365]---> Adder-cost: 90   maxlim: 16382   bits: 15/14
c ---[ 364]---> Adder-cost: 90   maxlim: 16382   bits: 15/14
c ---[ 363]---> Adder-cost: 90   maxlim: 16382   bits: 15/14
c ---[ 362]---> Adder-cost: 90   maxlim: 16382   bits: 15/14
c ---[ 361]---> Adder-cost: 90   maxlim: 16382   bits: 15/14
c ---[ 360]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 359]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 358]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 357]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 356]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 355]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 354]---> Adder-cost: 42   maxlim: 32766   bits: 16/15
c ---[ 353]---> Adder-cost: 42   maxlim: 32766   bits: 16/15
c ---[ 352]---> Adder-cost: 42   maxlim: 32766   bits: 16/15
c ---[ 351]---> Adder-cost: 42   maxlim: 32766   bits: 16/15
c ---[ 350]---> Adder-cost: 42   maxlim: 32766   bits: 16/15
c ---[ 349]---> Adder-cost: 42   maxlim: 32766   bits: 16/15
c ---[ 348]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 347]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 346]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 345]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 344]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 343]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 342]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 341]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 340]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 339]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 338]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 337]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 336]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 335]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 334]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 333]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 332]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 331]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 330]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 329]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 328]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 327]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 326]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 325]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 324]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 323]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 322]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 321]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 320]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 319]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 318]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[ 317]---> Adder-cost: 62   maxlim: 32766   bits: 16/15
c ---[ 316]---> Adder-cost: 62   maxlim: 32766   bits: 16/15
c ---[ 315]---> Adder-cost: 62   maxlim: 32766   bits: 16/15
c ---[ 314]---> Adder-cost: 62   maxlim: 32766   bits: 16/15
c ---[ 313]---> Adder-cost: 62   maxlim: 32766   bits: 16/15
c ---[ 312]---> Adder-cost: 62   maxlim: 32766   bits: 16/15
c ---[ 311]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 310]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 309]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 308]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 307]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 306]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 305]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 304]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 303]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 302]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 301]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 300]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 299]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 298]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 297]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 296]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 295]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 294]---> Adder-cost: 40   maxlim: 32766   bits: 16/15
c ---[ 293]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 292]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 291]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 290]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 289]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 288]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 287]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 286]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 285]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 284]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 283]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 282]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 281]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 280]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 279]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 278]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 277]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 276]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 275]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 274]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 273]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 272]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 271]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 270]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 269]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 268]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 267]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 266]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 265]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 264]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 263]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 262]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 261]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 260]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 259]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 258]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 257]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 256]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 255]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 254]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 253]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 252]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 251]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 250]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 249]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 248]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 247]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 246]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 245]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 244]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 243]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 242]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 241]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 240]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 239]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 238]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 237]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 236]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 235]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 234]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 233]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 232]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 231]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 230]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 229]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 228]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 227]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 226]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 225]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 224]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 223]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 222]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 221]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 220]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 219]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[ 218]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[ 217]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[ 216]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[ 215]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[ 214]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[ 213]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 212]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 211]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 210]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 209]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 208]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[ 207]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 206]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 205]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 204]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 203]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 202]---> Adder-cost: 56   maxlim: 16382   bits: 15/14
c ---[ 201]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 200]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 199]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 198]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 197]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 196]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 195]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 194]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 193]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 192]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 191]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 190]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 189]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 188]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 187]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 186]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 185]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 184]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 183]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 182]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 181]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 180]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 179]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 178]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 177]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 176]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 175]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 174]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 173]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 172]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[ 171]---> Adder-cost: 78   maxlim: 32766   bits: 16/15
c ---[ 170]---> Adder-cost: 78   maxlim: 32766   bits: 16/15
c ---[ 169]---> Adder-cost: 78   maxlim: 32766   bits: 16/15
c ---[ 168]---> Adder-cost: 78   maxlim: 32766   bits: 16/15
c ---[ 167]---> Adder-cost: 78   maxlim: 32766   bits: 16/15
c ---[ 166]---> Adder-cost: 78   maxlim: 32766   bits: 16/15
c ---[ 165]---> Adder-cost: 78   maxlim: 32766   bits: 16/15
c ---[ 164]---> Adder-cost: 44   maxlim: 32766   bits: 16/15
c ---[ 163]---> Adder-cost: 44   maxlim: 32766   bits: 16/15
c ---[ 162]---> Adder-cost: 44   maxlim: 32766   bits: 16/15
c ---[ 161]---> Adder-cost: 44   maxlim: 32766   bits: 16/15
c ---[ 160]---> Adder-cost: 44   maxlim: 32766   bits: 16/15
c ---[ 159]---> Adder-cost: 44   maxlim: 32766   bits: 16/15
c ---[ 158]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 157]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 156]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 155]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 154]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 153]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 152]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 151]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 150]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 149]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 148]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 147]---> Adder-cost: 16   maxlim: 16382   bits: 15/14
c ---[ 146]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 145]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 144]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 143]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 142]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 141]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 140]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 139]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 138]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 137]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 136]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 135]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 134]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 133]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 132]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 131]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 130]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 129]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 128]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 127]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 126]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 125]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 124]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 123]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 122]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 121]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 120]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 119]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 118]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 117]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 116]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 115]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 114]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 113]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 112]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 111]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 110]---> Adder-cost: 60   maxlim: 32766   bits: 16/15
c ---[ 109]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 108]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 107]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 106]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 105]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 104]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[ 103]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 102]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 101]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[ 100]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  99]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  98]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  97]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  96]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  95]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  94]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  93]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  92]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  91]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  90]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  89]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  88]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  87]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  86]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  85]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  84]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  83]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  82]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  81]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  80]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  79]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  78]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  77]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  76]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  75]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  74]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  73]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[  72]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[  71]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[  70]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[  69]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[  68]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[  67]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  66]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  65]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  64]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  63]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  62]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  61]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  60]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  59]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  58]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  57]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  56]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  55]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[  54]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  53]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  52]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  51]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  50]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  49]---> Adder-cost: 74   maxlim: 16382   bits: 15/14
c ---[  48]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  47]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  46]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  45]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  44]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  43]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  42]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  41]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  40]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  39]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  38]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  37]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  36]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  35]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  34]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  33]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  32]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  31]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  30]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  29]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  28]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  27]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  26]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  25]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  24]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  23]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  22]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  21]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  20]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  19]---> Adder-cost: 76   maxlim: 16382   bits: 15/14
c ---[  18]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[  17]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[  16]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[  15]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[  14]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[  13]---> Adder-cost: 54   maxlim: 16382   bits: 15/14
c ---[  12]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[  11]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[  10]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   9]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   8]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   7]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[   6]---> Adder-cost: 92   maxlim: 16382   bits: 15/14
c ---[   5]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   4]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   3]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   2]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   1]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ---[   0]---> Adder-cost: 86   maxlim: 16382   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  319959  1167260 |  106653       0        0     nan |  0.000 % |
c |       100 |  319959  1167260 |  117318     100      455     4.5 | 20.192 % |
c |       250 |  319944  1167213 |  129050     248     1527     6.2 | 20.197 % |
c |       476 |  319944  1167213 |  141955     474     3026     6.4 | 20.197 % |
c |       813 |  319944  1167213 |  156150     811     5592     6.9 | 20.197 % |
c |      1319 |  319929  1167166 |  171765    1316    10156     7.7 | 20.201 % |
c |      2078 |  319914  1167119 |  188942    2073    14215     6.9 | 20.206 % |
c |      3217 |  319899  1167072 |  207836    3211    23324     7.3 | 20.210 % |
c |      4926 |  319883  1167020 |  228620    4918    39701     8.1 | 20.213 % |
c |      7490 |  319867  1166968 |  251482    7480    68795     9.2 | 20.216 % |
c |     11334 |  319851  1166920 |  276630   11322   246232    21.7 | 20.221 % |
c |     17100 |  319818  1166821 |  304293   17085   363491    21.3 | 20.231 % |
c |     25750 |  319754  1166615 |  334722   25695   468109    18.2 | 20.245 % |
c |     38726 |  319690  1166397 |  368195   38657   646003    16.7 | 20.254 % |
c |     58187 |  319611  1166124 |  405014   58103  1059472    18.2 | 20.266 % |
c |     87379 |  319537  1165882 |  445516   87280  2093644    24.0 | 20.283 % |
c |    131169 |  319451  1165570 |  490067  131030  3956770    30.2 | 20.292 % |
c |    196854 |  319260  1164911 |  539074  196579  5967662    30.4 | 20.320 % |
c |    295381 |  318990  1163989 |  592981  294718 11211943    38.0 | 20.368 % |
c |    443171 |  318588  1162571 |  652280  442166 18635959    42.1 | 20.426 % |
c |    664856 |  318507  1162294 |  717508  663836 32451512    48.9 | 20.439 % |
#### 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.91 0.95 0.90 2/54 9650
Raw data (stat): 9650 (runsolver) R 9649 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541011104 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 8020 0 0 0 975 22 0 0 25 0 1 0 541011104 37838848 7627 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9238 7627 603 41 0 9197 0
vsize: 36952
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 8477 0 0 0 1974 24 0 0 25 0 1 0 541011104 39718912 8084 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9697 8084 603 41 0 9656 0
vsize: 38788
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 8670 0 0 0 2972 24 0 0 25 0 1 0 541011104 40521728 8277 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9893 8277 603 41 0 9852 0
vsize: 39572
[startup+40.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 8909 0 0 0 3972 25 0 0 25 0 1 0 541011104 41590784 8516 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10154 8516 603 41 0 10113 0
vsize: 40616
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 9277 0 0 0 4971 26 0 0 25 0 1 0 541011104 43069440 8884 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10515 8884 603 41 0 10474 0
vsize: 42060
[startup+60.0012 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 9597 0 0 0 5970 27 0 0 25 0 1 0 541011104 44277760 9204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10810 9204 603 41 0 10769 0
vsize: 43240
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 10201 0 0 0 6969 28 0 0 25 0 1 0 541011104 46956544 9808 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11464 9808 603 41 0 11423 0
vsize: 45856
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 10766 0 0 0 7968 29 0 0 25 0 1 0 541011104 49246208 10373 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12023 10373 603 41 0 11982 0
vsize: 48092
[startup+90.0026 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 11105 0 0 0 8967 31 0 0 25 0 1 0 541011104 50597888 10712 4294967295 134512640 134672761 3221224544 3221223712 134561130 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12353 10712 603 41 0 12312 0
vsize: 49412
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 11684 0 0 0 9965 33 0 0 25 0 1 0 541011104 52891648 11291 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12913 11291 603 41 0 12872 0
vsize: 51652
[startup+110.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 11969 0 0 0 10966 33 0 0 25 0 1 0 541011104 54108160 11576 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13210 11576 603 41 0 13169 0
vsize: 52840
[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 12309 0 0 0 11965 34 0 0 25 0 1 0 541011104 55451648 11916 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13538 11916 603 41 0 13497 0
vsize: 54152
[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 12744 0 0 0 12964 35 0 0 25 0 1 0 541011104 57192448 12351 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13963 12351 603 41 0 13922 0
vsize: 55852
[startup+140.035 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 13088 0 0 0 13966 35 0 0 25 0 1 0 541011104 58535936 12695 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14291 12695 603 41 0 14250 0
vsize: 57164
[startup+150.038 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 13495 0 0 0 14966 36 0 0 25 0 1 0 541011104 60809216 13102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14846 13102 603 41 0 14805 0
vsize: 59384
[startup+160.038 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 13841 0 0 0 15964 39 0 0 25 0 1 0 541011104 62156800 13448 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15175 13448 603 41 0 15134 0
vsize: 60700
[startup+170.059 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 14052 0 0 0 16965 39 0 0 25 0 1 0 541011104 62963712 13659 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15372 13660 603 41 0 15331 0
vsize: 61488
[startup+180.059 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 14223 0 0 0 17965 40 0 0 25 0 1 0 541011104 63635456 13830 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15536 13830 603 41 0 15495 0
vsize: 62144
[startup+190.061 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 14452 0 0 0 18964 41 0 0 25 0 1 0 541011104 64577536 14059 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15766 14059 603 41 0 15725 0
vsize: 63064
[startup+200.061 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 14687 0 0 0 19963 42 0 0 25 0 1 0 541011104 65523712 14294 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15997 14294 603 41 0 15956 0
vsize: 63988
[startup+210.064 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 14934 0 0 0 20963 43 0 0 25 0 1 0 541011104 66465792 14541 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16227 14541 603 41 0 16186 0
vsize: 64908
[startup+220.064 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 15102 0 0 0 21963 43 0 0 25 0 1 0 541011104 67141632 14709 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16392 14709 603 41 0 16351 0
vsize: 65568
[startup+230.07 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 15315 0 0 0 22963 43 0 0 25 0 1 0 541011104 67948544 14922 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16589 14922 603 41 0 16548 0
vsize: 66356
[startup+240.07 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 15784 0 0 0 23962 45 0 0 25 0 1 0 541011104 69836800 15391 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17050 15391 603 41 0 17009 0
vsize: 68200
[startup+250.074 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 15970 0 0 0 24962 45 0 0 25 0 1 0 541011104 70643712 15577 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17247 15577 603 41 0 17206 0
vsize: 68988
[startup+260.074 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 16176 0 0 0 25961 46 0 0 25 0 1 0 541011104 71450624 15783 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17444 15783 603 41 0 17403 0
vsize: 69776
[startup+270.076 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 16420 0 0 0 26961 46 0 0 25 0 1 0 541011104 72396800 16027 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17675 16027 603 41 0 17634 0
vsize: 70700
[startup+280.076 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 16593 0 0 0 27959 48 0 0 25 0 1 0 541011104 73068544 16200 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17839 16200 603 41 0 17798 0
vsize: 71356
[startup+290.076 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 16818 0 0 0 28959 48 0 0 25 0 1 0 541011104 74014720 16425 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18070 16425 603 41 0 18029 0
vsize: 72280
[startup+300.077 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 17368 0 0 0 29958 50 0 0 25 0 1 0 541011104 76296192 16975 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18627 16975 603 41 0 18586 0
vsize: 74508
[startup+310.077 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 18055 0 0 0 30956 52 0 0 25 0 1 0 541011104 78995456 17662 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19286 17662 603 41 0 19245 0
vsize: 77144
[startup+320.077 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 18658 0 0 0 31954 54 0 0 25 0 1 0 541011104 81547264 18265 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19909 18265 603 41 0 19868 0
vsize: 79636
[startup+330.077 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 19219 0 0 0 32953 55 0 0 25 0 1 0 541011104 83836928 18826 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20468 18826 603 41 0 20427 0
vsize: 81872
[startup+340.077 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 19810 0 0 0 33951 57 0 0 25 0 1 0 541011104 86253568 19417 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21058 19417 603 41 0 21017 0
vsize: 84232
[startup+350.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 20093 0 0 0 34950 58 0 0 25 0 1 0 541011104 87330816 19700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21321 19700 603 41 0 21280 0
vsize: 85284
[startup+360.077 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 20324 0 0 0 35950 58 0 0 25 0 1 0 541011104 88276992 19931 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21552 19931 603 41 0 21511 0
vsize: 86208
[startup+370.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 20562 0 0 0 36950 59 0 0 25 0 1 0 541011104 89214976 20169 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21781 20169 603 41 0 21740 0
vsize: 87124
[startup+380.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 20922 0 0 0 37949 61 0 0 25 0 1 0 541011104 91734016 20529 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22396 20529 603 41 0 22355 0
vsize: 89584
[startup+390.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 21229 0 0 0 38948 61 0 0 25 0 1 0 541011104 92950528 20836 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22693 20836 603 41 0 22652 0
vsize: 90772
[startup+400.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 21426 0 0 0 39948 62 0 0 25 0 1 0 541011104 93753344 21033 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22889 21033 603 41 0 22848 0
vsize: 91556
[startup+410.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 21566 0 0 0 40947 63 0 0 25 0 1 0 541011104 94294016 21173 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23021 21173 603 41 0 22980 0
vsize: 92084
[startup+420.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 21812 0 0 0 41946 64 0 0 25 0 1 0 541011104 95240192 21419 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23252 21419 603 41 0 23211 0
vsize: 93008
[startup+430.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 22170 0 0 0 42945 65 0 0 25 0 1 0 541011104 96727040 21777 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23615 21777 603 41 0 23574 0
vsize: 94460
[startup+440.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 22266 0 0 0 43945 65 0 0 25 0 1 0 541011104 97132544 21873 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23714 21873 603 41 0 23673 0
vsize: 94856
[startup+450.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 22571 0 0 0 44944 67 0 0 25 0 1 0 541011104 98349056 22178 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24011 22178 603 41 0 23970 0
vsize: 96044
[startup+460.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 22805 0 0 0 45943 68 0 0 25 0 1 0 541011104 99295232 22412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24242 22412 603 41 0 24201 0
vsize: 96968
[startup+470.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 22998 0 0 0 46942 68 0 0 25 0 1 0 541011104 100102144 22605 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24439 22605 603 41 0 24398 0
vsize: 97756
[startup+480.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 23450 0 0 0 47941 70 0 0 25 0 1 0 541011104 101847040 23057 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24865 23057 603 41 0 24824 0
vsize: 99460
[startup+490.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 23788 0 0 0 48941 70 0 0 25 0 1 0 541011104 103190528 23395 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25193 23395 603 41 0 25152 0
vsize: 100772
[startup+500.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 24158 0 0 0 49940 71 0 0 25 0 1 0 541011104 104677376 23765 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25556 23765 603 41 0 25515 0
vsize: 102224
[startup+510.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 24377 0 0 0 50940 72 0 0 25 0 1 0 541011104 105619456 23984 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25786 23984 603 41 0 25745 0
vsize: 103144
[startup+520.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 24575 0 0 0 51940 72 0 0 25 0 1 0 541011104 106426368 24182 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25983 24182 603 41 0 25942 0
vsize: 103932
[startup+530.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 24931 0 0 0 52939 73 0 0 25 0 1 0 541011104 107778048 24538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26313 24538 603 41 0 26272 0
vsize: 105252
[startup+540.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 25272 0 0 0 53938 74 0 0 25 0 1 0 541011104 109252608 24879 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26673 24879 603 41 0 26632 0
vsize: 106692
[startup+550.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 25612 0 0 0 54937 75 0 0 25 0 1 0 541011104 110596096 25219 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27001 25219 603 41 0 26960 0
vsize: 108004
[startup+560.082 s]
Raw data (loadavg): 1.37 1.08 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 25951 0 0 0 55936 76 0 0 25 0 1 0 541011104 111943680 25558 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27330 25558 603 41 0 27289 0
vsize: 109320
[startup+570.082 s]
Raw data (loadavg): 1.32 1.08 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 26395 0 0 0 56934 78 0 0 25 0 1 0 541011104 113692672 26002 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27757 26002 603 41 0 27716 0
vsize: 111028
[startup+580.084 s]
Raw data (loadavg): 1.27 1.08 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 26901 0 0 0 57933 79 0 0 25 0 1 0 541011104 115834880 26508 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28280 26508 603 41 0 28239 0
vsize: 113120
[startup+590.083 s]
Raw data (loadavg): 1.23 1.07 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 27541 0 0 0 58932 81 0 0 25 0 1 0 541011104 118382592 27148 4294967295 134512640 134672761 3221224544 3221223712 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28902 27148 603 41 0 28861 0
vsize: 115608
[startup+600.084 s]
Raw data (loadavg): 1.19 1.07 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 27896 0 0 0 59930 83 0 0 25 0 1 0 541011104 119861248 27503 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29263 27503 603 41 0 29222 0
vsize: 117052
[startup+610.084 s]
Raw data (loadavg): 1.16 1.07 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 28195 0 0 0 60930 83 0 0 25 0 1 0 541011104 121077760 27802 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29560 27802 603 41 0 29519 0
vsize: 118240
[startup+620.085 s]
Raw data (loadavg): 1.14 1.06 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 28323 0 0 0 61930 84 0 0 25 0 1 0 541011104 121618432 27930 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29692 27930 603 41 0 29651 0
vsize: 118768
[startup+630.084 s]
Raw data (loadavg): 1.11 1.06 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 28554 0 0 0 62929 85 0 0 25 0 1 0 541011104 122425344 28161 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29889 28161 603 41 0 29848 0
vsize: 119556
[startup+640.084 s]
Raw data (loadavg): 1.10 1.06 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 28769 0 0 0 63929 85 0 0 25 0 1 0 541011104 123367424 28376 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30119 28376 603 41 0 30078 0
vsize: 120476
[startup+650.086 s]
Raw data (loadavg): 1.08 1.06 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 28963 0 0 0 64928 86 0 0 25 0 1 0 541011104 124182528 28570 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30318 28570 603 41 0 30277 0
vsize: 121272
[startup+660.085 s]
Raw data (loadavg): 1.07 1.05 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 29187 0 0 0 65928 86 0 0 25 0 1 0 541011104 124993536 28794 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30516 28794 603 41 0 30475 0
vsize: 122064
[startup+670.086 s]
Raw data (loadavg): 1.06 1.05 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 29536 0 0 0 66927 87 0 0 25 0 1 0 541011104 126476288 29143 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30878 29143 603 41 0 30837 0
vsize: 123512
[startup+680.087 s]
Raw data (loadavg): 1.05 1.05 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 29878 0 0 0 67926 88 0 0 25 0 1 0 541011104 127815680 29485 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31205 29485 603 41 0 31164 0
vsize: 124820
[startup+690.086 s]
Raw data (loadavg): 1.04 1.05 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 30136 0 0 0 68925 90 0 0 25 0 1 0 541011104 128892928 29743 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31468 29743 603 41 0 31427 0
vsize: 125872
[startup+700.086 s]
Raw data (loadavg): 1.03 1.05 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 30349 0 0 0 69924 91 0 0 25 0 1 0 541011104 129703936 29956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31666 29956 603 41 0 31625 0
vsize: 126664
[startup+710.087 s]
Raw data (loadavg): 1.03 1.04 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 30543 0 0 0 70924 91 0 0 25 0 1 0 541011104 130514944 30150 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31864 30150 603 41 0 31823 0
vsize: 127456
[startup+720.088 s]
Raw data (loadavg): 1.02 1.04 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 30669 0 0 0 71924 91 0 0 25 0 1 0 541011104 131055616 30276 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31996 30276 603 41 0 31955 0
vsize: 127984
[startup+730.088 s]
Raw data (loadavg): 1.02 1.04 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 31284 0 0 0 72922 93 0 0 25 0 1 0 541011104 133476352 30891 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32587 30891 603 41 0 32546 0
vsize: 130348
[startup+740.087 s]
Raw data (loadavg): 1.02 1.04 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 31525 0 0 0 73921 94 0 0 25 0 1 0 541011104 134410240 31132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32815 31132 603 41 0 32774 0
vsize: 131260
[startup+750.088 s]
Raw data (loadavg): 1.01 1.04 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 31658 0 0 0 74921 95 0 0 25 0 1 0 541011104 134950912 31265 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32947 31265 603 41 0 32906 0
vsize: 131788
[startup+760.088 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 31856 0 0 0 75920 95 0 0 25 0 1 0 541011104 135761920 31463 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33145 31463 603 41 0 33104 0
vsize: 132580
[startup+770.089 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 32019 0 0 0 76920 96 0 0 25 0 1 0 541011104 136437760 31626 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 31626 603 41 0 33269 0
vsize: 133240
[startup+780.089 s]
Raw data (loadavg): 1.01 1.03 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 32180 0 0 0 77920 96 0 0 25 0 1 0 541011104 137113600 31787 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33475 31787 603 41 0 33434 0
vsize: 133900
[startup+790.09 s]
Raw data (loadavg): 1.00 1.03 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 32397 0 0 0 78919 97 0 0 25 0 1 0 541011104 137920512 32004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33672 32004 603 41 0 33631 0
vsize: 134688
[startup+800.09 s]
Raw data (loadavg): 1.00 1.03 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 32536 0 0 0 79919 97 0 0 25 0 1 0 541011104 138461184 32143 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33804 32143 603 41 0 33763 0
vsize: 135216
[startup+810.091 s]
Raw data (loadavg): 1.00 1.03 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 32617 0 0 0 80919 98 0 0 25 0 1 0 541011104 138866688 32224 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33903 32224 603 41 0 33862 0
vsize: 135612
[startup+820.092 s]
Raw data (loadavg): 1.00 1.03 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 32792 0 0 0 81919 98 0 0 25 0 1 0 541011104 139538432 32399 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34067 32399 603 41 0 34026 0
vsize: 136268
[startup+830.092 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 33183 0 0 0 82918 99 0 0 25 0 1 0 541011104 141160448 32790 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34463 32790 603 41 0 34422 0
vsize: 137852
[startup+840.091 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 33305 0 0 0 83917 100 0 0 25 0 1 0 541011104 141557760 32912 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34560 32912 603 41 0 34519 0
vsize: 138240
[startup+850.092 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 33439 0 0 0 84917 100 0 0 25 0 1 0 541011104 142110720 33046 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34695 33046 603 41 0 34654 0
vsize: 138780
[startup+860.092 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 33580 0 0 0 85917 101 0 0 25 0 1 0 541011104 142651392 33187 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34827 33187 603 41 0 34786 0
vsize: 139308
[startup+870.093 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 34117 0 0 0 86916 102 0 0 25 0 1 0 541011104 144941056 33724 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35386 33724 603 41 0 35345 0
vsize: 141544
[startup+880.094 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 34712 0 0 0 87914 104 0 0 25 0 1 0 541011104 147365888 34319 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35978 34319 603 41 0 35937 0
vsize: 143912
[startup+890.094 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 35162 0 0 0 88912 106 0 0 25 0 1 0 541011104 149114880 34769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36405 34769 603 41 0 36364 0
vsize: 145620
[startup+900.094 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 35807 0 0 0 89910 108 0 0 25 0 1 0 541011104 151789568 35414 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37058 35414 603 41 0 37017 0
vsize: 148232
[startup+910.094 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 36314 0 0 0 90909 109 0 0 25 0 1 0 541011104 153792512 35921 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37547 35921 603 41 0 37506 0
vsize: 150188
[startup+920.095 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 36835 0 0 0 91907 112 0 0 25 0 1 0 541011104 158031872 36442 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38582 36442 603 41 0 38541 0
vsize: 154328
[startup+930.095 s]
Raw data (loadavg): 1.00 1.02 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 37316 0 0 0 92906 113 0 0 25 0 1 0 541011104 160051200 36923 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39075 36923 603 41 0 39034 0
vsize: 156300
[startup+940.095 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 37791 0 0 0 93904 115 0 0 25 0 1 0 541011104 161935360 37398 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39535 37398 603 41 0 39494 0
vsize: 158140
[startup+950.096 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 38255 0 0 0 94903 116 0 0 25 0 1 0 541011104 163823616 37862 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39996 37862 603 41 0 39955 0
vsize: 159984
[startup+960.095 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 38717 0 0 0 95902 118 0 0 25 0 1 0 541011104 165744640 38324 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40465 38324 603 41 0 40424 0
vsize: 161860
[startup+970.096 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 39197 0 0 0 96900 120 0 0 25 0 1 0 541011104 167768064 38804 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40959 38804 603 41 0 40918 0
vsize: 163836
[startup+980.096 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 39510 0 0 0 97898 122 0 0 25 0 1 0 541011104 168988672 39117 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41257 39117 603 41 0 41216 0
vsize: 165028
[startup+990.095 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 39905 0 0 0 98897 123 0 0 25 0 1 0 541011104 170614784 39512 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41654 39512 603 41 0 41613 0
vsize: 166616
[startup+1000.1 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 40050 0 0 0 99897 124 0 0 25 0 1 0 541011104 171151360 39657 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41785 39657 603 41 0 41744 0
vsize: 167140
[startup+1010.1 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 40212 0 0 0 100897 124 0 0 25 0 1 0 541011104 171827200 39819 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41950 39819 603 41 0 41909 0
vsize: 167800
[startup+1020.1 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 40422 0 0 0 101896 124 0 0 25 0 1 0 541011104 172638208 40029 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42148 40029 603 41 0 42107 0
vsize: 168592
[startup+1030.1 s]
Raw data (loadavg): 1.00 1.01 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 40653 0 0 0 102896 125 0 0 25 0 1 0 541011104 173584384 40260 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42379 40260 603 41 0 42338 0
vsize: 169516
[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 40915 0 0 0 103895 126 0 0 25 0 1 0 541011104 174526464 40522 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42609 40522 603 41 0 42568 0
vsize: 170436
[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 41939 0 0 0 104893 128 0 0 25 0 1 0 541011104 178696192 41546 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43627 41546 603 41 0 43586 0
vsize: 174508
[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 42480 0 0 0 105892 129 0 0 25 0 1 0 541011104 180994048 42087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44188 42087 603 41 0 44147 0
vsize: 176752
[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 43057 0 0 0 106890 132 0 0 25 0 1 0 541011104 183287808 42664 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44748 42664 603 41 0 44707 0
vsize: 178992
[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 43597 0 0 0 107888 134 0 0 25 0 1 0 541011104 185458688 43204 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45278 43204 603 41 0 45237 0
vsize: 181112
[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 44092 0 0 0 108887 135 0 0 25 0 1 0 541011104 187482112 43699 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45772 43699 603 41 0 45731 0
vsize: 183088
[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 44264 0 0 0 109887 135 0 0 25 0 1 0 541011104 188153856 43871 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45936 43871 603 41 0 45895 0
vsize: 183744
[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 44413 0 0 0 110886 136 0 0 25 0 1 0 541011104 188690432 44020 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46067 44020 603 41 0 46026 0
vsize: 184268
[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 45289 0 0 0 111884 139 0 0 25 0 1 0 541011104 192323584 44896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46954 44896 603 41 0 46913 0
vsize: 187816
[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 46188 0 0 0 112881 142 0 0 25 0 1 0 541011104 195936256 45795 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47836 45795 603 41 0 47795 0
vsize: 191344
[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 47061 0 0 0 113879 144 0 0 25 0 1 0 541011104 199561216 46668 4294967295 134512640 134672761 3221224544 3221223648 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48721 46668 603 41 0 48680 0
vsize: 194884
[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 47507 0 0 0 114877 146 0 0 25 0 1 0 541011104 201306112 47114 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49147 47114 603 41 0 49106 0
vsize: 196588
[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 48014 0 0 0 115875 147 0 0 25 0 1 0 541011104 203452416 47621 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49671 47621 603 41 0 49630 0
vsize: 198684
[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 48586 0 0 0 116873 149 0 0 25 0 1 0 541011104 205733888 48193 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50228 48193 603 41 0 50187 0
vsize: 200912
[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 49328 0 0 0 117872 151 0 0 25 0 1 0 541011104 208691200 48935 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50950 48935 603 41 0 50909 0
vsize: 203800
[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 50197 0 0 0 118870 153 0 0 25 0 1 0 541011104 212205568 49804 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51808 49804 603 41 0 51767 0
vsize: 207232
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 9650
Raw data (stat): 9650 (minisat+) R 9649 11931 11930 0 -1 0 50939 0 0 0 119867 156 0 0 25 0 1 0 541011104 215302144 50546 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52564 50546 603 41 0 52523 0
vsize: 210256
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 9650
Raw data (stat): 9650 (minisat+) Z 9649 11931 11930 0 -1 12 50941 0 0 0 119867 166 0 0 25 0 1 0 541011104 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.2
CPU time (s): 1200.33
CPU user time (s): 1198.67
CPU system time (s): 1.66375
CPU usage (%): 100.012
Max. virtual memory (Kb): 210256
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####