PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-p2756.opb
MD5SUM	49fba7b1c2f3e65c53f8418d126e3ec3
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4605
Optimality of the best value was proved	NO
Number of terms in the objective function	2166
Biggest coefficient in the objective function	11000
Number of bits for the biggest coefficient in the objective function	14
Sum of the numbers in the objective function	321831
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	11000
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	321831
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06684
Number of variables	2756
Total number of constraints	3511
Number of constraints which are clauses	132
Number of constraints which are cardinality constraints (but not clauses)	2976
Number of constraints which are nor clauses,nor cardinality constraints	403
Minimum length of a constraint	1
Maximum length of a constraint	546
Trace number 21086

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        642144 kB
Buffers:         16092 kB
Cached:         355100 kB
SwapCached:        360 kB
Active:         161108 kB
Inactive:       212188 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        641892 kB
SwapTotal:     2097136 kB
SwapFree:      2095968 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5744 kB
Slab:            13488 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:02:54 (client local time) WITH STATUS 10 IN 1200.37 SECONDS
stats: 13751 7 1200.37 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 738 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssssssssss..ssssss.sss.ssss....................................................................................................................................
c ---[ 759]---> Adder-cost: 72   maxlim: 709   bits: 11/10
c ---[ 758]---> Adder-cost: 56   maxlim: 249   bits: 9/8
c ---[ 757]---> Adder-cost: 76   maxlim: 906   bits: 11/10
c ---[ 756]---> Adder-cost: 104   maxlim: 308   bits: 10/9
c ---[ 755]---> Adder-cost: 86   maxlim: 667   bits: 11/10
c ---[ 754]---> Adder-cost: 76   maxlim: 700   bits: 11/10
c ---[ 753]---> Adder-cost: 56   maxlim: 218   bits: 9/8
c ---[ 752]---> Adder-cost: 66   maxlim: 897   bits: 11/10
c ---[ 751]---> Adder-cost: 106   maxlim: 404   bits: 10/9
c ---[ 750]---> Adder-cost: 90   maxlim: 763   bits: 11/10
c ---[ 749]---> Adder-cost: 77   maxlim: 250   bits: 9/8
c ---[ 748]---> Adder-cost: 50   maxlim: 289   bits: 10/9
c ---[ 746]---> Adder-cost: 110   maxlim: 469   bits: 10/9
c ---[ 745]---> Adder-cost: 90   maxlim: 752   bits: 11/10
c ---[ 744]---> Adder-cost: 69   maxlim: 277   bits: 10/9
c ---[ 743]---> Adder-cost: 52   maxlim: 294   bits: 10/9
c ---[ 742]---> Adder-cost: 63   maxlim: 191   bits: 9/8
c ---[ 741]---> Adder-cost: 102   maxlim: 529   bits: 11/10
c ---[ 740]---> Adder-cost: 90   maxlim: 853   bits: 11/10
c ---[ 739]---> Adder-cost: 43   maxlim: 156   bits: 9/8
c ---[ 738]---> Adder-cost: 95   maxlim: 195   bits: 9/8
c ---[ 737]---> Adder-cost: 94   maxlim: 189   bits: 9/8
c ---[ 736]---> Adder-cost: 85   maxlim: 354   bits: 10/9
c ---[ 735]---> Adder-cost: 82   maxlim: 813   bits: 11/10
c ---[ 734]---> Adder-cost: 78   maxlim: 813   bits: 11/10
c ---[ 733]---> Adder-cost: 68   maxlim: 192   bits: 9/8
c ---[ 732]---> Adder-cost: 94   maxlim: 260   bits: 10/9
c ---[ 731]---> Adder-cost: 90   maxlim: 383   bits: 10/9
c ---[ 730]---> Adder-cost: 84   maxlim: 457   bits: 10/9
c ---[ 729]---> Adder-cost: 93   maxlim: 918   bits: 11/10
c ---[ 728]---> Adder-cost: 82   maxlim: 918   bits: 11/10
c ---[ 727]---> Adder-cost: 75   maxlim: 297   bits: 10/9
c ---[ 726]---> Adder-cost: 48   maxlim: 364   bits: 10/9
c ---[ 725]---> Adder-cost: 68   maxlim: 670   bits: 11/10
c ---[ 724]---> Adder-cost: 78   maxlim: 670   bits: 11/10
c ---[ 723]---> Adder-cost: 90   maxlim: 312   bits: 10/9
c ---[ 722]---> Adder-cost: 80   maxlim: 479   bits: 10/9
c ---[ 721]---> Adder-cost: 121   maxlim: 921   bits: 11/10
c ---[ 720]---> Adder-cost: 119   maxlim: 921   bits: 11/10
c ---[ 719]---> Adder-cost: 67   maxlim: 323   bits: 10/9
c ---[ 718]---> Adder-cost: 88   maxlim: 522   bits: 11/10
c ---[ 717]---> Adder-cost: 82   maxlim: 665   bits: 11/10
c ---[ 716]---> Adder-cost: 122   maxlim: 1206   bits: 12/11
c ---[ 715]---> Adder-cost: 126   maxlim: 1206   bits: 12/11
c ---[ 714]---> Adder-cost: 74   maxlim: 626   bits: 11/10
c ---[ 713]---> Adder-cost: 48   maxlim: 382   bits: 10/9
c ---[ 712]---> Adder-cost: 60   maxlim: 688   bits: 11/10
c ---[ 711]---> Adder-cost: 78   maxlim: 688   bits: 11/10
c ---[ 710]---> Adder-cost: 50   maxlim: 173   bits: 9/8
c ---[ 709]---> Adder-cost: 94   maxlim: 375   bits: 10/9
c ---[ 708]---> Adder-cost: 86   maxlim: 483   bits: 10/9
c ---[ 707]---> Adder-cost: 119   maxlim: 944   bits: 11/10
c ---[ 706]---> Adder-cost: 117   maxlim: 944   bits: 11/10
c ---[ 705]---> Adder-cost: 75   maxlim: 350   bits: 10/9
c ---[ 704]---> Adder-cost: 98   maxlim: 492   bits: 10/9
c ---[ 703]---> Adder-cost: 86   maxlim: 435   bits: 10/9
c ---[ 702]---> Adder-cost: 124   maxlim: 1229   bits: 12/11
c ---[ 701]---> Adder-cost: 116   maxlim: 1229   bits: 12/11
c ---[ 700]---> Adder-cost: 76   maxlim: 759   bits: 11/10
c ---[ 698]---> Adder-cost: 71   maxlim: 279   bits: 10/9
c ---[ 696]---> Adder-cost: 83   maxlim: 333   bits: 10/9
c ---[ 695]---> Adder-cost: 99   maxlim: 193   bits: 9/8
c ---[ 694]---> Adder-cost: 88   maxlim: 527   bits: 11/10
c ---[ 693]---> Adder-cost: 88   maxlim: 717   bits: 11/10
c ---[ 692]---> Adder-cost: 76   maxlim: 248   bits: 9/8
c ---[ 691]---> Adder-cost: 107   maxlim: 222   bits: 9/8
c ---[ 690]---> Adder-cost: 83   maxlim: 317   bits: 10/9
c ---[ 689]---> Adder-cost: 107   maxlim: 189   bits: 9/8
c ---[ 688]---> Adder-cost: 90   maxlim: 440   bits: 10/9
c ---[ 687]---> Adder-cost: 98   maxlim: 299   bits: 10/9
c ---[ 686]---> Adder-cost: 94   maxlim: 517   bits: 11/10
c ---[ 685]---> Adder-cost: 76   maxlim: 775   bits: 11/10
c ---[ 684]---> Adder-cost: 79   maxlim: 357   bits: 10/9
c ---[ 683]---> Adder-cost: 128   maxlim: 224   bits: 9/8
c ---[ 682]---> Adder-cost: 75   maxlim: 319   bits: 10/9
c ---[ 681]---> Adder-cost: 134   maxlim: 191   bits: 9/8
c ---[ 680]---> Adder-cost: 147   maxlim: 438   bits: 10/9
c ---[ 679]---> Adder-cost: 165   maxlim: 345   bits: 10/9
c ---[ 678]---> Adder-cost: 151   maxlim: 611   bits: 11/10
c ---[ 677]---> Adder-cost: 117   maxlim: 823   bits: 11/10
c ---[ 676]---> Adder-cost: 143   maxlim: 352   bits: 10/9
c ---[ 675]---> Adder-cost: 130   maxlim: 332   bits: 10/9
c ---[ 674]---> Adder-cost: 73   maxlim: 423   bits: 10/9
c ---[ 673]---> Adder-cost: 141   maxlim: 299   bits: 10/9
c ---[ 672]---> Adder-cost: 143   maxlim: 642   bits: 11/10
c ---[ 671]---> Adder-cost: 167   maxlim: 544   bits: 11/10
c ---[ 670]---> Adder-cost: 157   maxlim: 725   bits: 11/10
c ---[ 669]---> Adder-cost: 116   maxlim: 1157   bits: 12/11
c ---[ 668]---> Adder-cost: 147   maxlim: 556   bits: 11/10
c ---[ 667]---> Adder-cost: 120   maxlim: 309   bits: 10/9
c ---[ 666]---> Adder-cost: 108   maxlim: 489   bits: 10/9
c ---[ 665]---> Adder-cost: 108   maxlim: 652   bits: 11/10
c ---[ 663]---> Adder-cost: 134   maxlim: 1088   bits: 12/11
c ---[ 662]---> Adder-cost: 132   maxlim: 200   bits: 9/8
c ---[ 661]---> Adder-cost: 128   maxlim: 418   bits: 10/9
c ---[ 660]---> Adder-cost: 128   maxlim: 1026   bits: 12/11
c ---[ 658]---> Adder-cost: 134   maxlim: 427   bits: 10/9
c ---[ 657]---> Adder-cost: 127   maxlim: 659   bits: 11/10
c ---[ 656]---> Adder-cost: 128   maxlim: 1234   bits: 12/11
c ---[ 655]---> Adder-cost: 134   maxlim: 1043   bits: 12/11
c ---[ 653]---> Adder-cost: 104   maxlim: 373   bits: 10/9
c ---[ 652]---> Adder-cost: 129   maxlim: 981   bits: 11/10
c ---[ 651]---> Adder-cost: 134   maxlim: 197   bits: 9/8
c ---[ 650]---> Adder-cost: 145   maxlim: 443   bits: 10/9
c ---[ 649]---> Adder-cost: 106   maxlim: 669   bits: 11/10
c ---[ 648]---> Adder-cost: 128   maxlim: 1252   bits: 12/11
c ---[ 647]---> Adder-cost: 96   maxlim: 563   bits: 11/10
c ---[ 646]---> Adder-cost: 82   maxlim: 556   bits: 11/10
c ---[ 645]---> Adder-cost: 86   maxlim: 393   bits: 10/9
c ---[ 644]---> Adder-cost: 112   maxlim: 1040   bits: 12/11
c ---[ 643]---> Adder-cost: 117   maxlim: 920   bits: 11/10
c ---[ 642]---> Adder-cost: 109   maxlim: 640   bits: 11/10
c ---[ 641]---> Adder-cost: 96   maxlim: 627   bits: 11/10
c ---[ 640]---> Adder-cost: 82   maxlim: 621   bits: 11/10
c ---[ 639]---> Adder-cost: 92   maxlim: 458   bits: 10/9
c ---[ 638]---> Adder-cost: 120   maxlim: 1259   bits: 12/11
c ---[ 637]---> Adder-cost: 120   maxlim: 1139   bits: 12/11
c ---[ 636]---> Adder-cost: 121   maxlim: 861   bits: 11/10
c ---[ 635]---> Adder-cost: 98   maxlim: 586   bits: 11/10
c ---[ 634]---> Adder-cost: 78   maxlim: 580   bits: 11/10
c ---[ 633]---> Adder-cost: 86   maxlim: 417   bits: 10/9
c ---[ 632]---> Adder-cost: 120   maxlim: 1131   bits: 12/11
c ---[ 631]---> Adder-cost: 121   maxlim: 1011   bits: 11/10
c ---[ 630]---> Adder-cost: 109   maxlim: 731   bits: 11/10
c ---[ 629]---> Adder-cost: 103   maxlim: 731   bits: 11/10
c ---[ 628]---> Adder-cost: 76   maxlim: 725   bits: 11/10
c ---[ 627]---> Adder-cost: 94   maxlim: 562   bits: 11/10
c ---[ 626]---> Adder-cost: 113   maxlim: 208   bits: 9/8
c ---[ 625]---> Adder-cost: 118   maxlim: 1222   bits: 12/11
c ---[ 624]---> Adder-cost: 117   maxlim: 942   bits: 11/10
c ---[ 623]---> Adder-cost: 121   maxlim: 608   bits: 11/10
c ---[ 622]---> Adder-cost: 102   maxlim: 608   bits: 11/10
c ---[ 621]---> Adder-cost: 40   maxlim: 491   bits: 10/9
c ---[ 620]---> Adder-cost: 57   maxlim: 409   bits: 10/9
c ---[ 619]---> Adder-cost: 101   maxlim: 268   bits: 10/9
c ---[ 618]---> Adder-cost: 89   maxlim: 268   bits: 10/9
c ---[ 617]---> Adder-cost: 97   maxlim: 314   bits: 10/9
c ---[ 616]---> Adder-cost: 96   maxlim: 226   bits: 9/8
c ---[ 615]---> Adder-cost: 103   maxlim: 891   bits: 11/10
c ---[ 614]---> Adder-cost: 94   maxlim: 491   bits: 10/9
c ---[ 613]---> Adder-cost: 96   maxlim: 491   bits: 10/9
c ---[ 612]---> Adder-cost: 96   maxlim: 536   bits: 11/10
c ---[ 611]---> Adder-cost: 98   maxlim: 448   bits: 10/9
c ---[ 610]---> Adder-cost: 100   maxlim: 1113   bits: 12/11
c ---[ 609]---> Adder-cost: 97   maxlim: 262   bits: 10/9
c ---[ 608]---> Adder-cost: 89   maxlim: 262   bits: 10/9
c ---[ 607]---> Adder-cost: 95   maxlim: 308   bits: 10/9
c ---[ 606]---> Adder-cost: 92   maxlim: 220   bits: 9/8
c ---[ 605]---> Adder-cost: 99   maxlim: 885   bits: 11/10
c ---[ 604]---> Adder-cost: 100   maxlim: 480   bits: 10/9
c ---[ 603]---> Adder-cost: 98   maxlim: 480   bits: 10/9
c ---[ 602]---> Adder-cost: 96   maxlim: 532   bits: 11/10
c ---[ 601]---> Adder-cost: 96   maxlim: 438   bits: 10/9
c ---[ 600]---> Adder-cost: 92   maxlim: 1103   bits: 12/11
c ---[ 599]---> Adder-cost: 99   maxlim: 278   bits: 10/9
c ---[ 598]---> Adder-cost: 95   maxlim: 278   bits: 10/9
c ---[ 597]---> Adder-cost: 91   maxlim: 324   bits: 10/9
c ---[ 596]---> Adder-cost: 94   maxlim: 236   bits: 9/8
c ---[ 595]---> Adder-cost: 97   maxlim: 901   bits: 11/10
c ---[ 594]---> Adder-cost: 108   maxlim: 510   bits: 10/9
c ---[ 593]---> Adder-cost: 98   maxlim: 510   bits: 10/9
c ---[ 592]---> Adder-cost: 94   maxlim: 556   bits: 11/10
c ---[ 591]---> Adder-cost: 96   maxlim: 468   bits: 10/9
c ---[ 590]---> Adder-cost: 98   maxlim: 1133   bits: 12/11
c ---[ 589]---> Adder-cost: 125   maxlim: 869   bits: 11/10
c ---[ 588]---> Adder-cost: 127   maxlim: 923   bits: 11/10
c ---[ 587]---> Adder-cost: 120   maxlim: 325   bits: 10/9
c ---[ 586]---> Adder-cost: 128   maxlim: 1266   bits: 12/11
c ---[ 585]---> Adder-cost: 115   maxlim: 183   bits: 9/8
c ---[ 584]---> Adder-cost: 119   maxlim: 719   bits: 11/10
c ---[ 583]---> Adder-cost: 63   maxlim: 358   bits: 10/9
c ---[ 582]---> Adder-cost: 59   maxlim: 402   bits: 10/9
c ---[ 580]---> Adder-cost: 40   maxlim: 495   bits: 10/9
c ---[ 578]---> Adder-cost: 59   maxlim: 1192   bits: 12/11
c ---[ 577]---> Adder-cost: 61   maxlim: 470   bits: 10/9
c ---[ 575]---> Adder-cost: 34   maxlim: 526   bits: 11/10
c ---[ 573]---> Adder-cost: 63   maxlim: 1028   bits: 12/11
c ---[ 572]---> Adder-cost: 61   maxlim: 374   bits: 10/9
c ---[ 569]---> Adder-cost: 42   maxlim: 823   bits: 11/10
c ---[ 568]---> Adder-cost: 40   maxlim: 455   bits: 10/9
c ---[ 567]---> Adder-cost: 74   maxlim: 977   bits: 11/10
c ---[ 566]---> Adder-cost: 75   maxlim: 1031   bits: 12/11
c ---[ 565]---> Adder-cost: 51   maxlim: 385   bits: 10/9
c ---[ 564]---> Adder-cost: 52   maxlim: 796   bits: 11/10
c ---[ 563]---> Adder-cost: 35   maxlim: 450   bits: 10/9
c ---[ 562]---> Adder-cost: 58   maxlim: 882   bits: 11/10
c ---[ 561]---> Adder-cost: 78   maxlim: 903   bits: 11/10
c ---[ 560]---> Adder-cost: 51   maxlim: 284   bits: 10/9
c ---[ 559]---> Adder-cost: 26   maxlim: 450   bits: 10/9
c ---[ 557]---> Adder-cost: 61   maxlim: 1303   bits: 12/11
c ---[ 556]---> Adder-cost: 61   maxlim: 1275   bits: 12/11
c ---[ 555]---> Adder-cost: 57   maxlim: 943   bits: 11/10
c ---[ 554]---> Adder-cost: 60   maxlim: 484   bits: 10/9
c ---[ 553]---> Adder-cost: 48   maxlim: 433   bits: 10/9
c ---[ 552]---> Adder-cost: 58   maxlim: 1070   bits: 12/11
c ---[ 551]---> Adder-cost: 66   maxlim: 1238   bits: 12/11
c ---[ 550]---> Adder-cost: 63   maxlim: 1081   bits: 12/11
c ---[ 549]---> Adder-cost: 46   maxlim: 840   bits: 11/10
c ---[ 548]---> Adder-cost: 55   maxlim: 379   bits: 10/9
c ---[ 547]---> Adder-cost: 51   maxlim: 328   bits: 10/9
c ---[ 546]---> Adder-cost: 60   maxlim: 965   bits: 11/10
c ---[ 545]---> Adder-cost: 32   maxlim: 412   bits: 10/9
c ---[ 544]---> Adder-cost: 34   maxlim: 184   bits: 9/8
c ---[ 543]---> Adder-cost: 41   maxlim: 374   bits: 10/9
c ---[ 541]---> Adder-cost: 53   maxlim: 1152   bits: 12/11
c ---[ 540]---> Adder-cost: 58   maxlim: 818   bits: 11/10
c ---[ 539]---> Adder-cost: 70   maxlim: 695   bits: 11/10
c ---[ 538]---> Adder-cost: 75   maxlim: 644   bits: 11/10
c ---[ 537]---> Adder-cost: 58   maxlim: 939   bits: 11/10
c ---[ 536]---> Adder-cost: 57   maxlim: 942   bits: 11/10
c ---[ 535]---> Adder-cost: 52   maxlim: 632   bits: 11/10
c ---[ 532]---> Adder-cost: 46   maxlim: 636   bits: 11/10
c ---[ 531]---> Adder-cost: 20   maxlim: 394   bits: 10/9
c ---[ 530]---> Adder-cost: 40   maxlim: 166   bits: 9/8
c ---[ 529]---> Adder-cost: 46   maxlim: 356   bits: 10/9
c ---[ 528]---> Adder-cost: 35   maxlim: 739   bits: 11/10
c ---[ 527]---> Adder-cost: 57   maxlim: 1089   bits: 12/11
c ---[ 526]---> Adder-cost: 58   maxlim: 814   bits: 11/10
c ---[ 525]---> Adder-cost: 54   maxlim: 672   bits: 11/10
c ---[ 524]---> Adder-cost: 68   maxlim: 621   bits: 11/10
c ---[ 523]---> Adder-cost: 44   maxlim: 912   bits: 11/10
c ---[ 522]---> Adder-cost: 48   maxlim: 972   bits: 11/10
c ---[ 521]---> Adder-cost: 60   maxlim: 862   bits: 11/10
c ---[ 518]---> Adder-cost: 43   maxlim: 503   bits: 10/9
c ---[ 517]---> Adder-cost: 110   maxlim: 1326   bits: 12/11
c ---[ 516]---> Adder-cost: 58   maxlim: 868   bits: 11/10
c ---[ 515]---> Adder-cost: 110   maxlim: 1480   bits: 12/11
c ---[ 514]---> Adder-cost: 60   maxlim: 935   bits: 11/10
c ---[ 513]---> Adder-cost: 72   maxlim: 1428   bits: 12/11
c ---[ 512]---> Adder-cost: 58   maxlim: 927   bits: 11/10
c ---[ 511]---> Adder-cost: 49   maxlim: 541   bits: 11/10
c ---[ 510]---> Adder-cost: 54   maxlim: 1026   bits: 12/11
c ---[ 509]---> Adder-cost: 66   maxlim: 1288   bits: 12/11
c ---[ 508]---> Adder-cost: 38   maxlim: 830   bits: 11/10
c ---[ 507]---> Adder-cost: 66   maxlim: 1442   bits: 12/11
c ---[ 506]---> Adder-cost: 45   maxlim: 828   bits: 11/10
c ---[ 505]---> Adder-cost: 60   maxlim: 1322   bits: 12/11
c ---[ 504]---> Adder-cost: 66   maxlim: 937   bits: 11/10
c ---[ 503]---> Adder-cost: 57   maxlim: 483   bits: 10/9
c ---[ 502]---> Adder-cost: 47   maxlim: 917   bits: 11/10
c ---[ 501]---> Adder-cost: 80   maxlim: 1605   bits: 12/11
c ---[ 500]---> Adder-cost: 62   maxlim: 828   bits: 11/10
c ---[ 499]---> Adder-cost: 69   maxlim: 1759   bits: 12/11
c ---[ 498]---> Adder-cost: 82   maxlim: 1468   bits: 12/11
c ---[ 497]---> Adder-cost: 92   maxlim: 1914   bits: 12/11
c ---[ 496]---> Adder-cost: 103   maxlim: 1481   bits: 12/11
c ---[ 495]---> Adder-cost: 81   maxlim: 754   bits: 11/10
c ---[ 494]---> Adder-cost: 79   maxlim: 1560   bits: 12/11
c ---[ 493]---> Adder-cost: 90   maxlim: 1497   bits: 12/11
c ---[ 492]---> Adder-cost: 58   maxlim: 724   bits: 11/10
c ---[ 491]---> Adder-cost: 81   maxlim: 1651   bits: 12/11
c ---[ 490]---> Adder-cost: 94   maxlim: 1264   bits: 12/11
c ---[ 489]---> Adder-cost: 96   maxlim: 1715   bits: 12/11
c ---[ 488]---> Adder-cost: 93   maxlim: 1367   bits: 12/11
c ---[ 486]---> Adder-cost: 77   maxlim: 1356   bits: 12/11
c ---[ 485]---> Adder-cost: 75   maxlim: 1305   bits: 12/11
c ---[ 484]---> Adder-cost: 71   maxlim: 884   bits: 11/10
c ---[ 483]---> Adder-cost: 74   maxlim: 766   bits: 11/10
c ---[ 482]---> Adder-cost: 118   maxlim: 1452   bits: 12/11
c ---[ 481]---> Adder-cost: 76   maxlim: 664   bits: 11/10
c ---[ 480]---> Adder-cost: 77   maxlim: 1552   bits: 12/11
c ---[ 479]---> Adder-cost: 88   maxlim: 1299   bits: 12/11
c ---[ 478]---> Adder-cost: 70   maxlim: 666   bits: 11/10
c ---[ 477]---> Adder-cost: 136   maxlim: 1573   bits: 12/11
c ---[ 476]---> Adder-cost: 73   maxlim: 1325   bits: 12/11
c ---[ 475]---> Adder-cost: 92   maxlim: 1058   bits: 12/11
c ---[ 473]---> Adder-cost: 92   maxlim: 709   bits: 11/10
c ---[ 472]---> Adder-cost: 144   maxlim: 1597   bits: 12/11
c ---[ 471]---> Adder-cost: 63   maxlim: 1025   bits: 12/11
c ---[ 470]---> Adder-cost: 84   maxlim: 711   bits: 11/10
c ---[ 469]---> Adder-cost: 89   maxlim: 1555   bits: 12/11
c ---[ 468]---> Adder-cost: 81   maxlim: 1309   bits: 12/11
c ---[ 467]---> Adder-cost: 59   maxlim: 729   bits: 11/10
c ---[ 465]---> Adder-cost: 71   maxlim: 944   bits: 11/10
c ---[ 464]---> Adder-cost: 45   maxlim: 588   bits: 11/10
c ---[ 463]---> Adder-cost: 64   maxlim: 1080   bits: 12/11
c ---[ 462]---> Adder-cost: 77   maxlim: 585   bits: 11/10
c ---[ 461]---> Adder-cost: 77   maxlim: 654   bits: 11/10
c ---[ 460]---> Adder-cost: 75   maxlim: 950   bits: 11/10
c ---[ 459]---> Adder-cost: 65   maxlim: 880   bits: 11/10
c ---[ 458]---> Adder-cost: 45   maxlim: 523   bits: 11/10
c ---[ 457]---> Adder-cost: 65   maxlim: 1015   bits: 11/10
c ---[ 454]---> Adder-cost: 66   maxlim: 729   bits: 11/10
c ---[ 453]---> Adder-cost: 63   maxlim: 921   bits: 11/10
c ---[ 452]---> Adder-cost: 47   maxlim: 564   bits: 11/10
c ---[ 451]---> Adder-cost: 58   maxlim: 1056   bits: 12/11
c ---[ 450]---> Adder-cost: 68   maxlim: 494   bits: 10/9
c ---[ 449]---> Adder-cost: 61   maxlim: 563   bits: 11/10
c ---[ 448]---> Adder-cost: 50   maxlim: 859   bits: 11/10
c ---[ 447]---> Adder-cost: 69   maxlim: 776   bits: 11/10
c ---[ 446]---> Adder-cost: 54   maxlim: 419   bits: 10/9
c ---[ 445]---> Adder-cost: 61   maxlim: 911   bits: 11/10
c ---[ 444]---> Adder-cost: 72   maxlim: 1417   bits: 12/11
c ---[ 442]---> Adder-cost: 67   maxlim: 648   bits: 11/10
c ---[ 441]---> Adder-cost: 72   maxlim: 1159   bits: 12/11
c ---[ 440]---> Adder-cost: 70   maxlim: 796   bits: 11/10
c ---[ 438]---> Adder-cost: 28   maxlim: 165   bits: 9/8
c ---[ 437]---> Adder-cost: 40   maxlim: 437   bits: 10/9
c ---[ 436]---> Adder-cost: 56   maxlim: 1051   bits: 12/11
c ---[ 435]---> Adder-cost: 64   maxlim: 1016   bits: 11/10
c ---[ 434]---> Adder-cost: 67   maxlim: 971   bits: 11/10
c ---[ 433]---> Adder-cost: 54   maxlim: 1169   bits: 12/11
c ---[ 432]---> Adder-cost: 59   maxlim: 479   bits: 10/9
c ---[ 431]---> Adder-cost: 70   maxlim: 828   bits: 11/10
c ---[ 430]---> Adder-cost: 65   maxlim: 793   bits: 11/10
c ---[ 429]---> Adder-cost: 64   maxlim: 749   bits: 11/10
c ---[ 428]---> Adder-cost: 63   maxlim: 947   bits: 11/10
c ---[ 427]---> Adder-cost: 52   maxlim: 257   bits: 10/9
c ---[ 426]---> Adder-cost: 60   maxlim: 1057   bits: 12/11
c ---[ 425]---> Adder-cost: 57   maxlim: 1022   bits: 11/10
c ---[ 424]---> Adder-cost: 71   maxlim: 977   bits: 11/10
c ---[ 423]---> Adder-cost: 46   maxlim: 1175   bits: 12/11
c ---[ 422]---> Adder-cost: 55   maxlim: 485   bits: 10/9
c ---[ 421]---> Adder-cost: 56   maxlim: 839   bits: 11/10
c ---[ 420]---> Adder-cost: 53   maxlim: 804   bits: 11/10
c ---[ 419]---> Adder-cost: 66   maxlim: 753   bits: 11/10
c ---[ 418]---> Adder-cost: 57   maxlim: 957   bits: 11/10
c ---[ 417]---> Adder-cost: 58   maxlim: 267   bits: 10/9
c ---[ 416]---> Adder-cost: 58   maxlim: 1041   bits: 12/11
c ---[ 415]---> Adder-cost: 55   maxlim: 1006   bits: 11/10
c ---[ 414]---> Adder-cost: 61   maxlim: 961   bits: 11/10
c ---[ 413]---> Adder-cost: 56   maxlim: 1159   bits: 12/11
c ---[ 412]---> Adder-cost: 55   maxlim: 469   bits: 10/9
c ---[ 411]---> Adder-cost: 60   maxlim: 809   bits: 11/10
c ---[ 410]---> Adder-cost: 46   maxlim: 774   bits: 11/10
c ---[ 409]---> Adder-cost: 66   maxlim: 729   bits: 11/10
c ---[ 408]---> Adder-cost: 55   maxlim: 927   bits: 11/10
c ---[ 407]---> Adder-cost: 49   maxlim: 237   bits: 9/8
c ---[ 406]---> Adder-cost: 82   maxlim: 775   bits: 11/10
c ---[ 405]---> Adder-cost: 81   maxlim: 686   bits: 11/10
c ---[ 404]---> Adder-cost: 84   maxlim: 1404   bits: 12/11
c ---[ 402]---> Adder-cost: 82   maxlim: 1426   bits: 12/11
c ---[ 401]---> Adder-cost: 87   maxlim: 1010   bits: 11/10
c ---[ 400]---> Adder-cost: 34   maxlim: 608   bits: 11/10
c ---[ 399]---> Adder-cost: 32   maxlim: 529   bits: 11/10
c ---[ 397]---> Adder-cost: 1992   maxlim: 571   bits: 11/10
c ---[ 396]---> Adder-cost: 166   maxlim: 399   bits: 10/9
c ---[ 395]---> Adder-cost: 307   maxlim: 274   bits: 10/9
c ---[ 394]---> Adder-cost: 426   maxlim: 1316   bits: 11/11
c ---[ 393]---> Adder-cost: 540   maxlim: 1397   bits: 11/11
c ---[ 392]---> Adder-cost: 533   maxlim: 98   bits: 8/7
c ---[ 391]---> Adder-cost: 62   maxlim: 186   bits: 8/8
c ---[ 390]---> Adder-cost: 90   maxlim: 119   bits: 8/7
c ---[ 389]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 386]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 384]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 383]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 381]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 379]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 376]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 374]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 373]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 371]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 369]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 368]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 367]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 366]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 363]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 361]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 360]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 358]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 356]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 353]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 351]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 350]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 348]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 346]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 345]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 344]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 343]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 341]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 339]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 337]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 334]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 333]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 331]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 328]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 325]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 324]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 323]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 322]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 321]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 320]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 317]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 316]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 314]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 312]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 311]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 308]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 307]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 305]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 303]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 302]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 301]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 300]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 299]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 298]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 295]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 294]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 292]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 290]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 289]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 286]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 285]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 283]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 281]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 280]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 277]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 274]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 272]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 269]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 268]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 265]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 262]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 260]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 257]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 256]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 255]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 252]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 251]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 249]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 248]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 246]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 245]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 244]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 242]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 241]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 240]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 238]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 236]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 235]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 234]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 233]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 232]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 229]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 228]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 226]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 225]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 223]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 222]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 221]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 219]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 218]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 217]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 215]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 213]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 212]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 211]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 210]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 209]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 208]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 207]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 206]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 205]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 204]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 203]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 202]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 201]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 200]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 199]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 197]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 196]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 194]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 193]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 192]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 191]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 189]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 188]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 186]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 185]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 183]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 182]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 181]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 180]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 178]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 177]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 175]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 174]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 172]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 171]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 170]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 168]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 167]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 165]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 164]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 162]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 161]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 160]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 158]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 155]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 153]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 152]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 150]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 148]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 147]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 146]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 143]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 141]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 140]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 138]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 136]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 135]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 134]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 131]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 129]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 128]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 126]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 124]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 123]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 122]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 119]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 117]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 116]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 114]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 112]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 111]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 110]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 109]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 107]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 105]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 104]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 103]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 101]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 100]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  98]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  97]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  95]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  93]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  92]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  90]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  89]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  87]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  85]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  84]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  82]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  77]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  74]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  73]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  71]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  69]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  68]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  66]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  65]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  63]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  61]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  60]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  58]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  57]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  55]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  54]---> 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: 6   maxlim: 2   bits: 3/2
c ---[  46]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  44]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  43]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  42]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  41]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  37]---> Adder-cost: 378   maxlim: 188   bits: 9/8
c ---[  36]---> Adder-cost: 28   maxlim: 13   bits: 5/4
c ---[  35]---> Adder-cost: 28   maxlim: 13   bits: 5/4
c ---[  34]---> Adder-cost: 28   maxlim: 13   bits: 5/4
c ---[  33]---> Adder-cost: 28   maxlim: 13   bits: 5/4
c ---[  32]---> Adder-cost: 66   maxlim: 32   bits: 7/6
c ---[  31]---> Adder-cost: 63   maxlim: 31   bits: 6/5
c ---[  30]---> Adder-cost: 80   maxlim: 39   bits: 7/6
c ---[  29]---> Adder-cost: 92   maxlim: 45   bits: 7/6
c ---[  28]---> Adder-cost: 244   maxlim: 121   bits: 8/7
c ---[  27]---> Adder-cost: 244   maxlim: 121   bits: 8/7
c ---[  26]---> Adder-cost: 244   maxlim: 121   bits: 8/7
c ---[  25]---> Adder-cost: 244   maxlim: 121   bits: 8/7
c ---[  24]---> Adder-cost: 15   maxlim: 7   bits: 4/3
c ---[  23]---> Adder-cost: 120   maxlim: 59   bits: 7/6
c ---[  22]---> Adder-cost: 18   maxlim: 8   bits: 5/4
c ---[  21]---> Adder-cost: 46   maxlim: 164   bits: 9/8
c ---[  20]---> Adder-cost: 59   maxlim: 184   bits: 9/8
c ---[  19]---> Adder-cost: 46   maxlim: 151   bits: 9/8
c ---[  18]---> Adder-cost: 67   maxlim: 153   bits: 9/8
c ---[  17]---> Adder-cost: 78   maxlim: 179   bits: 9/8
c ---[  16]---> Adder-cost: 82   maxlim: 155   bits: 9/8
c ---[  15]---> Adder-cost: 35   maxlim: 142   bits: 9/8
c ---[  14]---> Adder-cost: 15   maxlim: 56   bits: 7/6
c ---[  13]---> Adder-cost: 31   maxlim: 133   bits: 9/8
c ---[  12]---> Adder-cost: 15   maxlim: 47   bits: 7/6
c ---[  11]---> Adder-cost: 38   maxlim: 82   bits: 8/7
c ---[  10]---> Adder-cost: 41   maxlim: 72   bits: 8/7
c ---[   9]---> Adder-cost: 37   maxlim: 72   bits: 8/7
c ---[   8]---> Adder-cost: 47   maxlim: 95   bits: 8/7
c ---[   7]---> Adder-cost: 49   maxlim: 95   bits: 8/7
c ---[   6]---> Adder-cost: 54   maxlim: 100   bits: 8/7
c ---[   5]---> Adder-cost: 78   maxlim: 118   bits: 8/7
c ---[   4]---> Adder-cost: 65   maxlim: 125   bits: 8/7
c ---[   3]---> Adder-cost: 36   maxlim: 88   bits: 8/7
c ---[   2]---> Adder-cost: 19   maxlim: 57   bits: 7/6
c ---[   1]---> Adder-cost: 73   maxlim: 132   bits: 9/8
c ---[   0]---> Adder-cost: 39   maxlim: 129   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  223572   792658 |   74524       0        0     nan |  0.000 % |
c |       100 |  223550   792596 |   81976      96      545     5.7 |  5.916 % |
c |       250 |  223544   792579 |   90174     245     1542     6.3 |  5.919 % |
c |       475 |  223544   792579 |   99191     470     2436     5.2 |  5.919 % |
c |       815 |  223538   792562 |  109110     809     4312     5.3 |  5.921 % |
c |      1322 |  223538   792562 |  120021    1316     8481     6.4 |  5.921 % |
c |      2083 |  223526   792528 |  132023    2075    13655     6.6 |  5.926 % |
c |      3222 |  223526   792528 |  145226    3214    22694     7.1 |  5.926 % |
c |      4930 |  223520   792511 |  159748    4921    38452     7.8 |  5.929 % |
c |      7492 |  223494   792431 |  175723    7476    61962     8.3 |  5.939 % |
c |     11336 |  223360   791983 |  193296   11294    98842     8.8 |  5.981 % |
c |     17102 |  223148   791281 |  212625   17018   165621     9.7 |  6.044 % |
c |     25751 |  222897   790449 |  233888   25481   313688    12.3 |  6.114 % |
c |     38726 |  222794   790097 |  257277   38409   862049    22.4 |  6.139 % |
c |     58187 |  222614   789530 |  283004   57819  1282330    22.2 |  6.194 % |
c |     87379 |  222237   788226 |  311305   86779  1743374    20.1 |  6.256 % |
c |    131169 |  221939   787226 |  342435  130344  3037834    23.3 |  6.321 % |
c |    196854 |  221427   785467 |  376679  195575  8729226    44.6 |  6.409 % |
c |    295381 |  221142   784502 |  414347  293859 13154872    44.8 |  6.469 % |
c ==============================================================================
c [1mFound solution: 134217[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11276   maxlim: 187614   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    320016 |  299973  1066096 |   99991  318484 13573703    42.6 |  6.469 % |
c |    320116 |  299973  1066096 |  109990   27914   331257    11.9 |  5.074 % |
c |    320268 |  299973  1066096 |  120989   28066   332360    11.8 |  5.074 % |
c |    320494 |  299973  1066096 |  133088   28292   334645    11.8 |  5.074 % |
c |    320831 |  299973  1066096 |  146396   28629   338383    11.8 |  5.074 % |
c |    321338 |  299973  1066096 |  161036   29136   343562    11.8 |  5.074 % |
c |    322097 |  299973  1066096 |  177140   29895   351395    11.8 |  5.074 % |
c |    323236 |  299970  1066087 |  194854   31033   364221    11.7 |  5.076 % |
c |    324945 |  299970  1066087 |  214339   32742   381854    11.7 |  5.076 % |
c |    327507 |  299955  1066034 |  235773   35301   408729    11.6 |  5.078 % |
c |    331351 |  299955  1066034 |  259350   39145   455344    11.6 |  5.078 % |
c |    337117 |  299955  1066034 |  285285   44911   537460    12.0 |  5.078 % |
c |    345766 |  299955  1066034 |  313814   53560   666871    12.5 |  5.078 % |
c |    358740 |  299955  1066034 |  345196   66534   931056    14.0 |  5.078 % |
c |    378201 |  299955  1066034 |  379715   85995  1229545    14.3 |  5.078 % |
c |    407395 |  299922  1065919 |  417687  115173  1892235    16.4 |  5.084 % |
c |    451184 |  299850  1065664 |  459455  158881  2878486    18.1 |  5.092 % |
c |    516868 |  299736  1065259 |  505401  224522  4894785    21.8 |  5.105 % |
c |    615394 |  299670  1065024 |  555941  322997  8744517    27.1 |  5.111 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1001_bit0 -C1002_bit0 -C1003_bit0 C1004_bit0 -C1005_bit0 -C1006_bit0 -C1009_bit0 C1010_bit0 -C1011_bit0 -C1014_bit0 -C1017_bit0 -C1019_bit0 -C1020_bit0 -C1021_bit0 -C1022_bit0 -C1023_bit0 -C1024_bit0 C1027_bit0 -C1029_bit0 -C1030_bit0 -C1031_bit0 -C1032_bit0 -C1033_bit0 -C1034_bit0 -C1035_bit0 -C1036_bit0 -C1037_bit0 -C1038_bit0 -C1039_bit0 -C1042_bit0 C1044_bit0 -C1045_bit0 -C1046_bit0 -C1047_bit0 C1048_bit0 -C1049_bit0 C1050_bit0 -C1051_bit0 -C1054_bit0 -C1056_bit0 -C1057_bit0 -C1058_bit0 C1059_bit0 -C1060_bit0 -C1061_bit0 -C1062_bit0 -C1065_bit0 -C1066_bit0 -C1067_bit0 C1068_bit0 -C1070_bit0 -C1073_bit0 -C1074_bit0 C1075_bit0 -C1076_bit0 -C1077_bit0 -C1078_bit0 -C1079_bit0 -C1080_bit0 -C1083_bit0 -C1085_bit0 -C1086_bit0 -C1087_bit0 -C1088_bit0 C1089_bit0 C1090_bit0 C1091_bit0 -C1092_bit0 -C1093_bit0 -C1094_bit0 -C1095_bit0 C1098_bit0 C1100_bit0 C1101_bit0 -C1102_bit0 -C1103_bit0 -C1104_bit0 -C1105_bit0 -C1106_bit0 -C1107_bit0 -C1110_bit0 -C1112_bit0 -C1113_bit0 -C1114_bit0 -C1115_bit0 C1116_bit0 -C1117_bit0 -C1119_bit0 -C1120_bit0 -C1121_bit0 -C1122_bit0 -C1123_bit0 -C1124_bit0 C1126_bit0 -C1127_bit0 -C1128_bit0 C1129_bit0 C1131_bit0 -C1132_bit0 -C1133_bit0 -C1134_bit0 -C1135_bit0 C1136_bit0 C1137_bit0 -C1139_bit0 C1140_bit0 C1141_bit0 -C1142_bit0 -C1143_bit0 -C1144_bit0 -C1145_bit0 -C1148_bit0 -C1149_bit0 -C1150_bit0 C1153_bit0 C1156_bit0 -C1158_bit0 -C1159_bit0 -C1160_bit0 -C1161_bit0 -C1162_bit0 -C1163_bit0 -C1166_bit0 -C1168_bit0 -C1169_bit0 -C1170_bit0 -C1171_bit0 -C1172_bit0 -C1173_bit0 -C1174_bit0 -C1175_bit0 -C1176_bit0 -C1177_bit0 -C1178_bit0 C1181_bit0 -C1183_bit0 -C1184_bit0 -C1185_bit0 C1186_bit0 -C1187_bit0 C1188_bit0 -C1189_bit0 C1190_bit0 -C1193_bit0 -C1195_bit0 C1196_bit0 -C1197_bit0 -C1198_bit0 C1199_bit0 -C1200_bit0 -C1201_bit0 -C1204_bit0 C1205_bit0 -C1206_bit0 -C1207_bit0 -C1209_bit0 -C1212_bit0 -C1213_bit0 -C1214_bit0 -C1215_bit0 -C1216_bit0 -C1217_bit0 -C1218_bit0 -C1219_bit0 -C1222_bit0 -C1224_bit0 -C1225_bit0 -C1226_bit0 -C1227_bit0 -C1228_bit0 -C1229_bit0 -C1230_bit0 C1231_bit0 -C1232_bit0 -C1233_bit0 -C1234_bit0 C1237_bit0 -C1239_bit0 -C1240_bit0 -C1241_bit0 -C1242_bit0 -C1243_bit0 -C1244_bit0 C1245_bit0 -C1246_bit0 -C1249_bit0 C1251_bit0 -C1252_bit0 -C1253_bit0 -C1254_bit0 -C1255_bit0 -C1256_bit0 C1258_bit0 -C1259_bit0 C1260_bit0 -C1261_bit0 -C1262_bit0 C1263_bit0 C1265_bit0 -C1266_bit0 -C1267_bit0 -C1268_bit0 C1270_bit0 -C1271_bit0 -C1272_bit0 C1273_bit0 -C1274_bit0 -C1275_bit0 -C1276_bit0 C1278_bit0 -C1279_bit0 -C1280_bit0 C1281_bit0 -C1283_bit0 -C1284_bit0 -C1285_bit0 -C1286_bit0 -C1289_bit0 -C1290_bit0 -C1291_bit0 -C1292_bit0 -C1293_bit0 -C1294_bit0 -C1295_bit0 C1296_bit0 -C1297_bit0 -C1298_bit0 -C1299_bit0 -C1300_bit0 -C1303_bit0 -C1304_bit0 -C1305_bit0 -C1306_bit0 -C1307_bit0 -C1308_bit0 -C1309_bit0 -C1310_bit0 -C1313_bit0 -C1314_bit0 -C1315_bit0 -C1316_bit0 -C1317_bit0 -C1318_bit0 -C1319_bit0 C1320_bit0 -C1321_bit0 -C1322_bit0 -C1323_bit0 -C1326_bit0 -C1327_bit0 -C1328_bit0 -C1329_bit0 -C1330_bit0 -C1331_bit0 C1332_bit0 C1333_bit0 -C1335_bit0 -C1338_bit0 -C1339_bit0 -C1340_bit0 -C1341_bit0 -C1343_bit0 -C1344_bit0 -C1345_bit0 -C1347_bit0 -C1348_bit0 -C1349_bit0 -C1351_bit0 -C1352_bit0 -C1353_bit0 -C1354_bit0 -C1356_bit0 -C1357_bit0 -C1358_bit0 -C1359_bit0 -C1360_bit0 -C1361_bit0 -C1362_bit0 -C1363_bit0 -C1366_bit0 -C1367_bit0 -C1368_bit0 C1369_bit0 -C1370_bit0 -C1371_bit0 -C1372_bit0 -C1373_bit0 -C1374_bit0 -C1375_bit0 -C1376_bit0 -C1377_bit0 -C1380_bit0 -C1381_bit0 -C1382_bit0 -C1383_bit0 C1384_bit0 -C1385_bit0 -C1386_bit0 C1387_bit0 -C1390_bit0 -C1391_bit0 -C1392_bit0 -C1393_bit0 -C1394_bit0 -C1395_bit0 -C1396_bit0 C1397_bit0 -C1398_bit0 -C1399_bit0 -C1400_bit0 -C1403_bit0 -C1404_bit0 -C1405_bit0 -C1406_bit0 -C1407_bit0 -C1408_bit0 -C1409_bit0 C1410_bit0 -C1411_bit0 -C1412_bit0 -C1415_bit0 -C1416_bit0 -C1417_bit0 C1418_bit0 -C1419_bit0 -C1420_bit0 C1421_bit0 -C1422_bit0 -C1423_bit0 -C1424_bit0 C1425_bit0 -C1426_bit0 -C1428_bit0 -C1429_bit0 -C1430_bit0 -C1431_bit0 -C1432_bit0 -C1433_bit0 -C1434_bit0 -C1435_bit0 -C1436_bit0 -C1437_bit0 -C1438_bit0 -C1439_bit0 -C1440_bit0 -C1441_bit0 -C1442_bit0 -C1443_bit0 C1444_bit0 -C1445_bit0 -C1446_bit0 -C1447_bit0 -C1448_bit0 C1449_bit0 -C1450_bit0 -C1451_bit0 -C1452_bit0 C1453_bit0 C1454_bit0 -C1456_bit0 -C1457_bit0 -C1458_bit0 -C1459_bit0 -C1460_bit0 C1461_bit0 -C1463_bit0 -C1464_bit0 -C1465_bit0 -C1466_bit0 -C1467_bit0 -C1468_bit0 -C1469_bit0 -C1470_bit0 C1471_bit0 C1472_bit0 -C1473_bit0 -C1474_bit0 -C1475_bit0 -C1476_bit0 -C1479_bit0 -C1480_bit0 -C1481_bit0 -C1482_bit0 -C1483_bit0 -C1484_bit0 -C1485_bit0 -C1486_bit0 -C1489_bit0 C1490_bit0 C1491_bit0 C1492_bit0 -C1493_bit0 -C1494_bit0 -C1495_bit0 -C1496_bit0 -C1497_bit0 -C1498_bit0 -C1499_bit0 -C1500_bit0 -C1501_bit0 -C1502_bit0 -C1503_bit0 -C1506_bit0 -C1507_bit0 C1508_bit0 -C1509_bit0 -C1510_bit0 -C1511_bit0 -C1512_bit0 -C1513_bit0 -C1514_bit0 -C1515_bit0 -C1516_bit0 -C1517_bit0 -C1519_bit0 -C1522_bit0 -C1523_bit0 -C1524_bit0 -C1525_bit0 -C1526_bit0 C1527_bit0 -C1528_bit0 -C1529_bit0 C1530_bit0 -C1531_bit0 -C1532_bit0 -C1533_bit0 -C1535_bit0 -C1536_bit0 -C1537_bit0 C1538_bit0 -C1539_bit0 -C1540_bit0 -C1541_bit0 -C1542_bit0 -C1543_bit0 -C1544_bit0 -C1545_bit0 C1546_bit0 C1549_bit0 -C1550_bit0 -C1551_bit0 C1552_bit0 -C1553_bit0 -C1554_bit0 -C1555_bit0 -C1556_bit0 -C1559_bit0 C1560_bit0 -C1561_bit0 C1562_bit0 -C1563_bit0 -C1564_bit0 -C1565_bit0 -C1566_bit0 -C1567_bit0 -C1568_bit0 -C1569_bit0 -C1570_bit0 -C1571_bit0 -C1572_bit0 C1573_bit0 -C1576_bit0 -C1577_bit0 -C1578_bit0 -C1579_bit0 -C1580_bit0 -C1581_bit0 -C1582_bit0 -C1583_bit0 -C1584_bit0 -C1585_bit0 -C1586_bit0 C1587_bit0 -C1588_bit0 -C1589_bit0 -C1592_bit0 -C1593_bit0 -C1594_bit0 -C1595_bit0 -C1596_bit0 -C1597_bit0 -C1598_bit0 -C1599_bit0 -C1600_bit0 -C1601_bit0 -C1602_bit0 -C1603_bit0 -C1605_bit0 -C1606_bit0 -C1607_bit0 -C1608_bit0 -C1609_bit0 C1610_bit0 C1611_bit0 -C1612_bit0 -C1613_bit0 -C1614_bit0 C1615_bit0 C1616_bit0 C1617_bit0 -C1618_bit0 C1619_bit0 -C1620_bit0 -C1621_bit0 C1622_bit0 -C1623_bit0 -C1624_bit0 -C1625_bit0 -C1626_bit0 -C1627_bit0 -C1628_bit0 -C1629_bit0 -C1630_bit0 C1631_bit0 -C1633_bit0 -C1634_bit0 -C1635_bit0 -C1636_bit0 -C1637_bit0 -C1638_bit0 -C1639_bit0 -C1640_bit0 -C1641_bit0 -C1642_bit0 -C1643_bit0 -C1644_bit0 -C1645_bit0 -C1646_bit0 -C1647_bit0 -C1648_bit0 C1650_bit0 -C1651_bit0 -C1652_bit0 -C1653_bit0 -C1656_bit0 -C1657_bit0 -C1658_bit0 -C1659_bit0 -C1660_bit0 -C1661_bit0 -C1662_bit0 -C1663_bit0 -C1666_bit0 -C1667_bit0 -C1668_bit0 -C1669_bit0 -C1670_bit0 -C1671_bit0 -C1672_bit0 -C1673_bit0 -C1674_bit0 C1675_bit0 -C1676_bit0 -C1677_bit0 -C1678_bit0 -C1679_bit0 -C1680_bit0 -C1683_bit0 -C1684_bit0 -C1685_bit0 C1686_bit0 -C1687_bit0 -C1688_bit0 -C1689_bit0 C1690_bit0 -C1691_bit0 -C1692_bit0 -C1693_bit0 C1694_bit0 -C1696_bit0 -C1699_bit0 -C1700_bit0 -C1701_bit0 -C1702_bit0 -C1703_bit0 -C1704_bit0 -C1705_bit0 -C1706_bit0 C1707_bit0 -C1708_bit0 -C1709_bit0 -C1710_bit0 -C1712_bit0 -C1713_bit0 -C1714_bit0 -C1715_bit0 -C1716_bit0 C1717_bit0 -C1718_bit0 -C1719_bit0 -C1720_bit0 -C1721_bit0 -C1722_bit0 -C1723_bit0 C1726_bit0 -C1727_bit0 C1728_bit0 -C1729_bit0 -C1730_bit0 -C1731_bit0 -C1732_bit0 -C1733_bit0 -C1736_bit0 -C1737_bit0 -C1738_bit0 C1739_bit0 C1740_bit0 -C1741_bit0 -C1742_bit0 -C1743_bit0 -C1744_bit0 -C1745_bit0 -C1746_bit0 -C1747_bit0 -C1748_bit0 -C1749_bit0 -C1750_bit0 -C1753_bit0 -C1754_bit0 -C1755_bit0 -C1756_bit0 -C1757_bit0 -C1758_bit0 -C1759_bit0 C1760_bit0 -C1761_bit0 -C1762_bit0 C1763_bit0 C1764_bit0 C1765_bit0 -C1766_bit0 C1769_bit0 -C1770_bit0 -C1771_bit0 -C1772_bit0 -C1773_bit0 -C1774_bit0 -C1775_bit0 -C1776_bit0 C1777_bit0 -C1778_bit0 -C1779_bit0 -C1780_bit0 -C1782_bit0 -C1783_bit0 -C1784_bit0 -C1785_bit0 -C1786_bit0 -C1787_bit0 C1788_bit0 -C1789_bit0 -C1790_bit0 -C1791_bit0 -C1792_bit0 -C1793_bit0 -C1796_bit0 -C1797_bit0 -C1798_bit0 -C1799_bit0 -C1800_bit0 -C1812_bit0 -C1813_bit0 -C1814_bit0 -C1815_bit0 -C1816_bit0 -C1817_bit0 -C1818_bit0 -C1821_bit0 -C1822_bit0 -C1823_bit0 -C1824_bit0 -C1825_bit0 -C1829_bit0 -C1833_bit0 -C1837_bit0 -C1838_bit0 C1839_bit0 C1840_bit0 -C1841_bit0 -C1842_bit0 -C1843_bit0 C1846_bit0 -C1847_bit0 C1848_bit0 C1849_bit0 -C1850_bit0 -C1851_bit0 -C1854_bit0 -C1856_bit0 -C1860_bit0 -C1864_bit0 C1865_bit0 -C1867_bit0 C1870_bit0 -C1871_bit0 -C1872_bit0 -C1873_bit0 C1875_bit0 -C1876_bit0 C1877_bit0 -C1878_bit0 -C1879_bit0 -C1880_bit0 -C1882_bit0 -C1883_bit0 -C1884_bit0 -C1885_bit0 -C1886_bit0 -C1887_bit0 -C1888_bit0 -C1889_bit0 -C1890_bit0 -C1891_bit0 -C1892_bit0 -C1893_bit0 C1896_bit0 -C1897_bit0 -C1898_bit0 -C1899_bit0 -C1900_bit0 C1904_bit0 -C1908_bit0 -C1912_bit0 -C1913_bit0 -C1914_bit0 -C1915_bit0 -C1916_bit0 C1917_bit0 -C1918_bit0 -C1921_bit0 -C1922_bit0 -C1923_bit0 -C1924_bit0 -C1925_bit0 -C1926_bit0 -C1929_bit0 -C1933_bit0 -C1937_bit0 C1938_bit0 -C1939_bit0 -C1940_bit0 -C1941_bit0 -C1942_bit0 -C1943_bit0 -C1946_bit0 -C1947_bit0 -C1948_bit0 -C1949_bit0 -C1950_bit0 -C1951_bit0 C1952_bit0 -C1954_bit0 -C1955_bit0 -C1956_bit0 -C1959_bit0 C1960_bit0 -C1961_bit0 -C1962_bit0 C1964_bit0 -C1965_bit0 -C1967_bit0 C1970_bit0 -C1971_bit0 -C1972_bit0 -C1973_bit0 -C1974_bit0 -C1975_bit0 -C1976_bit0 -C1977_bit0 -C1978_bit0 -C1979_bit0 C1980_bit0 -C1982_bit0 -C1983_bit0 -C1984_bit0 -C1985_bit0 -C1986_bit0 -C1987_bit0 -C1988_bit0 -C1989_bit0 -C1990_bit0 -C1991_bit0 -C1992_bit0 -C1993_bit0 -C1994_bit0 -C1995_bit0 -C1996_bit0 -C1997_bit0 -C2000_bit0 -C2001_bit0 -C2002_bit0 -C2003_bit0 -C2004_bit0 -C2005_bit0 -C2008_bit0 -C2011_bit0 -C2012_bit0 -C2013_bit0 -C2014_bit0 -C2016_bit0 -C2017_bit0 -C2018_bit0 -C2019_bit0 -C2020_bit0 -C2021_bit0 -C2022_bit0 -C2023_bit0 -C2024_bit0 -C2025_bit0 -C2026_bit0 -C2029_bit0 -C2030_bit0 -C2031_bit0 -C2032_bit0 -C2033_bit0 -C2034_bit0 -C2035_bit0 -C2036_bit0 C2037_bit0 -C2038_bit0 -C2039_bit0 C2040_bit0 -C2041_bit0 -C2042_bit0 -C2043_bit0 -C2045_bit0 -C2048_bit0 -C2049_bit0 C2050_bit0 -C2051_bit0 -C2052_bit0 -C2053_bit0 -C2054_bit0 -C2055_bit0 -C2056_bit0 -C2057_bit0 -C2058_bit0 -C2059_bit0 -C2060_bit0 -C2061_bit0 C2062_bit0 -C2063_bit0 -C2064_bit0 -C2065_bit0 -C2066_bit0 -C2067_bit0 -C2070_bit0 -C2071_bit0 -C2072_bit0 -C2073_bit0 -C2074_bit0 -C2075_bit0 -C2076_bit0 -C2077_bit0 -C2078_bit0 -C2079_bit0 -C2080_bit0 -C2081_bit0 -C2082_bit0 -C2083_bit0 -C2084_bit0 -C2085_bit0 C2086_bit0 -C2087_bit0 -C2088_bit0 -C2091_bit0 -C2092_bit0 -C2093_bit0 -C2094_bit0 -C2095_bit0 -C2096_bit0 C2097_bit0 -C2098_bit0 -C2099_bit0 -C2100_bit0 -C2101_bit0 -C2102_bit0 -C2103_bit0 -C2106_bit0 -C2107_bit0 C2108_bit0 -C2109_bit0 -C2110_bit0 -C2111_bit0 -C2112_bit0 -C2113_bit0 -C2114_bit0 -C2115_bit0 -C2116_bit0 -C2117_bit0 -C2118_bit0 -C2119_bit0 -C2120_bit0 C2121_bit0 -C2122_bit0 -C2123_bit0 -C2124_bit0 -C2126_bit0 -C2127_bit0 -C2128_bit0 -C2129_bit0 -C2130_bit0 -C2131_bit0 -C2132_bit0 -C2133_bit0 -C2134_bit0 -C2135_bit0 C2136_bit0 C2137_bit0 -C2138_bit0 -C2139_bit0 -C2140_bit0 -C2141_bit0 -C2144_bit0 C2145_bit0 -C2146_bit0 -C2147_bit0 -C2148_bit0 -C2149_bit0 -C2152_bit0 -C2155_bit0 C2156_bit0 -C2157_bit0 -C2158_bit0 -C2160_bit0 -C2161_bit0 -C2162_bit0 -C2163_bit0 -C2164_bit0 -C2165_bit0 C2166_bit0 -C2167_bit0 -C2168_bit0 -C2169_bit0 -C2170_bit0 C2173_bit0 -C2174_bit0 -C2175_bit0 -C2176_bit0 -C2177_bit0 -C2178_bit0 -C2179_bit0 -C2180_bit0 -C2181_bit0 C2182_bit0 -C2183_bit0 -C2184_bit0 C2185_bit0 -C2186_bit0 -C2187_bit0 -C2189_bit0 -C2192_bit0 -C2193_bit0 -C2194_bit0 -C2195_bit0 -C2196_bit0 -C2197_bit0 -C2198_bit0 C2199_bit0 -C2200_bit0 -C2201_bit0 C2202_bit0 -C2203_bit0 -C2204_bit0 -C2205_bit0 -C2206_bit0 -C2207_bit0 -C2208_bit0 C2209_bit0 -C2210_bit0 -C2211_bit0 -C2214_bit0 C2215_bit0 C2216_bit0 -C2217_bit0 -C2218_bit0 -C2219_bit0 -C2220_bit0 -C2221_bit0 -C2222_bit0 -C2223_bit0 -C2224_bit0 C2225_bit0 -C2226_bit0 C2227_bit0 C2228_bit0 -C2229_bit0 -C2230_bit0 -C2231_bit0 -C2232_bit0 C2235_bit0 -C2236_bit0 -C2237_bit0 C2238_bit0 -C2239_bit0 -C2240_bit0 -C2241_bit0 -C2242_bit0 -C2243_bit0 -C2244_bit0 C2245_bit0 -C2246_bit0 -C2247_bit0 -C2250_bit0 -C2251_bit0 -C2252_bit0 -C2253_bit0 -C2254_bit0 C2255_bit0 -C2256_bit0 -C2257_bit0 -C2258_bit0 -C2259_bit0 -C2260_bit0 -C2261_bit0 -C2262_bit0 -C2263_bit0 -C2264_bit0 C2265_bit0 -C2266_bit0 -C2267_bit0 -C2268_bit0 -C2270_bit0 -C2271_bit0 -C2272_bit0 -C2273_bit0 -C2274_bit0 -C2275_bit0 -C2276_bit0 -C2277_bit0 -C2278_bit0 C2279_bit0 -C2280_bit0 -C2281_bit0 -C2282_bit0 -C2283_bit0 -C2284_bit0 -C2285_bit0 -C2286_bit0 -C2287_bit0 -C2288_bit0 -C2289_bit0 C2290_bit0 -C2291_bit0 -C2292_bit0 -C2293_bit0 -C2294_bit0 -C2295_bit0 C2296_bit0 C2297_bit0 -C2298_bit0 -C2299_bit0 C2300_bit0 C2301_bit0 C2302_bit0 -C2303_bit0 -C2304_bit0 -C2305_bit0 -C2306_bit0 -C2307_bit0 -C2308_bit0 -C2309_bit0 -C2310_bit0 -C2311_bit0 -C2312_bit0 -C2313_bit0 -C2314_bit0 -C2315_bit0 -C2316_bit0 C2317_bit0 -C2318_bit0 -C2319_bit0 C2320_bit0 -C2321_bit0 -C2322_bit0 -C2323_bit0 -C2324_bit0 C2325_bit0 C2326_bit0 -C2327_bit0 -C2328_bit0 -C2329_bit0 C2330_bit0 C2331_bit0 -C2332_bit0 -C2333_bit0 -C2334_bit0 -C2335_bit0 -C2336_bit0 -C2337_bit0 -C2338_bit0 -C2339_bit0 -C2340_bit0 -C2341_bit0 -C2342_bit0 -C2343_bit0 -C2344_bit0 -C2345_bit0 -C2346_bit0 -C2348_bit0 -C2349_bit0 C2351_bit0 -C2352_bit0 -C2353_bit0 -C2354_bit0 -C2355_bit0 -C2356_bit0 -C2357_bit0 -C2358_bit0 -C2359_bit0 -C2360_bit0 C2361_bit0 -C2362_bit0 -C2363_bit0 C2364_bit0 -C2365_bit0 -C2366_bit0 -C2367_bit0 -C2369_bit0 -C2370_bit0 C2371_bit0 -C2372_bit0 -C2373_bit0 -C2374_bit0 -C2375_bit0 -C2376_bit0 -C2377_bit0 -C2378_bit0 C2379_bit0 -C2380_bit0 -C2381_bit0 C2382_bit0 -C2384_bit0 -C2386_bit0 -C2387_bit0 -C2391_bit0 -C2392_bit0 -C2393_bit0 -C2394_bit0 C2395_bit0 C2396_bit0 -C2397_bit0 -C2398_bit0 -C2399_bit0 C2401_bit0 -C2402_bit0 -C2404_bit0 -C2405_bit0 -C2406_bit0 -C2407_bit0 -C2408_bit0 -C2409_bit0 -C2410_bit0 -C2411_bit0 -C2412_bit0 -C2413_bit0 -C2414_bit0 -C2415_bit0 -C2416_bit0 -C2417_bit0 C2418_bit0 -C2419_bit0 -C2420_bit0 -C2422_bit0 -C2423_bit0 -C2424_bit0 -C2425_bit0 -C2426_bit0 -C2427_bit0 C2428_bit0 -C2429_bit0 -C2430_bit0 -C2431_bit0 -C2432_bit0 C2433_bit0 -C2434_bit0 C2435_bit0 -C2436_bit0 -C2437_bit0 -C2438_bit0 C2440_bit0 -C2441_bit0 -C2442_bit0 -C2443_bit0 C2444_bit0 -C2445_bit0 -C2446_bit0 -C2447_bit0 C2448_bit0 -C2449_bit0 -C2450_bit0 -C2451_bit0 -C2452_bit0 -C2453_bit0 -C2455_bit0 -C2457_bit0 -C2458_bit0 C2459_bit0 -C2460_bit0 -C2461_bit0 -C2462_bit0 -C2463_bit0 C2464_bit0 -C2465_bit0 -C2466_bit0 C2467_bit0 -C2468_bit0 -C2469_bit0 -C2470_bit0 C2471_bit0 -C2472_bit0 -C2473_bit0 -C2475_bit0 -C2476_bit0 -C2477_bit0 -C2478_bit0 -C2479_bit0 -C2480_bit0 -C2481_bit0 -C2482_bit0 -C2483_bit0 -C2484_bit0 -C2485_bit0 -C2486_bit0 -C2487_bit0 -C2488_bit0 C2489_bit0 -C2490_bit0 -C2491_bit0 -C2493_bit0 -C2494_bit0 -C2495_bit0 -C2496_bit0 -C2497_bit0 -C2498_bit0 -C2499_bit0 -C2500_bit0 -C2501_bit0 -C2502_bit0 -C2503_bit0 -C2504_bit0 -C2505_bit0 -C2506_bit0 -C2507_bit0 -C2508_bit0 -C2509_bit0 -C2511_bit0 -C2512_bit0 -C2513_bit0 -C2514_bit0 -C2515_bit0 -C2516_bit0 -C2517_bit0 -C2518_bit0 -C2519_bit0 C2520_bit0 C2521_bit0 -C2522_bit0 -C2524_bit0 -C2525_bit0 -C2526_bit0 -C2527_bit0 -C2528_bit0 C2529_bit0 C2530_bit0 -C2531_bit0 -C2532_bit0 -C2533_bit0 -C2534_bit0 -C2535_bit0 -C2536_bit0 C2537_bit0 C2538_bit0 C2539_bit0 -C2540_bit0 -C2542_bit0 -C2543_bit0 -C2544_bit0 -C2545_bit0 C2546_bit0 -C2547_bit0 -C2548_bit0 -C2549_bit0 -C2550_bit0 -C2551_bit0 -C2552_bit0 -C2553_bit0 -C2554_bit0 -C2555_bit0 C2556_bit0 -C2557_bit0 -C2558_bit0 -C2560_bit0 -C2561_bit0 -C2562_bit0 -C2563_bit0 -C2564_bit0 -C2565_bit0 -C2566_bit0 -C2567_bit0 -C2568_bit0 -C2569_bit0 -C2570_bit0 -C2571_bit0 -C2572_bit0 -C2573_bit0 -C2574_bit0 -C2575_bit0 C2576_bit0 -C2578_bit0 -C2579_bit0 C2580_bit0 -C2581_bit0 -C2582_bit0 -C2583_bit0 -C2584_bit0 C2585_bit0 -C2586_bit0 -C2587_bit0 -C2588_bit0 -C2589_bit0 C2591_bit0 C2592_bit0 -C2593_bit0 -C2594_bit0 C2595_bit0 -C2596_bit0 -C2597_bit0 -C2598_bit0 -C2599_bit0 -C2600_bit0 -C2601_bit0 C2602_bit0 -C2603_bit0 -C2604_bit0 -C2605_bit0 -C2606_bit0 -C2607_bit0 -C2609_bit0 C2610_bit0 C2611_bit0 -C2612_bit0 -C2613_bit0 -C2614_bit0 -C2615_bit0 -C2616_bit0 C2617_bit0 -C2618_bit0 -C2619_bit0 -C2620_bit0 -C2623_bit0 -C2624_bit0 C2625_bit0 C2626_bit0 -C2627_bit0 -C2628_bit0 -C2631_bit0 -C2634_bit0 -C2635_bit0 -C2636_bit0 -C2637_bit0 -C2639_bit0 -C2640_bit0 -C2641_bit0 -C2642_bit0 -C2643_bit0 -C2644_bit0 -C2647_bit0 -C2648_bit0 -C2649_bit0 -C2650_bit0 -C2651_bit0 -C2652_bit0 -C2653_bit0 -C2654_bit0 -C2655_bit0 -C2656_bit0 -C2658_bit0 -C2659_bit0 -C2660_bit0 -C2663_bit0 C2664_bit0 -C2665_bit0 -C2666_bit0 -C2667_bit0 -C2668_bit0 -C2669_bit0 -C2670_bit0 -C2671_bit0 -C2672_bit0 C2673_bit0 -C2675_bit0 -C2678_bit0 C2679_bit0 -C2680_bit0 -C2683_bit0 -C2684_bit0 -C2685_bit0 -C2686_bit0 -C2687_bit0 C2688_bit0 -C2690_bit0 -C2692_bit0 -C2694_bit0 -C2695_bit0 -C2696_bit0 -C2699_bit0 -C2700_bit0 C2701_bit0 -C2702_bit0 C2703_bit0 -C2704_bit0 -C2705_bit0 C2708_bit0 C2709_bit0 -C2710_bit0 -C2711_bit0 -C2712_bit0 -C2713_bit0 C2714_bit0 -C2716_bit0 -C2719_bit0 C2720_bit0 -C2721_bit0 -C2722_bit0 -C2723_bit0 -C2724_bit0 -C2725_bit0 -C2726_bit0 -C2727_bit0 -C2728_bit0 -C2729_bit0 -C2732_bit0 -C2733_bit0 -C2734_bit0 -C2735_bit0 -C2736_bit0 -C2737_bit0 -C2738_bit0 -C2739_bit0 -C2740_bit0 -C2741_bit0 -C2742_bit0 -C2743_bit0 -C2744_bit0 -C2745_bit0 -C2748_bit0 C2749_bit0 -C2750_bit0 C2751_bit0 -C2752_bit0 -C2753_bit0 -C2754_bit0 -C2755_bit0 -C2756_bit0 -C2757_bit0 C2758_bit0 -C2760_bit0 -C2763_bit0 C2764_bit0 -C2765_bit0 -C2766_bit0 -C2768_bit0 -C2769_bit0 -C2770_bit0 -C2771_bit0 -C2772_bit0 -C2773_bit0 -C2775_bit0 -C2776_bit0 -C2777_bit0 -C2779_bit0 -C2780_bit0 -C2781_bit0 C2782_bit0 -C2783_bit0 C2784_bit0 -C2785_bit0 -C2786_bit0 -C2787_bit0 -C2788_bit0 -C2789_bit0 -C2790_bit0 -C2793_bit0 C2794_bit0 -C2795_bit0 -C2796_bit0 C2797_bit0 -C2798_bit0 -C2799_bit0 -C2801_bit0 -C2804_bit0 -C2805_bit0 -C2806_bit0 -C2807_bit0 -C2808_bit0 C2809_bit0 C2810_bit0 -C2811_bit0 C2812_bit0 -C2813_bit0 -C2814_bit0 -C2817_bit0 -C2818_bit0 -C2819_bit0 -C2820_bit0 C2821_bit0 -C2822_bit0 -C2823_bit0 -C2824_bit0 -C2825_bit0 -C2826_bit0 -C2827_bit0 -C2828_bit0 -C2829_bit0 -C2830_bit0 -C2833_bit0 C2834_bit0 -C2835_bit0 -C2836_bit0 -C2837_bit0 -C2838_bit0 -C2839_bit0 -C2840_bit0 C2841_bit0 -C2842_bit0 C2843_bit0 -C2845_bit0 -C2848_bit0 -C2849_bit0 -C2850_bit0 C2851_bit0 -C2852_bit0 -C2853_bit0 C2854_bit0 -C2855_bit0 -C2856_bit0 C2857_bit0 -C2858_bit0 C2859_bit0 C2860_bit0 -C2861_bit0 -C2862_bit0 C2864_bit0 -C2865_bit0 C2866_bit0 -C2867_bit0 C2868_bit0 -C2869_bit0 C2870_bit0 -C2871_bit0 -C2872_bit0 -C2873_bit0 -C2874_bit0 -C2875_bit0 -C2878_bit0 C2879_bit0 -C2880_bit0 -C2881_bit0 -C2882_bit0 -C2883_bit0 -C2884_bit0 -C2885_bit0 -C2886_bit0 -C2889_bit0 -C2890_bit0 C2891_bit0 -C2892_bit0 -C2893_bit0 -C2894_bit0 C2895_bit0 -C2896_bit0 -C2897_bit0 -C2898_bit0 C2899_bit0 -C2902_bit0 C2903_bit0 -C2904_bit0 -C2905_bit0 -C2906_bit0 -C2907_bit0 -C2908_bit0 -C2909_bit0 -C2910_bit0 -C2911_bit0 C2912_bit0 -C2913_bit0 -C2914_bit0 -C2915_bit0 -C2918_bit0 -C2919_bit0 -C2920_bit0 -C2921_bit0 -C2922_bit0 -C2923_bit0 -C2924_bit0 -C2925_bit0 -C2926_bit0 -C2927_bit0 C2928_bit0 -C2929_bit0 -C2930_bit0 -C2933_bit0 C2934_bit0 -C2935_bit0 C2936_bit0 C2937_bit0 -C2938_bit0 -C2939_bit0 -C2940_bit0 -C2941_bit0 -C2942_bit0 -C2943_bit0 -C2944_bit0 -C2945_bit0 -C2946_bit0 -C2947_bit0 -C2949_bit0 -C2950_bit0 -C2951_bit0 -C2952_bit0 -C2953_bit0 -C2954_bit0 -C2955_bit0 -C2956_bit0 -C2957_bit0 -C2958_bit0 -C2959_bit0 -C2960_bit0 -C2961_bit0 -C2962_bit0 -C2963_bit0 C2966_bit0 -C2967_bit0 -C2968_bit0 -C2969_bit0 -C2970_bit0 -C2971_bit0 -C2972_bit0 -C2973_bit0 C2974_bit0 C2975_bit0 -C2976_bit0 -C2977_bit0 C2980_bit0 -C2981_bit0 -C2982_bit0 -C2983_bit0 C2984_bit0 -C2985_bit0 C2986_bit0 -C2987_bit0 -C2988_bit0 C2989_bit0 C2990_bit0 C2991_bit0 -C2992_bit0 -C2993_bit0 C2994_bit0 C2995_bit0 -C2996_bit0 -C2997_bit0 -C2998_bit0 -C2999_bit0 -C3000_bit0 C3001_bit0 -C3003_bit0 C3004_bit0 -C3005_bit0 C3006_bit0 C3007_bit0 -C3008_bit0 -C3009_bit0 -C3010_bit0 -C3011_bit0 -C3012_bit0 -C3013_bit0 -C3014_bit0 -C3015_bit0 -C3016_bit0 -C3017_bit0 -C3018_bit0 -C3019_bit0 -C3020_bit0 -C3021_bit0 C3022_bit0 C3023_bit0 -C3024_bit0 -C3025_bit0 C3027_bit0 -C3028_bit0 -C3029_bit0 C3030_bit0 C3031_bit0 -C3032_bit0 -C3033_bit0 -C3034_bit0 -C3035_bit0 -C3038_bit0 -C3040_bit0 -C3041_bit0 -C3042_bit0 -C3043_bit0 -C3045_bit0 -C3046_bit0 -C3047_bit0 -C3048_bit0 -C3049_bit0 C3050_bit0 -C3051_bit0 -C3053_bit0 -C3054_bit0 -C3055_bit0 C3056_bit0 -C3057_bit0 -C3058_bit0 -C3059_bit0 -C3060_bit0 -C3061_bit0 C3062_bit0 -C3064_bit0 -C3066_bit0 -C3067_bit0 C3068_bit0 -C3071_bit0 -C3072_bit0 -C3073_bit0 -C3074_bit0 -C3075_bit0 C3076_bit0 -C3077_bit0 -C3078_bit0 -C3080_bit0 -C3081_bit0 -C3082_bit0 -C3083_bit0 -C3084_bit0 -C3085_bit0 -C3086_bit0 -C3087_bit0 -C3088_bit0 C3089_bit0 C3090_bit0 C3091_bit0 -C3092_bit0 -C3094_bit0 -C3095_bit0 -C3096_bit0 -C3097_bit0 -C3098_bit0 -C3099_bit0 -C3100_bit0 -C3101_bit0 -C3102_bit0 -C3105_bit0 C3107_bit0 -C3108_bit0 -C3109_bit0 -C3110_bit0 -C3112_bit0 C3113_bit0 -C3114_bit0 -C3115_bit0 -C3116_bit0 -C3117_bit0 -C3118_bit0 -C3120_bit0 -C3121_bit0 -C3122_bit0 -C3123_bit0 -C3124_bit0 -C3125_bit0 -C3126_bit0 C3127_bit0 -C3128_bit0 -C3129_bit0 -C3131_bit0 C3133_bit0 C3134_bit0 -C3135_bit0 -C3138_bit0 -C3139_bit0 -C3140_bit0 -C3141_bit0 -C3142_bit0 -C3143_bit0 -C3144_bit0 -C3145_bit0 C3147_bit0 -C3148_bit0 -C3149_bit0 -C3150_bit0 -C3151_bit0 -C3152_bit0 -C3153_bit0 -C3154_bit0 -C3155_bit0 -C3156_bit0 -C3157_bit0 -C3158_bit0 -C3159_bit0 -C3161_bit0 -C3162_bit0 -C3163_bit0 -C3164_bit0 -C3165_bit0 -C3166_bit0 -C3167_bit0 -C3168_bit0 -C3169_bit0 -C3170_bit0 -C3172_bit0 -C3174_bit0 -C3175_bit0 -C3176_bit0 -C3177_bit0 -C3178_bit0 -C3179_bit0 C3180_bit0 -C3181_bit0 -C3182_bit0 -C3183_bit0 -C3184_bit0 -C3185_bit0 -C3187_bit0 -C3188_bit0 -C3189_bit0 -C3190_bit0 -C3191_bit0 -C3192_bit0 -C3193_bit0 -C3194_bit0 -C3195_bit0 C3196_bit0 -C3198_bit0 -C3200_bit0 -C3201_bit0 C3202_bit0 C3203_bit0 -C3204_bit0 -C3205_bit0 C3206_bit0 -C3207_bit0 -C3208_bit0 -C3209_bit0 -C3210_bit0 -C3211_bit0 -C3212_bit0 -C3214_bit0 C3215_bit0 -C3216_bit0 -C3217_bit0 -C3218_bit0 -C3219_bit0 -C3220_bit0 -C3221_bit0 -C3222_bit0 -C3223_bit0 -C3224_bit0 -C3225_bit0 C3226_bit0 -C3228_bit0 -C3229_bit0 -C3230_bit0 -C3231_bit0 -C3232_bit0 -C3233_bit0 -C3234_bit0 -C3235_bit0 -C3236_bit0 -C3237_bit0 -C3239_bit0 -C3241_bit0 -C3242_bit0 -C3243_bit0 -C3244_bit0 -C3245_bit0 -C3246_bit0 C3247_bit0 -C3248_bit0 -C3249_bit0 C3250_bit0 -C3251_bit0 -C3252_bit0 -C3254_bit0 -C3255_bit0 -C3256_bit0 -C3257_bit0 -C3258_bit0 -C3259_bit0 -C3260_bit0 C3261_bit0 -C3262_bit0 C3263_bit0 -C3265_bit0 C3267_bit0 C3268_bit0 C3269_bit0 -C3270_bit0 -C3271_bit0 -C3272_bit0 -C3273_bit0 C3274_bit0 -C3275_bit0 C3276_bit0 C3277_bit0 -C3278_bit0 -C3279_bit0 C3281_bit0 -C3282_bit0 C3283_bit0 C3284_bit0 -C3285_bit0 -C3286_bit0 -C3287_bit0 -C3288_bit0 -C3289_bit0 C3290_bit0 C3291_bit0 -C3292_bit0 -C3293_bit0 C3295_bit0 -C3296_bit0 C3297_bit0 C3298_bit0 C3299_bit0 -C3300_bit0 -C3301_bit0 -C3302_bit0 -C3303_bit0 C3306_bit0 C3308_bit0 -C3309_bit0 -C3310_bit0 -C3311_bit0 -C3313_bit0 C3314_bit0 -C3315_bit0 -C3316_bit0 -C3317_bit0 -C3318_bit0 -C3319_bit0 -C3321_bit0 -C3322_bit0 -C3323_bit0 -C3324_bit0 -C3325_bit0 -C3326_bit0 -C3327_bit0 -C3328_bit0 -C3329_bit0 C3330_bit0 -C3332_bit0 -C3334_bit0 -C3335_bit0 C3336_bit0 C3337_bit0 -C3339_bit0 -C3340_bit0 -C3341_bit0 -C3342_bit0 -C3343_bit0 -C3345_bit0 -C3346_bit0 -C3348_bit0 -C3349_bit0 -C3350_bit0 -C3351_bit0 -C3352_bit0 -C3353_bit0 -C3354_bit0 -C3355_bit0 -C3356_bit0 C3357_bit0 C3358_bit0 -C3359_bit0 -C3360_bit0 -C3362_bit0 -C3363_bit0 -C3364_bit0 -C3365_bit0 -C3366_bit0 -C3367_bit0 -C3368_bit0 C3369_bit0 -C3370_bit0 -C3373_bit0 C3375_bit0 -C3376_bit0 -C3377_bit0 -C3378_bit0 C3380_bit0 -C3381_bit0 -C3382_bit0 -C3383_bit0 -C3384_bit0 -C3385_bit0 -C3386_bit0 C3388_bit0 -C3389_bit0 C3390_bit0 -C3391_bit0 C3392_bit0 -C3393_bit0 C3394_bit0 -C3395_bit0 -C3396_bit0 C3397_bit0 C3399_bit0 -C3401_bit0 -C3402_bit0 -C3403_bit0 -C3404_bit0 -C3406_bit0 -C3407_bit0 -C3408_bit0 -C3409_bit0 -C3410_bit0 -C3411_bit0 -C3412_bit0 -C3413_bit0 -C3415_bit0 -C3416_bit0 -C3417_bit0 -C3418_bit0 -C3419_bit0 -C3420_bit0 -C3421_bit0 -C3422_bit0 -C3423_bit0 -C3424_bit0 -C3425_bit0 -C3426_bit0 -C3427_bit0 -C3428_bit0 -C3429_bit0 -C3430_bit0 -C3432_bit0 -C3433_bit0 -C3434_bit0 C3435_bit0 -C3436_bit0 -C3437_bit0 -C3438_bit0 C3439_bit0 -C3440_bit0 -C3441_bit0 C3442_bit0 -C3443_bit0 -C3444_bit0 -C3445_bit0 -C3446_bit0 -C3448_bit0 -C3449_bit0 -C3450_bit0 C3451_bit0 C3452_bit0 -C3453_bit0 -C3454_bit0 -C3455_bit0 -C3456_bit0 -C3457_bit0 -C3458_bit0 -C3459_bit0 -C3460_bit0 -C3461_bit0 -C3462_bit0 -C3463_bit0 -C3464_bit0 -C3466_bit0 -C3467_bit0 -C3468_bit0 C3469_bit0 -C3470_bit0 -C3471_bit0 -C3472_bit0 C3473_bit0 -C3474_bit0 -C3475_bit0 C3476_bit0 -C3477_bit0 -C3478_bit0 C3479_bit0 -C3480_bit0 -C3481_bit0 -C3483_bit0 -C3484_bit0 C3485_bit0 -C3486_bit0 -C3487_bit0 -C3488_bit0 C3489_bit0 -C3490_bit0 -C3491_bit0 C3492_bit0 -C3493_bit0 -C3494_bit0 -C3495_bit0 C3496_bit0 -C3497_bit0 C3499_bit0 C3500_bit0 C3501_bit0 C3502_bit0 C3503_bit0 -C3504_bit0 -C3505_bit0 -C3506_bit0 -C3507_bit0 -C3508_bit0 -C3509_bit0 -C3510_bit0 -C3511_bit0 -C3512_bit0 -C3513_bit0 -C3514_bit0 -C3515_bit0 -C3517_bit0 -C3518_bit0 -C3519_bit0 -C3520_bit0 -C3521_bit0 -C3522_bit0 -C3523_bit0 -C3524_bit0 -C3526_bit0 -C3527_bit0 -C3528_bit0 -C3529_bit0 -C3530_bit0 -C3531_bit0 -C3532_bit0 -C3534_bit0 -C3535_bit0 -C3536_bit0 -C3537_bit0 -C3538_bit0 C3539_bit0 -C3540_bit0 -C3541_bit0 -C3542_bit0 C3544_bit0 -C3545_bit0 C3546_bit0 C3547_bit0 -C3548_bit0 C3549_bit0 C3550_bit0 C3551_bit0 C3552_bit0 C3553_bit0 C3554_bit0 C3555_bit0 C3556_bit0 C3557_bit0 C3558_bit0 C3559_bit0 C3560_bit0 C3561_bit0 C3562_bit0 C3563_bit0 C3564_bit0 -C3565_bit0 -C3566_bit0 -C3567_bit0 -C1007_bit0 -C1008_bit0 -C1012_bit0 -C1013_bit0 -C1015_bit0 -C1016_bit0 -C1018_bit0 -C1025_bit0 -C1026_bit0 -C1028_bit0 -C1040_bit0 -C1041_bit0 C1043_bit0 -C1052_bit0 -C1053_bit0 -C1055_bit0 -C1063_bit0 C1064_bit0 C1069_bit0 -C1071_bit0 C1072_bit0 -C1081_bit0 -C1082_bit0 -C1084_bit0 -C1096_bit0 C1097_bit0 -C1099_bit0 -C1108_bit0 -C1109_bit0 -C1111_bit0 -C1118_bit0 -C1125_bit0 -C1130_bit0 -C1138_bit0 -C1146_bit0 -C1147_bit0 -C1151_bit0 -C1152_bit0 -C1154_bit0 -C1155_bit0 -C1157_bit0 -C1164_bit0 -C1165_bit0 -C1167_bit0 -C1179_bit0 -C1180_bit0 C1182_bit0 -C1191_bit0 C1192_bit0 C1194_bit0 -C1202_bit0 -C1203_bit0 -C1208_bit0 -C1210_bit0 -C1211_bit0 -C1220_bit0 -C1221_bit0 -C1223_bit0 -C1235_bit0 -C1236_bit0 -C1238_bit0 -C1247_bit0 C1248_bit0 -C1250_bit0 -C1257_bit0 -C1264_bit0 -C1269_bit0 -C1277_bit0 -C1282_bit0 -C1287_bit0 -C1288_bit0 -C1301_bit0 -C1302_bit0 -C1311_bit0 -C1312_bit0 -C1324_bit0 -C1325_bit0 C1334_bit0 C1336_bit0 -C1337_bit0 -C1342_bit0 -C1346_bit0 -C1350_bit0 -C1355_bit0 -C1364_bit0 -C1365_bit0 -C1378_bit0 -C1379_bit0 -C1388_bit0 -C1389_bit0 -C1401_bit0 -C1402_bit0 C1413_bit0 -C1414_bit0 -C1427_bit0 -C1455_bit0 -C1462_bit0 -C1477_bit0 -C1478_bit0 -C1487_bit0 C1488_bit0 -C1504_bit0 -C1505_bit0 -C1518_bit0 -C1520_bit0 -C1521_bit0 -C1534_bit0 -C1547_bit0 -C1548_bit0 C1557_bit0 -C1558_bit0 C1574_bit0 -C1575_bit0 -C1590_bit0 -C1591_bit0 -C1604_bit0 C1632_bit0 -C1649_bit0 -C1654_bit0 -C1655_bit0 -C1664_bit0 -C1665_bit0 -C1681_bit0 -C1682_bit0 -C1695_bit0 C1697_bit0 -C1698_bit0 -C1711_bit0 -C1724_bit0 -C1725_bit0 -C1734_bit0 -C1735_bit0 C1751_bit0 -C1752_bit0 -C1767_bit0 -C1768_bit0 -C1781_bit0 -C1794_bit0 -C1795_bit0 -C1801_bit0 -C1802_bit0 -C1803_bit0 -C1804_bit0 C1805_bit0 -C1806_bit0 C1807_bit0 -C1808_bit0 -C1809_bit0 C1810_bit0 -C1811_bit0 -C1819_bit0 -C1820_bit0 -C1826_bit0 -C1827_bit0 -C1828_bit0 -C1830_bit0 -C1831_bit0 -C1832_bit0 -C1834_bit0 C1835_bit0 C1836_bit0 -C1844_bit0 C1845_bit0 C1852_bit0 -C1853_bit0 -C1855_bit0 -C1857_bit0 -C1858_bit0 -C1859_bit0 -C1861_bit0 -C1862_bit0 -C1863_bit0 -C1866_bit0 -C1868_bit0 -C1869_bit0 -C1874_bit0 -C1881_bit0 -C1894_bit0 -C1895_bit0 -C1901_bit0 C1902_bit0 -C1903_bit0 -C1905_bit0 -C1906_bit0 -C1907_bit0 -C1909_bit0 -C1910_bit0 C1911_bit0 -C1919_bit0 -C1920_bit0 -C1927_bit0 -C1928_bit0 -C1930_bit0 -C1931_bit0 -C1932_bit0 -C1934_bit0 -C1935_bit0 -C1936_bit0 -C1944_bit0 -C1945_bit0 C1953_bit0 -C1957_bit0 C1958_bit0 C1963_bit0 -C1966_bit0 -C1968_bit0 -C1969_bit0 -C1981_bit0 -C1998_bit0 -C1999_bit0 -C2006_bit0 C2007_bit0 -C2009_bit0 -C2010_bit0 -C2015_bit0 -C2027_bit0 -C2028_bit0 C2044_bit0 -C2046_bit0 -C2047_bit0 -C2068_bit0 -C2069_bit0 C2089_bit0 -C2090_bit0 C2104_bit0 -C2105_bit0 -C2125_bit0 -C2142_bit0 C2143_bit0 -C2150_bit0 -C2151_bit0 -C2153_bit0 -C2154_bit0 -C2159_bit0 -C2171_bit0 -C2172_bit0 -C2188_bit0 -C2190_bit0 -C2191_bit0 -C2212_bit0 -C2213_bit0 -C2233_bit0 -C2234_bit0 -C2248_bit0 -C2249_bit0 C2269_bit0 C2347_bit0 -C2350_bit0 -C2368_bit0 C2383_bit0 -C2385_bit0 -C2388_bit0 -C2389_bit0 -C2390#### 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.58 0.80 0.86 2/54 30319
Raw data (stat): 30319 (runsolver) R 30318 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490550964 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.64 0.81 0.86 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 5057 0 0 0 985 14 0 0 25 0 1 0 490550964 23248896 4873 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5676 4873 603 41 0 5635 0
vsize: 22704
[startup+20.0002 s]
Raw data (loadavg): 0.70 0.81 0.86 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 5365 0 0 0 1984 15 0 0 25 0 1 0 490550964 24518656 5181 4294967295 134512640 134672761 3221224544 3221223712 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5986 5181 603 41 0 5945 0
vsize: 23944
[startup+29.9998 s]
Raw data (loadavg): 0.74 0.82 0.86 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 6149 0 0 0 2981 18 0 0 25 0 1 0 490550964 27877376 5965 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6806 5965 603 41 0 6765 0
vsize: 27224
[startup+39.9999 s]
Raw data (loadavg): 0.78 0.82 0.86 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 6552 0 0 0 3979 20 0 0 25 0 1 0 490550964 29491200 6368 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7200 6368 603 41 0 7159 0
vsize: 28800
[startup+50.0007 s]
Raw data (loadavg): 0.81 0.83 0.86 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 6982 0 0 0 4978 21 0 0 25 0 1 0 490550964 31367168 6798 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7658 6798 603 41 0 7617 0
vsize: 30632
[startup+59.9998 s]
Raw data (loadavg): 0.84 0.83 0.86 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 7289 0 0 0 5977 22 0 0 25 0 1 0 490550964 32575488 7105 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7953 7105 603 41 0 7912 0
vsize: 31812
[startup+70.001 s]
Raw data (loadavg): 0.87 0.84 0.86 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 7614 0 0 0 6977 23 0 0 25 0 1 0 490550964 33923072 7430 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8282 7430 603 41 0 8241 0
vsize: 33128
[startup+80.0014 s]
Raw data (loadavg): 0.89 0.84 0.86 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 8163 0 0 0 7975 25 0 0 25 0 1 0 490550964 36069376 7979 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8806 7979 603 41 0 8765 0
vsize: 35224
[startup+90.0018 s]
Raw data (loadavg): 0.90 0.85 0.87 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 8576 0 0 0 8973 27 0 0 25 0 1 0 490550964 37810176 8392 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9231 8392 603 41 0 9190 0
vsize: 36924
[startup+100.002 s]
Raw data (loadavg): 0.92 0.85 0.87 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 9049 0 0 0 9972 28 0 0 25 0 1 0 490550964 39698432 8865 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9692 8865 603 41 0 9651 0
vsize: 38768
[startup+110.001 s]
Raw data (loadavg): 0.93 0.86 0.87 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 9281 0 0 0 10972 28 0 0 25 0 1 0 490550964 40640512 9097 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9922 9097 603 41 0 9881 0
vsize: 39688
[startup+120.001 s]
Raw data (loadavg): 0.94 0.86 0.87 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 9546 0 0 0 11971 30 0 0 25 0 1 0 490550964 42106880 9362 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10280 9362 603 41 0 10239 0
vsize: 41120
[startup+130.001 s]
Raw data (loadavg): 0.95 0.86 0.87 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 9883 0 0 0 12970 30 0 0 25 0 1 0 490550964 43454464 9699 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10609 9699 603 41 0 10568 0
vsize: 42436
[startup+140.002 s]
Raw data (loadavg): 0.96 0.87 0.87 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 10267 0 0 0 13970 31 0 0 25 0 1 0 490550964 45072384 10083 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11004 10083 603 41 0 10963 0
vsize: 44016
[startup+150.002 s]
Raw data (loadavg): 0.96 0.87 0.87 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 10953 0 0 0 14968 33 0 0 25 0 1 0 490550964 47902720 10769 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11695 10769 603 41 0 11654 0
vsize: 46780
[startup+160.002 s]
Raw data (loadavg): 0.97 0.88 0.87 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 11687 0 0 0 15966 36 0 0 25 0 1 0 490550964 50839552 11503 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12412 11503 603 41 0 12371 0
vsize: 49648
[startup+170.002 s]
Raw data (loadavg): 0.97 0.88 0.87 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 12475 0 0 0 16964 38 0 0 25 0 1 0 490550964 54046720 12291 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13195 12291 603 41 0 13154 0
vsize: 52780
[startup+180.002 s]
Raw data (loadavg): 0.98 0.88 0.87 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 13089 0 0 0 17963 39 0 0 25 0 1 0 490550964 56602624 12905 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13819 12905 603 41 0 13778 0
vsize: 55276
[startup+190.003 s]
Raw data (loadavg): 0.98 0.89 0.87 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 13707 0 0 0 18961 41 0 0 25 0 1 0 490550964 59158528 13523 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14443 13523 603 41 0 14402 0
vsize: 57772
[startup+200.004 s]
Raw data (loadavg): 0.98 0.89 0.88 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 14333 0 0 0 19960 42 0 0 25 0 1 0 490550964 61698048 14149 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15063 14149 603 41 0 15022 0
vsize: 60252
[startup+210.003 s]
Raw data (loadavg): 0.98 0.89 0.88 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 14836 0 0 0 20959 43 0 0 25 0 1 0 490550964 63721472 14652 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15557 14652 603 41 0 15516 0
vsize: 62228
[startup+220.003 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 15072 0 0 0 21959 44 0 0 25 0 1 0 490550964 64667648 14888 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15788 14888 603 41 0 15747 0
vsize: 63152
[startup+230.003 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 15395 0 0 0 22959 44 0 0 25 0 1 0 490550964 66007040 15211 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16115 15211 603 41 0 16074 0
vsize: 64460
[startup+240.004 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 15587 0 0 0 23958 45 0 0 25 0 1 0 490550964 66682880 15403 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16280 15403 603 41 0 16239 0
vsize: 65120
[startup+250.004 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 15822 0 0 0 24957 46 0 0 25 0 1 0 490550964 67760128 15638 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16543 15638 603 41 0 16502 0
vsize: 66172
[startup+260.004 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 16006 0 0 0 25957 46 0 0 25 0 1 0 490550964 68435968 15822 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16708 15822 603 41 0 16667 0
vsize: 66832
[startup+270.005 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 16148 0 0 0 26957 47 0 0 25 0 1 0 490550964 68976640 15964 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16840 15964 603 41 0 16799 0
vsize: 67360
[startup+280.005 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 16321 0 0 0 27956 48 0 0 25 0 1 0 490550964 69652480 16137 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17005 16137 603 41 0 16964 0
vsize: 68020
[startup+290.005 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 16491 0 0 0 28956 48 0 0 25 0 1 0 490550964 70324224 16307 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17169 16307 603 41 0 17128 0
vsize: 68676
[startup+300.005 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 16663 0 0 0 29955 50 0 0 25 0 1 0 490550964 70995968 16479 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17333 16479 603 41 0 17292 0
vsize: 69332
[startup+310.005 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 16829 0 0 0 30954 50 0 0 25 0 1 0 490550964 71663616 16645 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17496 16645 603 41 0 17455 0
vsize: 69984
[startup+320.005 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 17014 0 0 0 31954 51 0 0 25 0 1 0 490550964 72470528 16830 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17693 16830 603 41 0 17652 0
vsize: 70772
[startup+330.006 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 17234 0 0 0 32953 52 0 0 25 0 1 0 490550964 73277440 17050 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17890 17050 603 41 0 17849 0
vsize: 71560
[startup+340.007 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 17397 0 0 0 33952 53 0 0 25 0 1 0 490550964 73945088 17213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18053 17213 603 41 0 18012 0
vsize: 72212
[startup+350.007 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 17739 0 0 0 34951 54 0 0 25 0 1 0 490550964 75292672 17555 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18382 17555 603 41 0 18341 0
vsize: 73528
[startup+360.007 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 18361 0 0 0 35949 57 0 0 25 0 1 0 490550964 78888960 18177 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19260 18177 603 41 0 19219 0
vsize: 77040
[startup+370.007 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 19052 0 0 0 36946 59 0 0 25 0 1 0 490550964 81702912 18868 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19947 18868 603 41 0 19906 0
vsize: 79788
[startup+380.007 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 19695 0 0 0 37944 62 0 0 25 0 1 0 490550964 84262912 19511 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20572 19511 603 41 0 20531 0
vsize: 82288
[startup+390.007 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 20230 0 0 0 38943 63 0 0 25 0 1 0 490550964 86417408 20046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21098 20046 603 41 0 21057 0
vsize: 84392
[startup+400.008 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 20688 0 0 0 39942 64 0 0 25 0 1 0 490550964 88297472 20504 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21557 20504 603 41 0 21516 0
vsize: 86228
[startup+410.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 20965 0 0 0 40941 65 0 0 25 0 1 0 490550964 89505792 20781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21852 20781 603 41 0 21811 0
vsize: 87408
[startup+420.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 21243 0 0 0 41941 65 0 0 25 0 1 0 490550964 90583040 21059 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22115 21059 603 41 0 22074 0
vsize: 88460
[startup+430.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 21421 0 0 0 42940 67 0 0 25 0 1 0 490550964 91258880 21237 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22280 21237 603 41 0 22239 0
vsize: 89120
[startup+440.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 21713 0 0 0 43939 67 0 0 25 0 1 0 490550964 92471296 21529 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22576 21529 603 41 0 22535 0
vsize: 90304
[startup+450.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23035 0 0 0 44936 70 0 0 25 0 1 0 490550964 98050048 22851 4294967295 134512640 134672761 3221224544 3221223844 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22851 603 41 0 23897 0
vsize: 95752
[startup+460.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23035 0 0 0 45937 70 0 0 25 0 1 0 490550964 98050048 22851 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22851 603 41 0 23897 0
vsize: 95752
[startup+470.007 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23035 0 0 0 46937 70 0 0 25 0 1 0 490550964 98050048 22851 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22851 603 41 0 23897 0
vsize: 95752
[startup+480.007 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23036 0 0 0 47937 70 0 0 25 0 1 0 490550964 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+490.008 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23036 0 0 0 48937 70 0 0 25 0 1 0 490550964 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+500.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23036 0 0 0 49937 70 0 0 25 0 1 0 490550964 98050048 22852 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+510.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23036 0 0 0 50938 70 0 0 25 0 1 0 490550964 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+520.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23036 0 0 0 51938 70 0 0 25 0 1 0 490550964 98050048 22852 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+530.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23036 0 0 0 52938 70 0 0 25 0 1 0 490550964 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+540.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23036 0 0 0 53938 70 0 0 25 0 1 0 490550964 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+550.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23037 0 0 0 54938 70 0 0 25 0 1 0 490550964 98050048 22853 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22853 603 41 0 23897 0
vsize: 95752
[startup+560.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23038 0 0 0 55938 70 0 0 25 0 1 0 490550964 98050048 22854 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22854 603 41 0 23897 0
vsize: 95752
[startup+570.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23038 0 0 0 56939 70 0 0 25 0 1 0 490550964 98050048 22854 4294967295 134512640 134672761 3221224544 3221223712 134564668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22854 603 41 0 23897 0
vsize: 95752
[startup+580.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23038 0 0 0 57939 70 0 0 25 0 1 0 490550964 98050048 22854 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22854 603 41 0 23897 0
vsize: 95752
[startup+590.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23038 0 0 0 58939 70 0 0 25 0 1 0 490550964 98050048 22854 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22854 603 41 0 23897 0
vsize: 95752
[startup+600.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23042 0 0 0 59939 70 0 0 25 0 1 0 490550964 98050048 22858 4294967295 134512640 134672761 3221224544 3221223728 134559660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+610.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23042 0 0 0 60939 70 0 0 25 0 1 0 490550964 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+620.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23042 0 0 0 61939 70 0 0 25 0 1 0 490550964 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+630.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23042 0 0 0 62940 70 0 0 25 0 1 0 490550964 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+640.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23042 0 0 0 63940 70 0 0 25 0 1 0 490550964 98050048 22858 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+650.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23042 0 0 0 64940 70 0 0 25 0 1 0 490550964 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+660.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23042 0 0 0 65940 70 0 0 25 0 1 0 490550964 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23045 0 0 0 66941 70 0 0 25 0 1 0 490550964 98050048 22861 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22861 603 41 0 23897 0
vsize: 95752
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23045 0 0 0 67941 71 0 0 25 0 1 0 490550964 98050048 22861 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22861 603 41 0 23897 0
vsize: 95752
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23046 0 0 0 68940 71 0 0 25 0 1 0 490550964 98050048 22862 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22862 603 41 0 23897 0
vsize: 95752
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23046 0 0 0 69940 71 0 0 25 0 1 0 490550964 98050048 22862 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22862 603 41 0 23897 0
vsize: 95752
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23047 0 0 0 70941 71 0 0 25 0 1 0 490550964 98050048 22863 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22863 603 41 0 23897 0
vsize: 95752
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 71941 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 72941 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 73941 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 74942 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 75942 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 76942 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 77942 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 78942 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 79943 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 80943 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560819 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+820.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 81943 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+830.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 82943 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+840.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 83944 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+850.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23048 0 0 0 84944 71 0 0 25 0 1 0 490550964 98050048 22864 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+860.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23050 0 0 0 85944 71 0 0 25 0 1 0 490550964 98050048 22866 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22866 603 41 0 23897 0
vsize: 95752
[startup+870.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23054 0 0 0 86943 71 0 0 25 0 1 0 490550964 98050048 22870 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22870 603 41 0 23897 0
vsize: 95752
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23057 0 0 0 87943 71 0 0 25 0 1 0 490550964 98050048 22873 4294967295 134512640 134672761 3221224544 3221223680 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22873 603 41 0 23897 0
vsize: 95752
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23061 0 0 0 88944 71 0 0 25 0 1 0 490550964 98050048 22877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22877 603 41 0 23897 0
vsize: 95752
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23064 0 0 0 89944 71 0 0 25 0 1 0 490550964 98050048 22880 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22880 603 41 0 23897 0
vsize: 95752
[startup+910.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23068 0 0 0 90944 71 0 0 25 0 1 0 490550964 98050048 22884 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22884 603 41 0 23897 0
vsize: 95752
[startup+920.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23071 0 0 0 91944 71 0 0 25 0 1 0 490550964 98050048 22887 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22887 603 41 0 23897 0
vsize: 95752
[startup+930.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23074 0 0 0 92944 71 0 0 25 0 1 0 490550964 98050048 22890 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22890 603 41 0 23897 0
vsize: 95752
[startup+940.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23078 0 0 0 93945 71 0 0 25 0 1 0 490550964 98050048 22894 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22894 603 41 0 23897 0
vsize: 95752
[startup+950.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23081 0 0 0 94945 71 0 0 25 0 1 0 490550964 98050048 22897 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22897 603 41 0 23897 0
vsize: 95752
[startup+960.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23084 0 0 0 95945 71 0 0 25 0 1 0 490550964 98050048 22900 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22900 603 41 0 23897 0
vsize: 95752
[startup+970.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23086 0 0 0 96945 71 0 0 25 0 1 0 490550964 98050048 22902 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22902 603 41 0 23897 0
vsize: 95752
[startup+980.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23089 0 0 0 97945 71 0 0 25 0 1 0 490550964 98050048 22905 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22905 603 41 0 23897 0
vsize: 95752
[startup+990.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23092 0 0 0 98946 71 0 0 25 0 1 0 490550964 98050048 22908 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22908 603 41 0 23897 0
vsize: 95752
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23095 0 0 0 99946 71 0 0 25 0 1 0 490550964 98050048 22911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22911 603 41 0 23897 0
vsize: 95752
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23099 0 0 0 100946 71 0 0 25 0 1 0 490550964 98050048 22915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22915 603 41 0 23897 0
vsize: 95752
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23102 0 0 0 101946 71 0 0 25 0 1 0 490550964 98050048 22918 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22918 603 41 0 23897 0
vsize: 95752
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30319
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23105 0 0 0 102946 71 0 0 25 0 1 0 490550964 98050048 22921 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22921 603 41 0 23897 0
vsize: 95752
[startup+1040.02 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 30372
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23108 0 0 0 103946 72 0 0 25 0 1 0 490550964 98050048 22924 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22924 603 41 0 23897 0
vsize: 95752
[startup+1050.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 30372
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23111 0 0 0 104945 72 0 0 25 0 1 0 490550964 98050048 22927 4294967295 134512640 134672761 3221224544 3221223668 134566115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22927 603 41 0 23897 0
vsize: 95752
[startup+1060.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 30372
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23115 0 0 0 105945 72 0 0 25 0 1 0 490550964 98050048 22931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22931 603 41 0 23897 0
vsize: 95752
[startup+1070.02 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 30372
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23118 0 0 0 106945 73 0 0 25 0 1 0 490550964 98050048 22934 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22934 603 41 0 23897 0
vsize: 95752
[startup+1080.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 30372
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23126 0 0 0 107945 73 0 0 25 0 1 0 490550964 98050048 22942 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22942 603 41 0 23897 0
vsize: 95752
[startup+1090.12 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 30372
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23133 0 0 0 108956 73 0 0 25 0 1 0 490550964 98050048 22949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22949 603 41 0 23897 0
vsize: 95752
[startup+1100.12 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 30374
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23136 0 0 0 109956 73 0 0 25 0 1 0 490550964 98050048 22952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22952 603 41 0 23897 0
vsize: 95752
[startup+1110.12 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 30374
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23138 0 0 0 110956 73 0 0 25 0 1 0 490550964 98050048 22954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22954 603 41 0 23897 0
vsize: 95752
[startup+1120.12 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 30374
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23142 0 0 0 111956 74 0 0 25 0 1 0 490550964 98050048 22958 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22958 603 41 0 23897 0
vsize: 95752
[startup+1130.12 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30374
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23145 0 0 0 112955 74 0 0 25 0 1 0 490550964 98050048 22961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22961 603 41 0 23897 0
vsize: 95752
[startup+1140.12 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30374
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23148 0 0 0 113955 74 0 0 25 0 1 0 490550964 98050048 22964 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22964 603 41 0 23897 0
vsize: 95752
[startup+1150.12 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30374
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23151 0 0 0 114955 75 0 0 25 0 1 0 490550964 98050048 22967 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22967 603 41 0 23897 0
vsize: 95752
[startup+1160.12 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 30374
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23154 0 0 0 115955 75 0 0 25 0 1 0 490550964 98050048 22970 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22970 603 41 0 23897 0
vsize: 95752
[startup+1170.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30374
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23157 0 0 0 116955 75 0 0 25 0 1 0 490550964 98050048 22973 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22973 603 41 0 23897 0
vsize: 95752
[startup+1180.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30374
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23161 0 0 0 117955 76 0 0 25 0 1 0 490550964 98050048 22977 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22977 603 41 0 23897 0
vsize: 95752
[startup+1190.13 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30374
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23164 0 0 0 118955 76 0 0 25 0 1 0 490550964 98050048 22980 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22980 603 41 0 23897 0
vsize: 95752
[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 30374
Raw data (stat): 30319 (minisat+) R 30318 30701 30700 0 -1 0 23166 0 0 0 119954 77 0 0 25 0 1 0 490550964 98050048 22982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22982 603 41 0 23897 0
vsize: 95752
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 30374
Raw data (stat): 30319 (minisat+) Z 30318 30701 30700 0 -1 12 23169 0 0 0 119955 81 0 0 25 0 1 0 490550964 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.18
CPU time (s): 1200.37
CPU user time (s): 1199.55
CPU system time (s): 0.815875
CPU usage (%): 100.016
Max. virtual memory (Kb): 95752
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####