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/miplib/normalized-mps-v2-13-7-p2756.opb
MD5SUM	cc9b9a1bf5f3e0998bc97d2eed5cbbd9
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.07484
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 15574

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        872776 kB
Buffers:          5236 kB
Cached:         133240 kB
SwapCached:        516 kB
Active:          30680 kB
Inactive:       109808 kB
HighTotal:      131008 kB
HighFree:        36540 kB
LowTotal:       903652 kB
LowFree:        836236 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            15844 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:25:05 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 17170 7 1200.23 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.85 0.95 0.93 2/54 28862
Raw data (stat): 28862 (runsolver) R 28861 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542419620 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.0005 s]
Raw data (loadavg): 0.87 0.95 0.93 2/54 28862
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 5052 0 0 0 984 14 0 0 25 0 1 0 542419620 23248896 4868 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5676 4868 603 41 0 5635 0
vsize: 22704
[startup+19.9998 s]
Raw data (loadavg): 0.89 0.96 0.93 2/54 28862
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 5359 0 0 0 1982 15 0 0 25 0 1 0 542419620 24518656 5175 4294967295 134512640 134672761 3221224544 3221223696 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5986 5175 603 41 0 5945 0
vsize: 23944
[startup+30.0012 s]
Raw data (loadavg): 0.91 0.96 0.93 2/54 28862
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 6145 0 0 0 2980 18 0 0 25 0 1 0 542419620 27877376 5961 4294967295 134512640 134672761 3221224544 3221223696 134565103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6806 5961 603 41 0 6765 0
vsize: 27224
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.96 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 6517 0 0 0 3978 19 0 0 25 0 1 0 542419620 29356032 6333 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7167 6333 603 41 0 7126 0
vsize: 28668
[startup+50.0032 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 6963 0 0 0 4976 21 0 0 25 0 1 0 542419620 31105024 6779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7594 6779 603 41 0 7553 0
vsize: 30376
[startup+60.0033 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 7266 0 0 0 5975 23 0 0 25 0 1 0 542419620 32575488 7082 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7953 7082 603 41 0 7912 0
vsize: 31812
[startup+70.004 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 7591 0 0 0 6974 24 0 0 25 0 1 0 542419620 33792000 7407 4294967295 134512640 134672761 3221224544 3221223672 1075347105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8250 7407 603 41 0 8209 0
vsize: 33000
[startup+80.0043 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 8111 0 0 0 7971 27 0 0 25 0 1 0 542419620 35938304 7927 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8774 7927 603 41 0 8733 0
vsize: 35096
[startup+90.0045 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 8523 0 0 0 8969 29 0 0 25 0 1 0 542419620 37539840 8339 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9165 8339 603 41 0 9124 0
vsize: 36660
[startup+100.005 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 9009 0 0 0 9967 31 0 0 25 0 1 0 542419620 39563264 8825 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9659 8825 603 41 0 9618 0
vsize: 38636
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 9248 0 0 0 10966 32 0 0 25 0 1 0 542419620 40505344 9064 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9889 9064 603 41 0 9848 0
vsize: 39556
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 9501 0 0 0 11965 33 0 0 25 0 1 0 542419620 41971712 9317 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10247 9317 603 41 0 10206 0
vsize: 40988
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 9854 0 0 0 12964 35 0 0 25 0 1 0 542419620 43454464 9670 4294967295 134512640 134672761 3221224544 3221223728 134558890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10609 9670 603 41 0 10568 0
vsize: 42436
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 10191 0 0 0 13964 35 0 0 25 0 1 0 542419620 44802048 10007 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10938 10007 603 41 0 10897 0
vsize: 43752
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 10875 0 0 0 14962 38 0 0 25 0 1 0 542419620 47505408 10691 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11598 10691 603 41 0 11557 0
vsize: 46392
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 11594 0 0 0 15960 39 0 0 25 0 1 0 542419620 50442240 11410 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12315 11410 603 41 0 12274 0
vsize: 49260
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 12371 0 0 0 16959 41 0 0 25 0 1 0 542419620 53645312 12187 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13097 12187 603 41 0 13056 0
vsize: 52388
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 13019 0 0 0 17957 43 0 0 25 0 1 0 542419620 56332288 12835 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13753 12835 603 41 0 13712 0
vsize: 55012
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 13650 0 0 0 18955 45 0 0 25 0 1 0 542419620 58888192 13466 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14377 13466 603 41 0 14336 0
vsize: 57508
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 14277 0 0 0 19954 46 0 0 25 0 1 0 542419620 61431808 14093 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14093 603 41 0 14957 0
vsize: 59992
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 14804 0 0 0 20952 48 0 0 25 0 1 0 542419620 63586304 14620 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15524 14620 603 41 0 15483 0
vsize: 62096
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 15048 0 0 0 21952 48 0 0 25 0 1 0 542419620 64532480 14864 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15755 14864 603 41 0 15714 0
vsize: 63020
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 15365 0 0 0 22952 49 0 0 25 0 1 0 542419620 65871872 15181 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16082 15181 603 41 0 16041 0
vsize: 64328
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 15567 0 0 0 23951 49 0 0 25 0 1 0 542419620 66682880 15383 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16280 15383 603 41 0 16239 0
vsize: 65120
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 15806 0 0 0 24950 51 0 0 25 0 1 0 542419620 67624960 15622 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16510 15622 603 41 0 16469 0
vsize: 66040
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 16004 0 0 0 25950 51 0 0 25 0 1 0 542419620 68435968 15820 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16708 15820 603 41 0 16667 0
vsize: 66832
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 16145 0 0 0 26950 51 0 0 25 0 1 0 542419620 68976640 15961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16840 15961 603 41 0 16799 0
vsize: 67360
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 16317 0 0 0 27949 52 0 0 25 0 1 0 542419620 69652480 16133 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17005 16133 603 41 0 16964 0
vsize: 68020
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 16479 0 0 0 28949 52 0 0 25 0 1 0 542419620 70324224 16295 4294967295 134512640 134672761 3221224544 3221223724 134565024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17169 16295 603 41 0 17128 0
vsize: 68676
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 16648 0 0 0 29949 53 0 0 25 0 1 0 542419620 70995968 16464 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17333 16464 603 41 0 17292 0
vsize: 69332
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 16817 0 0 0 30949 53 0 0 25 0 1 0 542419620 71663616 16633 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17496 16633 603 41 0 17455 0
vsize: 69984
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 17003 0 0 0 31948 54 0 0 25 0 1 0 542419620 72335360 16819 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17660 16819 603 41 0 17619 0
vsize: 70640
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 17224 0 0 0 32948 54 0 0 25 0 1 0 542419620 73277440 17040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17890 17040 603 41 0 17849 0
vsize: 71560
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 17387 0 0 0 33947 55 0 0 25 0 1 0 542419620 73945088 17203 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18053 17203 603 41 0 18012 0
vsize: 72212
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 17727 0 0 0 34946 57 0 0 25 0 1 0 542419620 75292672 17543 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18382 17543 603 41 0 18341 0
vsize: 73528
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 18327 0 0 0 35944 59 0 0 25 0 1 0 542419620 78753792 18143 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19227 18143 603 41 0 19186 0
vsize: 76908
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 19028 0 0 0 36943 60 0 0 25 0 1 0 542419620 81567744 18844 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19914 18844 603 41 0 19873 0
vsize: 79656
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 19684 0 0 0 37942 62 0 0 25 0 1 0 542419620 84262912 19500 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20572 19500 603 41 0 20531 0
vsize: 82288
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 20227 0 0 0 38940 63 0 0 25 0 1 0 542419620 86417408 20043 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21098 20043 603 41 0 21057 0
vsize: 84392
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 20683 0 0 0 39940 63 0 0 25 0 1 0 542419620 88297472 20499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21557 20499 603 41 0 21516 0
vsize: 86228
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 20967 0 0 0 40939 64 0 0 25 0 1 0 542419620 89505792 20783 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21852 20783 603 41 0 21811 0
vsize: 87408
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 21243 0 0 0 41938 65 0 0 25 0 1 0 542419620 90583040 21059 4294967295 134512640 134672761 3221224544 3221223648 134559769 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22115 21059 603 41 0 22074 0
vsize: 88460
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 21421 0 0 0 42937 66 0 0 25 0 1 0 542419620 91258880 21237 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22280 21237 603 41 0 22239 0
vsize: 89120
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 21713 0 0 0 43936 67 0 0 25 0 1 0 542419620 92471296 21529 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22576 21529 603 41 0 22535 0
vsize: 90304
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23035 0 0 0 44934 70 0 0 25 0 1 0 542419620 98050048 22851 4294967295 134512640 134672761 3221224544 3221223844 134556634 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23035 0 0 0 45934 70 0 0 25 0 1 0 542419620 98050048 22851 4294967295 134512640 134672761 3221224544 3221223744 134557809 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23035 0 0 0 46934 70 0 0 25 0 1 0 542419620 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23036 0 0 0 47934 71 0 0 25 0 1 0 542419620 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134560964 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23036 0 0 0 48934 71 0 0 25 0 1 0 542419620 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134561027 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23036 0 0 0 49934 71 0 0 25 0 1 0 542419620 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134561406 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23036 0 0 0 50934 71 0 0 25 0 1 0 542419620 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23036 0 0 0 51935 71 0 0 25 0 1 0 542419620 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23036 0 0 0 52935 71 0 0 25 0 1 0 542419620 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23036 0 0 0 53935 71 0 0 25 0 1 0 542419620 98050048 22852 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22852 603 41 0 23897 0
vsize: 95752
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23037 0 0 0 54935 71 0 0 25 0 1 0 542419620 98050048 22853 4294967295 134512640 134672761 3221224544 3221223720 134559059 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23038 0 0 0 55935 71 0 0 25 0 1 0 542419620 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+570.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23038 0 0 0 56936 71 0 0 25 0 1 0 542419620 98050048 22854 4294967295 134512640 134672761 3221224544 3221223696 134565137 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23038 0 0 0 57936 71 0 0 25 0 1 0 542419620 98050048 22854 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23038 0 0 0 58936 71 0 0 25 0 1 0 542419620 98050048 22854 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22854 603 41 0 23897 0
vsize: 95752
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23042 0 0 0 59936 71 0 0 25 0 1 0 542419620 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23042 0 0 0 60936 71 0 0 25 0 1 0 542419620 98050048 22858 4294967295 134512640 134672761 3221224544 3221223668 134566037 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.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23042 0 0 0 61936 71 0 0 25 0 1 0 542419620 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+630.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23042 0 0 0 62936 71 0 0 25 0 1 0 542419620 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23042 0 0 0 63937 71 0 0 25 0 1 0 542419620 98050048 22858 4294967295 134512640 134672761 3221224544 3221223744 134557822 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.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23042 0 0 0 64937 71 0 0 25 0 1 0 542419620 98050048 22858 4294967295 134512640 134672761 3221224544 3221223696 134565064 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.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23042 0 0 0 65937 71 0 0 25 0 1 0 542419620 98050048 22858 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22858 603 41 0 23897 0
vsize: 95752
[startup+670.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23045 0 0 0 66937 71 0 0 25 0 1 0 542419620 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+680.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23045 0 0 0 67937 71 0 0 25 0 1 0 542419620 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.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23046 0 0 0 68938 71 0 0 25 0 1 0 542419620 98050048 22862 4294967295 134512640 134672761 3221224544 3221223712 134560892 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.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23046 0 0 0 69938 71 0 0 25 0 1 0 542419620 98050048 22862 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22862 603 41 0 23897 0
vsize: 95752
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23047 0 0 0 70938 71 0 0 25 0 1 0 542419620 98050048 22863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22863 603 41 0 23897 0
vsize: 95752
[startup+720.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 71938 71 0 0 25 0 1 0 542419620 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+730.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 72938 71 0 0 25 0 1 0 542419620 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 73939 71 0 0 25 0 1 0 542419620 98050048 22864 4294967295 134512640 134672761 3221224544 3221223744 134557809 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 74939 71 0 0 25 0 1 0 542419620 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560871 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 75939 71 0 0 25 0 1 0 542419620 98050048 22864 4294967295 134512640 134672761 3221224544 3221223696 134565092 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 76939 71 0 0 25 0 1 0 542419620 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 77939 71 0 0 25 0 1 0 542419620 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134561001 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 78939 71 0 0 25 0 1 0 542419620 98050048 22864 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 79939 71 0 0 25 0 1 0 542419620 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 3/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 80940 71 0 0 25 0 1 0 542419620 98050048 22864 4294967295 134512640 134672761 3221224544 3221223744 134557852 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 81940 71 0 0 25 0 1 0 542419620 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 82940 71 0 0 25 0 1 0 542419620 98050048 22864 4294967295 134512640 134672761 3221224544 3221223712 134561118 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 83940 71 0 0 25 0 1 0 542419620 98050048 22864 4294967295 134512640 134672761 3221224544 3221223600 134565083 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.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23048 0 0 0 84940 71 0 0 25 0 1 0 542419620 98050048 22864 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22864 603 41 0 23897 0
vsize: 95752
[startup+860.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23050 0 0 0 85941 71 0 0 25 0 1 0 542419620 98050048 22866 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22866 603 41 0 23897 0
vsize: 95752
[startup+870.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23054 0 0 0 86940 71 0 0 25 0 1 0 542419620 98050048 22870 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 22870 603 41 0 23897 0
vsize: 95752
[startup+880.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23058 0 0 0 87940 71 0 0 25 0 1 0 542419620 98050048 22874 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22874 603 41 0 23897 0
vsize: 95752
[startup+890.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23061 0 0 0 88940 71 0 0 25 0 1 0 542419620 98050048 22877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22877 603 41 0 23897 0
vsize: 95752
[startup+900.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23065 0 0 0 89940 71 0 0 25 0 1 0 542419620 98050048 22881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22881 603 41 0 23897 0
vsize: 95752
[startup+910.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23068 0 0 0 90940 71 0 0 25 0 1 0 542419620 98050048 22884 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22884 603 41 0 23897 0
vsize: 95752
[startup+920.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23072 0 0 0 91941 71 0 0 25 0 1 0 542419620 98050048 22888 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22888 603 41 0 23897 0
vsize: 95752
[startup+930.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23075 0 0 0 92941 71 0 0 25 0 1 0 542419620 98050048 22891 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22891 603 41 0 23897 0
vsize: 95752
[startup+940.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23079 0 0 0 93941 71 0 0 25 0 1 0 542419620 98050048 22895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22895 603 41 0 23897 0
vsize: 95752
[startup+950.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23082 0 0 0 94941 71 0 0 25 0 1 0 542419620 98050048 22898 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22898 603 41 0 23897 0
vsize: 95752
[startup+960.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23084 0 0 0 95941 71 0 0 25 0 1 0 542419620 98050048 22900 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22900 603 41 0 23897 0
vsize: 95752
[startup+970.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23086 0 0 0 96941 71 0 0 25 0 1 0 542419620 98050048 22902 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22902 603 41 0 23897 0
vsize: 95752
[startup+980.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23089 0 0 0 97942 71 0 0 25 0 1 0 542419620 98050048 22905 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22905 603 41 0 23897 0
vsize: 95752
[startup+990.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23092 0 0 0 98942 71 0 0 25 0 1 0 542419620 98050048 22908 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22908 603 41 0 23897 0
vsize: 95752
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23096 0 0 0 99942 71 0 0 25 0 1 0 542419620 98050048 22912 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22912 603 41 0 23897 0
vsize: 95752
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23099 0 0 0 100942 71 0 0 25 0 1 0 542419620 98050048 22915 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22915 603 41 0 23897 0
vsize: 95752
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23102 0 0 0 101942 71 0 0 25 0 1 0 542419620 98050048 22918 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22918 603 41 0 23897 0
vsize: 95752
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23106 0 0 0 102942 71 0 0 25 0 1 0 542419620 98050048 22922 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22922 603 41 0 23897 0
vsize: 95752
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23109 0 0 0 103942 72 0 0 25 0 1 0 542419620 98050048 22925 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22925 603 41 0 23897 0
vsize: 95752
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23112 0 0 0 104942 72 0 0 25 0 1 0 542419620 98050048 22928 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22928 603 41 0 23897 0
vsize: 95752
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23115 0 0 0 105942 72 0 0 25 0 1 0 542419620 98050048 22931 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22931 603 41 0 23897 0
vsize: 95752
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23118 0 0 0 106943 72 0 0 25 0 1 0 542419620 98050048 22934 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22934 603 41 0 23897 0
vsize: 95752
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23128 0 0 0 107943 72 0 0 25 0 1 0 542419620 98050048 22944 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22944 603 41 0 23897 0
vsize: 95752
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23133 0 0 0 108943 72 0 0 25 0 1 0 542419620 98050048 22949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22949 603 41 0 23897 0
vsize: 95752
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23136 0 0 0 109943 72 0 0 25 0 1 0 542419620 98050048 22952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22952 603 41 0 23897 0
vsize: 95752
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23139 0 0 0 110943 72 0 0 25 0 1 0 542419620 98050048 22955 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22955 603 41 0 23897 0
vsize: 95752
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23142 0 0 0 111943 72 0 0 25 0 1 0 542419620 98050048 22958 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22958 603 41 0 23897 0
vsize: 95752
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23145 0 0 0 112944 72 0 0 25 0 1 0 542419620 98050048 22961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22961 603 41 0 23897 0
vsize: 95752
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23149 0 0 0 113944 72 0 0 25 0 1 0 542419620 98050048 22965 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22965 603 41 0 23897 0
vsize: 95752
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23152 0 0 0 114944 72 0 0 25 0 1 0 542419620 98050048 22968 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22968 603 41 0 23897 0
vsize: 95752
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23155 0 0 0 115944 72 0 0 25 0 1 0 542419620 98050048 22971 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22971 603 41 0 23897 0
vsize: 95752
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23158 0 0 0 116944 72 0 0 25 0 1 0 542419620 98050048 22974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22974 603 41 0 23897 0
vsize: 95752
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23161 0 0 0 117944 72 0 0 25 0 1 0 542419620 98050048 22977 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22977 603 41 0 23897 0
vsize: 95752
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23164 0 0 0 118945 72 0 0 25 0 1 0 542419620 98050048 22980 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22980 603 41 0 23897 0
vsize: 95752
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 28864
Raw data (stat): 28862 (minisat+) R 28861 27565 27564 0 -1 0 23167 0 0 0 119945 72 0 0 25 0 1 0 542419620 98050048 22983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23938 22983 603 41 0 23897 0
vsize: 95752
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 28864
Raw data (stat): 28862 (minisat+) Z 28861 27565 27564 0 -1 12 23170 0 0 0 119945 76 0 0 25 0 1 0 542419620 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.06
CPU time (s): 1200.23
CPU user time (s): 1199.46
CPU system time (s): 0.767883
CPU usage (%): 100.014
Max. virtual memory (Kb): 95752
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####