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/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-sp97ic.opb
MD5SUM	e8862b41c9b4f49ec8d11d1df0495e74
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	12497
Biggest coefficient in the objective function	1010107916
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	3093137085579
Number of bits of the sum of numbers in the objective function	42
Biggest number in a constraint	1010107916
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	3093137085579
Number of bits of the biggest sum of numbers	42
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	11.8052
Number of variables	12497
Total number of constraints	13530
Number of constraints which are clauses	41
Number of constraints which are cardinality constraints (but not clauses)	13312
Number of constraints which are nor clauses,nor cardinality constraints	177
Minimum length of a constraint	1
Maximum length of a constraint	6739
Trace number 14270

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-20 23:24:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20246 boxname=wulflinc9 idbench=1558 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  e8862b41c9b4f49ec8d11d1df0495e74  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-sp97ic.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-sp97ic.opb
IDLAUNCH: 20246
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        646756 kB
Buffers:         34660 kB
Cached:         329744 kB
SwapCached:          8 kB
Active:          57652 kB
Inactive:       309488 kB
HighTotal:      131008 kB
HighFree:        12264 kB
LowTotal:       903652 kB
LowFree:        634492 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6824 kB
Slab:            15000 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:44:06 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 20246 7 1200.3 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1033 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .sssss.sssssssssssssssss..s.sss.s.sssss.ss.sssssssssssssssssssssssssssssss..ss.ss.sssssssss.s.ssss...sssss.s...s.ss.s.s.s.s....ss.ssss.s.ss..sssssssssssssssss...s..ssssss
c ---[1158]---> BDD-cost:   39
c ---[1157]---> BDD-cost:   39
c ---[1156]---> BDD-cost:   39
c ---[1155]---> BDD-cost:   39
c ---[1154]---> BDD-cost:   39
c ---[1153]---> BDD-cost:   47
c ---[1152]---> BDD-cost:   47
c ---[1151]---> BDD-cost:   47
c ---[1150]---> BDD-cost:   47
c ---[1149]---> BDD-cost:   35
c ---[1147]---> BDD-cost:    7
c ---[1146]---> BDD-cost:   23
c ---[1145]---> BDD-cost:   23
c ---[1144]---> BDD-cost:   13
c ---[1143]---> BDD-cost:   25
c ---[1142]---> BDD-cost:   19
c ---[1141]---> BDD-cost:   23
c ---[1140]---> BDD-cost:   23
c ---[1139]---> BDD-cost:   23
c ---[1138]---> BDD-cost:   23
c ---[1136]---> BDD-cost:   23
c ---[1135]---> BDD-cost:   23
c ---[1134]---> BDD-cost:   25
c ---[1133]---> BDD-cost:   25
c ---[1132]---> BDD-cost:    5
c ---[1131]---> BDD-cost:   25
c ---[1130]---> BDD-cost:   19
c ---[1129]---> BDD-cost:   19
c ---[1128]---> BDD-cost:   19
c ---[1127]---> BDD-cost:   25
c ---[1125]---> BDD-cost:   19
c ---[1124]---> BDD-cost:   25
c ---[1123]---> BDD-cost:   19
c ---[1117]---> Adder-cost: 23092   maxlim: 39   bits: 7/6
c ---[1114]---> Adder-cost: 13882   maxlim: 29   bits: 6/5
c ---[1098]---> BDD-cost:  161
c ---[1093]---> BDD-cost: 2360
c ---[1082]---> BDD-cost: 1572
c ---[1071]---> BDD-cost:  200
c ---[1067]---> BDD-cost:  189
c ---[1060]---> BDD-cost:  294
c ---[1051]---> BDD-cost: 4351
c ---[1050]---> Adder-cost: 838   maxlim: 12   bits: 5/4
c ---[1033]---> BDD-cost:  212
c ---[1011]---> BDD-cost:   25
c ---[1010]---> BDD-cost:    7
c ---[1009]---> BDD-cost:    3
c ---[1008]---> BDD-cost:   13
c ---[1007]---> BDD-cost:    3
c ---[1006]---> BDD-cost:   25
c ---[1005]---> BDD-cost:   19
c ---[1004]---> BDD-cost:10182
c ---[1003]---> BDD-cost:   25
c ---[1002]---> BDD-cost:   23
c ---[1001]---> BDD-cost:   19
c ---[ 999]---> BDD-cost:   19
c ---[ 998]---> BDD-cost:   19
c ---[ 997]---> BDD-cost:    9
c ---[ 996]---> BDD-cost:   47
c ---[ 995]---> BDD-cost:    3
c ---[ 994]---> BDD-cost:   25
c ---[ 992]---> BDD-cost:   47
c ---[ 991]---> BDD-cost:   47
c ---[ 990]---> BDD-cost:   47
c ---[ 989]---> BDD-cost:   47
c ---[ 988]---> BDD-cost:    9
c ---[ 987]---> BDD-cost:   13
c ---[ 985]---> BDD-cost:   25
c ---[ 984]---> BDD-cost:   19
c ---[ 983]---> BDD-cost:   19
c ---[ 981]---> BDD-cost:   19
c ---[ 980]---> BDD-cost:   47
c ---[ 978]---> BDD-cost:   25
c ---[ 977]---> BDD-cost:   19
c ---[ 976]---> BDD-cost:   19
c ---[ 975]---> BDD-cost:    9
c ---[ 974]---> BDD-cost:   19
c ---[ 973]---> BDD-cost:   19
c ---[ 972]---> BDD-cost:   19
c ---[ 970]---> BDD-cost:   47
c ---[ 969]---> BDD-cost:   19
c ---[ 968]---> BDD-cost:   47
c ---[ 967]---> BDD-cost:   47
c ---[ 966]---> BDD-cost:   47
c ---[ 965]---> BDD-cost:   35
c ---[ 964]---> BDD-cost:   19
c ---[ 963]---> BDD-cost:   19
c ---[ 962]---> BDD-cost:   25
c ---[ 961]---> BDD-cost:   19
c ---[ 960]---> BDD-cost:    0
c ---[ 959]---> BDD-cost:   19
c ---[ 958]---> BDD-cost:   19
c ---[ 957]---> BDD-cost:   19
c ---[ 956]---> BDD-cost:   19
c ---[ 955]---> BDD-cost:   19
c ---[ 953]---> BDD-cost:   11
c ---[ 952]---> BDD-cost:    9
c ---[ 951]---> BDD-cost:   11
c ---[ 950]---> BDD-cost:    3
c ---[ 949]---> BDD-cost: 5686
c ---[ 948]---> BDD-cost:    5
c ---[ 947]---> BDD-cost:   11
c ---[ 946]---> BDD-cost:   25
c ---[ 945]---> BDD-cost:   47
c ---[ 944]---> BDD-cost:   47
c ---[ 943]---> BDD-cost:   47
c ---[ 942]---> BDD-cost:   11
c ---[ 941]---> BDD-cost:   25
c ---[ 940]---> BDD-cost:   25
c ---[ 939]---> BDD-cost:   25
c ---[ 938]---> BDD-cost: 7868
c ---[ 937]---> BDD-cost:   11
c ---[ 936]---> BDD-cost:   11
c ---[ 935]---> BDD-cost:   47
c ---[ 934]---> BDD-cost:    5
c ---[ 933]---> BDD-cost:   11
c ---[ 932]---> BDD-cost:   47
c ---[ 931]---> BDD-cost:   47
c ---[ 930]---> BDD-cost:   47
c ---[ 929]---> BDD-cost:   47
c ---[ 928]---> BDD-cost:   11
c ---[ 926]---> BDD-cost:   11
c ---[ 925]---> BDD-cost:   25
c ---[ 924]---> BDD-cost:    5
c ---[ 923]---> BDD-cost:   11
c ---[ 922]---> BDD-cost:   25
c ---[ 921]---> BDD-cost:   25
c ---[ 920]---> BDD-cost:   25
c ---[ 919]---> BDD-cost:    0
c ---[ 918]---> BDD-cost:    5
c ---[ 917]---> BDD-cost:   11
c ---[ 915]---> BDD-cost:   25
c ---[ 914]---> BDD-cost:   25
c ---[ 913]---> BDD-cost:   25
c ---[ 912]---> BDD-cost:   25
c ---[ 911]---> BDD-cost:   11
c ---[ 910]---> BDD-cost:   11
c ---[ 909]---> BDD-cost:   25
c ---[ 908]---> BDD-cost:   25
c ---[ 907]---> BDD-cost:   47
c ---[ 906]---> BDD-cost:   25
c ---[ 905]---> BDD-cost: 3423
c ---[ 903]---> BDD-cost:   47
c ---[ 902]---> BDD-cost:   25
c ---[ 901]---> BDD-cost:   47
c ---[ 900]---> BDD-cost:    7
c ---[ 899]---> BDD-cost:   25
c ---[ 898]---> BDD-cost:   25
c ---[ 897]---> BDD-cost:   25
c ---[ 896]---> BDD-cost:   25
c ---[ 895]---> BDD-cost:   25
c ---[ 894]---> BDD-cost:   25
c ---[ 892]---> BDD-cost:   25
c ---[ 891]---> BDD-cost:   25
c ---[ 890]---> BDD-cost:    5
c ---[ 889]---> BDD-cost:   25
c ---[ 888]---> BDD-cost:   11
c ---[ 887]---> BDD-cost:   47
c ---[ 886]---> BDD-cost:   47
c ---[ 885]---> BDD-cost:   19
c ---[ 884]---> BDD-cost:   25
c ---[ 883]---> BDD-cost:    9
c ---[ 882]---> BDD-cost: 6499
c ---[ 881]---> BDD-cost:   47
c ---[ 880]---> BDD-cost:   47
c ---[ 879]---> BDD-cost:   25
c ---[ 878]---> BDD-cost:   19
c ---[ 877]---> BDD-cost:   25
c ---[ 876]---> BDD-cost:   19
c ---[ 875]---> BDD-cost:   25
c ---[ 874]---> BDD-cost:    7
c ---[ 873]---> BDD-cost:   19
c ---[ 872]---> BDD-cost:   25
c ---[ 870]---> BDD-cost:   19
c ---[ 869]---> BDD-cost:   19
c ---[ 868]---> BDD-cost:   47
c ---[ 867]---> BDD-cost:   47
c ---[ 866]---> BDD-cost:   47
c ---[ 865]---> BDD-cost:   25
c ---[ 864]---> BDD-cost:   25
c ---[ 863]---> BDD-cost:   19
c ---[ 862]---> BDD-cost:   25
c ---[ 861]---> BDD-cost:    7
c ---[ 859]---> BDD-cost:   11
c ---[ 858]---> BDD-cost:   47
c ---[ 857]---> BDD-cost:   47
c ---[ 856]---> BDD-cost:   25
c ---[ 855]---> BDD-cost:   19
c ---[ 854]---> BDD-cost:    9
c ---[ 853]---> BDD-cost:    5
c ---[ 852]---> BDD-cost:   11
c ---[ 851]---> BDD-cost:   47
c ---[ 850]---> BDD-cost:   47
c ---[ 849]---> BDD-cost: 3650
c ---[ 848]---> BDD-cost:    9
c ---[ 847]---> BDD-cost:   25
c ---[ 846]---> BDD-cost:   25
c ---[ 845]---> BDD-cost:   19
c ---[ 844]---> BDD-cost:   25
c ---[ 843]---> BDD-cost:   19
c ---[ 842]---> BDD-cost:    3
c ---[ 841]---> BDD-cost:   11
c ---[ 840]---> BDD-cost:   25
c ---[ 839]---> BDD-cost:   19
c ---[ 838]---> BDD-cost: 6888
c ---[ 837]---> BDD-cost:   19
c ---[ 836]---> BDD-cost:   47
c ---[ 835]---> BDD-cost:   25
c ---[ 834]---> BDD-cost:   47
c ---[ 833]---> BDD-cost:   47
c ---[ 832]---> BDD-cost:   25
c ---[ 831]---> BDD-cost:   25
c ---[ 830]---> BDD-cost:   19
c ---[ 829]---> BDD-cost:    3
c ---[ 828]---> BDD-cost:    5
c ---[ 827]---> Adder-cost: 7844   maxlim: 5   bits: 4/3
c ---[ 826]---> BDD-cost:   43
c ---[ 825]---> BDD-cost:   35
c ---[ 824]---> BDD-cost:   43
c ---[ 823]---> BDD-cost:   43
c ---[ 822]---> BDD-cost:   11
c ---[ 821]---> BDD-cost:   35
c ---[ 820]---> BDD-cost:   35
c ---[ 819]---> BDD-cost:   11
c ---[ 818]---> BDD-cost:   47
c ---[ 817]---> BDD-cost:   23
c ---[ 816]---> Adder-cost: 16310   maxlim: 39   bits: 7/6
c ---[ 815]---> BDD-cost:    5
c ---[ 814]---> BDD-cost:   19
c ---[ 813]---> BDD-cost:   25
c ---[ 812]---> BDD-cost:   23
c ---[ 811]---> BDD-cost:   25
c ---[ 810]---> BDD-cost:   11
c ---[ 809]---> BDD-cost:    5
c ---[ 808]---> BDD-cost:   35
c ---[ 807]---> BDD-cost:   35
c ---[ 806]---> BDD-cost:   13
c ---[ 805]---> BDD-cost: 3504
c ---[ 804]---> BDD-cost:   25
c ---[ 803]---> BDD-cost:    5
c ---[ 802]---> BDD-cost:   35
c ---[ 801]---> BDD-cost:   35
c ---[ 800]---> BDD-cost:   35
c ---[ 799]---> BDD-cost:   11
c ---[ 798]---> BDD-cost:   35
c ---[ 797]---> BDD-cost:   43
c ---[ 796]---> BDD-cost:   43
c ---[ 795]---> BDD-cost:   43
c ---[ 794]---> BDD-cost: 4241
c ---[ 793]---> BDD-cost: 1556
c ---[ 792]---> BDD-cost:   43
c ---[ 791]---> BDD-cost:   43
c ---[ 790]---> BDD-cost:   43
c ---[ 789]---> BDD-cost:   35
c ---[ 788]---> BDD-cost:   35
c ---[ 787]---> BDD-cost:   35
c ---[ 786]---> BDD-cost:   35
c ---[ 785]---> BDD-cost:   35
c ---[ 784]---> BDD-cost:    5
c ---[ 783]---> BDD-cost:   35
c ---[ 782]---> BDD-cost: 6026
c ---[ 781]---> BDD-cost:   47
c ---[ 780]---> BDD-cost:   47
c ---[ 779]---> BDD-cost:   25
c ---[ 778]---> BDD-cost:   19
c ---[ 777]---> BDD-cost:   11
c ---[ 776]---> BDD-cost:   47
c ---[ 775]---> BDD-cost:   47
c ---[ 774]---> BDD-cost:   11
c ---[ 773]---> BDD-cost:   25
c ---[ 772]---> BDD-cost:   25
c ---[ 771]---> Adder-cost: 6634   maxlim: 29   bits: 6/5
c ---[ 770]---> BDD-cost:   19
c ---[ 769]---> BDD-cost:    3
c ---[ 768]---> BDD-cost:   25
c ---[ 767]---> BDD-cost:   19
c ---[ 766]---> BDD-cost:   25
c ---[ 765]---> BDD-cost:   47
c ---[ 764]---> BDD-cost:   25
c ---[ 763]---> BDD-cost:   47
c ---[ 762]---> BDD-cost:   47
c ---[ 761]---> BDD-cost:   25
c ---[ 760]---> BDD-cost: 1112
c ---[ 759]---> BDD-cost:   25
c ---[ 758]---> BDD-cost:   25
c ---[ 757]---> BDD-cost:   19
c ---[ 756]---> BDD-cost:    3
c ---[ 755]---> BDD-cost:    5
c ---[ 754]---> BDD-cost:   19
c ---[ 753]---> BDD-cost:   25
c ---[ 752]---> BDD-cost:   25
c ---[ 751]---> BDD-cost:   47
c ---[ 750]---> BDD-cost:   43
c ---[ 749]---> BDD-cost: 1117
c ---[ 748]---> BDD-cost:   39
c ---[ 747]---> BDD-cost:   19
c ---[ 746]---> BDD-cost:   25
c ---[ 745]---> BDD-cost:   43
c ---[ 744]---> BDD-cost:   43
c ---[ 743]---> BDD-cost:   13
c ---[ 742]---> BDD-cost:   13
c ---[ 741]---> BDD-cost:    5
c ---[ 740]---> BDD-cost:   25
c ---[ 739]---> BDD-cost:   47
c ---[ 737]---> BDD-cost:   13
c ---[ 736]---> BDD-cost:   13
c ---[ 735]---> BDD-cost:    5
c ---[ 734]---> BDD-cost:   39
c ---[ 733]---> BDD-cost:   23
c ---[ 732]---> BDD-cost:   47
c ---[ 731]---> BDD-cost:    5
c ---[ 730]---> BDD-cost:   13
c ---[ 729]---> BDD-cost:   25
c ---[ 728]---> BDD-cost:   47
c ---[ 726]---> BDD-cost:   47
c ---[ 725]---> BDD-cost:   47
c ---[ 724]---> BDD-cost:   47
c ---[ 723]---> BDD-cost:   47
c ---[ 722]---> BDD-cost:    7
c ---[ 721]---> BDD-cost:   13
c ---[ 720]---> BDD-cost:   47
c ---[ 719]---> BDD-cost:   47
c ---[ 718]---> BDD-cost:   39
c ---[ 717]---> BDD-cost:   47
c ---[ 715]---> BDD-cost:   47
c ---[ 714]---> BDD-cost:   43
c ---[ 713]---> BDD-cost:   43
c ---[ 712]---> BDD-cost:   47
c ---[ 711]---> BDD-cost:   47
c ---[ 710]---> BDD-cost:   43
c ---[ 709]---> BDD-cost:   43
c ---[ 708]---> BDD-cost:   47
c ---[ 707]---> BDD-cost:   47
c ---[ 706]---> BDD-cost:   13
c ---[ 704]---> BDD-cost:   13
c ---[ 703]---> BDD-cost:    7
c ---[ 702]---> BDD-cost:   43
c ---[ 701]---> BDD-cost:   43
c ---[ 700]---> BDD-cost:   47
c ---[ 699]---> BDD-cost:   47
c ---[ 698]---> BDD-cost:   13
c ---[ 697]---> BDD-cost:   13
c ---[ 696]---> BDD-cost:    7
c ---[ 695]---> BDD-cost:   47
c ---[ 693]---> BDD-cost:   47
c ---[ 692]---> BDD-cost:   47
c ---[ 691]---> BDD-cost:   13
c ---[ 690]---> BDD-cost:   13
c ---[ 687]---> BDD-cost:   43
c ---[ 686]---> BDD-cost:   43
c ---[ 685]---> BDD-cost:   13
c ---[ 684]---> BDD-cost:   13
c ---[ 683]---> BDD-cost: 5449
c ---[ 681]---> BDD-cost:   47
c ---[ 680]---> BDD-cost:    7
c ---[ 679]---> BDD-cost:   13
c ---[ 678]---> BDD-cost:    7
c ---[ 677]---> BDD-cost:   13
c ---[ 676]---> BDD-cost:    7
c ---[ 675]---> BDD-cost:   13
c ---[ 674]---> BDD-cost:   47
c ---[ 673]---> BDD-cost:   47
c ---[ 672]---> BDD-cost:   47
c ---[ 670]---> BDD-cost:   19
c ---[ 669]---> BDD-cost:   19
c ---[ 668]---> BDD-cost:   25
c ---[ 667]---> BDD-cost:    9
c ---[ 666]---> BDD-cost:    3
c ---[ 665]---> BDD-cost:   47
c ---[ 664]---> BDD-cost:   47
c ---[ 663]---> BDD-cost:    9
c ---[ 662]---> BDD-cost:   25
c ---[ 661]---> BDD-cost:   19
c ---[ 659]---> BDD-cost:   25
c ---[ 658]---> BDD-cost:   19
c ---[ 657]---> BDD-cost:   25
c ---[ 655]---> BDD-cost:   19
c ---[ 654]---> BDD-cost:   25
c ---[ 653]---> BDD-cost:   19
c ---[ 652]---> BDD-cost:   19
c ---[ 651]---> BDD-cost:   47
c ---[ 650]---> BDD-cost:   47
c ---[ 648]---> BDD-cost:   47
c ---[ 647]---> BDD-cost:   25
c ---[ 646]---> BDD-cost:   25
c ---[ 645]---> BDD-cost:   19
c ---[ 644]---> BDD-cost:   25
c ---[ 643]---> BDD-cost:   23
c ---[ 642]---> BDD-cost:   25
c ---[ 641]---> BDD-cost:   25
c ---[ 640]---> BDD-cost:   25
c ---[ 639]---> BDD-cost:   25
c ---[ 637]---> BDD-cost:   25
c ---[ 636]---> BDD-cost:   47
c ---[ 635]---> BDD-cost:   47
c ---[ 634]---> BDD-cost:   25
c ---[ 633]---> BDD-cost:   25
c ---[ 632]---> BDD-cost:   35
c ---[ 631]---> BDD-cost:   23
c ---[ 630]---> BDD-cost:   25
c ---[ 629]---> BDD-cost:   23
c ---[ 628]---> BDD-cost:   25
c ---[ 627]---> BDD-cost: 7382
c ---[ 626]---> BDD-cost:   25
c ---[ 625]---> BDD-cost:   25
c ---[ 624]---> BDD-cost:   23
c ---[ 623]---> BDD-cost:   25
c ---[ 622]---> BDD-cost:   23
c ---[ 621]---> BDD-cost:   47
c ---[ 620]---> BDD-cost:   23
c ---[ 619]---> BDD-cost:   47
c ---[ 618]---> BDD-cost:   23
c ---[ 617]---> BDD-cost:   23
c ---[ 616]---> BDD-cost:  960
c ---[ 615]---> BDD-cost:   25
c ---[ 614]---> BDD-cost:   25
c ---[ 613]---> BDD-cost:   25
c ---[ 612]---> BDD-cost:   19
c ---[ 611]---> BDD-cost:   25
c ---[ 610]---> BDD-cost:   47
c ---[ 609]---> BDD-cost:   39
c ---[ 608]---> BDD-cost:   25
c ---[ 607]---> BDD-cost:   19
c ---[ 606]---> BDD-cost:   43
c ---[ 604]---> BDD-cost:   47
c ---[ 603]---> BDD-cost:   43
c ---[ 602]---> BDD-cost:   47
c ---[ 601]---> BDD-cost:   19
c ---[ 600]---> BDD-cost:   25
c ---[ 599]---> BDD-cost:   35
c ---[ 598]---> BDD-cost:   25
c ---[ 597]---> BDD-cost:   19
c ---[ 596]---> BDD-cost:   13
c ---[ 595]---> BDD-cost:   13
c ---[ 593]---> BDD-cost:   43
c ---[ 592]---> BDD-cost:   25
c ---[ 591]---> BDD-cost:   19
c ---[ 590]---> BDD-cost:   13
c ---[ 589]---> BDD-cost:   13
c ---[ 587]---> BDD-cost:   19
c ---[ 586]---> BDD-cost:   25
c ---[ 585]---> BDD-cost:   13
c ---[ 584]---> BDD-cost:    5
c ---[ 582]---> BDD-cost:   13
c ---[ 581]---> BDD-cost:    5
c ---[ 580]---> BDD-cost:   13
c ---[ 579]---> BDD-cost:   39
c ---[ 578]---> BDD-cost:   39
c ---[ 577]---> BDD-cost:   35
c ---[ 576]---> BDD-cost:   13
c ---[ 575]---> BDD-cost:   23
c ---[ 574]---> BDD-cost:   23
c ---[ 569]---> BDD-cost:   25
c ---[ 568]---> BDD-cost:   19
c ---[ 567]---> BDD-cost:   19
c ---[ 566]---> BDD-cost:   19
c ---[ 565]---> BDD-cost:   47
c ---[ 564]---> BDD-cost:   47
c ---[ 563]---> BDD-cost:   11
c ---[ 562]---> BDD-cost:   47
c ---[ 561]---> BDD-cost:   47
c ---[ 560]---> BDD-cost: 9003
c ---[ 559]---> BDD-cost:   47
c ---[ 558]---> BDD-cost:   47
c ---[ 557]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:    9
c ---[ 555]---> BDD-cost:   19
c ---[ 554]---> BDD-cost:   19
c ---[ 553]---> BDD-cost:   25
c ---[ 552]---> BDD-cost:   13
c ---[ 551]---> BDD-cost:    9
c ---[ 550]---> BDD-cost:   19
c ---[ 549]---> BDD-cost: 8735
c ---[ 548]---> BDD-cost:   19
c ---[ 546]---> BDD-cost:   19
c ---[ 545]---> BDD-cost:   25
c ---[ 544]---> BDD-cost:   19
c ---[ 543]---> BDD-cost:   47
c ---[ 542]---> BDD-cost:   19
c ---[ 541]---> BDD-cost:   47
c ---[ 540]---> BDD-cost:   47
c ---[ 539]---> BDD-cost:   47
c ---[ 538]---> BDD-cost: 7408
c ---[ 537]---> BDD-cost:   11
c ---[ 536]---> BDD-cost:   19
c ---[ 535]---> BDD-cost:   25
c ---[ 534]---> BDD-cost:   25
c ---[ 533]---> BDD-cost:   25
c ---[ 532]---> BDD-cost:   19
c ---[ 531]---> BDD-cost:   25
c ---[ 530]---> BDD-cost:   19
c ---[ 529]---> BDD-cost:   25
c ---[ 528]---> BDD-cost:   19
c ---[ 526]---> BDD-cost:   25
c ---[ 525]---> BDD-cost:    9
c ---[ 524]---> BDD-cost:    9
c ---[ 523]---> BDD-cost:   47
c ---[ 522]---> BDD-cost:   47
c ---[ 521]---> BDD-cost:   47
c ---[ 520]---> BDD-cost:   47
c ---[ 519]---> BDD-cost:   23
c ---[ 518]---> BDD-cost:   19
c ---[ 517]---> BDD-cost:   47
c ---[ 515]---> BDD-cost:   39
c ---[ 514]---> BDD-cost:   47
c ---[ 513]---> BDD-cost:   47
c ---[ 512]---> BDD-cost:   47
c ---[ 511]---> BDD-cost:   47
c ---[ 510]---> BDD-cost:   39
c ---[ 509]---> BDD-cost:   47
c ---[ 508]---> BDD-cost:   47
c ---[ 507]---> BDD-cost:   39
c ---[ 506]---> BDD-cost:   39
c ---[ 505]---> BDD-cost:25076
c ---[ 504]---> BDD-cost:   47
c ---[ 503]---> BDD-cost:   39
c ---[ 502]---> BDD-cost:   47
c ---[ 501]---> BDD-cost:   47
c ---[ 500]---> BDD-cost:   47
c ---[ 499]---> BDD-cost:   47
c ---[ 498]---> BDD-cost:   47
c ---[ 497]---> BDD-cost:   47
c ---[ 496]---> BDD-cost:   11
c ---[ 495]---> BDD-cost:   25
c ---[ 493]---> BDD-cost:    3
c ---[ 492]---> BDD-cost:   25
c ---[ 491]---> BDD-cost:   19
c ---[ 490]---> BDD-cost:   13
c ---[ 489]---> BDD-cost:    3
c ---[ 488]---> BDD-cost:   19
c ---[ 487]---> BDD-cost:   25
c ---[ 486]---> BDD-cost:   11
c ---[ 485]---> BDD-cost:   25
c ---[ 484]---> BDD-cost:   47
c ---[ 482]---> BDD-cost:   25
c ---[ 481]---> BDD-cost:   47
c ---[ 480]---> BDD-cost:   25
c ---[ 479]---> BDD-cost:   47
c ---[ 478]---> BDD-cost:   47
c ---[ 477]---> BDD-cost:    7
c ---[ 476]---> BDD-cost:   25
c ---[ 475]---> BDD-cost:   25
c ---[ 474]---> BDD-cost:   25
c ---[ 473]---> BDD-cost:   25
c ---[ 471]---> BDD-cost:   25
c ---[ 470]---> BDD-cost:   19
c ---[ 469]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:    3
c ---[ 467]---> BDD-cost:   25
c ---[ 466]---> BDD-cost:   47
c ---[ 465]---> BDD-cost:   47
c ---[ 464]---> BDD-cost:   19
c ---[ 463]---> BDD-cost:   23
c ---[ 462]---> BDD-cost:   43
c ---[ 459]---> BDD-cost:   47
c ---[ 458]---> BDD-cost:   47
c ---[ 457]---> BDD-cost:   43
c ---[ 456]---> BDD-cost:   47
c ---[ 455]---> BDD-cost:   47
c ---[ 454]---> BDD-cost:   43
c ---[ 453]---> BDD-cost:   47
c ---[ 452]---> BDD-cost:   47
c ---[ 451]---> BDD-cost:   47
c ---[ 450]---> BDD-cost:   43
c ---[ 449]---> Adder-cost: 2679   maxlim: 22   bits: 6/5
c ---[ 448]---> BDD-cost:   43
c ---[ 447]---> BDD-cost:   47
c ---[ 446]---> BDD-cost:   47
c ---[ 445]---> BDD-cost:   43
c ---[ 444]---> BDD-cost:   47
c ---[ 443]---> BDD-cost:   47
c ---[ 442]---> BDD-cost:   47
c ---[ 441]---> BDD-cost:   47
c ---[ 440]---> BDD-cost:   47
c ---[ 439]---> BDD-cost:   23
c ---[ 438]---> BDD-cost: 3640
c ---[ 437]---> BDD-cost:   19
c ---[ 436]---> BDD-cost:   47
c ---[ 435]---> BDD-cost:   47
c ---[ 434]---> BDD-cost:   43
c ---[ 433]---> BDD-cost:   47
c ---[ 432]---> BDD-cost:   47
c ---[ 431]---> BDD-cost:   43
c ---[ 430]---> BDD-cost:   47
c ---[ 429]---> BDD-cost:   47
c ---[ 428]---> BDD-cost:   43
c ---[ 426]---> BDD-cost:   47
c ---[ 425]---> BDD-cost:   47
c ---[ 424]---> BDD-cost:   47
c ---[ 423]---> BDD-cost:   47
c ---[ 422]---> BDD-cost:   47
c ---[ 421]---> BDD-cost:   43
c ---[ 420]---> BDD-cost:   47
c ---[ 419]---> BDD-cost:   43
c ---[ 418]---> BDD-cost:   43
c ---[ 417]---> BDD-cost:   43
c ---[ 415]---> BDD-cost:   43
c ---[ 414]---> BDD-cost:   23
c ---[ 413]---> BDD-cost:   19
c ---[ 412]---> BDD-cost:   43
c ---[ 411]---> BDD-cost:   47
c ---[ 410]---> BDD-cost:   47
c ---[ 409]---> BDD-cost:   43
c ---[ 408]---> BDD-cost:   47
c ---[ 407]---> BDD-cost:   43
c ---[ 406]---> BDD-cost:   47
c ---[ 404]---> BDD-cost:   43
c ---[ 403]---> BDD-cost:   47
c ---[ 402]---> BDD-cost:   47
c ---[ 401]---> BDD-cost:   47
c ---[ 400]---> BDD-cost:   47
c ---[ 399]---> BDD-cost:   47
c ---[ 398]---> BDD-cost:   25
c ---[ 397]---> BDD-cost:    9
c ---[ 396]---> BDD-cost:   19
c ---[ 395]---> BDD-cost:   25
c ---[ 393]---> BDD-cost:   19
c ---[ 392]---> BDD-cost:   25
c ---[ 391]---> BDD-cost:   13
c ---[ 390]---> BDD-cost:    9
c ---[ 389]---> BDD-cost:   19
c ---[ 388]---> BDD-cost:   25
c ---[ 387]---> BDD-cost:   19
c ---[ 386]---> BDD-cost:   19
c ---[ 385]---> BDD-cost:   25
c ---[ 384]---> BDD-cost:   19
c ---[ 382]---> BDD-cost:   47
c ---[ 381]---> BDD-cost:   19
c ---[ 380]---> BDD-cost:   47
c ---[ 379]---> BDD-cost:   47
c ---[ 378]---> BDD-cost:   47
c ---[ 377]---> BDD-cost:   11
c ---[ 376]---> BDD-cost:   19
c ---[ 375]---> BDD-cost:   25
c ---[ 374]---> BDD-cost:   25
c ---[ 373]---> BDD-cost:   25
c ---[ 371]---> BDD-cost:   19
c ---[ 370]---> BDD-cost:   25
c ---[ 369]---> BDD-cost:   19
c ---[ 368]---> BDD-cost:   25
c ---[ 367]---> BDD-cost:   19
c ---[ 366]---> BDD-cost:   25
c ---[ 365]---> BDD-cost:    9
c ---[ 364]---> BDD-cost:    9
c ---[ 363]---> BDD-cost:   25
c ---[ 362]---> BDD-cost:   35
c ---[ 360]---> BDD-cost:   35
c ---[ 359]---> BDD-cost:   25
c ---[ 358]---> BDD-cost:   35
c ---[ 357]---> BDD-cost:   35
c ---[ 356]---> BDD-cost:   35
c ---[ 355]---> BDD-cost:   25
c ---[ 354]---> BDD-cost:   35
c ---[ 353]---> BDD-cost:   43
c ---[ 352]---> BDD-cost:   43
c ---[ 351]---> BDD-cost:   43
c ---[ 350]---> BDD-cost:11166
c ---[ 348]---> BDD-cost:   43
c ---[ 347]---> BDD-cost:   43
c ---[ 346]---> BDD-cost:   43
c ---[ 345]---> BDD-cost:   25
c ---[ 344]---> BDD-cost:   13
c ---[ 343]---> BDD-cost:   35
c ---[ 342]---> BDD-cost:   35
c ---[ 341]---> BDD-cost:   35
c ---[ 340]---> BDD-cost:   35
c ---[ 339]---> BDD-cost:   35
c ---[ 337]---> BDD-cost:   25
c ---[ 336]---> BDD-cost:   35
c ---[ 335]---> BDD-cost:   25
c ---[ 334]---> BDD-cost:   25
c ---[ 333]---> BDD-cost:   19
c ---[ 332]---> BDD-cost:   25
c ---[ 331]---> BDD-cost:   19
c ---[ 330]---> BDD-cost:   25
c ---[ 329]---> BDD-cost:   47
c ---[ 328]---> BDD-cost:   25
c ---[ 326]---> BDD-cost:   47
c ---[ 325]---> BDD-cost:   47
c ---[ 324]---> BDD-cost:   25
c ---[ 323]---> BDD-cost:   25
c ---[ 322]---> BDD-cost:   25
c ---[ 321]---> BDD-cost:   19
c ---[ 319]---> BDD-cost:   13
c ---[ 318]---> BDD-cost:   13
c ---[ 317]---> BDD-cost:   43
c ---[ 316]---> BDD-cost: 4990
c ---[ 314]---> BDD-cost:   13
c ---[ 313]---> BDD-cost:   13
c ---[ 312]---> BDD-cost:    7
c ---[ 311]---> BDD-cost:   13
c ---[ 310]---> BDD-cost:   13
c ---[ 309]---> BDD-cost:   13
c ---[ 308]---> BDD-cost:   13
c ---[ 307]---> BDD-cost:   39
c ---[ 306]---> BDD-cost:   39
c ---[ 305]---> BDD-cost:10657
c ---[ 304]---> BDD-cost:   35
c ---[ 303]---> BDD-cost:   23
c ---[ 302]---> BDD-cost:   23
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 299]---> BDD-cost:    9
c ---[ 298]---> BDD-cost:   25
c ---[ 297]---> BDD-cost:   19
c ---[ 296]---> BDD-cost:   19
c ---[ 295]---> BDD-cost:   19
c ---[ 294]---> BDD-cost:12172
c ---[ 293]---> BDD-cost:   47
c ---[ 292]---> BDD-cost:   25
c ---[ 291]---> BDD-cost:   19
c ---[ 290]---> BDD-cost:   13
c ---[ 289]---> BDD-cost:   13
c ---[ 287]---> BDD-cost:   19
c ---[ 286]---> BDD-cost:   25
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost: 8229
c ---[ 282]---> BDD-cost:    5
c ---[ 281]---> BDD-cost:    5
c ---[ 280]---> BDD-cost:   39
c ---[ 279]---> BDD-cost:   47
c ---[ 278]---> BDD-cost:   35
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 275]---> BDD-cost:   23
c ---[ 274]---> BDD-cost:   13
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost: 4792
c ---[ 271]---> BDD-cost:   13
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:   13
c ---[ 268]---> BDD-cost:   25
c ---[ 267]---> BDD-cost:   19
c ---[ 266]---> BDD-cost:   19
c ---[ 265]---> BDD-cost:   13
c ---[ 264]---> BDD-cost:   43
c ---[ 263]---> BDD-cost:   47
c ---[ 262]---> BDD-cost:   43
c ---[ 261]---> BDD-cost: 8472
c ---[ 260]---> BDD-cost:   43
c ---[ 259]---> BDD-cost:   35
c ---[ 258]---> BDD-cost:   43
c ---[ 257]---> BDD-cost:   47
c ---[ 256]---> BDD-cost:   43
c ---[ 255]---> BDD-cost:   13
c ---[ 254]---> BDD-cost:   19
c ---[ 253]---> BDD-cost:   25
c ---[ 252]---> BDD-cost:    9
c ---[ 251]---> BDD-cost:   25
c ---[ 250]---> BDD-cost: 2697
c ---[ 249]---> BDD-cost:   19
c ---[ 248]---> BDD-cost:   47
c ---[ 247]---> BDD-cost:   25
c ---[ 246]---> BDD-cost:   47
c ---[ 245]---> BDD-cost:   25
c ---[ 244]---> BDD-cost:   47
c ---[ 243]---> BDD-cost:   47
c ---[ 242]---> BDD-cost:    7
c ---[ 241]---> BDD-cost:   25
c ---[ 240]---> BDD-cost:   25
c ---[ 238]---> BDD-cost: 2179
c ---[ 237]---> BDD-cost:   25
c ---[ 236]---> BDD-cost:   25
c ---[ 235]---> BDD-cost:   19
c ---[ 234]---> BDD-cost:   25
c ---[ 233]---> BDD-cost:   25
c ---[ 232]---> BDD-cost:   19
c ---[ 229]---> BDD-cost:   25
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost: 1419
c ---[ 226]---> BDD-cost:   13
c ---[ 225]---> BDD-cost:   19
c ---[ 224]---> BDD-cost:    9
c ---[ 223]---> BDD-cost:   13
c ---[ 222]---> BDD-cost:   13
c ---[ 221]---> BDD-cost:   13
c ---[ 220]---> BDD-cost:   13
c ---[ 219]---> BDD-cost:   39
c ---[ 218]---> BDD-cost:   39
c ---[ 217]---> BDD-cost:   35
c ---[ 216]---> BDD-cost:15660
c ---[ 215]---> BDD-cost:   23
c ---[ 214]---> BDD-cost:   23
c ---[ 213]---> BDD-cost:   13
c ---[ 212]---> BDD-cost:   13
c ---[ 211]---> BDD-cost:   13
c ---[ 210]---> BDD-cost:   25
c ---[ 209]---> BDD-cost:   19
c ---[ 208]---> BDD-cost:   19
c ---[ 207]---> BDD-cost:   19
c ---[ 206]---> BDD-cost:   19
c ---[ 205]---> BDD-cost: 1442
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   13
c ---[ 202]---> BDD-cost:    5
c ---[ 201]---> BDD-cost:    7
c ---[ 200]---> BDD-cost:    5
c ---[ 199]---> BDD-cost:    7
c ---[ 198]---> BDD-cost:   47
c ---[ 197]---> BDD-cost:   39
c ---[ 196]---> BDD-cost:   13
c ---[ 195]---> BDD-cost:   13
c ---[ 193]---> BDD-cost:   25
c ---[ 192]---> BDD-cost:   23
c ---[ 191]---> BDD-cost:   13
c ---[ 190]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:   13
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:   13
c ---[ 186]---> BDD-cost:    5
c ---[ 185]---> BDD-cost:   19
c ---[ 184]---> BDD-cost:   19
c ---[ 182]---> BDD-cost:   19
c ---[ 181]---> BDD-cost:   47
c ---[ 180]---> BDD-cost:   47
c ---[ 179]---> BDD-cost:   47
c ---[ 178]---> BDD-cost:   25
c ---[ 177]---> BDD-cost:   25
c ---[ 176]---> BDD-cost:   19
c ---[ 175]---> BDD-cost:   25
c ---[ 174]---> BDD-cost:    9
c ---[ 173]---> BDD-cost:   13
c ---[ 171]---> BDD-cost:   13
c ---[ 170]---> BDD-cost:   39
c ---[ 169]---> BDD-cost:   39
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   23
c ---[ 166]---> BDD-cost:   13
c ---[ 165]---> BDD-cost:   25
c ---[ 164]---> BDD-cost:   19
c ---[ 163]---> BDD-cost:   39
c ---[ 162]---> BDD-cost:   39
c ---[ 160]---> BDD-cost:   43
c ---[ 159]---> BDD-cost:   43
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   13
c ---[ 156]---> BDD-cost:   47
c ---[ 155]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:    5
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:    5
c ---[ 151]---> BDD-cost:   13
c ---[ 149]---> BDD-cost:    5
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   47
c ---[ 146]---> BDD-cost:   25
c ---[ 145]---> BDD-cost:   19
c ---[ 144]---> BDD-cost:   47
c ---[ 143]---> BDD-cost:   39
c ---[ 142]---> BDD-cost:   39
c ---[ 141]---> BDD-cost:   47
c ---[ 140]---> BDD-cost:   23
c ---[ 138]---> BDD-cost:    5
c ---[ 137]---> BDD-cost:   13
c ---[ 136]---> BDD-cost:   47
c ---[ 135]---> BDD-cost:   25
c ---[ 134]---> BDD-cost:   43
c ---[ 133]---> BDD-cost:   43
c ---[ 132]---> BDD-cost:   39
c ---[ 131]---> BDD-cost:   39
c ---[ 130]---> BDD-cost:   47
c ---[ 129]---> BDD-cost:   39
c ---[ 128]---> BDD-cost:  526
c ---[ 127]---> BDD-cost: 6314
c ---[ 126]---> Adder-cost: 1713   maxlim: 4   bits: 4/3
c ---[ 125]---> BDD-cost: 5010
c ---[ 124]---> BDD-cost: 5984
c ---[ 123]---> BDD-cost: 6429
c ---[ 122]---> Adder-cost: 3066   maxlim: 6   bits: 4/3
c ---[ 121]---> Adder-cost: 8437   maxlim: 19   bits: 6/5
c ---[ 120]---> Adder-cost: 5125   maxlim: 18   bits: 6/5
c ---[ 119]---> Adder-cost: 1599   maxlim: 14   bits: 5/4
c ---[ 118]---> BDD-cost: 2172
c ---[ 117]---> BDD-cost:24906
c ---[ 116]---> Adder-cost: 885   maxlim: 12   bits: 5/4
c ---[ 115]---> BDD-cost: 2276
c ---[ 114]---> Adder-cost: 4102   maxlim: 9   bits: 5/4
c ---[ 113]---> BDD-cost: 2122
c ---[ 112]---> BDD-cost: 1446
c ---[ 111]---> BDD-cost:   44
c ---[ 110]---> BDD-cost: 6226
c ---[ 109]---> BDD-cost:  502
c ---[ 108]---> BDD-cost:  698
c ---[ 107]---> BDD-cost:  636
c ---[ 106]---> BDD-cost:  610
c ---[ 105]---> BDD-cost:   98
c ---[ 104]---> BDD-cost:  156
c ---[ 103]---> BDD-cost:  906
c ---[ 102]---> BDD-cost: 1270
c ---[ 101]---> BDD-cost: 1320
c ---[ 100]---> BDD-cost: 1876
c ---[  99]---> BDD-cost: 1098
c ---[  98]---> BDD-cost:  282
c ---[  97]---> BDD-cost:  230
c ---[  96]---> BDD-cost: 2814
c ---[  95]---> BDD-cost:  536
c ---[  94]---> BDD-cost: 2014
c ---[  93]---> BDD-cost: 1536
c ---[  92]---> BDD-cost: 4626
c ---[  91]---> BDD-cost: 3914
c ---[  90]---> BDD-cost: 3507
c ---[  89]---> BDD-cost:  217
c ---[  88]---> BDD-cost:12956
c ---[  87]---> BDD-cost: 1560
c ---[  86]---> BDD-cost: 2409
c ---[  85]---> BDD-cost: 2574
c ---[  84]---> BDD-cost: 1288
c ---[  83]---> BDD-cost:  279
c ---[  82]---> BDD-cost:  492
c ---[  81]---> BDD-cost:  775
c ---[  80]---> BDD-cost:  990
c ---[  79]---> BDD-cost: 1408
c ---[  78]---> BDD-cost:10070
c ---[  77]---> BDD-cost:  168
c ---[  76]---> BDD-cost: 4857
c ---[  75]---> BDD-cost: 3908
c ---[  74]---> BDD-cost: 3531
c ---[  73]---> BDD-cost: 1209
c ---[  72]---> BDD-cost:  468
c ---[  71]---> BDD-cost: 4718
c ---[  70]---> BDD-cost:  770
c ---[  69]---> BDD-cost: 3641
c ---[  68]---> BDD-cost:  748
c ---[  67]---> BDD-cost: 2696
c ---[  66]---> BDD-cost: 1134
c ---[  65]---> BDD-cost:  540
c ---[  64]---> BDD-cost:  100
c ---[  63]---> BDD-cost:  628
c ---[  62]---> BDD-cost:  494
c ---[  61]---> BDD-cost:  270
c ---[  60]---> BDD-cost:  326
c ---[  59]---> BDD-cost:  606
c ---[  58]---> BDD-cost:10995
c ---[  57]---> BDD-cost: 1283
c ---[  56]---> BDD-cost: 6499
c ---[  55]---> BDD-cost:  569
c ---[  54]---> BDD-cost:  657
c ---[  53]---> BDD-cost:  958
c ---[  52]---> BDD-cost:   88
c ---[  51]---> BDD-cost: 1082
c ---[  50]---> BDD-cost:  462
c ---[  49]---> BDD-cost: 1905
c ---[  48]---> BDD-cost:  297
c ---[  47]---> BDD-cost: 1018
c ---[  46]---> BDD-cost: 7706
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:  266
c ---[  43]---> BDD-cost:  148
c ---[  42]---> BDD-cost:  104
c ---[  41]---> BDD-cost: 1267
c ---[  40]---> Adder-cost: 7122   maxlim: 24   bits: 6/5
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost: 1432
c ---[  37]---> BDD-cost:  532
c ---[  36]---> BDD-cost:  182
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:  106
c ---[  33]---> BDD-cost:  166
c ---[  32]---> BDD-cost: 1536
c ---[  31]---> BDD-cost:  498
c ---[  30]---> BDD-cost: 1740
c ---[  29]---> BDD-cost:  492
c ---[  28]---> BDD-cost:  844
c ---[  27]---> BDD-cost:  212
c ---[  26]---> BDD-cost: 2544
c ---[  25]---> BDD-cost:    2
c ---[  24]---> BDD-cost: 2508
c ---[  23]---> BDD-cost:  330
c ---[  22]---> BDD-cost:  278
c ---[  21]---> BDD-cost: 2578
c ---[  20]---> BDD-cost: 2470
c ---[  19]---> BDD-cost: 3216
c ---[  18]---> BDD-cost:   51
c ---[  17]---> BDD-cost: 3862
c ---[  16]---> BDD-cost:  384
c ---[  15]---> BDD-cost:  423
c ---[  14]---> BDD-cost:  884
c ---[  13]---> BDD-cost:  778
c ---[  12]---> BDD-cost: 1398
c ---[  11]---> BDD-cost: 1234
c ---[  10]---> BDD-cost: 1820
c ---[   9]---> BDD-cost: 1756
c ---[   8]---> BDD-cost: 2370
c ---[   7]---> BDD-cost: 2110
c ---[   6]---> BDD-cost: 2142
c ---[   5]---> BDD-cost: 2646
c ---[   4]---> BDD-cost: 3906
c ---[   3]---> BDD-cost: 5663
c ---[   2]---> Adder-cost: 3775   maxlim: 7   bits: 4/3
c ---[   1]---> Adder-cost: 2539   maxlim: 7   bits: 4/3
c ---[   0]---> BDD-cost: 3822
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1641296  5477960 |  547098       0        0     nan |  0.000 % |
c |       100 | 1641296  5477960 |  601807     100      305     3.0 |  0.187 % |
c |       250 | 1641281  5477915 |  661988     245      799     3.3 |  0.187 % |
c |       475 | 1641165  5477573 |  728187     411     1411     3.4 |  0.192 % |
c |       812 | 1641078  5477318 |  801006     711     2573     3.6 |  0.196 % |
c |      1318 | 1640821  5476541 |  881106    1080     4461     4.1 |  0.210 % |
c |      2077 | 1640660  5476074 |  969217    1771     7550     4.3 |  0.219 % |
c |      3217 | 1640329  5475119 | 1066139    2813    14837     5.3 |  0.238 % |
c |      4925 | 1640228  5474830 | 1172753    4460    46290    10.4 |  0.243 % |
c |      7487 | 1639982  5474094 | 1290028    6892    64380     9.3 |  0.255 % |
c |     11331 | 1639853  5473673 | 1419031   10713   113965    10.6 |  0.259 % |
c |     17098 | 1639490  5472578 | 1560934   16280   163277    10.0 |  0.279 % |
c |     25747 | 1639244  5471836 | 1717027   24614   255396    10.4 |  0.292 % |
c |     38722 | 1638623  5469961 | 1888730   37383   390294    10.4 |  0.325 % |
c |     58184 | 1638051  5468161 | 2077603   56593   606784    10.7 |  0.349 % |
c |     87376 | 1637527  5466553 | 2285364   85514   979001    11.4 |  0.376 % |
#### 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.86 0.94 0.96 2/54 30502
Raw data (stat): 30502 (runsolver) R 30501 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482152864 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0006 s]
Raw data (loadavg): 0.88 0.95 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 16533 0 0 0 959 39 0 0 25 0 1 0 482152864 62656512 13299 4294967295 134512640 134672761 3221224624 3221222192 134523717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15297 13299 603 41 0 15256 0
vsize: 61188
[startup+20.0012 s]
Raw data (loadavg): 0.90 0.95 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 52257 0 0 0 1874 124 0 0 25 0 1 0 482152864 236441600 47612 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57725 47612 603 41 0 57684 0
vsize: 230900
[startup+30.0014 s]
Raw data (loadavg): 0.91 0.95 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 53350 0 0 0 2872 127 0 0 25 0 1 0 482152864 240902144 48705 4294967295 134512640 134672761 3221224624 3221223796 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58814 48705 603 41 0 58773 0
vsize: 235256
[startup+40.0017 s]
Raw data (loadavg): 0.93 0.95 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 53890 0 0 0 3870 128 0 0 25 0 1 0 482152864 243064832 49245 4294967295 134512640 134672761 3221224624 3221223804 134556674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59342 49245 603 41 0 59301 0
vsize: 237368
[startup+50.0015 s]
Raw data (loadavg): 0.94 0.95 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 54277 0 0 0 4870 128 0 0 25 0 1 0 482152864 244686848 49632 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59738 49632 603 41 0 59697 0
vsize: 238952
[startup+60.0027 s]
Raw data (loadavg): 0.95 0.95 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 54569 0 0 0 5869 129 0 0 25 0 1 0 482152864 245903360 49924 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60035 49924 603 41 0 59994 0
vsize: 240140
[startup+70.003 s]
Raw data (loadavg): 0.95 0.95 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 54930 0 0 0 6868 130 0 0 25 0 1 0 482152864 247255040 50285 4294967295 134512640 134672761 3221224624 3221223796 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60365 50285 603 41 0 60324 0
vsize: 241460
[startup+80.0028 s]
Raw data (loadavg): 0.96 0.95 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 55069 0 0 0 7868 130 0 0 25 0 1 0 482152864 247795712 50424 4294967295 134512640 134672761 3221224624 3221223808 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60497 50424 603 41 0 60456 0
vsize: 241988
[startup+90.0031 s]
Raw data (loadavg): 0.97 0.95 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 55107 0 0 0 8868 131 0 0 25 0 1 0 482152864 247930880 50462 4294967295 134512640 134672761 3221224624 3221223816 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60530 50462 603 41 0 60489 0
vsize: 242120
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 55240 0 0 0 9868 131 0 0 25 0 1 0 482152864 248471552 50595 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60662 50595 603 41 0 60621 0
vsize: 242648
[startup+110.004 s]
Raw data (loadavg): 0.98 0.95 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 55310 0 0 0 10868 131 0 0 25 0 1 0 482152864 248741888 50665 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60728 50665 603 41 0 60687 0
vsize: 242912
[startup+120.006 s]
Raw data (loadavg): 0.98 0.96 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 55376 0 0 0 11868 131 0 0 25 0 1 0 482152864 249008128 50731 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60793 50731 603 41 0 60752 0
vsize: 243172
[startup+130.006 s]
Raw data (loadavg): 0.98 0.96 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 55705 0 0 0 12867 133 0 0 25 0 1 0 482152864 250335232 51060 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61117 51060 603 41 0 61076 0
vsize: 244468
[startup+140.005 s]
Raw data (loadavg): 0.98 0.96 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 55825 0 0 0 13866 133 0 0 25 0 1 0 482152864 250740736 51180 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61216 51180 603 41 0 61175 0
vsize: 244864
[startup+150.007 s]
Raw data (loadavg): 0.99 0.96 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 55916 0 0 0 14866 134 0 0 25 0 1 0 482152864 251146240 51271 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61315 51271 603 41 0 61274 0
vsize: 245260
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 55951 0 0 0 15866 134 0 0 25 0 1 0 482152864 251281408 51306 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61348 51306 603 41 0 61307 0
vsize: 245392
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 55993 0 0 0 16866 134 0 0 25 0 1 0 482152864 251416576 51348 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61381 51348 603 41 0 61340 0
vsize: 245524
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56096 0 0 0 17865 135 0 0 25 0 1 0 482152864 251830272 51451 4294967295 134512640 134672761 3221224624 3221223792 134553595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61482 51451 603 41 0 61441 0
vsize: 245928
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56113 0 0 0 18865 135 0 0 25 0 1 0 482152864 251830272 51468 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61482 51468 603 41 0 61441 0
vsize: 245928
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56143 0 0 0 19865 135 0 0 25 0 1 0 482152864 251965440 51498 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61515 51498 603 41 0 61474 0
vsize: 246060
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56156 0 0 0 20865 135 0 0 25 0 1 0 482152864 252100608 51511 4294967295 134512640 134672761 3221224624 3221223760 134566155 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61548 51511 603 41 0 61507 0
vsize: 246192
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56204 0 0 0 21865 136 0 0 25 0 1 0 482152864 252100608 51559 4294967295 134512640 134672761 3221224624 3221223776 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61548 51559 603 41 0 61507 0
vsize: 246192
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56231 0 0 0 22865 136 0 0 25 0 1 0 482152864 252235776 51586 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61581 51586 603 41 0 61540 0
vsize: 246324
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56238 0 0 0 23865 136 0 0 25 0 1 0 482152864 252235776 51593 4294967295 134512640 134672761 3221224624 3221223748 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61581 51593 603 41 0 61540 0
vsize: 246324
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56257 0 0 0 24864 137 0 0 25 0 1 0 482152864 252370944 51612 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61614 51612 603 41 0 61573 0
vsize: 246456
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56271 0 0 0 25864 137 0 0 25 0 1 0 482152864 252370944 51626 4294967295 134512640 134672761 3221224624 3221223824 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61614 51626 603 41 0 61573 0
vsize: 246456
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56280 0 0 0 26864 137 0 0 25 0 1 0 482152864 252370944 51635 4294967295 134512640 134672761 3221224624 3221223792 134564464 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61614 51635 603 41 0 61573 0
vsize: 246456
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56317 0 0 0 27864 138 0 0 25 0 1 0 482152864 252506112 51672 4294967295 134512640 134672761 3221224624 3221223792 134564705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61647 51672 603 41 0 61606 0
vsize: 246588
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56323 0 0 0 28863 139 0 0 25 0 1 0 482152864 252506112 51678 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61647 51678 603 41 0 61606 0
vsize: 246588
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56346 0 0 0 29863 139 0 0 25 0 1 0 482152864 252776448 51701 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61713 51701 603 41 0 61672 0
vsize: 246852
[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56364 0 0 0 30864 140 0 0 25 0 1 0 482152864 252776448 51719 4294967295 134512640 134672761 3221224624 3221223748 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61713 51719 603 41 0 61672 0
vsize: 246852
[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56377 0 0 0 31863 140 0 0 25 0 1 0 482152864 252776448 51732 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61713 51732 603 41 0 61672 0
vsize: 246852
[startup+330.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56446 0 0 0 32863 140 0 0 25 0 1 0 482152864 253046784 51801 4294967295 134512640 134672761 3221224624 3221223792 134561415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61779 51801 603 41 0 61738 0
vsize: 247116
[startup+340.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56465 0 0 0 33863 140 0 0 25 0 1 0 482152864 253181952 51820 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61812 51820 603 41 0 61771 0
vsize: 247248
[startup+350.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56480 0 0 0 34863 141 0 0 25 0 1 0 482152864 253181952 51835 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61812 51835 603 41 0 61771 0
vsize: 247248
[startup+360.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56509 0 0 0 35863 141 0 0 25 0 1 0 482152864 253317120 51864 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61845 51864 603 41 0 61804 0
vsize: 247380
[startup+370.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56521 0 0 0 36862 142 0 0 25 0 1 0 482152864 253317120 51876 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61845 51876 603 41 0 61804 0
vsize: 247380
[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56531 0 0 0 37862 142 0 0 25 0 1 0 482152864 253452288 51886 4294967295 134512640 134672761 3221224624 3221223776 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61878 51886 603 41 0 61837 0
vsize: 247512
[startup+390.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56540 0 0 0 38862 142 0 0 25 0 1 0 482152864 253452288 51895 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61878 51895 603 41 0 61837 0
vsize: 247512
[startup+400.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56546 0 0 0 39862 143 0 0 25 0 1 0 482152864 253452288 51901 4294967295 134512640 134672761 3221224624 3221223792 134564729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61878 51901 603 41 0 61837 0
vsize: 247512
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56591 0 0 0 40862 143 0 0 25 0 1 0 482152864 253587456 51946 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61911 51946 603 41 0 61870 0
vsize: 247644
[startup+420.025 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56621 0 0 0 41861 143 0 0 25 0 1 0 482152864 253722624 51976 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61944 51976 603 41 0 61903 0
vsize: 247776
[startup+430.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56635 0 0 0 42861 144 0 0 25 0 1 0 482152864 253857792 51990 4294967295 134512640 134672761 3221224624 3221223748 134566040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61977 51990 603 41 0 61936 0
vsize: 247908
[startup+440.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56650 0 0 0 43861 144 0 0 25 0 1 0 482152864 253857792 52005 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61977 52005 603 41 0 61936 0
vsize: 247908
[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56668 0 0 0 44861 144 0 0 25 0 1 0 482152864 253992960 52023 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62010 52023 603 41 0 61969 0
vsize: 248040
[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56718 0 0 0 45861 144 0 0 25 0 1 0 482152864 254255104 52073 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62074 52073 603 41 0 62033 0
vsize: 248296
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56719 0 0 0 46861 144 0 0 25 0 1 0 482152864 254255104 52074 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62074 52074 603 41 0 62033 0
vsize: 248296
[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56722 0 0 0 47861 145 0 0 25 0 1 0 482152864 254255104 52077 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62074 52077 603 41 0 62033 0
vsize: 248296
[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56740 0 0 0 48861 145 0 0 25 0 1 0 482152864 254390272 52095 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62107 52095 603 41 0 62066 0
vsize: 248428
[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56751 0 0 0 49861 145 0 0 25 0 1 0 482152864 254390272 52106 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62107 52106 603 41 0 62066 0
vsize: 248428
[startup+510.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56766 0 0 0 50861 145 0 0 25 0 1 0 482152864 254390272 52121 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62107 52121 603 41 0 62066 0
vsize: 248428
[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56794 0 0 0 51861 146 0 0 25 0 1 0 482152864 254525440 52149 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62140 52149 603 41 0 62099 0
vsize: 248560
[startup+530.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56829 0 0 0 52860 146 0 0 25 0 1 0 482152864 254525440 52184 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62140 52184 603 41 0 62099 0
vsize: 248560
[startup+540.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56847 0 0 0 53861 146 0 0 25 0 1 0 482152864 254660608 52202 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62173 52202 603 41 0 62132 0
vsize: 248692
[startup+550.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56857 0 0 0 54860 146 0 0 25 0 1 0 482152864 254660608 52212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62173 52212 603 41 0 62132 0
vsize: 248692
[startup+560.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56866 0 0 0 55861 146 0 0 25 0 1 0 482152864 254795776 52221 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62206 52221 603 41 0 62165 0
vsize: 248824
[startup+570.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56929 0 0 0 56860 147 0 0 25 0 1 0 482152864 254930944 52284 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62239 52284 603 41 0 62198 0
vsize: 248956
[startup+580.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56941 0 0 0 57860 147 0 0 25 0 1 0 482152864 255066112 52296 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62272 52296 603 41 0 62231 0
vsize: 249088
[startup+590.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56961 0 0 0 58860 148 0 0 25 0 1 0 482152864 255066112 52316 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62272 52316 603 41 0 62231 0
vsize: 249088
[startup+600.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56982 0 0 0 59860 148 0 0 25 0 1 0 482152864 255201280 52337 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62305 52337 603 41 0 62264 0
vsize: 249220
[startup+610.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 56996 0 0 0 60860 148 0 0 25 0 1 0 482152864 255201280 52351 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62305 52351 603 41 0 62264 0
vsize: 249220
[startup+620.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57010 0 0 0 61859 149 0 0 25 0 1 0 482152864 255336448 52365 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62338 52365 603 41 0 62297 0
vsize: 249352
[startup+630.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57020 0 0 0 62859 149 0 0 25 0 1 0 482152864 255336448 52375 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62338 52375 603 41 0 62297 0
vsize: 249352
[startup+640.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57026 0 0 0 63859 149 0 0 25 0 1 0 482152864 255336448 52381 4294967295 134512640 134672761 3221224624 3221223748 134566073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62338 52381 603 41 0 62297 0
vsize: 249352
[startup+650.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57037 0 0 0 64859 149 0 0 25 0 1 0 482152864 255336448 52392 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62338 52392 603 41 0 62297 0
vsize: 249352
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57048 0 0 0 65859 149 0 0 25 0 1 0 482152864 255471616 52403 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62371 52403 603 41 0 62330 0
vsize: 249484
[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57068 0 0 0 66859 150 0 0 25 0 1 0 482152864 255471616 52423 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62371 52423 603 41 0 62330 0
vsize: 249484
[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57075 0 0 0 67858 150 0 0 25 0 1 0 482152864 255471616 52430 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62371 52430 603 41 0 62330 0
vsize: 249484
[startup+690.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57085 0 0 0 68858 151 0 0 25 0 1 0 482152864 255606784 52440 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62404 52440 603 41 0 62363 0
vsize: 249616
[startup+700.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57097 0 0 0 69858 151 0 0 25 0 1 0 482152864 255606784 52452 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62404 52452 603 41 0 62363 0
vsize: 249616
[startup+710.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57106 0 0 0 70858 151 0 0 25 0 1 0 482152864 255606784 52461 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62404 52461 603 41 0 62363 0
vsize: 249616
[startup+720.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57148 0 0 0 71858 152 0 0 25 0 1 0 482152864 255873024 52503 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62469 52503 603 41 0 62428 0
vsize: 249876
[startup+730.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57159 0 0 0 72858 152 0 0 25 0 1 0 482152864 255873024 52514 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62469 52514 603 41 0 62428 0
vsize: 249876
[startup+740.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57175 0 0 0 73857 152 0 0 25 0 1 0 482152864 255873024 52530 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62469 52530 603 41 0 62428 0
vsize: 249876
[startup+750.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57181 0 0 0 74858 152 0 0 25 0 1 0 482152864 255873024 52536 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62469 52536 603 41 0 62428 0
vsize: 249876
[startup+760.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57193 0 0 0 75856 152 0 0 25 0 1 0 482152864 256008192 52548 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62502 52548 603 41 0 62461 0
vsize: 250008
[startup+770.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57205 0 0 0 76856 152 0 0 25 0 1 0 482152864 256008192 52560 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62502 52560 603 41 0 62461 0
vsize: 250008
[startup+780.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57242 0 0 0 77856 152 0 0 25 0 1 0 482152864 256008192 52597 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62502 52597 603 41 0 62461 0
vsize: 250008
[startup+790.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57264 0 0 0 78857 153 0 0 25 0 1 0 482152864 256143360 52619 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62535 52619 603 41 0 62494 0
vsize: 250140
[startup+800.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57286 0 0 0 79856 153 0 0 25 0 1 0 482152864 256278528 52641 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62568 52641 603 41 0 62527 0
vsize: 250272
[startup+810.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57339 0 0 0 80856 153 0 0 25 0 1 0 482152864 256413696 52694 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62601 52694 603 41 0 62560 0
vsize: 250404
[startup+820.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57345 0 0 0 81857 153 0 0 25 0 1 0 482152864 256413696 52700 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62601 52700 603 41 0 62560 0
vsize: 250404
[startup+830.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57357 0 0 0 82857 153 0 0 25 0 1 0 482152864 256548864 52712 4294967295 134512640 134672761 3221224624 3221223816 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62634 52712 603 41 0 62593 0
vsize: 250536
[startup+840.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57379 0 0 0 83857 153 0 0 25 0 1 0 482152864 256548864 52734 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62634 52734 603 41 0 62593 0
vsize: 250536
[startup+850.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57384 0 0 0 84857 153 0 0 25 0 1 0 482152864 256679936 52739 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62666 52739 603 41 0 62625 0
vsize: 250664
[startup+860.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57391 0 0 0 85858 153 0 0 25 0 1 0 482152864 256679936 52746 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62666 52746 603 41 0 62625 0
vsize: 250664
[startup+870.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57403 0 0 0 86858 154 0 0 25 0 1 0 482152864 256679936 52758 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62666 52758 603 41 0 62625 0
vsize: 250664
[startup+880.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57413 0 0 0 87858 154 0 0 25 0 1 0 482152864 256942080 52768 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62730 52768 603 41 0 62689 0
vsize: 250920
[startup+890.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57426 0 0 0 88859 154 0 0 25 0 1 0 482152864 257077248 52781 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62763 52781 603 41 0 62722 0
vsize: 251052
[startup+900.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57445 0 0 0 89860 154 0 0 25 0 1 0 482152864 257077248 52800 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62763 52800 603 41 0 62722 0
vsize: 251052
[startup+910.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57466 0 0 0 90860 154 0 0 25 0 1 0 482152864 257212416 52821 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62796 52821 603 41 0 62755 0
vsize: 251184
[startup+920.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57489 0 0 0 91860 154 0 0 25 0 1 0 482152864 257347584 52844 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62829 52844 603 41 0 62788 0
vsize: 251316
[startup+930.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57498 0 0 0 92860 154 0 0 25 0 1 0 482152864 257347584 52853 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62829 52853 603 41 0 62788 0
vsize: 251316
[startup+940.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57513 0 0 0 93860 154 0 0 25 0 1 0 482152864 257347584 52868 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62829 52868 603 41 0 62788 0
vsize: 251316
[startup+950.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57528 0 0 0 94861 154 0 0 25 0 1 0 482152864 257482752 52883 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62862 52883 603 41 0 62821 0
vsize: 251448
[startup+960.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57544 0 0 0 95861 154 0 0 25 0 1 0 482152864 257482752 52899 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62862 52899 603 41 0 62821 0
vsize: 251448
[startup+970.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57555 0 0 0 96861 154 0 0 25 0 1 0 482152864 257482752 52910 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62862 52910 603 41 0 62821 0
vsize: 251448
[startup+980.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57564 0 0 0 97861 154 0 0 25 0 1 0 482152864 257617920 52919 4294967295 134512640 134672761 3221224624 3221223888 134562268 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62895 52919 603 41 0 62854 0
vsize: 251580
[startup+990.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57582 0 0 0 98861 154 0 0 25 0 1 0 482152864 257617920 52937 4294967295 134512640 134672761 3221224624 3221223772 134566158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62895 52937 603 41 0 62854 0
vsize: 251580
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57620 0 0 0 99861 154 0 0 25 0 1 0 482152864 257753088 52975 4294967295 134512640 134672761 3221224624 3221223776 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62928 52975 603 41 0 62887 0
vsize: 251712
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57630 0 0 0 100862 154 0 0 25 0 1 0 482152864 257888256 52985 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62961 52985 603 41 0 62920 0
vsize: 251844
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57649 0 0 0 101862 154 0 0 25 0 1 0 482152864 257888256 53004 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62961 53004 603 41 0 62920 0
vsize: 251844
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57662 0 0 0 102862 154 0 0 25 0 1 0 482152864 258023424 53017 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62994 53017 603 41 0 62953 0
vsize: 251976
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57680 0 0 0 103862 154 0 0 25 0 1 0 482152864 258023424 53035 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62994 53035 603 41 0 62953 0
vsize: 251976
[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57710 0 0 0 104862 154 0 0 25 0 1 0 482152864 258154496 53065 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63026 53065 603 41 0 62985 0
vsize: 252104
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57850 0 0 0 105862 155 0 0 25 0 1 0 482152864 258695168 53205 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63158 53205 603 41 0 63117 0
vsize: 252632
[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57873 0 0 0 106862 155 0 0 25 0 1 0 482152864 258830336 53228 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63191 53228 603 41 0 63150 0
vsize: 252764
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57961 0 0 0 107862 155 0 0 25 0 1 0 482152864 259100672 53316 4294967295 134512640 134672761 3221224624 3221223776 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63257 53316 603 41 0 63216 0
vsize: 253028
[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57981 0 0 0 108862 155 0 0 25 0 1 0 482152864 259235840 53336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63290 53336 603 41 0 63249 0
vsize: 253160
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 57996 0 0 0 109862 155 0 0 25 0 1 0 482152864 259235840 53351 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63290 53351 603 41 0 63249 0
vsize: 253160
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 58035 0 0 0 110862 155 0 0 25 0 1 0 482152864 259371008 53390 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63323 53390 603 41 0 63282 0
vsize: 253292
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 58067 0 0 0 111862 155 0 0 25 0 1 0 482152864 259506176 53422 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63356 53422 603 41 0 63315 0
vsize: 253424
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 58215 0 0 0 112861 156 0 0 25 0 1 0 482152864 260182016 53570 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63521 53570 603 41 0 63480 0
vsize: 254084
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 58244 0 0 0 113861 156 0 0 25 0 1 0 482152864 260317184 53599 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63554 53599 603 41 0 63513 0
vsize: 254216
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 58295 0 0 0 114861 156 0 0 25 0 1 0 482152864 260452352 53650 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63587 53650 603 41 0 63546 0
vsize: 254348
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 58383 0 0 0 115861 156 0 0 25 0 1 0 482152864 260853760 53738 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63685 53738 603 41 0 63644 0
vsize: 254740
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 58428 0 0 0 116862 157 0 0 25 0 1 0 482152864 260988928 53783 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63718 53783 603 41 0 63677 0
vsize: 254872
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 58449 0 0 0 117861 157 0 0 25 0 1 0 482152864 261124096 53804 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63751 53804 603 41 0 63710 0
vsize: 255004
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 58479 0 0 0 118862 157 0 0 25 0 1 0 482152864 261124096 53834 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63751 53834 603 41 0 63710 0
vsize: 255004
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 30502
Raw data (stat): 30502 (minisat+) R 30501 30854 30853 0 -1 0 58506 0 0 0 119862 157 0 0 25 0 1 0 482152864 261255168 53861 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63783 53861 603 41 0 63742 0
vsize: 255132
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.96 1/54 30502
Raw data (stat): 30502 (minisat+) Z 30501 30854 30853 0 -1 12 58508 0 0 0 119862 167 0 0 25 0 1 0 482152864 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.18
CPU time (s): 1200.3
CPU user time (s): 1198.62
CPU system time (s): 1.67874
CPU usage (%): 100.01
Max. virtual memory (Kb): 255132
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####