PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-p2756.opb
MD5SUM	f2badf1ad4c3213045697b74fa812a03
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.06284
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 21633

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        882548 kB
Buffers:          7900 kB
Cached:         123860 kB
SwapCached:        364 kB
Active:          24004 kB
Inactive:       109920 kB
HighTotal:      131008 kB
HighFree:        39844 kB
LowTotal:       903652 kB
LowFree:        842704 kB
SwapTotal:     2097136 kB
SwapFree:      2096008 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            12484 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 00:52:55 (client local time) WITH STATUS 10 IN 1200.38 SECONDS
stats: 12893 7 1200.38 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): ssssssss..ssssss.sss.ssss..................................................................................................................s.......s...........
c ---[ 759]---> Adder-cost: 72   maxlim: 709   bits: 11/10
c ---[ 758]---> Adder-cost: 90   maxlim: 763   bits: 11/10
c ---[ 757]---> Adder-cost: 147   maxlim: 556   bits: 11/10
c ---[ 756]---> Adder-cost: 120   maxlim: 309   bits: 10/9
c ---[ 755]---> Adder-cost: 108   maxlim: 489   bits: 10/9
c ---[ 754]---> Adder-cost: 108   maxlim: 652   bits: 11/10
c ---[ 752]---> Adder-cost: 134   maxlim: 1088   bits: 12/11
c ---[ 751]---> Adder-cost: 132   maxlim: 200   bits: 9/8
c ---[ 750]---> Adder-cost: 128   maxlim: 418   bits: 10/9
c ---[ 749]---> Adder-cost: 128   maxlim: 1026   bits: 12/11
c ---[ 747]---> Adder-cost: 134   maxlim: 427   bits: 10/9
c ---[ 746]---> Adder-cost: 127   maxlim: 659   bits: 11/10
c ---[ 745]---> Adder-cost: 128   maxlim: 1234   bits: 12/11
c ---[ 744]---> Adder-cost: 134   maxlim: 1043   bits: 12/11
c ---[ 742]---> Adder-cost: 104   maxlim: 373   bits: 10/9
c ---[ 741]---> Adder-cost: 129   maxlim: 981   bits: 11/10
c ---[ 740]---> Adder-cost: 134   maxlim: 197   bits: 9/8
c ---[ 739]---> Adder-cost: 145   maxlim: 443   bits: 10/9
c ---[ 738]---> Adder-cost: 106   maxlim: 669   bits: 11/10
c ---[ 737]---> Adder-cost: 128   maxlim: 1252   bits: 12/11
c ---[ 736]---> Adder-cost: 96   maxlim: 563   bits: 11/10
c ---[ 735]---> Adder-cost: 82   maxlim: 556   bits: 11/10
c ---[ 734]---> Adder-cost: 86   maxlim: 393   bits: 10/9
c ---[ 733]---> Adder-cost: 112   maxlim: 1040   bits: 12/11
c ---[ 732]---> Adder-cost: 117   maxlim: 920   bits: 11/10
c ---[ 731]---> Adder-cost: 109   maxlim: 640   bits: 11/10
c ---[ 730]---> Adder-cost: 96   maxlim: 627   bits: 11/10
c ---[ 729]---> Adder-cost: 82   maxlim: 621   bits: 11/10
c ---[ 728]---> Adder-cost: 92   maxlim: 458   bits: 10/9
c ---[ 727]---> Adder-cost: 120   maxlim: 1259   bits: 12/11
c ---[ 726]---> Adder-cost: 120   maxlim: 1139   bits: 12/11
c ---[ 725]---> Adder-cost: 121   maxlim: 861   bits: 11/10
c ---[ 724]---> Adder-cost: 98   maxlim: 586   bits: 11/10
c ---[ 723]---> Adder-cost: 78   maxlim: 580   bits: 11/10
c ---[ 722]---> Adder-cost: 86   maxlim: 417   bits: 10/9
c ---[ 721]---> Adder-cost: 120   maxlim: 1131   bits: 12/11
c ---[ 720]---> Adder-cost: 121   maxlim: 1011   bits: 11/10
c ---[ 719]---> Adder-cost: 109   maxlim: 731   bits: 11/10
c ---[ 718]---> Adder-cost: 103   maxlim: 731   bits: 11/10
c ---[ 717]---> Adder-cost: 76   maxlim: 725   bits: 11/10
c ---[ 716]---> Adder-cost: 94   maxlim: 562   bits: 11/10
c ---[ 715]---> Adder-cost: 113   maxlim: 208   bits: 9/8
c ---[ 714]---> Adder-cost: 118   maxlim: 1222   bits: 12/11
c ---[ 713]---> Adder-cost: 117   maxlim: 942   bits: 11/10
c ---[ 712]---> Adder-cost: 121   maxlim: 608   bits: 11/10
c ---[ 711]---> Adder-cost: 102   maxlim: 608   bits: 11/10
c ---[ 710]---> Adder-cost: 40   maxlim: 491   bits: 10/9
c ---[ 709]---> Adder-cost: 57   maxlim: 409   bits: 10/9
c ---[ 708]---> Adder-cost: 77   maxlim: 250   bits: 9/8
c ---[ 707]---> Adder-cost: 101   maxlim: 268   bits: 10/9
c ---[ 706]---> Adder-cost: 89   maxlim: 268   bits: 10/9
c ---[ 705]---> Adder-cost: 97   maxlim: 314   bits: 10/9
c ---[ 704]---> Adder-cost: 96   maxlim: 226   bits: 9/8
c ---[ 703]---> Adder-cost: 103   maxlim: 891   bits: 11/10
c ---[ 702]---> Adder-cost: 94   maxlim: 491   bits: 10/9
c ---[ 701]---> Adder-cost: 96   maxlim: 491   bits: 10/9
c ---[ 700]---> Adder-cost: 96   maxlim: 536   bits: 11/10
c ---[ 699]---> Adder-cost: 98   maxlim: 448   bits: 10/9
c ---[ 698]---> Adder-cost: 50   maxlim: 289   bits: 10/9
c ---[ 697]---> Adder-cost: 100   maxlim: 1113   bits: 12/11
c ---[ 696]---> Adder-cost: 97   maxlim: 262   bits: 10/9
c ---[ 695]---> Adder-cost: 89   maxlim: 262   bits: 10/9
c ---[ 694]---> Adder-cost: 95   maxlim: 308   bits: 10/9
c ---[ 693]---> Adder-cost: 92   maxlim: 220   bits: 9/8
c ---[ 692]---> Adder-cost: 99   maxlim: 885   bits: 11/10
c ---[ 691]---> Adder-cost: 100   maxlim: 480   bits: 10/9
c ---[ 690]---> Adder-cost: 98   maxlim: 480   bits: 10/9
c ---[ 689]---> Adder-cost: 96   maxlim: 532   bits: 11/10
c ---[ 688]---> Adder-cost: 96   maxlim: 438   bits: 10/9
c ---[ 686]---> Adder-cost: 92   maxlim: 1103   bits: 12/11
c ---[ 685]---> Adder-cost: 99   maxlim: 278   bits: 10/9
c ---[ 684]---> Adder-cost: 95   maxlim: 278   bits: 10/9
c ---[ 683]---> Adder-cost: 91   maxlim: 324   bits: 10/9
c ---[ 682]---> Adder-cost: 94   maxlim: 236   bits: 9/8
c ---[ 681]---> Adder-cost: 97   maxlim: 901   bits: 11/10
c ---[ 680]---> Adder-cost: 108   maxlim: 510   bits: 10/9
c ---[ 679]---> Adder-cost: 98   maxlim: 510   bits: 10/9
c ---[ 678]---> Adder-cost: 94   maxlim: 556   bits: 11/10
c ---[ 677]---> Adder-cost: 96   maxlim: 468   bits: 10/9
c ---[ 676]---> Adder-cost: 110   maxlim: 469   bits: 10/9
c ---[ 675]---> Adder-cost: 98   maxlim: 1133   bits: 12/11
c ---[ 674]---> Adder-cost: 125   maxlim: 869   bits: 11/10
c ---[ 673]---> Adder-cost: 127   maxlim: 923   bits: 11/10
c ---[ 672]---> Adder-cost: 120   maxlim: 325   bits: 10/9
c ---[ 671]---> Adder-cost: 128   maxlim: 1266   bits: 12/11
c ---[ 670]---> Adder-cost: 115   maxlim: 183   bits: 9/8
c ---[ 669]---> Adder-cost: 119   maxlim: 719   bits: 11/10
c ---[ 668]---> Adder-cost: 63   maxlim: 358   bits: 10/9
c ---[ 667]---> Adder-cost: 59   maxlim: 402   bits: 10/9
c ---[ 666]---> Adder-cost: 90   maxlim: 752   bits: 11/10
c ---[ 664]---> Adder-cost: 61   maxlim: 495   bits: 10/9
c ---[ 662]---> Adder-cost: 108   maxlim: 1192   bits: 12/11
c ---[ 661]---> Adder-cost: 93   maxlim: 470   bits: 10/9
c ---[ 659]---> Adder-cost: 58   maxlim: 526   bits: 11/10
c ---[ 657]---> Adder-cost: 104   maxlim: 1028   bits: 12/11
c ---[ 656]---> Adder-cost: 61   maxlim: 374   bits: 10/9
c ---[ 655]---> Adder-cost: 35   maxlim: 249   bits: 9/8
c ---[ 654]---> Adder-cost: 69   maxlim: 277   bits: 10/9
c ---[ 651]---> Adder-cost: 42   maxlim: 823   bits: 11/10
c ---[ 650]---> Adder-cost: 40   maxlim: 455   bits: 10/9
c ---[ 649]---> Adder-cost: 74   maxlim: 977   bits: 11/10
c ---[ 648]---> Adder-cost: 75   maxlim: 1031   bits: 12/11
c ---[ 647]---> Adder-cost: 51   maxlim: 385   bits: 10/9
c ---[ 646]---> Adder-cost: 52   maxlim: 796   bits: 11/10
c ---[ 645]---> Adder-cost: 52   maxlim: 294   bits: 10/9
c ---[ 644]---> Adder-cost: 35   maxlim: 450   bits: 10/9
c ---[ 643]---> Adder-cost: 78   maxlim: 882   bits: 11/10
c ---[ 642]---> Adder-cost: 111   maxlim: 903   bits: 11/10
c ---[ 641]---> Adder-cost: 85   maxlim: 284   bits: 10/9
c ---[ 640]---> Adder-cost: 38   maxlim: 450   bits: 10/9
c ---[ 638]---> Adder-cost: 94   maxlim: 1303   bits: 12/11
c ---[ 637]---> Adder-cost: 104   maxlim: 1275   bits: 12/11
c ---[ 636]---> Adder-cost: 43   maxlim: 191   bits: 9/8
c ---[ 635]---> Adder-cost: 85   maxlim: 943   bits: 11/10
c ---[ 634]---> Adder-cost: 88   maxlim: 484   bits: 10/9
c ---[ 633]---> Adder-cost: 75   maxlim: 433   bits: 10/9
c ---[ 632]---> Adder-cost: 80   maxlim: 1070   bits: 12/11
c ---[ 631]---> Adder-cost: 102   maxlim: 1238   bits: 12/11
c ---[ 630]---> Adder-cost: 92   maxlim: 1081   bits: 12/11
c ---[ 629]---> Adder-cost: 82   maxlim: 840   bits: 11/10
c ---[ 628]---> Adder-cost: 81   maxlim: 379   bits: 10/9
c ---[ 627]---> Adder-cost: 77   maxlim: 328   bits: 10/9
c ---[ 626]---> Adder-cost: 83   maxlim: 965   bits: 11/10
c ---[ 625]---> Adder-cost: 69   maxlim: 529   bits: 11/10
c ---[ 624]---> Adder-cost: 53   maxlim: 412   bits: 10/9
c ---[ 623]---> Adder-cost: 58   maxlim: 184   bits: 9/8
c ---[ 622]---> Adder-cost: 75   maxlim: 374   bits: 10/9
c ---[ 620]---> Adder-cost: 90   maxlim: 1152   bits: 12/11
c ---[ 619]---> Adder-cost: 86   maxlim: 818   bits: 11/10
c ---[ 618]---> Adder-cost: 121   maxlim: 695   bits: 11/10
c ---[ 617]---> Adder-cost: 117   maxlim: 644   bits: 11/10
c ---[ 616]---> Adder-cost: 81   maxlim: 939   bits: 11/10
c ---[ 615]---> Adder-cost: 97   maxlim: 942   bits: 11/10
c ---[ 614]---> Adder-cost: 56   maxlim: 853   bits: 11/10
c ---[ 613]---> Adder-cost: 82   maxlim: 632   bits: 11/10
c ---[ 610]---> Adder-cost: 74   maxlim: 636   bits: 11/10
c ---[ 609]---> Adder-cost: 38   maxlim: 394   bits: 10/9
c ---[ 608]---> Adder-cost: 62   maxlim: 166   bits: 9/8
c ---[ 607]---> Adder-cost: 75   maxlim: 356   bits: 10/9
c ---[ 606]---> Adder-cost: 52   maxlim: 739   bits: 11/10
c ---[ 605]---> Adder-cost: 90   maxlim: 1089   bits: 12/11
c ---[ 604]---> Adder-cost: 86   maxlim: 814   bits: 11/10
c ---[ 603]---> Adder-cost: 117   maxlim: 672   bits: 11/10
c ---[ 602]---> Adder-cost: 110   maxlim: 621   bits: 11/10
c ---[ 601]---> Adder-cost: 68   maxlim: 912   bits: 11/10
c ---[ 600]---> Adder-cost: 97   maxlim: 972   bits: 11/10
c ---[ 599]---> Adder-cost: 86   maxlim: 862   bits: 11/10
c ---[ 596]---> Adder-cost: 78   maxlim: 503   bits: 10/9
c ---[ 595]---> Adder-cost: 110   maxlim: 1326   bits: 12/11
c ---[ 594]---> Adder-cost: 82   maxlim: 868   bits: 11/10
c ---[ 593]---> Adder-cost: 31   maxlim: 156   bits: 9/8
c ---[ 592]---> Adder-cost: 110   maxlim: 1480   bits: 12/11
c ---[ 591]---> Adder-cost: 93   maxlim: 935   bits: 11/10
c ---[ 590]---> Adder-cost: 102   maxlim: 1428   bits: 12/11
c ---[ 589]---> Adder-cost: 91   maxlim: 927   bits: 11/10
c ---[ 588]---> Adder-cost: 82   maxlim: 541   bits: 11/10
c ---[ 587]---> Adder-cost: 78   maxlim: 1026   bits: 12/11
c ---[ 586]---> Adder-cost: 100   maxlim: 1288   bits: 12/11
c ---[ 585]---> Adder-cost: 84   maxlim: 830   bits: 11/10
c ---[ 584]---> Adder-cost: 106   maxlim: 1442   bits: 12/11
c ---[ 583]---> Adder-cost: 86   maxlim: 828   bits: 11/10
c ---[ 582]---> Adder-cost: 104   maxlim: 1322   bits: 12/11
c ---[ 581]---> Adder-cost: 99   maxlim: 937   bits: 11/10
c ---[ 580]---> Adder-cost: 84   maxlim: 483   bits: 10/9
c ---[ 579]---> Adder-cost: 76   maxlim: 917   bits: 11/10
c ---[ 578]---> Adder-cost: 132   maxlim: 1605   bits: 12/11
c ---[ 577]---> Adder-cost: 84   maxlim: 828   bits: 11/10
c ---[ 576]---> Adder-cost: 140   maxlim: 1759   bits: 12/11
c ---[ 575]---> Adder-cost: 148   maxlim: 1468   bits: 12/11
c ---[ 574]---> Adder-cost: 170   maxlim: 1914   bits: 12/11
c ---[ 573]---> Adder-cost: 160   maxlim: 1481   bits: 12/11
c ---[ 572]---> Adder-cost: 127   maxlim: 754   bits: 11/10
c ---[ 571]---> Adder-cost: 138   maxlim: 1560   bits: 12/11
c ---[ 570]---> Adder-cost: 138   maxlim: 1497   bits: 12/11
c ---[ 569]---> Adder-cost: 80   maxlim: 724   bits: 11/10
c ---[ 568]---> Adder-cost: 140   maxlim: 1651   bits: 12/11
c ---[ 567]---> Adder-cost: 140   maxlim: 1264   bits: 12/11
c ---[ 566]---> Adder-cost: 162   maxlim: 1715   bits: 12/11
c ---[ 565]---> Adder-cost: 158   maxlim: 1367   bits: 12/11
c ---[ 563]---> Adder-cost: 77   maxlim: 1356   bits: 12/11
c ---[ 562]---> Adder-cost: 62   maxlim: 195   bits: 9/8
c ---[ 561]---> Adder-cost: 75   maxlim: 1305   bits: 12/11
c ---[ 560]---> Adder-cost: 71   maxlim: 884   bits: 11/10
c ---[ 559]---> Adder-cost: 74   maxlim: 766   bits: 11/10
c ---[ 558]---> Adder-cost: 118   maxlim: 1452   bits: 12/11
c ---[ 557]---> Adder-cost: 76   maxlim: 664   bits: 11/10
c ---[ 556]---> Adder-cost: 77   maxlim: 1552   bits: 12/11
c ---[ 555]---> Adder-cost: 88   maxlim: 1299   bits: 12/11
c ---[ 554]---> Adder-cost: 70   maxlim: 666   bits: 11/10
c ---[ 553]---> Adder-cost: 136   maxlim: 1573   bits: 12/11
c ---[ 552]---> Adder-cost: 73   maxlim: 1325   bits: 12/11
c ---[ 551]---> Adder-cost: 76   maxlim: 906   bits: 11/10
c ---[ 550]---> Adder-cost: 51   maxlim: 189   bits: 9/8
c ---[ 549]---> Adder-cost: 92   maxlim: 1058   bits: 12/11
c ---[ 547]---> Adder-cost: 92   maxlim: 709   bits: 11/10
c ---[ 546]---> Adder-cost: 144   maxlim: 1597   bits: 12/11
c ---[ 545]---> Adder-cost: 63   maxlim: 1025   bits: 12/11
c ---[ 544]---> Adder-cost: 84   maxlim: 711   bits: 11/10
c ---[ 543]---> Adder-cost: 89   maxlim: 1555   bits: 12/11
c ---[ 542]---> Adder-cost: 81   maxlim: 1309   bits: 12/11
c ---[ 541]---> Adder-cost: 59   maxlim: 729   bits: 11/10
c ---[ 539]---> Adder-cost: 57   maxlim: 354   bits: 10/9
c ---[ 538]---> Adder-cost: 71   maxlim: 944   bits: 11/10
c ---[ 537]---> Adder-cost: 45   maxlim: 588   bits: 11/10
c ---[ 536]---> Adder-cost: 64   maxlim: 1080   bits: 12/11
c ---[ 535]---> Adder-cost: 77   maxlim: 585   bits: 11/10
c ---[ 534]---> Adder-cost: 77   maxlim: 654   bits: 11/10
c ---[ 533]---> Adder-cost: 75   maxlim: 950   bits: 11/10
c ---[ 532]---> Adder-cost: 65   maxlim: 880   bits: 11/10
c ---[ 531]---> Adder-cost: 45   maxlim: 523   bits: 11/10
c ---[ 530]---> Adder-cost: 65   maxlim: 1015   bits: 11/10
c ---[ 528]---> Adder-cost: 54   maxlim: 813   bits: 11/10
c ---[ 526]---> Adder-cost: 66   maxlim: 729   bits: 11/10
c ---[ 525]---> Adder-cost: 63   maxlim: 921   bits: 11/10
c ---[ 524]---> Adder-cost: 47   maxlim: 564   bits: 11/10
c ---[ 523]---> Adder-cost: 58   maxlim: 1056   bits: 12/11
c ---[ 522]---> Adder-cost: 68   maxlim: 494   bits: 10/9
c ---[ 521]---> Adder-cost: 61   maxlim: 563   bits: 11/10
c ---[ 520]---> Adder-cost: 50   maxlim: 859   bits: 11/10
c ---[ 519]---> Adder-cost: 69   maxlim: 776   bits: 11/10
c ---[ 518]---> Adder-cost: 54   maxlim: 419   bits: 10/9
c ---[ 517]---> Adder-cost: 51   maxlim: 813   bits: 11/10
c ---[ 516]---> Adder-cost: 61   maxlim: 911   bits: 11/10
c ---[ 515]---> Adder-cost: 72   maxlim: 1417   bits: 12/11
c ---[ 513]---> Adder-cost: 67   maxlim: 648   bits: 11/10
c ---[ 512]---> Adder-cost: 72   maxlim: 1159   bits: 12/11
c ---[ 511]---> Adder-cost: 70   maxlim: 796   bits: 11/10
c ---[ 509]---> Adder-cost: 28   maxlim: 165   bits: 9/8
c ---[ 508]---> Adder-cost: 40   maxlim: 437   bits: 10/9
c ---[ 507]---> Adder-cost: 46   maxlim: 192   bits: 9/8
c ---[ 506]---> Adder-cost: 56   maxlim: 1051   bits: 12/11
c ---[ 505]---> Adder-cost: 64   maxlim: 1016   bits: 11/10
c ---[ 504]---> Adder-cost: 67   maxlim: 971   bits: 11/10
c ---[ 503]---> Adder-cost: 54   maxlim: 1169   bits: 12/11
c ---[ 502]---> Adder-cost: 59   maxlim: 479   bits: 10/9
c ---[ 501]---> Adder-cost: 70   maxlim: 828   bits: 11/10
c ---[ 500]---> Adder-cost: 65   maxlim: 793   bits: 11/10
c ---[ 499]---> Adder-cost: 64   maxlim: 749   bits: 11/10
c ---[ 498]---> Adder-cost: 63   maxlim: 947   bits: 11/10
c ---[ 497]---> Adder-cost: 52   maxlim: 257   bits: 10/9
c ---[ 496]---> Adder-cost: 58   maxlim: 260   bits: 10/9
c ---[ 495]---> Adder-cost: 60   maxlim: 1057   bits: 12/11
c ---[ 494]---> Adder-cost: 57   maxlim: 1022   bits: 11/10
c ---[ 493]---> Adder-cost: 71   maxlim: 977   bits: 11/10
c ---[ 492]---> Adder-cost: 46   maxlim: 1175   bits: 12/11
c ---[ 491]---> Adder-cost: 55   maxlim: 485   bits: 10/9
c ---[ 490]---> Adder-cost: 56   maxlim: 839   bits: 11/10
c ---[ 489]---> Adder-cost: 53   maxlim: 804   bits: 11/10
c ---[ 488]---> Adder-cost: 66   maxlim: 753   bits: 11/10
c ---[ 487]---> Adder-cost: 57   maxlim: 957   bits: 11/10
c ---[ 486]---> Adder-cost: 58   maxlim: 267   bits: 10/9
c ---[ 485]---> Adder-cost: 61   maxlim: 383   bits: 10/9
c ---[ 484]---> Adder-cost: 58   maxlim: 1041   bits: 12/11
c ---[ 483]---> Adder-cost: 55   maxlim: 1006   bits: 11/10
c ---[ 482]---> Adder-cost: 61   maxlim: 961   bits: 11/10
c ---[ 481]---> Adder-cost: 56   maxlim: 1159   bits: 12/11
c ---[ 480]---> Adder-cost: 55   maxlim: 469   bits: 10/9
c ---[ 479]---> Adder-cost: 60   maxlim: 809   bits: 11/10
c ---[ 478]---> Adder-cost: 46   maxlim: 774   bits: 11/10
c ---[ 477]---> Adder-cost: 66   maxlim: 729   bits: 11/10
c ---[ 476]---> Adder-cost: 55   maxlim: 927   bits: 11/10
c ---[ 475]---> Adder-cost: 49   maxlim: 237   bits: 9/8
c ---[ 474]---> Adder-cost: 48   maxlim: 457   bits: 10/9
c ---[ 473]---> Adder-cost: 82   maxlim: 775   bits: 11/10
c ---[ 472]---> Adder-cost: 81   maxlim: 686   bits: 11/10
c ---[ 471]---> Adder-cost: 84   maxlim: 1404   bits: 12/11
c ---[ 469]---> Adder-cost: 82   maxlim: 1426   bits: 12/11
c ---[ 468]---> Adder-cost: 87   maxlim: 1010   bits: 11/10
c ---[ 467]---> Adder-cost: 34   maxlim: 608   bits: 11/10
c ---[ 466]---> Adder-cost: 32   maxlim: 529   bits: 11/10
c ---[ 464]---> Adder-cost: 1992   maxlim: 571   bits: 11/10
c ---[ 463]---> Adder-cost: 67   maxlim: 918   bits: 11/10
c ---[ 462]---> Adder-cost: 166   maxlim: 399   bits: 10/9
c ---[ 461]---> Adder-cost: 307   maxlim: 274   bits: 10/9
c ---[ 460]---> Adder-cost: 426   maxlim: 1316   bits: 11/11
c ---[ 459]---> Adder-cost: 540   maxlim: 1397   bits: 11/11
c ---[ 458]---> Adder-cost: 533   maxlim: 98   bits: 8/7
c ---[ 457]---> Adder-cost: 62   maxlim: 186   bits: 8/8
c ---[ 456]---> Adder-cost: 90   maxlim: 119   bits: 8/7
c ---[ 455]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 453]---> Adder-cost: 56   maxlim: 918   bits: 11/10
c ---[ 451]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 449]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 448]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 446]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 444]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 442]---> Adder-cost: 55   maxlim: 308   bits: 10/9
c ---[ 441]---> Adder-cost: 52   maxlim: 297   bits: 10/9
c ---[ 439]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 437]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 436]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 434]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 432]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 431]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 430]---> Adder-cost: 27   maxlim: 364   bits: 10/9
c ---[ 429]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 428]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 425]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 423]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 422]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 420]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 419]---> Adder-cost: 44   maxlim: 670   bits: 11/10
c ---[ 417]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 414]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 412]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 411]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 409]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 408]---> Adder-cost: 44   maxlim: 670   bits: 11/10
c ---[ 406]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 405]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 404]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 403]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 401]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 399]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 397]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 394]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 393]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 391]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 388]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 387]---> Adder-cost: 53   maxlim: 312   bits: 10/9
c ---[ 384]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 383]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 382]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 381]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 380]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 379]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 376]---> Adder-cost: 52   maxlim: 479   bits: 10/9
c ---[ 375]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 374]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 372]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 370]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 369]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 366]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 365]---> Adder-cost: 70   maxlim: 921   bits: 11/10
c ---[ 364]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 362]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 360]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 359]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 358]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 357]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 356]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 355]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 354]---> Adder-cost: 77   maxlim: 921   bits: 11/10
c ---[ 351]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 350]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 348]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 346]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 345]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 343]---> Adder-cost: 44   maxlim: 323   bits: 10/9
c ---[ 341]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 340]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 338]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 336]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 335]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 332]---> Adder-cost: 54   maxlim: 667   bits: 11/10
c ---[ 331]---> Adder-cost: 48   maxlim: 522   bits: 11/10
c ---[ 330]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 327]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 325]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 322]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 321]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 320]---> Adder-cost: 52   maxlim: 665   bits: 11/10
c ---[ 317]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 314]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 312]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 309]---> Adder-cost: 122   maxlim: 1206   bits: 12/11
c ---[ 308]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 307]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 306]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 303]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 302]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 300]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 299]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 298]---> Adder-cost: 126   maxlim: 1206   bits: 12/11
c ---[ 296]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 295]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 294]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 292]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 291]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 290]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 288]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 287]---> Adder-cost: 46   maxlim: 626   bits: 11/10
c ---[ 285]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 284]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 283]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 282]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 281]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 278]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 277]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 276]---> Adder-cost: 30   maxlim: 382   bits: 10/9
c ---[ 274]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 273]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 271]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 270]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 269]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 267]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 266]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 265]---> Adder-cost: 38   maxlim: 688   bits: 11/10
c ---[ 264]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 262]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 260]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 259]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 258]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 257]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 256]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 255]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 254]---> Adder-cost: 49   maxlim: 688   bits: 11/10
c ---[ 253]---> Adder-cost: 6   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 ---[ 250]---> 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 ---[ 247]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 246]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 245]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 243]---> Adder-cost: 33   maxlim: 173   bits: 9/8
c ---[ 242]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 241]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 239]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 238]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 237]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 236]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 234]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 233]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 232]---> Adder-cost: 61   maxlim: 375   bits: 10/9
c ---[ 230]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 229]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 227]---> 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 ---[ 224]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 222]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 221]---> Adder-cost: 76   maxlim: 700   bits: 11/10
c ---[ 220]---> Adder-cost: 58   maxlim: 483   bits: 10/9
c ---[ 219]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 217]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 216]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 214]---> 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 ---[ 210]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 209]---> Adder-cost: 56   maxlim: 944   bits: 11/10
c ---[ 208]---> 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 ---[ 203]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 202]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 201]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 199]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 198]---> Adder-cost: 75   maxlim: 944   bits: 11/10
c ---[ 195]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ---[ 193]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 192]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 190]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 188]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 187]---> Adder-cost: 51   maxlim: 350   bits: 10/9
c ---[ 186]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 185]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 182]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 180]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 179]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 177]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 176]---> Adder-cost: 49   maxlim: 492   bits: 10/9
c ---[ 174]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 173]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 172]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 169]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 167]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 166]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 165]---> Adder-cost: 60   maxlim: 435   bits: 10/9
c ---[ 163]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 161]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 160]---> Adder-cost: 0   maxlim: 1   bits: 2/1
c ---[ 159]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 156]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 154]---> Adder-cost: 124   maxlim: 1229   bits: 12/11
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: 0   maxlim: 1   bits: 2/1
c ---[ 146]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 145]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 143]---> Adder-cost: 116   maxlim: 1229   bits: 12/11
c ---[ 142]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 140]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 139]---> 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: 6   maxlim: 2   bits: 3/2
c ---[ 133]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 132]---> Adder-cost: 41   maxlim: 759   bits: 11/10
c ---[ 131]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 129]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 127]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 126]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 124]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 123]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 120]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 118]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 117]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 115]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 114]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 112]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 110]---> Adder-cost: 32   maxlim: 218   bits: 9/8
c ---[ 109]---> Adder-cost: 47   maxlim: 279   bits: 10/9
c ---[ 108]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 107]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 105]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 104]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 102]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 100]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  99]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  96]---> 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 ---[  91]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  90]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  88]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  87]---> Adder-cost: 50   maxlim: 333   bits: 10/9
c ---[  86]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  84]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  80]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 69   maxlim: 193   bits: 9/8
c ---[  75]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  74]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  72]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  71]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  70]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  69]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[  65]---> Adder-cost: 55   maxlim: 527   bits: 11/10
c ---[  64]---> Adder-cost: 378   maxlim: 188   bits: 9/8
c ---[  63]---> Adder-cost: 28   maxlim: 13   bits: 5/4
c ---[  62]---> Adder-cost: 28   maxlim: 13   bits: 5/4
c ---[  61]---> Adder-cost: 28   maxlim: 13   bits: 5/4
c ---[  60]---> Adder-cost: 28   maxlim: 13   bits: 5/4
c ---[  59]---> Adder-cost: 66   maxlim: 32   bits: 7/6
c ---[  58]---> Adder-cost: 63   maxlim: 31   bits: 6/5
c ---[  57]---> Adder-cost: 80   maxlim: 39   bits: 7/6
c ---[  56]---> Adder-cost: 92   maxlim: 45   bits: 7/6
c ---[  55]---> Adder-cost: 244   maxlim: 121   bits: 8/7
c ---[  54]---> Adder-cost: 55   maxlim: 717   bits: 11/10
c ---[  53]---> Adder-cost: 244   maxlim: 121   bits: 8/7
c ---[  52]---> Adder-cost: 244   maxlim: 121   bits: 8/7
c ---[  51]---> Adder-cost: 244   maxlim: 121   bits: 8/7
c ---[  50]---> Adder-cost: 15   maxlim: 7   bits: 4/3
c ---[  49]---> Adder-cost: 120   maxlim: 59   bits: 7/6
c ---[  48]---> Adder-cost: 18   maxlim: 8   bits: 5/4
c ---[  47]---> Adder-cost: 52   maxlim: 248   bits: 9/8
c ---[  46]---> Adder-cost: 73   maxlim: 222   bits: 9/8
c ---[  45]---> Adder-cost: 37   maxlim: 317   bits: 10/9
c ---[  44]---> Adder-cost: 67   maxlim: 189   bits: 9/8
c ---[  43]---> Adder-cost: 66   maxlim: 897   bits: 11/10
c ---[  42]---> Adder-cost: 49   maxlim: 440   bits: 10/9
c ---[  41]---> Adder-cost: 54   maxlim: 299   bits: 10/9
c ---[  40]---> Adder-cost: 61   maxlim: 517   bits: 11/10
c ---[  39]---> Adder-cost: 49   maxlim: 775   bits: 11/10
c ---[  38]---> Adder-cost: 50   maxlim: 357   bits: 10/9
c ---[  37]---> Adder-cost: 76   maxlim: 224   bits: 9/8
c ---[  36]---> Adder-cost: 53   maxlim: 319   bits: 10/9
c ---[  35]---> Adder-cost: 63   maxlim: 191   bits: 9/8
c ---[  34]---> Adder-cost: 81   maxlim: 438   bits: 10/9
c ---[  33]---> Adder-cost: 87   maxlim: 345   bits: 10/9
c ---[  32]---> Adder-cost: 65   maxlim: 404   bits: 10/9
c ---[  31]---> Adder-cost: 94   maxlim: 611   bits: 11/10
c ---[  30]---> Adder-cost: 71   maxlim: 823   bits: 11/10
c ---[  29]---> Adder-cost: 84   maxlim: 352   bits: 10/9
c ---[  28]---> Adder-cost: 82   maxlim: 332   bits: 10/9
c ---[  27]---> Adder-cost: 51   maxlim: 423   bits: 10/9
c ---[  26]---> Adder-cost: 82   maxlim: 299   bits: 10/9
c ---[  25]---> Adder-cost: 97   maxlim: 642   bits: 11/10
c ---[  24]---> Adder-cost: 101   maxlim: 544   bits: 11/10
c ---[  23]---> Adder-cost: 92   maxlim: 725   bits: 11/10
c ---[  22]---> Adder-cost: 116   maxlim: 1157   bits: 12/11
c ---[  21]---> Adder-cost: 67   maxlim: 153   bits: 9/8
c ---[  20]---> Adder-cost: 78   maxlim: 179   bits: 9/8
c ---[  19]---> Adder-cost: 82   maxlim: 155   bits: 9/8
c ---[  18]---> Adder-cost: 46   maxlim: 164   bits: 9/8
c ---[  17]---> Adder-cost: 35   maxlim: 142   bits: 9/8
c ---[  16]---> Adder-cost: 15   maxlim: 56   bits: 7/6
c ---[  15]---> Adder-cost: 31   maxlim: 133   bits: 9/8
c ---[  14]---> Adder-cost: 15   maxlim: 47   bits: 7/6
c ---[  13]---> Adder-cost: 38   maxlim: 82   bits: 8/7
c ---[  12]---> Adder-cost: 41   maxlim: 72   bits: 8/7
c ---[  11]---> Adder-cost: 37   maxlim: 72   bits: 8/7
c ---[  10]---> Adder-cost: 47   maxlim: 95   bits: 8/7
c ---[   9]---> Adder-cost: 49   maxlim: 95   bits: 8/7
c ---[   8]---> Adder-cost: 54   maxlim: 100   bits: 8/7
c ---[   7]---> Adder-cost: 78   maxlim: 118   bits: 8/7
c ---[   6]---> Adder-cost: 65   maxlim: 125   bits: 8/7
c ---[   5]---> Adder-cost: 36   maxlim: 88   bits: 8/7
c ---[   4]---> Adder-cost: 19   maxlim: 57   bits: 7/6
c ---[   3]---> Adder-cost: 73   maxlim: 132   bits: 9/8
c ---[   2]---> Adder-cost: 39   maxlim: 129   bits: 9/8
c ---[   1]---> Adder-cost: 59   maxlim: 184   bits: 9/8
c ---[   0]---> Adder-cost: 46   maxlim: 151   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 |  223556   792613 |   81976      98      554     5.7 |  5.914 % |
c |       251 |  223556   792613 |   90174     249     1521     6.1 |  5.914 % |
c |       476 |  223556   792613 |   99191     474     3395     7.2 |  5.914 % |
c |       813 |  223538   792562 |  109110     808     6718     8.3 |  5.921 % |
c |      1320 |  223520   792511 |  120021    1312    12302     9.4 |  5.929 % |
c |      2079 |  223496   792443 |  132023    2066    17937     8.7 |  5.939 % |
c |      3220 |  223466   792358 |  145226    3202    27875     8.7 |  5.951 % |
c |      4929 |  223448   792307 |  159748    4908    43303     8.8 |  5.959 % |
c |      7491 |  223399   792160 |  175723    7461    66275     8.9 |  5.976 % |
c |     11335 |  223350   792013 |  193296   11296   108703     9.6 |  5.994 % |
c |     17101 |  223289   791822 |  212625   17050   177391    10.4 |  6.016 % |
c |     25750 |  222965   790718 |  233888   25590   282272    11.0 |  6.089 % |
c |     38724 |  222848   790376 |  257277   38542   431135    11.2 |  6.134 % |
c |     58185 |  222598   789552 |  283004   57901   713958    12.3 |  6.199 % |
c |     87377 |  222374   788804 |  311305   86832  1279524    14.7 |  6.244 % |
c |    131166 |  221638   786260 |  342435  130187  2581708    19.8 |  6.384 % |
c |    196851 |  221400   785486 |  376679  195643  4115344    21.0 |  6.454 % |
c ==============================================================================
c [1mFound solution: 125716[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11276   maxlim: 196115   bits: 19/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    276541 |  299930  1065968 |   99976  274973  6233969    22.7 |  6.454 % |
c |    276641 |  299930  1065968 |  109973   32374   262025     8.1 |  5.094 % |
c |    276791 |  299915  1065915 |  120970   32521   263567     8.1 |  5.096 % |
c |    277017 |  299915  1065915 |  133068   32747   265750     8.1 |  5.096 % |
c |    277357 |  299915  1065915 |  146374   33087   268837     8.1 |  5.096 % |
c |    277863 |  299915  1065915 |  161012   33593   273273     8.1 |  5.096 % |
c |    278622 |  299915  1065915 |  177113   34352   280527     8.2 |  5.096 % |
c |    279762 |  299915  1065915 |  194824   35492   291429     8.2 |  5.096 % |
c |    281471 |  299900  1065862 |  214307   37198   309726     8.3 |  5.098 % |
c |    284033 |  299891  1065831 |  235738   39756   338974     8.5 |  5.100 % |
c |    287877 |  299891  1065831 |  259311   43600   400869     9.2 |  5.100 % |
c |    293643 |  299891  1065831 |  285243   49366   464102     9.4 |  5.100 % |
c |    302293 |  299885  1065814 |  313767   58014   601494    10.4 |  5.102 % |
c |    315267 |  299879  1065794 |  345144   70986  1475920    20.8 |  5.104 % |
c |    334728 |  299855  1065710 |  379658   90443  1725558    19.1 |  5.108 % |
c |    363920 |  299831  1065626 |  417624  119629  2152892    18.0 |  5.112 % |
c |    407711 |  299801  1065525 |  459387  163409  2651559    16.2 |  5.118 % |
c |    473395 |  299801  1065525 |  505325  229093  4149735    18.1 |  5.118 % |
c |    571922 |  299801  1065525 |  555858  327620  8026284    24.5 |  5.118 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1_bit0 -x2_bit0 -x3_bit0 -x4_bit0 x5_bit0 -x6_bit0 x9_bit0 -x10_bit0 -x11_bit0 -x14_bit0 -x17_bit0 -x19_bit0 -x20_bit0 -x21_bit0 -x22_bit0 -x23_bit0 -x24_bit0 x27_bit0 -x29_bit0 -x30_bit0 -x31_bit0 -x32_bit0 -x33_bit0 -x34_bit0 -x35_bit0 -x36_bit0 -x37_bit0 -x38_bit0 -x39_bit0 -x42_bit0 -x44_bit0 -x45_bit0 -x46_bit0 -x47_bit0 -x48_bit0 -x49_bit0 x50_bit0 x51_bit0 -x54_bit0 -x56_bit0 -x57_bit0 -x58_bit0 -x59_bit0 -x60_bit0 -x61_bit0 -x62_bit0 x65_bit0 -x66_bit0 -x67_bit0 x68_bit0 -x70_bit0 -x73_bit0 -x74_bit0 -x75_bit0 x76_bit0 -x77_bit0 -x78_bit0 -x79_bit0 -x80_bit0 x83_bit0 -x85_bit0 -x86_bit0 -x87_bit0 -x88_bit0 -x89_bit0 -x90_bit0 -x91_bit0 -x92_bit0 -x93_bit0 -x94_bit0 -x95_bit0 x98_bit0 -x100_bit0 -x101_bit0 -x102_bit0 -x103_bit0 -x104_bit0 -x105_bit0 -x106_bit0 -x107_bit0 -x110_bit0 -x112_bit0 -x113_bit0 -x114_bit0 -x115_bit0 x116_bit0 x117_bit0 x119_bit0 -x120_bit0 -x121_bit0 -x122_bit0 -x123_bit0 x124_bit0 -x126_bit0 -x127_bit0 x128_bit0 -x129_bit0 -x131_bit0 -x132_bit0 -x133_bit0 -x134_bit0 -x135_bit0 x136_bit0 -x137_bit0 -x139_bit0 x140_bit0 x141_bit0 -x142_bit0 -x143_bit0 -x144_bit0 -x145_bit0 x148_bit0 x149_bit0 -x150_bit0 x153_bit0 -x156_bit0 x158_bit0 -x159_bit0 x160_bit0 -x161_bit0 -x162_bit0 -x163_bit0 -x166_bit0 -x168_bit0 -x169_bit0 -x170_bit0 -x171_bit0 -x172_bit0 x173_bit0 x174_bit0 -x175_bit0 x176_bit0 -x177_bit0 -x178_bit0 -x181_bit0 -x183_bit0 -x184_bit0 -x185_bit0 x186_bit0 -x187_bit0 -x188_bit0 x189_bit0 x190_bit0 -x193_bit0 -x195_bit0 -x196_bit0 -x197_bit0 -x198_bit0 -x199_bit0 -x200_bit0 -x201_bit0 -x204_bit0 x205_bit0 -x206_bit0 -x207_bit0 -x209_bit0 -x212_bit0 -x213_bit0 -x214_bit0 -x215_bit0 -x216_bit0 -x217_bit0 -x218_bit0 -x219_bit0 -x222_bit0 -x224_bit0 -x225_bit0 -x226_bit0 -x227_bit0 -x228_bit0 -x229_bit0 -x230_bit0 -x231_bit0 -x232_bit0 -x233_bit0 -x234_bit0 x237_bit0 -x239_bit0 -x240_bit0 -x241_bit0 x242_bit0 -x243_bit0 -x244_bit0 x245_bit0 -x246_bit0 x249_bit0 -x251_bit0 -x252_bit0 x253_bit0 -x254_bit0 -x255_bit0 x256_bit0 -x258_bit0 -x259_bit0 x260_bit0 -x261_bit0 -x262_bit0 -x263_bit0 -x265_bit0 -x266_bit0 x267_bit0 x268_bit0 -x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 -x275_bit0 -x276_bit0 -x278_bit0 -x279_bit0 -x280_bit0 x281_bit0 -x283_bit0 -x284_bit0 -x285_bit0 -x286_bit0 -x289_bit0 -x290_bit0 -x291_bit0 -x292_bit0 -x293_bit0 x294_bit0 x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 -x299_bit0 -x300_bit0 -x303_bit0 -x304_bit0 -x305_bit0 x306_bit0 -x307_bit0 -x308_bit0 -x309_bit0 -x310_bit0 -x313_bit0 -x314_bit0 -x315_bit0 -x316_bit0 -x317_bit0 -x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 x333_bit0 -x335_bit0 -x338_bit0 -x339_bit0 -x340_bit0 -x341_bit0 -x343_bit0 -x344_bit0 -x345_bit0 -x347_bit0 -x348_bit0 -x349_bit0 -x351_bit0 -x352_bit0 -x353_bit0 -x354_bit0 -x356_bit0 x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 x363_bit0 -x366_bit0 -x367_bit0 -x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 -x373_bit0 -x374_bit0 -x375_bit0 -x376_bit0 -x377_bit0 -x380_bit0 -x381_bit0 -x382_bit0 -x383_bit0 -x384_bit0 x385_bit0 -x386_bit0 -x387_bit0 -x390_bit0 -x391_bit0 x392_bit0 x393_bit0 x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 -x399_bit0 -x400_bit0 x403_bit0 -x404_bit0 -x405_bit0 x406_bit0 -x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0 x412_bit0 x415_bit0 -x416_bit0 -x417_bit0 -x418_bit0 -x419_bit0 x420_bit0 -x421_bit0 -x422_bit0 x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x428_bit0 -x429_bit0 -x430_bit0 -x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 x436_bit0 x437_bit0 -x438_bit0 -x439_bit0 -x440_bit0 x441_bit0 -x442_bit0 -x443_bit0 -x444_bit0 -x445_bit0 x446_bit0 -x447_bit0 -x448_bit0 -x449_bit0 x450_bit0 -x451_bit0 -x452_bit0 -x453_bit0 x454_bit0 -x456_bit0 x457_bit0 -x458_bit0 -x459_bit0 -x460_bit0 x461_bit0 x463_bit0 -x464_bit0 -x465_bit0 x466_bit0 x467_bit0 x468_bit0 x469_bit0 -x470_bit0 -x471_bit0 x472_bit0 -x473_bit0 -x474_bit0 -x475_bit0 x476_bit0 x479_bit0 x480_bit0 x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 x485_bit0 x486_bit0 -x489_bit0 x490_bit0 -x491_bit0 -x492_bit0 x493_bit0 -x494_bit0 x495_bit0 -x496_bit0 -x497_bit0 x498_bit0 -x499_bit0 x500_bit0 x501_bit0 -x502_bit0 -x503_bit0 -x506_bit0 -x507_bit0 -x508_bit0 x509_bit0 -x510_bit0 -x511_bit0 x512_bit0 -x513_bit0 -x514_bit0 x515_bit0 -x516_bit0 x517_bit0 -x519_bit0 -x522_bit0 -x523_bit0 -x524_bit0 x525_bit0 x526_bit0 -x527_bit0 -x528_bit0 -x529_bit0 -x530_bit0 -x531_bit0 -x532_bit0 -x533_bit0 x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 -x540_bit0 -x541_bit0 x542_bit0 -x543_bit0 -x544_bit0 -x545_bit0 x546_bit0 x549_bit0 -x550_bit0 -x551_bit0 x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 x556_bit0 -x559_bit0 x560_bit0 x561_bit0 x562_bit0 x563_bit0 -x564_bit0 x565_bit0 -x566_bit0 -x567_bit0 -x568_bit0 -x569_bit0 x570_bit0 x571_bit0 -x572_bit0 -x573_bit0 x576_bit0 -x577_bit0 -x578_bit0 -x579_bit0 -x580_bit0 -x581_bit0 x582_bit0 -x583_bit0 -x584_bit0 -x585_bit0 -x586_bit0 -x587_bit0 x588_bit0 -x589_bit0 x592_bit0 -x593_bit0 -x594_bit0 -x595_bit0 x596_bit0 -x597_bit0 x598_bit0 x599_bit0 -x600_bit0 -x601_bit0 -x602_bit0 x603_bit0 -x605_bit0 -x606_bit0 -x607_bit0 -x608_bit0 -x609_bit0 -x610_bit0 -x611_bit0 -x612_bit0 -x613_bit0 -x614_bit0 -x615_bit0 -x616_bit0 -x617_bit0 -x618_bit0 x619_bit0 -x620_bit0 -x621_bit0 -x622_bit0 x623_bit0 x624_bit0 -x625_bit0 -x626_bit0 -x627_bit0 -x628_bit0 -x629_bit0 -x630_bit0 -x631_bit0 -x633_bit0 x634_bit0 -x635_bit0 -x636_bit0 -x637_bit0 x638_bit0 -x639_bit0 -x640_bit0 -x641_bit0 -x642_bit0 -x643_bit0 x644_bit0 -x645_bit0 x646_bit0 -x647_bit0 -x648_bit0 -x650_bit0 -x651_bit0 -x652_bit0 -x653_bit0 -x656_bit0 -x657_bit0 -x658_bit0 -x659_bit0 -x660_bit0 -x661_bit0 -x662_bit0 x663_bit0 -x666_bit0 -x667_bit0 -x668_bit0 -x669_bit0 -x670_bit0 -x671_bit0 -x672_bit0 -x673_bit0 -x674_bit0 -x675_bit0 -x676_bit0 -x677_bit0 -x678_bit0 -x679_bit0 -x680_bit0 -x683_bit0 x684_bit0 -x685_bit0 -x686_bit0 -x687_bit0 -x688_bit0 x689_bit0 -x690_bit0 -x691_bit0 -x692_bit0 -x693_bit0 -x694_bit0 -x696_bit0 -x699_bit0 -x700_bit0 x701_bit0 x702_bit0 -x703_bit0 -x704_bit0 -x705_bit0 -x706_bit0 x707_bit0 -x708_bit0 -x709_bit0 x710_bit0 -x712_bit0 -x713_bit0 -x714_bit0 -x715_bit0 -x716_bit0 x717_bit0 -x718_bit0 -x719_bit0 -x720_bit0 -x721_bit0 -x722_bit0 -x723_bit0 -x726_bit0 -x727_bit0 -x728_bit0 -x729_bit0 x730_bit0 x731_bit0 -x732_bit0 -x733_bit0 -x736_bit0 -x737_bit0 -x738_bit0 x739_bit0 -x740_bit0 -x741_bit0 -x742_bit0 -x743_bit0 -x744_bit0 -x745_bit0 -x746_bit0 -x747_bit0 x748_bit0 -x749_bit0 -x750_bit0 -x753_bit0 -x754_bit0 -x755_bit0 -x756_bit0 -x757_bit0 -x758_bit0 x759_bit0 -x760_bit0 -x761_bit0 -x762_bit0 -x763_bit0 -x764_bit0 x765_bit0 -x766_bit0 -x769_bit0 -x770_bit0 -x771_bit0 x772_bit0 -x773_bit0 x774_bit0 -x775_bit0 -x776_bit0 x777_bit0 -x778_bit0 -x779_bit0 -x780_bit0 -x782_bit0 -x783_bit0 -x784_bit0 -x785_bit0 -x786_bit0 -x787_bit0 x788_bit0 -x789_bit0 -x790_bit0 -x791_bit0 -x792_bit0 x793_bit0 x796_bit0 x797_bit0 -x798_bit0 -x799_bit0 -x800_bit0 -x812_bit0 -x813_bit0 -x814_bit0 -x815_bit0 -x816_bit0 -x817_bit0 -x818_bit0 -x821_bit0 -x822_bit0 x823_bit0 -x824_bit0 -x825_bit0 -x829_bit0 x833_bit0 -x837_bit0 -x838_bit0 x839_bit0 -x840_bit0 -x841_bit0 -x842_bit0 x843_bit0 x846_bit0 -x847_bit0 -x848_bit0 -x849_bit0 -x850_bit0 -x851_bit0 x854_bit0 -x856_bit0 x860_bit0 -x864_bit0 -x865_bit0 -x867_bit0 x870_bit0 -x871_bit0 x872_bit0 -x873_bit0 -x875_bit0 -x876_bit0 -x877_bit0 -x878_bit0 -x879_bit0 -x880_bit0 x882_bit0 -x883_bit0 -x884_bit0 -x885_bit0 -x886_bit0 -x887_bit0 -x888_bit0 x889_bit0 -x890_bit0 -x891_bit0 -x892_bit0 x893_bit0 -x896_bit0 -x897_bit0 -x898_bit0 -x899_bit0 -x900_bit0 -x904_bit0 x908_bit0 -x912_bit0 -x913_bit0 -x914_bit0 -x915_bit0 -x916_bit0 -x917_bit0 -x918_bit0 -x921_bit0 -x922_bit0 -x923_bit0 -x924_bit0 -x925_bit0 -x926_bit0 x929_bit0 -x933_bit0 -x937_bit0 -x938_bit0 -x939_bit0 -x940_bit0 -x941_bit0 -x942_bit0 -x943_bit0 x946_bit0 -x947_bit0 -x948_bit0 -x949_bit0 x950_bit0 -x951_bit0 -x952_bit0 -x954_bit0 x955_bit0 -x956_bit0 -x959_bit0 -x960_bit0 -x961_bit0 -x962_bit0 -x964_bit0 -x965_bit0 -x967_bit0 -x970_bit0 -x971_bit0 -x972_bit0 -x973_bit0 x974_bit0 -x975_bit0 -x976_bit0 x977_bit0 -x978_bit0 x979_bit0 -x980_bit0 x982_bit0 -x983_bit0 -x984_bit0 -x985_bit0 x986_bit0 -x987_bit0 x988_bit0 -x989_bit0 -x990_bit0 x991_bit0 x992_bit0 -x993_bit0 -x994_bit0 -x995_bit0 -x996_bit0 x997_bit0 x1000_bit0 -x1001_bit0 -x1002_bit0 -x1003_bit0 -x1004_bit0 x1005_bit0 -x1008_bit0 -x1011_bit0 -x1012_bit0 -x1013_bit0 -x1014_bit0 -x1016_bit0 -x1017_bit0 -x1018_bit0 -x1019_bit0 -x1020_bit0 -x1021_bit0 -x1022_bit0 -x1023_bit0 -x1024_bit0 -x1025_bit0 -x1026_bit0 -x1029_bit0 -x1030_bit0 -x1031_bit0 -x1032_bit0 -x1033_bit0 -x1034_bit0 -x1035_bit0 -x1036_bit0 -x1037_bit0 x1038_bit0 -x1039_bit0 -x1040_bit0 -x1041_bit0 -x1042_bit0 -x1043_bit0 -x1045_bit0 -x1048_bit0 -x1049_bit0 -x1050_bit0 -x1051_bit0 x1052_bit0 -x1053_bit0 -x1054_bit0 -x1055_bit0 -x1056_bit0 -x1057_bit0 -x1058_bit0 -x1059_bit0 -x1060_bit0 x1061_bit0 -x1062_bit0 x1063_bit0 -x1064_bit0 -x1065_bit0 -x1066_bit0 -x1067_bit0 -x1070_bit0 -x1071_bit0 -x1072_bit0 x1073_bit0 -x1074_bit0 -x1075_bit0 -x1076_bit0 -x1077_bit0 -x1078_bit0 -x1079_bit0 -x1080_bit0 -x1081_bit0 -x1082_bit0 -x1083_bit0 -x1084_bit0 x1085_bit0 -x1086_bit0 -x1087_bit0 x1088_bit0 x1091_bit0 -x1092_bit0 -x1093_bit0 -x1094_bit0 x1095_bit0 -x1096_bit0 -x1097_bit0 -x1098_bit0 -x1099_bit0 -x1100_bit0 -x1101_bit0 -x1102_bit0 -x1103_bit0 -x1106_bit0 -x1107_bit0 -x1108_bit0 -x1109_bit0 -x1110_bit0 -x1111_bit0 -x1112_bit0 -x1113_bit0 -x1114_bit0 -x1115_bit0 -x1116_bit0 -x1117_bit0 -x1118_bit0 x1119_bit0 -x1120_bit0 x1121_bit0 -x1122_bit0 -x1123_bit0 -x1124_bit0 x1126_bit0 -x1127_bit0 -x1128_bit0 -x1129_bit0 -x1130_bit0 -x1131_bit0 -x1132_bit0 -x1133_bit0 -x1134_bit0 -x1135_bit0 -x1136_bit0 x1137_bit0 -x1138_bit0 -x1139_bit0 -x1140_bit0 -x1141_bit0 x1144_bit0 -x1145_bit0 x1146_bit0 -x1147_bit0 -x1148_bit0 -x1149_bit0 -x1152_bit0 -x1155_bit0 -x1156_bit0 -x1157_bit0 -x1158_bit0 -x1160_bit0 -x1161_bit0 -x1162_bit0 -x1163_bit0 -x1164_bit0 -x1165_bit0 -x1166_bit0 -x1167_bit0 -x1168_bit0 -x1169_bit0 -x1170_bit0 x1173_bit0 -x1174_bit0 -x1175_bit0 -x1176_bit0 -x1177_bit0 -x1178_bit0 -x1179_bit0 -x1180_bit0 -x1181_bit0 -x1182_bit0 -x1183_bit0 -x1184_bit0 -x1185_bit0 -x1186_bit0 -x1187_bit0 -x1189_bit0 -x1192_bit0 -x1193_bit0 -x1194_bit0 -x1195_bit0 -x1196_bit0 -x1197_bit0 -x1198_bit0 -x1199_bit0 -x1200_bit0 x1201_bit0 -x1202_bit0 -x1203_bit0 -x1204_bit0 -x1205_bit0 x1206_bit0 -x1207_bit0 -x1208_bit0 -x1209_bit0 -x1210_bit0 -x1211_bit0 -x1214_bit0 -x1215_bit0 -x1216_bit0 -x1217_bit0 -x1218_bit0 -x1219_bit0 -x1220_bit0 -x1221_bit0 x1222_bit0 -x1223_bit0 -x1224_bit0 -x1225_bit0 -x1226_bit0 x1227_bit0 -x1228_bit0 -x1229_bit0 -x1230_bit0 -x1231_bit0 -x1232_bit0 -x1235_bit0 -x1236_bit0 -x1237_bit0 -x1238_bit0 -x1239_bit0 -x1240_bit0 x1241_bit0 -x1242_bit0 -x1243_bit0 x1244_bit0 -x1245_bit0 x1246_bit0 -x1247_bit0 x1250_bit0 -x1251_bit0 -x1252_bit0 -x1253_bit0 -x1254_bit0 -x1255_bit0 -x1256_bit0 -x1257_bit0 -x1258_bit0 -x1259_bit0 -x1260_bit0 -x1261_bit0 -x1262_bit0 -x1263_bit0 -x1264_bit0 -x1265_bit0 -x1266_bit0 -x1267_bit0 x1268_bit0 -x1270_bit0 -x1271_bit0 -x1272_bit0 -x1273_bit0 -x1274_bit0 -x1275_bit0 -x1276_bit0 x1277_bit0 x1278_bit0 -x1279_bit0 -x1280_bit0 -x1281_bit0 -x1282_bit0 -x1283_bit0 -x1284_bit0 x1285_bit0 -x1286_bit0 -x1287_bit0 x1288_bit0 -x1289_bit0 -x1290_bit0 -x1291_bit0 -x1292_bit0 -x1293_bit0 -x1294_bit0 -x1295_bit0 -x1296_bit0 -x1297_bit0 -x1298_bit0 -x1299_bit0 -x1300_bit0 -x1301_bit0 -x1302_bit0 -x1303_bit0 -x1304_bit0 x1305_bit0 -x1306_bit0 -x1307_bit0 -x1308_bit0 x1309_bit0 -x1310_bit0 -x1311_bit0 x1312_bit0 -x1313_bit0 -x1314_bit0 -x1315_bit0 -x1316_bit0 -x1317_bit0 x1318_bit0 x1319_bit0 -x1320_bit0 -x1321_bit0 -x1322_bit0 -x1323_bit0 -x1324_bit0 -x1325_bit0 -x1326_bit0 -x1327_bit0 -x1328_bit0 -x1329_bit0 -x1330_bit0 -x1331_bit0 -x1332_bit0 -x1333_bit0 -x1334_bit0 -x1335_bit0 -x1336_bit0 -x1337_bit0 -x1338_bit0 -x1339_bit0 x1340_bit0 x1341_bit0 -x1342_bit0 -x1343_bit0 -x1344_bit0 -x1345_bit0 x1346_bit0 -x1348_bit0 x1349_bit0 x1351_bit0 -x1352_bit0 -x1353_bit0 -x1354_bit0 x1355_bit0 -x1356_bit0 -x1357_bit0 -x1358_bit0 x1359_bit0 -x1360_bit0 -x1361_bit0 -x1362_bit0 -x1363_bit0 x1364_bit0 x1365_bit0 -x1366_bit0 -x1367_bit0 -x1369_bit0 -x1370_bit0 -x1371_bit0 x1372_bit0 -x1373_bit0 -x1374_bit0 -x1375_bit0 -x1376_bit0 x1377_bit0 -x1378_bit0 -x1379_bit0 x1380_bit0 -x1381_bit0 -x1382_bit0 -x1384_bit0 -x1386_bit0 -x1387_bit0 -x1391_bit0 -x1392_bit0 x1393_bit0 x1394_bit0 -x1395_bit0 -x1396_bit0 -x1397_bit0 -x1398_bit0 x1399_bit0 x1401_bit0 -x1402_bit0 x1404_bit0 -x1405_bit0 x1406_bit0 -x1407_bit0 x1408_bit0 -x1409_bit0 x1410_bit0 x1411_bit0 -x1412_bit0 -x1413_bit0 -x1414_bit0 -x1415_bit0 -x1416_bit0 -x1417_bit0 x1418_bit0 -x1419_bit0 -x1420_bit0 -x1422_bit0 -x1423_bit0 x1424_bit0 -x1425_bit0 x1426_bit0 -x1427_bit0 -x1428_bit0 x1429_bit0 -x1430_bit0 -x1431_bit0 x1432_bit0 -x1433_bit0 -x1434_bit0 -x1435_bit0 -x1436_bit0 -x1437_bit0 -x1438_bit0 -x1440_bit0 -x1441_bit0 -x1442_bit0 x1443_bit0 -x1444_bit0 -x1445_bit0 -x1446_bit0 x1447_bit0 x1448_bit0 -x1449_bit0 -x1450_bit0 -x1451_bit0 -x1452_bit0 x1453_bit0 x1455_bit0 -x1457_bit0 -x1458_bit0 -x1459_bit0 -x1460_bit0 -x1461_bit0 -x1462_bit0 -x1463_bit0 x1464_bit0 x1465_bit0 -x1466_bit0 -x1467_bit0 -x1468_bit0 -x1469_bit0 -x1470_bit0 -x1471_bit0 -x1472_bit0 x1473_bit0 -x1475_bit0 -x1476_bit0 x1477_bit0 x1478_bit0 -x1479_bit0 -x1480_bit0 -x1481_bit0 -x1482_bit0 -x1483_bit0 -x1484_bit0 -x1485_bit0 x1486_bit0 x1487_bit0 -x1488_bit0 -x1489_bit0 -x1490_bit0 -x1491_bit0 -x1493_bit0 x1494_bit0 -x1495_bit0 -x1496_bit0 -x1497_bit0 -x1498_bit0 -x1499_bit0 x1500_bit0 x1501_bit0 -x1502_bit0 -x1503_bit0 -x1504_bit0 -x1505_bit0 -x1506_bit0 x1507_bit0 -x1508_bit0 -x1509_bit0 -x1511_bit0 -x1512_bit0 x1513_bit0 x1514_bit0 x1515_bit0 -x1516_bit0 x1517_bit0 -x1518_bit0 -x1519_bit0 -x1520_bit0 x1521_bit0 -x1522_bit0 -x1524_bit0 -x1525_bit0 -x1526_bit0 x1527_bit0 -x1528_bit0 -x1529_bit0 -x1530_bit0 -x1531_bit0 -x1532_bit0 -x1533_bit0 -x1534_bit0 -x1535_bit0 -x1536_bit0 -x1537_bit0 x1538_bit0 -x1539_bit0 x1540_bit0 -x1542_bit0 -x1543_bit0 -x1544_bit0 -x1545_bit0 -x1546_bit0 -x1547_bit0 -x1548_bit0 -x1549_bit0 -x1550_bit0 -x1551_bit0 -x1552_bit0 -x1553_bit0 -x1554_bit0 -x1555_bit0 x1556_bit0 -x1557_bit0 -x1558_bit0 -x1560_bit0 -x1561_bit0 -x1562_bit0 -x1563_bit0 -x1564_bit0 -x1565_bit0 -x1566_bit0 x1567_bit0 -x1568_bit0 -x1569_bit0 x1570_bit0 -x1571_bit0 -x1572_bit0 -x1573_bit0 -x1574_bit0 -x1575_bit0 -x1576_bit0 -x1578_bit0 -x1579_bit0 -x1580_bit0 -x1581_bit0 -x1582_bit0 -x1583_bit0 x1584_bit0 -x1585_bit0 -x1586_bit0 -x1587_bit0 -x1588_bit0 x1589_bit0 -x1591_bit0 -x1592_bit0 x1593_bit0 x1594_bit0 x1595_bit0 -x1596_bit0 -x1597_bit0 x1598_bit0 x1599_bit0 -x1600_bit0 -x1601_bit0 -x1602_bit0 -x1603_bit0 -x1604_bit0 -x1605_bit0 -x1606_bit0 -x1607_bit0 x1609_bit0 -x1610_bit0 -x1611_bit0 -x1612_bit0 x1613_bit0 x1614_bit0 x1615_bit0 -x1616_bit0 -x1617_bit0 -x1618_bit0 x1619_bit0 -x1620_bit0 -x1623_bit0 -x1624_bit0 x1625_bit0 -x1626_bit0 -x1627_bit0 -x1628_bit0 -x1631_bit0 x1634_bit0 -x1635_bit0 x1636_bit0 -x1637_bit0 -x1639_bit0 -x1640_bit0 -x1641_bit0 -x1642_bit0 -x1643_bit0 -x1644_bit0 -x1647_bit0 -x1648_bit0 -x1649_bit0 -x1650_bit0 -x1651_bit0 -x1652_bit0 x1653_bit0 -x1654_bit0 -x1655_bit0 x1656_bit0 -x1658_bit0 -x1659_bit0 x1660_bit0 x1663_bit0 -x1664_bit0 x1665_bit0 -x1666_bit0 -x1667_bit0 -x1668_bit0 x1669_bit0 -x1670_bit0 -x1671_bit0 -x1672_bit0 -x1673_bit0 x1675_bit0 x1678_bit0 -x1679_bit0 -x1680_bit0 -x1683_bit0 x1684_bit0 -x1685_bit0 -x1686_bit0 -x1687_bit0 -x1688_bit0 -x1690_bit0 -x1692_bit0 -x1694_bit0 -x1695_bit0 -x1696_bit0 -x1699_bit0 -x1700_bit0 -x1701_bit0 -x1702_bit0 -x1703_bit0 -x1704_bit0 -x1705_bit0 -x1708_bit0 -x1709_bit0 -x1710_bit0 -x1711_bit0 x1712_bit0 -x1713_bit0 x1714_bit0 -x1716_bit0 -x1719_bit0 -x1720_bit0 -x1721_bit0 -x1722_bit0 -x1723_bit0 -x1724_bit0 -x1725_bit0 -x1726_bit0 -x1727_bit0 -x1728_bit0 x1729_bit0 -x1732_bit0 -x1733_bit0 -x1734_bit0 -x1735_bit0 -x1736_bit0 -x1737_bit0 x1738_bit0 -x1739_bit0 -x1740_bit0 x1741_bit0 -x1742_bit0 -x1743_bit0 -x1744_bit0 x1745_bit0 -x1748_bit0 -x1749_bit0 x1750_bit0 x1751_bit0 -x1752_bit0 -x1753_bit0 x1754_bit0 -x1755_bit0 -x1756_bit0 -x1757_bit0 -x1758_bit0 x1760_bit0 -x1763_bit0 -x1764_bit0 -x1765_bit0 x1766_bit0 -x1768_bit0 x1769_bit0 -x1770_bit0 -x1771_bit0 -x1772_bit0 x1773_bit0 x1775_bit0 -x1776_bit0 -x1777_bit0 -x1779_bit0 x1780_bit0 x1781_bit0 x1782_bit0 x1783_bit0 -x1784_bit0 -x1785_bit0 -x1786_bit0 -x1787_bit0 x1788_bit0 -x1789_bit0 -x1790_bit0 -x1793_bit0 -x1794_bit0 -x1795_bit0 -x1796_bit0 -x1797_bit0 -x1798_bit0 -x1799_bit0 x1801_bit0 -x1804_bit0 -x1805_bit0 -x1806_bit0 x1807_bit0 -x1808_bit0 -x1809_bit0 x1810_bit0 -x1811_bit0 -x1812_bit0 -x1813_bit0 x1814_bit0 x1817_bit0 -x1818_bit0 -x1819_bit0 -x1820_bit0 -x1821_bit0 -x1822_bit0 -x1823_bit0 -x1824_bit0 -x1825_bit0 -x1826_bit0 -x1827_bit0 -x1828_bit0 -x1829_bit0 -x1830_bit0 -x1833_bit0 -x1834_bit0 -x1835_bit0 -x1836_bit0 -x1837_bit0 -x1838_bit0 -x1839_bit0 -x1840_bit0 -x1841_bit0 -x1842_bit0 -x1843_bit0 -x1845_bit0 x1848_bit0 -x1849_bit0 -x1850_bit0 -x1851_bit0 -x1852_bit0 -x1853_bit0 x1854_bit0 -x1855_bit0 -x1856_bit0 -x1857_bit0 x1858_bit0 -x1859_bit0 -x1860_bit0 -x1861_bit0 x1862_bit0 -x1864_bit0 -x1865_bit0 x1866_bit0 -x1867_bit0 -x1868_bit0 -x1869_bit0 x1870_bit0 -x1871_bit0 -x1872_bit0 -x1873_bit0 -x1874_bit0 -x1875_bit0 -x1878_bit0 -x1879_bit0 -x1880_bit0 x1881_bit0 -x1882_bit0 -x1883_bit0 -x1884_bit0 -x1885_bit0 -x1886_bit0 -x1889_bit0 -x1890_bit0 x1891_bit0 -x1892_bit0 -x1893_bit0 x1894_bit0 x1895_bit0 -x1896_bit0 -x1897_bit0 -x1898_bit0 -x1899_bit0 x1902_bit0 -x1903_bit0 -x1904_bit0 -x1905_bit0 x1906_bit0 -x1907_bit0 -x1908_bit0 -x1909_bit0 -x1910_bit0 -x1911_bit0 x1912_bit0 -x1913_bit0 -x1914_bit0 -x1915_bit0 -x1918_bit0 -x1919_bit0 -x1920_bit0 -x1921_bit0 -x1922_bit0 x1923_bit0 -x1924_bit0 -x1925_bit0 -x1926_bit0 -x1927_bit0 x1928_bit0 -x1929_bit0 -x1930_bit0 -x1933_bit0 x1934_bit0 x1935_bit0 -x1936_bit0 x1937_bit0 -x1938_bit0 x1939_bit0 -x1940_bit0 -x1941_bit0 -x1942_bit0 -x1943_bit0 x1944_bit0 x1945_bit0 -x1946_bit0 -x1947_bit0 x1949_bit0 -x1950_bit0 -x1951_bit0 x1952_bit0 x1953_bit0 -x1954_bit0 x1955_bit0 -x1956_bit0 -x1957_bit0 -x1958_bit0 -x1959_bit0 -x1960_bit0 -x1961_bit0 -x1962_bit0 -x1963_bit0 -x1966_bit0 -x1967_bit0 -x1968_bit0 -x1969_bit0 -x1970_bit0 -x1971_bit0 -x1972_bit0 -x1973_bit0 -x1974_bit0 -x1975_bit0 -x1976_bit0 -x1977_bit0 -x1980_bit0 -x1981_bit0 -x1982_bit0 -x1983_bit0 -x1984_bit0 -x1985_bit0 x1986_bit0 -x1987_bit0 -x1988_bit0 -x1989_bit0 -x1990_bit0 x1991_bit0 -x1992_bit0 -x1993_bit0 -x1994_bit0 -x1995_bit0 -x1996_bit0 -x1997_bit0 -x1998_bit0 x1999_bit0 -x2000_bit0 -x2001_bit0 -x2003_bit0 -x2004_bit0 x2005_bit0 -x2006_bit0 -x2007_bit0 -x2008_bit0 x2009_bit0 -x2010_bit0 -x2011_bit0 -x2012_bit0 -x2013_bit0 x2014_bit0 -x2015_bit0 -x2016_bit0 x2017_bit0 -x2018_bit0 -x2019_bit0 -x2020_bit0 -x2021_bit0 x2022_bit0 x2023_bit0 -x2024_bit0 -x2025_bit0 -x2027_bit0 -x2028_bit0 -x2029_bit0 -x2030_bit0 -x2031_bit0 -x2032_bit0 x2033_bit0 -x2034_bit0 -x2035_bit0 x2038_bit0 x2040_bit0 -x2041_bit0 -x2042_bit0 -x2043_bit0 -x2045_bit0 x2046_bit0 -x2047_bit0 -x2048_bit0 x2049_bit0 -x2050_bit0 -x2051_bit0 -x2053_bit0 x2054_bit0 x2055_bit0 x2056_bit0 x2057_bit0 -x2058_bit0 x2059_bit0 -x2060_bit0 -x2061_bit0 -x2062_bit0 -x2064_bit0 -x2066_bit0 -x2067_bit0 x2068_bit0 -x2071_bit0 -x2072_bit0 -x2073_bit0 -x2074_bit0 -x2075_bit0 -x2076_bit0 -x2077_bit0 -x2078_bit0 -x2080_bit0 -x2081_bit0 -x2082_bit0 x2083_bit0 x2084_bit0 -x2085_bit0 -x2086_bit0 -x2087_bit0 -x2088_bit0 -x2089_bit0 -x2090_bit0 -x2091_bit0 -x2092_bit0 x2094_bit0 x2095_bit0 -x2096_bit0 -x2097_bit0 -x2098_bit0 -x2099_bit0 x2100_bit0 -x2101_bit0 -x2102_bit0 x2105_bit0 x2107_bit0 -x2108_bit0 -x2109_bit0 -x2110_bit0 -x2112_bit0 x2113_bit0 -x2114_bit0 -x2115_bit0 -x2116_bit0 x2117_bit0 -x2118_bit0 -x2120_bit0 -x2121_bit0 -x2122_bit0 -x2123_bit0 x2124_bit0 -x2125_bit0 -x2126_bit0 -x2127_bit0 -x2128_bit0 -x2129_bit0 x2131_bit0 -x2133_bit0 x2134_bit0 -x2135_bit0 -x2138_bit0 -x2139_bit0 x2140_bit0 -x2141_bit0 -x2142_bit0 x2143_bit0 -x2144_bit0 x2145_bit0 x2147_bit0 x2148_bit0 -x2149_bit0 x2150_bit0 -x2151_bit0 -x2152_bit0 x2153_bit0 -x2154_bit0 -x2155_bit0 -x2156_bit0 -x2157_bit0 -x2158_bit0 -x2159_bit0 -x2161_bit0 -x2162_bit0 -x2163_bit0 -x2164_bit0 -x2165_bit0 -x2166_bit0 x2167_bit0 -x2168_bit0 -x2169_bit0 x2170_bit0 -x2172_bit0 -x2174_bit0 -x2175_bit0 -x2176_bit0 -x2177_bit0 -x2178_bit0 -x2179_bit0 x2180_bit0 -x2181_bit0 -x2182_bit0 -x2183_bit0 -x2184_bit0 -x2185_bit0 -x2187_bit0 -x2188_bit0 -x2189_bit0 -x2190_bit0 x2191_bit0 -x2192_bit0 -x2193_bit0 -x2194_bit0 -x2195_bit0 -x2196_bit0 -x2198_bit0 x2200_bit0 -x2201_bit0 -x2202_bit0 -x2203_bit0 -x2204_bit0 -x2205_bit0 x2206_bit0 -x2207_bit0 -x2208_bit0 x2209_bit0 -x2210_bit0 -x2211_bit0 -x2212_bit0 x2214_bit0 -x2215_bit0 x2216_bit0 -x2217_bit0 -x2218_bit0 -x2219_bit0 x2220_bit0 -x2221_bit0 -x2222_bit0 -x2223_bit0 -x2224_bit0 -x2225_bit0 -x2226_bit0 -x2228_bit0 -x2229_bit0 -x2230_bit0 -x2231_bit0 -x2232_bit0 -x2233_bit0 x2234_bit0 -x2235_bit0 -x2236_bit0 -x2237_bit0 -x2239_bit0 -x2241_bit0 -x2242_bit0 -x2243_bit0 -x2244_bit0 x2245_bit0 -x2246_bit0 x2247_bit0 -x2248_bit0 -x2249_bit0 -x2250_bit0 -x2251_bit0 -x2252_bit0 x2254_bit0 -x2255_bit0 x2256_bit0 -x2257_bit0 -x2258_bit0 -x2259_bit0 x2260_bit0 -x2261_bit0 -x2262_bit0 -x2263_bit0 x2265_bit0 -x2267_bit0 x2268_bit0 -x2269_bit0 -x2270_bit0 -x2271_bit0 -x2272_bit0 x2273_bit0 -x2274_bit0 -x2275_bit0 -x2276_bit0 -x2277_bit0 -x2278_bit0 -x2279_bit0 x2281_bit0 -x2282_bit0 -x2283_bit0 -x2284_bit0 -x2285_bit0 -x2286_bit0 -x2287_bit0 x2288_bit0 -x2289_bit0 x2290_bit0 x2291_bit0 x2292_bit0 -x2293_bit0 x2295_bit0 -x2296_bit0 x2297_bit0 -x2298_bit0 x2299_bit0 -x2300_bit0 -x2301_bit0 -x2302_bit0 -x2303_bit0 -x2306_bit0 -x2308_bit0 -x2309_bit0 -x2310_bit0 -x2311_bit0 -x2313_bit0 -x2314_bit0 x2315_bit0 -x2316_bit0 -x2317_bit0 -x2318_bit0 x2319_bit0 -x2321_bit0 -x2322_bit0 -x2323_bit0 -x2324_bit0 -x2325_bit0 -x2326_bit0 x2327_bit0 -x2328_bit0 -x2329_bit0 x2330_bit0 x2332_bit0 x2334_bit0 -x2335_bit0 -x2336_bit0 -x2337_bit0 -x2339_bit0 -x2340_bit0 -x2341_bit0 -x2342_bit0 -x2343_bit0 -x2345_bit0 -x2346_bit0 -x2348_bit0 -x2349_bit0 -x2350_bit0 -x2351_bit0 -x2352_bit0 -x2353_bit0 x2354_bit0 -x2355_bit0 -x2356_bit0 -x2357_bit0 -x2358_bit0 -x2359_bit0 -x2360_bit0 x2362_bit0 -x2363_bit0 -x2364_bit0 x2365_bit0 x2366_bit0 -x2367_bit0 x2368_bit0 -x2369_bit0 -x2370_bit0 x2373_bit0 x2375_bit0 -x2376_bit0 -x2377_bit0 x2378_bit0 -x2380_bit0 x2381_bit0 -x2382_bit0 -x2383_bit0 -x2384_bit0 x2385_bit0 -x2386_bit0 -x2388_bit0 -x2389_bit0 -x2390_bit0 -x2391_bit0 -x2392_bit0 -x2393_bit0 x2394_bit0 -x2395_bit0 -x2396_bit0 -x2397_bit0 x2399_bit0 x2401_bit0 -x2402_bit0 -x2403_bit0 -x2404_bit0 -x2406_bit0 x2407_bit0 -x2408_bit0 -x2409_bit0 -x2410_bit0 x2411_bit0 -x2412_bit0 -x2413_bit0 -x2415_bit0 -x2416_bit0 -x2417_bit0 -x2418_bit0 -x2419_bit0 -x2420_bit0 x2421_bit0 -x2422_bit0 -x2423_bit0 -x2424_bit0 x2425_bit0 -x2426_bit0 -x2427_bit0 -x2428_bit0 x2429_bit0 -x2430_bit0 -x2432_bit0 -x2433_bit0 -x2434_bit0 -x2435_bit0 x2436_bit0 -x2437_bit0 -x2438_bit0 -x2439_bit0 -x2440_bit0 -x2441_bit0 -x2442_bit0 -x2443_bit0 -x2444_bit0 -x2445_bit0 -x2446_bit0 -x2448_bit0 -x2449_bit0 -x2450_bit0 x2451_bit0 -x2452_bit0 -x2453_bit0 -x2454_bit0 -x2455_bit0 -x2456_bit0 -x2457_bit0 -x2458_bit0 -x2459_bit0 x2460_bit0 -x2461_bit0 -x2462_bit0 -x2463_bit0 -x2464_bit0 -x2466_bit0 -x2467_bit0 -x2468_bit0 -x2469_bit0 -x2470_bit0 -x2471_bit0 x2472_bit0 -x2473_bit0 -x2474_bit0 -x2475_bit0 -x2476_bit0 -x2477_bit0 -x2478_bit0 -x2479_bit0 -x2480_bit0 -x2481_bit0 x2483_bit0 x2484_bit0 x2485_bit0 x2486_bit0 x2487_bit0 x2488_bit0 -x2489_bit0 -x2490_bit0 -x2491_bit0 -x2492_bit0 -x2493_bit0 -x2494_bit0 x2495_bit0 -x2496_bit0 x2497_bit0 x2499_bit0 -x2500_bit0 x2501_bit0 -x2502_bit0 x2503_bit0 -x2504_bit0 -x2505_bit0 x2506_bit0 -x2507_bit0 -x2508_bit0 -x2509_bit0 x2510_bit0 -x2511_bit0 -x2512_bit0 -x2513_bit0 -x2514_bit0 x2515_bit0 x2517_bit0 -x2518_bit0 x2519_bit0 -x2520_bit0 -x2521_bit0 -x2522_bit0 -x2523_bit0 -x2524_bit0 -x2526_bit0 x2527_bit0 x2528_bit0 -x2529_bit0 -x2530_bit0 x2531_bit0 -x2532_bit0 -x2534_bit0 -x2535_bit0 -x2536_bit0 x2537_bit0 -x2538_bit0 -x2539_bit0 -x2540_bit0 -x2541_bit0 -x2542_bit0 -x2544_bit0 x2545_bit0 x2546_bit0 -x2547_bit0 x2548_bit0 x2549_bit0 -x2550_bit0 x2551_bit0 x2552_bit0 x2553_bit0 x2554_bit0 x2555_bit0 x2556_bit0 x2557_bit0 x2558_bit0 x2559_bit0 x2560_bit0 x2561_bit0 x2562_bit0 x2563_bit0 x2564_bit0 -x2565_bit0 -x2566_bit0 -x2567_bit0 -x7_bit0 x8_bit0 -x12_bit0 -x13_bit0 -x15_bit0 -x16_bit0 -x18_bit0 -x25_bit0 -x26_bit0 -x28_bit0 x40_bit0 -x41_bit0 -x43_bit0 -x52_bit0 -x53_bit0 -x55_bit0 -x63_bit0 x64_bit0 x69_bit0 -x71_bit0 x72_bit0 -x81_bit0 -x82_bit0 -x84_bit0 -x96_bit0 -x97_bit0 -x99_bit0 -x108_bit0 -x109_bit0 -x111_bit0 -x118_bit0 -x125_bit0 x130_bit0 -x138_bit0 -x146_bit0 x147_bit0 -x151_bit0 x152_bit0 -x154_bit0 -x155_bit0 x157_bit0 -x164_bit0 -x165_bit0 -x167_bit0 -x179_bit0 -x180_bit0 x182_bit0 -x191_bit0 -x192_bit0 x194_bit0 -x202_bit0 -x203_bit0 -x208_bit0 -x210_bit0 -x211_bit0 -x220_bit0 -x221_bit0 -x223_bit0 -x235_bit0 -x236_bit0 -x238_bit0 -x247_bit0 -x248_bit0 -x250_bit0 -x257_bit0 -x264_bit0 x269_bit0 x277_bit0 -x282_bit0 -x287_bit0 -x288_bit0 x301_bit0 -x302_bit0 -x311_bit0 -x312_bit0 -x324_bit0 -x325_bit0 -x334_bit0 -x336_bit0 -x337_bit0 -x342_bit0 -x346_bit0 -x350_bit0 -x355_bit0 -x364_bit0 -x365_bit0 -x378_bit0 -x379_bit0 -x388_bit0 -x389_bit0 -x401_bit0 -x402_bit0 -x413_bit0 -x414_bit0 -x427_bit0 x455_bit0 x462_bit0 -x477_bit0 -x478_bit0 -x487_bit0 -x488_bit0 -x504_bit0 -x505_bit0 -x518_bit0 -x520_bit0 -x521_bit0 -x534_bit0 -x547_bit0 -x548_bit0 -x557_bit0 -x558_bit0 -x574_bit0 -x575_bit0 -x590_bit0 x591_bit0 -x604_bit0 -x632_bit0 -x649_bit0 -x654_bit0 -x655_bit0 -x664_bit0 -x665_bit0 -x681_bit0 -x682_bit0 x695_bit0 -x697_bit0 x698_bit0 -x711_bit0 -x724_bit0 x725_bit0 -x734_bit0 -x735_bit0 -x751_bit0 -x752_bit0 x767_bit0 -x768_bit0 -x781_bit0 -x794_bit0 -x795_bit0 -x801_bit0 -x802_bit0 x803_bit0 -x804_bit0 -x805_bit0 -x806_bit0 -x807_bit0 x808_bit0 x809_bit0 -x810_bit0 -x811_bit0 x819_bit0 -x820_bit0 -x826_bit0 -x827_bit0 x828_bit0 -x830_bit0 x831_bit0 -x832_bit0 -x834_bit0 -x835_bit0 x836_bit0 -x844_bit0 x845_bit0 -x852_bit0 -x853_bit0 -x855_bit0 -x857_bit0 -x858_bit0 -x859_bit0 -x861_bit0 -x862_bit0 -x863_bit0 -x866_bit0 -x868_bit0 -x869_bit0 x874_bit0 -x881_bit0 -x894_bit0 -x895_bit0 x901_bit0 -x902_bit0 x903_bit0 -x905_bit0 x906_bit0 -x907_bit0 -x909_bit0 x910_bit0 -x911_bit0 -x919_bit0 -x920_bit0 -x927_bit0 x928_bit0 x930_bit0 -x931_bit0 -x932_bit0 -x934_bit0 -x935_bit0 x936_bit0 -x944_bit0 -x945_bit0 -x953_bit0 -x957_bit0 -x958_bit0 -x963_bit0 x966_bit0 -x968_bit0 -x969_bit0 -x981_bit0 -x998_bit0 -x999_bit0 -x1006_bit0 -x1007_bit0 -x1009_bit0 -x1010_bit0 -x1015_bit0 -x1027_bit0 -x1028_bit0 x1044_bit0 x1046_bit0 -x1047_bit0 -x1068_bit0 -x1069_bit0 -x1089_bit0 -x1090_bit0 -x1104_bit0 -x1105_bit0 -x1125_bit0 -x1142_bit0 -x1143_bit0 -x1150_bit0 -x1151_bit0 -x1153_bit0 -x1154_bit0 -x1159_bit0 -x1171_bit0 -x1172_bit0 -x1188_bit0 -x1190_bit0 -x1191_bit0 -x1212_bit0 x1213_bit0 -x1233_bit0 -x1234_bit0 -x1248_bit0 x1249_bit0 -x1269_bit0 -x1347_bit0 -x1350_bit0 -x1368_bit0 x1383_bit0 -x1385_bit0 x1388_bit0 x1389_bit0 x1390_bit0 x1400_bit0 x1403_bit0 -x1421_bit0 -x1439_bit0 -x1454_bit0 x1456_bit0 -x1474_bit0 -x1492_bit0 x1510_bit0 -x1523_bit0 -x1541_bit0 -x1559_bit0 -x1577_bit0 -x1590_bit0 -x1608_bit0 -x1621_bit0 -x1622_bit0 -x1629_bit0 x1630_bit0 x1632_bit0 -x1633_bit0 -x1638_bit0 x1645_bit0 -x1646_bit0 x1657_bit0 -x1661_bit0 -x1662_bit0 x1674_bit0 -x1676_bit0 -x1677_bit0 x1681_bit0 -x1682_bit0 x1689_bit0 -x1691_bit0 -x1693_bit0 -x1697_bit0 -x1698_bit0 -x1706_bit0 -x1707_bit0 -x1715_bit0 -x1717_bit0 -x1718_bit0 -x1730_bit0 -x1731_bit0 -x1746_bit0 x1747_bit0 x1759_bit0 -x1761_bit0 -x1762_bit0 x1767_bit0 -x1774_bit0 x1778_bit0 x1791_bit0 -x1792_bit0 -x1800_bit0 -x1802_bit0 -x1803_bit0 -x1815_bit0 -x1816_bit0 x1831_bit0 -x1832_bit0 -x1844_bit0 -x1846_bit0 -x1847_bit0 x1863_bit0 -x1876_bit0 -x1877_bit0 -x1887_bit0 -x1888_bit0 -x1900_bit0 -x1901_bit0 -x1916_bit0 -x1917_bit0 -x1931_bit0 -x1932_bit0 x1948_bit0 -x1964_bit0 -x1965_bit0 -x1978_bit0 -x1979_bit0 x2002_bit0 -x2026_bit0 x2036_bit0 -x2037_bit0 -x2039_bit0 x2044_bit0 -x2052_bit0 x2063_bit0 x2065_bit0 -x2069_bit0 -x2070_bit0 -x2079_bit0 -x2093_bit0 -x2103_bit0 -x2104_bit0 -x2106_bit0 x2111_bit0 -x2119_bit0 -x2130_bit0 -x2132_bit0 -x2136_bit0 x2137_bit0 -x21#### 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.76 0.94 0.92 1/54 20551
Raw data (stat): 20551 (runsolver) D 20550 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 491202262 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.80 0.94 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 5002 0 0 0 979 13 0 0 25 0 1 0 491202262 23023616 4819 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5621 4819 603 41 0 5580 0
vsize: 22484
[startup+20.0017 s]
Raw data (loadavg): 0.83 0.94 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 5277 0 0 0 1978 14 0 0 25 0 1 0 491202262 24244224 5094 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5094 603 41 0 5878 0
vsize: 23676
[startup+30.0021 s]
Raw data (loadavg): 0.85 0.94 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 5618 0 0 0 2977 15 0 0 25 0 1 0 491202262 25714688 5435 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6278 5435 603 41 0 6237 0
vsize: 25112
[startup+40.003 s]
Raw data (loadavg): 0.88 0.94 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 5909 0 0 0 3975 17 0 0 25 0 1 0 491202262 26791936 5726 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6541 5726 603 41 0 6500 0
vsize: 26164
[startup+50.0045 s]
Raw data (loadavg): 0.89 0.94 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 6271 0 0 0 4974 18 0 0 25 0 1 0 491202262 28278784 6088 4294967295 134512640 134672761 3221224544 3221223668 134566095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6904 6088 603 41 0 6863 0
vsize: 27616
[startup+60.0047 s]
Raw data (loadavg): 0.91 0.94 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 6733 0 0 0 5972 20 0 0 25 0 1 0 491202262 30429184 6550 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7429 6550 603 41 0 7388 0
vsize: 29716
[startup+70.0055 s]
Raw data (loadavg): 0.92 0.95 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 7098 0 0 0 6971 22 0 0 25 0 1 0 491202262 31776768 6915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7758 6915 603 41 0 7717 0
vsize: 31032
[startup+80.0069 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 7363 0 0 0 7969 23 0 0 25 0 1 0 491202262 32845824 7180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8019 7180 603 41 0 7978 0
vsize: 32076
[startup+90.0072 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 7743 0 0 0 8968 24 0 0 25 0 1 0 491202262 34451456 7560 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7560 603 41 0 8370 0
vsize: 33644
[startup+100.007 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 8052 0 0 0 9967 26 0 0 25 0 1 0 491202262 35663872 7869 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8707 7869 603 41 0 8666 0
vsize: 34828
[startup+110.008 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 8551 0 0 0 10966 27 0 0 25 0 1 0 491202262 37670912 8368 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9197 8368 603 41 0 9156 0
vsize: 36788
[startup+120.009 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 8915 0 0 0 11964 29 0 0 25 0 1 0 491202262 39669760 8732 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9685 8732 603 41 0 9644 0
vsize: 38740
[startup+130.009 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 9085 0 0 0 12963 30 0 0 25 0 1 0 491202262 40341504 8902 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9849 8902 603 41 0 9808 0
vsize: 39396
[startup+140.01 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 9308 0 0 0 13963 31 0 0 25 0 1 0 491202262 41152512 9125 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10047 9125 603 41 0 10006 0
vsize: 40188
[startup+150.01 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 9568 0 0 0 14961 33 0 0 25 0 1 0 491202262 42225664 9385 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10309 9385 603 41 0 10268 0
vsize: 41236
[startup+160.01 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 9879 0 0 0 15959 34 0 0 25 0 1 0 491202262 43438080 9696 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10605 9696 603 41 0 10564 0
vsize: 42420
[startup+170.015 s]
Raw data (loadavg): 0.98 0.96 0.92 4/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 10299 0 0 0 16958 37 0 0 25 0 1 0 491202262 45051904 10116 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10999 10116 603 41 0 10958 0
vsize: 43996
[startup+180.015 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 10521 0 0 0 17958 37 0 0 25 0 1 0 491202262 45993984 10338 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11229 10338 603 41 0 11188 0
vsize: 44916
[startup+190.016 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 10814 0 0 0 18958 37 0 0 25 0 1 0 491202262 47202304 10631 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11524 10631 603 41 0 11483 0
vsize: 46096
[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 11242 0 0 0 19957 38 0 0 25 0 1 0 491202262 48824320 11059 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11920 11059 603 41 0 11879 0
vsize: 47680
[startup+210.015 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 11460 0 0 0 20957 38 0 0 25 0 1 0 491202262 49770496 11277 4294967295 134512640 134672761 3221224544 3221223648 134555126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12151 11277 603 41 0 12110 0
vsize: 48604
[startup+220.016 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 11681 0 0 0 21956 39 0 0 25 0 1 0 491202262 50577408 11498 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12348 11498 603 41 0 12307 0
vsize: 49392
[startup+230.017 s]
Raw data (loadavg): 0.99 0.96 0.92 3/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 11853 0 0 0 22956 40 0 0 25 0 1 0 491202262 51249152 11670 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12512 11670 603 41 0 12471 0
vsize: 50048
[startup+240.017 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 11984 0 0 0 23955 40 0 0 25 0 1 0 491202262 51781632 11801 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12642 11801 603 41 0 12601 0
vsize: 50568
[startup+250.017 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 12187 0 0 0 24955 41 0 0 25 0 1 0 491202262 52600832 12004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12842 12004 603 41 0 12801 0
vsize: 51368
[startup+260.017 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 12379 0 0 0 25954 42 0 0 25 0 1 0 491202262 53403648 12196 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13038 12196 603 41 0 12997 0
vsize: 52152
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 12943 0 0 0 26952 44 0 0 25 0 1 0 491202262 55689216 12760 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13596 12760 603 41 0 13555 0
vsize: 54384
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 13608 0 0 0 27951 46 0 0 25 0 1 0 491202262 58380288 13425 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14253 13425 603 41 0 14212 0
vsize: 57012
[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 13788 0 0 0 28950 46 0 0 25 0 1 0 491202262 59043840 13605 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14415 13605 603 41 0 14374 0
vsize: 57660
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 13941 0 0 0 29950 47 0 0 25 0 1 0 491202262 60764160 13758 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14835 13758 603 41 0 14794 0
vsize: 59340
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 14075 0 0 0 30950 47 0 0 25 0 1 0 491202262 61300736 13892 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14966 13892 603 41 0 14925 0
vsize: 59864
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15322 0 0 0 31948 49 0 0 25 0 1 0 491202262 66514944 15139 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15139 603 41 0 16198 0
vsize: 64956
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15324 0 0 0 32947 49 0 0 25 0 1 0 491202262 66514944 15141 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15141 603 41 0 16198 0
vsize: 64956
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15324 0 0 0 33948 49 0 0 25 0 1 0 491202262 66514944 15141 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15141 603 41 0 16198 0
vsize: 64956
[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15324 0 0 0 34949 49 0 0 25 0 1 0 491202262 66514944 15141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15141 603 41 0 16198 0
vsize: 64956
[startup+360.133 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15324 0 0 0 35959 49 0 0 25 0 1 0 491202262 66514944 15141 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15141 603 41 0 16198 0
vsize: 64956
[startup+370.133 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15324 0 0 0 36959 49 0 0 25 0 1 0 491202262 66514944 15141 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15141 603 41 0 16198 0
vsize: 64956
[startup+380.133 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15325 0 0 0 37959 49 0 0 25 0 1 0 491202262 66514944 15142 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15142 603 41 0 16198 0
vsize: 64956
[startup+390.159 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15325 0 0 0 38962 49 0 0 25 0 1 0 491202262 66514944 15142 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15142 603 41 0 16198 0
vsize: 64956
[startup+400.184 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 39965 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+410.184 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 40965 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+420.185 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 41965 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+430.185 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 42965 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+440.186 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 43966 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+450.186 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 44966 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+460.186 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 45966 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+470.19 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 46967 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+480.19 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 47967 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+490.19 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 48967 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+500.191 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 49967 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+510.191 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 50967 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+520.191 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 51967 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+530.191 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 52968 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+540.192 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 53968 49 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+550.192 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 54968 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+560.192 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 55968 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+570.192 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 56968 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+580.192 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 57968 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+590.193 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 58969 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+600.193 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 59969 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+610.193 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 60969 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+620.193 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 61969 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+630.193 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 62969 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+640.193 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 63969 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+650.194 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 64970 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+660.193 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 65970 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223612 1075346603 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+670.193 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 66970 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+680.193 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 67970 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+690.194 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 68970 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+700.194 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 69970 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+710.194 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 70969 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+720.194 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 71969 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+730.194 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 72970 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+740.195 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 73970 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+750.196 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 74970 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+760.196 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 15329 0 0 0 75970 50 0 0 25 0 1 0 491202262 66514944 15146 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+770.196 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 16118 0 0 0 76967 53 0 0 25 0 1 0 491202262 69750784 15935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17029 15935 603 41 0 16988 0
vsize: 68116
[startup+780.197 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 16783 0 0 0 77966 55 0 0 25 0 1 0 491202262 72441856 16600 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17686 16600 603 41 0 17645 0
vsize: 70744
[startup+790.197 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 17127 0 0 0 78965 56 0 0 25 0 1 0 491202262 73912320 16944 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18045 16944 603 41 0 18004 0
vsize: 72180
[startup+800.197 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 17237 0 0 0 79965 56 0 0 25 0 1 0 491202262 74313728 17054 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18143 17054 603 41 0 18102 0
vsize: 72572
[startup+810.197 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 17352 0 0 0 80965 56 0 0 25 0 1 0 491202262 74719232 17169 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18242 17169 603 41 0 18201 0
vsize: 72968
[startup+820.198 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 17437 0 0 0 81965 57 0 0 25 0 1 0 491202262 75124736 17254 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18341 17254 603 41 0 18300 0
vsize: 73364
[startup+830.198 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 17529 0 0 0 82965 57 0 0 25 0 1 0 491202262 75395072 17346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18407 17346 603 41 0 18366 0
vsize: 73628
[startup+840.199 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 17649 0 0 0 83965 57 0 0 25 0 1 0 491202262 75935744 17466 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18539 17466 603 41 0 18498 0
vsize: 74156
[startup+850.2 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 17759 0 0 0 84965 57 0 0 25 0 1 0 491202262 76337152 17576 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18637 17576 603 41 0 18596 0
vsize: 74548
[startup+860.199 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 17874 0 0 0 85965 58 0 0 25 0 1 0 491202262 76738560 17691 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18735 17691 603 41 0 18694 0
vsize: 74940
[startup+870.199 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 17984 0 0 0 86965 58 0 0 25 0 1 0 491202262 77279232 17801 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18867 17801 603 41 0 18826 0
vsize: 75468
[startup+880.199 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 18048 0 0 0 87965 58 0 0 25 0 1 0 491202262 77545472 17865 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18932 17865 603 41 0 18891 0
vsize: 75728
[startup+890.2 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 18141 0 0 0 88964 58 0 0 25 0 1 0 491202262 77815808 17958 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18998 17958 603 41 0 18957 0
vsize: 75992
[startup+900.201 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 18235 0 0 0 89964 59 0 0 25 0 1 0 491202262 78221312 18052 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19097 18052 603 41 0 19056 0
vsize: 76388
[startup+910.201 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 18559 0 0 0 90963 60 0 0 25 0 1 0 491202262 79568896 18376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19426 18376 603 41 0 19385 0
vsize: 77704
[startup+920.202 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 18637 0 0 0 91963 60 0 0 25 0 1 0 491202262 79839232 18454 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19492 18454 603 41 0 19451 0
vsize: 77968
[startup+930.202 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 18734 0 0 0 92962 61 0 0 25 0 1 0 491202262 80244736 18551 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19591 18551 603 41 0 19550 0
vsize: 78364
[startup+940.202 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 18851 0 0 0 93962 61 0 0 25 0 1 0 491202262 80773120 18668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19720 18668 603 41 0 19679 0
vsize: 78880
[startup+950.202 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 19214 0 0 0 94960 63 0 0 25 0 1 0 491202262 82247680 19031 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19031 603 41 0 20039 0
vsize: 80320
[startup+960.203 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 19830 0 0 0 95959 65 0 0 25 0 1 0 491202262 84676608 19647 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20673 19647 603 41 0 20632 0
vsize: 82692
[startup+970.203 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 20434 0 0 0 96957 67 0 0 25 0 1 0 491202262 87117824 20251 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21269 20251 603 41 0 21228 0
vsize: 85076
[startup+980.203 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 20955 0 0 0 97955 69 0 0 25 0 1 0 491202262 89272320 20772 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21795 20772 603 41 0 21754 0
vsize: 87180
[startup+990.204 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 21480 0 0 0 98954 70 0 0 25 0 1 0 491202262 91443200 21297 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22325 21297 603 41 0 22284 0
vsize: 89300
[startup+1000.2 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 21905 0 0 0 99953 71 0 0 25 0 1 0 491202262 93192192 21722 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22752 21722 603 41 0 22711 0
vsize: 91008
[startup+1010.2 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 22345 0 0 0 100952 72 0 0 25 0 1 0 491202262 94941184 22162 4294967295 134512640 134672761 3221224544 3221223680 134560585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23179 22162 603 41 0 23138 0
vsize: 92716
[startup+1020.2 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 22753 0 0 0 101951 74 0 0 25 0 1 0 491202262 96579584 22570 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23579 22570 603 41 0 23538 0
vsize: 94316
[startup+1030.2 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 22995 0 0 0 102951 74 0 0 25 0 1 0 491202262 97665024 22812 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23844 22812 603 41 0 23803 0
vsize: 95376
[startup+1040.2 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 23104 0 0 0 103950 75 0 0 25 0 1 0 491202262 98070528 22921 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23943 22921 603 41 0 23902 0
vsize: 95772
[startup+1050.2 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 23292 0 0 0 104950 75 0 0 25 0 1 0 491202262 98738176 23109 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24106 23109 603 41 0 24065 0
vsize: 96424
[startup+1060.2 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 23477 0 0 0 105950 76 0 0 25 0 1 0 491202262 99549184 23294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24304 23294 603 41 0 24263 0
vsize: 97216
[startup+1070.2 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 23648 0 0 0 106949 76 0 0 25 0 1 0 491202262 100225024 23465 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24469 23465 603 41 0 24428 0
vsize: 97876
[startup+1080.2 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 23751 0 0 0 107949 77 0 0 25 0 1 0 491202262 100630528 23568 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24568 23568 603 41 0 24527 0
vsize: 98272
[startup+1090.21 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 23876 0 0 0 108949 77 0 0 25 0 1 0 491202262 101167104 23693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24699 23693 603 41 0 24658 0
vsize: 98796
[startup+1100.21 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 24014 0 0 0 109948 78 0 0 25 0 1 0 491202262 101707776 23831 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24831 23831 603 41 0 24790 0
vsize: 99324
[startup+1110.21 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 24119 0 0 0 110948 79 0 0 25 0 1 0 491202262 102113280 23936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24930 23936 603 41 0 24889 0
vsize: 99720
[startup+1120.21 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 24229 0 0 0 111948 79 0 0 25 0 1 0 491202262 102518784 24046 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25029 24046 603 41 0 24988 0
vsize: 100116
[startup+1130.21 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 24286 0 0 0 112948 79 0 0 25 0 1 0 491202262 102785024 24103 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25094 24103 603 41 0 25053 0
vsize: 100376
[startup+1140.21 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 24492 0 0 0 113947 80 0 0 25 0 1 0 491202262 103608320 24309 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25295 24309 603 41 0 25254 0
vsize: 101180
[startup+1150.22 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 24601 0 0 0 114948 81 0 0 25 0 1 0 491202262 104009728 24418 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25393 24418 603 41 0 25352 0
vsize: 101572
[startup+1160.22 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 24674 0 0 0 115948 81 0 0 25 0 1 0 491202262 104280064 24491 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25459 24491 603 41 0 25418 0
vsize: 101836
[startup+1170.23 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 24901 0 0 0 116948 82 0 0 25 0 1 0 491202262 105222144 24718 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25689 24718 603 41 0 25648 0
vsize: 102756
[startup+1180.23 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 25136 0 0 0 117947 83 0 0 25 0 1 0 491202262 106168320 24953 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25920 24953 603 41 0 25879 0
vsize: 103680
[startup+1190.23 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 25244 0 0 0 118947 83 0 0 25 0 1 0 491202262 106573824 25061 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26019 25061 603 41 0 25978 0
vsize: 104076
[startup+1200.24 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20551
Raw data (stat): 20551 (minisat+) R 20550 5897 5896 0 -1 0 25319 0 0 0 119948 83 0 0 25 0 1 0 491202262 106979328 25136 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26118 25136 603 41 0 26077 0
vsize: 104472
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.76 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 20551
Raw data (stat): 20551 (minisat+) Z 20550 5897 5896 0 -1 12 25322 0 0 0 119949 88 0 0 20 0 1 0 491202262 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.76
CPU time (s): 1200.38
CPU user time (s): 1199.49
CPU system time (s): 0.885865
CPU usage (%): 99.9678
Max. virtual memory (Kb): 104472
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####