PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-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.07284
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 15349

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        808432 kB
Buffers:         25880 kB
Cached:         178892 kB
SwapCached:        316 kB
Active:          35972 kB
Inactive:       171116 kB
HighTotal:      131008 kB
HighFree:        22260 kB
LowTotal:       903652 kB
LowFree:        786172 kB
SwapTotal:     2097136 kB
SwapFree:      2096236 kB
Dirty:              44 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            13664 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:21:25 (client local time) WITH STATUS 10 IN 1200.6 SECONDS
stats: 17885 7 1200.6 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.93 1.00 0.93 2/54 19382
Raw data (stat): 19382 (runsolver) R 19381 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483813377 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.94 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 5004 0 0 0 984 14 0 0 25 0 1 0 483813377 23023616 4821 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5621 4821 603 41 0 5580 0
vsize: 22484
[startup+20.0022 s]
Raw data (loadavg): 0.95 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 5276 0 0 0 1983 15 0 0 25 0 1 0 483813377 24244224 5093 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5919 5093 603 41 0 5878 0
vsize: 23676
[startup+30.0017 s]
Raw data (loadavg): 0.95 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 5615 0 0 0 2982 16 0 0 25 0 1 0 483813377 25714688 5432 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6278 5432 603 41 0 6237 0
vsize: 25112
[startup+40.0016 s]
Raw data (loadavg): 0.96 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 5908 0 0 0 3981 17 0 0 25 0 1 0 483813377 26791936 5725 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6541 5725 603 41 0 6500 0
vsize: 26164
[startup+50.0028 s]
Raw data (loadavg): 0.97 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 6263 0 0 0 4980 18 0 0 25 0 1 0 483813377 28278784 6080 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6904 6080 603 41 0 6863 0
vsize: 27616
[startup+60.0032 s]
Raw data (loadavg): 0.97 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 6729 0 0 0 5979 19 0 0 25 0 1 0 483813377 30294016 6546 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7396 6546 603 41 0 7355 0
vsize: 29584
[startup+70.0041 s]
Raw data (loadavg): 0.98 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 7093 0 0 0 6979 20 0 0 25 0 1 0 483813377 31776768 6910 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7758 6910 603 41 0 7717 0
vsize: 31032
[startup+80.0042 s]
Raw data (loadavg): 0.98 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 7353 0 0 0 7978 21 0 0 25 0 1 0 483813377 32845824 7170 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8019 7170 603 41 0 7978 0
vsize: 32076
[startup+90.0048 s]
Raw data (loadavg): 0.98 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 7707 0 0 0 8977 22 0 0 25 0 1 0 483813377 34181120 7524 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8345 7524 603 41 0 8304 0
vsize: 33380
[startup+100.005 s]
Raw data (loadavg): 0.98 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 8040 0 0 0 9976 23 0 0 25 0 1 0 483813377 35532800 7857 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8675 7857 603 41 0 8634 0
vsize: 34700
[startup+110.006 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 8517 0 0 0 10975 25 0 0 25 0 1 0 483813377 37539840 8334 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9165 8334 603 41 0 9124 0
vsize: 36660
[startup+120.006 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 8908 0 0 0 11974 26 0 0 25 0 1 0 483813377 39534592 8725 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9652 8725 603 41 0 9611 0
vsize: 38608
[startup+130.006 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 9078 0 0 0 12973 27 0 0 25 0 1 0 483813377 40206336 8895 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9816 8895 603 41 0 9775 0
vsize: 39264
[startup+140.015 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 9290 0 0 0 13974 27 0 0 25 0 1 0 483813377 41152512 9107 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10047 9107 603 41 0 10006 0
vsize: 40188
[startup+150.015 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 9542 0 0 0 14973 28 0 0 25 0 1 0 483813377 42094592 9359 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10277 9359 603 41 0 10236 0
vsize: 41108
[startup+160.016 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 9847 0 0 0 15973 29 0 0 25 0 1 0 483813377 43307008 9664 4294967295 134512640 134672761 3221224544 3221223668 134566089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10573 9664 603 41 0 10532 0
vsize: 42292
[startup+170.017 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 10275 0 0 0 16971 30 0 0 25 0 1 0 483813377 45051904 10092 4294967295 134512640 134672761 3221224544 3221223696 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10999 10092 603 41 0 10958 0
vsize: 43996
[startup+180.016 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 10505 0 0 0 17970 31 0 0 25 0 1 0 483813377 45993984 10322 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11229 10322 603 41 0 11188 0
vsize: 44916
[startup+190.016 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 10774 0 0 0 18970 32 0 0 25 0 1 0 483813377 46931968 10591 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11458 10591 603 41 0 11417 0
vsize: 45832
[startup+200.016 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 11225 0 0 0 19969 34 0 0 25 0 1 0 483813377 48824320 11042 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11920 11042 603 41 0 11879 0
vsize: 47680
[startup+210.017 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 11438 0 0 0 20968 34 0 0 25 0 1 0 483813377 49635328 11255 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12118 11255 603 41 0 12077 0
vsize: 48472
[startup+220.017 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 11671 0 0 0 21967 35 0 0 25 0 1 0 483813377 50577408 11488 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12348 11488 603 41 0 12307 0
vsize: 49392
[startup+230.017 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 11843 0 0 0 22967 35 0 0 25 0 1 0 483813377 51249152 11660 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12512 11660 603 41 0 12471 0
vsize: 50048
[startup+240.017 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 11978 0 0 0 23967 36 0 0 25 0 1 0 483813377 51781632 11795 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12642 11795 603 41 0 12601 0
vsize: 50568
[startup+250.017 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 12176 0 0 0 24966 37 0 0 25 0 1 0 483813377 52600832 11993 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12842 11993 603 41 0 12801 0
vsize: 51368
[startup+260.019 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19382
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 12366 0 0 0 25965 38 0 0 25 0 1 0 483813377 53403648 12183 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13038 12183 603 41 0 12997 0
vsize: 52152
[startup+270.019 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 12914 0 0 0 26964 39 0 0 25 0 1 0 483813377 55558144 12731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13564 12731 603 41 0 13523 0
vsize: 54256
[startup+280.019 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 13598 0 0 0 27962 42 0 0 25 0 1 0 483813377 58380288 13415 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14253 13415 603 41 0 14212 0
vsize: 57012
[startup+290.019 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 13782 0 0 0 28962 42 0 0 25 0 1 0 483813377 59043840 13599 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14415 13599 603 41 0 14374 0
vsize: 57660
[startup+300.091 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 13939 0 0 0 29968 43 0 0 25 0 1 0 483813377 60764160 13756 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14835 13756 603 41 0 14794 0
vsize: 59340
[startup+310.092 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 14074 0 0 0 30968 43 0 0 25 0 1 0 483813377 61300736 13891 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14966 13891 603 41 0 14925 0
vsize: 59864
[startup+320.093 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15322 0 0 0 31965 46 0 0 25 0 1 0 483813377 66514944 15139 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.093 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15324 0 0 0 32965 46 0 0 25 0 1 0 483813377 66514944 15141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15141 603 41 0 16198 0
vsize: 64956
[startup+340.094 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15324 0 0 0 33966 46 0 0 25 0 1 0 483813377 66514944 15141 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15141 603 41 0 16198 0
vsize: 64956
[startup+350.094 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15324 0 0 0 34966 46 0 0 25 0 1 0 483813377 66514944 15141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15141 603 41 0 16198 0
vsize: 64956
[startup+360.095 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15324 0 0 0 35966 46 0 0 25 0 1 0 483813377 66514944 15141 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15141 603 41 0 16198 0
vsize: 64956
[startup+370.101 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15324 0 0 0 36967 46 0 0 25 0 1 0 483813377 66514944 15141 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15141 603 41 0 16198 0
vsize: 64956
[startup+380.102 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15325 0 0 0 37967 46 0 0 25 0 1 0 483813377 66514944 15142 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15142 603 41 0 16198 0
vsize: 64956
[startup+390.102 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15325 0 0 0 38967 46 0 0 25 0 1 0 483813377 66514944 15142 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15142 603 41 0 16198 0
vsize: 64956
[startup+400.102 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 39968 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+410.107 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 40968 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+420.108 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 41968 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+430.107 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 42969 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+440.109 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 43969 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+450.11 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 44969 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+460.11 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 45969 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+470.11 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 46969 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+480.111 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 47970 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+490.111 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 48970 46 0 0 25 0 1 0 483813377 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+500.112 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 49970 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+510.114 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 50970 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+520.114 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 51971 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+530.114 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 52971 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+540.121 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 53972 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+550.126 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 54972 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+560.127 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 55972 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+570.128 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 56973 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+580.128 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 57973 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+590.148 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 58975 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+600.148 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 59975 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+610.196 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 60980 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+620.203 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 61981 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+630.21 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 62982 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+640.258 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 63987 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+650.284 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 64990 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+660.292 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 65991 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+670.296 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 66991 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+680.296 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 67991 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+690.297 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 68992 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+700.298 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 69992 46 0 0 25 0 1 0 483813377 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+710.307 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 70992 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+720.32 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 71994 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+730.32 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 72994 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+740.321 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 73994 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+750.322 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15329 0 0 0 74994 46 0 0 25 0 1 0 483813377 66514944 15146 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16239 15146 603 41 0 16198 0
vsize: 64956
[startup+760.321 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 15367 0 0 0 75994 46 0 0 25 0 1 0 483813377 66650112 15184 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16272 15184 603 41 0 16231 0
vsize: 65088
[startup+770.321 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 16208 0 0 0 76992 49 0 0 25 0 1 0 483813377 70156288 16025 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17128 16025 603 41 0 17087 0
vsize: 68512
[startup+780.321 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 16794 0 0 0 77990 51 0 0 25 0 1 0 483813377 72441856 16611 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17686 16611 603 41 0 17645 0
vsize: 70744
[startup+790.322 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 17137 0 0 0 78990 51 0 0 25 0 1 0 483813377 73912320 16954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18045 16954 603 41 0 18004 0
vsize: 72180
[startup+800.323 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 17246 0 0 0 79990 52 0 0 25 0 1 0 483813377 74313728 17063 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18143 17063 603 41 0 18102 0
vsize: 72572
[startup+810.323 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 17363 0 0 0 80990 52 0 0 25 0 1 0 483813377 74854400 17180 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18275 17180 603 41 0 18234 0
vsize: 73100
[startup+820.344 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 17449 0 0 0 81991 53 0 0 25 0 1 0 483813377 75124736 17266 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18341 17266 603 41 0 18300 0
vsize: 73364
[startup+830.353 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 17543 0 0 0 82992 53 0 0 25 0 1 0 483813377 75530240 17360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18440 17360 603 41 0 18399 0
vsize: 73760
[startup+840.354 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 17666 0 0 0 83992 53 0 0 25 0 1 0 483813377 75935744 17483 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18539 17483 603 41 0 18498 0
vsize: 74156
[startup+850.355 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 17778 0 0 0 84992 53 0 0 25 0 1 0 483813377 76472320 17595 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18670 17595 603 41 0 18629 0
vsize: 74680
[startup+860.364 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 17882 0 0 0 85993 54 0 0 25 0 1 0 483813377 76873728 17699 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18768 17699 603 41 0 18727 0
vsize: 75072
[startup+870.364 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 17990 0 0 0 86993 54 0 0 25 0 1 0 483813377 77279232 17807 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18867 17807 603 41 0 18826 0
vsize: 75468
[startup+880.364 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 18058 0 0 0 87992 55 0 0 25 0 1 0 483813377 77545472 17875 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18932 17875 603 41 0 18891 0
vsize: 75728
[startup+890.364 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 18160 0 0 0 88992 55 0 0 25 0 1 0 483813377 77950976 17977 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19031 17977 603 41 0 18990 0
vsize: 76124
[startup+900.365 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 18255 0 0 0 89993 55 0 0 25 0 1 0 483813377 78356480 18072 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19130 18072 603 41 0 19089 0
vsize: 76520
[startup+910.365 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 18568 0 0 0 90992 55 0 0 25 0 1 0 483813377 79568896 18385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19426 18385 603 41 0 19385 0
vsize: 77704
[startup+920.366 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 18650 0 0 0 91992 55 0 0 25 0 1 0 483813377 79974400 18467 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19525 18467 603 41 0 19484 0
vsize: 78100
[startup+930.367 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 18748 0 0 0 92992 56 0 0 25 0 1 0 483813377 80379904 18565 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19624 18565 603 41 0 19583 0
vsize: 78496
[startup+940.368 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 18862 0 0 0 93992 56 0 0 25 0 1 0 483813377 80773120 18679 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19720 18679 603 41 0 19679 0
vsize: 78880
[startup+950.367 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 19292 0 0 0 94991 57 0 0 25 0 1 0 483813377 82513920 19109 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20145 19109 603 41 0 20104 0
vsize: 80580
[startup+960.367 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 19922 0 0 0 95989 59 0 0 25 0 1 0 483813377 85082112 19739 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20772 19739 603 41 0 20731 0
vsize: 83088
[startup+970.368 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 20492 0 0 0 96988 61 0 0 25 0 1 0 483813377 87388160 20309 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21335 20309 603 41 0 21294 0
vsize: 85340
[startup+980.368 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 21017 0 0 0 97986 62 0 0 25 0 1 0 483813377 89542656 20834 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21861 20834 603 41 0 21820 0
vsize: 87444
[startup+990.369 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 21543 0 0 0 98986 63 0 0 25 0 1 0 483813377 91713536 21360 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22391 21360 603 41 0 22350 0
vsize: 89564
[startup+1000.37 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 21949 0 0 0 99985 64 0 0 25 0 1 0 483813377 93327360 21766 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22785 21766 603 41 0 22744 0
vsize: 91140
[startup+1010.37 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 22383 0 0 0 100982 67 0 0 25 0 1 0 483813377 95076352 22200 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23212 22200 603 41 0 23171 0
vsize: 92848
[startup+1020.37 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 22788 0 0 0 101981 68 0 0 25 0 1 0 483813377 96714752 22605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23612 22605 603 41 0 23571 0
vsize: 94448
[startup+1030.37 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 23009 0 0 0 102981 69 0 0 25 0 1 0 483813377 97665024 22826 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23844 22826 603 41 0 23803 0
vsize: 95376
[startup+1040.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 23115 0 0 0 103982 69 0 0 25 0 1 0 483813377 98070528 22932 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23943 22932 603 41 0 23902 0
vsize: 95772
[startup+1050.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 23300 0 0 0 104981 70 0 0 25 0 1 0 483813377 98873344 23117 4294967295 134512640 134672761 3221224544 3221223680 134560720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24139 23117 603 41 0 24098 0
vsize: 96556
[startup+1060.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 23524 0 0 0 105980 71 0 0 25 0 1 0 483813377 99684352 23341 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24337 23341 603 41 0 24296 0
vsize: 97348
[startup+1070.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 23661 0 0 0 106980 71 0 0 25 0 1 0 483813377 100225024 23478 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24469 23478 603 41 0 24428 0
vsize: 97876
[startup+1080.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 23761 0 0 0 107980 72 0 0 25 0 1 0 483813377 100630528 23578 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24568 23578 603 41 0 24527 0
vsize: 98272
[startup+1090.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 23890 0 0 0 108980 72 0 0 25 0 1 0 483813377 101167104 23707 4294967295 134512640 134672761 3221224544 3221223668 134566045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24699 23707 603 41 0 24658 0
vsize: 98796
[startup+1100.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 24024 0 0 0 109979 72 0 0 25 0 1 0 483813377 101707776 23841 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24831 23841 603 41 0 24790 0
vsize: 99324
[startup+1110.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 24130 0 0 0 110979 73 0 0 25 0 1 0 483813377 102113280 23947 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24930 23947 603 41 0 24889 0
vsize: 99720
[startup+1120.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 24240 0 0 0 111979 73 0 0 25 0 1 0 483813377 102518784 24057 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25029 24057 603 41 0 24988 0
vsize: 100116
[startup+1130.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 24293 0 0 0 112979 74 0 0 25 0 1 0 483813377 102785024 24110 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25094 24110 603 41 0 25053 0
vsize: 100376
[startup+1140.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 24499 0 0 0 113979 74 0 0 25 0 1 0 483813377 103608320 24316 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25295 24316 603 41 0 25254 0
vsize: 101180
[startup+1150.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 24617 0 0 0 114979 74 0 0 25 0 1 0 483813377 104144896 24434 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25426 24434 603 41 0 25385 0
vsize: 101704
[startup+1160.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 24686 0 0 0 115978 75 0 0 25 0 1 0 483813377 104415232 24503 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25492 24503 603 41 0 25451 0
vsize: 101968
[startup+1170.38 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 24931 0 0 0 116978 76 0 0 25 0 1 0 483813377 105357312 24748 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25722 24748 603 41 0 25681 0
vsize: 102888
[startup+1180.39 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 25146 0 0 0 117977 77 0 0 25 0 1 0 483813377 106303488 24963 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25953 24963 603 41 0 25912 0
vsize: 103812
[startup+1190.39 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 25251 0 0 0 118977 77 0 0 25 0 1 0 483813377 106708992 25068 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26052 25068 603 41 0 26011 0
vsize: 104208
[startup+1200.39 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 19384
Raw data (stat): 19382 (minisat+) R 19381 25285 25284 0 -1 0 25330 0 0 0 119976 78 0 0 25 0 1 0 483813377 106979328 25147 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26118 25147 603 41 0 26077 0
vsize: 104472
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.45 s]
Raw data (loadavg): 0.99 1.00 0.93 1/54 19384
Raw data (stat): 19382 (minisat+) Z 19381 25285 25284 0 -1 12 25333 0 0 0 119977 82 0 0 25 0 1 0 483813377 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.44
CPU time (s): 1200.6
CPU user time (s): 1199.77
CPU system time (s): 0.829873
CPU usage (%): 100.013
Max. virtual memory (Kb): 104472
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####