PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-aflow30a.opb
MD5SUM	7fcbcb2a8848112bb780308c9eb60989
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4241
Optimality of the best value was proved	NO
Number of terms in the objective function	421
Biggest coefficient in the objective function	500
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	72290
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	3334110
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.05
Number of variables	7195
Total number of constraints	1321
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	450
Number of constraints which are nor clauses,nor cardinality constraints	871
Minimum length of a constraint	1
Maximum length of a constraint	555
Trace number 16859

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-21 08:43:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12413 boxname=wulflinc11 idbench=955 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7fcbcb2a8848112bb780308c9eb60989  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-aflow30a.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-aflow30a.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-aflow30a.opb
IDLAUNCH: 12413
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        759208 kB
Buffers:         29316 kB
Cached:         225072 kB
SwapCached:          0 kB
Active:          99232 kB
Inactive:       157944 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        758956 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            12756 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:03:58 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 12413 7 1200.29 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 958 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[1020]---> BDD-cost:   16
c ---[1019]---> BDD-cost:   14
c ---[1018]---> BDD-cost:   14
c ---[1017]---> BDD-cost:   15
c ---[1016]---> BDD-cost:   16
c ---[1015]---> BDD-cost:   15
c ---[1014]---> BDD-cost:   16
c ---[1013]---> BDD-cost:   15
c ---[1012]---> BDD-cost:   16
c ---[1011]---> BDD-cost:   14
c ---[1010]---> BDD-cost:   16
c ---[1009]---> BDD-cost:   16
c ---[1008]---> BDD-cost:   15
c ---[1007]---> BDD-cost:   14
c ---[1006]---> BDD-cost:   15
c ---[1005]---> BDD-cost:   16
c ---[1004]---> BDD-cost:   16
c ---[1002]---> BDD-cost:   16
c ---[1001]---> BDD-cost:   16
c ---[1000]---> BDD-cost:   15
c ---[ 999]---> BDD-cost:   16
c ---[ 998]---> BDD-cost:   16
c ---[ 996]---> BDD-cost:   16
c ---[ 995]---> BDD-cost:   15
c ---[ 993]---> BDD-cost:   15
c ---[ 992]---> BDD-cost:   16
c ---[ 991]---> BDD-cost:   15
c ---[ 990]---> BDD-cost:   16
c ---[ 989]---> BDD-cost:   15
c ---[ 988]---> BDD-cost:   15
c ---[ 987]---> BDD-cost:   16
c ---[ 986]---> BDD-cost:   16
c ---[ 985]---> BDD-cost:   15
c ---[ 984]---> BDD-cost:   16
c ---[ 981]---> BDD-cost:   16
c ---[ 980]---> BDD-cost:   14
c ---[ 978]---> BDD-cost:   16
c ---[ 977]---> BDD-cost:   15
c ---[ 974]---> BDD-cost:   13
c ---[ 973]---> BDD-cost:   15
c ---[ 972]---> BDD-cost:   14
c ---[ 971]---> BDD-cost:   16
c ---[ 970]---> BDD-cost:   13
c ---[ 969]---> BDD-cost:   16
c ---[ 968]---> BDD-cost:   16
c ---[ 967]---> BDD-cost:   16
c ---[ 966]---> BDD-cost:   15
c ---[ 964]---> BDD-cost:   16
c ---[ 963]---> BDD-cost:   16
c ---[ 962]---> BDD-cost:   15
c ---[ 961]---> BDD-cost:   13
c ---[ 960]---> BDD-cost:   16
c ---[ 959]---> BDD-cost:   13
c ---[ 958]---> BDD-cost:   16
c ---[ 956]---> BDD-cost:   15
c ---[ 955]---> BDD-cost:   16
c ---[ 954]---> BDD-cost:   14
c ---[ 953]---> BDD-cost:   16
c ---[ 952]---> BDD-cost:   16
c ---[ 951]---> BDD-cost:   14
c ---[ 950]---> BDD-cost:   16
c ---[ 949]---> BDD-cost:   16
c ---[ 948]---> BDD-cost:   16
c ---[ 947]---> BDD-cost:   16
c ---[ 946]---> BDD-cost:   16
c ---[ 945]---> BDD-cost:   16
c ---[ 944]---> BDD-cost:   15
c ---[ 943]---> BDD-cost:   16
c ---[ 942]---> BDD-cost:   16
c ---[ 941]---> BDD-cost:   14
c ---[ 940]---> BDD-cost:   16
c ---[ 939]---> BDD-cost:   16
c ---[ 937]---> BDD-cost:   16
c ---[ 936]---> BDD-cost:   15
c ---[ 935]---> BDD-cost:   13
c ---[ 934]---> BDD-cost:   16
c ---[ 933]---> BDD-cost:   13
c ---[ 932]---> BDD-cost:   15
c ---[ 931]---> BDD-cost:   15
c ---[ 930]---> BDD-cost:   16
c ---[ 928]---> BDD-cost:   14
c ---[ 927]---> BDD-cost:   16
c ---[ 926]---> BDD-cost:   16
c ---[ 925]---> BDD-cost:   16
c ---[ 924]---> BDD-cost:   16
c ---[ 923]---> BDD-cost:   14
c ---[ 922]---> BDD-cost:   15
c ---[ 921]---> BDD-cost:   15
c ---[ 919]---> BDD-cost:   15
c ---[ 918]---> BDD-cost:   15
c ---[ 917]---> BDD-cost:   16
c ---[ 916]---> BDD-cost:   13
c ---[ 915]---> BDD-cost:   15
c ---[ 914]---> BDD-cost:   16
c ---[ 913]---> BDD-cost:   16
c ---[ 912]---> BDD-cost:   16
c ---[ 911]---> BDD-cost:   16
c ---[ 910]---> BDD-cost:   15
c ---[ 908]---> BDD-cost:   16
c ---[ 907]---> BDD-cost:   16
c ---[ 906]---> BDD-cost:   15
c ---[ 905]---> BDD-cost:   16
c ---[ 903]---> BDD-cost:   16
c ---[ 902]---> BDD-cost:   16
c ---[ 900]---> BDD-cost:   16
c ---[ 899]---> BDD-cost:   13
c ---[ 898]---> BDD-cost:   15
c ---[ 897]---> BDD-cost:   15
c ---[ 896]---> BDD-cost:   15
c ---[ 895]---> BDD-cost:   16
c ---[ 893]---> BDD-cost:   15
c ---[ 892]---> BDD-cost:   16
c ---[ 891]---> BDD-cost:   14
c ---[ 890]---> BDD-cost:   16
c ---[ 889]---> BDD-cost:   16
c ---[ 888]---> BDD-cost:   16
c ---[ 887]---> BDD-cost:   16
c ---[ 886]---> BDD-cost:   14
c ---[ 885]---> BDD-cost:   16
c ---[ 883]---> BDD-cost:   13
c ---[ 882]---> BDD-cost:   14
c ---[ 881]---> BDD-cost:   16
c ---[ 880]---> BDD-cost:   16
c ---[ 879]---> BDD-cost:   16
c ---[ 878]---> BDD-cost:   15
c ---[ 877]---> BDD-cost:   14
c ---[ 876]---> BDD-cost:   13
c ---[ 875]---> BDD-cost:   16
c ---[ 874]---> BDD-cost:   16
c ---[ 873]---> BDD-cost:   14
c ---[ 871]---> BDD-cost:   15
c ---[ 870]---> BDD-cost:   16
c ---[ 869]---> BDD-cost:   15
c ---[ 867]---> BDD-cost:   14
c ---[ 866]---> BDD-cost:   16
c ---[ 865]---> BDD-cost:   16
c ---[ 863]---> BDD-cost:   16
c ---[ 862]---> BDD-cost:   16
c ---[ 861]---> BDD-cost:   15
c ---[ 860]---> BDD-cost:   16
c ---[ 859]---> BDD-cost:   15
c ---[ 858]---> BDD-cost:   16
c ---[ 857]---> BDD-cost:   15
c ---[ 856]---> BDD-cost:   16
c ---[ 855]---> BDD-cost:   15
c ---[ 853]---> BDD-cost:   16
c ---[ 851]---> BDD-cost:   16
c ---[ 850]---> BDD-cost:   15
c ---[ 849]---> BDD-cost:   14
c ---[ 848]---> BDD-cost:   15
c ---[ 847]---> BDD-cost:   16
c ---[ 846]---> BDD-cost:   15
c ---[ 845]---> BDD-cost:   16
c ---[ 844]---> BDD-cost:   15
c ---[ 843]---> BDD-cost:   15
c ---[ 842]---> BDD-cost:   14
c ---[ 841]---> BDD-cost:   14
c ---[ 840]---> BDD-cost:   13
c ---[ 839]---> BDD-cost:   16
c ---[ 837]---> BDD-cost:   13
c ---[ 836]---> BDD-cost:   15
c ---[ 835]---> BDD-cost:   16
c ---[ 834]---> BDD-cost:   16
c ---[ 833]---> BDD-cost:   16
c ---[ 832]---> BDD-cost:   16
c ---[ 831]---> BDD-cost:   16
c ---[ 829]---> BDD-cost:   16
c ---[ 828]---> BDD-cost:   15
c ---[ 825]---> BDD-cost:   14
c ---[ 824]---> BDD-cost:   16
c ---[ 823]---> BDD-cost:   16
c ---[ 822]---> BDD-cost:   15
c ---[ 821]---> BDD-cost:   16
c ---[ 820]---> BDD-cost:   16
c ---[ 819]---> BDD-cost:   16
c ---[ 818]---> BDD-cost:   16
c ---[ 817]---> BDD-cost:   16
c ---[ 816]---> BDD-cost:   16
c ---[ 815]---> BDD-cost:   16
c ---[ 814]---> BDD-cost:   13
c ---[ 812]---> BDD-cost:   16
c ---[ 811]---> BDD-cost:   14
c ---[ 809]---> BDD-cost:   15
c ---[ 808]---> BDD-cost:   15
c ---[ 807]---> BDD-cost:   16
c ---[ 806]---> BDD-cost:   16
c ---[ 805]---> BDD-cost:   15
c ---[ 804]---> BDD-cost:   15
c ---[ 803]---> BDD-cost:   16
c ---[ 801]---> BDD-cost:   16
c ---[ 800]---> BDD-cost:   16
c ---[ 799]---> BDD-cost:   14
c ---[ 798]---> BDD-cost:   15
c ---[ 797]---> BDD-cost:   16
c ---[ 796]---> BDD-cost:   14
c ---[ 795]---> BDD-cost:   16
c ---[ 793]---> BDD-cost:   15
c ---[ 791]---> BDD-cost:   16
c ---[ 790]---> BDD-cost:   15
c ---[ 789]---> BDD-cost:   14
c ---[ 788]---> BDD-cost:   16
c ---[ 787]---> BDD-cost:   16
c ---[ 786]---> BDD-cost:   16
c ---[ 785]---> BDD-cost:   16
c ---[ 784]---> BDD-cost:   14
c ---[ 782]---> BDD-cost:   13
c ---[ 781]---> BDD-cost:   16
c ---[ 780]---> BDD-cost:   14
c ---[ 779]---> BDD-cost:   16
c ---[ 778]---> BDD-cost:   16
c ---[ 777]---> BDD-cost:   14
c ---[ 776]---> BDD-cost:   14
c ---[ 774]---> BDD-cost:   16
c ---[ 772]---> BDD-cost:   15
c ---[ 771]---> BDD-cost:   16
c ---[ 770]---> BDD-cost:   16
c ---[ 769]---> BDD-cost:   16
c ---[ 768]---> BDD-cost:   16
c ---[ 767]---> BDD-cost:   14
c ---[ 766]---> BDD-cost:   16
c ---[ 764]---> BDD-cost:   16
c ---[ 763]---> BDD-cost:   13
c ---[ 762]---> BDD-cost:   16
c ---[ 761]---> BDD-cost:   16
c ---[ 760]---> BDD-cost:   16
c ---[ 759]---> BDD-cost:   15
c ---[ 758]---> BDD-cost:   15
c ---[ 757]---> BDD-cost:   14
c ---[ 756]---> BDD-cost:   15
c ---[ 754]---> BDD-cost:   13
c ---[ 753]---> BDD-cost:   16
c ---[ 752]---> BDD-cost:   16
c ---[ 751]---> BDD-cost:   13
c ---[ 750]---> BDD-cost:   15
c ---[ 749]---> BDD-cost:   16
c ---[ 747]---> BDD-cost:   15
c ---[ 746]---> BDD-cost:   15
c ---[ 745]---> BDD-cost:   15
c ---[ 744]---> BDD-cost:   14
c ---[ 743]---> BDD-cost:   15
c ---[ 742]---> BDD-cost:   16
c ---[ 741]---> BDD-cost:   14
c ---[ 740]---> BDD-cost:   15
c ---[ 738]---> BDD-cost:   15
c ---[ 737]---> BDD-cost:   15
c ---[ 736]---> BDD-cost:   15
c ---[ 734]---> BDD-cost:   14
c ---[ 733]---> BDD-cost:   15
c ---[ 732]---> BDD-cost:   14
c ---[ 730]---> BDD-cost:   15
c ---[ 729]---> BDD-cost:   13
c ---[ 728]---> BDD-cost:   15
c ---[ 727]---> BDD-cost:   15
c ---[ 726]---> BDD-cost:   15
c ---[ 725]---> BDD-cost:   14
c ---[ 723]---> BDD-cost:   16
c ---[ 722]---> BDD-cost:   15
c ---[ 721]---> BDD-cost:   16
c ---[ 720]---> BDD-cost:   16
c ---[ 719]---> BDD-cost:   13
c ---[ 718]---> BDD-cost:   16
c ---[ 717]---> BDD-cost:   15
c ---[ 716]---> BDD-cost:   14
c ---[ 713]---> BDD-cost:   15
c ---[ 712]---> BDD-cost:   14
c ---[ 711]---> BDD-cost:   15
c ---[ 710]---> BDD-cost:   15
c ---[ 708]---> BDD-cost:   16
c ---[ 706]---> BDD-cost:   16
c ---[ 705]---> BDD-cost:   16
c ---[ 704]---> BDD-cost:   13
c ---[ 703]---> BDD-cost:   16
c ---[ 702]---> BDD-cost:   16
c ---[ 701]---> BDD-cost:   16
c ---[ 700]---> BDD-cost:   16
c ---[ 699]---> BDD-cost:   15
c ---[ 698]---> BDD-cost:   16
c ---[ 695]---> BDD-cost:   14
c ---[ 694]---> BDD-cost:   15
c ---[ 693]---> BDD-cost:   16
c ---[ 692]---> BDD-cost:   16
c ---[ 691]---> BDD-cost:   16
c ---[ 690]---> BDD-cost:   15
c ---[ 688]---> BDD-cost:   15
c ---[ 687]---> BDD-cost:   14
c ---[ 686]---> BDD-cost:   16
c ---[ 684]---> BDD-cost:   16
c ---[ 683]---> BDD-cost:   14
c ---[ 682]---> BDD-cost:   14
c ---[ 681]---> BDD-cost:   16
c ---[ 680]---> BDD-cost:   16
c ---[ 679]---> BDD-cost:   15
c ---[ 678]---> BDD-cost:   15
c ---[ 677]---> BDD-cost:   15
c ---[ 676]---> BDD-cost:   16
c ---[ 675]---> BDD-cost:   15
c ---[ 673]---> BDD-cost:   14
c ---[ 672]---> BDD-cost:   16
c ---[ 671]---> BDD-cost:   16
c ---[ 670]---> BDD-cost:   16
c ---[ 668]---> BDD-cost:   16
c ---[ 667]---> BDD-cost:   16
c ---[ 666]---> BDD-cost:   14
c ---[ 665]---> BDD-cost:   15
c ---[ 664]---> BDD-cost:   15
c ---[ 663]---> BDD-cost:   16
c ---[ 662]---> BDD-cost:   16
c ---[ 661]---> BDD-cost:   15
c ---[ 660]---> BDD-cost:   14
c ---[ 659]---> BDD-cost:   16
c ---[ 658]---> BDD-cost:   16
c ---[ 657]---> BDD-cost:   15
c ---[ 656]---> BDD-cost:   16
c ---[ 655]---> BDD-cost:   15
c ---[ 654]---> BDD-cost:   13
c ---[ 653]---> BDD-cost:   13
c ---[ 651]---> BDD-cost:   15
c ---[ 649]---> BDD-cost:   15
c ---[ 648]---> BDD-cost:   15
c ---[ 647]---> BDD-cost:   16
c ---[ 645]---> BDD-cost:   16
c ---[ 644]---> BDD-cost:   13
c ---[ 643]---> BDD-cost:   16
c ---[ 642]---> BDD-cost:   16
c ---[ 640]---> BDD-cost:   15
c ---[ 638]---> BDD-cost:   16
c ---[ 637]---> BDD-cost:   15
c ---[ 636]---> BDD-cost:   16
c ---[ 635]---> BDD-cost:   15
c ---[ 634]---> BDD-cost:   14
c ---[ 633]---> BDD-cost:   15
c ---[ 632]---> BDD-cost:   16
c ---[ 631]---> BDD-cost:   15
c ---[ 630]---> BDD-cost:   16
c ---[ 628]---> BDD-cost:   15
c ---[ 627]---> BDD-cost:   16
c ---[ 625]---> BDD-cost:   16
c ---[ 624]---> BDD-cost:   16
c ---[ 623]---> BDD-cost:   15
c ---[ 622]---> BDD-cost:   15
c ---[ 621]---> BDD-cost:   13
c ---[ 620]---> BDD-cost:   15
c ---[ 619]---> BDD-cost:   16
c ---[ 618]---> BDD-cost:   14
c ---[ 617]---> BDD-cost:   14
c ---[ 616]---> BDD-cost:   16
c ---[ 615]---> BDD-cost:   16
c ---[ 614]---> BDD-cost:   13
c ---[ 613]---> BDD-cost:   15
c ---[ 608]---> BDD-cost:   15
c ---[ 607]---> BDD-cost:   16
c ---[ 606]---> BDD-cost:   14
c ---[ 605]---> BDD-cost:   16
c ---[ 604]---> BDD-cost:   14
c ---[ 603]---> BDD-cost:   16
c ---[ 602]---> BDD-cost:   16
c ---[ 601]---> BDD-cost:   16
c ---[ 600]---> BDD-cost:   13
c ---[ 598]---> BDD-cost:   17
c ---[ 596]---> BDD-cost:   25
c ---[ 595]---> BDD-cost:    8
c ---[ 594]---> BDD-cost:    4
c ---[ 593]---> BDD-cost:    8
c ---[ 592]---> BDD-cost:    8
c ---[ 591]---> BDD-cost:    6
c ---[ 590]---> BDD-cost:    8
c ---[ 589]---> BDD-cost:    8
c ---[ 588]---> BDD-cost:    8
c ---[ 587]---> BDD-cost:    5
c ---[ 586]---> BDD-cost:    6
c ---[ 584]---> BDD-cost:   27
c ---[ 583]---> BDD-cost:    8
c ---[ 582]---> BDD-cost:    7
c ---[ 581]---> BDD-cost:    8
c ---[ 580]---> BDD-cost:    8
c ---[ 579]---> BDD-cost:    6
c ---[ 578]---> BDD-cost:    6
c ---[ 577]---> BDD-cost:    6
c ---[ 576]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:    6
c ---[ 574]---> BDD-cost:    8
c ---[ 572]---> BDD-cost:   29
c ---[ 571]---> BDD-cost:    8
c ---[ 570]---> BDD-cost:    5
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:    6
c ---[ 567]---> BDD-cost:   21
c ---[ 566]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    5
c ---[ 564]---> BDD-cost:    7
c ---[ 563]---> BDD-cost:    5
c ---[ 562]---> BDD-cost:    7
c ---[ 560]---> BDD-cost:   27
c ---[ 559]---> BDD-cost:    8
c ---[ 558]---> BDD-cost:    8
c ---[ 557]---> BDD-cost:    7
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    6
c ---[ 554]---> BDD-cost:    5
c ---[ 553]---> BDD-cost:   18
c ---[ 552]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    8
c ---[ 548]---> BDD-cost:   19
c ---[ 547]---> BDD-cost:   20
c ---[ 546]---> BDD-cost:    7
c ---[ 545]---> BDD-cost:    6
c ---[ 544]---> BDD-cost:    6
c ---[ 543]---> BDD-cost:    3
c ---[ 542]---> BDD-cost:    6
c ---[ 541]---> BDD-cost:    8
c ---[ 540]---> BDD-cost:    7
c ---[ 539]---> BDD-cost:    5
c ---[ 538]---> BDD-cost:    8
c ---[ 536]---> BDD-cost:   23
c ---[ 535]---> BDD-cost:   19
c ---[ 534]---> BDD-cost:    7
c ---[ 533]---> BDD-cost:   18
c ---[ 532]---> BDD-cost:    8
c ---[ 531]---> BDD-cost:    6
c ---[ 530]---> BDD-cost:   18
c ---[ 529]---> BDD-cost:    7
c ---[ 528]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:    7
c ---[ 526]---> BDD-cost:   20
c ---[ 524]---> BDD-cost:   27
c ---[ 523]---> BDD-cost:    5
c ---[ 522]---> BDD-cost:    8
c ---[ 521]---> BDD-cost:    6
c ---[ 520]---> BDD-cost:    8
c ---[ 519]---> BDD-cost:    8
c ---[ 518]---> BDD-cost:    7
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    3
c ---[ 515]---> BDD-cost:    6
c ---[ 514]---> BDD-cost:    7
c ---[ 512]---> BDD-cost:   23
c ---[ 511]---> BDD-cost:    5
c ---[ 510]---> BDD-cost:    5
c ---[ 509]---> BDD-cost:    7
c ---[ 508]---> BDD-cost:    7
c ---[ 507]---> BDD-cost:    6
c ---[ 506]---> BDD-cost:    5
c ---[ 505]---> BDD-cost:    6
c ---[ 504]---> BDD-cost:    6
c ---[ 503]---> BDD-cost:    7
c ---[ 502]---> BDD-cost:    4
c ---[ 500]---> BDD-cost:   31
c ---[ 499]---> BDD-cost:    7
c ---[ 498]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:   21
c ---[ 496]---> BDD-cost:    8
c ---[ 495]---> BDD-cost:    5
c ---[ 494]---> BDD-cost:   18
c ---[ 493]---> BDD-cost:   21
c ---[ 492]---> BDD-cost:    6
c ---[ 491]---> BDD-cost:    6
c ---[ 490]---> BDD-cost:    8
c ---[ 488]---> BDD-cost:   25
c ---[ 487]---> BDD-cost:    7
c ---[ 486]---> BDD-cost:    8
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    8
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    5
c ---[ 480]---> BDD-cost:    8
c ---[ 479]---> BDD-cost:   19
c ---[ 478]---> BDD-cost:    7
c ---[ 476]---> BDD-cost:   23
c ---[ 474]---> BDD-cost:   33
c ---[ 473]---> BDD-cost:    3
c ---[ 472]---> BDD-cost:    4
c ---[ 471]---> BDD-cost:    6
c ---[ 470]---> BDD-cost:    6
c ---[ 469]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    6
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 464]---> BDD-cost:    8
c ---[ 462]---> BDD-cost:   19
c ---[ 461]---> BDD-cost:    7
c ---[ 460]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    8
c ---[ 458]---> BDD-cost:    3
c ---[ 457]---> BDD-cost:   21
c ---[ 456]---> BDD-cost:    4
c ---[ 455]---> BDD-cost:    4
c ---[ 454]---> BDD-cost:    6
c ---[ 453]---> BDD-cost:    4
c ---[ 452]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:   27
c ---[ 449]---> BDD-cost:    3
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:    6
c ---[ 445]---> BDD-cost:   20
c ---[ 444]---> BDD-cost:    7
c ---[ 443]---> BDD-cost:    3
c ---[ 442]---> BDD-cost:    8
c ---[ 441]---> BDD-cost:    8
c ---[ 440]---> BDD-cost:    8
c ---[ 438]---> BDD-cost:   35
c ---[ 437]---> BDD-cost:   19
c ---[ 436]---> BDD-cost:    8
c ---[ 435]---> BDD-cost:    6
c ---[ 434]---> BDD-cost:    8
c ---[ 433]---> BDD-cost:    8
c ---[ 432]---> BDD-cost:    8
c ---[ 431]---> BDD-cost:    8
c ---[ 430]---> BDD-cost:    5
c ---[ 429]---> BDD-cost:    7
c ---[ 428]---> BDD-cost:    8
c ---[ 426]---> BDD-cost:   27
c ---[ 425]---> BDD-cost:   20
c ---[ 424]---> BDD-cost:    7
c ---[ 423]---> BDD-cost:    5
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 420]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    7
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:   20
c ---[ 414]---> BDD-cost:   19
c ---[ 413]---> BDD-cost:    7
c ---[ 412]---> BDD-cost:    6
c ---[ 411]---> BDD-cost:    7
c ---[ 410]---> BDD-cost:    6
c ---[ 409]---> BDD-cost:   20
c ---[ 408]---> BDD-cost:    6
c ---[ 407]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:    5
c ---[ 405]---> BDD-cost:    7
c ---[ 404]---> BDD-cost:    6
c ---[ 402]---> BDD-cost:   31
c ---[ 401]---> BDD-cost:    7
c ---[ 400]---> BDD-cost:    7
c ---[ 399]---> BDD-cost:    8
c ---[ 398]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    5
c ---[ 394]---> BDD-cost:    7
c ---[ 393]---> BDD-cost:    4
c ---[ 392]---> BDD-cost:    6
c ---[ 390]---> BDD-cost:   25
c ---[ 389]---> BDD-cost:   20
c ---[ 388]---> BDD-cost:   20
c ---[ 387]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    3
c ---[ 385]---> BDD-cost:    5
c ---[ 384]---> BDD-cost:    6
c ---[ 383]---> BDD-cost:    7
c ---[ 382]---> BDD-cost:   19
c ---[ 381]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:    6
c ---[ 376]---> BDD-cost:    6
c ---[ 375]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    8
c ---[ 373]---> BDD-cost:    6
c ---[ 372]---> BDD-cost:    5
c ---[ 371]---> BDD-cost:    5
c ---[ 370]---> BDD-cost:    8
c ---[ 369]---> BDD-cost:    8
c ---[ 368]---> BDD-cost:    5
c ---[ 366]---> BDD-cost:   33
c ---[ 365]---> BDD-cost:    3
c ---[ 364]---> BDD-cost:    6
c ---[ 363]---> BDD-cost:    5
c ---[ 362]---> BDD-cost:    6
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:   19
c ---[ 359]---> BDD-cost:    7
c ---[ 358]---> BDD-cost:    6
c ---[ 357]---> BDD-cost:    8
c ---[ 356]---> BDD-cost:   17
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> Adder-cost: 849   maxlim: 818166   bits: 21/20
c ---[ 351]---> BDD-cost:    8
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    4
c ---[ 348]---> BDD-cost:   22
c ---[ 347]---> BDD-cost:   18
c ---[ 346]---> BDD-cost:    6
c ---[ 345]---> BDD-cost:   20
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:   17
c ---[ 342]---> BDD-cost:    6
c ---[ 340]---> Adder-cost: 704   maxlim: 1189875   bits: 21/21
c ---[ 339]---> BDD-cost:    7
c ---[ 338]---> BDD-cost:    7
c ---[ 337]---> BDD-cost:    8
c ---[ 336]---> BDD-cost:   20
c ---[ 335]---> BDD-cost:    7
c ---[ 334]---> BDD-cost:    8
c ---[ 333]---> BDD-cost:   22
c ---[ 332]---> BDD-cost:   19
c ---[ 331]---> BDD-cost:   22
c ---[ 330]---> BDD-cost:    3
c ---[ 328]---> Adder-cost: 1078   maxlim: 1449967   bits: 22/21
c ---[ 327]---> BDD-cost:    5
c ---[ 326]---> BDD-cost:    7
c ---[ 325]---> BDD-cost:    3
c ---[ 324]---> BDD-cost:    6
c ---[ 323]---> BDD-cost:    5
c ---[ 322]---> BDD-cost:    6
c ---[ 321]---> BDD-cost:    3
c ---[ 320]---> BDD-cost:    3
c ---[ 319]---> BDD-cost:    3
c ---[ 318]---> BDD-cost:    6
c ---[ 316]---> Adder-cost: 1006   maxlim: 1169393   bits: 22/21
c ---[ 315]---> BDD-cost:    4
c ---[ 314]---> BDD-cost:    7
c ---[ 313]---> BDD-cost:   19
c ---[ 312]---> BDD-cost:   19
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    8
c ---[ 309]---> BDD-cost:    8
c ---[ 308]---> BDD-cost:    4
c ---[ 307]---> BDD-cost:    5
c ---[ 306]---> BDD-cost:   22
c ---[ 304]---> Adder-cost: 1030   maxlim: 1483760   bits: 22/21
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:   22
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 298]---> BDD-cost:   17
c ---[ 297]---> BDD-cost:    3
c ---[ 296]---> BDD-cost:    7
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    5
c ---[ 292]---> Adder-cost: 672   maxlim: 746486   bits: 21/20
c ---[ 291]---> BDD-cost:    5
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    8
c ---[ 288]---> BDD-cost:    8
c ---[ 287]---> BDD-cost:    5
c ---[ 286]---> BDD-cost:   22
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:   19
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    8
c ---[ 280]---> Adder-cost: 882   maxlim: 1305585   bits: 22/21
c ---[ 279]---> BDD-cost:    7
c ---[ 278]---> BDD-cost:    8
c ---[ 277]---> BDD-cost:    7
c ---[ 276]---> BDD-cost:    4
c ---[ 275]---> BDD-cost:   18
c ---[ 274]---> BDD-cost:    6
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    7
c ---[ 270]---> BDD-cost:    6
c ---[ 268]---> Adder-cost: 942   maxlim: 1302514   bits: 22/21
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:   20
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    8
c ---[ 261]---> BDD-cost:    7
c ---[ 260]---> BDD-cost:   22
c ---[ 259]---> BDD-cost:   22
c ---[ 258]---> BDD-cost:    6
c ---[ 256]---> Adder-cost: 980   maxlim: 1616878   bits: 22/21
c ---[ 255]---> BDD-cost:    5
c ---[ 254]---> BDD-cost:    5
c ---[ 253]---> BDD-cost:    7
c ---[ 252]---> BDD-cost:   17
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:    5
c ---[ 249]---> BDD-cost:    7
c ---[ 248]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:   20
c ---[ 246]---> BDD-cost:    7
c ---[ 244]---> Adder-cost: 820   maxlim: 1307634   bits: 22/21
c ---[ 243]---> BDD-cost:    7
c ---[ 242]---> BDD-cost:    7
c ---[ 241]---> BDD-cost:    6
c ---[ 240]---> BDD-cost:    7
c ---[ 239]---> BDD-cost:    5
c ---[ 238]---> BDD-cost:    7
c ---[ 237]---> BDD-cost:    3
c ---[ 236]---> BDD-cost:    4
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:   22
c ---[ 232]---> BDD-cost:   27
c ---[ 230]---> Adder-cost: 868   maxlim: 1257457   bits: 22/21
c ---[ 229]---> BDD-cost:    5
c ---[ 228]---> BDD-cost:    7
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    4
c ---[ 225]---> BDD-cost:    5
c ---[ 224]---> BDD-cost:   22
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:   21
c ---[ 221]---> BDD-cost:    7
c ---[ 220]---> BDD-cost:    7
c ---[ 218]---> Adder-cost: 936   maxlim: 1176560   bits: 22/21
c ---[ 217]---> BDD-cost:    5
c ---[ 216]---> BDD-cost:   20
c ---[ 215]---> BDD-cost:    6
c ---[ 214]---> BDD-cost:    8
c ---[ 213]---> BDD-cost:    5
c ---[ 212]---> BDD-cost:    7
c ---[ 211]---> BDD-cost:    6
c ---[ 210]---> BDD-cost:    8
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    3
c ---[ 206]---> Adder-cost: 933   maxlim: 1047537   bits: 21/20
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    7
c ---[ 203]---> BDD-cost:   18
c ---[ 202]---> BDD-cost:   18
c ---[ 201]---> BDD-cost:   20
c ---[ 200]---> BDD-cost:    3
c ---[ 199]---> BDD-cost:    6
c ---[ 198]---> BDD-cost:    8
c ---[ 197]---> BDD-cost:   22
c ---[ 196]---> BDD-cost:    8
c ---[ 194]---> Adder-cost: 858   maxlim: 810997   bits: 21/20
c ---[ 193]---> BDD-cost:    8
c ---[ 192]---> BDD-cost:    6
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:    5
c ---[ 189]---> BDD-cost:    8
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    8
c ---[ 186]---> BDD-cost:   21
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    3
c ---[ 182]---> Adder-cost: 752   maxlim: 1157107   bits: 22/21
c ---[ 181]---> BDD-cost:    6
c ---[ 180]---> BDD-cost:    5
c ---[ 179]---> BDD-cost:    6
c ---[ 178]---> BDD-cost:    7
c ---[ 177]---> BDD-cost:    3
c ---[ 176]---> BDD-cost:    4
c ---[ 175]---> BDD-cost:    7
c ---[ 174]---> BDD-cost:    8
c ---[ 173]---> BDD-cost:    3
c ---[ 172]---> BDD-cost:    6
c ---[ 170]---> Adder-cost: 938   maxlim: 1399793   bits: 22/21
c ---[ 169]---> BDD-cost:    7
c ---[ 168]---> BDD-cost:   20
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    8
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    5
c ---[ 163]---> BDD-cost:    5
c ---[ 162]---> BDD-cost:    5
c ---[ 161]---> BDD-cost:    7
c ---[ 160]---> BDD-cost:   20
c ---[ 158]---> Adder-cost: 674   maxlim: 1276915   bits: 21/21
c ---[ 157]---> BDD-cost:    8
c ---[ 156]---> BDD-cost:    5
c ---[ 155]---> BDD-cost:    5
c ---[ 154]---> BDD-cost:    7
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    4
c ---[ 149]---> BDD-cost:   22
c ---[ 148]---> BDD-cost:    8
c ---[ 146]---> Adder-cost: 1010   maxlim: 1387503   bits: 22/21
c ---[ 145]---> BDD-cost:    6
c ---[ 144]---> BDD-cost:    8
c ---[ 143]---> BDD-cost:    4
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    7
c ---[ 140]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:   20
c ---[ 138]---> BDD-cost:    7
c ---[ 137]---> BDD-cost:    6
c ---[ 136]---> BDD-cost:    8
c ---[ 134]---> Adder-cost: 1056   maxlim: 1096690   bits: 22/21
c ---[ 132]---> Adder-cost: 966   maxlim: 1423342   bits: 22/21
c ---[ 130]---> BDD-cost:   29
c ---[ 128]---> Adder-cost: 740   maxlim: 960501   bits: 21/20
c ---[ 126]---> Adder-cost: 796   maxlim: 1239025   bits: 21/21
c ---[ 124]---> Adder-cost: 1062   maxlim: 1713133   bits: 22/21
c ---[ 122]---> Adder-cost: 872   maxlim: 1144817   bits: 22/21
c ---[ 120]---> Adder-cost: 758   maxlim: 669685   bits: 21/20
c ---[ 118]---> Adder-cost: 868   maxlim: 1154031   bits: 22/21
c ---[ 116]---> Adder-cost: 1012   maxlim: 1354738   bits: 22/21
c ---[ 114]---> Adder-cost: 742   maxlim: 1047540   bits: 21/20
c ---[ 112]---> Adder-cost: 1002   maxlim: 1405934   bits: 22/21
c ---[ 111]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:    5
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:   20
c ---[ 105]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    5
c ---[ 103]---> BDD-cost:    6
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    6
c ---[ 100]---> BDD-cost:    7
c ---[  99]---> BDD-cost:    6
c ---[  97]---> BDD-cost:   27
c ---[  96]---> BDD-cost:    6
c ---[  95]---> BDD-cost:    7
c ---[  94]---> BDD-cost:    3
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:    7
c ---[  90]---> BDD-cost:    6
c ---[  89]---> BDD-cost:    3
c ---[  88]---> BDD-cost:    3
c ---[  87]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   25
c ---[  84]---> BDD-cost:   21
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:    8
c ---[  81]---> BDD-cost:    6
c ---[  80]---> BDD-cost:    7
c ---[  79]---> BDD-cost:    7
c ---[  78]---> BDD-cost:   22
c ---[  77]---> BDD-cost:    3
c ---[  76]---> BDD-cost:    6
c ---[  75]---> BDD-cost:   18
c ---[  73]---> BDD-cost:   33
c ---[  72]---> BDD-cost:    5
c ---[  71]---> BDD-cost:   19
c ---[  70]---> BDD-cost:    5
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:   19
c ---[  67]---> BDD-cost:   22
c ---[  66]---> BDD-cost:    5
c ---[  65]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    6
c ---[  63]---> BDD-cost:    4
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:    1
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:    1
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:    1
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:    1
c ---[  10]---> BDD-cost:    1
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:    1
c ---[   6]---> BDD-cost:    1
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  192227   675203 |   57668       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/34955          
c   -- var.elim.:  2000/34955          
c   -- var.elim.:  3000/34955          
c   -- var.elim.:  4000/34955          
c   -- var.elim.:  5000/34955          
c   -- var.elim.:  6000/34955          
c   -- var.elim.:  7000/34955          
c   -- var.elim.:  8000/34955          
c   -- var.elim.:  9000/34955          
c   -- var.elim.:  10000/34955          
c   -- var.elim.:  11000/34955          
c   -- var.elim.:  12000/34955          
c   -- var.elim.:  13000/34955          
c   -- var.elim.:  14000/34955          
c   -- var.elim.:  15000/34955          
c   -- var.elim.:  16000/34955          
c   -- var.elim.:  17000/34955          
c   -- var.elim.:  18000/34955          
c   -- var.elim.:  19000/34955          
c   -- var.elim.:  20000/34955          
c   -- var.elim.:  21000/34955          
c   -- var.elim.:  22000/34955          
c   -- var.elim.:  23000/34955          
c   -- var.elim.:  24000/34955          
c   -- var.elim.:  25000/34955          
c   -- var.elim.:  26000/34955          
c   -- var.elim.:  27000/34955          
c   -- var.elim.:  28000/34955          
c   -- var.elim.:  29000/34955          
c   -- var.elim.:  30000/34955          
c   -- var.elim.:  31000/34955          
c   -- var.elim.:  32000/34955          
c   -- var.elim.:  33000/34955          
c   -- var.elim.:  34000/34955          
c   -- var.elim.:  34955/34955          
c   -- var.elim.:  1000/4235          
c   -- var.elim.:  2000/4235          
c   -- var.elim.:  3000/4235          
c   -- var.elim.:  4000/4235          
c   -- var.elim.:  4235/4235          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  620/620          
c   -- var.elim.:  132/132          
c |         0 |  185460   646071 |      --       0       --      -- |     --   | -3342/-8361
c |         0 |  185460   646071 |   74184       0        0     nan |  0.000 % |
c |       101 |  185460   646071 |   81602     101     1190    11.8 |  6.237 % |
c |       251 |  185460   646071 |   89762     251     1675     6.7 |  6.237 % |
c |       477 |  185460   646071 |   98738     477     5042    10.6 |  6.237 % |
c |       814 |  185460   646071 |  108612     814     7969     9.8 |  6.237 % |
c |      1320 |  185460   646071 |  119474    1320    22369    16.9 |  6.237 % |
c |      2081 |  185460   646071 |  131421    2081    39713    19.1 |  6.237 % |
c |      3221 |  185432   645953 |  144541    3218    66161    20.6 |  6.243 % |
c |      4930 |  185404   645835 |  158971    4919   173746    35.3 |  6.248 % |
c |      7492 |  185390   645776 |  174855    7479   436941    58.4 |  6.251 % |
c |     11338 |  185362   645658 |  192312   11319   687660    60.8 |  6.257 % |
c |     17106 |  185337   645548 |  211515   17085  2702699   158.2 |  6.263 % |
c |     25755 |  185248   645179 |  232555   25707  3933154   153.0 |  6.283 % |
c |     38729 |  185187   644928 |  255726   38672  6558165   169.6 |  6.297 % |
c |     58191 |  185159   644810 |  281256   58130 10159049   174.8 |  6.302 % |
c |     87383 |  185117   644633 |  309311   87317 15969357   182.9 |  6.311 % |
#### 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.80 0.95 0.96 2/54 31301
Raw data (stat): 31301 (runsolver) R 31300 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485509941 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0006 s]
Raw data (loadavg): 0.83 0.95 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 8133 0 0 0 976 23 0 0 25 0 1 0 485509941 34631680 7223 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8455 7223 603 41 0 8414 0
vsize: 33820
[startup+20.0003 s]
Raw data (loadavg): 0.86 0.95 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 8348 0 0 0 1975 23 0 0 25 0 1 0 485509941 35598336 7438 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8691 7438 603 41 0 8650 0
vsize: 34764
[startup+30.0014 s]
Raw data (loadavg): 0.88 0.95 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 8803 0 0 0 2974 24 0 0 25 0 1 0 485509941 37584896 7893 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9176 7893 603 41 0 9135 0
vsize: 36704
[startup+40.0009 s]
Raw data (loadavg): 0.90 0.96 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 9541 0 0 0 3973 26 0 0 25 0 1 0 485509941 40579072 8631 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9907 8631 603 41 0 9866 0
vsize: 39628
[startup+50.0006 s]
Raw data (loadavg): 0.91 0.96 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 10349 0 0 0 4972 27 0 0 25 0 1 0 485509941 43855872 9439 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10707 9439 603 41 0 10666 0
vsize: 42828
[startup+60.0004 s]
Raw data (loadavg): 0.92 0.96 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 10821 0 0 0 5970 29 0 0 25 0 1 0 485509941 45842432 9911 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11192 9911 603 41 0 11151 0
vsize: 44768
[startup+70.0002 s]
Raw data (loadavg): 0.94 0.96 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 11123 0 0 0 6969 30 0 0 25 0 1 0 485509941 47161344 10213 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11514 10213 603 41 0 11473 0
vsize: 46056
[startup+80.001 s]
Raw data (loadavg): 0.94 0.96 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 11354 0 0 0 7969 30 0 0 25 0 1 0 485509941 48095232 10444 4294967295 134512640 134672761 3221224544 3221223712 134615859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11742 10444 603 41 0 11701 0
vsize: 46968
[startup+90.0011 s]
Raw data (loadavg): 0.95 0.96 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 11831 0 0 0 8968 32 0 0 25 0 1 0 485509941 49938432 10921 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12192 10921 603 41 0 12151 0
vsize: 48768
[startup+100.001 s]
Raw data (loadavg): 0.96 0.96 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 12685 0 0 0 9966 34 0 0 25 0 1 0 485509941 53469184 11775 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13054 11775 603 41 0 13013 0
vsize: 52216
[startup+110.001 s]
Raw data (loadavg): 0.97 0.96 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 13822 0 0 0 10964 36 0 0 25 0 1 0 485509941 58068992 12912 4294967295 134512640 134672761 3221224544 3221223688 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14177 12912 603 41 0 14136 0
vsize: 56708
[startup+120.001 s]
Raw data (loadavg): 0.97 0.96 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 14147 0 0 0 11963 37 0 0 25 0 1 0 485509941 59518976 13237 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14531 13237 603 41 0 14490 0
vsize: 58124
[startup+130.001 s]
Raw data (loadavg): 0.97 0.96 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 14545 0 0 0 12962 39 0 0 25 0 1 0 485509941 61231104 13635 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14949 13635 603 41 0 14908 0
vsize: 59796
[startup+140.001 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 14844 0 0 0 13961 40 0 0 25 0 1 0 485509941 62410752 13934 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15237 13934 603 41 0 15196 0
vsize: 60948
[startup+150.001 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 15123 0 0 0 14960 41 0 0 25 0 1 0 485509941 63467520 14213 4294967295 134512640 134672761 3221224544 3221223680 134614713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15495 14213 603 41 0 15454 0
vsize: 61980
[startup+160.001 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 15441 0 0 0 15959 42 0 0 25 0 1 0 485509941 64786432 14531 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15817 14531 603 41 0 15776 0
vsize: 63268
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 15639 0 0 0 16958 43 0 0 25 0 1 0 485509941 65581056 14729 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16011 14729 603 41 0 15970 0
vsize: 64044
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 15818 0 0 0 17958 43 0 0 25 0 1 0 485509941 66379776 14908 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16206 14908 603 41 0 16165 0
vsize: 64824
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 15979 0 0 0 18958 44 0 0 25 0 1 0 485509941 67039232 15069 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16367 15069 603 41 0 16326 0
vsize: 65468
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 16130 0 0 0 19958 44 0 0 25 0 1 0 485509941 67575808 15220 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16498 15220 603 41 0 16457 0
vsize: 65992
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 16311 0 0 0 20957 44 0 0 25 0 1 0 485509941 68370432 15401 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16692 15401 603 41 0 16651 0
vsize: 66768
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 16623 0 0 0 21957 45 0 0 25 0 1 0 485509941 69570560 15713 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16985 15713 603 41 0 16944 0
vsize: 67940
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 16903 0 0 0 22956 46 0 0 25 0 1 0 485509941 70750208 15993 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17273 15993 603 41 0 17232 0
vsize: 69092
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 17174 0 0 0 23955 47 0 0 25 0 1 0 485509941 71942144 16264 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17564 16264 603 41 0 17523 0
vsize: 70256
[startup+250 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 17488 0 0 0 24954 49 0 0 25 0 1 0 485509941 73134080 16578 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17855 16578 603 41 0 17814 0
vsize: 71420
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 17778 0 0 0 25953 50 0 0 25 0 1 0 485509941 74326016 16868 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18146 16868 603 41 0 18105 0
vsize: 72584
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 18062 0 0 0 26952 51 0 0 25 0 1 0 485509941 75501568 17152 4294967295 134512640 134672761 3221224544 3221223728 134615614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18433 17152 603 41 0 18392 0
vsize: 73732
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 18395 0 0 0 27950 53 0 0 25 0 1 0 485509941 76820480 17485 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18755 17485 603 41 0 18714 0
vsize: 75020
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 18705 0 0 0 28949 54 0 0 25 0 1 0 485509941 78147584 17795 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19079 17795 603 41 0 19038 0
vsize: 76316
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 18958 0 0 0 29949 54 0 0 25 0 1 0 485509941 79208448 18048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19338 18048 603 41 0 19297 0
vsize: 77352
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 19207 0 0 0 30949 55 0 0 25 0 1 0 485509941 80130048 18297 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19563 18297 603 41 0 19522 0
vsize: 78252
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 19478 0 0 0 31948 56 0 0 25 0 1 0 485509941 81313792 18568 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19852 18568 603 41 0 19811 0
vsize: 79408
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 19752 0 0 0 32947 57 0 0 25 0 1 0 485509941 82370560 18842 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20110 18842 603 41 0 20069 0
vsize: 80440
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 20039 0 0 0 33946 58 0 0 25 0 1 0 485509941 83566592 19129 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20402 19129 603 41 0 20361 0
vsize: 81608
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 20369 0 0 0 34945 60 0 0 25 0 1 0 485509941 84885504 19459 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20724 19459 603 41 0 20683 0
vsize: 82896
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 20693 0 0 0 35944 61 0 0 25 0 1 0 485509941 86478848 19783 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21113 19783 603 41 0 21072 0
vsize: 84452
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 20955 0 0 0 36943 61 0 0 25 0 1 0 485509941 87535616 20045 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21371 20045 603 41 0 21330 0
vsize: 85484
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 21278 0 0 0 37942 63 0 0 25 0 1 0 485509941 88850432 20368 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21692 20368 603 41 0 21651 0
vsize: 86768
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 21592 0 0 0 38942 63 0 0 25 0 1 0 485509941 90185728 20682 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22018 20682 603 41 0 21977 0
vsize: 88072
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 21919 0 0 0 39941 64 0 0 25 0 1 0 485509941 91521024 21009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22344 21009 603 41 0 22303 0
vsize: 89376
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 22224 0 0 0 40940 65 0 0 25 0 1 0 485509941 92708864 21314 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22634 21314 603 41 0 22593 0
vsize: 90536
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 22505 0 0 0 41939 66 0 0 25 0 1 0 485509941 93892608 21595 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22923 21595 603 41 0 22882 0
vsize: 91692
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 22784 0 0 0 42938 67 0 0 25 0 1 0 485509941 95076352 21874 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23212 21874 603 41 0 23171 0
vsize: 92848
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 23093 0 0 0 43938 68 0 0 25 0 1 0 485509941 96268288 22183 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23503 22183 603 41 0 23462 0
vsize: 94012
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 23385 0 0 0 44937 69 0 0 25 0 1 0 485509941 97468416 22475 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23796 22475 603 41 0 23755 0
vsize: 95184
[startup+460.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 23664 0 0 0 45937 69 0 0 25 0 1 0 485509941 98701312 22754 4294967295 134512640 134672761 3221224544 3221223728 134615761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24097 22754 603 41 0 24056 0
vsize: 96388
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 23933 0 0 0 46936 70 0 0 25 0 1 0 485509941 99762176 23023 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24356 23023 603 41 0 24315 0
vsize: 97424
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 24181 0 0 0 47935 71 0 0 25 0 1 0 485509941 100818944 23271 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24614 23271 603 41 0 24573 0
vsize: 98456
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 24424 0 0 0 48935 72 0 0 25 0 1 0 485509941 101744640 23514 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24840 23514 603 41 0 24799 0
vsize: 99360
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 24704 0 0 0 49934 73 0 0 25 0 1 0 485509941 102940672 23794 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25132 23794 603 41 0 25091 0
vsize: 100528
[startup+510.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 24955 0 0 0 50933 75 0 0 25 0 1 0 485509941 103890944 24045 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25364 24045 603 41 0 25323 0
vsize: 101456
[startup+520.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 25684 0 0 0 51931 76 0 0 25 0 1 0 485509941 106942464 24774 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26109 24774 603 41 0 26068 0
vsize: 104436
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 25867 0 0 0 52931 76 0 0 25 0 1 0 485509941 107614208 24957 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26273 24957 603 41 0 26232 0
vsize: 105092
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 26028 0 0 0 53931 77 0 0 25 0 1 0 485509941 108277760 25118 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26435 25118 603 41 0 26394 0
vsize: 105740
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 26223 0 0 0 54930 78 0 0 25 0 1 0 485509941 109064192 25313 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26627 25313 603 41 0 26586 0
vsize: 106508
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 26407 0 0 0 55929 79 0 0 25 0 1 0 485509941 109858816 25497 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26821 25497 603 41 0 26780 0
vsize: 107284
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 26594 0 0 0 56929 79 0 0 25 0 1 0 485509941 110653440 25684 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27015 25684 603 41 0 26974 0
vsize: 108060
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 26781 0 0 0 57928 80 0 0 25 0 1 0 485509941 111452160 25871 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27210 25871 603 41 0 27169 0
vsize: 108840
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 26956 0 0 0 58928 81 0 0 25 0 1 0 485509941 112107520 26046 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27370 26046 603 41 0 27329 0
vsize: 109480
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 27237 0 0 0 59927 82 0 0 25 0 1 0 485509941 113299456 26327 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27661 26327 603 41 0 27620 0
vsize: 110644
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 27432 0 0 0 60927 82 0 0 25 0 1 0 485509941 114089984 26522 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27854 26522 603 41 0 27813 0
vsize: 111416
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 27762 0 0 0 61926 83 0 0 25 0 1 0 485509941 115400704 26852 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28174 26852 603 41 0 28133 0
vsize: 112696
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 28648 0 0 0 62925 84 0 0 25 0 1 0 485509941 119066624 27738 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29069 27738 603 41 0 29028 0
vsize: 116276
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 29341 0 0 0 63923 87 0 0 25 0 1 0 485509941 121856000 28431 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29750 28431 603 41 0 29709 0
vsize: 119000
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 29514 0 0 0 64923 87 0 0 25 0 1 0 485509941 122519552 28604 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29912 28604 603 41 0 29871 0
vsize: 119648
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 29799 0 0 0 65922 88 0 0 25 0 1 0 485509941 123715584 28889 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30204 28889 603 41 0 30163 0
vsize: 120816
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 30137 0 0 0 66921 89 0 0 25 0 1 0 485509941 125034496 29227 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30526 29227 603 41 0 30485 0
vsize: 122104
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 30467 0 0 0 67920 90 0 0 25 0 1 0 485509941 126492672 29557 4294967295 134512640 134672761 3221224544 3221223728 134615508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30882 29557 603 41 0 30841 0
vsize: 123528
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 30795 0 0 0 68920 91 0 0 25 0 1 0 485509941 127819776 29885 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31206 29885 603 41 0 31165 0
vsize: 124824
[startup+700.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 31115 0 0 0 69919 91 0 0 25 0 1 0 485509941 129142784 30205 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31529 30205 603 41 0 31488 0
vsize: 126116
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 31445 0 0 0 70918 93 0 0 25 0 1 0 485509941 130465792 30535 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31852 30535 603 41 0 31811 0
vsize: 127408
[startup+720.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 31852 0 0 0 71917 94 0 0 25 0 1 0 485509941 132059136 30942 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32241 30942 603 41 0 32200 0
vsize: 128964
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 32244 0 0 0 72916 95 0 0 25 0 1 0 485509941 133640192 31334 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32627 31334 603 41 0 32586 0
vsize: 130508
[startup+740.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 32661 0 0 0 73915 97 0 0 25 0 1 0 485509941 135479296 31751 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33076 31751 603 41 0 33035 0
vsize: 132304
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 33035 0 0 0 74913 99 0 0 25 0 1 0 485509941 136921088 32125 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33428 32125 603 41 0 33387 0
vsize: 133712
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 33451 0 0 0 75912 100 0 0 25 0 1 0 485509941 138637312 32541 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33847 32541 603 41 0 33806 0
vsize: 135388
[startup+770.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 33738 0 0 0 76912 100 0 0 25 0 1 0 485509941 139833344 32828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34139 32828 603 41 0 34098 0
vsize: 136556
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 34033 0 0 0 77911 101 0 0 25 0 1 0 485509941 141012992 33123 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34427 33123 603 41 0 34386 0
vsize: 137708
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 34318 0 0 0 78911 102 0 0 25 0 1 0 485509941 142192640 33408 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34715 33408 603 41 0 34674 0
vsize: 138860
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 34633 0 0 0 79910 102 0 0 25 0 1 0 485509941 143511552 33723 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35037 33723 603 41 0 34996 0
vsize: 140148
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 34972 0 0 0 80910 103 0 0 25 0 1 0 485509941 144830464 34062 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35359 34062 603 41 0 35318 0
vsize: 141436
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 35251 0 0 0 81909 104 0 0 25 0 1 0 485509941 146558976 34341 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35781 34341 603 41 0 35740 0
vsize: 143124
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 35483 0 0 0 82907 105 0 0 25 0 1 0 485509941 147480576 34573 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36006 34573 603 41 0 35965 0
vsize: 144024
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 35790 0 0 0 83906 106 0 0 25 0 1 0 485509941 148799488 34880 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36328 34880 603 41 0 36287 0
vsize: 145312
[startup+850.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 36060 0 0 0 84905 107 0 0 25 0 1 0 485509941 149856256 35150 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36586 35150 603 41 0 36545 0
vsize: 146344
[startup+860.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 36386 0 0 0 85905 108 0 0 25 0 1 0 485509941 151171072 35476 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36907 35476 603 41 0 36866 0
vsize: 147628
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 36702 0 0 0 86904 109 0 0 25 0 1 0 485509941 152485888 35792 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37228 35792 603 41 0 37187 0
vsize: 148912
[startup+880.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 37014 0 0 0 87903 110 0 0 25 0 1 0 485509941 153673728 36104 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37518 36104 603 41 0 37477 0
vsize: 150072
[startup+890.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 37320 0 0 0 88902 111 0 0 25 0 1 0 485509941 155004928 36410 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37843 36410 603 41 0 37802 0
vsize: 151372
[startup+900.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 37598 0 0 0 89901 112 0 0 25 0 1 0 485509941 156057600 36688 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38100 36688 603 41 0 38059 0
vsize: 152400
[startup+910.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 37854 0 0 0 90900 113 0 0 25 0 1 0 485509941 157118464 36944 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38359 36944 603 41 0 38318 0
vsize: 153436
[startup+920.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 38183 0 0 0 91899 115 0 0 25 0 1 0 485509941 158433280 37273 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38680 37273 603 41 0 38639 0
vsize: 154720
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 38508 0 0 0 92898 116 0 0 25 0 1 0 485509941 159883264 37598 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39034 37598 603 41 0 38993 0
vsize: 156136
[startup+940.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 38813 0 0 0 93897 117 0 0 25 0 1 0 485509941 161071104 37903 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39324 37903 603 41 0 39283 0
vsize: 157296
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 39132 0 0 0 94897 118 0 0 25 0 1 0 485509941 162418688 38222 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39653 38222 603 41 0 39612 0
vsize: 158612
[startup+960.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31301
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 39438 0 0 0 95896 119 0 0 25 0 1 0 485509941 163602432 38528 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39942 38528 603 41 0 39901 0
vsize: 159768
[startup+970.015 s]
Raw data (loadavg): 0.99 0.97 0.96 3/58 31307
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 39728 0 0 0 96895 120 0 0 25 0 1 0 485509941 164794368 38818 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40233 38818 603 41 0 40192 0
vsize: 160932
[startup+980.015 s]
Raw data (loadavg): 1.15 1.00 0.97 2/54 31354
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 39995 0 0 0 97894 121 0 0 25 0 1 0 485509941 165867520 39085 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40495 39085 603 41 0 40454 0
vsize: 161980
[startup+990.016 s]
Raw data (loadavg): 1.12 1.00 0.97 2/54 31354
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 40283 0 0 0 98893 122 0 0 25 0 1 0 485509941 167063552 39373 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40787 39373 603 41 0 40746 0
vsize: 163148
[startup+1000.02 s]
Raw data (loadavg): 1.10 1.00 0.97 2/54 31354
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 40600 0 0 0 99892 123 0 0 25 0 1 0 485509941 168382464 39690 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41109 39690 603 41 0 41068 0
vsize: 164436
[startup+1010.02 s]
Raw data (loadavg): 1.09 1.00 0.97 2/54 31354
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 40917 0 0 0 100891 124 0 0 25 0 1 0 485509941 169713664 40007 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41434 40007 603 41 0 41393 0
vsize: 165736
[startup+1020.02 s]
Raw data (loadavg): 1.07 1.00 0.97 2/54 31354
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 41222 0 0 0 101891 125 0 0 25 0 1 0 485509941 170901504 40312 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41724 40312 603 41 0 41683 0
vsize: 166896
[startup+1030.02 s]
Raw data (loadavg): 1.06 1.00 0.97 2/54 31354
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 41548 0 0 0 102890 126 0 0 25 0 1 0 485509941 172355584 40638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42079 40638 603 41 0 42038 0
vsize: 168316
[startup+1040.02 s]
Raw data (loadavg): 1.05 1.00 0.97 2/54 31354
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 41853 0 0 0 103889 127 0 0 25 0 1 0 485509941 173535232 40943 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42367 40943 603 41 0 42326 0
vsize: 169468
[startup+1050.02 s]
Raw data (loadavg): 1.04 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 42128 0 0 0 104889 128 0 0 25 0 1 0 485509941 174723072 41218 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42657 41218 603 41 0 42616 0
vsize: 170628
[startup+1060.02 s]
Raw data (loadavg): 1.04 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 42413 0 0 0 105888 128 0 0 25 0 1 0 485509941 175812608 41503 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42923 41503 603 41 0 42882 0
vsize: 171692
[startup+1070.02 s]
Raw data (loadavg): 1.03 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 42699 0 0 0 106888 129 0 0 25 0 1 0 485509941 177008640 41789 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43215 41789 603 41 0 43174 0
vsize: 172860
[startup+1080.02 s]
Raw data (loadavg): 1.03 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 42965 0 0 0 107888 129 0 0 25 0 1 0 485509941 178061312 42055 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43472 42055 603 41 0 43431 0
vsize: 173888
[startup+1090.02 s]
Raw data (loadavg): 1.02 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 43244 0 0 0 108887 130 0 0 25 0 1 0 485509941 179249152 42334 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43762 42334 603 41 0 43721 0
vsize: 175048
[startup+1100.02 s]
Raw data (loadavg): 1.02 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 43527 0 0 0 109886 131 0 0 25 0 1 0 485509941 180469760 42617 4294967295 134512640 134672761 3221224544 3221223728 134615843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44060 42617 603 41 0 44019 0
vsize: 176240
[startup+1110.02 s]
Raw data (loadavg): 1.01 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 43828 0 0 0 110886 132 0 0 25 0 1 0 485509941 181653504 42918 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44349 42918 603 41 0 44308 0
vsize: 177396
[startup+1120.02 s]
Raw data (loadavg): 1.01 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 44106 0 0 0 111884 133 0 0 25 0 1 0 485509941 182853632 43196 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44642 43196 603 41 0 44601 0
vsize: 178568
[startup+1130.02 s]
Raw data (loadavg): 1.01 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 44372 0 0 0 112884 134 0 0 25 0 1 0 485509941 183939072 43462 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44907 43462 603 41 0 44866 0
vsize: 179628
[startup+1140.02 s]
Raw data (loadavg): 1.01 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 44611 0 0 0 113883 135 0 0 25 0 1 0 485509941 184864768 43701 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45133 43701 603 41 0 45092 0
vsize: 180532
[startup+1150.02 s]
Raw data (loadavg): 1.01 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 44881 0 0 0 114882 136 0 0 25 0 1 0 485509941 186056704 43971 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45424 43971 603 41 0 45383 0
vsize: 181696
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 45106 0 0 0 115882 137 0 0 25 0 1 0 485509941 186978304 44196 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45649 44196 603 41 0 45608 0
vsize: 182596
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 45356 0 0 0 116881 138 0 0 25 0 1 0 485509941 187895808 44446 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45873 44446 603 41 0 45832 0
vsize: 183492
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 45610 0 0 0 117880 139 0 0 25 0 1 0 485509941 188948480 44700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46130 44700 603 41 0 46089 0
vsize: 184520
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 45844 0 0 0 118879 140 0 0 25 0 1 0 485509941 190005248 44934 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46388 44934 603 41 0 46347 0
vsize: 185552
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/54 31356
Raw data (stat): 31301 (minisat+) R 31300 32461 32460 0 -1 0 46093 0 0 0 119878 141 0 0 25 0 1 0 485509941 191070208 45183 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46648 45183 603 41 0 46607 0
vsize: 186592
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.97 1/54 31356
Raw data (stat): 31301 (minisat+) Z 31300 32461 32460 0 -1 12 46093 0 0 0 119878 150 0 0 25 0 1 0 485509941 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: 0
Real time (s): 1200.11
CPU time (s): 1200.29
CPU user time (s): 1198.79
CPU system time (s): 1.50177
CPU usage (%): 100.015
Max. virtual memory (Kb): 186592
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####