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 19927

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-21 19:55:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15781 boxname=wulflinc19 idbench=1214 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6bb160e5eb0ef9c02ca7232f62836f2b  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-fit1d.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-fit1d.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-fit1d.opb
IDLAUNCH: 15781
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        766352 kB
Buffers:         25024 kB
Cached:         218944 kB
SwapCached:        560 kB
Active:          49544 kB
Inactive:       196484 kB
HighTotal:      131008 kB
HighFree:         6020 kB
LowTotal:       903652 kB
LowFree:        760332 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5168 kB
Slab:            16552 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 20:15:06 (client local time) WITH STATUS 0 IN 1200.59 SECONDS
stats: 15781 7 1200.59 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-c#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.94 2/55 7629
Raw data (stat): 7629 (runsolver) R 7628 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547755973 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 12324 0 0 0 972 26 0 0 25 0 1 0 547755973 42450944 9096 4294967295 134512640 134672761 3221224544 3220453312 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10364 9096 603 41 0 10323 0
vsize: 41456
[startup+20.001 s]
Raw data (loadavg): 0.94 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 14680 0 0 0 1968 30 0 0 25 0 1 0 547755973 56041472 11452 4294967295 134512640 134672761 3221224544 3220482864 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13682 11452 603 41 0 13641 0
vsize: 54728
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 21511 0 0 0 2953 46 0 0 25 0 1 0 547755973 71577600 15647 4294967295 134512640 134672761 3221224544 3220511200 134594095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17475 15647 603 41 0 17434 0
vsize: 69900
[startup+40.0026 s]
Raw data (loadavg): 0.96 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 22875 0 0 0 3950 48 0 0 25 0 1 0 547755973 75767808 17011 4294967295 134512640 134672761 3221224544 3220494112 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18498 17011 603 41 0 18457 0
vsize: 73992
[startup+50.0034 s]
Raw data (loadavg): 0.96 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 24440 0 0 0 4948 51 0 0 25 0 1 0 547755973 80633856 18576 4294967295 134512640 134672761 3221224544 3220526848 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19686 18576 603 41 0 19645 0
vsize: 78744
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 25848 0 0 0 5945 54 0 0 25 0 1 0 547755973 97542144 19984 4294967295 134512640 134672761 3221224544 3220686784 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23814 19984 603 41 0 23773 0
vsize: 95256
[startup+70.004 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 27065 0 0 0 6943 56 0 0 25 0 1 0 547755973 101326848 21201 4294967295 134512640 134672761 3221224544 3220545264 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24738 21201 603 41 0 24697 0
vsize: 98952
[startup+80.0048 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 28208 0 0 0 7941 58 0 0 25 0 1 0 547755973 104841216 22344 4294967295 134512640 134672761 3221224544 3220609104 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25596 22344 603 41 0 25555 0
vsize: 102384
[startup+90.0053 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 39702 0 0 0 8915 84 0 0 25 0 1 0 547755973 129409024 28564 4294967295 134512640 134672761 3221224544 3221003264 134592600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31594 28565 603 41 0 31553 0
vsize: 126376
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 40727 0 0 0 9913 86 0 0 25 0 1 0 547755973 132517888 29589 4294967295 134512640 134672761 3221224544 3220573680 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32353 29589 603 41 0 32312 0
vsize: 129412
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 41760 0 0 0 10912 88 0 0 25 0 1 0 547755973 135761920 30622 4294967295 134512640 134672761 3221224544 3220546720 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33145 30622 603 41 0 33104 0
vsize: 132580
[startup+120.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 42741 0 0 0 11910 90 0 0 25 0 1 0 547755973 138735616 31603 4294967295 134512640 134672761 3221224544 3220568416 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33871 31603 603 41 0 33830 0
vsize: 135484
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 43693 0 0 0 12909 91 0 0 25 0 1 0 547755973 141709312 32555 4294967295 134512640 134672761 3221224544 3220572912 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34597 32555 603 41 0 34556 0
vsize: 138388
[startup+140.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 44579 0 0 0 13908 93 0 0 25 0 1 0 547755973 144412672 33441 4294967295 134512640 134672761 3221224544 3220534336 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35257 33441 603 41 0 35216 0
vsize: 141028
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 45435 0 0 0 14906 95 0 0 25 0 1 0 547755973 146980864 34297 4294967295 134512640 134672761 3221224544 3220615168 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35884 34297 603 41 0 35843 0
vsize: 143536
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 46223 0 0 0 15904 97 0 0 25 0 1 0 547755973 149413888 35085 4294967295 134512640 134672761 3221224544 3220571296 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36478 35085 603 41 0 36437 0
vsize: 145912
[startup+170.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 46991 0 0 0 16903 98 0 0 25 0 1 0 547755973 151846912 35853 4294967295 134512640 134672761 3221224544 3220554208 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37072 35853 603 41 0 37031 0
vsize: 148288
[startup+180.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 47739 0 0 0 17902 99 0 0 25 0 1 0 547755973 179310592 36601 4294967295 134512640 134672761 3221224544 3220546224 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43777 36601 603 41 0 43736 0
vsize: 175108
[startup+190.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 48507 0 0 0 18900 101 0 0 25 0 1 0 547755973 181743616 37369 4294967295 134512640 134672761 3221224544 3220554880 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44371 37369 603 41 0 44330 0
vsize: 177484
[startup+200.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 49216 0 0 0 19899 103 0 0 25 0 1 0 547755973 183906304 38078 4294967295 134512640 134672761 3221224544 3220607856 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44899 38078 603 41 0 44858 0
vsize: 179596
[startup+210.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 49923 0 0 0 20898 104 0 0 25 0 1 0 547755973 186068992 38785 4294967295 134512640 134672761 3221224544 3220606048 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45427 38785 603 41 0 45386 0
vsize: 181708
[startup+220.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 50602 0 0 0 21897 105 0 0 25 0 1 0 547755973 188096512 39464 4294967295 134512640 134672761 3221224544 3220695232 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45922 39464 603 41 0 45881 0
vsize: 183688
[startup+230.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 51265 0 0 0 22896 106 0 0 25 0 1 0 547755973 190124032 40127 4294967295 134512640 134672761 3221224544 3220748496 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46417 40127 603 41 0 46376 0
vsize: 185668
[startup+240.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 51916 0 0 0 23895 108 0 0 25 0 1 0 547755973 192151552 40778 4294967295 134512640 134672761 3221224544 3220573104 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46912 40778 603 41 0 46871 0
vsize: 187648
[startup+250.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 52549 0 0 0 24894 109 0 0 25 0 1 0 547755973 194179072 41411 4294967295 134512640 134672761 3221224544 3220700992 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47407 41411 603 41 0 47366 0
vsize: 189628
[startup+260.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 53157 0 0 0 25893 111 0 0 25 0 1 0 547755973 196071424 42019 4294967295 134512640 134672761 3221224544 3220669792 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47869 42019 603 41 0 47828 0
vsize: 191476
[startup+270.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 53734 0 0 0 26892 112 0 0 25 0 1 0 547755973 197828608 42596 4294967295 134512640 134672761 3221224544 3220609984 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48298 42596 603 41 0 48257 0
vsize: 193192
[startup+280.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7629
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 54302 0 0 0 27891 113 0 0 25 0 1 0 547755973 199585792 43164 4294967295 134512640 134672761 3221224544 3220719520 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48727 43164 603 41 0 48686 0
vsize: 194908
[startup+290.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7631
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 54848 0 0 0 28891 114 0 0 25 0 1 0 547755973 201207808 43710 4294967295 134512640 134672761 3221224544 3220681488 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49123 43710 603 41 0 49082 0
vsize: 196492
[startup+300.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 7631
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 76301 0 0 0 29842 163 0 0 25 0 1 0 547755973 245485568 54617 4294967295 134512640 134672761 3221224544 3220693776 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59933 54617 603 41 0 59892 0
vsize: 239732
[startup+310.022 s]
Raw data (loadavg): 1.07 1.00 0.95 2/55 7684
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 76823 0 0 0 30839 166 0 0 25 0 1 0 547755973 247107584 55139 4294967295 134512640 134672761 3221224544 3220624672 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60329 55139 603 41 0 60288 0
vsize: 241316
[startup+320.022 s]
Raw data (loadavg): 1.06 1.00 0.95 2/55 7684
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 77329 0 0 0 31838 167 0 0 25 0 1 0 547755973 248729600 55645 4294967295 134512640 134672761 3221224544 3220597984 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60725 55645 603 41 0 60684 0
vsize: 242900
[startup+330.022 s]
Raw data (loadavg): 1.05 1.00 0.95 2/55 7684
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 77864 0 0 0 32838 167 0 0 25 0 1 0 547755973 250351616 56180 4294967295 134512640 134672761 3221224544 3220639248 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61121 56180 603 41 0 61080 0
vsize: 244484
[startup+340.022 s]
Raw data (loadavg): 1.04 1.00 0.95 2/55 7684
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 78370 0 0 0 33837 168 0 0 25 0 1 0 547755973 251973632 56686 4294967295 134512640 134672761 3221224544 3220624272 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61517 56686 603 41 0 61476 0
vsize: 246068
[startup+350.026 s]
Raw data (loadavg): 1.03 1.00 0.95 2/55 7684
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 78900 0 0 0 34836 169 0 0 25 0 1 0 547755973 253595648 57216 4294967295 134512640 134672761 3221224544 3220640320 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61913 57216 603 41 0 61872 0
vsize: 247652
[startup+360.025 s]
Raw data (loadavg): 1.03 1.00 0.95 2/55 7684
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 79386 0 0 0 35835 170 0 0 25 0 1 0 547755973 255082496 57702 4294967295 134512640 134672761 3221224544 3220681888 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62276 57702 603 41 0 62235 0
vsize: 249104
[startup+370.026 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 7684
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 79860 0 0 0 36836 171 0 0 25 0 1 0 547755973 256569344 58176 4294967295 134512640 134672761 3221224544 3220651648 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62639 58176 603 41 0 62598 0
vsize: 250556
[startup+380.028 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 80315 0 0 0 37835 171 0 0 25 0 1 0 547755973 257921024 58631 4294967295 134512640 134672761 3221224544 3220611040 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62969 58631 603 41 0 62928 0
vsize: 251876
[startup+390.029 s]
Raw data (loadavg): 1.02 1.00 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 80777 0 0 0 38835 172 0 0 25 0 1 0 547755973 259407872 59093 4294967295 134512640 134672761 3221224544 3220651728 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63332 59093 603 41 0 63291 0
vsize: 253328
[startup+400.029 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 81244 0 0 0 39834 173 0 0 25 0 1 0 547755973 260759552 59560 4294967295 134512640 134672761 3221224544 3220722400 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63662 59560 603 41 0 63621 0
vsize: 254648
[startup+410.029 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 81769 0 0 0 40833 174 0 0 25 0 1 0 547755973 262381568 60085 4294967295 134512640 134672761 3221224544 3220792192 134594101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64058 60085 603 41 0 64017 0
vsize: 256232
[startup+420.03 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 82250 0 0 0 41833 174 0 0 25 0 1 0 547755973 263868416 60566 4294967295 134512640 134672761 3221224544 3220744752 134594261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64421 60566 603 41 0 64380 0
vsize: 257684
[startup+430.031 s]
Raw data (loadavg): 1.01 1.00 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 82747 0 0 0 42832 175 0 0 25 0 1 0 547755973 265355264 61063 4294967295 134512640 134672761 3221224544 3220704160 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64784 61063 603 41 0 64743 0
vsize: 259136
[startup+440.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 83245 0 0 0 43832 176 0 0 25 0 1 0 547755973 266977280 61561 4294967295 134512640 134672761 3221224544 3220785664 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65180 61561 603 41 0 65139 0
vsize: 260720
[startup+450.033 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 83693 0 0 0 44831 177 0 0 25 0 1 0 547755973 268328960 62009 4294967295 134512640 134672761 3221224544 3220625824 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65510 62009 603 41 0 65469 0
vsize: 262040
[startup+460.032 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 84181 0 0 0 45831 177 0 0 25 0 1 0 547755973 269815808 62497 4294967295 134512640 134672761 3221224544 3220795936 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65873 62497 603 41 0 65832 0
vsize: 263492
[startup+470.032 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 84643 0 0 0 46830 179 0 0 25 0 1 0 547755973 271302656 62959 4294967295 134512640 134672761 3221224544 3220648368 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66236 62959 603 41 0 66195 0
vsize: 264944
[startup+480.032 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 85085 0 0 0 47829 180 0 0 25 0 1 0 547755973 272654336 63401 4294967295 134512640 134672761 3221224544 3220726704 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66566 63401 603 41 0 66525 0
vsize: 266264
[startup+490.033 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 85533 0 0 0 48829 180 0 0 25 0 1 0 547755973 274006016 63849 4294967295 134512640 134672761 3221224544 3220766464 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66896 63849 603 41 0 66855 0
vsize: 267584
[startup+500.032 s]
Raw data (loadavg): 1.07 1.02 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 85953 0 0 0 49828 181 0 0 25 0 1 0 547755973 275357696 64269 4294967295 134512640 134672761 3221224544 3220692240 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67226 64269 603 41 0 67185 0
vsize: 268904
[startup+510.032 s]
Raw data (loadavg): 1.06 1.02 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 86400 0 0 0 50827 182 0 0 25 0 1 0 547755973 276709376 64716 4294967295 134512640 134672761 3221224544 3220675344 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67556 64716 603 41 0 67515 0
vsize: 270224
[startup+520.033 s]
Raw data (loadavg): 1.05 1.01 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 86924 0 0 0 51827 183 0 0 25 0 1 0 547755973 278331392 65240 4294967295 134512640 134672761 3221224544 3220731040 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67952 65240 603 41 0 67911 0
vsize: 271808
[startup+530.033 s]
Raw data (loadavg): 1.04 1.01 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 87859 0 0 0 52825 184 0 0 25 0 1 0 547755973 281169920 66175 4294967295 134512640 134672761 3221224544 3220654512 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68645 66175 603 41 0 68604 0
vsize: 274580
[startup+540.034 s]
Raw data (loadavg): 1.04 1.01 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 88706 0 0 0 53824 186 0 0 25 0 1 0 547755973 283738112 67022 4294967295 134512640 134672761 3221224544 3220808416 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69272 67022 603 41 0 69231 0
vsize: 277088
[startup+550.034 s]
Raw data (loadavg): 1.03 1.01 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 89536 0 0 0 54823 187 0 0 25 0 1 0 547755973 286306304 67852 4294967295 134512640 134672761 3221224544 3220869936 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69899 67852 603 41 0 69858 0
vsize: 279596
[startup+560.034 s]
Raw data (loadavg): 1.02 1.01 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 90303 0 0 0 55821 189 0 0 25 0 1 0 547755973 288739328 68619 4294967295 134512640 134672761 3221224544 3220940016 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70493 68619 603 41 0 70452 0
vsize: 281972
[startup+570.034 s]
Raw data (loadavg): 1.02 1.01 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 91027 0 0 0 56820 190 0 0 25 0 1 0 547755973 290902016 69343 4294967295 134512640 134672761 3221224544 3220895472 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71021 69343 603 41 0 70980 0
vsize: 284084
[startup+580.034 s]
Raw data (loadavg): 1.02 1.01 0.95 2/55 7686
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 91696 0 0 0 57819 191 0 0 25 0 1 0 547755973 293064704 70012 4294967295 134512640 134672761 3221224544 3220812064 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71549 70012 603 41 0 71508 0
vsize: 286196
[startup+590.035 s]
Raw data (loadavg): 1.01 1.01 0.95 2/55 7688
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 92388 0 0 0 58818 192 0 0 25 0 1 0 547755973 295092224 70704 4294967295 134512640 134672761 3221224544 3220700704 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72044 70704 603 41 0 72003 0
vsize: 288176
[startup+600.035 s]
Raw data (loadavg): 1.01 1.01 0.95 2/55 7688
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 93050 0 0 0 59817 194 0 0 25 0 1 0 547755973 297119744 71366 4294967295 134512640 134672761 3221224544 3220716048 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72539 71366 603 41 0 72498 0
vsize: 290156
[startup+610.034 s]
Raw data (loadavg): 1.01 1.01 0.95 2/55 7688
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 93673 0 0 0 60815 196 0 0 25 0 1 0 547755973 349478912 71989 4294967295 134512640 134672761 3221224544 3220900768 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85322 71989 603 41 0 85281 0
vsize: 341288
[startup+620.035 s]
Raw data (loadavg): 1.08 1.02 0.96 2/55 7688
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 94311 0 0 0 61815 197 0 0 25 0 1 0 547755973 351371264 72627 4294967295 134512640 134672761 3221224544 3221004292 134592581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85784 72627 603 41 0 85743 0
vsize: 343136
[startup+630.035 s]
Raw data (loadavg): 1.07 1.02 0.96 2/55 7688
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 94907 0 0 0 62814 198 0 0 25 0 1 0 547755973 353263616 73223 4294967295 134512640 134672761 3221224544 3220690136 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86246 73223 603 41 0 86205 0
vsize: 344984
[startup+640.035 s]
Raw data (loadavg): 1.06 1.02 0.96 2/55 7688
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 95487 0 0 0 63813 198 0 0 25 0 1 0 547755973 355020800 73803 4294967295 134512640 134672761 3221224544 3220870528 134594133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86675 73803 603 41 0 86634 0
vsize: 346700
[startup+650.035 s]
Raw data (loadavg): 1.05 1.02 0.96 2/55 7688
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 96270 0 0 0 64812 199 0 0 25 0 1 0 547755973 357453824 74586 4294967295 134512640 134672761 3221224544 3220839808 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87269 74586 603 41 0 87228 0
vsize: 349076
[startup+660.036 s]
Raw data (loadavg): 1.04 1.02 0.96 2/55 7688
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 97377 0 0 0 65810 201 0 0 25 0 1 0 547755973 360833024 75693 4294967295 134512640 134672761 3221224544 3221087952 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88094 75693 603 41 0 88053 0
vsize: 352376
[startup+670.036 s]
Raw data (loadavg): 1.03 1.02 0.96 2/55 7688
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 98308 0 0 0 66809 203 0 0 25 0 1 0 547755973 363671552 76624 4294967295 134512640 134672761 3221224544 3220907104 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88787 76624 603 41 0 88746 0
vsize: 355148
[startup+680.036 s]
Raw data (loadavg): 1.03 1.02 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 99171 0 0 0 67808 204 0 0 25 0 1 0 547755973 366374912 77487 4294967295 134512640 134672761 3221224544 3220960176 134594206 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 89447 77487 603 41 0 89406 0
vsize: 357788
[startup+690.037 s]
Raw data (loadavg): 1.02 1.01 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 100022 0 0 0 68807 205 0 0 25 0 1 0 547755973 368943104 78338 4294967295 134512640 134672761 3221224544 3221002528 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90074 78338 603 41 0 90033 0
vsize: 360296
[startup+700.037 s]
Raw data (loadavg): 1.02 1.01 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 100845 0 0 0 69806 206 0 0 25 0 1 0 547755973 371511296 79161 4294967295 134512640 134672761 3221224544 3221049760 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90701 79161 603 41 0 90660 0
vsize: 362804
[startup+710.037 s]
Raw data (loadavg): 1.02 1.01 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 101606 0 0 0 70805 207 0 0 25 0 1 0 547755973 373944320 79922 4294967295 134512640 134672761 3221224544 3220722776 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 91295 79922 603 41 0 91254 0
vsize: 365180
[startup+720.038 s]
Raw data (loadavg): 1.01 1.01 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 106084 0 0 0 71798 215 0 0 25 0 1 0 547755973 387731456 84400 4294967295 134512640 134672761 3221224544 3220761184 134594151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 94661 84400 603 41 0 94620 0
vsize: 378644
[startup+730.038 s]
Raw data (loadavg): 1.01 1.01 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 150812 0 0 0 72692 321 0 0 25 0 1 0 547755973 481955840 108036 4294967295 134512640 134672761 3221224544 3220985344 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117665 108036 603 41 0 117624 0
vsize: 470660
[startup+740.038 s]
Raw data (loadavg): 1.01 1.01 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 156208 0 0 0 73683 330 0 0 25 0 1 0 547755973 498581504 113432 4294967295 134512640 134672761 3221224544 3221021824 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121724 113432 603 41 0 121683 0
vsize: 486896
[startup+750.038 s]
Raw data (loadavg): 1.01 1.01 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 159295 0 0 0 74677 336 0 0 25 0 1 0 547755973 508043264 116519 4294967295 134512640 134672761 3221224544 3220873504 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124034 116519 603 41 0 123993 0
vsize: 496136
[startup+760.038 s]
Raw data (loadavg): 1.00 1.01 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 164850 0 0 0 75668 345 0 0 25 0 1 0 547755973 525209600 122074 4294967295 134512640 134672761 3221224544 3220878016 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 128225 122074 603 41 0 128184 0
vsize: 512900
[startup+770.038 s]
Raw data (loadavg): 1.00 1.01 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 176067 0 0 0 76652 362 0 0 25 0 1 0 547755973 559812608 133291 4294967295 134512640 134672761 3221224544 3220962496 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 136673 133291 603 41 0 136632 0
vsize: 546692
[startup+780.038 s]
Raw data (loadavg): 1.00 1.01 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 196524 0 0 0 77617 397 0 0 25 0 1 0 547755973 723464192 153748 4294967295 134512640 134672761 3221224544 3221085704 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 176660 153749 603 41 0 176619 0
vsize: 706508
[startup+790.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 206104 0 0 0 78596 418 0 0 25 0 1 0 547755973 662478848 140958 4294967295 134512640 134672761 3221224544 3220506784 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 161738 140958 603 41 0 161697 0
vsize: 646952
[startup+800.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 207897 0 0 0 79593 422 0 0 25 0 1 0 547755973 667209728 142751 4294967295 134512640 134672761 3221224544 3220526064 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 162893 142751 603 41 0 162852 0
vsize: 651572
[startup+810.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 211766 0 0 0 80584 431 0 0 25 0 1 0 547755973 675721216 145302 4294967295 134512640 134672761 3221224544 3220517152 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 164971 145302 603 41 0 164930 0
vsize: 659884
[startup+820.039 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 212798 0 0 0 81583 432 0 0 25 0 1 0 547755973 678424576 146334 4294967295 134512640 134672761 3221224544 3220556128 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 165631 146334 603 41 0 165590 0
vsize: 662524
[startup+830.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 213886 0 0 0 82581 434 0 0 25 0 1 0 547755973 681127936 147422 4294967295 134512640 134672761 3221224544 3220681216 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 166291 147422 603 41 0 166250 0
vsize: 665164
[startup+840.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 214607 0 0 0 83580 435 0 0 25 0 1 0 547755973 683020288 148143 4294967295 134512640 134672761 3221224544 3220464336 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 166753 148143 603 41 0 166712 0
vsize: 667012
[startup+850.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 256956 0 0 0 84475 540 0 0 25 0 1 0 547755973 856203264 190492 4294967295 134512640 134672761 3221224544 3220531552 134523749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 209034 190492 603 41 0 208993 0
vsize: 836136
[startup+860.039 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 257493 0 0 0 85470 545 0 0 25 0 1 0 547755973 771301376 169938 4294967295 134512640 134672761 3221224544 3220520224 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 188306 169938 603 41 0 188265 0
vsize: 753224
[startup+870.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 258432 0 0 0 86469 547 0 0 25 0 1 0 547755973 773599232 170877 4294967295 134512640 134672761 3221224544 3220618048 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 188867 170877 603 41 0 188826 0
vsize: 755468
[startup+880.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7690
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 264138 0 0 0 87455 560 0 0 25 0 1 0 547755973 785612800 173946 4294967295 134512640 134672761 3221224544 3220519072 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 191800 173946 603 41 0 191759 0
vsize: 767200
[startup+890.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 264548 0 0 0 88455 561 0 0 25 0 1 0 547755973 786558976 174356 4294967295 134512640 134672761 3221224544 3220513200 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 192031 174356 603 41 0 191990 0
vsize: 768124
[startup+900.041 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 265008 0 0 0 89454 562 0 0 25 0 1 0 547755973 787775488 174816 4294967295 134512640 134672761 3221224544 3220492944 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 192328 174816 603 41 0 192287 0
vsize: 769312
[startup+910.041 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 265772 0 0 0 90453 563 0 0 25 0 1 0 547755973 789803008 175580 4294967295 134512640 134672761 3221224544 3220661056 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 192823 175580 603 41 0 192782 0
vsize: 771292
[startup+920.041 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 266280 0 0 0 91452 564 0 0 25 0 1 0 547755973 791019520 176088 4294967295 134512640 134672761 3221224544 3220675072 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 193120 176088 603 41 0 193079 0
vsize: 772480
[startup+930.041 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 266731 0 0 0 92452 565 0 0 25 0 1 0 547755973 792236032 176539 4294967295 134512640 134672761 3221224544 3220588656 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 193417 176539 603 41 0 193376 0
vsize: 773668
[startup+940.046 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 267184 0 0 0 93452 565 0 0 25 0 1 0 547755973 793452544 176992 4294967295 134512640 134672761 3221224544 3220579456 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 193714 176992 603 41 0 193673 0
vsize: 774856
[startup+950.045 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 267603 0 0 0 94452 566 0 0 25 0 1 0 547755973 794533888 177411 4294967295 134512640 134672761 3221224544 3220531072 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 193978 177411 603 41 0 193937 0
vsize: 775912
[startup+960.046 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 268330 0 0 0 95450 568 0 0 25 0 1 0 547755973 796291072 178138 4294967295 134512640 134672761 3221224544 3220727584 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 194407 178138 603 41 0 194366 0
vsize: 777628
[startup+970.046 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 268797 0 0 0 96450 568 0 0 25 0 1 0 547755973 797507584 178605 4294967295 134512640 134672761 3221224544 3220553232 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 194704 178605 603 41 0 194663 0
vsize: 778816
[startup+980.046 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 269198 0 0 0 97449 569 0 0 25 0 1 0 547755973 798588928 179006 4294967295 134512640 134672761 3221224544 3220604400 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 194968 179006 603 41 0 194927 0
vsize: 779872
[startup+990.046 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 269583 0 0 0 98449 570 0 0 25 0 1 0 547755973 799535104 179391 4294967295 134512640 134672761 3221224544 3220608624 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 195199 179391 603 41 0 195158 0
vsize: 780796
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 269942 0 0 0 99448 570 0 0 25 0 1 0 547755973 800481280 179750 4294967295 134512640 134672761 3221224544 3220604128 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 195430 179750 603 41 0 195389 0
vsize: 781720
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 270293 0 0 0 100448 571 0 0 25 0 1 0 547755973 801427456 180101 4294967295 134512640 134672761 3221224544 3220450032 134594261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 195661 180101 603 41 0 195620 0
vsize: 782644
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 271045 0 0 0 101447 572 0 0 25 0 1 0 547755973 803319808 180853 4294967295 134512640 134672761 3221224544 3220642224 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 196123 180853 603 41 0 196082 0
vsize: 784492
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 271402 0 0 0 102446 573 0 0 25 0 1 0 547755973 804265984 181210 4294967295 134512640 134672761 3221224544 3220513392 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 196354 181210 603 41 0 196313 0
vsize: 785416
[startup+1040.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 271744 0 0 0 103445 574 0 0 25 0 1 0 547755973 805076992 181552 4294967295 134512640 134672761 3221224544 3220500432 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 196552 181552 603 41 0 196511 0
vsize: 786208
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 272089 0 0 0 104445 574 0 0 25 0 1 0 547755973 806023168 181897 4294967295 134512640 134672761 3221224544 3220601424 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 196783 181897 603 41 0 196742 0
vsize: 787132
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 272406 0 0 0 105444 575 0 0 25 0 1 0 547755973 806834176 182214 4294967295 134512640 134672761 3221224544 3220476432 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 196981 182215 603 41 0 196940 0
vsize: 787924
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 272734 0 0 0 106444 575 0 0 25 0 1 0 547755973 807645184 182542 4294967295 134512640 134672761 3221224544 3220453968 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 197179 182542 603 41 0 197138 0
vsize: 788716
[startup+1080.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 273361 0 0 0 107443 576 0 0 25 0 1 0 547755973 809267200 183169 4294967295 134512640 134672761 3221224544 3220659408 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 197575 183169 603 41 0 197534 0
vsize: 790300
[startup+1090.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 273668 0 0 0 108443 577 0 0 25 0 1 0 547755973 810078208 183476 4294967295 134512640 134672761 3221224544 3220519360 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 197773 183476 603 41 0 197732 0
vsize: 791092
[startup+1100.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 273958 0 0 0 109443 578 0 0 25 0 1 0 547755973 810889216 183766 4294967295 134512640 134672761 3221224544 3220548928 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 197971 183766 603 41 0 197930 0
vsize: 791884
[startup+1110.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 274467 0 0 0 110442 579 0 0 25 0 1 0 547755973 812105728 184275 4294967295 134512640 134672761 3221224544 3220672960 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 198268 184275 603 41 0 198227 0
vsize: 793072
[startup+1120.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 285265 0 0 0 111413 606 0 0 25 0 1 0 547755973 834379776 189742 4294967295 134512640 134672761 3221224544 3220648576 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 203706 189742 603 41 0 203665 0
vsize: 814824
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 285482 0 0 0 112413 606 0 0 25 0 1 0 547755973 834785280 189950 4294967295 134512640 134672761 3221224544 3220608832 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 203805 189950 603 41 0 203764 0
vsize: 815220
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 285671 0 0 0 113413 607 0 0 25 0 1 0 547755973 835325952 190131 4294967295 134512640 134672761 3221224544 3220540848 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 203937 190131 603 41 0 203896 0
vsize: 815748
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 285886 0 0 0 114413 607 0 0 25 0 1 0 547755973 835866624 190343 4294967295 134512640 134672761 3221224544 3220543536 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 204069 190343 603 41 0 204028 0
vsize: 816276
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 286412 0 0 0 115412 608 0 0 25 0 1 0 547755973 837083136 190863 4294967295 134512640 134672761 3221224544 3220787008 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 204366 190863 603 41 0 204325 0
vsize: 817464
[startup+1170.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 286710 0 0 0 116411 608 0 0 25 0 1 0 547755973 837894144 191160 4294967295 134512640 134672761 3221224544 3220677376 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 204564 191160 603 41 0 204523 0
vsize: 818256
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7692
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 286941 0 0 0 117411 609 0 0 25 0 1 0 547755973 838434816 191391 4294967295 134512640 134672761 3221224544 3220526256 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 204696 191391 603 41 0 204655 0
vsize: 818784
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7694
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 287206 0 0 0 118411 609 0 0 25 0 1 0 547755973 839110656 191656 4294967295 134512640 134672761 3221224544 3220463952 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 204861 191656 603 41 0 204820 0
vsize: 819444
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 7694
Raw data (stat): 7629 (minisat+) R 7628 22929 22928 0 -1 0 287663 0 0 0 119411 610 0 0 25 0 1 0 547755973 840327168 192112 4294967295 134512640 134672761 3221224544 3220658064 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 205158 192112 603 41 0 205117 0
vsize: 820632
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.49 s]
Raw data (loadavg): 1.00 1.00 0.96 1/55 7694
Raw data (stat): 7629 (minisat+) Z 7628 22929 22928 0 -1 12 287666 0 0 0 119411 647 0 0 21 0 1 0 547755973 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.49
CPU time (s): 1200.59
CPU user time (s): 1194.12
CPU system time (s): 6.47002
CPU usage (%): 100.008
Max. virtual memory (Kb): 836136
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####