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 16217

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-21 06:29:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15774 boxname=wulflinc30 idbench=1214 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  6bb160e5eb0ef9c02ca7232f62836f2b  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-fit1d.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-fit1d.opb
IDLAUNCH: 15774
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 3
cpu MHz		: 451.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        651152 kB
Buffers:         24328 kB
Cached:         326960 kB
SwapCached:          0 kB
Active:         163132 kB
Inactive:       190964 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        650900 kB
SwapTotal:     2097892 kB
SwapFree:      2097824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            23760 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 06:49:28 (client local time) WITH STATUS 0 IN 1200.34 SECONDS
stats: 15774 7 1200.34 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 | 2897016 10335363 |  965672       0        0     nan |  0.000 % |
c |       100 | 2897016 10335363 | 1062239     100      316     3.2 |  0.309 % |
c |       250 | 2897016 10335363 | 1168463     250      805     3.2 |  0.309 % |
c |       475 | 2897016 10335363 | 1285309     475     1622     3.4 |  0.309 % |
c |       812 | 2897016 10335363 | 1413840     812     2791     3.4 |  0.309 % |
c |      1318 | 2897016 10335363 | 1555224    1318     4644     3.5 |  0.309 % |
c |      2078 | 2897016 10335363 | 1710746    2078     8307     4.0 |  0.309 % |
c |      3217 | 2897016 10335363 | 1881821    3217    12398     3.9 |  0.309 % |
c |      4926 | 2897016 10335363 | 2070003    4926    20547     4.2 |  0.309 % |
c |      7488 | 2897016 10335363 | 2277004    7488    31967     4.3 |  0.309 % |
c |     11332 | 2897016 10335363 | 2504704   11332    46641     4.1 |  0.309 % |
c |     17098 | 2897016 10335363 | 2755174   17098   118769     6.9 |  0.309 % |
c |     25748 | 2897016 10335363 | 3030692   25748   521490    20.3 |  0.309 % |
c |     38722 | 2897016 10335363 | 3333761   38722   599222    15.5 |  0.309 % |
c |     58183 | 2897016 10335363 | 3667137   58183  1594932    27.4 |  0.309 % |
c |     87375 | 2897002 10335317 | 4033851   87373  2712476    31.0 |  0.309 % |
c |    131165 | 2896996 10335300 | 4437236  131160  5322261    40.6 |  0.309 % |
c |    196849 | 2896984 10335266 | 4880960  196842  7921653    40.2 |  0.310 % |
c |    295376 | 2896984 10335266 | 5369056  295369 17704313    59.9 |  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.85 0.94 0.90 2/54 14254
Raw data (stat): 14254 (runsolver) R 14253 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542923813 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.001 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 10556 0 0 0 973 24 0 0 25 0 1 0 542923813 39518208 7165 4294967295 134512640 134672761 3221224624 3221222752 134597191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9648 7165 603 41 0 9607 0
vsize: 38592
[startup+20.0018 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 10556 0 0 0 1974 24 0 0 25 0 1 0 542923813 39518208 7165 4294967295 134512640 134672761 3221224624 3221223328 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9648 7165 603 41 0 9607 0
vsize: 38592
[startup+30.0023 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 19554 0 0 0 2956 43 0 0 25 0 1 0 542923813 70127616 13395 4294967295 134512640 134672761 3221224624 3221222464 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17121 13395 603 41 0 17080 0
vsize: 68484
[startup+40.0024 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 20512 0 0 0 3954 45 0 0 25 0 1 0 542923813 70291456 13397 4294967295 134512640 134672761 3221224624 3221222424 134544378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17161 13397 603 41 0 17120 0
vsize: 68644
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 37390 0 0 0 4917 81 0 0 25 0 1 0 542923813 143269888 29355 4294967295 134512640 134672761 3221224624 3221217816 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34978 29356 603 41 0 34937 0
vsize: 139912
[startup+60.0018 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 61973 0 0 0 5858 139 0 0 25 0 1 0 542923813 247099392 53938 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60327 53938 603 41 0 60286 0
vsize: 241308
[startup+70.0018 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 62508 0 0 0 6856 141 0 0 25 0 1 0 542923813 249397248 54473 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60888 54473 603 41 0 60847 0
vsize: 243552
[startup+80.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 62934 0 0 0 7855 142 0 0 25 0 1 0 542923813 251154432 54899 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61317 54899 603 41 0 61276 0
vsize: 245268
[startup+90.0021 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 63312 0 0 0 8854 143 0 0 25 0 1 0 542923813 252641280 55277 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61680 55277 603 41 0 61639 0
vsize: 246720
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 63621 0 0 0 9853 144 0 0 25 0 1 0 542923813 254025728 55586 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62018 55586 603 41 0 61977 0
vsize: 248072
[startup+110.014 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 64240 0 0 0 10852 146 0 0 25 0 1 0 542923813 256454656 56205 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62611 56205 603 41 0 62570 0
vsize: 250444
[startup+120.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 64404 0 0 0 11852 146 0 0 25 0 1 0 542923813 257130496 56369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62776 56369 603 41 0 62735 0
vsize: 251104
[startup+130.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 64560 0 0 0 12852 146 0 0 25 0 1 0 542923813 257806336 56525 4294967295 134512640 134672761 3221224624 3221223748 134566120 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62941 56525 603 41 0 62900 0
vsize: 251764
[startup+140.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 64690 0 0 0 13852 147 0 0 25 0 1 0 542923813 258211840 56655 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63040 56655 603 41 0 62999 0
vsize: 252160
[startup+150.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 64809 0 0 0 14852 147 0 0 25 0 1 0 542923813 258879488 56774 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63203 56774 603 41 0 63162 0
vsize: 252812
[startup+160.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 64901 0 0 0 15851 147 0 0 25 0 1 0 542923813 259284992 56866 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63302 56866 603 41 0 63261 0
vsize: 253208
[startup+170.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 64981 0 0 0 16851 148 0 0 25 0 1 0 542923813 259555328 56946 4294967295 134512640 134672761 3221224624 3221223792 134560767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63368 56946 603 41 0 63327 0
vsize: 253472
[startup+180.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 65057 0 0 0 17851 148 0 0 25 0 1 0 542923813 259825664 57022 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63434 57022 603 41 0 63393 0
vsize: 253736
[startup+190.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 65140 0 0 0 18851 148 0 0 25 0 1 0 542923813 260231168 57105 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63533 57105 603 41 0 63492 0
vsize: 254132
[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 65231 0 0 0 19850 149 0 0 25 0 1 0 542923813 260501504 57196 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63599 57196 603 41 0 63558 0
vsize: 254396
[startup+210.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 65792 0 0 0 20850 150 0 0 25 0 1 0 542923813 262791168 57757 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64158 57757 603 41 0 64117 0
vsize: 256632
[startup+220.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 66437 0 0 0 21848 152 0 0 25 0 1 0 542923813 265486336 58402 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64816 58402 603 41 0 64775 0
vsize: 259264
[startup+230.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 66678 0 0 0 22847 152 0 0 25 0 1 0 542923813 266428416 58643 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65046 58643 603 41 0 65005 0
vsize: 260184
[startup+240.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 67165 0 0 0 23847 153 0 0 25 0 1 0 542923813 268570624 59130 4294967295 134512640 134672761 3221224624 3221223792 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65569 59130 603 41 0 65528 0
vsize: 262276
[startup+250.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 67350 0 0 0 24846 154 0 0 25 0 1 0 542923813 269381632 59315 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65767 59315 603 41 0 65726 0
vsize: 263068
[startup+260.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 67702 0 0 0 25845 155 0 0 25 0 1 0 542923813 270864384 59667 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66129 59667 603 41 0 66088 0
vsize: 264516
[startup+270.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 68013 0 0 0 26844 156 0 0 25 0 1 0 542923813 272076800 59978 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66425 59978 603 41 0 66384 0
vsize: 265700
[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 68097 0 0 0 27844 156 0 0 25 0 1 0 542923813 272347136 60062 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66491 60062 603 41 0 66450 0
vsize: 265964
[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 68168 0 0 0 28844 156 0 0 25 0 1 0 542923813 272617472 60133 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66557 60133 603 41 0 66516 0
vsize: 266228
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 68507 0 0 0 29843 157 0 0 25 0 1 0 542923813 274096128 60472 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66918 60472 603 41 0 66877 0
vsize: 267672
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 69019 0 0 0 30843 159 0 0 25 0 1 0 542923813 276123648 60984 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67413 60984 603 41 0 67372 0
vsize: 269652
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 69281 0 0 0 31842 160 0 0 25 0 1 0 542923813 277204992 61246 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67677 61246 603 41 0 67636 0
vsize: 270708
[startup+330.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 69362 0 0 0 32842 160 0 0 25 0 1 0 542923813 277475328 61327 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67743 61327 603 41 0 67702 0
vsize: 270972
[startup+340.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 69422 0 0 0 33842 160 0 0 25 0 1 0 542923813 277745664 61387 4294967295 134512640 134672761 3221224624 3221223748 134566115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67809 61387 603 41 0 67768 0
vsize: 271236
[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 69514 0 0 0 34842 160 0 0 25 0 1 0 542923813 278151168 61479 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67908 61479 603 41 0 67867 0
vsize: 271632
[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 69587 0 0 0 35842 161 0 0 25 0 1 0 542923813 278421504 61552 4294967295 134512640 134672761 3221224624 3221223760 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67974 61552 603 41 0 67933 0
vsize: 271896
[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 69658 0 0 0 36842 161 0 0 25 0 1 0 542923813 278691840 61623 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68040 61623 603 41 0 67999 0
vsize: 272160
[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 69710 0 0 0 37842 161 0 0 25 0 1 0 542923813 278827008 61675 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68073 61675 603 41 0 68032 0
vsize: 272292
[startup+390.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 69769 0 0 0 38842 161 0 0 25 0 1 0 542923813 279097344 61734 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68139 61734 603 41 0 68098 0
vsize: 272556
[startup+400.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 70183 0 0 0 39840 163 0 0 25 0 1 0 542923813 280702976 62148 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68531 62148 603 41 0 68490 0
vsize: 274124
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 71050 0 0 0 40838 165 0 0 25 0 1 0 542923813 284336128 63015 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69418 63015 603 41 0 69377 0
vsize: 277672
[startup+420.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 71480 0 0 0 41836 167 0 0 25 0 1 0 542923813 286650368 63445 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69983 63445 603 41 0 69942 0
vsize: 279932
[startup+430.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 71606 0 0 0 42836 167 0 0 25 0 1 0 542923813 287055872 63571 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70082 63571 603 41 0 70041 0
vsize: 280328
[startup+440.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 71889 0 0 0 43835 168 0 0 25 0 1 0 542923813 288276480 63854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70380 63854 603 41 0 70339 0
vsize: 281520
[startup+450.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 72134 0 0 0 44835 169 0 0 25 0 1 0 542923813 289222656 64099 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70611 64099 603 41 0 70570 0
vsize: 282444
[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 72410 0 0 0 45835 170 0 0 25 0 1 0 542923813 290304000 64375 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70875 64375 603 41 0 70834 0
vsize: 283500
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 72659 0 0 0 46833 171 0 0 25 0 1 0 542923813 291377152 64624 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71137 64624 603 41 0 71096 0
vsize: 284548
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 72876 0 0 0 47833 172 0 0 25 0 1 0 542923813 292196352 64841 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71337 64841 603 41 0 71296 0
vsize: 285348
[startup+490.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 73081 0 0 0 48833 172 0 0 25 0 1 0 542923813 293023744 65046 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71539 65046 603 41 0 71498 0
vsize: 286156
[startup+500.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 73284 0 0 0 49832 173 0 0 25 0 1 0 542923813 293961728 65249 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71768 65249 603 41 0 71727 0
vsize: 287072
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 73460 0 0 0 50831 174 0 0 25 0 1 0 542923813 294633472 65425 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71932 65425 603 41 0 71891 0
vsize: 287728
[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 73657 0 0 0 51831 174 0 0 25 0 1 0 542923813 295444480 65622 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72130 65622 603 41 0 72089 0
vsize: 288520
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 73819 0 0 0 52831 175 0 0 25 0 1 0 542923813 296120320 65784 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72295 65784 603 41 0 72254 0
vsize: 289180
[startup+540.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 74000 0 0 0 53830 175 0 0 25 0 1 0 542923813 296931328 65965 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72493 65965 603 41 0 72452 0
vsize: 289972
[startup+550.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 74164 0 0 0 54830 176 0 0 25 0 1 0 542923813 297615360 66129 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72660 66129 603 41 0 72619 0
vsize: 290640
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 74337 0 0 0 55830 176 0 0 25 0 1 0 542923813 298291200 66302 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72825 66302 603 41 0 72784 0
vsize: 291300
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 74469 0 0 0 56830 177 0 0 25 0 1 0 542923813 298827776 66434 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72956 66434 603 41 0 72915 0
vsize: 291824
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 74600 0 0 0 57830 177 0 0 25 0 1 0 542923813 299372544 66565 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73089 66565 603 41 0 73048 0
vsize: 292356
[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 74758 0 0 0 58829 177 0 0 25 0 1 0 542923813 300109824 66723 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73269 66723 603 41 0 73228 0
vsize: 293076
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 74800 0 0 0 59828 178 0 0 25 0 1 0 542923813 300244992 66765 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73302 66765 603 41 0 73261 0
vsize: 293208
[startup+610.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 74838 0 0 0 60828 178 0 0 25 0 1 0 542923813 300380160 66803 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73335 66803 603 41 0 73294 0
vsize: 293340
[startup+620.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 74880 0 0 0 61828 178 0 0 25 0 1 0 542923813 300515328 66845 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73368 66845 603 41 0 73327 0
vsize: 293472
[startup+630.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 74993 0 0 0 62828 178 0 0 25 0 1 0 542923813 301051904 66958 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73499 66958 603 41 0 73458 0
vsize: 293996
[startup+640.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75033 0 0 0 63828 178 0 0 25 0 1 0 542923813 301187072 66998 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73532 66998 603 41 0 73491 0
vsize: 294128
[startup+650.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75070 0 0 0 64828 179 0 0 25 0 1 0 542923813 301322240 67035 4294967295 134512640 134672761 3221224624 3221223824 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73565 67035 603 41 0 73524 0
vsize: 294260
[startup+660.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75126 0 0 0 65828 179 0 0 25 0 1 0 542923813 301592576 67091 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73631 67091 603 41 0 73590 0
vsize: 294524
[startup+670.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75172 0 0 0 66828 179 0 0 25 0 1 0 542923813 301727744 67137 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73664 67137 603 41 0 73623 0
vsize: 294656
[startup+680.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75207 0 0 0 67828 179 0 0 25 0 1 0 542923813 301862912 67172 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73697 67172 603 41 0 73656 0
vsize: 294788
[startup+690.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75244 0 0 0 68829 179 0 0 25 0 1 0 542923813 301998080 67209 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73730 67209 603 41 0 73689 0
vsize: 294920
[startup+700.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75279 0 0 0 69829 179 0 0 25 0 1 0 542923813 302133248 67244 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73763 67244 603 41 0 73722 0
vsize: 295052
[startup+710.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75307 0 0 0 70829 179 0 0 25 0 1 0 542923813 302268416 67272 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73796 67272 603 41 0 73755 0
vsize: 295184
[startup+720.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75345 0 0 0 71829 179 0 0 25 0 1 0 542923813 302403584 67310 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73829 67310 603 41 0 73788 0
vsize: 295316
[startup+730.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75383 0 0 0 72829 179 0 0 25 0 1 0 542923813 302538752 67348 4294967295 134512640 134672761 3221224624 3221223776 134565070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73862 67348 603 41 0 73821 0
vsize: 295448
[startup+740.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75446 0 0 0 73829 180 0 0 25 0 1 0 542923813 302809088 67411 4294967295 134512640 134672761 3221224624 3221223748 134566062 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73928 67411 603 41 0 73887 0
vsize: 295712
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75518 0 0 0 74829 180 0 0 25 0 1 0 542923813 303079424 67483 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73994 67483 603 41 0 73953 0
vsize: 295976
[startup+760.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75547 0 0 0 75829 180 0 0 25 0 1 0 542923813 303214592 67512 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74027 67512 603 41 0 73986 0
vsize: 296108
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 75601 0 0 0 76829 180 0 0 25 0 1 0 542923813 303349760 67566 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74060 67566 603 41 0 74019 0
vsize: 296240
[startup+780.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 76369 0 0 0 77827 183 0 0 25 0 1 0 542923813 306450432 68334 4294967295 134512640 134672761 3221224624 3221223808 134559424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74817 68334 603 41 0 74776 0
vsize: 299268
[startup+790.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 77131 0 0 0 78825 185 0 0 25 0 1 0 542923813 309551104 69096 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75574 69096 603 41 0 75533 0
vsize: 302296
[startup+800.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 77635 0 0 0 79824 186 0 0 25 0 1 0 542923813 311693312 69600 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76097 69600 603 41 0 76056 0
vsize: 304388
[startup+810.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 78289 0 0 0 80823 188 0 0 25 0 1 0 542923813 314249216 70254 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76721 70254 603 41 0 76680 0
vsize: 306884
[startup+820.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 78891 0 0 0 81820 190 0 0 25 0 1 0 542923813 316801024 70856 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77344 70856 603 41 0 77303 0
vsize: 309376
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 79561 0 0 0 82818 193 0 0 25 0 1 0 542923813 319492096 71526 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78001 71526 603 41 0 77960 0
vsize: 312004
[startup+840.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 80182 0 0 0 83816 194 0 0 25 0 1 0 542923813 323088384 72147 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78879 72147 603 41 0 78838 0
vsize: 315516
[startup+850.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 80702 0 0 0 84815 196 0 0 25 0 1 0 542923813 325115904 72667 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79374 72667 603 41 0 79333 0
vsize: 317496
[startup+860.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 81252 0 0 0 85813 198 0 0 25 0 1 0 542923813 327393280 73217 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79930 73217 603 41 0 79889 0
vsize: 319720
[startup+870.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 81798 0 0 0 86811 200 0 0 25 0 1 0 542923813 329670656 73763 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80486 73763 603 41 0 80445 0
vsize: 321944
[startup+880.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 82341 0 0 0 87810 201 0 0 25 0 1 0 542923813 331866112 74306 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81022 74306 603 41 0 80981 0
vsize: 324088
[startup+890.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 82842 0 0 0 88809 202 0 0 25 0 1 0 542923813 333877248 74807 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81513 74807 603 41 0 81472 0
vsize: 326052
[startup+900.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 83302 0 0 0 89809 203 0 0 25 0 1 0 542923813 335765504 75267 4294967295 134512640 134672761 3221224624 3221223728 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81974 75267 603 41 0 81933 0
vsize: 327896
[startup+910.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 83737 0 0 0 90808 204 0 0 25 0 1 0 542923813 337534976 75702 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82406 75702 603 41 0 82365 0
vsize: 329624
[startup+920.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 84195 0 0 0 91807 206 0 0 25 0 1 0 542923813 339415040 76160 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82865 76160 603 41 0 82824 0
vsize: 331460
[startup+930.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 84646 0 0 0 92806 207 0 0 25 0 1 0 542923813 341299200 76611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83325 76611 603 41 0 83284 0
vsize: 333300
[startup+940.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 85046 0 0 0 93804 208 0 0 25 0 1 0 542923813 342921216 77011 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83721 77011 603 41 0 83680 0
vsize: 334884
[startup+950.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 85461 0 0 0 94804 209 0 0 25 0 1 0 542923813 344653824 77426 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84144 77426 603 41 0 84103 0
vsize: 336576
[startup+960.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 85733 0 0 0 95802 211 0 0 25 0 1 0 542923813 345735168 77698 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84408 77698 603 41 0 84367 0
vsize: 337632
[startup+970.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 85823 0 0 0 96802 211 0 0 25 0 1 0 542923813 346136576 77788 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84506 77788 603 41 0 84465 0
vsize: 338024
[startup+980.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 85931 0 0 0 97802 211 0 0 25 0 1 0 542923813 346546176 77896 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84606 77896 603 41 0 84565 0
vsize: 338424
[startup+990.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 86045 0 0 0 98802 211 0 0 25 0 1 0 542923813 346951680 78010 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84705 78010 603 41 0 84664 0
vsize: 338820
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 86162 0 0 0 99802 212 0 0 25 0 1 0 542923813 347488256 78127 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84836 78127 603 41 0 84795 0
vsize: 339344
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 86269 0 0 0 100801 212 0 0 25 0 1 0 542923813 347889664 78234 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84934 78234 603 41 0 84893 0
vsize: 339736
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 86382 0 0 0 101801 212 0 0 25 0 1 0 542923813 348422144 78347 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85064 78347 603 41 0 85023 0
vsize: 340256
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 86485 0 0 0 102801 213 0 0 25 0 1 0 542923813 348688384 78450 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85129 78450 603 41 0 85088 0
vsize: 340516
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 86583 0 0 0 103801 213 0 0 25 0 1 0 542923813 349089792 78548 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85227 78548 603 41 0 85186 0
vsize: 340908
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 86688 0 0 0 104801 214 0 0 25 0 1 0 542923813 349630464 78653 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85359 78653 603 41 0 85318 0
vsize: 341436
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 86804 0 0 0 105801 214 0 0 25 0 1 0 542923813 350040064 78769 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85459 78769 603 41 0 85418 0
vsize: 341836
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 86913 0 0 0 106801 214 0 0 25 0 1 0 542923813 350539776 78878 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85581 78878 603 41 0 85540 0
vsize: 342324
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 87017 0 0 0 107801 214 0 0 25 0 1 0 542923813 350945280 78982 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85680 78982 603 41 0 85639 0
vsize: 342720
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 87127 0 0 0 108800 215 0 0 25 0 1 0 542923813 351494144 79092 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85814 79092 603 41 0 85773 0
vsize: 343256
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 87237 0 0 0 109800 215 0 0 25 0 1 0 542923813 351899648 79202 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85913 79202 603 41 0 85872 0
vsize: 343652
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 87358 0 0 0 110800 216 0 0 25 0 1 0 542923813 352305152 79323 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86012 79323 603 41 0 85971 0
vsize: 344048
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 87458 0 0 0 111800 216 0 0 25 0 1 0 542923813 352706560 79423 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86110 79423 603 41 0 86069 0
vsize: 344440
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 87583 0 0 0 112800 216 0 0 25 0 1 0 542923813 353411072 79548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86282 79548 603 41 0 86241 0
vsize: 345128
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 87710 0 0 0 113800 216 0 0 25 0 1 0 542923813 353828864 79675 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86384 79675 603 41 0 86343 0
vsize: 345536
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 87856 0 0 0 114800 217 0 0 25 0 1 0 542923813 354484224 79821 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86544 79821 603 41 0 86503 0
vsize: 346176
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 88003 0 0 0 115799 217 0 0 25 0 1 0 542923813 355168256 79968 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86711 79968 603 41 0 86670 0
vsize: 346844
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 88150 0 0 0 116799 217 0 0 25 0 1 0 542923813 355708928 80115 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86843 80115 603 41 0 86802 0
vsize: 347372
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 88284 0 0 0 117799 218 0 0 25 0 1 0 542923813 356249600 80249 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86975 80249 603 41 0 86934 0
vsize: 347900
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 88428 0 0 0 118799 218 0 0 25 0 1 0 542923813 356786176 80393 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87106 80393 603 41 0 87065 0
vsize: 348424
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14254
Raw data (stat): 14254 (minisat+) R 14253 11931 11930 0 -1 0 88560 0 0 0 119799 218 0 0 25 0 1 0 542923813 357322752 80525 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87237 80525 603 41 0 87196 0
vsize: 348948
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 14254
Raw data (stat): 14254 (minisat+) Z 14253 11931 11930 0 -1 12 88562 0 0 0 119799 233 0 0 25 0 1 0 542923813 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.2
CPU time (s): 1200.34
CPU user time (s): 1198
CPU system time (s): 2.33864
CPU usage (%): 100.011
Max. virtual memory (Kb): 348948
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####