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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-fit1d.opb
MD5SUM	6bb160e5eb0ef9c02ca7232f62836f2b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	8436
Biggest coefficient in the objective function	368640
Number of bits for the biggest coefficient in the objective function	19
Sum of the numbers in the objective function	57614442
Number of bits of the sum of numbers in the objective function	26
Biggest number in a constraint	483840
Number of bits of the biggest number in a constraint	19
Biggest sum of numbers in a constraint	72412534
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1195.48
Number of variables	8436
Total number of constraints	1050
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1050
Minimum length of a constraint	8
Maximum length of a constraint	8436
Trace number 19923

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        674640 kB
Buffers:         30072 kB
Cached:         308136 kB
SwapCached:        364 kB
Active:          53428 kB
Inactive:       287304 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        674388 kB
SwapTotal:     2097136 kB
SwapFree:      2096356 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6404 kB
Slab:            13616 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 20:14:49 (client local time) WITH STATUS 0 IN 1200.38 SECONDS
stats: 15782 7 1200.38 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1051 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): (none)
c ---[1050]---> BDD-cost:    7
c ---[1049]---> BDD-cost:    7
c ---[1048]---> BDD-cost:    7
c ---[1047]---> BDD-cost:    7
c ---[1046]---> BDD-cost:    7
c ---[1045]---> BDD-cost:    7
c ---[1044]---> BDD-cost:    7
c ---[1043]---> BDD-cost:    7
c ---[1042]---> BDD-cost:    7
c ---[1041]---> BDD-cost:    7
c ---[1040]---> BDD-cost:    7
c ---[1039]---> BDD-cost:    7
c ---[1038]---> BDD-cost:    7
c ---[1037]---> BDD-cost:    7
c ---[1036]---> BDD-cost:    7
c ---[1035]---> BDD-cost:    7
c ---[1034]---> BDD-cost:    7
c ---[1033]---> BDD-cost:    7
c ---[1032]---> BDD-cost:    7
c ---[1031]---> BDD-cost:    7
c ---[1030]---> BDD-cost:    7
c ---[1029]---> BDD-cost:    7
c ---[1028]---> BDD-cost:    7
c ---[1027]---> BDD-cost:    7
c ---[1026]---> BDD-cost:    7
c ---[1025]---> BDD-cost:    7
c ---[1024]---> BDD-cost:    7
c ---[1023]---> BDD-cost:    7
c ---[1022]---> BDD-cost:    7
c ---[1021]---> BDD-cost:    7
c ---[1020]---> BDD-cost:    7
c ---[1019]---> BDD-cost:    7
c ---[1018]---> BDD-cost:    7
c ---[1017]---> BDD-cost:    7
c ---[1016]---> BDD-cost:    7
c ---[1015]---> BDD-cost:    7
c ---[1014]---> BDD-cost:    7
c ---[1013]---> BDD-cost:    7
c ---[1012]---> BDD-cost:    7
c ---[1011]---> BDD-cost:    7
c ---[1010]---> BDD-cost:    7
c ---[1009]---> BDD-cost:    7
c ---[1008]---> BDD-cost:    7
c ---[1007]---> BDD-cost:    7
c ---[1006]---> BDD-cost:    7
c ---[1005]---> BDD-cost:    7
c ---[1004]---> BDD-cost:    7
c ---[1003]---> BDD-cost:    7
c ---[1002]---> BDD-cost:    7
c ---[1001]---> BDD-cost:    7
c ---[1000]---> BDD-cost:    7
c ---[ 999]---> BDD-cost:    7
c ---[ 998]---> BDD-cost:    7
c ---[ 997]---> BDD-cost:    7
c ---[ 996]---> BDD-cost:    7
c ---[ 995]---> BDD-cost:    7
c ---[ 994]---> BDD-cost:    7
c ---[ 993]---> BDD-cost:    7
c ---[ 992]---> BDD-cost:    7
c ---[ 991]---> BDD-cost:    7
c ---[ 990]---> BDD-cost:    7
c ---[ 989]---> BDD-cost:    7
c ---[ 988]---> BDD-cost:    7
c ---[ 987]---> BDD-cost:    7
c ---[ 986]---> BDD-cost:    7
c ---[ 985]---> BDD-cost:    7
c ---[ 984]---> BDD-cost:    7
c ---[ 983]---> BDD-cost:    7
c ---[ 982]---> BDD-cost:    7
c ---[ 981]---> BDD-cost:    7
c ---[ 980]---> BDD-cost:    7
c ---[ 979]---> BDD-cost:    7
c ---[ 978]---> BDD-cost:    7
c ---[ 977]---> BDD-cost:    7
c ---[ 976]---> BDD-cost:    7
c ---[ 975]---> BDD-cost:    7
c ---[ 974]---> BDD-cost:    7
c ---[ 973]---> BDD-cost:    7
c ---[ 972]---> BDD-cost:    7
c ---[ 971]---> BDD-cost:    7
c ---[ 970]---> BDD-cost:    7
c ---[ 969]---> BDD-cost:    7
c ---[ 968]---> BDD-cost:    7
c ---[ 967]---> BDD-cost:    7
c ---[ 966]---> BDD-cost:    7
c ---[ 965]---> BDD-cost:    7
c ---[ 964]---> BDD-cost:    7
c ---[ 963]---> BDD-cost:    7
c ---[ 962]---> BDD-cost:    7
c ---[ 961]---> BDD-cost:    7
c ---[ 960]---> BDD-cost:    7
c ---[ 959]---> BDD-cost:    7
c ---[ 958]---> BDD-cost:    7
c ---[ 957]---> BDD-cost:    7
c ---[ 956]---> BDD-cost:    7
c ---[ 955]---> BDD-cost:    7
c ---[ 954]---> BDD-cost:    7
c ---[ 953]---> BDD-cost:    7
c ---[ 952]---> BDD-cost:    7
c ---[ 951]---> BDD-cost:    7
c ---[ 950]---> BDD-cost:    7
c ---[ 949]---> BDD-cost:    7
c ---[ 948]---> BDD-cost:    7
c ---[ 947]---> BDD-cost:    7
c ---[ 946]---> BDD-cost:    7
c ---[ 945]---> BDD-cost:    7
c ---[ 944]---> BDD-cost:    7
c ---[ 943]---> BDD-cost:    7
c ---[ 942]---> BDD-cost:    7
c ---[ 941]---> BDD-cost:    7
c ---[ 940]---> BDD-cost:    7
c ---[ 939]---> BDD-cost:    7
c ---[ 938]---> BDD-cost:    7
c ---[ 937]---> BDD-cost:    7
c ---[ 936]---> BDD-cost:    7
c ---[ 935]---> BDD-cost:    7
c ---[ 934]---> BDD-cost:    7
c ---[ 933]---> BDD-cost:    7
c ---[ 932]---> BDD-cost:    7
c ---[ 931]---> BDD-cost:    7
c ---[ 930]---> BDD-cost:    7
c ---[ 929]---> BDD-cost:    7
c ---[ 928]---> BDD-cost:    7
c ---[ 927]---> BDD-cost:    7
c ---[ 926]---> BDD-cost:    7
c ---[ 925]---> BDD-cost:    7
c ---[ 924]---> BDD-cost:    7
c ---[ 923]---> BDD-cost:    7
c ---[ 922]---> BDD-cost:    7
c ---[ 921]---> BDD-cost:    7
c ---[ 920]---> BDD-cost:    7
c ---[ 919]---> BDD-cost:    7
c ---[ 918]---> BDD-cost:    7
c ---[ 917]---> BDD-cost:    7
c ---[ 916]---> BDD-cost:    7
c ---[ 915]---> BDD-cost:    7
c ---[ 914]---> BDD-cost:    7
c ---[ 913]---> BDD-cost:    7
c ---[ 912]---> BDD-cost:    7
c ---[ 911]---> BDD-cost:    7
c ---[ 910]---> BDD-cost:    7
c ---[ 909]---> BDD-cost:    7
c ---[ 908]---> BDD-cost:    7
c ---[ 907]---> BDD-cost:    7
c ---[ 906]---> BDD-cost:    7
c ---[ 905]---> BDD-cost:    7
c ---[ 904]---> BDD-cost:    7
c ---[ 903]---> BDD-cost:    7
c ---[ 902]---> BDD-cost:    7
c ---[ 901]---> BDD-cost:    7
c ---[ 900]---> BDD-cost:    7
c ---[ 899]---> BDD-cost:    7
c ---[ 898]---> BDD-cost:    7
c ---[ 897]---> BDD-cost:    7
c ---[ 896]---> BDD-cost:    7
c ---[ 895]---> BDD-cost:    7
c ---[ 894]---> BDD-cost:    7
c ---[ 893]---> BDD-cost:    7
c ---[ 892]---> BDD-cost:    7
c ---[ 891]---> BDD-cost:    7
c ---[ 890]---> BDD-cost:    7
c ---[ 889]---> BDD-cost:    7
c ---[ 888]---> BDD-cost:    7
c ---[ 887]---> BDD-cost:    7
c ---[ 886]---> BDD-cost:    7
c ---[ 885]---> BDD-cost:    7
c ---[ 884]---> BDD-cost:    7
c ---[ 883]---> BDD-cost:    7
c ---[ 882]---> BDD-cost:    7
c ---[ 881]---> BDD-cost:    7
c ---[ 880]---> BDD-cost:    7
c ---[ 879]---> BDD-cost:    7
c ---[ 878]---> BDD-cost:    7
c ---[ 877]---> BDD-cost:    7
c ---[ 876]---> BDD-cost:    7
c ---[ 875]---> BDD-cost:    7
c ---[ 874]---> BDD-cost:    7
c ---[ 873]---> BDD-cost:    7
c ---[ 872]---> BDD-cost:    7
c ---[ 871]---> BDD-cost:    7
c ---[ 870]---> BDD-cost:    7
c ---[ 869]---> BDD-cost:    7
c ---[ 868]---> BDD-cost:    7
c ---[ 867]---> BDD-cost:    7
c ---[ 866]---> BDD-cost:    7
c ---[ 865]---> BDD-cost:    7
c ---[ 864]---> BDD-cost:    7
c ---[ 863]---> BDD-cost:    7
c ---[ 862]---> BDD-cost:    7
c ---[ 861]---> BDD-cost:    7
c ---[ 860]---> BDD-cost:    7
c ---[ 859]---> BDD-cost:    7
c ---[ 858]---> BDD-cost:    7
c ---[ 857]---> BDD-cost:    7
c ---[ 856]---> BDD-cost:    7
c ---[ 855]---> BDD-cost:    7
c ---[ 854]---> BDD-cost:    7
c ---[ 853]---> BDD-cost:    7
c ---[ 852]---> BDD-cost:    7
c ---[ 851]---> BDD-cost:    7
c ---[ 850]---> BDD-cost:    7
c ---[ 849]---> BDD-cost:    7
c ---[ 848]---> BDD-cost:    7
c ---[ 847]---> BDD-cost:    7
c ---[ 846]---> BDD-cost:    7
c ---[ 845]---> BDD-cost:    7
c ---[ 844]---> BDD-cost:    7
c ---[ 843]---> BDD-cost:    7
c ---[ 842]---> BDD-cost:    7
c ---[ 841]---> BDD-cost:    7
c ---[ 840]---> BDD-cost:    7
c ---[ 839]---> BDD-cost:    7
c ---[ 838]---> BDD-cost:    7
c ---[ 837]---> BDD-cost:    7
c ---[ 836]---> BDD-cost:    7
c ---[ 835]---> BDD-cost:    7
c ---[ 834]---> BDD-cost:    7
c ---[ 833]---> BDD-cost:    7
c ---[ 832]---> BDD-cost:    7
c ---[ 831]---> BDD-cost:    7
c ---[ 830]---> BDD-cost:    7
c ---[ 829]---> BDD-cost:    7
c ---[ 828]---> BDD-cost:    7
c ---[ 827]---> BDD-cost:    7
c ---[ 826]---> BDD-cost:    7
c ---[ 825]---> BDD-cost:    7
c ---[ 824]---> BDD-cost:    7
c ---[ 823]---> BDD-cost:    7
c ---[ 822]---> BDD-cost:    7
c ---[ 821]---> BDD-cost:    7
c ---[ 820]---> BDD-cost:    7
c ---[ 819]---> BDD-cost:    7
c ---[ 818]---> BDD-cost:    7
c ---[ 817]---> BDD-cost:    7
c ---[ 816]---> BDD-cost:    7
c ---[ 815]---> BDD-cost:    7
c ---[ 814]---> BDD-cost:    7
c ---[ 813]---> BDD-cost:    7
c ---[ 812]---> BDD-cost:    7
c ---[ 811]---> BDD-cost:    7
c ---[ 810]---> BDD-cost:    7
c ---[ 809]---> BDD-cost:    7
c ---[ 808]---> BDD-cost:    7
c ---[ 807]---> BDD-cost:    7
c ---[ 806]---> BDD-cost:    7
c ---[ 805]---> BDD-cost:    7
c ---[ 804]---> BDD-cost:    7
c ---[ 803]---> BDD-cost:    7
c ---[ 802]---> BDD-cost:    7
c ---[ 801]---> BDD-cost:    7
c ---[ 800]---> BDD-cost:    7
c ---[ 799]---> BDD-cost:    7
c ---[ 798]---> BDD-cost:    7
c ---[ 797]---> BDD-cost:    7
c ---[ 796]---> BDD-cost:    7
c ---[ 795]---> BDD-cost:    7
c ---[ 794]---> BDD-cost:    7
c ---[ 793]---> BDD-cost:    7
c ---[ 792]---> BDD-cost:    7
c ---[ 791]---> BDD-cost:    7
c ---[ 790]---> BDD-cost:    7
c ---[ 789]---> BDD-cost:    7
c ---[ 788]---> BDD-cost:    7
c ---[ 787]---> BDD-cost:    7
c ---[ 786]---> BDD-cost:    7
c ---[ 785]---> BDD-cost:    7
c ---[ 784]---> BDD-cost:    7
c ---[ 783]---> BDD-cost:    7
c ---[ 782]---> BDD-cost:    7
c ---[ 781]---> BDD-cost:    7
c ---[ 780]---> BDD-cost:    7
c ---[ 779]---> BDD-cost:    7
c ---[ 778]---> BDD-cost:    7
c ---[ 777]---> BDD-cost:    7
c ---[ 776]---> BDD-cost:    7
c ---[ 775]---> BDD-cost:    7
c ---[ 774]---> BDD-cost:    7
c ---[ 773]---> BDD-cost:    7
c ---[ 772]---> BDD-cost:    7
c ---[ 771]---> BDD-cost:    7
c ---[ 770]---> BDD-cost:    7
c ---[ 769]---> BDD-cost:    7
c ---[ 768]---> BDD-cost:    7
c ---[ 767]---> BDD-cost:    7
c ---[ 766]---> BDD-cost:    7
c ---[ 765]---> BDD-cost:    7
c ---[ 764]---> BDD-cost:    7
c ---[ 763]---> BDD-cost:    7
c ---[ 762]---> BDD-cost:    7
c ---[ 761]---> BDD-cost:    7
c ---[ 760]---> BDD-cost:    7
c ---[ 759]---> BDD-cost:    7
c ---[ 758]---> BDD-cost:    7
c ---[ 757]---> BDD-cost:    7
c ---[ 756]---> BDD-cost:    7
c ---[ 755]---> BDD-cost:    7
c ---[ 754]---> BDD-cost:    7
c ---[ 753]---> BDD-cost:    7
c ---[ 752]---> BDD-cost:    7
c ---[ 751]---> BDD-cost:    7
c ---[ 750]---> BDD-cost:    7
c ---[ 749]---> BDD-cost:    7
c ---[ 748]---> BDD-cost:    7
c ---[ 747]---> BDD-cost:    7
c ---[ 746]---> BDD-cost:    7
c ---[ 745]---> BDD-cost:    7
c ---[ 744]---> BDD-cost:    7
c ---[ 743]---> BDD-cost:    7
c ---[ 742]---> BDD-cost:    7
c ---[ 741]---> BDD-cost:    7
c ---[ 740]---> BDD-cost:    7
c ---[ 739]---> BDD-cost:    7
c ---[ 738]---> BDD-cost:    7
c ---[ 737]---> BDD-cost:    7
c ---[ 736]---> BDD-cost:    7
c ---[ 735]---> BDD-cost:    7
c ---[ 734]---> BDD-cost:    7
c ---[ 733]---> BDD-cost:    7
c ---[ 732]---> BDD-cost:    7
c ---[ 731]---> BDD-cost:    7
c ---[ 730]---> BDD-cost:    7
c ---[ 729]---> BDD-cost:    7
c ---[ 728]---> BDD-cost:    7
c ---[ 727]---> BDD-cost:    7
c ---[ 726]---> BDD-cost:    7
c ---[ 725]---> BDD-cost:    7
c ---[ 724]---> BDD-cost:    7
c ---[ 723]---> BDD-cost:    7
c ---[ 722]---> BDD-cost:    7
c ---[ 721]---> BDD-cost:    7
c ---[ 720]---> BDD-cost:    7
c ---[ 719]---> BDD-cost:    7
c ---[ 718]---> BDD-cost:    7
c ---[ 717]---> BDD-cost:    7
c ---[ 716]---> BDD-cost:    7
c ---[ 715]---> BDD-cost:    7
c ---[ 714]---> BDD-cost:    7
c ---[ 713]---> BDD-cost:    7
c ---[ 712]---> BDD-cost:    7
c ---[ 711]---> BDD-cost:    7
c ---[ 710]---> BDD-cost:    7
c ---[ 709]---> BDD-cost:    7
c ---[ 708]---> BDD-cost:    7
c ---[ 707]---> BDD-cost:    7
c ---[ 706]---> BDD-cost:    7
c ---[ 705]---> BDD-cost:    7
c ---[ 704]---> BDD-cost:    7
c ---[ 703]---> BDD-cost:    7
c ---[ 702]---> BDD-cost:    7
c ---[ 701]---> BDD-cost:    7
c ---[ 700]---> BDD-cost:    7
c ---[ 699]---> BDD-cost:    7
c ---[ 698]---> BDD-cost:    7
c ---[ 697]---> BDD-cost:    7
c ---[ 696]---> BDD-cost:    7
c ---[ 695]---> BDD-cost:    7
c ---[ 694]---> BDD-cost:    7
c ---[ 693]---> BDD-cost:    7
c ---[ 692]---> BDD-cost:    7
c ---[ 691]---> BDD-cost:    7
c ---[ 690]---> BDD-cost:    7
c ---[ 689]---> BDD-cost:    7
c ---[ 688]---> BDD-cost:    7
c ---[ 687]---> BDD-cost:    7
c ---[ 686]---> BDD-cost:    7
c ---[ 685]---> BDD-cost:    7
c ---[ 684]---> BDD-cost:    7
c ---[ 683]---> BDD-cost:    7
c ---[ 682]---> BDD-cost:    7
c ---[ 681]---> BDD-cost:    7
c ---[ 680]---> BDD-cost:    7
c ---[ 679]---> BDD-cost:    7
c ---[ 678]---> BDD-cost:    7
c ---[ 677]---> BDD-cost:    7
c ---[ 676]---> BDD-cost:    7
c ---[ 675]---> BDD-cost:    7
c ---[ 674]---> BDD-cost:    7
c ---[ 673]---> BDD-cost:    7
c ---[ 672]---> BDD-cost:    7
c ---[ 671]---> BDD-cost:    7
c ---[ 670]---> BDD-cost:    7
c ---[ 669]---> BDD-cost:    7
c ---[ 668]---> BDD-cost:    7
c ---[ 667]---> BDD-cost:    7
c ---[ 666]---> BDD-cost:    7
c ---[ 665]---> BDD-cost:    7
c ---[ 664]---> BDD-cost:    7
c ---[ 663]---> BDD-cost:    7
c ---[ 662]---> BDD-cost:    7
c ---[ 661]---> BDD-cost:    7
c ---[ 660]---> BDD-cost:    7
c ---[ 659]---> BDD-cost:    7
c ---[ 658]---> BDD-cost:    7
c ---[ 657]---> BDD-cost:    7
c ---[ 656]---> BDD-cost:    7
c ---[ 655]---> BDD-cost:    7
c ---[ 654]---> BDD-cost:    7
c ---[ 653]---> BDD-cost:    7
c ---[ 652]---> BDD-cost:    7
c ---[ 651]---> BDD-cost:    7
c ---[ 650]---> BDD-cost:    7
c ---[ 649]---> BDD-cost:    7
c ---[ 648]---> BDD-cost:    7
c ---[ 647]---> BDD-cost:    7
c ---[ 646]---> BDD-cost:    7
c ---[ 645]---> BDD-cost:    7
c ---[ 644]---> BDD-cost:    7
c ---[ 643]---> BDD-cost:    7
c ---[ 642]---> BDD-cost:    7
c ---[ 641]---> BDD-cost:    7
c ---[ 640]---> BDD-cost:    7
c ---[ 639]---> BDD-cost:    7
c ---[ 638]---> BDD-cost:    7
c ---[ 637]---> BDD-cost:    7
c ---[ 636]---> BDD-cost:    7
c ---[ 635]---> BDD-cost:    7
c ---[ 634]---> BDD-cost:    7
c ---[ 633]---> BDD-cost:    7
c ---[ 632]---> BDD-cost:    7
c ---[ 631]---> BDD-cost:    7
c ---[ 630]---> BDD-cost:    7
c ---[ 629]---> BDD-cost:    7
c ---[ 628]---> BDD-cost:    7
c ---[ 627]---> BDD-cost:    7
c ---[ 626]---> BDD-cost:    7
c ---[ 625]---> BDD-cost:    7
c ---[ 624]---> BDD-cost:    7
c ---[ 623]---> BDD-cost:    7
c ---[ 622]---> BDD-cost:    7
c ---[ 621]---> BDD-cost:    7
c ---[ 620]---> BDD-cost:    7
c ---[ 619]---> BDD-cost:    7
c ---[ 618]---> BDD-cost:    7
c ---[ 617]---> BDD-cost:    7
c ---[ 616]---> BDD-cost:    7
c ---[ 615]---> BDD-cost:    7
c ---[ 614]---> BDD-cost:    7
c ---[ 613]---> BDD-cost:    7
c ---[ 612]---> BDD-cost:    7
c ---[ 611]---> BDD-cost:    7
c ---[ 610]---> BDD-cost:    7
c ---[ 609]---> BDD-cost:    7
c ---[ 608]---> BDD-cost:    7
c ---[ 607]---> BDD-cost:    7
c ---[ 606]---> BDD-cost:    7
c ---[ 605]---> BDD-cost:    7
c ---[ 604]---> BDD-cost:    7
c ---[ 603]---> BDD-cost:    7
c ---[ 602]---> BDD-cost:    7
c ---[ 601]---> BDD-cost:    7
c ---[ 600]---> BDD-cost:    7
c ---[ 599]---> BDD-cost:    7
c ---[ 598]---> BDD-cost:    7
c ---[ 597]---> BDD-cost:    7
c ---[ 596]---> BDD-cost:    7
c ---[ 595]---> BDD-cost:    7
c ---[ 594]---> BDD-cost:    7
c ---[ 593]---> BDD-cost:    7
c ---[ 592]---> BDD-cost:    7
c ---[ 591]---> BDD-cost:    7
c ---[ 590]---> BDD-cost:    7
c ---[ 589]---> BDD-cost:    7
c ---[ 588]---> BDD-cost:    7
c ---[ 587]---> BDD-cost:    7
c ---[ 586]---> BDD-cost:    7
c ---[ 585]---> BDD-cost:    7
c ---[ 584]---> BDD-cost:    7
c ---[ 583]---> BDD-cost:    7
c ---[ 582]---> BDD-cost:    7
c ---[ 581]---> BDD-cost:    7
c ---[ 580]---> BDD-cost:    7
c ---[ 579]---> BDD-cost:    7
c ---[ 578]---> BDD-cost:    7
c ---[ 577]---> BDD-cost:    7
c ---[ 576]---> BDD-cost:    7
c ---[ 575]---> BDD-cost:    7
c ---[ 574]---> BDD-cost:    7
c ---[ 573]---> BDD-cost:    7
c ---[ 572]---> BDD-cost:    7
c ---[ 571]---> BDD-cost:    7
c ---[ 570]---> BDD-cost:    7
c ---[ 569]---> BDD-cost:    7
c ---[ 568]---> BDD-cost:    7
c ---[ 567]---> BDD-cost:    7
c ---[ 566]---> BDD-cost:    7
c ---[ 565]---> BDD-cost:    7
c ---[ 564]---> BDD-cost:    7
c ---[ 563]---> BDD-cost:    7
c ---[ 562]---> BDD-cost:    7
c ---[ 561]---> BDD-cost:    7
c ---[ 560]---> BDD-cost:    7
c ---[ 559]---> BDD-cost:    7
c ---[ 558]---> BDD-cost:    7
c ---[ 557]---> BDD-cost:    7
c ---[ 556]---> BDD-cost:    7
c ---[ 555]---> BDD-cost:    7
c ---[ 554]---> BDD-cost:    7
c ---[ 553]---> BDD-cost:    7
c ---[ 552]---> BDD-cost:    7
c ---[ 551]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    7
c ---[ 549]---> BDD-cost:    7
c ---[ 548]---> BDD-cost:    7
c ---[ 547]---> BDD-cost:    7
c ---[ 546]---> BDD-cost:    7
c ---[ 545]---> BDD-cost:    7
c ---[ 544]---> BDD-cost:    7
c ---[ 543]---> BDD-cost:    7
c ---[ 542]---> BDD-cost:    7
c ---[ 541]---> BDD-cost:    7
c ---[ 540]---> BDD-cost:    7
c ---[ 539]---> BDD-cost:    7
c ---[ 538]---> BDD-cost:    7
c ---[ 537]---> BDD-cost:    7
c ---[ 536]---> BDD-cost:    7
c ---[ 535]---> BDD-cost:    7
c ---[ 534]---> BDD-cost:    7
c ---[ 533]---> BDD-cost:    7
c ---[ 532]---> BDD-cost:    7
c ---[ 531]---> BDD-cost:    7
c ---[ 530]---> BDD-cost:    7
c ---[ 529]---> BDD-cost:    7
c ---[ 528]---> BDD-cost:    7
c ---[ 527]---> BDD-cost:    7
c ---[ 526]---> BDD-cost:    7
c ---[ 525]---> BDD-cost:    7
c ---[ 524]---> BDD-cost:    7
c ---[ 523]---> BDD-cost:    7
c ---[ 522]---> BDD-cost:    7
c ---[ 521]---> BDD-cost:    7
c ---[ 520]---> BDD-cost:    7
c ---[ 519]---> BDD-cost:    7
c ---[ 518]---> BDD-cost:    7
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    7
c ---[ 515]---> BDD-cost:    7
c ---[ 514]---> BDD-cost:    7
c ---[ 513]---> BDD-cost:    7
c ---[ 512]---> BDD-cost:    7
c ---[ 511]---> BDD-cost:    7
c ---[ 510]---> BDD-cost:    7
c ---[ 509]---> BDD-cost:    7
c ---[ 508]---> BDD-cost:    7
c ---[ 507]---> BDD-cost:    7
c ---[ 506]---> BDD-cost:    7
c ---[ 505]---> BDD-cost:    7
c ---[ 504]---> BDD-cost:    7
c ---[ 503]---> BDD-cost:    7
c ---[ 502]---> BDD-cost:    7
c ---[ 501]---> BDD-cost:    7
c ---[ 500]---> BDD-cost:    7
c ---[ 499]---> BDD-cost:    7
c ---[ 498]---> BDD-cost:    7
c ---[ 497]---> BDD-cost:    7
c ---[ 496]---> BDD-cost:    7
c ---[ 495]---> BDD-cost:    7
c ---[ 494]---> BDD-cost:    7
c ---[ 493]---> BDD-cost:    7
c ---[ 492]---> BDD-cost:    7
c ---[ 491]---> BDD-cost:    7
c ---[ 490]---> BDD-cost:    7
c ---[ 489]---> BDD-cost:    7
c ---[ 488]---> BDD-cost:    7
c ---[ 487]---> BDD-cost:    7
c ---[ 486]---> BDD-cost:    7
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 476]---> BDD-cost:    7
c ---[ 475]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 470]---> BDD-cost:    7
c ---[ 469]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 464]---> BDD-cost:    7
c ---[ 463]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 461]---> BDD-cost:    7
c ---[ 460]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 456]---> BDD-cost:    7
c ---[ 455]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 449]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 443]---> BDD-cost:    7
c ---[ 442]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 438]---> BDD-cost:    7
c ---[ 437]---> BDD-cost:    7
c ---[ 436]---> BDD-cost:    7
c ---[ 435]---> BDD-cost:    7
c ---[ 434]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 432]---> BDD-cost:    7
c ---[ 431]---> BDD-cost:    7
c ---[ 430]---> BDD-cost:    7
c ---[ 429]---> BDD-cost:    7
c ---[ 428]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 426]---> BDD-cost:    7
c ---[ 425]---> BDD-cost:    7
c ---[ 424]---> BDD-cost:    7
c ---[ 423]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 420]---> BDD-cost:    7
c ---[ 419]---> BDD-cost:    7
c ---[ 418]---> BDD-cost:    7
c ---[ 417]---> BDD-cost:    7
c ---[ 416]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 414]---> BDD-cost:    7
c ---[ 413]---> BDD-cost:    7
c ---[ 412]---> BDD-cost:    7
c ---[ 411]---> BDD-cost:    7
c ---[ 410]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 407]---> BDD-cost:    7
c ---[ 406]---> BDD-cost:    7
c ---[ 405]---> BDD-cost:    7
c ---[ 404]---> BDD-cost:    7
c ---[ 403]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 401]---> BDD-cost:    7
c ---[ 400]---> BDD-cost:    7
c ---[ 399]---> BDD-cost:    7
c ---[ 398]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 395]---> BDD-cost:    7
c ---[ 394]---> BDD-cost:    7
c ---[ 393]---> BDD-cost:    7
c ---[ 392]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 389]---> BDD-cost:    7
c ---[ 388]---> BDD-cost:    7
c ---[ 387]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 383]---> BDD-cost:    7
c ---[ 382]---> BDD-cost:    7
c ---[ 381]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 377]---> BDD-cost:    7
c ---[ 376]---> BDD-cost:    7
c ---[ 375]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 371]---> BDD-cost:    7
c ---[ 370]---> BDD-cost:    7
c ---[ 369]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 363]---> BDD-cost:    7
c ---[ 362]---> BDD-cost:    7
c ---[ 361]---> BDD-cost:    7
c ---[ 360]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 358]---> BDD-cost:    7
c ---[ 357]---> BDD-cost:    7
c ---[ 356]---> BDD-cost:    7
c ---[ 355]---> BDD-cost:    7
c ---[ 354]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 352]---> BDD-cost:    7
c ---[ 351]---> BDD-cost:    7
c ---[ 350]---> BDD-cost:    7
c ---[ 349]---> BDD-cost:    7
c ---[ 348]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 346]---> BDD-cost:    7
c ---[ 345]---> BDD-cost:    7
c ---[ 344]---> BDD-cost:    7
c ---[ 343]---> BDD-cost:    7
c ---[ 342]---> BDD-cost:    7
c ---[ 341]---> BDD-cost:    7
c ---[ 340]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 338]---> BDD-cost:    7
c ---[ 337]---> BDD-cost:    7
c ---[ 336]---> BDD-cost:    7
c ---[ 335]---> BDD-cost:    7
c ---[ 334]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 332]---> BDD-cost:    7
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:    7
c ---[ 329]---> BDD-cost:    7
c ---[ 328]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 326]---> BDD-cost:    7
c ---[ 325]---> BDD-cost:    7
c ---[ 324]---> BDD-cost:    7
c ---[ 323]---> BDD-cost:    7
c ---[ 322]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 320]---> BDD-cost:    7
c ---[ 319]---> BDD-cost:    7
c ---[ 318]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:    7
c ---[ 316]---> BDD-cost:    7
c ---[ 315]---> BDD-cost:    7
c ---[ 314]---> BDD-cost:    7
c ---[ 313]---> BDD-cost:    7
c ---[ 312]---> BDD-cost:    7
c ---[ 311]---> BDD-cost:    7
c ---[ 310]---> BDD-cost:    7
c ---[ 309]---> BDD-cost:    7
c ---[ 308]---> BDD-cost:    7
c ---[ 307]---> BDD-cost:    7
c ---[ 306]---> BDD-cost:    7
c ---[ 305]---> BDD-cost:    7
c ---[ 304]---> BDD-cost:    7
c ---[ 303]---> BDD-cost:    7
c ---[ 302]---> BDD-cost:    7
c ---[ 301]---> BDD-cost:    7
c ---[ 300]---> BDD-cost:    7
c ---[ 299]---> BDD-cost:    7
c ---[ 298]---> BDD-cost:    7
c ---[ 297]---> BDD-cost:    7
c ---[ 296]---> BDD-cost:    7
c ---[ 295]---> BDD-cost:    7
c ---[ 294]---> BDD-cost:    7
c ---[ 293]---> BDD-cost:    7
c ---[ 292]---> BDD-cost:    7
c ---[ 291]---> BDD-cost:    7
c ---[ 290]---> BDD-cost:    7
c ---[ 289]---> BDD-cost:    7
c ---[ 288]---> BDD-cost:    7
c ---[ 287]---> BDD-cost:    7
c ---[ 286]---> BDD-cost:    7
c ---[ 285]---> BDD-cost:    7
c ---[ 284]---> BDD-cost:    7
c ---[ 283]---> BDD-cost:    7
c ---[ 282]---> BDD-cost:    7
c ---[ 281]---> BDD-cost:    7
c ---[ 280]---> BDD-cost:    7
c ---[ 279]---> BDD-cost:    7
c ---[ 278]---> BDD-cost:    7
c ---[ 277]---> BDD-cost:    7
c ---[ 276]---> BDD-cost:    7
c ---[ 275]---> BDD-cost:    7
c ---[ 274]---> BDD-cost:    7
c ---[ 273]---> BDD-cost:    7
c ---[ 272]---> BDD-cost:    7
c ---[ 271]---> BDD-cost:    7
c ---[ 270]---> BDD-cost:    7
c ---[ 269]---> BDD-cost:    7
c ---[ 268]---> BDD-cost:    7
c ---[ 267]---> BDD-cost:    7
c ---[ 266]---> BDD-cost:    7
c ---[ 265]---> BDD-cost:    7
c ---[ 264]---> BDD-cost:    7
c ---[ 263]---> BDD-cost:    7
c ---[ 262]---> BDD-cost:    7
c ---[ 261]---> BDD-cost:    7
c ---[ 260]---> BDD-cost:    7
c ---[ 259]---> BDD-cost:    7
c ---[ 258]---> BDD-cost:    7
c ---[ 257]---> BDD-cost:    7
c ---[ 256]---> BDD-cost:    7
c ---[ 255]---> BDD-cost:    7
c ---[ 254]---> BDD-cost:    7
c ---[ 253]---> BDD-cost:    7
c ---[ 252]---> BDD-cost:    8
c ---[ 251]---> BDD-cost:    8
c ---[ 250]---> BDD-cost:    8
c ---[ 249]---> BDD-cost:    8
c ---[ 248]---> BDD-cost:    8
c ---[ 247]---> BDD-cost:    8
c ---[ 246]---> BDD-cost:    8
c ---[ 245]---> BDD-cost:    8
c ---[ 244]---> BDD-cost:    8
c ---[ 243]---> BDD-cost:    8
c ---[ 242]---> BDD-cost:    8
c ---[ 241]---> BDD-cost:    8
c ---[ 240]---> BDD-cost:    8
c ---[ 239]---> BDD-cost:    8
c ---[ 238]---> BDD-cost:    8
c ---[ 237]---> BDD-cost:    8
c ---[ 236]---> BDD-cost:    8
c ---[ 235]---> BDD-cost:    8
c ---[ 234]---> BDD-cost:    8
c ---[ 233]---> BDD-cost:    8
c ---[ 232]---> BDD-cost:    8
c ---[ 231]---> BDD-cost:    8
c ---[ 230]---> BDD-cost:    8
c ---[ 229]---> BDD-cost:    8
c ---[ 228]---> BDD-cost:    8
c ---[ 227]---> BDD-cost:    8
c ---[ 226]---> BDD-cost:    8
c ---[ 225]---> BDD-cost:    8
c ---[ 224]---> BDD-cost:    8
c ---[ 223]---> BDD-cost:    8
c ---[ 222]---> BDD-cost:    8
c ---[ 221]---> BDD-cost:    8
c ---[ 220]---> BDD-cost:    8
c ---[ 219]---> BDD-cost:    8
c ---[ 218]---> BDD-cost:    8
c ---[ 217]---> BDD-cost:    8
c ---[ 216]---> BDD-cost:    8
c ---[ 215]---> BDD-cost:    8
c ---[ 214]---> BDD-cost:    8
c ---[ 213]---> BDD-cost:    8
c ---[ 212]---> BDD-cost:    8
c ---[ 211]---> BDD-cost:    8
c ---[ 210]---> BDD-cost:    8
c ---[ 209]---> BDD-cost:    8
c ---[ 208]---> BDD-cost:    8
c ---[ 207]---> BDD-cost:    8
c ---[ 206]---> BDD-cost:    8
c ---[ 205]---> BDD-cost:    8
c ---[ 204]---> BDD-cost:    8
c ---[ 203]---> BDD-cost:    8
c ---[ 202]---> BDD-cost:    8
c ---[ 201]---> BDD-cost:    8
c ---[ 200]---> BDD-cost:    8
c ---[ 199]---> BDD-cost:    8
c ---[ 198]---> BDD-cost:    8
c ---[ 197]---> BDD-cost:    8
c ---[ 196]---> BDD-cost:    8
c ---[ 195]---> BDD-cost:    8
c ---[ 194]---> BDD-cost:    8
c ---[ 193]---> BDD-cost:    8
c ---[ 192]---> BDD-cost:    8
c ---[ 191]---> BDD-cost:    8
c ---[ 190]---> BDD-cost:    8
c ---[ 189]---> BDD-cost:    8
c ---[ 188]---> BDD-cost:    8
c ---[ 187]---> BDD-cost:    8
c ---[ 186]---> BDD-cost:    8
c ---[ 185]---> BDD-cost:    8
c ---[ 184]---> BDD-cost:    8
c ---[ 183]---> BDD-cost:    8
c ---[ 182]---> BDD-cost:    8
c ---[ 181]---> BDD-cost:    8
c ---[ 180]---> BDD-cost:    8
c ---[ 179]---> BDD-cost:    8
c ---[ 178]---> BDD-cost:    8
c ---[ 177]---> BDD-cost:    8
c ---[ 176]---> BDD-cost:    8
c ---[ 175]---> BDD-cost:    8
c ---[ 174]---> BDD-cost:    8
c ---[ 173]---> BDD-cost:    8
c ---[ 172]---> BDD-cost:    8
c ---[ 171]---> BDD-cost:    8
c ---[ 170]---> BDD-cost:    8
c ---[ 169]---> BDD-cost:    8
c ---[ 168]---> BDD-cost:    8
c ---[ 167]---> BDD-cost:    8
c ---[ 166]---> BDD-cost:    8
c ---[ 165]---> BDD-cost:    8
c ---[ 164]---> BDD-cost:    8
c ---[ 163]---> BDD-cost:    8
c ---[ 162]---> BDD-cost:    8
c ---[ 161]---> BDD-cost:    8
c ---[ 160]---> BDD-cost:    8
c ---[ 159]---> BDD-cost:    8
c ---[ 158]---> BDD-cost:    8
c ---[ 157]---> BDD-cost:    8
c ---[ 156]---> BDD-cost:    8
c ---[ 155]---> BDD-cost:    8
c ---[ 154]---> BDD-cost:    8
c ---[ 153]---> BDD-cost:    8
c ---[ 152]---> BDD-cost:    8
c ---[ 151]---> BDD-cost:    8
c ---[ 150]---> BDD-cost:    8
c ---[ 149]---> BDD-cost:    8
c ---[ 148]---> BDD-cost:    8
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:    8
c ---[ 145]---> BDD-cost:    8
c ---[ 144]---> BDD-cost:    8
c ---[ 143]---> BDD-cost:    8
c ---[ 142]---> BDD-cost:    8
c ---[ 141]---> BDD-cost:    8
c ---[ 140]---> BDD-cost:    8
c ---[ 139]---> BDD-cost:    8
c ---[ 138]---> BDD-cost:    8
c ---[ 137]---> BDD-cost:    8
c ---[ 136]---> BDD-cost:    8
c ---[ 135]---> BDD-cost:    8
c ---[ 134]---> BDD-cost:    8
c ---[ 133]---> BDD-cost:    8
c ---[ 132]---> BDD-cost:    8
c ---[ 131]---> BDD-cost:    8
c ---[ 130]---> BDD-cost:    8
c ---[ 129]---> BDD-cost:    8
c ---[ 128]---> BDD-cost:    8
c ---[ 127]---> BDD-cost:    8
c ---[ 126]---> BDD-cost:    8
c ---[ 125]---> BDD-cost:    8
c ---[ 124]---> BDD-cost:    8
c ---[ 123]---> BDD-cost:    8
c ---[ 122]---> BDD-cost:    8
c ---[ 121]---> BDD-cost:    8
c ---[ 120]---> BDD-cost:    8
c ---[ 119]---> BDD-cost:    8
c ---[ 118]---> BDD-cost:    8
c ---[ 117]---> BDD-cost:    8
c ---[ 116]---> BDD-cost:    8
c ---[ 115]---> BDD-cost:    8
c ---[ 114]---> BDD-cost:    8
c ---[ 113]---> BDD-cost:    8
c ---[ 112]---> BDD-cost:    8
c ---[ 111]---> BDD-cost:    8
c ---[ 110]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:    8
c ---[ 108]---> BDD-cost:    8
c ---[ 107]---> BDD-cost:    8
c ---[ 106]---> BDD-cost:    8
c ---[ 105]---> BDD-cost:    8
c ---[ 104]---> BDD-cost:    8
c ---[ 103]---> BDD-cost:    8
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    8
c ---[ 100]---> BDD-cost:    8
c ---[  99]---> BDD-cost:    8
c ---[  98]---> BDD-cost:    8
c ---[  97]---> BDD-cost:    8
c ---[  96]---> BDD-cost:    8
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    8
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:    8
c ---[  90]---> BDD-cost:    8
c ---[  89]---> BDD-cost:    8
c ---[  88]---> BDD-cost:    8
c ---[  87]---> BDD-cost:    8
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:    8
c ---[  84]---> BDD-cost:    8
c ---[  83]---> BDD-cost:    8
c ---[  82]---> BDD-cost:    8
c ---[  81]---> BDD-cost:    8
c ---[  80]---> BDD-cost:    8
c ---[  79]---> BDD-cost:    8
c ---[  78]---> BDD-cost:    8
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:    8
c ---[  75]---> BDD-cost:    8
c ---[  74]---> BDD-cost:    8
c ---[  73]---> BDD-cost:    8
c ---[  72]---> BDD-cost:    8
c ---[  71]---> BDD-cost:    8
c ---[  70]---> BDD-cost:    8
c ---[  69]---> BDD-cost:    8
c ---[  68]---> BDD-cost:    8
c ---[  67]---> BDD-cost:    8
c ---[  66]---> BDD-cost:    8
c ---[  65]---> BDD-cost:    8
c ---[  64]---> BDD-cost:    8
c ---[  63]---> BDD-cost:    8
c ---[  62]---> BDD-cost:    8
c ---[  61]---> BDD-cost:    8
c ---[  60]---> BDD-cost:    8
c ---[  59]---> BDD-cost:    8
c ---[  58]---> BDD-cost:    8
c ---[  57]---> BDD-cost:    8
c ---[  56]---> BDD-cost:    8
c ---[  55]---> BDD-cost:    8
c ---[  54]---> BDD-cost:    8
c ---[  53]---> BDD-cost:    8
c ---[  52]---> BDD-cost:    8
c ---[  51]---> BDD-cost:    8
c ---[  50]---> BDD-cost:    8
c ---[  49]---> BDD-cost:    8
c ---[  48]---> BDD-cost:    8
c ---[  47]---> BDD-cost:    8
c ---[  46]---> BDD-cost:    8
c ---[  45]---> BDD-cost:    8
c ---[  44]---> BDD-cost:    8
c ---[  43]---> BDD-cost:    8
c ---[  42]---> BDD-cost:    8
c ---[  41]---> BDD-cost:    8
c ---[  40]---> BDD-cost:    8
c ---[  39]---> BDD-cost:    8
c ---[  38]---> BDD-cost:    8
c ---[  37]---> BDD-cost:    8
c ---[  36]---> BDD-cost:    8
c ---[  35]---> BDD-cost:    8
c ---[  34]---> BDD-cost:    8
c ---[  33]---> BDD-cost:    8
c ---[  32]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:    8
c ---[  28]---> BDD-cost:    8
c ---[  27]---> BDD-cost:    8
c ---[  23]---> Adder-cost: 16837   maxlim: 101745   bits: 18/17
c ---[  22]---> Adder-cost: 35787   maxlim: 6633569   bits: 24/23
c ---[  21]---> Adder-cost: 18126   maxlim: 4660379   bits: 24/23
c ---[  20]---> Adder-cost: 13526   maxlim: 7782034   bits: 24/23
c ---[  19]---> Adder-cost: 46920   maxlim: 49412548   bits: 27/26
c ---[  18]---> Adder-cost: 7270   maxlim: 202757   bits: 18/18
c ---[  17]---> Adder-cost: 28854   maxlim: 3340290   bits: 23/22
c ---[  16]---> Adder-cost: 44525   maxlim: 3367019   bits: 23/22
c ---[  15]---> Adder-cost: 37629   maxlim: 7305239   bits: 24/23
c ---[  14]---> Adder-cost: 14038   maxlim: 171104   bits: 19/18
c ---[  13]---> Adder-cost: 18310   maxlim: 585650   bits: 20/20
c ---[  12]---> Adder-cost: 51276   maxlim: 48594727   bits: 27/26
c ---[  11]---> Adder-cost: 2096   maxlim: 88902   bits: 17/17
c ---[  10]---> Adder-cost: 8416   maxlim: 4571464   bits: 23/23
c ---[   9]---> Adder-cost: 28701   maxlim: 3985139   bits: 23/22
c ---[   8]---> Adder-cost: 4168   maxlim: 64077   bits: 17/16
c ---[   7]---> Adder-cost: 4299   maxlim: 30599   bits: 16/15
c ---[   6]---> Adder-cost: 4676   maxlim: 35189   bits: 17/16
c ---[   5]---> Adder-cost: 8358   maxlim: 67319   bits: 18/17
c ---[   4]---> Adder-cost: 4270   maxlim: 73024   bits: 17/17
c ---[   3]---> Adder-cost: 3309   maxlim: 24989   bits: 16/15
c ---[   2]---> Adder-cost: 2149   maxlim: 15809   bits: 15/14
c ---[   1]---> Adder-cost: 5642   maxlim: 93949   bits: 18/17
c ---[   0]---> Adder-cost: 3842   maxlim: 34424   bits: 17/16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2898715 10345966 |  966238       0        0     nan |  0.000 % |
c |       100 | 2898715 10345966 | 1062861     100      319     3.2 |  0.309 % |
c |       250 | 2898715 10345966 | 1169147     250      870     3.5 |  0.309 % |
c |       475 | 2898715 10345966 | 1286062     475     1792     3.8 |  0.309 % |
c |       812 | 2898715 10345966 | 1414669     812     2966     3.7 |  0.309 % |
c |      1318 | 2898715 10345966 | 1556135    1318     4803     3.6 |  0.309 % |
c |      2077 | 2898715 10345966 | 1711749    2077     7465     3.6 |  0.309 % |
c |      3216 | 2898715 10345966 | 1882924    3216    14652     4.6 |  0.309 % |
c |      4924 | 2898715 10345966 | 2071216    4924    20442     4.2 |  0.309 % |
c |      7486 | 2898715 10345966 | 2278338    7486    37183     5.0 |  0.309 % |
c |     11330 | 2898715 10345966 | 2506172   11330    52287     4.6 |  0.309 % |
c |     17096 | 2898715 10345966 | 2756789   17096    76790     4.5 |  0.309 % |
c |     25746 | 2898715 10345966 | 3032468   25746   363288    14.1 |  0.309 % |
c |     38720 | 2898715 10345966 | 3335715   38720   453362    11.7 |  0.309 % |
c |     58181 | 2898715 10345966 | 3669287   58181  1092330    18.8 |  0.309 % |
c |     87373 | 2898708 10345943 | 4036215   87372  1880976    21.5 |  0.309 % |
c |    131164 | 2898701 10345920 | 4439837  131162  3644072    27.8 |  0.309 % |
c |    196848 | 2898689 10345886 | 4883821  196844  6854364    34.8 |  0.310 % |
c |    295375 | 2898689 10345886 | 5372203  295371 12286298    41.6 |  0.310 % |
#### 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.91 0.98 0.91 2/54 15071
Raw data (stat): 15071 (runsolver) R 15070 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489533577 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 10556 0 0 0 971 27 0 0 25 0 1 0 489533577 39518208 7165 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9648 7165 603 41 0 9607 0
vsize: 38592
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 10556 0 0 0 1971 27 0 0 25 0 1 0 489533577 39518208 7165 4294967295 134512640 134672761 3221224544 3221222960 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9648 7165 603 41 0 9607 0
vsize: 38592
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 19554 0 0 0 2953 46 0 0 25 0 1 0 489533577 70127616 13395 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17121 13395 603 41 0 17080 0
vsize: 68484
[startup+40.0016 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 20510 0 0 0 3951 48 0 0 25 0 1 0 489533577 70127616 13395 4294967295 134512640 134672761 3221224544 3221222152 134544673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17121 13395 603 41 0 17080 0
vsize: 68484
[startup+50.0028 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 36830 0 0 0 4912 87 0 0 25 0 1 0 489533577 140980224 28795 4294967295 134512640 134672761 3221224544 3221218328 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34419 28796 603 41 0 34378 0
vsize: 137676
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 61655 0 0 0 5854 144 0 0 25 0 1 0 489533577 245358592 53620 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59902 53620 603 41 0 59861 0
vsize: 239608
[startup+70.0032 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 62209 0 0 0 6852 147 0 0 25 0 1 0 489533577 247656448 54174 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60463 54174 603 41 0 60422 0
vsize: 241852
[startup+80.0037 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 62661 0 0 0 7850 149 0 0 25 0 1 0 489533577 249548800 54626 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60925 54626 603 41 0 60884 0
vsize: 243700
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 62965 0 0 0 8850 150 0 0 25 0 1 0 489533577 250765312 54930 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61222 54930 603 41 0 61181 0
vsize: 244888
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 63232 0 0 0 9848 151 0 0 25 0 1 0 489533577 251846656 55197 4294967295 134512640 134672761 3221224544 3221223712 134564676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61486 55197 603 41 0 61445 0
vsize: 245944
[startup+110.003 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 63419 0 0 0 10848 151 0 0 25 0 1 0 489533577 252645376 55384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61681 55384 603 41 0 61640 0
vsize: 246724
[startup+120.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 63913 0 0 0 11847 153 0 0 25 0 1 0 489533577 254668800 55878 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62175 55878 603 41 0 62134 0
vsize: 248700
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 64033 0 0 0 12847 153 0 0 25 0 1 0 489533577 255209472 55998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62307 55998 603 41 0 62266 0
vsize: 249228
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 64148 0 0 0 13846 154 0 0 25 0 1 0 489533577 255614976 56113 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62406 56113 603 41 0 62365 0
vsize: 249624
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 64266 0 0 0 14846 154 0 0 25 0 1 0 489533577 256020480 56231 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62505 56231 603 41 0 62464 0
vsize: 250020
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 64382 0 0 0 15846 155 0 0 25 0 1 0 489533577 256688128 56347 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62668 56347 603 41 0 62627 0
vsize: 250672
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 64462 0 0 0 16846 155 0 0 25 0 1 0 489533577 256958464 56427 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62734 56427 603 41 0 62693 0
vsize: 250936
[startup+180.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 64537 0 0 0 17845 155 0 0 25 0 1 0 489533577 257228800 56502 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62800 56502 603 41 0 62759 0
vsize: 251200
[startup+190.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 64823 0 0 0 18844 156 0 0 25 0 1 0 489533577 258445312 56788 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63097 56788 603 41 0 63056 0
vsize: 252388
[startup+200.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 65400 0 0 0 19842 158 0 0 25 0 1 0 489533577 260730880 57365 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63655 57365 603 41 0 63614 0
vsize: 254620
[startup+210.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 65591 0 0 0 20841 159 0 0 25 0 1 0 489533577 261541888 57556 4294967295 134512640 134672761 3221224544 3221223668 134566007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63853 57556 603 41 0 63812 0
vsize: 255412
[startup+220.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 65699 0 0 0 21841 160 0 0 25 0 1 0 489533577 261947392 57664 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63952 57664 603 41 0 63911 0
vsize: 255808
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 65792 0 0 0 22840 160 0 0 25 0 1 0 489533577 262352896 57757 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64051 57757 603 41 0 64010 0
vsize: 256204
[startup+240.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 65977 0 0 0 23840 161 0 0 25 0 1 0 489533577 263290880 57942 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64280 57942 603 41 0 64239 0
vsize: 257120
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 66057 0 0 0 24839 162 0 0 25 0 1 0 489533577 263561216 58022 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64346 58022 603 41 0 64305 0
vsize: 257384
[startup+260.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 66364 0 0 0 25839 163 0 0 25 0 1 0 489533577 264908800 58329 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64675 58329 603 41 0 64634 0
vsize: 258700
[startup+270.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 66806 0 0 0 26838 164 0 0 25 0 1 0 489533577 266723328 58771 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65118 58771 603 41 0 65077 0
vsize: 260472
[startup+280.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 66961 0 0 0 27838 164 0 0 25 0 1 0 489533577 267264000 58926 4294967295 134512640 134672761 3221224544 3221223712 134560788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65250 58926 603 41 0 65209 0
vsize: 261000
[startup+290.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 67211 0 0 0 28837 165 0 0 25 0 1 0 489533577 268341248 59176 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65513 59176 603 41 0 65472 0
vsize: 262052
[startup+300.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 67571 0 0 0 29836 166 0 0 25 0 1 0 489533577 269815808 59536 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65873 59536 603 41 0 65832 0
vsize: 263492
[startup+310.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 15071
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 67911 0 0 0 30835 167 0 0 25 0 1 0 489533577 271163392 59876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66202 59876 603 41 0 66161 0
vsize: 264808
[startup+320.013 s]
Raw data (loadavg): 1.07 0.99 0.92 2/57 15112
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 68237 0 0 0 31834 168 0 0 25 0 1 0 489533577 272506880 60202 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66530 60202 603 41 0 66489 0
vsize: 266120
[startup+330.014 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 15124
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 68497 0 0 0 32832 171 0 0 25 0 1 0 489533577 273453056 60462 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66761 60462 603 41 0 66720 0
vsize: 267044
[startup+340.013 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 15124
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 68782 0 0 0 33831 171 0 0 25 0 1 0 489533577 274657280 60747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67055 60747 603 41 0 67014 0
vsize: 268220
[startup+350.013 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 15124
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69026 0 0 0 34830 173 0 0 25 0 1 0 489533577 275595264 60991 4294967295 134512640 134672761 3221224544 3221223648 134555175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67284 60991 603 41 0 67243 0
vsize: 269136
[startup+360.014 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 15124
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69147 0 0 0 35830 173 0 0 25 0 1 0 489533577 276664320 61112 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67545 61112 603 41 0 67504 0
vsize: 270180
[startup+370.014 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 15124
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69209 0 0 0 36830 173 0 0 25 0 1 0 489533577 276934656 61174 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67611 61174 603 41 0 67570 0
vsize: 270444
[startup+380.014 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 15124
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69271 0 0 0 37830 173 0 0 25 0 1 0 489533577 277204992 61236 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67677 61236 603 41 0 67636 0
vsize: 270708
[startup+390.014 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69316 0 0 0 38830 174 0 0 25 0 1 0 489533577 277340160 61281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67710 61281 603 41 0 67669 0
vsize: 270840
[startup+400.015 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69372 0 0 0 39830 174 0 0 25 0 1 0 489533577 277610496 61337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67776 61337 603 41 0 67735 0
vsize: 271104
[startup+410.015 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69420 0 0 0 40830 174 0 0 25 0 1 0 489533577 277745664 61385 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67809 61385 603 41 0 67768 0
vsize: 271236
[startup+420.015 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69486 0 0 0 41830 174 0 0 25 0 1 0 489533577 278016000 61451 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67875 61451 603 41 0 67834 0
vsize: 271500
[startup+430.016 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69525 0 0 0 42830 174 0 0 25 0 1 0 489533577 278151168 61490 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67908 61490 603 41 0 67867 0
vsize: 271632
[startup+440.017 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69576 0 0 0 43830 175 0 0 25 0 1 0 489533577 278286336 61541 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67941 61541 603 41 0 67900 0
vsize: 271764
[startup+450.017 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69611 0 0 0 44830 175 0 0 25 0 1 0 489533577 278421504 61576 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67974 61576 603 41 0 67933 0
vsize: 271896
[startup+460.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69677 0 0 0 45830 175 0 0 25 0 1 0 489533577 278700032 61642 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68042 61642 603 41 0 68001 0
vsize: 272168
[startup+470.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 69845 0 0 0 46830 175 0 0 25 0 1 0 489533577 279375872 61810 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68207 61810 603 41 0 68166 0
vsize: 272828
[startup+480.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 70022 0 0 0 47830 176 0 0 25 0 1 0 489533577 280104960 61987 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68385 61987 603 41 0 68344 0
vsize: 273540
[startup+490.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 70158 0 0 0 48830 176 0 0 25 0 1 0 489533577 280731648 62123 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68538 62123 603 41 0 68497 0
vsize: 274152
[startup+500.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 70206 0 0 0 49830 176 0 0 25 0 1 0 489533577 281001984 62171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68604 62171 603 41 0 68563 0
vsize: 274416
[startup+510.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 70260 0 0 0 50830 176 0 0 25 0 1 0 489533577 281137152 62225 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68637 62225 603 41 0 68596 0
vsize: 274548
[startup+520.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 70419 0 0 0 51829 177 0 0 25 0 1 0 489533577 281812992 62384 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68802 62384 603 41 0 68761 0
vsize: 275208
[startup+530.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 71157 0 0 0 52827 179 0 0 25 0 1 0 489533577 284774400 63122 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69525 63122 603 41 0 69484 0
vsize: 278100
[startup+540.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 71811 0 0 0 53825 181 0 0 25 0 1 0 489533577 287477760 63776 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70185 63776 603 41 0 70144 0
vsize: 280740
[startup+550.019 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 72387 0 0 0 54824 182 0 0 25 0 1 0 489533577 289763328 64352 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70743 64352 603 41 0 70702 0
vsize: 282972
[startup+560.02 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 72843 0 0 0 55824 183 0 0 25 0 1 0 489533577 291655680 64808 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71205 64808 603 41 0 71164 0
vsize: 284820
[startup+570.021 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 72994 0 0 0 56824 184 0 0 25 0 1 0 489533577 292343808 64959 4294967295 134512640 134672761 3221224544 3221223712 134564752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71373 64959 603 41 0 71332 0
vsize: 285492
[startup+580.021 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 73096 0 0 0 57823 184 0 0 25 0 1 0 489533577 292753408 65061 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71473 65061 603 41 0 71432 0
vsize: 285892
[startup+590.021 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 73299 0 0 0 58823 185 0 0 25 0 1 0 489533577 293556224 65264 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71669 65264 603 41 0 71628 0
vsize: 286676
[startup+600.022 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 73702 0 0 0 59822 186 0 0 25 0 1 0 489533577 295178240 65667 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72065 65667 603 41 0 72024 0
vsize: 288260
[startup+610.022 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 74046 0 0 0 60821 187 0 0 25 0 1 0 489533577 296534016 66011 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72396 66011 603 41 0 72355 0
vsize: 289584
[startup+620.023 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 74652 0 0 0 61819 189 0 0 25 0 1 0 489533577 298962944 66617 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72989 66617 603 41 0 72948 0
vsize: 291956
[startup+630.023 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 75460 0 0 0 62816 192 0 0 25 0 1 0 489533577 302317568 67425 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73808 67425 603 41 0 73767 0
vsize: 295232
[startup+640.023 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 75765 0 0 0 63816 193 0 0 25 0 1 0 489533577 303534080 67730 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74105 67730 603 41 0 74064 0
vsize: 296420
[startup+650.023 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 76159 0 0 0 64815 194 0 0 25 0 1 0 489533577 305139712 68124 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74497 68124 603 41 0 74456 0
vsize: 297988
[startup+660.023 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 76554 0 0 0 65813 195 0 0 25 0 1 0 489533577 306757632 68519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74892 68519 603 41 0 74851 0
vsize: 299568
[startup+670.024 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 76617 0 0 0 66813 195 0 0 25 0 1 0 489533577 307032064 68582 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74959 68582 603 41 0 74918 0
vsize: 299836
[startup+680.025 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15126
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 76659 0 0 0 67814 195 0 0 25 0 1 0 489533577 307167232 68624 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74992 68624 603 41 0 74951 0
vsize: 299968
[startup+690.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 76709 0 0 0 68813 196 0 0 25 0 1 0 489533577 307302400 68674 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75025 68674 603 41 0 74984 0
vsize: 300100
[startup+700.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 76742 0 0 0 69813 196 0 0 25 0 1 0 489533577 307437568 68707 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75058 68707 603 41 0 75017 0
vsize: 300232
[startup+710.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 76786 0 0 0 70813 196 0 0 25 0 1 0 489533577 307572736 68751 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75091 68751 603 41 0 75050 0
vsize: 300364
[startup+720.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 76814 0 0 0 71814 196 0 0 25 0 1 0 489533577 307707904 68779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75124 68779 603 41 0 75083 0
vsize: 300496
[startup+730.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 76849 0 0 0 72814 196 0 0 25 0 1 0 489533577 307843072 68814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75157 68814 603 41 0 75116 0
vsize: 300628
[startup+740.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 76962 0 0 0 73814 196 0 0 25 0 1 0 489533577 308383744 68927 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75289 68927 603 41 0 75248 0
vsize: 301156
[startup+750.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 77816 0 0 0 74812 198 0 0 25 0 1 0 489533577 311746560 69781 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76110 69781 603 41 0 76069 0
vsize: 304440
[startup+760.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 78335 0 0 0 75810 200 0 0 25 0 1 0 489533577 315035648 70300 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76913 70300 603 41 0 76872 0
vsize: 307652
[startup+770.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 78734 0 0 0 76809 201 0 0 25 0 1 0 489533577 316653568 70699 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77308 70699 603 41 0 77267 0
vsize: 309232
[startup+780.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 79135 0 0 0 77808 203 0 0 25 0 1 0 489533577 318349312 71100 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77722 71100 603 41 0 77681 0
vsize: 310888
[startup+790.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 79554 0 0 0 78807 205 0 0 25 0 1 0 489533577 319995904 71519 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78124 71519 603 41 0 78083 0
vsize: 312496
[startup+800.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 79978 0 0 0 79806 205 0 0 25 0 1 0 489533577 321744896 71943 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78551 71943 603 41 0 78510 0
vsize: 314204
[startup+810.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 80150 0 0 0 80805 206 0 0 25 0 1 0 489533577 322490368 72115 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78733 72115 603 41 0 78692 0
vsize: 314932
[startup+820.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 80283 0 0 0 81805 206 0 0 25 0 1 0 489533577 322895872 72248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78832 72248 603 41 0 78791 0
vsize: 315328
[startup+830.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 80433 0 0 0 82805 207 0 0 25 0 1 0 489533577 323567616 72398 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78996 72398 603 41 0 78955 0
vsize: 315984
[startup+840.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 80594 0 0 0 83804 207 0 0 25 0 1 0 489533577 324231168 72559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79158 72559 603 41 0 79117 0
vsize: 316632
[startup+850.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 80767 0 0 0 84804 208 0 0 25 0 1 0 489533577 324902912 72732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79322 72732 603 41 0 79281 0
vsize: 317288
[startup+860.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 80931 0 0 0 85804 208 0 0 25 0 1 0 489533577 325566464 72896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79484 72896 603 41 0 79443 0
vsize: 317936
[startup+870.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 81112 0 0 0 86803 209 0 0 25 0 1 0 489533577 326279168 73077 4294967295 134512640 134672761 3221224544 3221223728 134559239 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79658 73077 603 41 0 79617 0
vsize: 318632
[startup+880.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 81301 0 0 0 87803 209 0 0 25 0 1 0 489533577 327114752 73266 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79862 73266 603 41 0 79821 0
vsize: 319448
[startup+890.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 81501 0 0 0 88803 210 0 0 25 0 1 0 489533577 327880704 73466 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80049 73466 603 41 0 80008 0
vsize: 320196
[startup+900.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 81731 0 0 0 89802 211 0 0 25 0 1 0 489533577 328908800 73696 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80300 73696 603 41 0 80259 0
vsize: 321200
[startup+910.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 81859 0 0 0 90802 211 0 0 25 0 1 0 489533577 329322496 73824 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80401 73824 603 41 0 80360 0
vsize: 321604
[startup+920.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 81975 0 0 0 91802 211 0 0 25 0 1 0 489533577 329863168 73940 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80533 73940 603 41 0 80492 0
vsize: 322132
[startup+930.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 82140 0 0 0 92802 212 0 0 25 0 1 0 489533577 330543104 74105 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80699 74105 603 41 0 80658 0
vsize: 322796
[startup+940.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 82331 0 0 0 93802 212 0 0 25 0 1 0 489533577 331370496 74296 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80901 74296 603 41 0 80860 0
vsize: 323604
[startup+950.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 82511 0 0 0 94802 213 0 0 25 0 1 0 489533577 332046336 74476 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81066 74476 603 41 0 81025 0
vsize: 324264
[startup+960.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 82702 0 0 0 95802 213 0 0 25 0 1 0 489533577 332754944 74667 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81239 74667 603 41 0 81198 0
vsize: 324956
[startup+970.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 82888 0 0 0 96801 215 0 0 25 0 1 0 489533577 333557760 74853 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81435 74853 603 41 0 81394 0
vsize: 325740
[startup+980.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 83090 0 0 0 97801 215 0 0 25 0 1 0 489533577 334360576 75055 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81631 75055 603 41 0 81590 0
vsize: 326524
[startup+990.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 83284 0 0 0 98801 216 0 0 25 0 1 0 489533577 335171584 75249 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81829 75249 603 41 0 81788 0
vsize: 327316
[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 83525 0 0 0 99801 216 0 0 25 0 1 0 489533577 336109568 75490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82058 75490 603 41 0 82017 0
vsize: 328232
[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 83769 0 0 0 100800 217 0 0 25 0 1 0 489533577 337182720 75734 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82320 75734 603 41 0 82279 0
vsize: 329280
[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 84025 0 0 0 101800 218 0 0 25 0 1 0 489533577 338128896 75990 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82551 75990 603 41 0 82510 0
vsize: 330204
[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 84258 0 0 0 102799 218 0 0 25 0 1 0 489533577 339070976 76223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82781 76223 603 41 0 82740 0
vsize: 331124
[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 84482 0 0 0 103799 219 0 0 25 0 1 0 489533577 340025344 76447 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83014 76447 603 41 0 82973 0
vsize: 332056
[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 84713 0 0 0 104798 220 0 0 25 0 1 0 489533577 340967424 76678 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83244 76678 603 41 0 83203 0
vsize: 332976
[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 84925 0 0 0 105798 221 0 0 25 0 1 0 489533577 341913600 76890 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83475 76890 603 41 0 83434 0
vsize: 333900
[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 85209 0 0 0 106797 221 0 0 25 0 1 0 489533577 343126016 77174 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83771 77174 603 41 0 83730 0
vsize: 335084
[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 85466 0 0 0 107797 222 0 0 25 0 1 0 489533577 344121344 77431 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84014 77431 603 41 0 83973 0
vsize: 336056
[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 85595 0 0 0 108797 222 0 0 25 0 1 0 489533577 344666112 77560 4294967295 134512640 134672761 3221224544 3221223544 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84147 77560 603 41 0 84106 0
vsize: 336588
[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 85720 0 0 0 109797 222 0 0 25 0 1 0 489533577 345202688 77685 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84278 77685 603 41 0 84237 0
vsize: 337112
[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 85802 0 0 0 110797 223 0 0 25 0 1 0 489533577 345624576 77767 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84381 77767 603 41 0 84340 0
vsize: 337524
[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 85915 0 0 0 111797 223 0 0 25 0 1 0 489533577 346030080 77880 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84480 77880 603 41 0 84439 0
vsize: 337920
[startup+1130.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 86056 0 0 0 112796 223 0 0 25 0 1 0 489533577 346648576 78021 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84631 78021 603 41 0 84590 0
vsize: 338524
[startup+1140.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 86213 0 0 0 113797 223 0 0 25 0 1 0 489533577 347189248 78178 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84763 78178 603 41 0 84722 0
vsize: 339052
[startup+1150.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 86372 0 0 0 114796 224 0 0 25 0 1 0 489533577 347889664 78337 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84934 78337 603 41 0 84893 0
vsize: 339736
[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 86522 0 0 0 115796 224 0 0 25 0 1 0 489533577 348467200 78487 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85075 78487 603 41 0 85034 0
vsize: 340300
[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 86658 0 0 0 116796 224 0 0 25 0 1 0 489533577 349143040 78623 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85240 78623 603 41 0 85199 0
vsize: 340960
[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 86783 0 0 0 117796 225 0 0 25 0 1 0 489533577 349708288 78748 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85378 78748 603 41 0 85337 0
vsize: 341512
[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 86933 0 0 0 118796 225 0 0 25 0 1 0 489533577 350244864 78898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85509 78898 603 41 0 85468 0
vsize: 342036
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15128
Raw data (stat): 15071 (minisat+) R 15070 5897 5896 0 -1 0 87080 0 0 0 119796 225 0 0 25 0 1 0 489533577 350912512 79045 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85672 79045 603 41 0 85631 0
vsize: 342688
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.22 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 15128
Raw data (stat): 15071 (minisat+) Z 15070 5897 5896 0 -1 12 87082 0 0 0 119796 241 0 0 25 0 1 0 489533577 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.22
CPU time (s): 1200.38
CPU user time (s): 1197.96
CPU system time (s): 2.41163
CPU usage (%): 100.013
Max. virtual memory (Kb): 342688
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####