PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-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 18193

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        301840 kB
Buffers:         35180 kB
Cached:         667168 kB
SwapCached:         24 kB
Active:         193644 kB
Inactive:       511452 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        301588 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            22140 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:12:23 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 18743 7 1200.21 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.91 0.95 0.95 2/54 3014
Raw data (stat): 3014 (runsolver) R 3013 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545582919 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.0006 s]
Raw data (loadavg): 0.93 0.95 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 5055 0 0 0 984 14 0 0 25 0 1 0 545582919 23248896 4871 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5676 4871 603 41 0 5635 0
vsize: 22704
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.96 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 5363 0 0 0 1982 15 0 0 25 0 1 0 545582919 24518656 5179 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5986 5179 603 41 0 5945 0
vsize: 23944
[startup+30.0019 s]
Raw data (loadavg): 0.95 0.96 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 6149 0 0 0 2981 17 0 0 25 0 1 0 545582919 27877376 5965 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6806 5965 603 41 0 6765 0
vsize: 27224
[startup+40.0021 s]
Raw data (loadavg): 0.95 0.96 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 6547 0 0 0 3979 18 0 0 25 0 1 0 545582919 29356032 6363 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7167 6363 603 41 0 7126 0
vsize: 28668
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.96 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 6981 0 0 0 4977 21 0 0 25 0 1 0 545582919 31367168 6797 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7658 6797 603 41 0 7617 0
vsize: 30632
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.96 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 7294 0 0 0 5975 22 0 0 25 0 1 0 545582919 32710656 7110 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7986 7110 603 41 0 7945 0
vsize: 31944
[startup+70.0019 s]
Raw data (loadavg): 0.97 0.96 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 7616 0 0 0 6974 23 0 0 25 0 1 0 545582919 33923072 7432 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8282 7432 603 41 0 8241 0
vsize: 33128
[startup+80.0024 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 8174 0 0 0 7973 25 0 0 25 0 1 0 545582919 36204544 7990 4294967295 134512640 134672761 3221224544 3221223680 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8839 7990 603 41 0 8798 0
vsize: 35356
[startup+90.002 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 8595 0 0 0 8972 26 0 0 25 0 1 0 545582919 37810176 8411 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9231 8411 603 41 0 9190 0
vsize: 36924
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 9062 0 0 0 9971 28 0 0 25 0 1 0 545582919 39698432 8878 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9692 8878 603 41 0 9651 0
vsize: 38768
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 9296 0 0 0 10970 28 0 0 25 0 1 0 545582919 40640512 9112 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9922 9112 603 41 0 9881 0
vsize: 39688
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 9576 0 0 0 11969 29 0 0 25 0 1 0 545582919 42242048 9392 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10313 9392 603 41 0 10272 0
vsize: 41252
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 9905 0 0 0 12969 30 0 0 25 0 1 0 545582919 43589632 9721 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10642 9721 603 41 0 10601 0
vsize: 42568
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 10327 0 0 0 13967 32 0 0 25 0 1 0 545582919 45342720 10143 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11070 10143 603 41 0 11029 0
vsize: 44280
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 11026 0 0 0 14966 34 0 0 25 0 1 0 545582919 48173056 10842 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11761 10842 603 41 0 11720 0
vsize: 47044
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 11789 0 0 0 15964 36 0 0 25 0 1 0 545582919 51240960 11605 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12510 11605 603 41 0 12469 0
vsize: 50040
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 12587 0 0 0 16962 38 0 0 25 0 1 0 545582919 54579200 12403 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13325 12403 603 41 0 13284 0
vsize: 53300
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 13187 0 0 0 17961 39 0 0 25 0 1 0 545582919 57004032 13003 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13917 13003 603 41 0 13876 0
vsize: 55668
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 13815 0 0 0 18958 42 0 0 25 0 1 0 545582919 59559936 13631 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14541 13631 603 41 0 14500 0
vsize: 58164
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 14465 0 0 0 19956 44 0 0 25 0 1 0 545582919 62234624 14281 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15194 14281 603 41 0 15153 0
vsize: 60776
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 14885 0 0 0 20955 45 0 0 25 0 1 0 545582919 63991808 14701 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15623 14701 603 41 0 15582 0
vsize: 62492
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 15139 0 0 0 21954 46 0 0 25 0 1 0 545582919 64933888 14955 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15853 14955 603 41 0 15812 0
vsize: 63412
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 15434 0 0 0 22954 47 0 0 25 0 1 0 545582919 66142208 15250 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16148 15250 603 41 0 16107 0
vsize: 64592
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 15630 0 0 0 23953 48 0 0 25 0 1 0 545582919 66953216 15446 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16346 15446 603 41 0 16305 0
vsize: 65384
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 15851 0 0 0 24952 48 0 0 25 0 1 0 545582919 67760128 15667 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16543 15667 603 41 0 16502 0
vsize: 66172
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 16034 0 0 0 25951 49 0 0 25 0 1 0 545582919 68571136 15850 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16741 15850 603 41 0 16700 0
vsize: 66964
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 16207 0 0 0 26950 50 0 0 25 0 1 0 545582919 69246976 16023 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16906 16023 603 41 0 16865 0
vsize: 67624
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 16366 0 0 0 27950 50 0 0 25 0 1 0 545582919 69918720 16182 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17070 16182 603 41 0 17029 0
vsize: 68280
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 16537 0 0 0 28949 51 0 0 25 0 1 0 545582919 70594560 16353 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17235 16353 603 41 0 17194 0
vsize: 68940
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 16703 0 0 0 29949 51 0 0 25 0 1 0 545582919 71262208 16519 4294967295 134512640 134672761 3221224544 3221223728 134559327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17398 16519 603 41 0 17357 0
vsize: 69592
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 16877 0 0 0 30949 52 0 0 25 0 1 0 545582919 71929856 16693 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17561 16693 603 41 0 17520 0
vsize: 70244
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 17068 0 0 0 31948 53 0 0 25 0 1 0 545582919 72605696 16884 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17726 16884 603 41 0 17685 0
vsize: 70904
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 17289 0 0 0 32947 54 0 0 25 0 1 0 545582919 73543680 17105 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17955 17105 603 41 0 17914 0
vsize: 71820
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 17518 0 0 0 33947 54 0 0 25 0 1 0 545582919 74485760 17334 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18185 17334 603 41 0 18144 0
vsize: 72740
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 17828 0 0 0 34946 55 0 0 25 0 1 0 545582919 76746752 17644 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18737 17644 603 41 0 18696 0
vsize: 74948
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 18608 0 0 0 35944 57 0 0 25 0 1 0 545582919 79826944 18424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19489 18424 603 41 0 19448 0
vsize: 77956
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 19300 0 0 0 36942 59 0 0 25 0 1 0 545582919 82640896 19116 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20176 19116 603 41 0 20135 0
vsize: 80704
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 19912 0 0 0 37941 61 0 0 25 0 1 0 545582919 85209088 19728 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20803 19728 603 41 0 20762 0
vsize: 83212
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 20479 0 0 0 38938 64 0 0 25 0 1 0 545582919 87490560 20295 4294967295 134512640 134672761 3221224544 3221223728 134559482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21360 20295 603 41 0 21319 0
vsize: 85440
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 20777 0 0 0 39937 65 0 0 25 0 1 0 545582919 88707072 20593 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21657 20593 603 41 0 21616 0
vsize: 86628
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 21102 0 0 0 40937 66 0 0 25 0 1 0 545582919 90042368 20918 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21983 20918 603 41 0 21942 0
vsize: 87932
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 21312 0 0 0 41936 67 0 0 25 0 1 0 545582919 90853376 21128 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22181 21128 603 41 0 22140 0
vsize: 88724
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 21550 0 0 0 42934 68 0 0 25 0 1 0 545582919 91795456 21366 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22411 21366 603 41 0 22370 0
vsize: 89644
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 21775 0 0 0 43933 68 0 0 25 0 1 0 545582919 92741632 21591 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22642 21591 603 41 0 22601 0
vsize: 90568
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23035 0 0 0 44930 72 0 0 25 0 1 0 545582919 98050048 22851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22851 603 41 0 23897 0
vsize: 95752
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 3014
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23035 0 0 0 45930 72 0 0 25 0 1 0 545582919 98050048 22851 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22851 603 41 0 23897 0
vsize: 95752
[startup+470.004 s]
Raw data (loadavg): 1.07 0.99 0.96 2/54 3067
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23035 0 0 0 46930 72 0 0 25 0 1 0 545582919 98050048 22851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22851 603 41 0 23897 0
vsize: 95752
[startup+480.005 s]
Raw data (loadavg): 1.06 0.99 0.96 2/54 3067
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23036 0 0 0 47930 72 0 0 25 0 1 0 545582919 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+490.005 s]
Raw data (loadavg): 1.05 0.99 0.96 2/54 3067
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23036 0 0 0 48930 72 0 0 25 0 1 0 545582919 98050048 22852 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+500.004 s]
Raw data (loadavg): 1.04 0.99 0.96 2/54 3067
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23036 0 0 0 49930 72 0 0 25 0 1 0 545582919 98050048 22852 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+510.005 s]
Raw data (loadavg): 1.04 0.99 0.96 2/54 3067
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23036 0 0 0 50930 72 0 0 25 0 1 0 545582919 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+520.005 s]
Raw data (loadavg): 1.03 0.99 0.96 2/54 3067
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23036 0 0 0 51931 72 0 0 25 0 1 0 545582919 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+530.005 s]
Raw data (loadavg): 1.03 0.99 0.96 2/54 3067
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23036 0 0 0 52931 72 0 0 25 0 1 0 545582919 98050048 22852 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+540.005 s]
Raw data (loadavg): 1.02 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23037 0 0 0 53931 72 0 0 25 0 1 0 545582919 98050048 22853 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22853 603 41 0 23897 0
vsize: 95752
[startup+550.012 s]
Raw data (loadavg): 1.02 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23037 0 0 0 54931 72 0 0 25 0 1 0 545582919 98050048 22853 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22853 603 41 0 23897 0
vsize: 95752
[startup+560.012 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23038 0 0 0 55932 72 0 0 25 0 1 0 545582919 98050048 22854 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22854 603 41 0 23897 0
vsize: 95752
[startup+570.012 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23038 0 0 0 56932 72 0 0 25 0 1 0 545582919 98050048 22854 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22854 603 41 0 23897 0
vsize: 95752
[startup+580.013 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23038 0 0 0 57932 72 0 0 25 0 1 0 545582919 98050048 22854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22854 603 41 0 23897 0
vsize: 95752
[startup+590.013 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23042 0 0 0 58932 73 0 0 25 0 1 0 545582919 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+600.013 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23042 0 0 0 59932 73 0 0 25 0 1 0 545582919 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+610.013 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23042 0 0 0 60932 73 0 0 25 0 1 0 545582919 98050048 22858 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+620.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23042 0 0 0 61932 73 0 0 25 0 1 0 545582919 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+630.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23042 0 0 0 62933 73 0 0 25 0 1 0 545582919 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+640.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23042 0 0 0 63933 73 0 0 25 0 1 0 545582919 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+650.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23042 0 0 0 64932 74 0 0 25 0 1 0 545582919 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+660.014 s]
Raw data (loadavg): 1.00 0.99 0.96 3/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23044 0 0 0 65932 74 0 0 25 0 1 0 545582919 98050048 22860 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22860 603 41 0 23897 0
vsize: 95752
[startup+670.014 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23045 0 0 0 66932 74 0 0 25 0 1 0 545582919 98050048 22861 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22861 603 41 0 23897 0
vsize: 95752
[startup+680.015 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23045 0 0 0 67932 74 0 0 25 0 1 0 545582919 98050048 22861 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.015 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23046 0 0 0 68932 74 0 0 25 0 1 0 545582919 98050048 22862 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22862 603 41 0 23897 0
vsize: 95752
[startup+700.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23047 0 0 0 69932 74 0 0 25 0 1 0 545582919 98050048 22863 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22863 603 41 0 23897 0
vsize: 95752
[startup+710.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 70933 75 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+720.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 71933 75 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+730.017 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 72933 75 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+740.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 73933 75 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+750.016 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 74933 75 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+760.017 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 75933 75 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+770.017 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 76933 75 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+780.018 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 77934 75 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+790.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 78934 75 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223728 134559351 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+800.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 79934 75 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+810.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 80934 75 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+820.019 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3069
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 81934 75 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+830.02 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 82934 76 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+840.02 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23048 0 0 0 83934 76 0 0 25 0 1 0 545582919 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+850.02 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23050 0 0 0 84934 76 0 0 25 0 1 0 545582919 98050048 22866 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22866 603 41 0 23897 0
vsize: 95752
[startup+860.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23053 0 0 0 85934 76 0 0 25 0 1 0 545582919 98050048 22869 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22869 603 41 0 23897 0
vsize: 95752
[startup+870.02 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23056 0 0 0 86934 76 0 0 25 0 1 0 545582919 98050048 22872 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22872 603 41 0 23897 0
vsize: 95752
[startup+880.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23060 0 0 0 87934 76 0 0 25 0 1 0 545582919 98050048 22876 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22876 603 41 0 23897 0
vsize: 95752
[startup+890.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23064 0 0 0 88933 76 0 0 25 0 1 0 545582919 98050048 22880 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22880 603 41 0 23897 0
vsize: 95752
[startup+900.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23067 0 0 0 89933 76 0 0 25 0 1 0 545582919 98050048 22883 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22883 603 41 0 23897 0
vsize: 95752
[startup+910.023 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23070 0 0 0 90933 76 0 0 25 0 1 0 545582919 98050048 22886 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22886 603 41 0 23897 0
vsize: 95752
[startup+920.023 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23074 0 0 0 91933 77 0 0 25 0 1 0 545582919 98050048 22890 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22890 603 41 0 23897 0
vsize: 95752
[startup+930.025 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23078 0 0 0 92933 77 0 0 25 0 1 0 545582919 98050048 22894 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22894 603 41 0 23897 0
vsize: 95752
[startup+940.025 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23081 0 0 0 93933 77 0 0 25 0 1 0 545582919 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+950.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23084 0 0 0 94934 77 0 0 25 0 1 0 545582919 98050048 22900 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22900 603 41 0 23897 0
vsize: 95752
[startup+960.035 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23086 0 0 0 95934 78 0 0 25 0 1 0 545582919 98050048 22902 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22902 603 41 0 23897 0
vsize: 95752
[startup+970.035 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23088 0 0 0 96934 78 0 0 25 0 1 0 545582919 98050048 22904 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22904 603 41 0 23897 0
vsize: 95752
[startup+980.036 s]
Raw data (loadavg): 1.07 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23091 0 0 0 97933 78 0 0 25 0 1 0 545582919 98050048 22907 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22907 603 41 0 23897 0
vsize: 95752
[startup+990.036 s]
Raw data (loadavg): 1.06 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23094 0 0 0 98933 78 0 0 25 0 1 0 545582919 98050048 22910 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22910 603 41 0 23897 0
vsize: 95752
[startup+1000.04 s]
Raw data (loadavg): 1.05 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23098 0 0 0 99934 78 0 0 25 0 1 0 545582919 98050048 22914 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22914 603 41 0 23897 0
vsize: 95752
[startup+1010.04 s]
Raw data (loadavg): 1.04 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23101 0 0 0 100934 78 0 0 25 0 1 0 545582919 98050048 22917 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22917 603 41 0 23897 0
vsize: 95752
[startup+1020.04 s]
Raw data (loadavg): 1.04 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23105 0 0 0 101934 79 0 0 25 0 1 0 545582919 98050048 22921 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22921 603 41 0 23897 0
vsize: 95752
[startup+1030.04 s]
Raw data (loadavg): 1.03 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23108 0 0 0 102933 79 0 0 25 0 1 0 545582919 98050048 22924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22924 603 41 0 23897 0
vsize: 95752
[startup+1040.04 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23111 0 0 0 103933 79 0 0 25 0 1 0 545582919 98050048 22927 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22927 603 41 0 23897 0
vsize: 95752
[startup+1050.04 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23114 0 0 0 104933 79 0 0 25 0 1 0 545582919 98050048 22930 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22930 603 41 0 23897 0
vsize: 95752
[startup+1060.04 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23117 0 0 0 105933 80 0 0 25 0 1 0 545582919 98050048 22933 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22933 603 41 0 23897 0
vsize: 95752
[startup+1070.04 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23124 0 0 0 106933 80 0 0 25 0 1 0 545582919 98050048 22940 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22940 603 41 0 23897 0
vsize: 95752
[startup+1080.04 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23132 0 0 0 107933 80 0 0 25 0 1 0 545582919 98050048 22948 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22948 603 41 0 23897 0
vsize: 95752
[startup+1090.04 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23135 0 0 0 108933 80 0 0 25 0 1 0 545582919 98050048 22951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22951 603 41 0 23897 0
vsize: 95752
[startup+1100.04 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23138 0 0 0 109932 81 0 0 25 0 1 0 545582919 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+1110.04 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23141 0 0 0 110932 81 0 0 25 0 1 0 545582919 98050048 22957 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22957 603 41 0 23897 0
vsize: 95752
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23144 0 0 0 111932 81 0 0 25 0 1 0 545582919 98050048 22960 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22960 603 41 0 23897 0
vsize: 95752
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23147 0 0 0 112932 81 0 0 25 0 1 0 545582919 98050048 22963 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22963 603 41 0 23897 0
vsize: 95752
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23151 0 0 0 113932 81 0 0 25 0 1 0 545582919 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+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23154 0 0 0 114932 82 0 0 25 0 1 0 545582919 98050048 22970 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22970 603 41 0 23897 0
vsize: 95752
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23157 0 0 0 115932 82 0 0 25 0 1 0 545582919 98050048 22973 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22973 603 41 0 23897 0
vsize: 95752
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23160 0 0 0 116932 82 0 0 25 0 1 0 545582919 98050048 22976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22976 603 41 0 23897 0
vsize: 95752
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23163 0 0 0 117932 82 0 0 25 0 1 0 545582919 98050048 22979 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22979 603 41 0 23897 0
vsize: 95752
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23166 0 0 0 118932 83 0 0 25 0 1 0 545582919 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
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 3071
Raw data (stat): 3014 (minisat+) R 3013 26298 26297 0 -1 0 23169 0 0 0 119932 83 0 0 25 0 1 0 545582919 98050048 22985 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22985 603 41 0 23897 0
vsize: 95752
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 3071
Raw data (stat): 3014 (minisat+) Z 3013 26298 26297 0 -1 12 23172 0 0 0 119932 88 0 0 25 0 1 0 545582919 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.1
CPU time (s): 1200.21
CPU user time (s): 1199.32
CPU system time (s): 0.880866
CPU usage (%): 100.009
Max. virtual memory (Kb): 95752
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####