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-aflow30a.opb
MD5SUM	b74fb9cd57e8b4068255c4ac98aa23ca
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3191
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	12800
Number of bits of the biggest number in a constraint	14
Biggest sum of numbers in a constraint	416734
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	1189.12
Number of variables	5932
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	453
Trace number 15501

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 04:41:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17405 boxname=wulflinc2 idbench=1339 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b74fb9cd57e8b4068255c4ac98aa23ca  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-aflow30a.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-aflow30a.opb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-aflow30a.opb
IDLAUNCH: 17405
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        794652 kB
Buffers:         13512 kB
Cached:         203408 kB
SwapCached:          0 kB
Active:          25688 kB
Inactive:       194028 kB
HighTotal:      131008 kB
HighFree:        45920 kB
LowTotal:       903652 kB
LowFree:        748732 kB
SwapTotal:     2097136 kB
SwapFree:      2096988 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            14368 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:01:14 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 17405 7 1200.3 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:   13
c ---[1019]---> BDD-cost:   11
c ---[1018]---> BDD-cost:   11
c ---[1017]---> BDD-cost:   12
c ---[1016]---> BDD-cost:   13
c ---[1015]---> BDD-cost:   12
c ---[1014]---> BDD-cost:   13
c ---[1013]---> BDD-cost:   12
c ---[1012]---> BDD-cost:   13
c ---[1011]---> BDD-cost:   11
c ---[1010]---> BDD-cost:   13
c ---[1009]---> BDD-cost:   13
c ---[1008]---> BDD-cost:   12
c ---[1007]---> BDD-cost:   11
c ---[1006]---> BDD-cost:   12
c ---[1005]---> BDD-cost:   13
c ---[1004]---> BDD-cost:   13
c ---[1002]---> BDD-cost:   13
c ---[1001]---> BDD-cost:   13
c ---[1000]---> BDD-cost:   12
c ---[ 999]---> BDD-cost:   13
c ---[ 998]---> BDD-cost:   13
c ---[ 996]---> BDD-cost:   13
c ---[ 995]---> BDD-cost:   12
c ---[ 993]---> BDD-cost:   12
c ---[ 992]---> BDD-cost:   13
c ---[ 991]---> BDD-cost:   12
c ---[ 990]---> BDD-cost:   13
c ---[ 989]---> BDD-cost:   12
c ---[ 988]---> BDD-cost:   12
c ---[ 987]---> BDD-cost:   13
c ---[ 986]---> BDD-cost:   13
c ---[ 985]---> BDD-cost:   12
c ---[ 984]---> BDD-cost:   13
c ---[ 981]---> BDD-cost:   13
c ---[ 980]---> BDD-cost:   11
c ---[ 978]---> BDD-cost:   13
c ---[ 977]---> BDD-cost:   12
c ---[ 974]---> BDD-cost:   10
c ---[ 973]---> BDD-cost:   12
c ---[ 972]---> BDD-cost:   11
c ---[ 971]---> BDD-cost:   13
c ---[ 970]---> BDD-cost:   10
c ---[ 969]---> BDD-cost:   13
c ---[ 968]---> BDD-cost:   13
c ---[ 967]---> BDD-cost:   13
c ---[ 966]---> BDD-cost:   12
c ---[ 964]---> BDD-cost:   13
c ---[ 963]---> BDD-cost:   13
c ---[ 962]---> BDD-cost:   12
c ---[ 961]---> BDD-cost:   10
c ---[ 960]---> BDD-cost:   13
c ---[ 959]---> BDD-cost:   10
c ---[ 958]---> BDD-cost:   13
c ---[ 956]---> BDD-cost:   12
c ---[ 955]---> BDD-cost:   13
c ---[ 954]---> BDD-cost:   11
c ---[ 953]---> BDD-cost:   13
c ---[ 952]---> BDD-cost:   13
c ---[ 951]---> BDD-cost:   11
c ---[ 950]---> BDD-cost:   13
c ---[ 949]---> BDD-cost:   13
c ---[ 948]---> BDD-cost:   13
c ---[ 947]---> BDD-cost:   13
c ---[ 946]---> BDD-cost:   13
c ---[ 945]---> BDD-cost:   13
c ---[ 944]---> BDD-cost:   12
c ---[ 943]---> BDD-cost:   13
c ---[ 942]---> BDD-cost:   13
c ---[ 941]---> BDD-cost:   11
c ---[ 940]---> BDD-cost:   13
c ---[ 939]---> BDD-cost:   13
c ---[ 937]---> BDD-cost:   13
c ---[ 936]---> BDD-cost:   12
c ---[ 935]---> BDD-cost:   10
c ---[ 934]---> BDD-cost:   13
c ---[ 933]---> BDD-cost:   10
c ---[ 932]---> BDD-cost:   12
c ---[ 931]---> BDD-cost:   12
c ---[ 930]---> BDD-cost:   13
c ---[ 928]---> BDD-cost:   11
c ---[ 927]---> BDD-cost:   13
c ---[ 926]---> BDD-cost:   13
c ---[ 925]---> BDD-cost:   13
c ---[ 924]---> BDD-cost:   13
c ---[ 923]---> BDD-cost:   11
c ---[ 922]---> BDD-cost:   12
c ---[ 921]---> BDD-cost:   12
c ---[ 919]---> BDD-cost:   12
c ---[ 918]---> BDD-cost:   12
c ---[ 917]---> BDD-cost:   13
c ---[ 916]---> BDD-cost:   10
c ---[ 915]---> BDD-cost:   12
c ---[ 914]---> BDD-cost:   13
c ---[ 913]---> BDD-cost:   13
c ---[ 912]---> BDD-cost:   13
c ---[ 911]---> BDD-cost:   13
c ---[ 910]---> BDD-cost:   12
c ---[ 908]---> BDD-cost:   13
c ---[ 907]---> BDD-cost:   13
c ---[ 906]---> BDD-cost:   12
c ---[ 905]---> BDD-cost:   13
c ---[ 903]---> BDD-cost:   13
c ---[ 902]---> BDD-cost:   13
c ---[ 900]---> BDD-cost:   13
c ---[ 899]---> BDD-cost:   10
c ---[ 898]---> BDD-cost:   12
c ---[ 897]---> BDD-cost:   12
c ---[ 896]---> BDD-cost:   12
c ---[ 895]---> BDD-cost:   13
c ---[ 893]---> BDD-cost:   12
c ---[ 892]---> BDD-cost:   13
c ---[ 891]---> BDD-cost:   11
c ---[ 890]---> BDD-cost:   13
c ---[ 889]---> BDD-cost:   13
c ---[ 888]---> BDD-cost:   13
c ---[ 887]---> BDD-cost:   13
c ---[ 886]---> BDD-cost:   11
c ---[ 885]---> BDD-cost:   13
c ---[ 883]---> BDD-cost:   10
c ---[ 882]---> BDD-cost:   11
c ---[ 881]---> BDD-cost:   13
c ---[ 880]---> BDD-cost:   13
c ---[ 879]---> BDD-cost:   13
c ---[ 878]---> BDD-cost:   12
c ---[ 877]---> BDD-cost:   11
c ---[ 876]---> BDD-cost:   10
c ---[ 875]---> BDD-cost:   13
c ---[ 874]---> BDD-cost:   13
c ---[ 873]---> BDD-cost:   11
c ---[ 871]---> BDD-cost:   12
c ---[ 870]---> BDD-cost:   13
c ---[ 869]---> BDD-cost:   12
c ---[ 867]---> BDD-cost:   11
c ---[ 866]---> BDD-cost:   13
c ---[ 865]---> BDD-cost:   13
c ---[ 863]---> BDD-cost:   13
c ---[ 862]---> BDD-cost:   13
c ---[ 861]---> BDD-cost:   12
c ---[ 860]---> BDD-cost:   13
c ---[ 859]---> BDD-cost:   12
c ---[ 858]---> BDD-cost:   13
c ---[ 857]---> BDD-cost:   12
c ---[ 856]---> BDD-cost:   13
c ---[ 855]---> BDD-cost:   12
c ---[ 853]---> BDD-cost:   13
c ---[ 851]---> BDD-cost:   13
c ---[ 850]---> BDD-cost:   12
c ---[ 849]---> BDD-cost:   11
c ---[ 848]---> BDD-cost:   12
c ---[ 847]---> BDD-cost:   13
c ---[ 846]---> BDD-cost:   12
c ---[ 845]---> BDD-cost:   13
c ---[ 844]---> BDD-cost:   12
c ---[ 843]---> BDD-cost:   12
c ---[ 842]---> BDD-cost:   11
c ---[ 841]---> BDD-cost:   11
c ---[ 840]---> BDD-cost:   10
c ---[ 839]---> BDD-cost:   13
c ---[ 837]---> BDD-cost:   10
c ---[ 836]---> BDD-cost:   12
c ---[ 835]---> BDD-cost:   13
c ---[ 834]---> BDD-cost:   13
c ---[ 833]---> BDD-cost:   13
c ---[ 832]---> BDD-cost:   13
c ---[ 831]---> BDD-cost:   13
c ---[ 829]---> BDD-cost:   13
c ---[ 828]---> BDD-cost:   12
c ---[ 825]---> BDD-cost:   11
c ---[ 824]---> BDD-cost:   13
c ---[ 823]---> BDD-cost:   13
c ---[ 822]---> BDD-cost:   12
c ---[ 821]---> BDD-cost:   13
c ---[ 820]---> BDD-cost:   13
c ---[ 819]---> BDD-cost:   13
c ---[ 818]---> BDD-cost:   13
c ---[ 817]---> BDD-cost:   13
c ---[ 816]---> BDD-cost:   13
c ---[ 815]---> BDD-cost:   13
c ---[ 814]---> BDD-cost:   10
c ---[ 812]---> BDD-cost:   13
c ---[ 811]---> BDD-cost:   11
c ---[ 809]---> BDD-cost:   12
c ---[ 808]---> BDD-cost:   12
c ---[ 807]---> BDD-cost:   13
c ---[ 806]---> BDD-cost:   13
c ---[ 805]---> BDD-cost:   12
c ---[ 804]---> BDD-cost:   12
c ---[ 803]---> BDD-cost:   13
c ---[ 801]---> BDD-cost:   13
c ---[ 800]---> BDD-cost:   13
c ---[ 799]---> BDD-cost:   11
c ---[ 798]---> BDD-cost:   12
c ---[ 797]---> BDD-cost:   13
c ---[ 796]---> BDD-cost:   11
c ---[ 795]---> BDD-cost:   13
c ---[ 793]---> BDD-cost:   12
c ---[ 791]---> BDD-cost:   13
c ---[ 790]---> BDD-cost:   12
c ---[ 789]---> BDD-cost:   11
c ---[ 788]---> BDD-cost:   13
c ---[ 787]---> BDD-cost:   13
c ---[ 786]---> BDD-cost:   13
c ---[ 785]---> BDD-cost:   13
c ---[ 784]---> BDD-cost:   11
c ---[ 782]---> BDD-cost:   10
c ---[ 781]---> BDD-cost:   13
c ---[ 780]---> BDD-cost:   11
c ---[ 779]---> BDD-cost:   13
c ---[ 778]---> BDD-cost:   13
c ---[ 777]---> BDD-cost:   11
c ---[ 776]---> BDD-cost:   11
c ---[ 774]---> BDD-cost:   13
c ---[ 772]---> BDD-cost:   12
c ---[ 771]---> BDD-cost:   13
c ---[ 770]---> BDD-cost:   13
c ---[ 769]---> BDD-cost:   13
c ---[ 768]---> BDD-cost:   13
c ---[ 767]---> BDD-cost:   11
c ---[ 766]---> BDD-cost:   13
c ---[ 764]---> BDD-cost:   13
c ---[ 763]---> BDD-cost:   10
c ---[ 762]---> BDD-cost:   13
c ---[ 761]---> BDD-cost:   13
c ---[ 760]---> BDD-cost:   13
c ---[ 759]---> BDD-cost:   12
c ---[ 758]---> BDD-cost:   12
c ---[ 757]---> BDD-cost:   11
c ---[ 756]---> BDD-cost:   12
c ---[ 754]---> BDD-cost:   10
c ---[ 753]---> BDD-cost:   13
c ---[ 752]---> BDD-cost:   13
c ---[ 751]---> BDD-cost:   10
c ---[ 750]---> BDD-cost:   12
c ---[ 749]---> BDD-cost:   13
c ---[ 747]---> BDD-cost:   12
c ---[ 746]---> BDD-cost:   12
c ---[ 745]---> BDD-cost:   12
c ---[ 744]---> BDD-cost:   11
c ---[ 743]---> BDD-cost:   12
c ---[ 742]---> BDD-cost:   13
c ---[ 741]---> BDD-cost:   11
c ---[ 740]---> BDD-cost:   12
c ---[ 738]---> BDD-cost:   12
c ---[ 737]---> BDD-cost:   12
c ---[ 736]---> BDD-cost:   12
c ---[ 734]---> BDD-cost:   11
c ---[ 733]---> BDD-cost:   12
c ---[ 732]---> BDD-cost:   11
c ---[ 730]---> BDD-cost:   12
c ---[ 729]---> BDD-cost:   10
c ---[ 728]---> BDD-cost:   12
c ---[ 727]---> BDD-cost:   12
c ---[ 726]---> BDD-cost:   12
c ---[ 725]---> BDD-cost:   11
c ---[ 723]---> BDD-cost:   13
c ---[ 722]---> BDD-cost:   12
c ---[ 721]---> BDD-cost:   13
c ---[ 720]---> BDD-cost:   13
c ---[ 719]---> BDD-cost:   10
c ---[ 718]---> BDD-cost:   13
c ---[ 717]---> BDD-cost:   12
c ---[ 716]---> BDD-cost:   11
c ---[ 713]---> BDD-cost:   12
c ---[ 712]---> BDD-cost:   11
c ---[ 711]---> BDD-cost:   12
c ---[ 710]---> BDD-cost:   12
c ---[ 708]---> BDD-cost:   13
c ---[ 706]---> BDD-cost:   13
c ---[ 705]---> BDD-cost:   13
c ---[ 704]---> BDD-cost:   10
c ---[ 703]---> BDD-cost:   13
c ---[ 702]---> BDD-cost:   13
c ---[ 701]---> BDD-cost:   13
c ---[ 700]---> BDD-cost:   13
c ---[ 699]---> BDD-cost:   12
c ---[ 698]---> BDD-cost:   13
c ---[ 695]---> BDD-cost:   11
c ---[ 694]---> BDD-cost:   12
c ---[ 693]---> BDD-cost:   13
c ---[ 692]---> BDD-cost:   13
c ---[ 691]---> BDD-cost:   13
c ---[ 690]---> BDD-cost:   12
c ---[ 688]---> BDD-cost:   12
c ---[ 687]---> BDD-cost:   11
c ---[ 686]---> BDD-cost:   13
c ---[ 684]---> BDD-cost:   13
c ---[ 683]---> BDD-cost:   11
c ---[ 682]---> BDD-cost:   11
c ---[ 681]---> BDD-cost:   13
c ---[ 680]---> BDD-cost:   13
c ---[ 679]---> BDD-cost:   12
c ---[ 678]---> BDD-cost:   12
c ---[ 677]---> BDD-cost:   12
c ---[ 676]---> BDD-cost:   13
c ---[ 675]---> BDD-cost:   12
c ---[ 673]---> BDD-cost:   11
c ---[ 672]---> BDD-cost:   13
c ---[ 671]---> BDD-cost:   13
c ---[ 670]---> BDD-cost:   13
c ---[ 668]---> BDD-cost:   13
c ---[ 667]---> BDD-cost:   13
c ---[ 666]---> BDD-cost:   11
c ---[ 665]---> BDD-cost:   12
c ---[ 664]---> BDD-cost:   12
c ---[ 663]---> BDD-cost:   13
c ---[ 662]---> BDD-cost:   13
c ---[ 661]---> BDD-cost:   12
c ---[ 660]---> BDD-cost:   11
c ---[ 659]---> BDD-cost:   13
c ---[ 658]---> BDD-cost:   13
c ---[ 657]---> BDD-cost:   12
c ---[ 656]---> BDD-cost:   13
c ---[ 655]---> BDD-cost:   12
c ---[ 654]---> BDD-cost:   10
c ---[ 653]---> BDD-cost:   10
c ---[ 651]---> BDD-cost:   12
c ---[ 649]---> BDD-cost:   12
c ---[ 648]---> BDD-cost:   12
c ---[ 647]---> BDD-cost:   13
c ---[ 645]---> BDD-cost:   13
c ---[ 644]---> BDD-cost:   10
c ---[ 643]---> BDD-cost:   13
c ---[ 642]---> BDD-cost:   13
c ---[ 640]---> BDD-cost:   12
c ---[ 638]---> BDD-cost:   13
c ---[ 637]---> BDD-cost:   12
c ---[ 636]---> BDD-cost:   13
c ---[ 635]---> BDD-cost:   12
c ---[ 634]---> BDD-cost:   11
c ---[ 633]---> BDD-cost:   12
c ---[ 632]---> BDD-cost:   13
c ---[ 631]---> BDD-cost:   12
c ---[ 630]---> BDD-cost:   13
c ---[ 628]---> BDD-cost:   12
c ---[ 627]---> BDD-cost:   13
c ---[ 625]---> BDD-cost:   13
c ---[ 624]---> BDD-cost:   13
c ---[ 623]---> BDD-cost:   12
c ---[ 622]---> BDD-cost:   12
c ---[ 621]---> BDD-cost:   10
c ---[ 620]---> BDD-cost:   12
c ---[ 619]---> BDD-cost:   13
c ---[ 618]---> BDD-cost:   11
c ---[ 617]---> BDD-cost:   11
c ---[ 616]---> BDD-cost:   13
c ---[ 615]---> BDD-cost:   13
c ---[ 614]---> BDD-cost:   10
c ---[ 613]---> BDD-cost:   12
c ---[ 608]---> BDD-cost:   12
c ---[ 607]---> BDD-cost:   13
c ---[ 606]---> BDD-cost:   11
c ---[ 605]---> BDD-cost:   13
c ---[ 604]---> BDD-cost:   11
c ---[ 603]---> BDD-cost:   13
c ---[ 602]---> BDD-cost:   13
c ---[ 601]---> BDD-cost:   13
c ---[ 600]---> BDD-cost:   10
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:   18
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:   15
c ---[ 552]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    8
c ---[ 548]---> BDD-cost:   19
c ---[ 547]---> BDD-cost:   17
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:   16
c ---[ 534]---> BDD-cost:    7
c ---[ 533]---> BDD-cost:   15
c ---[ 532]---> BDD-cost:    8
c ---[ 531]---> BDD-cost:    6
c ---[ 530]---> BDD-cost:   15
c ---[ 529]---> BDD-cost:    7
c ---[ 528]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:    7
c ---[ 526]---> BDD-cost:   17
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:   18
c ---[ 496]---> BDD-cost:    8
c ---[ 495]---> BDD-cost:    5
c ---[ 494]---> BDD-cost:   15
c ---[ 493]---> BDD-cost:   18
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:   16
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:   18
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:   17
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:   16
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:   17
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:   17
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:   17
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:   17
c ---[ 388]---> BDD-cost:   17
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:   16
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:   16
c ---[ 359]---> BDD-cost:    7
c ---[ 358]---> BDD-cost:    6
c ---[ 357]---> BDD-cost:    8
c ---[ 356]---> BDD-cost:   14
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> Adder-cost: 693   maxlim: 102262   bits: 18/17
c ---[ 351]---> BDD-cost:    8
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    4
c ---[ 348]---> BDD-cost:   19
c ---[ 347]---> BDD-cost:   15
c ---[ 346]---> BDD-cost:    6
c ---[ 345]---> BDD-cost:   17
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:   14
c ---[ 342]---> BDD-cost:    6
c ---[ 340]---> Adder-cost: 572   maxlim: 148723   bits: 18/18
c ---[ 339]---> BDD-cost:    7
c ---[ 338]---> BDD-cost:    7
c ---[ 337]---> BDD-cost:    8
c ---[ 336]---> BDD-cost:   17
c ---[ 335]---> BDD-cost:    7
c ---[ 334]---> BDD-cost:    8
c ---[ 333]---> BDD-cost:   19
c ---[ 332]---> BDD-cost:   16
c ---[ 331]---> BDD-cost:   19
c ---[ 330]---> BDD-cost:    3
c ---[ 328]---> Adder-cost: 880   maxlim: 181231   bits: 19/18
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: 820   maxlim: 146161   bits: 19/18
c ---[ 315]---> BDD-cost:    4
c ---[ 314]---> BDD-cost:    7
c ---[ 313]---> BDD-cost:   16
c ---[ 312]---> BDD-cost:   16
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:   19
c ---[ 304]---> Adder-cost: 838   maxlim: 185456   bits: 19/18
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:   19
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 298]---> BDD-cost:   14
c ---[ 297]---> BDD-cost:    3
c ---[ 296]---> BDD-cost:    7
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    5
c ---[ 292]---> Adder-cost: 546   maxlim: 93302   bits: 18/17
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:   19
c ---[ 285]---> BDD-cost:    5
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:    5
c ---[ 282]---> BDD-cost:    8
c ---[ 280]---> Adder-cost: 720   maxlim: 163185   bits: 19/18
c ---[ 279]---> BDD-cost:    7
c ---[ 278]---> BDD-cost:    8
c ---[ 277]---> BDD-cost:    7
c ---[ 276]---> BDD-cost:    4
c ---[ 275]---> BDD-cost:   15
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: 768   maxlim: 162802   bits: 19/18
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:   17
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    8
c ---[ 261]---> BDD-cost:    7
c ---[ 260]---> BDD-cost:   19
c ---[ 259]---> BDD-cost:   19
c ---[ 258]---> BDD-cost:    6
c ---[ 256]---> Adder-cost: 800   maxlim: 202094   bits: 19/18
c ---[ 255]---> BDD-cost:    5
c ---[ 254]---> BDD-cost:    5
c ---[ 253]---> BDD-cost:    7
c ---[ 252]---> BDD-cost:   14
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:    5
c ---[ 249]---> BDD-cost:    7
c ---[ 248]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:   17
c ---[ 246]---> BDD-cost:    7
c ---[ 244]---> Adder-cost: 670   maxlim: 163442   bits: 19/18
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:   19
c ---[ 232]---> BDD-cost:   27
c ---[ 230]---> Adder-cost: 706   maxlim: 157169   bits: 19/18
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:   19
c ---[ 223]---> BDD-cost:    6
c ---[ 222]---> BDD-cost:   18
c ---[ 221]---> BDD-cost:    7
c ---[ 220]---> BDD-cost:    7
c ---[ 218]---> Adder-cost: 762   maxlim: 147056   bits: 19/18
c ---[ 217]---> BDD-cost:    5
c ---[ 216]---> BDD-cost:   17
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: 759   maxlim: 130929   bits: 18/17
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    7
c ---[ 203]---> BDD-cost:   15
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   17
c ---[ 200]---> BDD-cost:    3
c ---[ 199]---> BDD-cost:    6
c ---[ 198]---> BDD-cost:    8
c ---[ 197]---> BDD-cost:   19
c ---[ 196]---> BDD-cost:    8
c ---[ 194]---> Adder-cost: 696   maxlim: 101365   bits: 18/17
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:   18
c ---[ 185]---> BDD-cost:    7
c ---[ 184]---> BDD-cost:    3
c ---[ 182]---> Adder-cost: 614   maxlim: 144627   bits: 19/18
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: 764   maxlim: 174961   bits: 19/18
c ---[ 169]---> BDD-cost:    7
c ---[ 168]---> BDD-cost:   17
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:   17
c ---[ 158]---> Adder-cost: 548   maxlim: 159603   bits: 18/18
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:   19
c ---[ 148]---> BDD-cost:    8
c ---[ 146]---> Adder-cost: 824   maxlim: 173423   bits: 19/18
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:   17
c ---[ 138]---> BDD-cost:    7
c ---[ 137]---> BDD-cost:    6
c ---[ 136]---> BDD-cost:    8
c ---[ 134]---> Adder-cost: 858   maxlim: 137074   bits: 19/18
c ---[ 132]---> Adder-cost: 786   maxlim: 177902   bits: 19/18
c ---[ 130]---> BDD-cost:   29
c ---[ 128]---> Adder-cost: 602   maxlim: 120053   bits: 18/17
c ---[ 126]---> Adder-cost: 646   maxlim: 154865   bits: 18/18
c ---[ 124]---> Adder-cost: 864   maxlim: 214125   bits: 19/18
c ---[ 122]---> Adder-cost: 710   maxlim: 143089   bits: 19/18
c ---[ 120]---> Adder-cost: 614   maxlim: 83701   bits: 18/17
c ---[ 118]---> Adder-cost: 706   maxlim: 144239   bits: 19/18
c ---[ 116]---> Adder-cost: 826   maxlim: 169330   bits: 19/18
c ---[ 114]---> Adder-cost: 604   maxlim: 130932   bits: 18/17
c ---[ 112]---> Adder-cost: 816   maxlim: 175726   bits: 19/18
c ---[ 111]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:    5
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:   17
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:   18
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:   19
c ---[  77]---> BDD-cost:    3
c ---[  76]---> BDD-cost:    6
c ---[  75]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   33
c ---[  72]---> BDD-cost:    5
c ---[  71]---> BDD-cost:   16
c ---[  70]---> BDD-cost:    5
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:   16
c ---[  67]---> BDD-cost:   19
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 ---#### 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.75 0.89 0.93 2/54 19596
Raw data (stat): 19596 (runsolver) R 19595 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484057861 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.79 0.89 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 6793 0 0 0 979 18 0 0 25 0 1 0 484057861 28950528 6193 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7068 6193 603 41 0 7027 0
vsize: 28272
[startup+20.0011 s]
Raw data (loadavg): 0.82 0.89 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 7130 0 0 0 1978 19 0 0 25 0 1 0 484057861 30396416 6530 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7421 6530 603 41 0 7380 0
vsize: 29684
[startup+30.0014 s]
Raw data (loadavg): 0.85 0.90 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 7455 0 0 0 2978 20 0 0 25 0 1 0 484057861 31711232 6855 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7742 6855 603 41 0 7701 0
vsize: 30968
[startup+40.001 s]
Raw data (loadavg): 0.87 0.90 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 7837 0 0 0 3977 21 0 0 25 0 1 0 484057861 33165312 7237 4294967295 134512640 134672761 3221224544 3221223584 134613815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8097 7237 603 41 0 8056 0
vsize: 32388
[startup+50.002 s]
Raw data (loadavg): 0.89 0.90 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 8350 0 0 0 4976 23 0 0 25 0 1 0 484057861 35364864 7750 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8634 7750 603 41 0 8593 0
vsize: 34536
[startup+60.0014 s]
Raw data (loadavg): 0.91 0.91 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 9411 0 0 0 5973 26 0 0 25 0 1 0 484057861 39649280 8811 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9680 8811 603 41 0 9639 0
vsize: 38720
[startup+70.002 s]
Raw data (loadavg): 0.92 0.91 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 9676 0 0 0 6972 27 0 0 25 0 1 0 484057861 40706048 9076 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9938 9076 603 41 0 9897 0
vsize: 39752
[startup+80.003 s]
Raw data (loadavg): 0.93 0.91 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 10079 0 0 0 7971 28 0 0 25 0 1 0 484057861 42434560 9479 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10360 9479 603 41 0 10319 0
vsize: 41440
[startup+90.0023 s]
Raw data (loadavg): 0.94 0.91 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 10605 0 0 0 8970 29 0 0 25 0 1 0 484057861 44691456 10005 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10911 10005 603 41 0 10870 0
vsize: 43644
[startup+100.002 s]
Raw data (loadavg): 0.95 0.92 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 11171 0 0 0 9968 31 0 0 25 0 1 0 484057861 47063040 10571 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11490 10571 603 41 0 11449 0
vsize: 45960
[startup+110.002 s]
Raw data (loadavg): 0.96 0.92 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 11499 0 0 0 10967 32 0 0 25 0 1 0 484057861 48398336 10899 4294967295 134512640 134672761 3221224544 3221223728 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11816 10899 603 41 0 11775 0
vsize: 47264
[startup+120.002 s]
Raw data (loadavg): 0.96 0.92 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 12682 0 0 0 11964 36 0 0 25 0 1 0 484057861 53170176 12082 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12981 12082 603 41 0 12940 0
vsize: 51924
[startup+130.002 s]
Raw data (loadavg): 0.97 0.92 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 13075 0 0 0 12963 37 0 0 25 0 1 0 484057861 54763520 12475 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13370 12475 603 41 0 13329 0
vsize: 53480
[startup+140.002 s]
Raw data (loadavg): 0.97 0.92 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 13459 0 0 0 13962 39 0 0 25 0 1 0 484057861 56352768 12859 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13758 12859 603 41 0 13717 0
vsize: 55032
[startup+150.002 s]
Raw data (loadavg): 0.98 0.93 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 13799 0 0 0 14961 40 0 0 25 0 1 0 484057861 57679872 13199 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14082 13199 603 41 0 14041 0
vsize: 56328
[startup+160.002 s]
Raw data (loadavg): 0.98 0.93 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 14199 0 0 0 15960 41 0 0 25 0 1 0 484057861 59383808 13599 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14498 13599 603 41 0 14457 0
vsize: 57992
[startup+170.003 s]
Raw data (loadavg): 0.98 0.93 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 14560 0 0 0 16960 41 0 0 25 0 1 0 484057861 60833792 13960 4294967295 134512640 134672761 3221224544 3221223744 134610681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14852 13960 603 41 0 14811 0
vsize: 59408
[startup+180.002 s]
Raw data (loadavg): 0.98 0.93 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 14843 0 0 0 17958 43 0 0 25 0 1 0 484057861 62029824 14243 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15144 14243 603 41 0 15103 0
vsize: 60576
[startup+190.002 s]
Raw data (loadavg): 0.99 0.93 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 15178 0 0 0 18957 44 0 0 25 0 1 0 484057861 63352832 14578 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15467 14578 603 41 0 15426 0
vsize: 61868
[startup+200.002 s]
Raw data (loadavg): 0.99 0.94 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 15501 0 0 0 19957 45 0 0 25 0 1 0 484057861 64675840 14901 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15790 14901 603 41 0 15749 0
vsize: 63160
[startup+210.002 s]
Raw data (loadavg): 0.99 0.94 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 15855 0 0 0 20956 46 0 0 25 0 1 0 484057861 66129920 15255 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16145 15255 603 41 0 16104 0
vsize: 64580
[startup+220.002 s]
Raw data (loadavg): 0.99 0.94 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 16207 0 0 0 21954 47 0 0 25 0 1 0 484057861 67592192 15607 4294967295 134512640 134672761 3221224544 3221223744 134610681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16502 15607 603 41 0 16461 0
vsize: 66008
[startup+230.002 s]
Raw data (loadavg): 0.99 0.94 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 16572 0 0 0 22953 49 0 0 25 0 1 0 484057861 69066752 15972 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16862 15972 603 41 0 16821 0
vsize: 67448
[startup+240.001 s]
Raw data (loadavg): 0.99 0.94 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 16946 0 0 0 23952 50 0 0 25 0 1 0 484057861 70541312 16346 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17222 16346 603 41 0 17181 0
vsize: 68888
[startup+250.001 s]
Raw data (loadavg): 0.99 0.94 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 17280 0 0 0 24951 51 0 0 25 0 1 0 484057861 72122368 16680 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17608 16680 603 41 0 17567 0
vsize: 70432
[startup+260.001 s]
Raw data (loadavg): 0.99 0.94 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 17627 0 0 0 25951 52 0 0 25 0 1 0 484057861 73584640 17027 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17965 17027 603 41 0 17924 0
vsize: 71860
[startup+270.002 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 17975 0 0 0 26950 53 0 0 25 0 1 0 484057861 75051008 17375 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18323 17375 603 41 0 18282 0
vsize: 73292
[startup+280.002 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 18282 0 0 0 27949 54 0 0 25 0 1 0 484057861 76234752 17682 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18612 17682 603 41 0 18571 0
vsize: 74448
[startup+290.002 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 18694 0 0 0 28948 55 0 0 25 0 1 0 484057861 77975552 18094 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19037 18094 603 41 0 18996 0
vsize: 76148
[startup+300.002 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 19029 0 0 0 29947 56 0 0 25 0 1 0 484057861 79425536 18429 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19391 18429 603 41 0 19350 0
vsize: 77564
[startup+310.002 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 19352 0 0 0 30946 57 0 0 25 0 1 0 484057861 80760832 18752 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19717 18752 603 41 0 19676 0
vsize: 78868
[startup+320.003 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 19727 0 0 0 31945 59 0 0 25 0 1 0 484057861 82231296 19127 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20076 19127 603 41 0 20035 0
vsize: 80304
[startup+330.004 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 20106 0 0 0 32944 60 0 0 25 0 1 0 484057861 83804160 19506 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20460 19506 603 41 0 20419 0
vsize: 81840
[startup+340.003 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 20480 0 0 0 33943 61 0 0 25 0 1 0 484057861 85377024 19880 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20844 19880 603 41 0 20803 0
vsize: 83376
[startup+350.003 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 20864 0 0 0 34942 62 0 0 25 0 1 0 484057861 86958080 20264 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21230 20264 603 41 0 21189 0
vsize: 84920
[startup+360.003 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 21237 0 0 0 35941 63 0 0 25 0 1 0 484057861 88408064 20637 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21584 20637 603 41 0 21543 0
vsize: 86336
[startup+370.004 s]
Raw data (loadavg): 0.99 0.95 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 21656 0 0 0 36941 64 0 0 25 0 1 0 484057861 90120192 21056 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21056 603 41 0 21961 0
vsize: 88008
[startup+380.004 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 21952 0 0 0 37940 65 0 0 25 0 1 0 484057861 91316224 21352 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22294 21352 603 41 0 22253 0
vsize: 89176
[startup+390.004 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 22118 0 0 0 38939 66 0 0 25 0 1 0 484057861 91979776 21518 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22456 21518 603 41 0 22415 0
vsize: 89824
[startup+400.004 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 22275 0 0 0 39939 66 0 0 25 0 1 0 484057861 92635136 21675 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22616 21675 603 41 0 22575 0
vsize: 90464
[startup+410.004 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 22444 0 0 0 40938 67 0 0 25 0 1 0 484057861 93298688 21844 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22778 21844 603 41 0 22737 0
vsize: 91112
[startup+420.005 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 22650 0 0 0 41937 68 0 0 25 0 1 0 484057861 94232576 22050 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23006 22050 603 41 0 22965 0
vsize: 92024
[startup+430.005 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 22831 0 0 0 42937 69 0 0 25 0 1 0 484057861 94892032 22231 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23167 22231 603 41 0 23126 0
vsize: 92668
[startup+440.005 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 22989 0 0 0 43937 69 0 0 25 0 1 0 484057861 95551488 22389 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23328 22389 603 41 0 23287 0
vsize: 93312
[startup+450.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 23175 0 0 0 44936 70 0 0 25 0 1 0 484057861 96350208 22575 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23523 22575 603 41 0 23482 0
vsize: 94092
[startup+460.006 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 23372 0 0 0 45935 71 0 0 25 0 1 0 484057861 97153024 22772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23719 22772 603 41 0 23678 0
vsize: 94876
[startup+470.007 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 23620 0 0 0 46934 72 0 0 25 0 1 0 484057861 98078720 23020 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23945 23020 603 41 0 23904 0
vsize: 95780
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 23857 0 0 0 47934 73 0 0 25 0 1 0 484057861 99131392 23257 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24202 23257 603 41 0 24161 0
vsize: 96808
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 24090 0 0 0 48933 74 0 0 25 0 1 0 484057861 100061184 23490 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24429 23490 603 41 0 24388 0
vsize: 97716
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 24316 0 0 0 49932 75 0 0 25 0 1 0 484057861 100986880 23716 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24655 23716 603 41 0 24614 0
vsize: 98620
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 24534 0 0 0 50931 76 0 0 25 0 1 0 484057861 101904384 23934 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24879 23934 603 41 0 24838 0
vsize: 99516
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 24716 0 0 0 51931 77 0 0 25 0 1 0 484057861 102567936 24116 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25041 24116 603 41 0 25000 0
vsize: 100164
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 24872 0 0 0 52930 78 0 0 25 0 1 0 484057861 103235584 24272 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25204 24272 603 41 0 25163 0
vsize: 100816
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 25019 0 0 0 53930 78 0 0 25 0 1 0 484057861 103890944 24419 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25364 24419 603 41 0 25323 0
vsize: 101456
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 25192 0 0 0 54930 79 0 0 25 0 1 0 484057861 104550400 24592 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25525 24592 603 41 0 25484 0
vsize: 102100
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 25376 0 0 0 55930 79 0 0 25 0 1 0 484057861 105357312 24776 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25722 24776 603 41 0 25681 0
vsize: 102888
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 25581 0 0 0 56929 80 0 0 25 0 1 0 484057861 106156032 24981 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25917 24981 603 41 0 25876 0
vsize: 103668
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 25795 0 0 0 57928 80 0 0 25 0 1 0 484057861 106950656 25195 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26111 25195 603 41 0 26070 0
vsize: 104444
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 26009 0 0 0 58928 81 0 0 25 0 1 0 484057861 107896832 25409 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26342 25409 603 41 0 26301 0
vsize: 105368
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 26238 0 0 0 59927 82 0 0 25 0 1 0 484057861 108822528 25638 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26568 25638 603 41 0 26527 0
vsize: 106272
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 26475 0 0 0 60926 83 0 0 25 0 1 0 484057861 109756416 25875 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26796 25875 603 41 0 26755 0
vsize: 107184
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 26733 0 0 0 61926 84 0 0 25 0 1 0 484057861 110821376 26133 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27056 26133 603 41 0 27015 0
vsize: 108224
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 26993 0 0 0 62925 85 0 0 25 0 1 0 484057861 111882240 26393 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27315 26393 603 41 0 27274 0
vsize: 109260
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 27321 0 0 0 63925 85 0 0 25 0 1 0 484057861 113217536 26721 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27641 26721 603 41 0 27600 0
vsize: 110564
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 27560 0 0 0 64924 86 0 0 25 0 1 0 484057861 114180096 26960 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27876 26960 603 41 0 27835 0
vsize: 111504
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 27897 0 0 0 65923 87 0 0 25 0 1 0 484057861 115634176 27297 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28231 27297 603 41 0 28190 0
vsize: 112924
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 28282 0 0 0 66922 88 0 0 25 0 1 0 484057861 117219328 27682 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28618 27682 603 41 0 28577 0
vsize: 114472
[startup+680.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 28603 0 0 0 67922 89 0 0 25 0 1 0 484057861 118554624 28003 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28944 28003 603 41 0 28903 0
vsize: 115776
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 28849 0 0 0 68921 90 0 0 25 0 1 0 484057861 119480320 28249 4294967295 134512640 134672761 3221224544 3221223744 134610654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29170 28249 603 41 0 29129 0
vsize: 116680
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 29174 0 0 0 69920 91 0 0 25 0 1 0 484057861 120803328 28574 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29493 28574 603 41 0 29452 0
vsize: 117972
[startup+710.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 29508 0 0 0 70919 93 0 0 25 0 1 0 484057861 122253312 28908 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29847 28908 603 41 0 29806 0
vsize: 119388
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 29787 0 0 0 71918 93 0 0 25 0 1 0 484057861 123838464 29187 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30234 29187 603 41 0 30193 0
vsize: 120936
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 30002 0 0 0 72918 94 0 0 25 0 1 0 484057861 124768256 29402 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30461 29402 603 41 0 30420 0
vsize: 121844
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 30243 0 0 0 73917 94 0 0 25 0 1 0 484057861 125698048 29643 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30688 29643 603 41 0 30647 0
vsize: 122752
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 30510 0 0 0 74917 95 0 0 25 0 1 0 484057861 126758912 29910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30947 29910 603 41 0 30906 0
vsize: 123788
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 30825 0 0 0 75916 96 0 0 25 0 1 0 484057861 128081920 30225 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31270 30225 603 41 0 31229 0
vsize: 125080
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 31111 0 0 0 76916 97 0 0 25 0 1 0 484057861 129269760 30511 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31560 30511 603 41 0 31519 0
vsize: 126240
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 31394 0 0 0 77915 98 0 0 25 0 1 0 484057861 130461696 30794 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31851 30794 603 41 0 31810 0
vsize: 127404
[startup+790.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 31703 0 0 0 78914 99 0 0 25 0 1 0 484057861 131657728 31103 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32143 31103 603 41 0 32102 0
vsize: 128572
[startup+800.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 31984 0 0 0 79913 99 0 0 25 0 1 0 484057861 132849664 31384 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32434 31384 603 41 0 32393 0
vsize: 129736
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 32271 0 0 0 80913 101 0 0 25 0 1 0 484057861 134041600 31671 4294967295 134512640 134672761 3221224544 3221223744 134610528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32725 31671 603 41 0 32684 0
vsize: 130900
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 32555 0 0 0 81912 101 0 0 25 0 1 0 484057861 135102464 31955 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32984 31955 603 41 0 32943 0
vsize: 131936
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 32813 0 0 0 82912 102 0 0 25 0 1 0 484057861 136171520 32213 4294967295 134512640 134672761 3221224544 3221223728 134616005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33245 32213 603 41 0 33204 0
vsize: 132980
[startup+840.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 33085 0 0 0 83911 103 0 0 25 0 1 0 484057861 137363456 32485 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33536 32485 603 41 0 33495 0
vsize: 134144
[startup+850.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 33350 0 0 0 84910 103 0 0 25 0 1 0 484057861 138420224 32750 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33794 32750 603 41 0 33753 0
vsize: 135176
[startup+860.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 33598 0 0 0 85910 104 0 0 25 0 1 0 484057861 139395072 32998 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34032 32998 603 41 0 33991 0
vsize: 136128
[startup+870.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 33849 0 0 0 86909 105 0 0 25 0 1 0 484057861 140468224 33249 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34294 33249 603 41 0 34253 0
vsize: 137176
[startup+880.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 34106 0 0 0 87908 106 0 0 25 0 1 0 484057861 141524992 33506 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34552 33506 603 41 0 34511 0
vsize: 138208
[startup+890.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 34547 0 0 0 88908 107 0 0 25 0 1 0 484057861 143261696 33947 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34976 33947 603 41 0 34935 0
vsize: 139904
[startup+900.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 34672 0 0 0 89908 107 0 0 25 0 1 0 484057861 143798272 34072 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35107 34072 603 41 0 35066 0
vsize: 140428
[startup+910.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 34825 0 0 0 90908 107 0 0 25 0 1 0 484057861 144457728 34225 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35268 34225 603 41 0 35227 0
vsize: 141072
[startup+920.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 35000 0 0 0 91907 108 0 0 25 0 1 0 484057861 145125376 34400 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35431 34400 603 41 0 35390 0
vsize: 141724
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 35202 0 0 0 92906 109 0 0 25 0 1 0 484057861 146046976 34602 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35656 34602 603 41 0 35615 0
vsize: 142624
[startup+940.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 35418 0 0 0 93906 110 0 0 25 0 1 0 484057861 146833408 34818 4294967295 134512640 134672761 3221224544 3221223688 134616275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35848 34818 603 41 0 35807 0
vsize: 143392
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 35617 0 0 0 94906 110 0 0 25 0 1 0 484057861 147636224 35017 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36044 35017 603 41 0 36003 0
vsize: 144176
[startup+960.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 35927 0 0 0 95905 111 0 0 25 0 1 0 484057861 148951040 35327 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36365 35327 603 41 0 36324 0
vsize: 145460
[startup+970.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 36243 0 0 0 96904 112 0 0 25 0 1 0 484057861 150265856 35643 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36686 35643 603 41 0 36645 0
vsize: 146744
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 36566 0 0 0 97904 112 0 0 25 0 1 0 484057861 151584768 35966 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37008 35966 603 41 0 36967 0
vsize: 148032
[startup+990.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 36909 0 0 0 98903 113 0 0 25 0 1 0 484057861 153026560 36309 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37360 36309 603 41 0 37319 0
vsize: 149440
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 37314 0 0 0 99903 114 0 0 25 0 1 0 484057861 154607616 36714 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37746 36714 603 41 0 37705 0
vsize: 150984
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 37689 0 0 0 100902 115 0 0 25 0 1 0 484057861 156213248 37089 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38138 37090 603 41 0 38097 0
vsize: 152552
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 38054 0 0 0 101900 117 0 0 25 0 1 0 484057861 157663232 37454 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38492 37454 603 41 0 38451 0
vsize: 153968
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 38365 0 0 0 102899 118 0 0 25 0 1 0 484057861 158973952 37765 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38812 37765 603 41 0 38771 0
vsize: 155248
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 38690 0 0 0 103899 119 0 0 25 0 1 0 484057861 160305152 38090 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39137 38090 603 41 0 39096 0
vsize: 156548
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 38993 0 0 0 104899 119 0 0 25 0 1 0 484057861 161492992 38393 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39427 38393 603 41 0 39386 0
vsize: 157708
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 39315 0 0 0 105897 121 0 0 25 0 1 0 484057861 162807808 38715 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39748 38715 603 41 0 39707 0
vsize: 158992
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 39660 0 0 0 106897 122 0 0 25 0 1 0 484057861 164253696 39060 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40101 39060 603 41 0 40060 0
vsize: 160404
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 40002 0 0 0 107896 123 0 0 25 0 1 0 484057861 165564416 39402 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40421 39402 603 41 0 40380 0
vsize: 161684
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 40374 0 0 0 108895 123 0 0 25 0 1 0 484057861 167157760 39774 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40810 39774 603 41 0 40769 0
vsize: 163240
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 40705 0 0 0 109895 124 0 0 25 0 1 0 484057861 168476672 40105 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41132 40105 603 41 0 41091 0
vsize: 164528
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 41063 0 0 0 110894 124 0 0 25 0 1 0 484057861 169926656 40463 4294967295 134512640 134672761 3221224544 3221223696 134614555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41486 40463 603 41 0 41445 0
vsize: 165944
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 41500 0 0 0 111893 126 0 0 25 0 1 0 484057861 171765760 40900 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41935 40900 603 41 0 41894 0
vsize: 167740
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19596
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 41685 0 0 0 112893 126 0 0 25 0 1 0 484057861 172560384 41085 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42129 41085 603 41 0 42088 0
vsize: 168516
[startup+1140.01 s]
Raw data (loadavg): 1.23 1.02 0.94 2/58 19639
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 41830 0 0 0 113892 127 0 0 25 0 1 0 484057861 173101056 41230 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42261 41230 603 41 0 42220 0
vsize: 169044
[startup+1150.02 s]
Raw data (loadavg): 1.20 1.02 0.94 2/54 19649
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 42036 0 0 0 114892 127 0 0 25 0 1 0 484057861 173912064 41436 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42459 41436 603 41 0 42418 0
vsize: 169836
[startup+1160.02 s]
Raw data (loadavg): 1.17 1.02 0.94 2/54 19649
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 42229 0 0 0 115891 129 0 0 25 0 1 0 484057861 174698496 41629 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42651 41629 603 41 0 42610 0
vsize: 170604
[startup+1170.02 s]
Raw data (loadavg): 1.14 1.02 0.94 2/54 19649
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 42518 0 0 0 116890 130 0 0 25 0 1 0 484057861 175878144 41918 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42939 41918 603 41 0 42898 0
vsize: 171756
[startup+1180.02 s]
Raw data (loadavg): 1.12 1.02 0.94 2/54 19649
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 42822 0 0 0 117889 131 0 0 25 0 1 0 484057861 177201152 42222 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43262 42222 603 41 0 43221 0
vsize: 173048
[startup+1190.02 s]
Raw data (loadavg): 1.10 1.02 0.94 2/54 19649
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 43092 0 0 0 118889 132 0 0 25 0 1 0 484057861 178257920 42492 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43520 42492 603 41 0 43479 0
vsize: 174080
[startup+1200.02 s]
Raw data (loadavg): 1.08 1.01 0.94 2/54 19649
Raw data (stat): 19596 (minisat+) R 19595 20937 20936 0 -1 0 43358 0 0 0 119888 133 0 0 25 0 1 0 484057861 179310592 42758 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43777 42758 603 41 0 43736 0
vsize: 175108
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.08 1.01 0.94 1/54 19649
Raw data (stat): 19596 (minisat+) Z 19595 20937 20936 0 -1 12 43358 0 0 0 119888 141 0 0 25 0 1 0 484057861 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.1
CPU time (s): 1200.3
CPU user time (s): 1198.88
CPU system time (s): 1.41179
CPU usage (%): 100.016
Max. virtual memory (Kb): 175108
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####