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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-30:30:4.5:0.5:100.opb
MD5SUM	bc393d4b1cc38ed414c3e21eb8bc6b60
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	56
Optimality of the best value was proved	NO
Number of terms in the objective function	4447
Biggest coefficient in the objective function	2128
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	12580
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	2128
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	12580
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06284
Number of variables	4447
Total number of constraints	9372
Number of constraints which are clauses	4205
Number of constraints which are cardinality constraints (but not clauses)	5167
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	27
Trace number 5316

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-13 23:21:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3756 boxname=wulflinc18 idbench=372 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bc393d4b1cc38ed414c3e21eb8bc6b60  /oldhome/oroussel/tmp/wulflinc18/normalized-30:30:4.5:0.5:100.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc18/normalized-30:30:4.5:0.5:100.opb /oldhome/oroussel/tmp/wulflinc18/normalized-30:30:4.5:0.5:100.opb
IDLAUNCH: 3756
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        887248 kB
Buffers:         34284 kB
Cached:          77120 kB
SwapCached:        320 kB
Active:          54140 kB
Inactive:        60480 kB
HighTotal:      131008 kB
HighFree:        49952 kB
LowTotal:       903652 kB
LowFree:        837296 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27260 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:41:31 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 3756 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4925 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 740]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 739]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 738]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 737]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 736]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 735]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 734]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 733]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 732]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 731]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 730]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 729]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 728]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 727]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 726]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 725]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 724]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 723]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 722]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 721]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 720]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 719]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 718]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 717]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 716]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 715]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 714]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 713]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 712]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 711]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 710]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 709]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 708]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 707]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 706]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 705]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 704]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 703]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 702]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 701]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 700]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 699]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 698]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 697]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 696]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 695]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 694]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 693]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 692]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 691]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 690]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 689]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 688]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 686]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 685]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 684]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 683]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 682]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 681]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 680]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 679]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 678]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 677]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 676]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 675]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 674]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 673]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 672]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 671]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 670]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 669]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 668]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 667]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 666]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 665]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 664]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 663]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 662]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 661]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 660]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 659]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 658]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 657]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 656]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 655]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 654]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 653]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 652]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 651]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 650]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 649]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 648]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 647]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 646]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 645]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 644]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 643]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 642]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 641]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 640]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 639]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 638]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 637]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 636]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 635]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 634]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 633]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 632]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 631]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 630]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 629]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 628]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 627]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 626]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 625]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 624]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 623]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 622]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 621]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 620]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 619]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 618]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 617]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 616]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 615]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 614]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 613]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 612]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 611]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 610]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 609]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 608]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 607]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 606]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 605]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 604]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 603]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 602]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 601]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 600]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 599]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 598]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 597]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 596]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 595]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 594]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 593]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 592]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 591]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 590]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 589]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 588]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 587]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 586]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 585]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 584]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 583]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 582]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 581]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 580]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 579]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 578]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 577]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 576]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 575]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 574]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 573]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 572]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 571]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 570]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 569]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 568]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 567]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 566]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 565]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 564]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 563]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 562]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 561]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 560]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 559]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 558]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 557]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 556]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 555]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 554]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 553]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 552]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 551]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 550]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 549]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 548]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 547]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 546]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 545]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 544]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 543]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 542]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 541]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 540]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 539]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 538]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 537]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 536]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 535]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 534]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 533]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 532]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 531]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 530]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 529]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 528]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 527]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 526]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 525]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 524]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 523]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 522]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 521]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 520]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 519]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 518]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 517]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 516]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 515]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 514]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 513]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 512]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 511]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 510]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 509]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 508]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 507]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 506]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 505]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 504]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 503]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 502]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 501]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 500]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 499]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 498]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 497]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 496]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 495]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 494]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 493]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 492]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 491]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 490]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 489]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 488]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 487]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 486]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 485]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 484]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 483]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 482]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 481]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 480]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 479]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 478]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 477]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 476]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 475]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 474]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 473]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 472]---> Adder-cost: 43   maxlim: 2   bits: 3/2
c ---[ 471]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 470]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 469]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 468]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 467]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 466]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 465]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 464]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 463]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 462]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 461]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 460]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 459]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 458]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 457]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 456]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 455]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 454]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 453]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 452]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 451]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 450]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 449]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 448]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 447]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 446]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 445]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 444]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 443]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 442]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 441]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 440]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 439]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 438]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 437]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 436]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 435]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 434]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 433]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 432]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 431]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 430]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 429]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 428]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 427]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 426]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 425]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 424]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 423]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 422]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 421]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 420]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 419]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 418]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 417]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 416]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 415]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 414]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 413]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 412]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 411]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 410]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 409]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 408]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 407]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 406]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 405]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 404]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 403]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 402]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 401]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 400]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 399]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 398]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 397]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 396]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 395]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 394]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 393]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 392]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 391]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 390]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 389]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 388]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 387]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 386]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 385]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 384]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 383]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 382]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 381]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 380]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 379]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 378]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 377]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 376]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 375]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 374]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 373]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 372]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 371]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 370]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 369]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 368]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 367]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 366]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 365]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 364]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 363]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 362]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 361]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 360]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 359]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 358]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 357]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 356]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 355]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 354]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 353]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 352]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 351]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 350]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 349]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 348]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 347]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 346]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 345]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 344]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 343]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 342]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 341]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 340]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 339]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 338]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 337]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 336]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 335]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 334]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 333]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 332]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 331]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 330]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 329]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 328]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 327]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 326]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 325]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 324]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 323]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 322]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 321]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 320]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 319]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 318]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 317]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 316]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 315]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 314]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 313]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 312]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 311]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 310]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 309]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 308]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 307]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 306]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 305]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 304]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 303]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 302]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 301]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 300]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 299]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 298]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 297]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 296]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 295]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 294]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 293]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 292]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 291]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 290]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 289]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 288]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 287]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 286]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 285]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 284]---> Adder-cost: 43   maxlim: 2   bits: 3/2
c ---[ 283]---> Adder-cost: 43   maxlim: 2   bits: 3/2
c ---[ 282]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 281]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 280]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 279]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 278]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 277]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 276]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 275]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 274]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 273]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 272]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 271]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 270]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 269]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 268]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 267]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 266]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 265]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 264]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 263]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 262]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 261]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 260]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 259]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 258]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 257]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 256]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 255]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 254]---> Adder-cost: 41   maxlim: 2   bits: 3/2
c ---[ 253]---> Adder-cost: 43   maxlim: 2   bits: 3/2
c ---[ 252]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 251]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 250]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 249]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 248]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 247]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 246]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 245]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 244]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 243]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 242]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 241]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 240]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 239]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 238]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 237]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 236]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 235]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 234]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 233]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 232]---> Adder-cost: 18   maxlim: 2   bits: 3/2
c ---[ 231]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 230]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 229]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 228]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 227]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 226]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 225]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 224]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 223]---> Adder-cost: 36   maxlim: 2   bits: 3/2
c ---[ 222]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 221]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 220]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 219]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 218]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 217]---> Adder-cost: 34   maxlim: 2   bits: 3/2
c ---[ 216]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 215]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 214]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 213]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 212]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 211]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 210]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 209]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 208]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 207]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 206]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 205]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 204]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 203]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 202]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 201]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 200]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 199]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 198]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 197]---> Adder-cost: 25   maxlim: 2   bits: 3/2
c ---[ 196]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 195]---> Adder-cost: 32   maxlim: 2   bits: 3/2
c ---[ 194]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 193]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 192]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 191]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 190]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 189]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 188]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 187]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 186]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 185]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 184]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 183]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 182]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 181]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 180]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 179]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 178]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 177]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 176]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 175]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 174]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 173]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 172]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 171]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 170]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 169]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 168]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 167]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 166]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 165]---> Adder-cost: 29   maxlim: 2   bits: 3/2
c ---[ 164]---> Adder-cost: 27   maxlim: 2   bits: 3/2
c ---[ 163]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 162]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 161]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 160]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 159]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 158]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 157]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 156]---> Adder-cost: 18   maxlim: 2   bits: 3/2
c ---[ 155]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 154]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 153]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 152]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 151]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 150]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 149]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 148]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 147]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 146]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 145]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 144]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 143]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 142]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 141]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 140]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 139]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 138]---> Adder-cost: 17   maxlim: 1   bits: 2/1
c ---[ 137]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 136]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 135]---> Adder-cost: 22   maxlim: 2   bits: 3/2
c ---[ 134]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 133]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 132]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 131]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 130]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 129]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 128]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 127]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 126]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 125]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 124]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 123]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 122]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 121]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 120]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 119]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 118]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 117]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[ 116]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 113]---> Adder-cost: 3   maxlim: 1   bits: 2/1
c ---[ 112]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 111]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[ 110]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 109]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 108]---> Adder-cost: 11   maxlim: 1   bits: 2/1
c ---[ 107]---> Adder-cost: 20   maxlim: 2   bits: 3/2
c ---[ 106]---> Adder-cost: 15   maxlim: 2   bits: 3/2
c ---[ 105]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 104]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 103]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 102]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 101]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[ 100]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  99]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  98]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  97]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  96]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  95]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  94]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  93]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  92]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  91]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  90]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  89]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  87]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  80]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 8   maxlim: 1   bits: 2/1
c ---[  77]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  75]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  74]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  73]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  72]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  71]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  70]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  69]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  68]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  67]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  66]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  64]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  63]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  62]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  61]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  60]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  59]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  58]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  57]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  56]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  55]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  54]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  53]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  52]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  51]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  50]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  49]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  47]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  46]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  45]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  44]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  43]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  42]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  41]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  40]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  39]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  38]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  37]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  36]---> Adder-cost: 13   maxlim: 2   bits: 3/2
c ---[  35]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  34]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  32]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  29]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  28]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  27]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  26]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  25]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  24]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  23]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  22]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  21]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  19]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  18]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  17]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  16]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  15]---> Adder-cost: 8   maxlim: 2   bits: 3/2
c ---[  14]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  13]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[  12]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[   8]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   7]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[   6]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[   5]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   4]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[   1]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   93809   328308 |   31269       0        0     nan |  0.000 % |
c |       101 |   93803   328291 |   34395     100      431     4.3 |  6.666 % |
c |       251 |   93797   328274 |   37835     248     1142     4.6 |  6.671 % |
c |       476 |   93791   328257 |   41619     472     2199     4.7 |  6.676 % |
c |       813 |   93791   328257 |   45780     809     3719     4.6 |  6.676 % |
c |      1319 |   93791   328257 |   50359    1315     6498     4.9 |  6.676 % |
c |      2078 |   93791   328257 |   55394    2074    10614     5.1 |  6.676 % |
c |      3217 |   93785   328240 |   60934    3212    16565     5.2 |  6.680 % |
c |      4925 |   93785   328240 |   67027    4920    25636     5.2 |  6.680 % |
c |      7487 |   93779   328223 |   73730    7481    39384     5.3 |  6.685 % |
c |     11331 |   93767   328189 |   81103   11323    60871     5.4 |  6.695 % |
c ==============================================================================
c [1mFound solution: 1045[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10872   maxlim: 7279   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11694 |  169790   599672 |   56596   11686    63086     5.4 |  6.695 % |
c |     11794 |  169790   599672 |   62255   11786    63601     5.4 |  4.419 % |
c |     11944 |  169790   599672 |   68481   11936    64324     5.4 |  4.419 % |
c |     12169 |  169790   599672 |   75329   12161    65539     5.4 |  4.419 % |
c |     12506 |  169790   599672 |   82862   12498    67314     5.4 |  4.419 % |
c |     13013 |  169784   599655 |   91148   13004    86495     6.7 |  4.422 % |
c |     13772 |  169784   599655 |  100263   13763    90488     6.6 |  4.422 % |
c |     14911 |  169775   599624 |  110289   14900    96937     6.5 |  4.425 % |
c |     16622 |  169775   599624 |  121318   16611   107564     6.5 |  4.425 % |
c |     19185 |  169775   599624 |  133450   19174   124430     6.5 |  4.425 % |
c |     23029 |  169775   599624 |  146795   23018   151807     6.6 |  4.425 % |
c |     28795 |  169775   599624 |  161474   28784   193506     6.7 |  4.425 % |
c |     37445 |  169775   599624 |  177622   37434   257546     6.9 |  4.425 % |
c |     50419 |  169760   599573 |  195384   50405   370782     7.4 |  4.432 % |
c ==============================================================================
c [1mFound solution: 703[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7621   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50748 |  169783   599690 |   56594   50734   373369     7.4 |  4.432 % |
c |     50848 |  169783   599690 |   62253   50834   374037     7.4 |  4.446 % |
c |     50998 |  169783   599690 |   68478   50984   375096     7.4 |  4.446 % |
c |     51223 |  169783   599690 |   75326   51209   376740     7.4 |  4.446 % |
c |     51560 |  169783   599690 |   82859   51546   382269     7.4 |  4.446 % |
c |     52066 |  169783   599690 |   91145   52052   385413     7.4 |  4.446 % |
c |     52825 |  169783   599690 |  100259   52811   390672     7.4 |  4.446 % |
c |     53964 |  169783   599690 |  110285   53950   399426     7.4 |  4.446 % |
c |     55672 |  169783   599690 |  121314   55658   414452     7.4 |  4.446 % |
c |     58234 |  169783   599690 |  133445   58220   433279     7.4 |  4.446 % |
c |     62078 |  169783   599690 |  146790   62064   464525     7.5 |  4.446 % |
c |     67847 |  169783   599690 |  161469   67833   710196    10.5 |  4.446 % |
c |     76497 |  169783   599690 |  177616   76483  2058451    26.9 |  4.446 % |
c |     89471 |  169783   599690 |  195377   89457  2654603    29.7 |  4.446 % |
c |    108932 |  169783   599690 |  214915  108918  4566858    41.9 |  4.446 % |
c |    138124 |  169777   599673 |  236407  138105  7963642    57.7 |  4.449 % |
c ==============================================================================
c [1mFound solution: 634[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 7690   bits: 14/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    145911 |  169789   599744 |   56596  145892  8133222    55.7 |  4.449 % |
c |    146011 |  169789   599744 |   62255   26765  1419155    53.0 |  4.461 % |
c |    146161 |  169789   599744 |   68481   26915  1420065    52.8 |  4.461 % |
c |    146388 |  169789   599744 |   75329   27142  1421458    52.4 |  4.461 % |
c |    146726 |  169789   599744 |   82862   27480  1423397    51.8 |  4.461 % |
c |    147232 |  169789   599744 |   91148   27986  1426393    51.0 |  4.461 % |
c |    147991 |  169789   599744 |  100263   28745  1430562    49.8 |  4.461 % |
c |    149130 |  169789   599744 |  110289   29884  1437121    48.1 |  4.461 % |
c |    150838 |  169789   599744 |  121318   31592  1447896    45.8 |  4.461 % |
c |    153400 |  169789   599744 |  133450   34154  1463891    42.9 |  4.461 % |
c |    157244 |  169789   599744 |  146795   37998  1977749    52.0 |  4.461 % |
c |    163010 |  169783   599727 |  161474   43762  2027251    46.3 |  4.464 % |
c |    171659 |  169783   599727 |  177622   52411  2191074    41.8 |  4.464 % |
c |    184634 |  169783   599727 |  195384   65386  2486435    38.0 |  4.464 % |
c |    204095 |  169783   599727 |  214923   84847  5577257    65.7 |  4.464 % |
c |    233289 |  169783   599727 |  236415  114041  6023584    52.8 |  4.464 % |
c |    277080 |  169783   599727 |  260057  157832 10277633    65.1 |  4.464 % |
c |    342764 |  169783   599727 |  286062  223516 18530520    82.9 |  4.464 % |
c |    441290 |  169783   599727 |  314669   53365  1603105    30.0 |  4.464 % |
c |    589082 |  169783   599727 |  346135  201157 17885054    88.9 |  4.464 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -v3896 -v3446 -v3326 v3226 v3142 -v1870 -v192 v170 -v3447 v3330 -v1960 -v1871 -v3895 -v3451 v3329 v3227 v3146 -v1959 -v191 v169 -v3450 v3331 v3228 v3144 -v1961 -v1477 -v1436 -v195 -v172 v3901 -v3448 v3335 -v3231 -v2283 -v1962 -v1851 -v1690 -v1476 -v1435 -v217 v3899 -v3449 v3334 -v3229 -v3145 -v2287 v1963 -v1689 -v1482 v1437 -v196 -v173 v3332 -v3230 -v3149 -v2082 -v1970 -v1850 -v1691 -v1481 v1438 -v216 -v175 v3900 -v3333 -v2440 v1964 -v1694 -v1483 v1439 -v220 -v176 -v4136 -v3904 -v3755 -v2439 v1965 -v1856 v1693 v1487 -v1446 -v1403 v4135 -v2445 v1966 -v1854 -v1830 v1698 v1486 -v1440 -v221 v4137 -v3758 -v3556 -v2444 -v1829 v1697 v1484 -v1441 -v4333 v4140 -v3759 -v3560 v2576 -v2446 -v1855 -v1831 v1695 -v1485 -v1442 v577 -v4332 v4139 -v3730 -v3484 v2575 -v2450 -v1859 -v1832 v1696 v576 -v4338 v4144 -v3483 -v2449 -v1833 v578 v242 -v4337 v4143 -v3733 -v3485 v2577 -v2447 -v2395 -v1840 -v1570 v579 v241 -v4339 v4141 -v3734 v3488 -v2579 -v2448 -v1834 -v1574 v580 -v4343 v4142 v3487 -v2394 v2378 -v1835 -v973 -v587 v243 -v4342 v3492 -v2580 -v2398 v2377 -v1836 v581 -v245 -v4340 -v3999 v3491 -v2582 v2379 v582 -v4341 v3775 v3489 -v2583 -v2399 v4438 -v583 -v246 v3774 v3490 -v1199 v248 v4439 v4440 -v249 v3781 v4441 -v2358 -v2202 v3780 -v2942 v2362 -v3778 v2941 v2201 -v1089 -v3779 -v3891 -v3445 -v3223 v3141 v2722 v1872 -v166 -v3444 -v3325 v3225 -v2726 -v3897 -v3455 -v3327 v3224 v3147 -v193 v171 v3328 v3232 -v197 -v174 v3902 -v3339 -v3150 -v2282 -v2078 v1973 -v1876 -v1846 v178 -v3148 -v2286 v1974 -v1478 -v177 v3905 -v2081 -v1969 -v1897 -v1852 -v1479 -v1449 -v1399 v218 -v199 v3903 v1692 v1480 -v1450 v222 -v200 -v3754 -v1967 v1857 -v1706 v1491 -v1445 -v1402 -v2441 -v1702 v3760 -v3555 -v2442 -v1860 -v1701 -v1443 v224 v4138 -v3559 -v2571 -v2443 -v1858 -v225 v4152 -v3729 -v3375 -v2570 -v2454 -v2182 -v1843 -v4334 v4148 -v3379 -v1844 -v237 -v4335 v4147 -v3800 -v3763 -v3735 v2578 -v1839 -v1569 -v1042 v969 -v590 v236 -v4336 -v3486 -v2581 -v1573 -v1046 -v591 -v4347 -v3995 v3500 v2585 -v2396 -v1837 -v1378 -v972 -v586 v244 v3496 v2584 -v2400 -v247 -v3998 v3738 -v3495 -v1195 -v584 v251 v2380 v250 -v4020 -v2402 -v2388 -v1198 v4024 v3776 -v2403 -v2384 v3777 -v2383 v3785 v2465 -v2357 -v2198 -v1092 v2938 -v2469 v2361 -v1093 v2937 v2203 -v1088 -v3289 -v1086 -v3293 -v3458 v3139 v2721 v1873 -v188 -v3890 -v3459 v3222 v3143 -v2725 -v165 -v4092 -v4047 -v3892 -v3454 v3342 v3240 v3140 v1972 v1877 -v194 -v167 -v4096 -v3898 v3343 -v3236 -v3151 v1971 -v1875 -v212 -v198 v168 v3894 -v3452 -v3354 -v3338 -v3235 v2284 -v2077 -v1893 -v1448 -v211 -v202 -v182 v3906 -v2288 -v1845 -v1447 -v201 -v3750 -v3336 v2083 -v1896 -v1847 -v1703 -v1494 -v1398 v219 -v1853 -v1705 v1495 v223 -v3756 v2290 -v2010 -v1968 v1849 v1490 -v1404 -v1170 v227 v2291 -v1861 -v1174 v226 v4149 v3761 -v3725 -v3684 -v3557 -v2457 -v2178 -v2086 -v1842 -v1699 -v1488 -v1444 -v49 v4151 -v3561 -v2458 -v1841 -v53 -v3796 -v3764 -v3731 v3374 -v2453 -v2181 -v1700 -v1407 -v589 -v3762 -v3378 v2572 -v2390 -v588 -v4350 -v4145 -v3799 -v3736 -v3563 -v3497 v2573 -v2451 -v2389 -v1571 -v1374 -v1124 -v1041 v968 -v4351 -v3564 -v3499 v2574 -v1575 -v1045 v238 -v4346 -v4146 -v3994 v3739 -v2589 -v2397 -v1838 -v1377 -v974 v239 v3737 -v2401 v240 -v4344 -v4000 -v3493 -v3425 v2405 -v2385 -v1577 -v1194 -v585 v255 -v3429 v2404 -v2387 -v1578 -v4019 -v3494 -v1200 v977 v4023 v4003 -v3788 -v2381 -v1091 v3789 -v1090 v3784 v2464 -v2382 v2359 -v1203 v873 -v2468 v2363 -v2197 -v3782 v2199 v2939 v2204 v3288 v2940 -v2795 -v2365 -v1087 -v3292 v2799 -v2366 v4442 -v4043 -v3456 -v3341 -v3237 v2723 v1874 v71 -v3340 v3239 v3138 -v2727 -v2278 v1878 -v187 v75 -v4091 -v4046 -v3350 -v3159 -v2277 -v2073 -v189 -v185 -v4095 -v3893 -v3155 -v190 -v186 -v3914 -v3453 -v3353 -v3233 -v3154 v2729 -v2490 v2285 -v2079 -v1892 -v1493 -v1394 -v206 -v181 -v3910 v2730 -v2494 v2289 -v1704 -v1492 -v213 -v3909 -v3337 -v3234 v2293 v2084 -v2006 -v1898 v1400 -v214 -v179 v3749 -v3551 v2292 -v1848 v215 v3751 -v3680 -v3550 -v2456 -v2308 -v2087 -v2009 -v1869 -v1405 -v1169 v511 -v231 v4150 -v3757 -v2455 v2312 -v2085 -v1865 -v1173 v3753 -v3683 -v3558 -v2177 -v1901 -v1864 -v1489 -v1408 -v48 -v3765 -v3724 v3562 -v1565 -v1406 -v52 -v4349 -v3795 -v3726 -v3566 v3376 -v2183 -v1564 v1120 -v964 -v4348 -v3732 -v3565 -v3498 -v3380 -v3990 -v3801 v3728 -v2592 -v2452 v1572 -v1373 -v1123 v1043 v970 v3740 -v2593 v2391 -v1576 -v1047 -v3996 -v3382 -v2588 v2392 -v2186 -v1580 -v1379 -v1190 -v975 v258 -v3383 v2393 -v2386 -v1579 v259 -v4345 -v4001 -v3804 -v3424 -v2586 -v2409 -v1674 -v1196 -v1049 v978 v254 -v3428 -v1050 v976 v4021 v4004 -v3787 -v2539 -v1382 -v1201 -v252 v4025 v4002 -v3786 -v2543 v2353 v2352 v1204 -v994 -v869 -v1202 -v998 v4027 v2466 v2360 v872 -v333 -v4028 -v2470 v2364 -v337 -v3783 -v2368 -v2367 v2200 v3290 v2945 -v2794 v2472 v2212 -v3294 v2946 v2798 -v2473 v2208 -v4042 -v3457 -v3238 -v3156 v2724 v1886 -v184 v70 -v3158 v2728 v1882 -v183 v74 -v4093 v4048 -v3911 -v3349 v2732 -v1888 v1881 -v209 -v4097 -v3913 v2731 v2279 -v2072 -v210 -v3355 -v3152 -v2489 v2280 -v2074 -v1894 -v673 -v205 -v2493 v2281 v2080 v1393 -v677 -v4099 -v4051 -v3907 -v3153 v2297 v2076 -v2005 -v1899 -v1866 -v1461 v1395 -v507 -v234 -v203 -v180 -v146 -v4100 -v2088 -v1868 v1401 -v235 -v150 -v3908 -v3679 -v3358 -v2307 -v2173 -v2011 -v1902 v1397 -v1171 v510 -v230 v3752 v3552 -v3370 v2311 -v1900 -v1409 -v1175 v3791 -v3773 -v3685 v3553 -v3369 -v2179 -v1862 -v228 -v50 v3769 v3554 -v1037 v54 -v4307 v3797 v3768 -v3705 -v3570 v3377 -v2591 v2184 -v2014 -v1863 -v1369 v1177 v1119 -v1036 -v3727 -v3709 -v3381 -v2590 -v1566 -v1178 -v963 -v3802 -v3748 -v3688 -v3385 -v2187 v1567 -v1375 -v1125 v1044 -v965 v257 -v56 v3989 v3744 -v3384 -v2185 v1568 v1048 v971 v256 -v57 v3991 v3805 -v3743 v2412 -v1670 -v1645 -v1584 -v1380 v1052 v967 -v4015 -v3997 -v3803 v2413 -v1649 -v1189 -v1051 v979 v4014 v3993 -v3426 -v2587 -v2408 -v1673 v1383 -v1270 -v1191 -v1128 v4005 -v3430 v1381 -v1274 v1197 v4022 -v2538 -v2406 v1193 -v253 v4026 -v2542 -v2460 v1205 v4030 -v3432 -v2459 -v993 -v868 v4029 -v3433 v2354 -v997 v2467 v2355 v874 -v408 -v332 -v3284 -v2471 v2356 -v412 -v336 -v3283 -v2944 v2475 v2372 -v2209 -v1019 -v2943 v2474 v2211 -v1023 v3291 -v2796 -v877 -v3295 v2800 v2207 -v4088 v4044 v3345 -v3157 -v2720 -v1885 -v286 -v208 v72 -v3912 v2719 -v207 v76 -v4094 v4049 -v3351 v2736 -v1879 v725 -v457 -v4098 -v1887 -v461 -v4102 -v4052 -v3356 v2491 -v2300 -v2001 -v1889 -v1880 v1457 -v825 -v672 -v233 -v78 -v4101 -v4050 -v2495 -v2301 -v2075 -v1895 -v1867 -v1165 -v676 -v232 -v79 -v4068 -v3675 -v3359 v2296 -v2096 -v2007 v1891 -v1460 -v1164 -v506 -v204 -v145 -v4072 -v3357 -v2092 -v1903 v1396 -v149 -v44 -v3770 -v3681 -v2497 v2309 -v2294 -v2091 -v2012 -v1417 -v1172 v512 v43 -v3772 -v2498 v2313 v2172 -v1413 -v1176 -v4303 -v3686 -v3573 v2174 -v2031 -v2015 -v1412 v1180 -v1115 -v229 v51 v3790 -v3574 v3371 -v2180 -v2035 -v2013 v1179 v55 -v4306 v3792 v3766 -v3745 -v3704 -v3689 -v3569 v3372 -v2315 v2176 v1121 -v1067 -v515 -v59 v3798 -v3747 -v3708 -v3687 v3373 -v2316 -v2188 -v1368 -v1071 -v1038 -v58 v3794 -v3767 -v3567 -v3389 v2411 v1587 -v1370 -v1126 -v1039 -v121 v3806 -v3420 v2410 v1588 -v1376 v1040 -v966 -v125 -v3741 -v3419 -v1669 -v1644 -v1583 v1372 v1129 -v1056 v987 v3992 -v1648 v1384 v1127 v983 -v4013 -v3742 -v3427 -v1675 -v1581 -v1269 v982 v4016 v4009 -v3431 -v1273 -v1192 v4017 -v4008 -v3435 -v2540 -v2407 v1213 -v864 v4018 -v3434 -v2544 v1209 v4034 -v1678 -v1208 -v995 v870 v2461 -v999 -v3964 -v2546 v2462 v2375 v875 -v407 -v334 -v2790 -v2547 v2463 v2376 -v2210 -v411 v338 -v2789 v2479 -v2371 -v1018 -v1001 v878 v3285 v1022 -v1002 v876 v3286 v2797 -v2369 -v1311 -v340 v3287 v2801 v2205 -v341 v4040 -v3242 v2739 -v1883 -v721 -v285 v73 -v4087 v4045 v3344 v2740 -v2485 v77 -v4089 v4041 v3346 -v2735 -v2484 -v2299 -v821 v724 -v456 v81 v4090 -v4053 -v3352 -v2298 -v460 -v80 v4106 -v3825 v3348 -v2733 v2492 -v2093 v1456 -v824 -v674 -v502 -v3360 -v2496 -v2303 -v2095 -v2000 -v1890 -v678 -v4067 v3074 -v2500 v2302 -v2002 -v1911 v1462 -v1414 -v508 -v147 -v4071 -v3771 -v3674 -v3078 -v2499 -v2008 v1907 -v1416 -v1166 v151 -v3676 -v3572 -v3123 v2310 -v2295 -v2089 -v2004 -v1906 -v1167 -v680 v513 -v3682 -v3571 v2314 -v2016 v1168 -v681 v45 -v4302 -v3678 v2318 -v2090 -v2030 -v1465 -v1410 -v1184 v516 v153 v46 -v3746 -v3690 -v2317 v2175 v2034 -v1114 -v514 v154 v47 -v4308 -v3706 -v3392 -v2196 v1586 -v1411 v1116 -v1066 v63 v3793 -v3710 -v3393 v2192 v1585 v1122 -v1070 -v3814 -v3568 -v3388 v2191 -v1665 v1118 -v1059 -v984 v120 -v3810 -v1371 v1130 -v1060 v986 -v124 -v4311 -v4010 -v3809 -v3712 -v3386 -v1671 -v1646 -v1392 -v1055 -v4012 -v3713 -v3421 -v2534 v1650 v1388 -v3422 -v2533 -v1676 -v1582 v1387 -v1271 -v1210 -v1053 -v980 -v698 -v3423 v1275 -v1212 -v989 -v702 v4037 -v4006 -v3439 -v2541 v1679 -v1652 -v988 -v981 -v387 v4038 v2545 -v1677 -v1653 -v863 -v328 v4033 -v4007 -v3960 -v2549 v2374 -v1277 -v1206 -v996 v865 -v327 -v2548 v2373 -v1278 -v1000 v871 v4031 -v3963 -v2812 -v2482 -v1207 -v1004 v867 -v409 -v335 -v2816 -v2483 -v1003 v879 v413 v339 -v3660 v2478 -v1307 -v1020 -v343 -v2791 v1024 -v342 v3298 v2792 -v2476 -v2370 v1333 -v1310 -v415 v3299 v2793 v2206 -v416 -v3241 -v2737 -v1884 v1541 -v1419 -v720 -v287 v69 v4039 -v1545 -v668 v68 -v4109 v4061 -v3821 -v1452 -v820 v726 -v667 -v458 -v85 -v4110 -v4057 v3347 -v2486 -v2094 -v462 -v141 v4105 -v4056 -v3824 v3368 -v2734 -v2487 -v1908 v1458 -v826 -v675 v291 -v140 v3364 v2488 -v1910 -v1415 -v679 -v501 v4103 -v4069 -v3363 -v3119 v3073 -v2504 v1463 -v729 v683 -v503 -v464 v148 -v4073 -v3077 v2304 -v2003 v682 v509 -v465 v152 v4298 -v3122 v2305 -v2024 -v1904 -v1466 v1187 -v829 v505 v156 -v3700 -v3677 v2306 -v2020 -v1464 v1188 v517 v155 -v4304 -v4075 -v3699 -v3698 -v3391 -v2322 -v2193 -v2032 -v2019 -v1905 -v1183 v66 -v4076 -v3694 -v3390 -v2195 v2036 v67 -v4309 -v3811 -v3707 -v3693 -v1181 -v1068 -v1058 -v62 -v3813 -v3711 -v1640 v1117 -v1072 -v1057 -v985 -v4312 -v3715 v2189 v2038 -v1742 -v1639 -v1389 -v1138 v122 -v60 -v4310 -v4011 -v3714 -v2039 -v1664 -v1391 -v1265 v1134 -v126 -v3807 -v3387 v2190 -v1666 v1647 -v1599 -v1264 v1133 -v1074 -v746 -v1672 v1651 -v1211 -v1075 -v750 -v4036 -v3808 -v3442 v1668 -v1655 v1385 -v1272 v1145 -v1054 v697 v383 -v128 -v4035 -v3443 -v2535 v1680 -v1654 v1276 -v1149 -v701 -v129 -v3438 v2536 v1386 v1280 -v386 v2537 v1279 v990 -v403 -v3959 -v3436 -v2553 -v2481 v991 -v402 -v2480 -v1014 v992 v866 v329 v4032 -v3965 -v3656 -v2811 v1013 v1008 -v887 v410 v330 -v2815 -v883 v414 v331 -v3659 -v3297 -v3029 v1329 -v1306 -v1021 -v882 v418 v347 v3296 v1025 v417 -v3968 v2804 -v2477 v1332 -v1312 -v1026 v2805 -v1027 -v4108 v4058 -v3243 -v2738 -v1915 v1540 -v1418 -v816 -v722 v453 -v288 -v88 -v4107 v4060 -v1919 -v1544 v89 -v4116 -v3820 v3365 -v1790 -v822 v727 v459 v292 -v84 v4120 -v4063 v3367 -v1909 -v1451 -v669 -v463 v290 -v4062 -v4054 -v3826 -v3247 -v2507 -v1453 -v827 -v730 v670 v467 -v82 v2508 v1459 -v728 v671 -v466 -v142 -v4104 -v4070 -v4055 -v3361 -v3118 v3075 -v2976 -v2503 -v2021 v1455 -v1186 -v830 -v800 -v687 v143 -v4074 -v3079 -v2980 -v2026 -v2023 -v1467 -v1185 -v828 v504 v144 -v4078 -v3829 -v3695 -v3362 -v3124 -v2501 -v2325 -v2025 v648 v525 -v160 v65 v4297 -v4077 -v3697 -v2326 -v2194 -v1062 v652 -v521 v64 v4299 -v3081 -v2321 -v2033 -v2017 -v1061 -v520 v4305 -v3812 -v3701 -v3082 v2037 -v116 v4301 -v3875 -v3702 -v3691 -v3127 -v2319 v2041 -v2018 -v1738 -v1182 -v1135 v1069 -v115 v4313 -v3703 v2040 -v1390 -v1137 -v1073 -v3719 -v3692 -v2337 -v1741 v1595 -v1077 v123 -v61 -v1641 -v1076 -v127 -v3441 v1642 -v1598 -v1131 -v745 -v131 -v3440 v1667 v1643 v1266 -v749 -v130 -v1688 v1659 v1267 v1144 -v1132 v699 v382 -v1684 v1268 -v1148 -v703 v3955 v2556 -v1683 v1284 -v388 v2557 -v3961 -v3437 -v2552 -v1011 -v884 v705 v532 -v1012 -v886 v706 v536 -v404 v3966 -v3655 -v3025 -v2813 -v2550 -v1302 -v1007 -v405 -v391 -v350 -v2817 v1015 v406 -v351 -v3969 -v3661 -v3028 -v2803 -v1815 v1328 -v1308 v1016 -v1005 -v880 v422 -v346 -v3967 v2802 v1017 v2819 v1334 -v1313 -v1031 -v881 -v344 -v2820 v4059 -v3816 -v3244 -v1914 v1786 v1542 -v1420 -v718 v289 -v86 v3366 v1918 -v1546 -v815 -v723 v452 v293 -v4115 -v3822 v3248 -v2514 -v2506 -v1789 -v1353 -v817 v719 v454 v4119 v3246 -v3069 -v2518 -v2505 -v823 -v731 v455 -v3827 -v3114 -v3068 -v1548 -v1424 v819 -v796 v690 v471 -v83 -v4064 -v2022 -v1549 -v1454 -v831 v691 -v4065 -v3830 -v3170 -v3120 v3076 -v2975 -v2324 v1475 -v799 -v686 -v522 -v433 -v163 -v4066 -v3828 -v3696 v3080 -v2979 -v2323 v1471 v524 -v437 v164 -v4082 -v3125 -v3084 -v2502 v1470 -v684 v647 -v159 -v3083 v2027 v651 -v3871 v3128 -v2918 v2028 -v518 -v157 v4300 -v3126 -v2922 v2029 -v1136 -v1063 -v4362 v4321 -v3874 -v3722 -v2333 -v2320 -v2045 -v1737 -v1064 -v519 v482 -v4317 -v3723 v1065 -v486 -v117 -v4316 -v3718 -v2336 v1743 v1594 -v1081 -v118 v693 v119 -v3716 -v2751 -v1685 -v1662 -v1600 -v747 v692 -v378 v135 -v1687 -v1663 -v751 -v3507 v2555 -v1746 v1658 -v1287 v1146 v700 v384 -v3511 v2554 -v1288 v1150 -v704 -v1681 v1656 -v1603 v1283 -v1010 -v753 v708 v389 v3954 -v2807 -v1009 -v885 -v754 v707 v3956 -v3651 v2806 -v1682 v1281 v1152 v531 -v392 -v349 -v3962 v1153 v535 -v390 -v348 v3958 -v3657 -v3024 v2814 -v2551 -v1811 -v1324 -v1249 -v425 v3970 v2818 v1301 -v426 -v3662 -v3030 -v2953 v2822 -v1814 v1330 v1303 -v1034 -v1006 v421 -v2957 v2821 -v1309 -v1035 v3663 v1335 v1305 -v1030 v419 -v345 v3664 -v1314 v3245 -v1916 v1785 v1543 -v1421 -v1349 -v301 -v87 -v3815 v3249 v1920 -v1547 -v717 v297 v4268 -v4117 -v3817 -v2513 -v1791 -v1551 -v1425 -v1352 -v739 -v689 -v474 -v296 v4121 -v3823 -v2517 -v1550 -v1423 v818 v735 -v688 v475 v3819 -v3166 -v1922 -v1472 v839 -v795 v734 v470 -v162 -v3831 -v3113 -v3070 -v1923 v1474 v835 -v523 -v161 -v4123 -v4085 -v3169 v3115 -v3071 -v2977 -v1794 v834 -v801 v468 -v432 -v4124 -v4086 v3121 v3072 -v2981 v436 -v4081 v3117 -v3088 v1468 -v685 v649 v3129 v653 -v4358 -v4318 -v4079 -v3870 -v3721 -v2983 -v2917 -v2048 -v1733 -v1469 -v804 -v158 -v4320 -v3720 -v2984 -v2921 -v2049 -v4361 -v3876 -v2874 -v2332 -v2044 v1739 v1590 -v1084 -v655 v481 v1085 -v741 -v656 -v485 -v4314 -v2747 -v2338 -v2042 v1744 -v1661 v1596 -v1080 -v771 -v740 v138 -v1686 -v1660 -v1140 -v775 v139 -v4419 -v4315 -v3879 -v3717 v2750 -v1747 v1601 -v1286 -v1139 -v1078 -v748 -v270 v134 -v4423 -v1745 -v1285 -v752 v694 -v377 -v3506 -v2341 -v1604 v1147 -v756 v695 -v379 -v132 -v3510 -v1602 v1151 -v755 v696 v385 v1657 v1155 -v919 -v712 v381 v1154 -v923 v393 v3404 v3020 v1282 -v1245 v533 -v424 v3957 -v3650 v2808 v537 -v423 v3978 -v3652 -v3026 v2809 -v2675 -v1810 -v1248 -v1033 -v3974 -v3658 v2810 -v2679 -v1323 -v1032 -v3973 v3654 -v3536 -v3031 -v2952 -v2826 -v1816 -v1325 -v846 v539 v3665 -v2956 v1331 v1304 -v850 v540 v3032 v1327 v1322 -v1028 -v420 v3033 -v1336 v1318 -v4264 -v4112 v3257 v1917 v1787 v1539 -v1422 -v1348 -v736 -v473 -v300 v3253 v1921 v1538 -v1426 -v738 -v472 v4267 -v4118 v3252 -v2897 -v2515 -v1925 v1792 -v1555 -v1354 v836 -v791 -v294 v4122 -v3818 -v2971 -v2519 -v1924 -v1473 v838 v4126 -v4084 v3839 -v3165 -v2970 v1795 -v898 -v797 v732 -v295 -v4125 -v4083 -v3835 v1793 v643 -v3834 -v3171 -v3091 -v2978 -v2521 -v1357 v832 -v802 v733 v642 v469 v434 v3116 -v3092 -v2982 -v2522 v438 -v3866 v3137 -v3087 v2986 -v2107 -v2047 v833 -v805 v650 -v24 -v4319 v3133 -v2985 -v2046 -v803 v654 -v28 -v4357 -v4080 -v3872 -v3174 -v3132 -v3085 -v2919 v2870 -v2328 -v1083 v658 -v440 -v2923 -v1732 -v1082 v657 -v441 -v4363 v3877 -v2873 -v2334 -v1734 v483 v137 v1740 v1589 -v487 v136 -v3880 -v3846 -v2925 -v2746 -v2339 -v2043 v1736 v1591 -v770 -v266 -v3878 -v3850 -v2926 -v1748 v1597 -v774 -v742 -v4418 -v4366 v2752 -v2604 -v2342 v1593 -v1079 -v743 -v489 -v269 -v4422 -v2340 -v1605 v1141 -v744 -v490 -v3508 v1142 -v760 v715 -v133 -v3512 v1143 v716 -v527 -v380 -v3400 v2755 -v1159 -v918 -v711 -v602 -v526 -v401 -v922 -v397 -v3975 -v3514 v3403 -v2629 -v1806 -v1244 -v709 v534 -v396 -v3977 -v3515 v3019 v538 -v3631 -v3532 v3021 v2829 -v2674 -v1812 v1250 v542 -v3653 -v3635 -v3027 v2830 -v2678 v541 -v3971 v3673 -v3535 v3023 -v2954 -v2825 -v1817 v1319 -v845 -v3669 v3034 -v2958 v1326 v1321 -v849 -v3972 -v3668 -v2823 -v2244 v1818 v1344 -v1253 -v1029 v2248 v1819 v1340 v1317 -v4263 -v3256 v2893 -v2510 v1913 v1783 -v1558 -v1497 -v1434 -v1350 -v737 -v298 -v4111 v1912 v1788 -v1559 -v1430 -v837 v4269 v4113 -v3836 -v3250 -v3161 -v2896 -v2516 -v1929 v1784 -v1554 -v1429 -v1355 -v894 v4114 v3838 v2520 v1796 -v790 -v428 v4130 -v3251 -v3167 -v3090 -v2524 -v1944 -v1552 -v1358 -v897 -v792 -v427 -v3089 -v2972 -v2523 -v1356 -v798 -v4272 -v3832 -v3172 -v3134 -v2973 -v2103 -v794 v435 -v3136 v2974 -v2913 -v806 v644 v439 -v4353 -v3833 -v3175 -v2990 -v2912 -v2106 -v1620 v645 v443 -v23 -v3865 -v3173 -v1624 v646 v477 v442 -v27 -v4359 -v4213 -v3867 -v3130 -v3086 -v2920 v2869 v662 v476 v3873 -v2924 -v2327 -v4364 v3869 -v3207 -v3131 -v2928 -v2875 -v2742 -v2329 v1713 v484 v3881 -v2927 -v2335 -v1735 -v1717 -v488 -v4367 -v3845 -v2748 -v2600 v2331 v1756 -v772 -v492 -v265 -v4365 -v3849 -v3502 -v2343 v1752 v1592 -v776 -v491 -v4420 -v3501 -v2878 v2753 -v2603 -v1751 v1613 -v763 v714 -v271 -v4424 -v1609 -v764 v713 -v3509 v2756 -v1608 v1162 -v778 -v759 -v598 -v398 -v3513 v2754 v1163 -v779 -v400 -v4426 -v4163 -v3606 v3517 -v3399 v2625 -v1240 -v1158 -v920 -v757 -v601 -v274 -v4427 -v3976 -v3610 v3516 -v924 v528 v3405 -v2828 -v2628 v1246 -v1156 -v710 v529 -v394 -v2948 v2827 -v1805 v530 v3670 -v3630 -v3531 -v3310 -v2947 -v2676 -v1807 v1251 -v926 v546 -v395 v3672 -v3634 v3022 -v2680 -v1813 v1320 -v927 -v3537 -v3408 -v3042 -v2955 v1809 -v1341 -v1254 -v847 v3038 -v2959 v1820 -v1343 -v1252 -v851 -v3666 v3037 -v2960 -v2824 -v2682 -v2243 -v2060 -v2961 -v2683 v2247 -v1339 -v1315 -v4265 -v3916 -v3254 v2892 -v1932 -v1556 -v1496 -v1433 v1346 -v299 -v3837 v2509 -v1933 v1782 -v1351 v4270 v4133 -v2898 v2511 -v1940 -v1928 v1804 -v1427 v1347 -v893 v4134 -v3160 v2512 -v1800 -v1359 v4273 -v4129 v3162 v2528 -v2424 -v1943 -v1926 -v1799 -v1553 -v1428 -v899 -v4271 -v3168 -v3135 -v793 -v429 -v4127 v3164 -v2993 -v2901 v2700 -v2102 -v814 -v430 v3176 v2994 -v2704 -v810 v431 -v4209 -v2989 v2865 -v2108 -v1619 -v902 -v809 -v665 v447 v308 -v25 -v4352 -v2914 -v1623 -v666 -v312 -v29 -v4354 -v4212 -v3203 -v2987 -v2915 v2871 -v948 -v661 -v4360 -v3868 -v2916 -v766 v478 -v4356 v3889 -v3206 -v2932 -v2876 -v2111 -v1981 v1753 v1712 -v765 -v659 v479 -v261 -v31 -v4414 -v4368 -v3885 -v2741 -v2330 -v1985 v1755 -v1716 v480 -v32 -v4413 -v3884 -v3847 -v2879 -v2743 -v2654 -v2599 -v2351 -v2153 v1610 -v773 -v762 v496 -v267 -v3851 -v2877 -v2749 v2347 -v2157 v1612 -v777 -v761 -v4421 v2745 -v2605 v2346 -v1749 -v1161 -v781 -v272 -v100 -v4425 v3503 v2757 -v1160 -v914 -v780 -v399 -v4429 -v4159 -v3853 v3504 -v3395 -v1750 -v1606 -v913 -v597 -v362 -v275 -v4428 -v3854 v3505 -v273 -v4162 -v3605 v3521 -v3401 v2624 -v2608 -v1607 -v921 -v758 -v603 -v3609 -v2670 -v1239 -v925 -v3527 v3406 -v3306 -v3049 -v2669 -v2630 -v1241 -v1157 -v929 v549 v3671 -v3053 v1247 -v928 v841 v550 -v3632 -v3533 v3409 -v3309 -v3039 -v2677 v1243 v840 -v606 v545 -v3636 v3407 -v3041 -v2949 -v2681 -v1808 -v1342 -v1255 -v3538 -v2950 -v2685 -v2633 -v2056 v1828 -v848 v543 -v2951 -v2684 -v1824 -v852 -v3942 -v3667 -v3638 -v3539 v3035 -v2965 -v2245 v2059 -v1823 v853 -v3639 -v3540 v2249 -v1337 -v1316 v854 -v4261 -v4132 -v3915 -v3255 v2894 -v1930 v1801 -v1557 -v1498 -v1431 -v889 -v4266 v4131 v1803 v1345 v4262 -v3000 -v2899 -v2531 -v2420 -v1939 -v1367 -v895 v4274 -v3004 v2532 v1363 -v2992 -v2902 v2527 -v2423 -v2098 -v1945 -v1927 -v1797 -v1502 v1362 -v900 -v811 v3163 -v2991 -v2900 -v813 -v19 -v4128 v3184 v2699 v2525 -v2104 -v1798 -v903 -v664 -v450 -v18 v3180 -v2703 -v901 -v663 v451 -v4208 -v3179 -v2109 -v1948 -v1621 -v1519 -v944 -v807 v446 v307 -v26 v2864 -v1625 -v1523 -v311 -v30 -v4214 v3886 -v3202 -v2988 -v2935 v2866 -v2112 -v947 -v808 v444 v34 -v4355 v3888 -v3841 -v2936 v2872 -v2110 v1754 v33 -v4376 -v3840 -v3208 -v2931 v2868 -v2650 -v2595 -v2348 -v1980 v1714 -v1627 -v1224 -v660 v499 -v4372 -v2880 -v2350 -v1984 -v1718 -v1628 v1611 -v767 v500 -v260 -v4371 -v4217 -v3882 -v3848 -v2929 -v2653 -v2601 -v2152 -v768 v495 -v262 -v96 -v4415 -v3852 -v2744 -v2156 v769 -v268 -v4416 -v3883 -v3856 -v3211 -v2765 -v2606 v2344 -v1720 v785 -v593 v493 -v358 -v264 -v99 v4417 -v3855 -v2761 -v1721 -v276 v4433 -v4158 -v3524 -v3264 -v2760 v2620 -v2609 v2345 -v599 v361 -v3525 -v3394 -v3268 -v2607 -v915 -v4164 -v3607 v3520 -v3396 v2626 -v916 -v627 -v604 v548 -v3626 -v3611 -v3402 -v917 v547 -v3625 v3518 v3398 -v3305 -v3048 -v2631 -v933 -v607 -v561 -v3526 v3410 -v3052 -v3040 -v2671 -v1242 -v605 -v4167 -v3633 -v3613 -v3528 -v3311 -v2672 -v2634 v1825 -v1263 v3637 -v3614 -v3534 -v2673 -v2632 -v2239 v1827 -v1259 v842 -v3938 -v3641 v3530 -v2968 -v2689 v2238 -v2055 -v1258 v843 v544 -v3640 -v3541 -v2969 v844 v3941 -v3314 -v3036 -v2964 -v2265 -v2246 v2061 -v1821 v858 -v7 v2250 -v1338 -v11 -v3917 v2890 -v2530 v1935 -v1931 -v1802 v1499 -v1432 -v1364 v4260 v2895 -v2529 -v1366 -v888 -v4282 -v2999 v2891 -v2419 -v1941 v1503 -v890 -v4278 -v3003 -v2903 v1501 -v896 -v812 -v4277 -v3921 v3181 -v2425 -v2128 v1946 v1360 -v892 -v449 v3183 -v2132 -v2097 -v1615 -v904 -v448 -v4204 v2701 v2526 v2099 -v1949 -v1614 v1361 -v2705 -v2105 -v1947 v20 -v4210 -v4188 -v3198 -v3177 -v2934 v2428 v2101 -v1622 -v1518 -v943 v309 v21 -v3887 -v2933 -v2113 -v1708 -v1626 -v1522 -v313 v22 -v4373 -v4215 -v3204 -v3178 v2707 -v1763 v1707 -v1630 -v1220 -v949 -v498 v445 -v38 -v4375 v2867 v2708 -v2349 -v1767 -v1629 -v497 -v4218 -v3209 v2888 -v2649 -v2219 -v1982 v1715 -v1223 -v315 -v4216 -v3842 v2884 -v2594 -v2223 -v1986 -v1719 -v316 -v4369 -v3843 -v3212 -v2930 v2883 -v2762 -v2655 -v2596 -v2154 -v1723 -v952 -v788 -v95 v3844 -v3210 -v2764 -v2602 -v2158 -v1722 -v789 -v263 v4436 -v4370 -v4154 v3860 -v3523 v2598 -v1988 v784 -v494 -v357 -v284 -v101 v4437 -v3601 -v3522 -v2610 -v1989 -v592 -v280 v4432 -v4160 v3600 -v3263 -v2758 -v2658 -v2160 v782 -v623 v594 v363 -v279 -v3267 v2619 -v2161 -v600 v4430 -v4165 -v3608 -v3301 -v2837 -v2759 v2621 -v936 -v626 v596 -v557 -v104 -v3612 -v3397 -v2841 v2627 -v937 -v608 -v4168 -v3616 v3519 v3418 -v3307 -v3050 v2623 -v1260 -v932 -v560 v366 -v4166 v3627 -v3615 -v3414 -v3054 -v2635 -v1826 -v1262 v3628 -v3413 -v3312 -v2967 -v2692 -v2051 -v930 v3629 -v3529 -v2966 -v2693 -v3937 -v3645 -v3549 -v3315 -v3056 -v2688 -v2261 -v2057 -v1256 v861 v3545 -v3313 -v3057 v2240 v862 v3943 v3544 -v2962 -v2686 -v2264 v2241 v2062 -v1822 -v1257 v857 -v6 v2242 -v10 -v4279 -v3918 v2415 v1500 -v1365 -v4281 v2889 v1934 v1504 -v3922 v3001 v2911 -v2421 v1936 -v3920 v3182 -v3005 -v2907 -v2695 -v1942 -v891 -v4275 -v3465 -v2906 -v2694 -v2426 -v2127 v1938 -v912 -v2131 -v1950 -v908 v303 -v4276 -v4184 -v3007 v2702 v2429 -v939 -v907 v302 -v4203 -v3008 -v2706 v2427 v2100 -v1616 -v4386 -v4205 -v4187 v2710 v2121 -v1617 -v1520 -v945 v310 -v41 -v4374 -v4211 -v3197 v2709 -v2117 -v1976 -v1618 -v1524 -v314 -v42 -v4207 -v3199 v2885 -v2645 -v2116 -v1975 -v1762 -v1634 -v1219 -v950 -v318 -v37 -v4219 -v3205 v2887 -v2148 -v1766 v1709 -v317 v3201 -v2651 -v2218 -v2147 -v1983 v1710 -v1526 v1225 -v953 -v787 -v91 -v35 v3213 -v2763 -v2222 -v1987 v1711 -v1527 -v951 -v786 -v4435 v3863 v2881 -v2656 -v2155 -v1991 v1727 -v353 -v281 -v97 -v4434 v3864 -v2597 -v2159 -v1990 -v283 v3859 v2882 -v2659 -v2618 -v2163 -v1228 -v359 -v102 -v4153 -v2657 v2614 -v2162 -v4155 v3857 -v3265 v2613 -v935 v783 -v622 v364 -v277 -v105 -v4161 v3602 -v3269 -v3044 -v934 v595 -v103 -v4431 -v4157 v3603 v3415 -v3043 -v2836 -v1099 -v628 -v616 -v556 v367 -v278 -v4169 v3604 v3417 v3300 -v2840 v2622 -v1261 -v612 v365 -v3620 v3302 -v3271 -v3051 -v2691 -v2643 -v611 -v562 -v3308 -v3272 -v3055 -v2690 -v2639 v3933 v3648 -v3546 -v3411 v3304 -v3059 -v2638 -v931 -v860 -v631 v3649 -v3548 v3316 -v3058 -v2050 v859 -v3939 -v3644 -v3412 -v2260 -v2052 v565 -v2058 v3944 -v3642 v3542 -v2963 -v2687 -v2266 v2253 v2054 v855 v8 v2254 -v2063 -v12 -v4280 -v3919 -v2996 v2908 -v1512 -v1290 -v3923 v2910 v2414 v1508 -v1294 -v3461 v3002 v2416 v1507 -v909 -v3006 -v2422 v1937 -v911 v3464 -v3010 -v2904 v2418 -v2129 v1958 -v3009 -v2696 v2430 -v2133 -v1954 -v1514 -v4382 -v4183 -v2905 v2697 -v2118 -v1953 -v1513 -v905 -v40 v2698 -v2120 -v938 v304 -v39 -v4385 -v4189 v2714 -v2135 -v1637 -v1521 -v1215 -v940 -v906 v305 -v4206 v2886 -v2136 -v1638 -v1525 -v946 v306 -v4227 -v2114 -v1764 -v1633 -v1529 -v1221 -v942 -v322 -v4223 -v3200 -v2644 -v1977 -v1768 -v1528 -v954 -v4222 -v4192 -v3862 v3585 -v3221 -v2646 -v2220 -v2115 -v1978 -v1730 -v1631 v1226 -v36 -v3861 v3217 -v2652 -v2224 -v2149 -v1979 -v1731 -v282 -v90 v3216 v2648 -v2615 -v2150 -v1995 -v1770 v1726 -v1229 -v92 -v3259 -v2660 -v2617 -v2151 -v1771 -v1227 -v352 -v98 -v3258 -v2226 -v2167 v1724 v618 -v354 -v94 -v2227 -v360 -v106 -v3858 -v3266 -v2611 -v1095 -v624 -v613 -v552 v356 -v4156 v3416 -v3270 -v615 v368 -v4177 v3623 -v3274 -v2838 -v2640 -v2612 -v1098 -v629 -v558 -v4173 v3624 -v3273 -v#### 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.85 0.97 0.91 2/55 24870
Raw data (stat): 24870 (runsolver) R 24869 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479862921 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.0002 s]
Raw data (loadavg): 0.87 0.97 0.91 2/55 24870
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 2500 0 0 0 991 7 0 0 25 0 1 0 479862921 12804096 2467 4294967295 134512640 134672761 3221224544 3221223780 134564428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3126 2467 603 41 0 3085 0
vsize: 12504
[startup+20.0001 s]
Raw data (loadavg): 0.89 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 3842 0 0 0 1988 10 0 0 25 0 1 0 479862921 17477632 3722 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4267 3722 603 41 0 4226 0
vsize: 17068
[startup+30.0007 s]
Raw data (loadavg): 0.91 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 3981 0 0 0 2987 10 0 0 25 0 1 0 479862921 18071552 3861 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4412 3861 603 41 0 4371 0
vsize: 17648
[startup+40.001 s]
Raw data (loadavg): 0.92 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4041 0 0 0 3987 10 0 0 25 0 1 0 479862921 18206720 3921 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4445 3921 603 41 0 4404 0
vsize: 17780
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4114 0 0 0 4987 11 0 0 25 0 1 0 479862921 18477056 3994 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4511 3994 603 41 0 4470 0
vsize: 18044
[startup+60.0014 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4172 0 0 0 5987 11 0 0 25 0 1 0 479862921 18747392 4052 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4577 4052 603 41 0 4536 0
vsize: 18308
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4226 0 0 0 6987 11 0 0 25 0 1 0 479862921 19017728 4106 4294967295 134512640 134672761 3221224544 3221223456 1075358820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4643 4107 603 41 0 4602 0
vsize: 18572
[startup+80.0026 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4275 0 0 0 7987 11 0 0 25 0 1 0 479862921 19279872 4155 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4707 4155 603 41 0 4666 0
vsize: 18828
[startup+90.0022 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4336 0 0 0 8987 11 0 0 25 0 1 0 479862921 19550208 4216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4773 4216 603 41 0 4732 0
vsize: 19092
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4399 0 0 0 9987 12 0 0 25 0 1 0 479862921 19685376 4279 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4806 4279 603 41 0 4765 0
vsize: 19224
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4450 0 0 0 10987 12 0 0 25 0 1 0 479862921 19955712 4330 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4872 4330 603 41 0 4831 0
vsize: 19488
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4539 0 0 0 11986 12 0 0 25 0 1 0 479862921 20357120 4419 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4970 4419 603 41 0 4929 0
vsize: 19880
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4666 0 0 0 12986 13 0 0 25 0 1 0 479862921 20692992 4522 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5052 4522 603 41 0 5011 0
vsize: 20208
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4687 0 0 0 13985 13 0 0 25 0 1 0 479862921 20828160 4543 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5085 4543 603 41 0 5044 0
vsize: 20340
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4748 0 0 0 14986 13 0 0 25 0 1 0 479862921 21098496 4604 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5151 4604 603 41 0 5110 0
vsize: 20604
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 4831 0 0 0 15985 13 0 0 25 0 1 0 479862921 21368832 4687 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5217 4687 603 41 0 5176 0
vsize: 20868
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 5873 0 0 0 16983 16 0 0 25 0 1 0 479862921 25812992 5729 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6302 5729 603 41 0 6261 0
vsize: 25208
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 6636 0 0 0 17981 18 0 0 25 0 1 0 479862921 28917760 6492 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7060 6492 603 41 0 7019 0
vsize: 28240
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 7216 0 0 0 18980 19 0 0 25 0 1 0 479862921 31342592 7072 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7652 7072 603 41 0 7611 0
vsize: 30608
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 7374 0 0 0 19980 20 0 0 25 0 1 0 479862921 31883264 7230 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7784 7230 603 41 0 7743 0
vsize: 31136
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 7809 0 0 0 20978 22 0 0 25 0 1 0 479862921 33632256 7665 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8211 7665 603 41 0 8170 0
vsize: 32844
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 8539 0 0 0 21976 24 0 0 25 0 1 0 479862921 36720640 8395 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8965 8395 603 41 0 8924 0
vsize: 35860
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 9294 0 0 0 22974 26 0 0 25 0 1 0 479862921 39665664 9150 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9684 9150 603 41 0 9643 0
vsize: 38736
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 9698 0 0 0 23972 28 0 0 25 0 1 0 479862921 41422848 9554 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10113 9554 603 41 0 10072 0
vsize: 40452
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 9941 0 0 0 24971 29 0 0 25 0 1 0 479862921 42364928 9797 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10343 9797 603 41 0 10302 0
vsize: 41372
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 10505 0 0 0 25969 31 0 0 25 0 1 0 479862921 44646400 10361 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10900 10361 603 41 0 10859 0
vsize: 43600
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 11395 0 0 0 26967 34 0 0 25 0 1 0 479862921 48279552 11251 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11787 11251 603 41 0 11746 0
vsize: 47148
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 12213 0 0 0 27964 36 0 0 25 0 1 0 479862921 52162560 12069 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12069 603 41 0 12694 0
vsize: 50940
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 12964 0 0 0 28963 38 0 0 25 0 1 0 479862921 55123968 12820 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13458 12820 603 41 0 13417 0
vsize: 53832
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13324 0 0 0 29962 39 0 0 25 0 1 0 479862921 56610816 13180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13821 13180 603 41 0 13780 0
vsize: 55284
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24872
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13436 0 0 0 30962 40 0 0 25 0 1 0 479862921 57012224 13292 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13919 13292 603 41 0 13878 0
vsize: 55676
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 31962 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 32962 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 33962 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223668 134566106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 34962 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 35962 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 36963 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 37963 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 38963 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 39963 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 40963 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 41963 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 42964 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 43964 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 44964 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 45964 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 46964 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 47965 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 48965 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 49965 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223728 134559356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 13517 0 0 0 50965 40 0 0 25 0 1 0 479862921 57147392 13321 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13952 13321 603 41 0 13911 0
vsize: 55808
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 14110 0 0 0 51964 41 0 0 25 0 1 0 479862921 59572224 13914 4294967295 134512640 134672761 3221224544 3221223648 134555333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14544 13914 603 41 0 14503 0
vsize: 58176
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 14691 0 0 0 52963 43 0 0 25 0 1 0 479862921 61997056 14495 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15136 14495 603 41 0 15095 0
vsize: 60544
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 15262 0 0 0 53962 44 0 0 25 0 1 0 479862921 64294912 15066 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15697 15066 603 41 0 15656 0
vsize: 62788
[startup+550.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 15836 0 0 0 54961 46 0 0 25 0 1 0 479862921 66732032 15640 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16292 15640 603 41 0 16251 0
vsize: 65168
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 16391 0 0 0 55958 48 0 0 25 0 1 0 479862921 69033984 16195 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16854 16195 603 41 0 16813 0
vsize: 67416
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 17025 0 0 0 56956 50 0 0 25 0 1 0 479862921 71577600 16829 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17475 16829 603 41 0 17434 0
vsize: 69900
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 17705 0 0 0 57955 52 0 0 25 0 1 0 479862921 74260480 17509 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18130 17509 603 41 0 18089 0
vsize: 72520
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 18406 0 0 0 58953 54 0 0 25 0 1 0 479862921 77213696 18210 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18851 18210 603 41 0 18810 0
vsize: 75404
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 19114 0 0 0 59951 56 0 0 25 0 1 0 479862921 80035840 18918 4294967295 134512640 134672761 3221224544 3221223612 1075346600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19540 18918 603 41 0 19499 0
vsize: 78160
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24874
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 19672 0 0 0 60950 58 0 0 25 0 1 0 479862921 82317312 19476 4294967295 134512640 134672761 3221224544 3221223728 134557980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20097 19476 603 41 0 20056 0
vsize: 80388
[startup+620.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 20149 0 0 0 61949 59 0 0 25 0 1 0 479862921 84201472 19953 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20557 19953 603 41 0 20516 0
vsize: 82228
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 20635 0 0 0 62948 60 0 0 25 0 1 0 479862921 86212608 20439 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21048 20439 603 41 0 21007 0
vsize: 84192
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 21135 0 0 0 63947 61 0 0 25 0 1 0 479862921 88215552 20939 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21537 20939 603 41 0 21496 0
vsize: 86148
[startup+650.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 21662 0 0 0 64945 63 0 0 25 0 1 0 479862921 90472448 21466 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22088 21466 603 41 0 22047 0
vsize: 88352
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 22097 0 0 0 65945 63 0 0 25 0 1 0 479862921 92225536 21901 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22516 21901 603 41 0 22475 0
vsize: 90064
[startup+670.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 22587 0 0 0 66944 64 0 0 25 0 1 0 479862921 94236672 22391 4294967295 134512640 134672761 3221224544 3221223616 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23007 22391 603 41 0 22966 0
vsize: 92028
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 23000 0 0 0 67943 66 0 0 25 0 1 0 479862921 95850496 22804 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23401 22804 603 41 0 23360 0
vsize: 93604
[startup+690.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 23452 0 0 0 68942 67 0 0 25 0 1 0 479862921 97734656 23256 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23861 23256 603 41 0 23820 0
vsize: 95444
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 23881 0 0 0 69942 68 0 0 25 0 1 0 479862921 99479552 23685 4294967295 134512640 134672761 3221224544 3221223728 134558937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24287 23685 603 41 0 24246 0
vsize: 97148
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 24266 0 0 0 70941 69 0 0 25 0 1 0 479862921 101076992 24070 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24677 24070 603 41 0 24636 0
vsize: 98708
[startup+720.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 24661 0 0 0 71940 70 0 0 25 0 1 0 479862921 102559744 24465 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25039 24465 603 41 0 24998 0
vsize: 100156
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 25064 0 0 0 72939 71 0 0 25 0 1 0 479862921 104304640 24868 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25465 24868 603 41 0 25424 0
vsize: 101860
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 25291 0 0 0 73938 71 0 0 25 0 1 0 479862921 105115648 25095 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25663 25095 603 41 0 25622 0
vsize: 102652
[startup+750.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 25504 0 0 0 74939 71 0 0 25 0 1 0 479862921 106053632 25308 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25892 25308 603 41 0 25851 0
vsize: 103568
[startup+760.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 25659 0 0 0 75938 72 0 0 25 0 1 0 479862921 106594304 25463 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26024 25463 603 41 0 25983 0
vsize: 104096
[startup+770.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 25823 0 0 0 76938 72 0 0 25 0 1 0 479862921 107266048 25627 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26188 25627 603 41 0 26147 0
vsize: 104752
[startup+780.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 26012 0 0 0 77938 73 0 0 25 0 1 0 479862921 108072960 25816 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26385 25816 603 41 0 26344 0
vsize: 105540
[startup+790.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 26155 0 0 0 78937 73 0 0 25 0 1 0 479862921 109662208 25959 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26773 25959 603 41 0 26732 0
vsize: 107092
[startup+800.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 26301 0 0 0 79937 74 0 0 25 0 1 0 479862921 110198784 26105 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26904 26105 603 41 0 26863 0
vsize: 107616
[startup+810.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 26660 0 0 0 80936 75 0 0 25 0 1 0 479862921 111677440 26464 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27265 26464 603 41 0 27224 0
vsize: 109060
[startup+820.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 27371 0 0 0 81934 77 0 0 25 0 1 0 479862921 114491392 27175 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27952 27175 603 41 0 27911 0
vsize: 111808
[startup+830.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 27803 0 0 0 82933 78 0 0 25 0 1 0 479862921 116244480 27607 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28380 27607 603 41 0 28339 0
vsize: 113520
[startup+840.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28134 0 0 0 83933 79 0 0 25 0 1 0 479862921 117583872 27938 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28707 27938 603 41 0 28666 0
vsize: 114828
[startup+850.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 84932 79 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+860.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 85933 79 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+870.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 86933 79 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+880.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 87933 79 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+890.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 88932 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+900.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 89932 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223464 1075351157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+910.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24876
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 90933 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+920.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 91933 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+930.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 92933 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+940.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 93933 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+950.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 94933 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+960.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 95934 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223668 134566133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+970.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 96934 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+980.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 97934 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+990.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 98934 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 99934 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 100935 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 101935 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223620 134565028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 102935 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 103935 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 104935 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 105935 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223676 1075347104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 106936 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 107936 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 108936 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 109936 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 110937 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 111937 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 112937 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 113937 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 114937 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 115938 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 116938 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 117938 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 118938 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 24878
Raw data (stat): 24870 (minisat+) R 24869 20024 20023 0 -1 0 28456 0 0 0 119937 80 0 0 25 0 1 0 479862921 118923264 28260 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29034 28260 603 41 0 28993 0
vsize: 116136
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 24878
Raw data (stat): 24870 (minisat+) Z 24869 20024 20023 0 -1 12 28459 0 0 0 119938 85 0 0 25 0 1 0 479862921 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: 10
Real time (s): 1200.12
CPU time (s): 1200.25
CPU user time (s): 1199.39
CPU system time (s): 0.858869
CPU usage (%): 100.011
Max. virtual memory (Kb): 116136
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####