PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-fit1d.opb
MD5SUM	de6e9dcd85d0fedc70e76c82543d6a33
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	11514
Biggest coefficient in the objective function	2949120
Number of bits for the biggest coefficient in the objective function	22
Sum of the numbers in the objective function	462466666
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	3870720
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	580921206
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.18
Number of variables	11514
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	11
Maximum length of a constraint	11514
Trace number 23003

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-22 04:08:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=10782 boxname=wulflinc22 idbench=830 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  de6e9dcd85d0fedc70e76c82543d6a33  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-fit1d.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-fit1d.opb
IDLAUNCH: 10782
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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	: 3
cpu MHz		: 451.031
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:        721748 kB
Buffers:         27504 kB
Cached:         249268 kB
SwapCached:      12296 kB
Active:          53904 kB
Inactive:       236840 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        721468 kB
SwapTotal:     2097892 kB
SwapFree:      2085136 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5204 kB
Slab:            16520 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 04:28:14 (client local time) WITH STATUS 0 IN 1200.54 SECONDS
stats: 10782 7 1200.54 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:   10
c ---[1049]---> BDD-cost:   10
c ---[1048]---> BDD-cost:   10
c ---[1047]---> BDD-cost:   10
c ---[1046]---> BDD-cost:   10
c ---[1045]---> BDD-cost:   10
c ---[1044]---> BDD-cost:   10
c ---[1043]---> BDD-cost:   10
c ---[1042]---> BDD-cost:   10
c ---[1041]---> BDD-cost:   10
c ---[1040]---> BDD-cost:   10
c ---[1039]---> BDD-cost:   10
c ---[1038]---> BDD-cost:   10
c ---[1037]---> BDD-cost:   10
c ---[1036]---> BDD-cost:   10
c ---[1035]---> BDD-cost:   10
c ---[1034]---> BDD-cost:   10
c ---[1033]---> BDD-cost:   10
c ---[1032]---> BDD-cost:   10
c ---[1031]---> BDD-cost:   10
c ---[1030]---> BDD-cost:   10
c ---[1029]---> BDD-cost:   10
c ---[1028]---> BDD-cost:   10
c ---[1027]---> BDD-cost:   10
c ---[1026]---> BDD-cost:   10
c ---[1025]---> BDD-cost:   10
c ---[1024]---> BDD-cost:   10
c ---[1023]---> BDD-cost:   10
c ---[1022]---> BDD-cost:   10
c ---[1021]---> BDD-cost:   10
c ---[1020]---> BDD-cost:   10
c ---[1019]---> BDD-cost:   10
c ---[1018]---> BDD-cost:   10
c ---[1017]---> BDD-cost:   10
c ---[1016]---> BDD-cost:   10
c ---[1015]---> BDD-cost:   10
c ---[1014]---> BDD-cost:   10
c ---[1013]---> BDD-cost:   10
c ---[1012]---> BDD-cost:   10
c ---[1011]---> BDD-cost:   10
c ---[1010]---> BDD-cost:   10
c ---[1009]---> BDD-cost:   10
c ---[1008]---> BDD-cost:   10
c ---[1007]---> BDD-cost:   10
c ---[1006]---> BDD-cost:   10
c ---[1005]---> BDD-cost:   10
c ---[1004]---> BDD-cost:   10
c ---[1003]---> BDD-cost:   10
c ---[1002]---> BDD-cost:   10
c ---[1001]---> BDD-cost:   10
c ---[1000]---> BDD-cost:   10
c ---[ 999]---> BDD-cost:   10
c ---[ 998]---> BDD-cost:   10
c ---[ 997]---> BDD-cost:   10
c ---[ 996]---> BDD-cost:   10
c ---[ 995]---> BDD-cost:   10
c ---[ 994]---> BDD-cost:   10
c ---[ 993]---> BDD-cost:   10
c ---[ 992]---> BDD-cost:   10
c ---[ 991]---> BDD-cost:   10
c ---[ 990]---> BDD-cost:   10
c ---[ 989]---> BDD-cost:   10
c ---[ 988]---> BDD-cost:   10
c ---[ 987]---> BDD-cost:   10
c ---[ 986]---> BDD-cost:   10
c ---[ 985]---> BDD-cost:   10
c ---[ 984]---> BDD-cost:   10
c ---[ 983]---> BDD-cost:   10
c ---[ 982]---> BDD-cost:   10
c ---[ 981]---> BDD-cost:   10
c ---[ 980]---> BDD-cost:   10
c ---[ 979]---> BDD-cost:   10
c ---[ 978]---> BDD-cost:   10
c ---[ 977]---> BDD-cost:   10
c ---[ 976]---> BDD-cost:   10
c ---[ 975]---> BDD-cost:   10
c ---[ 974]---> BDD-cost:   10
c ---[ 973]---> BDD-cost:   10
c ---[ 972]---> BDD-cost:   10
c ---[ 971]---> BDD-cost:   10
c ---[ 970]---> BDD-cost:   10
c ---[ 969]---> BDD-cost:   10
c ---[ 968]---> BDD-cost:   10
c ---[ 967]---> BDD-cost:   10
c ---[ 966]---> BDD-cost:   10
c ---[ 965]---> BDD-cost:   10
c ---[ 964]---> BDD-cost:   10
c ---[ 963]---> BDD-cost:   10
c ---[ 962]---> BDD-cost:   10
c ---[ 961]---> BDD-cost:   10
c ---[ 960]---> BDD-cost:   10
c ---[ 959]---> BDD-cost:   10
c ---[ 958]---> BDD-cost:   10
c ---[ 957]---> BDD-cost:   10
c ---[ 956]---> BDD-cost:   10
c ---[ 955]---> BDD-cost:   10
c ---[ 954]---> BDD-cost:   10
c ---[ 953]---> BDD-cost:   10
c ---[ 952]---> BDD-cost:   10
c ---[ 951]---> BDD-cost:   10
c ---[ 950]---> BDD-cost:   10
c ---[ 949]---> BDD-cost:   10
c ---[ 948]---> BDD-cost:   10
c ---[ 947]---> BDD-cost:   10
c ---[ 946]---> BDD-cost:   10
c ---[ 945]---> BDD-cost:   10
c ---[ 944]---> BDD-cost:   10
c ---[ 943]---> BDD-cost:   10
c ---[ 942]---> BDD-cost:   10
c ---[ 941]---> BDD-cost:   10
c ---[ 940]---> BDD-cost:   10
c ---[ 939]---> BDD-cost:   10
c ---[ 938]---> BDD-cost:   10
c ---[ 937]---> BDD-cost:   10
c ---[ 936]---> BDD-cost:   10
c ---[ 935]---> BDD-cost:   10
c ---[ 934]---> BDD-cost:   10
c ---[ 933]---> BDD-cost:   10
c ---[ 932]---> BDD-cost:   10
c ---[ 931]---> BDD-cost:   10
c ---[ 930]---> BDD-cost:   10
c ---[ 929]---> BDD-cost:   10
c ---[ 928]---> BDD-cost:   10
c ---[ 927]---> BDD-cost:   10
c ---[ 926]---> BDD-cost:   10
c ---[ 925]---> BDD-cost:   10
c ---[ 924]---> BDD-cost:   10
c ---[ 923]---> BDD-cost:   10
c ---[ 922]---> BDD-cost:   10
c ---[ 921]---> BDD-cost:   10
c ---[ 920]---> BDD-cost:   10
c ---[ 919]---> BDD-cost:   10
c ---[ 918]---> BDD-cost:   10
c ---[ 917]---> BDD-cost:   10
c ---[ 916]---> BDD-cost:   10
c ---[ 915]---> BDD-cost:   10
c ---[ 914]---> BDD-cost:   10
c ---[ 913]---> BDD-cost:   10
c ---[ 912]---> BDD-cost:   10
c ---[ 911]---> BDD-cost:   10
c ---[ 910]---> BDD-cost:   10
c ---[ 909]---> BDD-cost:   10
c ---[ 908]---> BDD-cost:   10
c ---[ 907]---> BDD-cost:   10
c ---[ 906]---> BDD-cost:   10
c ---[ 905]---> BDD-cost:   10
c ---[ 904]---> BDD-cost:   10
c ---[ 903]---> BDD-cost:   10
c ---[ 902]---> BDD-cost:   10
c ---[ 901]---> BDD-cost:   10
c ---[ 900]---> BDD-cost:   10
c ---[ 899]---> BDD-cost:   10
c ---[ 898]---> BDD-cost:   10
c ---[ 897]---> BDD-cost:   10
c ---[ 896]---> BDD-cost:   10
c ---[ 895]---> BDD-cost:   10
c ---[ 894]---> BDD-cost:   10
c ---[ 893]---> BDD-cost:   10
c ---[ 892]---> BDD-cost:   10
c ---[ 891]---> BDD-cost:   10
c ---[ 890]---> BDD-cost:   10
c ---[ 889]---> BDD-cost:   10
c ---[ 888]---> BDD-cost:   10
c ---[ 887]---> BDD-cost:   10
c ---[ 886]---> BDD-cost:   10
c ---[ 885]---> BDD-cost:   10
c ---[ 884]---> BDD-cost:   10
c ---[ 883]---> BDD-cost:   10
c ---[ 882]---> BDD-cost:   10
c ---[ 881]---> BDD-cost:   10
c ---[ 880]---> BDD-cost:   10
c ---[ 879]---> BDD-cost:   10
c ---[ 878]---> BDD-cost:   10
c ---[ 877]---> BDD-cost:   10
c ---[ 876]---> BDD-cost:   10
c ---[ 875]---> BDD-cost:   10
c ---[ 874]---> BDD-cost:   10
c ---[ 873]---> BDD-cost:   10
c ---[ 872]---> BDD-cost:   10
c ---[ 871]---> BDD-cost:   10
c ---[ 870]---> BDD-cost:   10
c ---[ 869]---> BDD-cost:   10
c ---[ 868]---> BDD-cost:   10
c ---[ 867]---> BDD-cost:   10
c ---[ 866]---> BDD-cost:   10
c ---[ 865]---> BDD-cost:   10
c ---[ 864]---> BDD-cost:   10
c ---[ 863]---> BDD-cost:   10
c ---[ 862]---> BDD-cost:   10
c ---[ 861]---> BDD-cost:   10
c ---[ 860]---> BDD-cost:   10
c ---[ 859]---> BDD-cost:   10
c ---[ 858]---> BDD-cost:   10
c ---[ 857]---> BDD-cost:   10
c ---[ 856]---> BDD-cost:   10
c ---[ 855]---> BDD-cost:   10
c ---[ 854]---> BDD-cost:   10
c ---[ 853]---> BDD-cost:   10
c ---[ 852]---> BDD-cost:   10
c ---[ 851]---> BDD-cost:   10
c ---[ 850]---> BDD-cost:   10
c ---[ 849]---> BDD-cost:   10
c ---[ 848]---> BDD-cost:   10
c ---[ 847]---> BDD-cost:   10
c ---[ 846]---> BDD-cost:   10
c ---[ 845]---> BDD-cost:   10
c ---[ 844]---> BDD-cost:   10
c ---[ 843]---> BDD-cost:   10
c ---[ 842]---> BDD-cost:   10
c ---[ 841]---> BDD-cost:   10
c ---[ 840]---> BDD-cost:   10
c ---[ 839]---> BDD-cost:   10
c ---[ 838]---> BDD-cost:   10
c ---[ 837]---> BDD-cost:   10
c ---[ 836]---> BDD-cost:   10
c ---[ 835]---> BDD-cost:   10
c ---[ 834]---> BDD-cost:   10
c ---[ 833]---> BDD-cost:   10
c ---[ 832]---> BDD-cost:   10
c ---[ 831]---> BDD-cost:   10
c ---[ 830]---> BDD-cost:   10
c ---[ 829]---> BDD-cost:   10
c ---[ 828]---> BDD-cost:   10
c ---[ 827]---> BDD-cost:   10
c ---[ 826]---> BDD-cost:   10
c ---[ 825]---> BDD-cost:   10
c ---[ 824]---> BDD-cost:   10
c ---[ 823]---> BDD-cost:   10
c ---[ 822]---> BDD-cost:   10
c ---[ 821]---> BDD-cost:   10
c ---[ 820]---> BDD-cost:   10
c ---[ 819]---> BDD-cost:   10
c ---[ 818]---> BDD-cost:   10
c ---[ 817]---> BDD-cost:   10
c ---[ 816]---> BDD-cost:   10
c ---[ 815]---> BDD-cost:   10
c ---[ 814]---> BDD-cost:   10
c ---[ 813]---> BDD-cost:   10
c ---[ 812]---> BDD-cost:   10
c ---[ 811]---> BDD-cost:   10
c ---[ 810]---> BDD-cost:   10
c ---[ 809]---> BDD-cost:   10
c ---[ 808]---> BDD-cost:   10
c ---[ 807]---> BDD-cost:   10
c ---[ 806]---> BDD-cost:   10
c ---[ 805]---> BDD-cost:   10
c ---[ 804]---> BDD-cost:   10
c ---[ 803]---> BDD-cost:   10
c ---[ 802]---> BDD-cost:   10
c ---[ 801]---> BDD-cost:   10
c ---[ 800]---> BDD-cost:   10
c ---[ 799]---> BDD-cost:   10
c ---[ 798]---> BDD-cost:   10
c ---[ 797]---> BDD-cost:   10
c ---[ 796]---> BDD-cost:   10
c ---[ 795]---> BDD-cost:   10
c ---[ 794]---> BDD-cost:   10
c ---[ 793]---> BDD-cost:   10
c ---[ 792]---> BDD-cost:   10
c ---[ 791]---> BDD-cost:   10
c ---[ 790]---> BDD-cost:   10
c ---[ 789]---> BDD-cost:   10
c ---[ 788]---> BDD-cost:   10
c ---[ 787]---> BDD-cost:   10
c ---[ 786]---> BDD-cost:   10
c ---[ 785]---> BDD-cost:   10
c ---[ 784]---> BDD-cost:   10
c ---[ 783]---> BDD-cost:   10
c ---[ 782]---> BDD-cost:   10
c ---[ 781]---> BDD-cost:   10
c ---[ 780]---> BDD-cost:   10
c ---[ 779]---> BDD-cost:   10
c ---[ 778]---> BDD-cost:   10
c ---[ 777]---> BDD-cost:   10
c ---[ 776]---> BDD-cost:   10
c ---[ 775]---> BDD-cost:   10
c ---[ 774]---> BDD-cost:   10
c ---[ 773]---> BDD-cost:   10
c ---[ 772]---> BDD-cost:   10
c ---[ 771]---> BDD-cost:   10
c ---[ 770]---> BDD-cost:   10
c ---[ 769]---> BDD-cost:   10
c ---[ 768]---> BDD-cost:   10
c ---[ 767]---> BDD-cost:   10
c ---[ 766]---> BDD-cost:   10
c ---[ 765]---> BDD-cost:   10
c ---[ 764]---> BDD-cost:   10
c ---[ 763]---> BDD-cost:   10
c ---[ 762]---> BDD-cost:   10
c ---[ 761]---> BDD-cost:   10
c ---[ 760]---> BDD-cost:   10
c ---[ 759]---> BDD-cost:   10
c ---[ 758]---> BDD-cost:   10
c ---[ 757]---> BDD-cost:   10
c ---[ 756]---> BDD-cost:   10
c ---[ 755]---> BDD-cost:   10
c ---[ 754]---> BDD-cost:   10
c ---[ 753]---> BDD-cost:   10
c ---[ 752]---> BDD-cost:   10
c ---[ 751]---> BDD-cost:   10
c ---[ 750]---> BDD-cost:   10
c ---[ 749]---> BDD-cost:   10
c ---[ 748]---> BDD-cost:   10
c ---[ 747]---> BDD-cost:   10
c ---[ 746]---> BDD-cost:   10
c ---[ 745]---> BDD-cost:   10
c ---[ 744]---> BDD-cost:   10
c ---[ 743]---> BDD-cost:   10
c ---[ 742]---> BDD-cost:   10
c ---[ 741]---> BDD-cost:   10
c ---[ 740]---> BDD-cost:   10
c ---[ 739]---> BDD-cost:   10
c ---[ 738]---> BDD-cost:   10
c ---[ 737]---> BDD-cost:   10
c ---[ 736]---> BDD-cost:   10
c ---[ 735]---> BDD-cost:   10
c ---[ 734]---> BDD-cost:   10
c ---[ 733]---> BDD-cost:   10
c ---[ 732]---> BDD-cost:   10
c ---[ 731]---> BDD-cost:   10
c ---[ 730]---> BDD-cost:   10
c ---[ 729]---> BDD-cost:   10
c ---[ 728]---> BDD-cost:   10
c ---[ 727]---> BDD-cost:   10
c ---[ 726]---> BDD-cost:   10
c ---[ 725]---> BDD-cost:   10
c ---[ 724]---> BDD-cost:   10
c ---[ 723]---> BDD-cost:   10
c ---[ 722]---> BDD-cost:   10
c ---[ 721]---> BDD-cost:   10
c ---[ 720]---> BDD-cost:   10
c ---[ 719]---> BDD-cost:   10
c ---[ 718]---> BDD-cost:   10
c ---[ 717]---> BDD-cost:   10
c ---[ 716]---> BDD-cost:   10
c ---[ 715]---> BDD-cost:   10
c ---[ 714]---> BDD-cost:   10
c ---[ 713]---> BDD-cost:   10
c ---[ 712]---> BDD-cost:   10
c ---[ 711]---> BDD-cost:   10
c ---[ 710]---> BDD-cost:   10
c ---[ 709]---> BDD-cost:   10
c ---[ 708]---> BDD-cost:   10
c ---[ 707]---> BDD-cost:   10
c ---[ 706]---> BDD-cost:   10
c ---[ 705]---> BDD-cost:   10
c ---[ 704]---> BDD-cost:   10
c ---[ 703]---> BDD-cost:   10
c ---[ 702]---> BDD-cost:   10
c ---[ 701]---> BDD-cost:   10
c ---[ 700]---> BDD-cost:   10
c ---[ 699]---> BDD-cost:   10
c ---[ 698]---> BDD-cost:   10
c ---[ 697]---> BDD-cost:   10
c ---[ 696]---> BDD-cost:   10
c ---[ 695]---> BDD-cost:   10
c ---[ 694]---> BDD-cost:   10
c ---[ 693]---> BDD-cost:   10
c ---[ 692]---> BDD-cost:   10
c ---[ 691]---> BDD-cost:   10
c ---[ 690]---> BDD-cost:   10
c ---[ 689]---> BDD-cost:   10
c ---[ 688]---> BDD-cost:   10
c ---[ 687]---> BDD-cost:   10
c ---[ 686]---> BDD-cost:   10
c ---[ 685]---> BDD-cost:   10
c ---[ 684]---> BDD-cost:   10
c ---[ 683]---> BDD-cost:   10
c ---[ 682]---> BDD-cost:   10
c ---[ 681]---> BDD-cost:   10
c ---[ 680]---> BDD-cost:   10
c ---[ 679]---> BDD-cost:   10
c ---[ 678]---> BDD-cost:   10
c ---[ 677]---> BDD-cost:   10
c ---[ 676]---> BDD-cost:   10
c ---[ 675]---> BDD-cost:   10
c ---[ 674]---> BDD-cost:   10
c ---[ 673]---> BDD-cost:   10
c ---[ 672]---> BDD-cost:   10
c ---[ 671]---> BDD-cost:   10
c ---[ 670]---> BDD-cost:   10
c ---[ 669]---> BDD-cost:   10
c ---[ 668]---> BDD-cost:   10
c ---[ 667]---> BDD-cost:   10
c ---[ 666]---> BDD-cost:   10
c ---[ 665]---> BDD-cost:   10
c ---[ 664]---> BDD-cost:   10
c ---[ 663]---> BDD-cost:   10
c ---[ 662]---> BDD-cost:   10
c ---[ 661]---> BDD-cost:   10
c ---[ 660]---> BDD-cost:   10
c ---[ 659]---> BDD-cost:   10
c ---[ 658]---> BDD-cost:   10
c ---[ 657]---> BDD-cost:   10
c ---[ 656]---> BDD-cost:   10
c ---[ 655]---> BDD-cost:   10
c ---[ 654]---> BDD-cost:   10
c ---[ 653]---> BDD-cost:   10
c ---[ 652]---> BDD-cost:   10
c ---[ 651]---> BDD-cost:   10
c ---[ 650]---> BDD-cost:   10
c ---[ 649]---> BDD-cost:   10
c ---[ 648]---> BDD-cost:   10
c ---[ 647]---> BDD-cost:   10
c ---[ 646]---> BDD-cost:   10
c ---[ 645]---> BDD-cost:   10
c ---[ 644]---> BDD-cost:   10
c ---[ 643]---> BDD-cost:   10
c ---[ 642]---> BDD-cost:   10
c ---[ 641]---> BDD-cost:   10
c ---[ 640]---> BDD-cost:   10
c ---[ 639]---> BDD-cost:   10
c ---[ 638]---> BDD-cost:   10
c ---[ 637]---> BDD-cost:   10
c ---[ 636]---> BDD-cost:   10
c ---[ 635]---> BDD-cost:   10
c ---[ 634]---> BDD-cost:   10
c ---[ 633]---> BDD-cost:   10
c ---[ 632]---> BDD-cost:   10
c ---[ 631]---> BDD-cost:   10
c ---[ 630]---> BDD-cost:   10
c ---[ 629]---> BDD-cost:   10
c ---[ 628]---> BDD-cost:   10
c ---[ 627]---> BDD-cost:   10
c ---[ 626]---> BDD-cost:   10
c ---[ 625]---> BDD-cost:   10
c ---[ 624]---> BDD-cost:   10
c ---[ 623]---> BDD-cost:   10
c ---[ 622]---> BDD-cost:   10
c ---[ 621]---> BDD-cost:   10
c ---[ 620]---> BDD-cost:   10
c ---[ 619]---> BDD-cost:   10
c ---[ 618]---> BDD-cost:   10
c ---[ 617]---> BDD-cost:   10
c ---[ 616]---> BDD-cost:   10
c ---[ 615]---> BDD-cost:   10
c ---[ 614]---> BDD-cost:   10
c ---[ 613]---> BDD-cost:   10
c ---[ 612]---> BDD-cost:   10
c ---[ 611]---> BDD-cost:   10
c ---[ 610]---> BDD-cost:   10
c ---[ 609]---> BDD-cost:   10
c ---[ 608]---> BDD-cost:   10
c ---[ 607]---> BDD-cost:   10
c ---[ 606]---> BDD-cost:   10
c ---[ 605]---> BDD-cost:   10
c ---[ 604]---> BDD-cost:   10
c ---[ 603]---> BDD-cost:   10
c ---[ 602]---> BDD-cost:   10
c ---[ 601]---> BDD-cost:   10
c ---[ 600]---> BDD-cost:   10
c ---[ 599]---> BDD-cost:   10
c ---[ 598]---> BDD-cost:   10
c ---[ 597]---> BDD-cost:   10
c ---[ 596]---> BDD-cost:   10
c ---[ 595]---> BDD-cost:   10
c ---[ 594]---> BDD-cost:   10
c ---[ 593]---> BDD-cost:   10
c ---[ 592]---> BDD-cost:   10
c ---[ 591]---> BDD-cost:   10
c ---[ 590]---> BDD-cost:   10
c ---[ 589]---> BDD-cost:   10
c ---[ 588]---> BDD-cost:   10
c ---[ 587]---> BDD-cost:   10
c ---[ 586]---> BDD-cost:   10
c ---[ 585]---> BDD-cost:   10
c ---[ 584]---> BDD-cost:   10
c ---[ 583]---> BDD-cost:   10
c ---[ 582]---> BDD-cost:   10
c ---[ 581]---> BDD-cost:   10
c ---[ 580]---> BDD-cost:   10
c ---[ 579]---> BDD-cost:   10
c ---[ 578]---> BDD-cost:   10
c ---[ 577]---> BDD-cost:   10
c ---[ 576]---> BDD-cost:   10
c ---[ 575]---> BDD-cost:   10
c ---[ 574]---> BDD-cost:   10
c ---[ 573]---> BDD-cost:   10
c ---[ 572]---> BDD-cost:   10
c ---[ 571]---> BDD-cost:   10
c ---[ 570]---> BDD-cost:   10
c ---[ 569]---> BDD-cost:   10
c ---[ 568]---> BDD-cost:   10
c ---[ 567]---> BDD-cost:   10
c ---[ 566]---> BDD-cost:   10
c ---[ 565]---> BDD-cost:   10
c ---[ 564]---> BDD-cost:   10
c ---[ 563]---> BDD-cost:   10
c ---[ 562]---> BDD-cost:   10
c ---[ 561]---> BDD-cost:   10
c ---[ 560]---> BDD-cost:   10
c ---[ 559]---> BDD-cost:   10
c ---[ 558]---> BDD-cost:   10
c ---[ 557]---> BDD-cost:   10
c ---[ 556]---> BDD-cost:   10
c ---[ 555]---> BDD-cost:   10
c ---[ 554]---> BDD-cost:   10
c ---[ 553]---> BDD-cost:   10
c ---[ 552]---> BDD-cost:   10
c ---[ 551]---> BDD-cost:   10
c ---[ 550]---> BDD-cost:   10
c ---[ 549]---> BDD-cost:   10
c ---[ 548]---> BDD-cost:   10
c ---[ 547]---> BDD-cost:   10
c ---[ 546]---> BDD-cost:   10
c ---[ 545]---> BDD-cost:   10
c ---[ 544]---> BDD-cost:   10
c ---[ 543]---> BDD-cost:   10
c ---[ 542]---> BDD-cost:   10
c ---[ 541]---> BDD-cost:   10
c ---[ 540]---> BDD-cost:   10
c ---[ 539]---> BDD-cost:   10
c ---[ 538]---> BDD-cost:   10
c ---[ 537]---> BDD-cost:   10
c ---[ 536]---> BDD-cost:   10
c ---[ 535]---> BDD-cost:   10
c ---[ 534]---> BDD-cost:   10
c ---[ 533]---> BDD-cost:   10
c ---[ 532]---> BDD-cost:   10
c ---[ 531]---> BDD-cost:   10
c ---[ 530]---> BDD-cost:   10
c ---[ 529]---> BDD-cost:   10
c ---[ 528]---> BDD-cost:   10
c ---[ 527]---> BDD-cost:   10
c ---[ 526]---> BDD-cost:   10
c ---[ 525]---> BDD-cost:   10
c ---[ 524]---> BDD-cost:   10
c ---[ 523]---> BDD-cost:   10
c ---[ 522]---> BDD-cost:   10
c ---[ 521]---> BDD-cost:   10
c ---[ 520]---> BDD-cost:   10
c ---[ 519]---> BDD-cost:   10
c ---[ 518]---> BDD-cost:   10
c ---[ 517]---> BDD-cost:   10
c ---[ 516]---> BDD-cost:   10
c ---[ 515]---> BDD-cost:   10
c ---[ 514]---> BDD-cost:   10
c ---[ 513]---> BDD-cost:   10
c ---[ 512]---> BDD-cost:   10
c ---[ 511]---> BDD-cost:   10
c ---[ 510]---> BDD-cost:   10
c ---[ 509]---> BDD-cost:   10
c ---[ 508]---> BDD-cost:   10
c ---[ 507]---> BDD-cost:   10
c ---[ 506]---> BDD-cost:   10
c ---[ 505]---> BDD-cost:   10
c ---[ 504]---> BDD-cost:   10
c ---[ 503]---> BDD-cost:   10
c ---[ 502]---> BDD-cost:   10
c ---[ 501]---> BDD-cost:   10
c ---[ 500]---> BDD-cost:   10
c ---[ 499]---> BDD-cost:   10
c ---[ 498]---> BDD-cost:   10
c ---[ 497]---> BDD-cost:   10
c ---[ 496]---> BDD-cost:   10
c ---[ 495]---> BDD-cost:   10
c ---[ 494]---> BDD-cost:   10
c ---[ 493]---> BDD-cost:   10
c ---[ 492]---> BDD-cost:   10
c ---[ 491]---> BDD-cost:   10
c ---[ 490]---> BDD-cost:   10
c ---[ 489]---> BDD-cost:   10
c ---[ 488]---> BDD-cost:   10
c ---[ 487]---> BDD-cost:   10
c ---[ 486]---> BDD-cost:   10
c ---[ 485]---> BDD-cost:   10
c ---[ 484]---> BDD-cost:   10
c ---[ 483]---> BDD-cost:   10
c ---[ 482]---> BDD-cost:   10
c ---[ 481]---> BDD-cost:   10
c ---[ 480]---> BDD-cost:   10
c ---[ 479]---> BDD-cost:   10
c ---[ 478]---> BDD-cost:   10
c ---[ 477]---> BDD-cost:   10
c ---[ 476]---> BDD-cost:   10
c ---[ 475]---> BDD-cost:   10
c ---[ 474]---> BDD-cost:   10
c ---[ 473]---> BDD-cost:   10
c ---[ 472]---> BDD-cost:   10
c ---[ 471]---> BDD-cost:   10
c ---[ 470]---> BDD-cost:   10
c ---[ 469]---> BDD-cost:   10
c ---[ 468]---> BDD-cost:   10
c ---[ 467]---> BDD-cost:   10
c ---[ 466]---> BDD-cost:   10
c ---[ 465]---> BDD-cost:   10
c ---[ 464]---> BDD-cost:   10
c ---[ 463]---> BDD-cost:   10
c ---[ 462]---> BDD-cost:   10
c ---[ 461]---> BDD-cost:   10
c ---[ 460]---> BDD-cost:   10
c ---[ 459]---> BDD-cost:   10
c ---[ 458]---> BDD-cost:   10
c ---[ 457]---> BDD-cost:   10
c ---[ 456]---> BDD-cost:   10
c ---[ 455]---> BDD-cost:   10
c ---[ 454]---> BDD-cost:   10
c ---[ 453]---> BDD-cost:   10
c ---[ 452]---> BDD-cost:   10
c ---[ 451]---> BDD-cost:   10
c ---[ 450]---> BDD-cost:   10
c ---[ 449]---> BDD-cost:   10
c ---[ 448]---> BDD-cost:   10
c ---[ 447]---> BDD-cost:   10
c ---[ 446]---> BDD-cost:   10
c ---[ 445]---> BDD-cost:   10
c ---[ 444]---> BDD-cost:   10
c ---[ 443]---> BDD-cost:   10
c ---[ 442]---> BDD-cost:   10
c ---[ 441]---> BDD-cost:   10
c ---[ 440]---> BDD-cost:   10
c ---[ 439]---> BDD-cost:   10
c ---[ 438]---> BDD-cost:   10
c ---[ 437]---> BDD-cost:   10
c ---[ 436]---> BDD-cost:   10
c ---[ 435]---> BDD-cost:   10
c ---[ 434]---> BDD-cost:   10
c ---[ 433]---> BDD-cost:   10
c ---[ 432]---> BDD-cost:   10
c ---[ 431]---> BDD-cost:   10
c ---[ 430]---> BDD-cost:   10
c ---[ 429]---> BDD-cost:   10
c ---[ 428]---> BDD-cost:   10
c ---[ 427]---> BDD-cost:   10
c ---[ 426]---> BDD-cost:   10
c ---[ 425]---> BDD-cost:   10
c ---[ 424]---> BDD-cost:   10
c ---[ 423]---> BDD-cost:   10
c ---[ 422]---> BDD-cost:   10
c ---[ 421]---> BDD-cost:   10
c ---[ 420]---> BDD-cost:   10
c ---[ 419]---> BDD-cost:   10
c ---[ 418]---> BDD-cost:   10
c ---[ 417]---> BDD-cost:   10
c ---[ 416]---> BDD-cost:   10
c ---[ 415]---> BDD-cost:   10
c ---[ 414]---> BDD-cost:   10
c ---[ 413]---> BDD-cost:   10
c ---[ 412]---> BDD-cost:   10
c ---[ 411]---> BDD-cost:   10
c ---[ 410]---> BDD-cost:   10
c ---[ 409]---> BDD-cost:   10
c ---[ 408]---> BDD-cost:   10
c ---[ 407]---> BDD-cost:   10
c ---[ 406]---> BDD-cost:   10
c ---[ 405]---> BDD-cost:   10
c ---[ 404]---> BDD-cost:   10
c ---[ 403]---> BDD-cost:   10
c ---[ 402]---> BDD-cost:   10
c ---[ 401]---> BDD-cost:   10
c ---[ 400]---> BDD-cost:   10
c ---[ 399]---> BDD-cost:   10
c ---[ 398]---> BDD-cost:   10
c ---[ 397]---> BDD-cost:   10
c ---[ 396]---> BDD-cost:   10
c ---[ 395]---> BDD-cost:   10
c ---[ 394]---> BDD-cost:   10
c ---[ 393]---> BDD-cost:   10
c ---[ 392]---> BDD-cost:   10
c ---[ 391]---> BDD-cost:   10
c ---[ 390]---> BDD-cost:   10
c ---[ 389]---> BDD-cost:   10
c ---[ 388]---> BDD-cost:   10
c ---[ 387]---> BDD-cost:   10
c ---[ 386]---> BDD-cost:   10
c ---[ 385]---> BDD-cost:   10
c ---[ 384]---> BDD-cost:   10
c ---[ 383]---> BDD-cost:   10
c ---[ 382]---> BDD-cost:   10
c ---[ 381]---> BDD-cost:   10
c ---[ 380]---> BDD-cost:   10
c ---[ 379]---> BDD-cost:   10
c ---[ 378]---> BDD-cost:   10
c ---[ 377]---> BDD-cost:   10
c ---[ 376]---> BDD-cost:   10
c ---[ 375]---> BDD-cost:   10
c ---[ 374]---> BDD-cost:   10
c ---[ 373]---> BDD-cost:   10
c ---[ 372]---> BDD-cost:   10
c ---[ 371]---> BDD-cost:   10
c ---[ 370]---> BDD-cost:   10
c ---[ 369]---> BDD-cost:   10
c ---[ 368]---> BDD-cost:   10
c ---[ 367]---> BDD-cost:   10
c ---[ 366]---> BDD-cost:   10
c ---[ 365]---> BDD-cost:   10
c ---[ 364]---> BDD-cost:   10
c ---[ 363]---> BDD-cost:   10
c ---[ 362]---> BDD-cost:   10
c ---[ 361]---> BDD-cost:   10
c ---[ 360]---> BDD-cost:   10
c ---[ 359]---> BDD-cost:   10
c ---[ 358]---> BDD-cost:   10
c ---[ 357]---> BDD-cost:   10
c ---[ 356]---> BDD-cost:   10
c ---[ 355]---> BDD-cost:   10
c ---[ 354]---> BDD-cost:   10
c ---[ 353]---> BDD-cost:   10
c ---[ 352]---> BDD-cost:   10
c ---[ 351]---> BDD-cost:   10
c ---[ 350]---> BDD-cost:   10
c ---[ 349]---> BDD-cost:   10
c ---[ 348]---> BDD-cost:   10
c ---[ 347]---> BDD-cost:   10
c ---[ 346]---> BDD-cost:   10
c ---[ 345]---> BDD-cost:   10
c ---[ 344]---> BDD-cost:   10
c ---[ 343]---> BDD-cost:   10
c ---[ 342]---> BDD-cost:   10
c ---[ 341]---> BDD-cost:   10
c ---[ 340]---> BDD-cost:   10
c ---[ 339]---> BDD-cost:   10
c ---[ 338]---> BDD-cost:   10
c ---[ 337]---> BDD-cost:   10
c ---[ 336]---> BDD-cost:   10
c ---[ 335]---> BDD-cost:   10
c ---[ 334]---> BDD-cost:   10
c ---[ 333]---> BDD-cost:   10
c ---[ 332]---> BDD-cost:   10
c ---[ 331]---> BDD-cost:   10
c ---[ 330]---> BDD-cost:   10
c ---[ 329]---> BDD-cost:   10
c ---[ 328]---> BDD-cost:   10
c ---[ 327]---> BDD-cost:   10
c ---[ 326]---> BDD-cost:   10
c ---[ 325]---> BDD-cost:   10
c ---[ 324]---> BDD-cost:   10
c ---[ 323]---> BDD-cost:   10
c ---[ 322]---> BDD-cost:   10
c ---[ 321]---> BDD-cost:   10
c ---[ 320]---> BDD-cost:   10
c ---[ 319]---> BDD-cost:   10
c ---[ 318]---> BDD-cost:   10
c ---[ 317]---> BDD-cost:   10
c ---[ 316]---> BDD-cost:   10
c ---[ 315]---> BDD-cost:   10
c ---[ 314]---> BDD-cost:   10
c ---[ 313]---> BDD-cost:   10
c ---[ 312]---> BDD-cost:   10
c ---[ 311]---> BDD-cost:   10
c ---[ 310]---> BDD-cost:   10
c ---[ 309]---> BDD-cost:   10
c ---[ 308]---> BDD-cost:   10
c ---[ 307]---> BDD-cost:   10
c ---[ 306]---> BDD-cost:   10
c ---[ 305]---> BDD-cost:   10
c ---[ 304]---> BDD-cost:   10
c ---[ 303]---> BDD-cost:   10
c ---[ 302]---> BDD-cost:   10
c ---[ 301]---> BDD-cost:   10
c ---[ 300]---> BDD-cost:   10
c ---[ 299]---> BDD-cost:   10
c ---[ 298]---> BDD-cost:   10
c ---[ 297]---> BDD-cost:   10
c ---[ 296]---> BDD-cost:   10
c ---[ 295]---> BDD-cost:   10
c ---[ 294]---> BDD-cost:   10
c ---[ 293]---> BDD-cost:   10
c ---[ 292]---> BDD-cost:   10
c ---[ 291]---> BDD-cost:   10
c ---[ 290]---> BDD-cost:   10
c ---[ 289]---> BDD-cost:   10
c ---[ 288]---> BDD-cost:   10
c ---[ 287]---> BDD-cost:   10
c ---[ 286]---> BDD-cost:   10
c ---[ 285]---> BDD-cost:   10
c ---[ 284]---> BDD-cost:   10
c ---[ 283]---> BDD-cost:   10
c ---[ 282]---> BDD-cost:   10
c ---[ 281]---> BDD-cost:   10
c ---[ 280]---> BDD-cost:   10
c ---[ 279]---> BDD-cost:   10
c ---[ 278]---> BDD-cost:   10
c ---[ 277]---> BDD-cost:   10
c ---[ 276]---> BDD-cost:   10
c ---[ 275]---> BDD-cost:   10
c ---[ 274]---> BDD-cost:   10
c ---[ 273]---> BDD-cost:   10
c ---[ 272]---> BDD-cost:   10
c ---[ 271]---> BDD-cost:   10
c ---[ 270]---> BDD-cost:   10
c ---[ 269]---> BDD-cost:   10
c ---[ 268]---> BDD-cost:   10
c ---[ 267]---> BDD-cost:   10
c ---[ 266]---> BDD-cost:   10
c ---[ 265]---> BDD-cost:   10
c ---[ 264]---> BDD-cost:   10
c ---[ 263]---> BDD-cost:   10
c ---[ 262]---> BDD-cost:   10
c ---[ 261]---> BDD-cost:   10
c ---[ 260]---> BDD-cost:   10
c ---[ 259]---> BDD-cost:   10
c ---[ 258]---> BDD-cost:   10
c ---[ 257]---> BDD-cost:   10
c ---[ 256]---> BDD-cost:   10
c ---[ 255]---> BDD-cost:   10
c ---[ 254]---> BDD-cost:   10
c ---[ 253]---> BDD-cost:   10
c ---[ 252]---> BDD-cost:   11
c ---[ 251]---> BDD-cost:   11
c ---[ 250]---> BDD-cost:   11
c ---[ 249]---> BDD-cost:   11
c ---[ 248]---> BDD-cost:   11
c ---[ 247]---> BDD-cost:   11
c ---[ 246]---> BDD-cost:   11
c ---[ 245]---> BDD-cost:   11
c ---[ 244]---> BDD-cost:   11
c ---[ 243]---> BDD-cost:   11
c ---[ 242]---> BDD-cost:   11
c ---[ 241]---> BDD-cost:   11
c ---[ 240]---> BDD-cost:   11
c ---[ 239]---> BDD-cost:   11
c ---[ 238]---> BDD-cost:   11
c ---[ 237]---> BDD-cost:   11
c ---[ 236]---> BDD-cost:   11
c ---[ 235]---> BDD-cost:   11
c ---[ 234]---> BDD-cost:   11
c ---[ 233]---> BDD-cost:   11
c ---[ 232]---> BDD-cost:   11
c ---[ 231]---> BDD-cost:   11
c ---[ 230]---> BDD-cost:   11
c ---[ 229]---> BDD-cost:   11
c ---[ 228]---> BDD-cost:   11
c ---[ 227]---> BDD-cost:   11
c ---[ 226]---> BDD-cost:   11
c ---[ 225]---> BDD-cost:   11
c ---[ 224]---> BDD-cost:   11
c ---[ 223]---> BDD-cost:   11
c ---[ 222]---> BDD-cost:   11
c ---[ 221]---> BDD-cost:   11
c ---[ 220]---> BDD-cost:   11
c ---[ 219]---> BDD-cost:   11
c ---[ 218]---> BDD-cost:   11
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   11
c ---[ 215]---> BDD-cost:   11
c ---[ 214]---> BDD-cost:   11
c ---[ 213]---> BDD-cost:   11
c ---[ 212]---> BDD-cost:   11
c ---[ 211]---> BDD-cost:   11
c ---[ 210]---> BDD-cost:   11
c ---[ 209]---> BDD-cost:   11
c ---[ 208]---> BDD-cost:   11
c ---[ 207]---> BDD-cost:   11
c ---[ 206]---> BDD-cost:   11
c ---[ 205]---> BDD-cost:   11
c ---[ 204]---> BDD-cost:   11
c ---[ 203]---> BDD-cost:   11
c ---[ 202]---> BDD-cost:   11
c ---[ 201]---> BDD-cost:   11
c ---[ 200]---> BDD-cost:   11
c ---[ 199]---> BDD-cost:   11
c ---[ 198]---> BDD-cost:   11
c ---[ 197]---> BDD-cost:   11
c ---[ 196]---> BDD-cost:   11
c ---[ 195]---> BDD-cost:   11
c ---[ 194]---> BDD-cost:   11
c ---[ 193]---> BDD-cost:   11
c ---[ 192]---> BDD-cost:   11
c ---[ 191]---> BDD-cost:   11
c ---[ 190]---> BDD-cost:   11
c ---[ 189]---> BDD-cost:   11
c ---[ 188]---> BDD-cost:   11
c ---[ 187]---> BDD-cost:   11
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   11
c ---[ 184]---> BDD-cost:   11
c ---[ 183]---> BDD-cost:   11
c ---[ 182]---> BDD-cost:   11
c ---[ 181]---> BDD-cost:   11
c ---[ 180]---> BDD-cost:   11
c ---[ 179]---> BDD-cost:   11
c ---[ 178]---> BDD-cost:   11
c ---[ 177]---> BDD-cost:   11
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:   11
c ---[ 173]---> BDD-cost:   11
c ---[ 172]---> BDD-cost:   11
c ---[ 171]---> BDD-cost:   11
c ---[ 170]---> BDD-cost:   11
c ---[ 169]---> BDD-cost:   11
c ---[ 168]---> BDD-cost:   11
c ---[ 167]---> BDD-cost:   11
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   11
c ---[ 164]---> BDD-cost:   11
c ---[ 163]---> BDD-cost:   11
c ---[ 162]---> BDD-cost:   11
c ---[ 161]---> BDD-cost:   11
c ---[ 160]---> BDD-cost:   11
c ---[ 159]---> BDD-cost:   11
c ---[ 158]---> BDD-cost:   11
c ---[ 157]---> BDD-cost:   11
c ---[ 156]---> BDD-cost:   11
c ---[ 155]---> BDD-cost:   11
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:   11
c ---[ 152]---> BDD-cost:   11
c ---[ 151]---> BDD-cost:   11
c ---[ 150]---> BDD-cost:   11
c ---[ 149]---> BDD-cost:   11
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:   11
c ---[ 146]---> BDD-cost:   11
c ---[ 145]---> BDD-cost:   11
c ---[ 144]---> BDD-cost:   11
c ---[ 143]---> BDD-cost:   11
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   11
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:   11
c ---[ 138]---> BDD-cost:   11
c ---[ 137]---> BDD-cost:   11
c ---[ 136]---> BDD-cost:   11
c ---[ 135]---> BDD-cost:   11
c ---[ 134]---> BDD-cost:   11
c ---[ 133]---> BDD-cost:   11
c ---[ 132]---> BDD-cost:   11
c ---[ 131]---> BDD-cost:   11
c ---[ 130]---> BDD-cost:   11
c ---[ 129]---> BDD-cost:   11
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   11
c ---[ 126]---> BDD-cost:   11
c ---[ 125]---> BDD-cost:   11
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   11
c ---[ 122]---> BDD-cost:   11
c ---[ 121]---> BDD-cost:   11
c ---[ 120]---> BDD-cost:   11
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:   11
c ---[ 117]---> BDD-cost:   11
c ---[ 116]---> BDD-cost:   11
c ---[ 115]---> BDD-cost:   11
c ---[ 114]---> BDD-cost:   11
c ---[ 113]---> BDD-cost:   11
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   11
c ---[ 110]---> BDD-cost:   11
c ---[ 109]---> BDD-cost:   11
c ---[ 108]---> BDD-cost:   11
c ---[ 107]---> BDD-cost:   11
c ---[ 106]---> BDD-cost:   11
c ---[ 105]---> BDD-cost:   11
c ---[ 104]---> BDD-cost:   11
c ---[ 103]---> BDD-cost:   11
c ---[ 102]---> BDD-cost:   11
c ---[ 101]---> BDD-cost:   11
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   11
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   11
c ---[  96]---> BDD-cost:   11
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   11
c ---[  89]---> BDD-cost:   11
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   11
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   11
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:   11
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   11
c ---[  73]---> BDD-cost:   11
c ---[  72]---> BDD-cost:   11
c ---[  71]---> BDD-cost:   11
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   11
c ---[  67]---> BDD-cost:   11
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   11
c ---[  64]---> BDD-cost:   11
c ---[  63]---> BDD-cost:   11
c ---[  62]---> BDD-cost:   11
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:   11
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   11
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:   11
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   11
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   11
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   11
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   11
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   11
c ---[  29]---> BDD-cost:   11
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   11
c ---[  23]---> Adder-cost: 22993   maxlim: 816753   bits: 21/20
c ---[  22]---> Adder-cost: 48143   maxlim: 53250657   bits: 27/26
c ---[  21]---> Adder-cost: 24490   maxlim: 37410971   bits: 27/26
c ---[  20]---> Adder-cost: 18532   maxlim: 62407570   bits: 27/26
c ---[  19]---> Adder-cost: 64462   maxlim: 396293572   bits: 30/29
c ---[  18]---> Adder-cost: 9918   maxlim: 1625605   bits: 21/21
c ---[  17]---> Adder-cost: 39824   maxlim: 26785026   bits: 26/25
c ---[  16]---> Adder-cost: 60627   maxlim: 27028587   bits: 26/25
c ---[  15]---> Adder-cost: 50627   maxlim: 58642455   bits: 27/26
c ---[  14]---> Adder-cost: 19026   maxlim: 1373536   bits: 22/21
c ---[  13]---> Adder-cost: 25006   maxlim: 4696498   bits: 23/23
c ---[  12]---> Adder-cost: 69126   maxlim: 389685799   bits: 30/29
c ---[  11]---> Adder-cost: 2804   maxlim: 712518   bits: 20/20
c ---[  10]---> Adder-cost: 11416   maxlim: 36659016   bits: 26/26
c ---[   9]---> Adder-cost: 39511   maxlim: 31990515   bits: 26/25
c ---[   8]---> Adder-cost: 5682   maxlim: 513869   bits: 20/19
c ---[   7]---> Adder-cost: 5867   maxlim: 245639   bits: 19/18
c ---[   6]---> Adder-cost: 6404   maxlim: 282485   bits: 20/19
c ---[   5]---> Adder-cost: 11426   maxlim: 540407   bits: 21/20
c ---[   4]---> Adder-cost: 5814   maxlim: 585536   bits: 20/20
c ---[   3]---> Adder-cost: 4529   maxlim: 200605   bits: 19/18
c ---[   2]---> Adder-cost: 2945   maxlim: 126913   bits: 18/17
c ---[   1]---> Adder-cost: 7696   maxlim: 753405   bits: 21/20
c ---[   0]---> Adder-cost: 5242   maxlim: 276344   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 3943420 14068188 | 1314473       0        0     nan |  0.000 % |
c |       100 | 3943420 14068188 | 1445920     100      323     3.2 |  0.236 % |
c |       250 | 3943420 14068188 | 1590512     250      816     3.3 |  0.236 % |
c |       475 | 3943420 14068188 | 1749563     475     1545     3.3 |  0.236 % |
c |       812 | 3943420 14068188 | 1924519     812     2651     3.3 |  0.236 % |
c |      1319 | 3943420 14068188 | 2116971    1319     4341     3.3 |  0.236 % |
c |      2078 | 3943414 14068171 | 2328669    2076     6982     3.4 |  0.236 % |
c |      3217 | 3943414 14068171 | 2561536    3215    11255     3.5 |  0.236 % |
c |      4925 | 3943414 14068171 | 2817689    4923    18542     3.8 |  0.236 % |
c |      7487 | 3943414 14068171 | 3099458    7485    29742     4.0 |  0.236 % |
c |     11331 | 3943414 14068171 | 3409404   11329    44956     4.0 |  0.236 % |
c |     17097 | 3943398 14068119 | 3750344   17093    82578     4.8 |  0.237 % |
c |     25746 | 3943398 14068119 | 4125379   25742   122605     4.8 |  0.237 % |
c |     38720 | 3943398 14068119 | 4537917   38716   326863     8.4 |  0.237 % |
c |     58181 | 3943398 14068119 | 4991709   58177   443965     7.6 |  0.237 % |
c |     87373 | 3943398 14068119 | 5490879   87369   747339     8.6 |  0.237 % |
c |    131162 | 3943398 14068119 | 6039967  131158  1836070    14.0 |  0.237 % |
#### 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.72 0.96 0.95 2/54 17389
Raw data (stat): 17389 (runsolver) R 17388 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550718682 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.77 0.96 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 11880 0 0 0 968 30 0 0 25 0 1 0 550718682 43876352 8238 4294967295 134512640 134672761 3221224624 3221221608 1075349622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10712 8238 603 41 0 10671 0
vsize: 42848
[startup+20.0027 s]
Raw data (loadavg): 0.80 0.96 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 13513 0 0 0 1964 34 0 0 25 0 1 0 550718682 43900928 8292 4294967295 134512640 134672761 3221224624 3221222464 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10718 8292 603 41 0 10677 0
vsize: 42872
[startup+30.0026 s]
Raw data (loadavg): 0.83 0.96 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 13513 0 0 0 2964 35 0 0 25 0 1 0 550718682 43900928 8292 4294967295 134512640 134672761 3221224624 3221222896 134597008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10718 8292 603 41 0 10677 0
vsize: 42872
[startup+40.0027 s]
Raw data (loadavg): 0.86 0.96 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 13513 0 0 0 3964 35 0 0 25 0 1 0 550718682 43900928 8292 4294967295 134512640 134672761 3221224624 3221222728 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10718 8292 603 41 0 10677 0
vsize: 42872
[startup+50.0034 s]
Raw data (loadavg): 0.88 0.96 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 21199 0 0 0 4946 53 0 0 25 0 1 0 550718682 72740864 13782 4294967295 134512640 134672761 3221224624 3221223184 134597008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17759 13782 603 41 0 17718 0
vsize: 71036
[startup+60.0029 s]
Raw data (loadavg): 0.90 0.96 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 21943 0 0 0 5944 55 0 0 25 0 1 0 550718682 72740864 13782 4294967295 134512640 134672761 3221224624 3221223808 134593641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17759 13782 603 41 0 17718 0
vsize: 71036
[startup+70.004 s]
Raw data (loadavg): 0.91 0.96 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 22537 0 0 0 6942 57 0 0 25 0 1 0 550718682 72740864 13782 4294967295 134512640 134672761 3221224624 3221223008 134522369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17759 13782 603 41 0 17718 0
vsize: 71036
[startup+80.0047 s]
Raw data (loadavg): 0.92 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 24437 0 0 0 7939 60 0 0 25 0 1 0 550718682 75689984 14937 4294967295 134512640 134672761 3221224624 3221222340 134544789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18479 14937 603 41 0 18438 0
vsize: 73916
[startup+90.0039 s]
Raw data (loadavg): 0.94 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 54718 0 0 0 8870 130 0 0 25 0 1 0 550718682 218705920 44685 4294967295 134512640 134672761 3221224624 3221214464 134556287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53395 44685 603 41 0 53354 0
vsize: 213580
[startup+100.005 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 79519 0 0 0 9808 191 0 0 25 0 1 0 550718682 332496896 69486 4294967295 134512640 134672761 3221224624 3221223832 134561962 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81176 69486 603 41 0 81135 0
vsize: 324704
[startup+110.006 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 80000 0 0 0 10807 193 0 0 25 0 1 0 550718682 334524416 69967 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81671 69967 603 41 0 81630 0
vsize: 326684
[startup+120.007 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 80385 0 0 0 11806 194 0 0 25 0 1 0 550718682 336154624 70352 4294967295 134512640 134672761 3221224624 3221223776 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82069 70352 603 41 0 82028 0
vsize: 328276
[startup+130.007 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 80739 0 0 0 12805 195 0 0 25 0 1 0 550718682 337506304 70706 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82399 70706 603 41 0 82358 0
vsize: 329596
[startup+140.007 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 81072 0 0 0 13804 196 0 0 25 0 1 0 550718682 338857984 71039 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82729 71039 603 41 0 82688 0
vsize: 330916
[startup+150.007 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 81388 0 0 0 14803 198 0 0 25 0 1 0 550718682 340226048 71355 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83063 71355 603 41 0 83022 0
vsize: 332252
[startup+160.007 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 81677 0 0 0 15801 199 0 0 25 0 1 0 550718682 341442560 71644 4294967295 134512640 134672761 3221224624 3221223748 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83360 71644 603 41 0 83319 0
vsize: 333440
[startup+170.008 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 81905 0 0 0 16801 200 0 0 25 0 1 0 550718682 342388736 71872 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83591 71872 603 41 0 83550 0
vsize: 334364
[startup+180.008 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 82120 0 0 0 17800 200 0 0 25 0 1 0 550718682 343199744 72087 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83789 72087 603 41 0 83748 0
vsize: 335156
[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 82280 0 0 0 18800 201 0 0 25 0 1 0 550718682 343875584 72247 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83954 72247 603 41 0 83913 0
vsize: 335816
[startup+200.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 82405 0 0 0 19800 202 0 0 25 0 1 0 550718682 344416256 72372 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84086 72372 603 41 0 84045 0
vsize: 336344
[startup+210.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 82539 0 0 0 20800 202 0 0 25 0 1 0 550718682 344956928 72506 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84218 72506 603 41 0 84177 0
vsize: 336872
[startup+220.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 82670 0 0 0 21799 203 0 0 25 0 1 0 550718682 345497600 72637 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84350 72637 603 41 0 84309 0
vsize: 337400
[startup+230.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 82772 0 0 0 22799 203 0 0 25 0 1 0 550718682 345903104 72739 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84449 72739 603 41 0 84408 0
vsize: 337796
[startup+240.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83089 0 0 0 23797 205 0 0 25 0 1 0 550718682 347250688 73056 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84778 73056 603 41 0 84737 0
vsize: 339112
[startup+250.068 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83180 0 0 0 24801 206 0 0 25 0 1 0 550718682 347656192 73147 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84877 73147 603 41 0 84836 0
vsize: 339508
[startup+260.087 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83255 0 0 0 25803 206 0 0 25 0 1 0 550718682 347926528 73222 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84943 73222 603 41 0 84902 0
vsize: 339772
[startup+270.097 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83338 0 0 0 26803 206 0 0 25 0 1 0 550718682 348196864 73305 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85009 73305 603 41 0 84968 0
vsize: 340036
[startup+280.097 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83403 0 0 0 27803 207 0 0 25 0 1 0 550718682 348467200 73370 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85075 73370 603 41 0 85034 0
vsize: 340300
[startup+290.098 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83477 0 0 0 28802 207 0 0 25 0 1 0 550718682 348737536 73444 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85141 73444 603 41 0 85100 0
vsize: 340564
[startup+300.098 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83534 0 0 0 29802 208 0 0 25 0 1 0 550718682 349007872 73501 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85207 73501 603 41 0 85166 0
vsize: 340828
[startup+310.099 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83590 0 0 0 30802 208 0 0 25 0 1 0 550718682 349278208 73557 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85273 73557 603 41 0 85232 0
vsize: 341092
[startup+320.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83643 0 0 0 31801 209 0 0 25 0 1 0 550718682 349413376 73610 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85306 73610 603 41 0 85265 0
vsize: 341224
[startup+330.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83696 0 0 0 32801 209 0 0 25 0 1 0 550718682 349683712 73663 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85372 73663 603 41 0 85331 0
vsize: 341488
[startup+340.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83750 0 0 0 33800 210 0 0 25 0 1 0 550718682 349818880 73717 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85405 73717 603 41 0 85364 0
vsize: 341620
[startup+350.101 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83803 0 0 0 34800 210 0 0 25 0 1 0 550718682 350089216 73770 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85471 73770 603 41 0 85430 0
vsize: 341884
[startup+360.101 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83848 0 0 0 35799 211 0 0 25 0 1 0 550718682 350224384 73815 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85504 73815 603 41 0 85463 0
vsize: 342016
[startup+370.103 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83895 0 0 0 36799 211 0 0 25 0 1 0 550718682 350359552 73862 4294967295 134512640 134672761 3221224624 3221223840 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85537 73862 603 41 0 85496 0
vsize: 342148
[startup+380.103 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83949 0 0 0 37799 211 0 0 25 0 1 0 550718682 350629888 73916 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85603 73916 603 41 0 85562 0
vsize: 342412
[startup+390.103 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 83990 0 0 0 38799 212 0 0 25 0 1 0 550718682 350765056 73957 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85636 73957 603 41 0 85595 0
vsize: 342544
[startup+400.103 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84029 0 0 0 39799 212 0 0 25 0 1 0 550718682 350900224 73996 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85669 73996 603 41 0 85628 0
vsize: 342676
[startup+410.104 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84067 0 0 0 40798 212 0 0 25 0 1 0 550718682 351035392 74034 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85702 74034 603 41 0 85661 0
vsize: 342808
[startup+420.105 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84106 0 0 0 41798 213 0 0 25 0 1 0 550718682 351305728 74073 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85768 74073 603 41 0 85727 0
vsize: 343072
[startup+430.106 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84142 0 0 0 42798 213 0 0 25 0 1 0 550718682 351440896 74109 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85801 74109 603 41 0 85760 0
vsize: 343204
[startup+440.106 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84199 0 0 0 43798 214 0 0 25 0 1 0 550718682 351576064 74166 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85834 74166 603 41 0 85793 0
vsize: 343336
[startup+450.107 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84239 0 0 0 44798 214 0 0 25 0 1 0 550718682 351711232 74206 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85867 74206 603 41 0 85826 0
vsize: 343468
[startup+460.108 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84280 0 0 0 45797 214 0 0 25 0 1 0 550718682 351981568 74247 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85933 74247 603 41 0 85892 0
vsize: 343732
[startup+470.109 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84316 0 0 0 46797 215 0 0 25 0 1 0 550718682 352116736 74283 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85966 74283 603 41 0 85925 0
vsize: 343864
[startup+480.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84354 0 0 0 47796 215 0 0 25 0 1 0 550718682 352251904 74321 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85999 74321 603 41 0 85958 0
vsize: 343996
[startup+490.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84390 0 0 0 48796 216 0 0 25 0 1 0 550718682 352387072 74357 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86032 74357 603 41 0 85991 0
vsize: 344128
[startup+500.111 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84417 0 0 0 49796 216 0 0 25 0 1 0 550718682 352522240 74384 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86065 74384 603 41 0 86024 0
vsize: 344260
[startup+510.112 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84449 0 0 0 50796 216 0 0 25 0 1 0 550718682 352657408 74416 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86098 74416 603 41 0 86057 0
vsize: 344392
[startup+520.114 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84487 0 0 0 51795 217 0 0 25 0 1 0 550718682 352792576 74454 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86131 74454 603 41 0 86090 0
vsize: 344524
[startup+530.114 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84544 0 0 0 52795 218 0 0 25 0 1 0 550718682 352927744 74511 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86164 74511 603 41 0 86123 0
vsize: 344656
[startup+540.114 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84580 0 0 0 53794 218 0 0 25 0 1 0 550718682 353062912 74547 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86197 74547 603 41 0 86156 0
vsize: 344788
[startup+550.127 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84611 0 0 0 54795 219 0 0 25 0 1 0 550718682 353198080 74578 4294967295 134512640 134672761 3221224624 3221223792 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86230 74578 603 41 0 86189 0
vsize: 344920
[startup+560.135 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84639 0 0 0 55795 219 0 0 25 0 1 0 550718682 353333248 74606 4294967295 134512640 134672761 3221224624 3221223776 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86263 74606 603 41 0 86222 0
vsize: 345052
[startup+570.135 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84668 0 0 0 56795 219 0 0 25 0 1 0 550718682 353730560 74635 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86360 74635 603 41 0 86319 0
vsize: 345440
[startup+580.136 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84696 0 0 0 57795 220 0 0 25 0 1 0 550718682 353865728 74663 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86393 74663 603 41 0 86352 0
vsize: 345572
[startup+590.136 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84718 0 0 0 58795 220 0 0 25 0 1 0 550718682 353865728 74685 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86393 74685 603 41 0 86352 0
vsize: 345572
[startup+600.136 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84754 0 0 0 59794 221 0 0 25 0 1 0 550718682 354000896 74721 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86426 74721 603 41 0 86385 0
vsize: 345704
[startup+610.138 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84778 0 0 0 60794 221 0 0 25 0 1 0 550718682 354136064 74745 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86459 74745 603 41 0 86418 0
vsize: 345836
[startup+620.138 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84803 0 0 0 61793 222 0 0 25 0 1 0 550718682 354271232 74770 4294967295 134512640 134672761 3221224624 3221223788 134564515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86492 74770 603 41 0 86451 0
vsize: 345968
[startup+630.138 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84837 0 0 0 62793 222 0 0 25 0 1 0 550718682 354406400 74804 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86525 74804 603 41 0 86484 0
vsize: 346100
[startup+640.153 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84859 0 0 0 63794 222 0 0 25 0 1 0 550718682 354406400 74826 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86525 74826 603 41 0 86484 0
vsize: 346100
[startup+650.153 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84889 0 0 0 64794 223 0 0 25 0 1 0 550718682 354541568 74856 4294967295 134512640 134672761 3221224624 3221223792 134564705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86558 74856 603 41 0 86517 0
vsize: 346232
[startup+660.154 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 84935 0 0 0 65794 223 0 0 25 0 1 0 550718682 354676736 74902 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86591 74902 603 41 0 86550 0
vsize: 346364
[startup+670.156 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85096 0 0 0 66793 224 0 0 25 0 1 0 550718682 355352576 75063 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86756 75063 603 41 0 86715 0
vsize: 347024
[startup+680.164 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85171 0 0 0 67794 224 0 0 25 0 1 0 550718682 355618816 75138 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86821 75138 603 41 0 86780 0
vsize: 347284
[startup+690.164 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85197 0 0 0 68793 225 0 0 25 0 1 0 550718682 355753984 75164 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86854 75164 603 41 0 86813 0
vsize: 347416
[startup+700.165 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85218 0 0 0 69793 226 0 0 25 0 1 0 550718682 355889152 75185 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86887 75185 603 41 0 86846 0
vsize: 347548
[startup+710.165 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85243 0 0 0 70792 226 0 0 25 0 1 0 550718682 356024320 75210 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86920 75210 603 41 0 86879 0
vsize: 347680
[startup+720.166 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85265 0 0 0 71792 227 0 0 25 0 1 0 550718682 356024320 75232 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86920 75232 603 41 0 86879 0
vsize: 347680
[startup+730.167 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85292 0 0 0 72791 227 0 0 25 0 1 0 550718682 356159488 75259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86953 75259 603 41 0 86912 0
vsize: 347812
[startup+740.167 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85312 0 0 0 73791 227 0 0 25 0 1 0 550718682 356294656 75279 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86986 75279 603 41 0 86945 0
vsize: 347944
[startup+750.168 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85333 0 0 0 74791 228 0 0 25 0 1 0 550718682 356294656 75300 4294967295 134512640 134672761 3221224624 3221223856 134557600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86986 75300 603 41 0 86945 0
vsize: 347944
[startup+760.169 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85356 0 0 0 75791 228 0 0 25 0 1 0 550718682 356429824 75323 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87019 75323 603 41 0 86978 0
vsize: 348076
[startup+770.171 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85385 0 0 0 76791 228 0 0 25 0 1 0 550718682 356564992 75352 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87052 75352 603 41 0 87011 0
vsize: 348208
[startup+780.171 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85430 0 0 0 77791 229 0 0 25 0 1 0 550718682 356700160 75397 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87085 75397 603 41 0 87044 0
vsize: 348340
[startup+790.274 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85456 0 0 0 78800 229 0 0 25 0 1 0 550718682 356835328 75423 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87118 75423 603 41 0 87077 0
vsize: 348472
[startup+800.275 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85837 0 0 0 79799 230 0 0 25 0 1 0 550718682 358309888 75804 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87478 75804 603 41 0 87437 0
vsize: 349912
[startup+810.275 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85861 0 0 0 80799 231 0 0 25 0 1 0 550718682 358445056 75828 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87511 75828 603 41 0 87470 0
vsize: 350044
[startup+820.284 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85886 0 0 0 81799 231 0 0 25 0 1 0 550718682 358580224 75853 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87544 75853 603 41 0 87503 0
vsize: 350176
[startup+830.292 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85909 0 0 0 82800 231 0 0 25 0 1 0 550718682 358580224 75876 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87544 75876 603 41 0 87503 0
vsize: 350176
[startup+840.301 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85930 0 0 0 83800 231 0 0 25 0 1 0 550718682 358715392 75897 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87577 75897 603 41 0 87536 0
vsize: 350308
[startup+850.302 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85955 0 0 0 84800 232 0 0 25 0 1 0 550718682 358850560 75922 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87610 75922 603 41 0 87569 0
vsize: 350440
[startup+860.302 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 85976 0 0 0 85800 232 0 0 25 0 1 0 550718682 358850560 75943 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87610 75943 603 41 0 87569 0
vsize: 350440
[startup+870.303 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 86000 0 0 0 86800 233 0 0 25 0 1 0 550718682 358985728 75967 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87643 75967 603 41 0 87602 0
vsize: 350572
[startup+880.303 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 86021 0 0 0 87800 233 0 0 25 0 1 0 550718682 359120896 75988 4294967295 134512640 134672761 3221224624 3221223748 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87676 75988 603 41 0 87635 0
vsize: 350704
[startup+890.303 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 86041 0 0 0 88800 233 0 0 25 0 1 0 550718682 359120896 76008 4294967295 134512640 134672761 3221224624 3221223792 134564436 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87676 76008 603 41 0 87635 0
vsize: 350704
[startup+900.304 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 86063 0 0 0 89799 234 0 0 25 0 1 0 550718682 359256064 76030 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87709 76030 603 41 0 87668 0
vsize: 350836
[startup+910.305 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 86090 0 0 0 90799 234 0 0 25 0 1 0 550718682 359391232 76057 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87742 76057 603 41 0 87701 0
vsize: 350968
[startup+920.304 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 86114 0 0 0 91799 234 0 0 25 0 1 0 550718682 359391232 76081 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87742 76081 603 41 0 87701 0
vsize: 350968
[startup+930.305 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 86136 0 0 0 92798 235 0 0 25 0 1 0 550718682 359526400 76103 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87775 76103 603 41 0 87734 0
vsize: 351100
[startup+940.305 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 86163 0 0 0 93798 235 0 0 25 0 1 0 550718682 359661568 76130 4294967295 134512640 134672761 3221224624 3221223760 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87808 76130 603 41 0 87767 0
vsize: 351232
[startup+950.305 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 86479 0 0 0 94798 236 0 0 25 0 1 0 550718682 360878080 76446 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88105 76446 603 41 0 88064 0
vsize: 352420
[startup+960.306 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87035 0 0 0 95796 237 0 0 25 0 1 0 550718682 363192320 77002 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88670 77002 603 41 0 88629 0
vsize: 354680
[startup+970.306 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87149 0 0 0 96795 238 0 0 25 0 1 0 550718682 364138496 77116 4294967295 134512640 134672761 3221224624 3221223760 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88901 77116 603 41 0 88860 0
vsize: 355604
[startup+980.306 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87174 0 0 0 97795 238 0 0 25 0 1 0 550718682 364273664 77141 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88934 77141 603 41 0 88893 0
vsize: 355736
[startup+990.306 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87199 0 0 0 98795 238 0 0 25 0 1 0 550718682 364408832 77166 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88967 77166 603 41 0 88926 0
vsize: 355868
[startup+1000.31 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87230 0 0 0 99794 239 0 0 25 0 1 0 550718682 364408832 77197 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88967 77197 603 41 0 88926 0
vsize: 355868
[startup+1010.31 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87250 0 0 0 100794 240 0 0 25 0 1 0 550718682 364544000 77217 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89000 77217 603 41 0 88959 0
vsize: 356000
[startup+1020.31 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87268 0 0 0 101794 240 0 0 25 0 1 0 550718682 364679168 77235 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89033 77235 603 41 0 88992 0
vsize: 356132
[startup+1030.31 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87292 0 0 0 102794 240 0 0 25 0 1 0 550718682 364679168 77259 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89033 77259 603 41 0 88992 0
vsize: 356132
[startup+1040.31 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87312 0 0 0 103794 240 0 0 25 0 1 0 550718682 364814336 77279 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89066 77279 603 41 0 89025 0
vsize: 356264
[startup+1050.31 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87337 0 0 0 104794 240 0 0 25 0 1 0 550718682 364814336 77304 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89066 77304 603 41 0 89025 0
vsize: 356264
[startup+1060.31 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87358 0 0 0 105794 241 0 0 25 0 1 0 550718682 364949504 77325 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89099 77325 603 41 0 89058 0
vsize: 356396
[startup+1070.31 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87378 0 0 0 106793 241 0 0 25 0 1 0 550718682 364949504 77345 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89099 77345 603 41 0 89058 0
vsize: 356396
[startup+1080.31 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87407 0 0 0 107793 242 0 0 25 0 1 0 550718682 365084672 77374 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89132 77374 603 41 0 89091 0
vsize: 356528
[startup+1090.31 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87423 0 0 0 108793 242 0 0 25 0 1 0 550718682 365084672 77390 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89132 77390 603 41 0 89091 0
vsize: 356528
[startup+1100.31 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87441 0 0 0 109793 242 0 0 25 0 1 0 550718682 365219840 77408 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89165 77408 603 41 0 89124 0
vsize: 356660
[startup+1110.31 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87538 0 0 0 110792 243 0 0 25 0 1 0 550718682 365621248 77505 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89263 77505 603 41 0 89222 0
vsize: 357052
[startup+1120.32 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87563 0 0 0 111792 244 0 0 25 0 1 0 550718682 365756416 77530 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89296 77530 603 41 0 89255 0
vsize: 357184
[startup+1130.32 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87580 0 0 0 112792 244 0 0 25 0 1 0 550718682 365756416 77547 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89296 77547 603 41 0 89255 0
vsize: 357184
[startup+1140.32 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87598 0 0 0 113792 244 0 0 25 0 1 0 550718682 365891584 77565 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89329 77565 603 41 0 89288 0
vsize: 357316
[startup+1150.32 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87611 0 0 0 114791 245 0 0 25 0 1 0 550718682 365891584 77578 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89329 77578 603 41 0 89288 0
vsize: 357316
[startup+1160.32 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 87948 0 0 0 115789 247 0 0 25 0 1 0 550718682 367235072 77915 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89657 77915 603 41 0 89616 0
vsize: 358628
[startup+1170.32 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 88409 0 0 0 116787 249 0 0 25 0 1 0 550718682 369111040 78376 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90115 78376 603 41 0 90074 0
vsize: 360460
[startup+1180.32 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 88817 0 0 0 117786 251 0 0 25 0 1 0 550718682 370757632 78784 4294967295 134512640 134672761 3221224624 3221223728 134555200 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90517 78784 603 41 0 90476 0
vsize: 362068
[startup+1190.32 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 89174 0 0 0 118785 252 0 0 25 0 1 0 550718682 372236288 79141 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90878 79141 603 41 0 90837 0
vsize: 363512
[startup+1200.33 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 17389
Raw data (stat): 17389 (minisat+) R 17388 26298 26297 0 -1 0 89489 0 0 0 119784 253 0 0 25 0 1 0 550718682 373575680 79456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91205 79456 603 41 0 91164 0
vsize: 364820
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.48 s]
Raw data (loadavg): 0.99 0.97 0.95 1/54 17389
Raw data (stat): 17389 (minisat+) Z 17388 26298 26297 0 -1 12 89491 0 0 0 119784 268 0 0 25 0 1 0 550718682 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.48
CPU time (s): 1200.54
CPU user time (s): 1197.85
CPU system time (s): 2.68959
CPU usage (%): 100.004
Max. virtual memory (Kb): 364820
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####