PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-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	12.972
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 13281

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        740684 kB
Buffers:         33160 kB
Cached:         226776 kB
SwapCached:        164 kB
Active:          71464 kB
Inactive:       190960 kB
HighTotal:      131008 kB
HighFree:        28840 kB
LowTotal:       903652 kB
LowFree:        711844 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6088 kB
Slab:            25896 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 20:43:43 (client local time) WITH STATUS 0 IN 1200.49 SECONDS
stats: 15241 7 1200.49 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.90 0.53 0.21 2/54 6936
Raw data (stat): 6936 (runsolver) R 6935 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539296495 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99998 s]
Raw data (loadavg): 0.91 0.55 0.22 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 16533 0 0 0 955 43 0 0 25 0 1 0 539296495 62656512 13299 4294967295 134512640 134672761 3221224624 3221222192 134523714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15297 13299 603 41 0 15256 0
vsize: 61188
[startup+20.0504 s]
Raw data (loadavg): 0.93 0.56 0.23 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 52257 0 0 0 1874 130 0 0 25 0 1 0 539296495 236441600 47612 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57725 47612 603 41 0 57684 0
vsize: 230900
[startup+30.0506 s]
Raw data (loadavg): 0.94 0.58 0.24 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 53350 0 0 0 2871 132 0 0 25 0 1 0 539296495 240902144 48705 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58814 48705 603 41 0 58773 0
vsize: 235256
[startup+40.0509 s]
Raw data (loadavg): 0.95 0.59 0.25 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 53890 0 0 0 3870 134 0 0 25 0 1 0 539296495 243064832 49245 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59342 49245 603 41 0 59301 0
vsize: 237368
[startup+50.0505 s]
Raw data (loadavg): 0.95 0.60 0.25 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 54270 0 0 0 4868 135 0 0 25 0 1 0 539296495 244686848 49625 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59738 49625 603 41 0 59697 0
vsize: 238952
[startup+60.0506 s]
Raw data (loadavg): 1.03 0.63 0.27 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 54564 0 0 0 5866 137 0 0 25 0 1 0 539296495 245768192 49919 4294967295 134512640 134672761 3221224624 3221223804 134553584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60002 49919 603 41 0 59961 0
vsize: 240008
[startup+70.0498 s]
Raw data (loadavg): 1.03 0.64 0.27 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 54930 0 0 0 6865 138 0 0 25 0 1 0 539296495 247255040 50285 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60365 50285 603 41 0 60324 0
vsize: 241460
[startup+80.0495 s]
Raw data (loadavg): 1.02 0.65 0.28 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 55066 0 0 0 7864 139 0 0 25 0 1 0 539296495 247795712 50421 4294967295 134512640 134672761 3221224624 3221223792 134553613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60497 50421 603 41 0 60456 0
vsize: 241988
[startup+90.0492 s]
Raw data (loadavg): 1.02 0.66 0.29 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 55099 0 0 0 8863 140 0 0 25 0 1 0 539296495 247930880 50454 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60530 50454 603 41 0 60489 0
vsize: 242120
[startup+100.049 s]
Raw data (loadavg): 1.02 0.67 0.29 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 55240 0 0 0 9863 140 0 0 25 0 1 0 539296495 248471552 50595 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60662 50595 603 41 0 60621 0
vsize: 242648
[startup+110.072 s]
Raw data (loadavg): 1.01 0.68 0.30 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 55306 0 0 0 10865 140 0 0 25 0 1 0 539296495 248741888 50661 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60728 50661 603 41 0 60687 0
vsize: 242912
[startup+120.176 s]
Raw data (loadavg): 1.08 0.72 0.32 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 55361 0 0 0 11875 141 0 0 25 0 1 0 539296495 249008128 50716 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60793 50716 603 41 0 60752 0
vsize: 243172
[startup+130.177 s]
Raw data (loadavg): 1.06 0.72 0.32 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 55701 0 0 0 12874 142 0 0 25 0 1 0 539296495 250335232 51056 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61117 51056 603 41 0 61076 0
vsize: 244468
[startup+140.176 s]
Raw data (loadavg): 1.05 0.73 0.33 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 55808 0 0 0 13873 143 0 0 25 0 1 0 539296495 250740736 51163 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61216 51163 603 41 0 61175 0
vsize: 244864
[startup+150.176 s]
Raw data (loadavg): 1.05 0.74 0.34 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 55916 0 0 0 14873 143 0 0 25 0 1 0 539296495 251146240 51271 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61315 51271 603 41 0 61274 0
vsize: 245260
[startup+160.176 s]
Raw data (loadavg): 1.04 0.75 0.34 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 55941 0 0 0 15872 144 0 0 25 0 1 0 539296495 251146240 51296 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61315 51296 603 41 0 61274 0
vsize: 245260
[startup+170.176 s]
Raw data (loadavg): 1.03 0.76 0.35 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 55984 0 0 0 16872 144 0 0 25 0 1 0 539296495 251281408 51339 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61348 51339 603 41 0 61307 0
vsize: 245392
[startup+180.175 s]
Raw data (loadavg): 1.03 0.76 0.36 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56091 0 0 0 17871 145 0 0 25 0 1 0 539296495 251830272 51446 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61482 51446 603 41 0 61441 0
vsize: 245928
[startup+190.176 s]
Raw data (loadavg): 1.02 0.77 0.36 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56109 0 0 0 18871 145 0 0 25 0 1 0 539296495 251830272 51464 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61482 51464 603 41 0 61441 0
vsize: 245928
[startup+200.175 s]
Raw data (loadavg): 1.02 0.78 0.37 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56139 0 0 0 19871 146 0 0 25 0 1 0 539296495 251965440 51494 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61515 51494 603 41 0 61474 0
vsize: 246060
[startup+210.175 s]
Raw data (loadavg): 1.02 0.79 0.38 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56153 0 0 0 20871 146 0 0 25 0 1 0 539296495 252100608 51508 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61548 51508 603 41 0 61507 0
vsize: 246192
[startup+220.176 s]
Raw data (loadavg): 1.01 0.79 0.38 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56172 0 0 0 21870 147 0 0 25 0 1 0 539296495 252100608 51527 4294967295 134512640 134672761 3221224624 3221223808 134557994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61548 51527 603 41 0 61507 0
vsize: 246192
[startup+230.176 s]
Raw data (loadavg): 1.01 0.80 0.39 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56227 0 0 0 22870 147 0 0 25 0 1 0 539296495 252235776 51582 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61581 51582 603 41 0 61540 0
vsize: 246324
[startup+240.176 s]
Raw data (loadavg): 1.01 0.80 0.39 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56234 0 0 0 23870 147 0 0 25 0 1 0 539296495 252235776 51589 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61581 51589 603 41 0 61540 0
vsize: 246324
[startup+250.176 s]
Raw data (loadavg): 1.01 0.81 0.40 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56253 0 0 0 24870 148 0 0 25 0 1 0 539296495 252235776 51608 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61581 51608 603 41 0 61540 0
vsize: 246324
[startup+260.176 s]
Raw data (loadavg): 1.00 0.82 0.41 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56263 0 0 0 25870 148 0 0 25 0 1 0 539296495 252370944 51618 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61614 51618 603 41 0 61573 0
vsize: 246456
[startup+270.176 s]
Raw data (loadavg): 1.00 0.82 0.41 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56274 0 0 0 26869 149 0 0 25 0 1 0 539296495 252370944 51629 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61614 51629 603 41 0 61573 0
vsize: 246456
[startup+280.176 s]
Raw data (loadavg): 1.00 0.83 0.42 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56306 0 0 0 27869 149 0 0 25 0 1 0 539296495 252506112 51661 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61647 51661 603 41 0 61606 0
vsize: 246588
[startup+290.177 s]
Raw data (loadavg): 1.00 0.83 0.42 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56321 0 0 0 28869 149 0 0 25 0 1 0 539296495 252506112 51676 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61647 51676 603 41 0 61606 0
vsize: 246588
[startup+300.176 s]
Raw data (loadavg): 1.00 0.84 0.43 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56344 0 0 0 29869 149 0 0 25 0 1 0 539296495 252641280 51699 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61680 51699 603 41 0 61639 0
vsize: 246720
[startup+310.177 s]
Raw data (loadavg): 1.00 0.84 0.43 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56356 0 0 0 30869 149 0 0 25 0 1 0 539296495 252776448 51711 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61713 51711 603 41 0 61672 0
vsize: 246852
[startup+320.177 s]
Raw data (loadavg): 1.00 0.85 0.44 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56377 0 0 0 31869 150 0 0 25 0 1 0 539296495 252776448 51732 4294967295 134512640 134672761 3221224624 3221223796 134556598 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.177 s]
Raw data (loadavg): 1.00 0.85 0.45 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56394 0 0 0 32870 150 0 0 25 0 1 0 539296495 252911616 51749 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61746 51749 603 41 0 61705 0
vsize: 246984
[startup+340.177 s]
Raw data (loadavg): 1.00 0.86 0.45 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56454 0 0 0 33869 150 0 0 25 0 1 0 539296495 253046784 51809 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61779 51809 603 41 0 61738 0
vsize: 247116
[startup+350.177 s]
Raw data (loadavg): 1.00 0.86 0.46 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56478 0 0 0 34870 150 0 0 25 0 1 0 539296495 253181952 51833 4294967295 134512640 134672761 3221224624 3221223792 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61812 51833 603 41 0 61771 0
vsize: 247248
[startup+360.177 s]
Raw data (loadavg): 1.00 0.86 0.46 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56503 0 0 0 35870 150 0 0 25 0 1 0 539296495 253317120 51858 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61845 51858 603 41 0 61804 0
vsize: 247380
[startup+370.177 s]
Raw data (loadavg): 1.00 0.87 0.47 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56518 0 0 0 36870 150 0 0 25 0 1 0 539296495 253317120 51873 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61845 51873 603 41 0 61804 0
vsize: 247380
[startup+380.176 s]
Raw data (loadavg): 1.00 0.87 0.47 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56529 0 0 0 37870 150 0 0 25 0 1 0 539296495 253452288 51884 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61878 51884 603 41 0 61837 0
vsize: 247512
[startup+390.177 s]
Raw data (loadavg): 1.00 0.88 0.48 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56538 0 0 0 38870 150 0 0 25 0 1 0 539296495 253452288 51893 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61878 51893 603 41 0 61837 0
vsize: 247512
[startup+400.177 s]
Raw data (loadavg): 1.00 0.88 0.48 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56544 0 0 0 39870 150 0 0 25 0 1 0 539296495 253452288 51899 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61878 51899 603 41 0 61837 0
vsize: 247512
[startup+410.177 s]
Raw data (loadavg): 1.00 0.88 0.49 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56580 0 0 0 40870 150 0 0 25 0 1 0 539296495 253587456 51935 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61911 51935 603 41 0 61870 0
vsize: 247644
[startup+420.177 s]
Raw data (loadavg): 1.00 0.89 0.49 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56605 0 0 0 41871 150 0 0 25 0 1 0 539296495 253722624 51960 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61944 51960 603 41 0 61903 0
vsize: 247776
[startup+430.177 s]
Raw data (loadavg): 1.00 0.89 0.50 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56627 0 0 0 42871 150 0 0 25 0 1 0 539296495 253722624 51982 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61944 51982 603 41 0 61903 0
vsize: 247776
[startup+440.176 s]
Raw data (loadavg): 1.00 0.89 0.50 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56641 0 0 0 43871 150 0 0 25 0 1 0 539296495 253857792 51996 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61977 51996 603 41 0 61936 0
vsize: 247908
[startup+450.176 s]
Raw data (loadavg): 1.00 0.90 0.51 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56662 0 0 0 44871 150 0 0 25 0 1 0 539296495 253857792 52017 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61977 52017 603 41 0 61936 0
vsize: 247908
[startup+460.176 s]
Raw data (loadavg): 1.00 0.90 0.51 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56679 0 0 0 45871 150 0 0 25 0 1 0 539296495 253992960 52034 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62010 52034 603 41 0 61969 0
vsize: 248040
[startup+470.176 s]
Raw data (loadavg): 1.00 0.90 0.52 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56718 0 0 0 46871 150 0 0 25 0 1 0 539296495 254255104 52073 4294967295 134512640 134672761 3221224624 3221223820 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62074 52073 603 41 0 62033 0
vsize: 248296
[startup+480.175 s]
Raw data (loadavg): 1.00 0.90 0.52 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56719 0 0 0 47871 150 0 0 25 0 1 0 539296495 254255104 52074 4294967295 134512640 134672761 3221224624 3221223748 134566115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62074 52074 603 41 0 62033 0
vsize: 248296
[startup+490.175 s]
Raw data (loadavg): 1.00 0.91 0.53 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56734 0 0 0 48871 150 0 0 25 0 1 0 539296495 254255104 52089 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62074 52089 603 41 0 62033 0
vsize: 248296
[startup+500.174 s]
Raw data (loadavg): 1.00 0.91 0.53 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56745 0 0 0 49872 150 0 0 25 0 1 0 539296495 254390272 52100 4294967295 134512640 134672761 3221224624 3221223792 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62107 52100 603 41 0 62066 0
vsize: 248428
[startup+510.175 s]
Raw data (loadavg): 1.00 0.91 0.54 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56764 0 0 0 50872 151 0 0 25 0 1 0 539296495 254390272 52119 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62107 52119 603 41 0 62066 0
vsize: 248428
[startup+520.175 s]
Raw data (loadavg): 1.00 0.91 0.54 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56779 0 0 0 51872 151 0 0 25 0 1 0 539296495 254525440 52134 4294967295 134512640 134672761 3221224624 3221223840 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62140 52134 603 41 0 62099 0
vsize: 248560
[startup+530.175 s]
Raw data (loadavg): 1.00 0.92 0.55 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56822 0 0 0 52871 151 0 0 25 0 1 0 539296495 254525440 52177 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62140 52177 603 41 0 62099 0
vsize: 248560
[startup+540.175 s]
Raw data (loadavg): 1.00 0.92 0.55 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56839 0 0 0 53870 151 0 0 25 0 1 0 539296495 254660608 52194 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62173 52194 603 41 0 62132 0
vsize: 248692
[startup+550.175 s]
Raw data (loadavg): 1.00 0.92 0.55 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56855 0 0 0 54870 151 0 0 25 0 1 0 539296495 254660608 52210 4294967295 134512640 134672761 3221224624 3221223792 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62173 52210 603 41 0 62132 0
vsize: 248692
[startup+560.174 s]
Raw data (loadavg): 1.00 0.92 0.56 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56863 0 0 0 55871 151 0 0 25 0 1 0 539296495 254660608 52218 4294967295 134512640 134672761 3221224624 3221223792 134553613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62173 52218 603 41 0 62132 0
vsize: 248692
[startup+570.176 s]
Raw data (loadavg): 1.00 0.92 0.56 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56923 0 0 0 56871 152 0 0 25 0 1 0 539296495 254930944 52278 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62239 52278 603 41 0 62198 0
vsize: 248956
[startup+580.176 s]
Raw data (loadavg): 1.00 0.93 0.57 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56938 0 0 0 57871 152 0 0 25 0 1 0 539296495 255066112 52293 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62272 52293 603 41 0 62231 0
vsize: 249088
[startup+590.176 s]
Raw data (loadavg): 1.00 0.93 0.57 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56950 0 0 0 58871 152 0 0 25 0 1 0 539296495 255066112 52305 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62272 52305 603 41 0 62231 0
vsize: 249088
[startup+600.176 s]
Raw data (loadavg): 1.00 0.93 0.57 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56977 0 0 0 59871 152 0 0 25 0 1 0 539296495 255201280 52332 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62305 52332 603 41 0 62264 0
vsize: 249220
[startup+610.176 s]
Raw data (loadavg): 1.00 0.93 0.58 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 56989 0 0 0 60871 152 0 0 25 0 1 0 539296495 255201280 52344 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62305 52344 603 41 0 62264 0
vsize: 249220
[startup+620.175 s]
Raw data (loadavg): 1.00 0.93 0.58 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57008 0 0 0 61871 152 0 0 25 0 1 0 539296495 255201280 52363 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62305 52363 603 41 0 62264 0
vsize: 249220
[startup+630.177 s]
Raw data (loadavg): 1.00 0.94 0.58 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57015 0 0 0 62872 152 0 0 25 0 1 0 539296495 255336448 52370 4294967295 134512640 134672761 3221224624 3221223792 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62338 52370 603 41 0 62297 0
vsize: 249352
[startup+640.177 s]
Raw data (loadavg): 1.00 0.94 0.59 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57023 0 0 0 63872 152 0 0 25 0 1 0 539296495 255336448 52378 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62338 52378 603 41 0 62297 0
vsize: 249352
[startup+650.177 s]
Raw data (loadavg): 1.00 0.94 0.59 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57031 0 0 0 64872 152 0 0 25 0 1 0 539296495 255336448 52386 4294967295 134512640 134672761 3221224624 3221223840 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62338 52386 603 41 0 62297 0
vsize: 249352
[startup+660.177 s]
Raw data (loadavg): 1.00 0.94 0.60 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57043 0 0 0 65872 152 0 0 25 0 1 0 539296495 255336448 52398 4294967295 134512640 134672761 3221224624 3221223748 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62338 52398 603 41 0 62297 0
vsize: 249352
[startup+670.185 s]
Raw data (loadavg): 1.00 0.94 0.60 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57061 0 0 0 66873 152 0 0 25 0 1 0 539296495 255471616 52416 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62371 52416 603 41 0 62330 0
vsize: 249484
[startup+680.187 s]
Raw data (loadavg): 1.00 0.94 0.60 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57072 0 0 0 67873 152 0 0 25 0 1 0 539296495 255471616 52427 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62371 52427 603 41 0 62330 0
vsize: 249484
[startup+690.187 s]
Raw data (loadavg): 1.00 0.94 0.61 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57082 0 0 0 68873 152 0 0 25 0 1 0 539296495 255606784 52437 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62404 52437 603 41 0 62363 0
vsize: 249616
[startup+700.187 s]
Raw data (loadavg): 1.00 0.95 0.61 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57092 0 0 0 69873 152 0 0 25 0 1 0 539296495 255606784 52447 4294967295 134512640 134672761 3221224624 3221223760 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62404 52447 603 41 0 62363 0
vsize: 249616
[startup+710.19 s]
Raw data (loadavg): 1.00 0.95 0.62 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57101 0 0 0 70874 152 0 0 25 0 1 0 539296495 255606784 52456 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62404 52456 603 41 0 62363 0
vsize: 249616
[startup+720.19 s]
Raw data (loadavg): 1.00 0.95 0.62 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57116 0 0 0 71874 152 0 0 25 0 1 0 539296495 255741952 52471 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62437 52471 603 41 0 62396 0
vsize: 249748
[startup+730.189 s]
Raw data (loadavg): 1.00 0.95 0.62 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57156 0 0 0 72874 152 0 0 25 0 1 0 539296495 255873024 52511 4294967295 134512640 134672761 3221224624 3221223824 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62469 52511 603 41 0 62428 0
vsize: 249876
[startup+740.189 s]
Raw data (loadavg): 1.00 0.95 0.63 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57170 0 0 0 73874 152 0 0 25 0 1 0 539296495 255873024 52525 4294967295 134512640 134672761 3221224624 3221223748 134566062 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62469 52525 603 41 0 62428 0
vsize: 249876
[startup+750.189 s]
Raw data (loadavg): 1.00 0.95 0.63 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57178 0 0 0 74874 153 0 0 25 0 1 0 539296495 255873024 52533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62469 52533 603 41 0 62428 0
vsize: 249876
[startup+760.191 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57188 0 0 0 75875 153 0 0 25 0 1 0 539296495 256008192 52543 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62502 52543 603 41 0 62461 0
vsize: 250008
[startup+770.191 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57201 0 0 0 76873 153 0 0 25 0 1 0 539296495 256008192 52556 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62502 52556 603 41 0 62461 0
vsize: 250008
[startup+780.19 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57240 0 0 0 77873 153 0 0 25 0 1 0 539296495 256008192 52595 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62502 52595 603 41 0 62461 0
vsize: 250008
[startup+790.189 s]
Raw data (loadavg): 1.00 0.95 0.64 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57260 0 0 0 78873 153 0 0 25 0 1 0 539296495 256143360 52615 4294967295 134512640 134672761 3221224624 3221223796 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62535 52615 603 41 0 62494 0
vsize: 250140
[startup+800.189 s]
Raw data (loadavg): 1.00 0.96 0.65 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57282 0 0 0 79873 153 0 0 25 0 1 0 539296495 256278528 52637 4294967295 134512640 134672761 3221224624 3221223792 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62568 52637 603 41 0 62527 0
vsize: 250272
[startup+810.189 s]
Raw data (loadavg): 1.00 0.96 0.65 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57324 0 0 0 80873 154 0 0 25 0 1 0 539296495 256413696 52679 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62601 52679 603 41 0 62560 0
vsize: 250404
[startup+820.188 s]
Raw data (loadavg): 1.00 0.96 0.65 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57345 0 0 0 81873 154 0 0 25 0 1 0 539296495 256413696 52700 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62601 52700 603 41 0 62560 0
vsize: 250404
[startup+830.195 s]
Raw data (loadavg): 1.00 0.96 0.66 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57349 0 0 0 82874 154 0 0 25 0 1 0 539296495 256548864 52704 4294967295 134512640 134672761 3221224624 3221223792 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62634 52704 603 41 0 62593 0
vsize: 250536
[startup+840.202 s]
Raw data (loadavg): 1.00 0.96 0.66 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57374 0 0 0 83874 154 0 0 25 0 1 0 539296495 256548864 52729 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62634 52729 603 41 0 62593 0
vsize: 250536
[startup+850.201 s]
Raw data (loadavg): 1.00 0.96 0.66 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57382 0 0 0 84874 154 0 0 25 0 1 0 539296495 256548864 52737 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62634 52737 603 41 0 62593 0
vsize: 250536
[startup+860.201 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57389 0 0 0 85875 154 0 0 25 0 1 0 539296495 256679936 52744 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62666 52744 603 41 0 62625 0
vsize: 250664
[startup+870.201 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57398 0 0 0 86875 154 0 0 25 0 1 0 539296495 256679936 52753 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62666 52753 603 41 0 62625 0
vsize: 250664
[startup+880.2 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57410 0 0 0 87875 154 0 0 25 0 1 0 539296495 256942080 52765 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62730 52765 603 41 0 62689 0
vsize: 250920
[startup+890.2 s]
Raw data (loadavg): 1.00 0.96 0.67 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57424 0 0 0 88875 154 0 0 25 0 1 0 539296495 257077248 52779 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62763 52779 603 41 0 62722 0
vsize: 251052
[startup+900.201 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57439 0 0 0 89875 154 0 0 25 0 1 0 539296495 257077248 52794 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62763 52794 603 41 0 62722 0
vsize: 251052
[startup+910.2 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57462 0 0 0 90875 154 0 0 25 0 1 0 539296495 257212416 52817 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62796 52817 603 41 0 62755 0
vsize: 251184
[startup+920.2 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57481 0 0 0 91875 154 0 0 25 0 1 0 539296495 257212416 52836 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62796 52836 603 41 0 62755 0
vsize: 251184
[startup+930.205 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57495 0 0 0 92876 155 0 0 25 0 1 0 539296495 257347584 52850 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62829 52850 603 41 0 62788 0
vsize: 251316
[startup+940.212 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57511 0 0 0 93877 155 0 0 25 0 1 0 539296495 257347584 52866 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62829 52866 603 41 0 62788 0
vsize: 251316
[startup+950.213 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57524 0 0 0 94877 155 0 0 25 0 1 0 539296495 257482752 52879 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62862 52879 603 41 0 62821 0
vsize: 251448
[startup+960.213 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57541 0 0 0 95877 155 0 0 25 0 1 0 539296495 257482752 52896 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62862 52896 603 41 0 62821 0
vsize: 251448
[startup+970.217 s]
Raw data (loadavg): 1.00 0.97 0.70 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57553 0 0 0 96878 155 0 0 25 0 1 0 539296495 257482752 52908 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62862 52908 603 41 0 62821 0
vsize: 251448
[startup+980.217 s]
Raw data (loadavg): 1.00 0.97 0.70 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57564 0 0 0 97878 155 0 0 25 0 1 0 539296495 257617920 52919 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62895 52919 603 41 0 62854 0
vsize: 251580
[startup+990.217 s]
Raw data (loadavg): 1.00 0.97 0.70 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57581 0 0 0 98878 155 0 0 25 0 1 0 539296495 257617920 52936 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62895 52936 603 41 0 62854 0
vsize: 251580
[startup+1000.22 s]
Raw data (loadavg): 1.00 0.97 0.71 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57598 0 0 0 99878 155 0 0 25 0 1 0 539296495 257753088 52953 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62928 52953 603 41 0 62887 0
vsize: 251712
[startup+1010.22 s]
Raw data (loadavg): 1.00 0.97 0.71 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57629 0 0 0 100878 156 0 0 25 0 1 0 539296495 257888256 52984 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62961 52984 603 41 0 62920 0
vsize: 251844
[startup+1020.22 s]
Raw data (loadavg): 1.00 0.97 0.71 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57648 0 0 0 101878 156 0 0 25 0 1 0 539296495 257888256 53003 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62961 53003 603 41 0 62920 0
vsize: 251844
[startup+1030.22 s]
Raw data (loadavg): 1.00 0.97 0.72 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57661 0 0 0 102878 156 0 0 25 0 1 0 539296495 258023424 53016 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62994 53016 603 41 0 62953 0
vsize: 251976
[startup+1040.22 s]
Raw data (loadavg): 1.00 0.97 0.72 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57679 0 0 0 103879 156 0 0 25 0 1 0 539296495 258023424 53034 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62994 53034 603 41 0 62953 0
vsize: 251976
[startup+1050.22 s]
Raw data (loadavg): 1.00 0.97 0.72 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57709 0 0 0 104879 156 0 0 25 0 1 0 539296495 258154496 53064 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63026 53064 603 41 0 62985 0
vsize: 252104
[startup+1060.22 s]
Raw data (loadavg): 1.00 0.97 0.72 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57850 0 0 0 105878 156 0 0 25 0 1 0 539296495 258695168 53205 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63158 53205 603 41 0 63117 0
vsize: 252632
[startup+1070.22 s]
Raw data (loadavg): 1.00 0.97 0.73 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57872 0 0 0 106877 157 0 0 25 0 1 0 539296495 258830336 53227 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63191 53227 603 41 0 63150 0
vsize: 252764
[startup+1080.22 s]
Raw data (loadavg): 1.00 0.97 0.73 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57956 0 0 0 107877 157 0 0 25 0 1 0 539296495 259100672 53311 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63257 53311 603 41 0 63216 0
vsize: 253028
[startup+1090.22 s]
Raw data (loadavg): 1.00 0.97 0.73 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57981 0 0 0 108877 157 0 0 25 0 1 0 539296495 259235840 53336 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63290 53336 603 41 0 63249 0
vsize: 253160
[startup+1100.22 s]
Raw data (loadavg): 1.00 0.97 0.73 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 57995 0 0 0 109877 157 0 0 25 0 1 0 539296495 259235840 53350 4294967295 134512640 134672761 3221224624 3221223796 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63290 53350 603 41 0 63249 0
vsize: 253160
[startup+1110.22 s]
Raw data (loadavg): 1.00 0.97 0.74 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 58034 0 0 0 110877 157 0 0 25 0 1 0 539296495 259371008 53389 4294967295 134512640 134672761 3221224624 3221223748 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63323 53389 603 41 0 63282 0
vsize: 253292
[startup+1120.22 s]
Raw data (loadavg): 1.00 0.97 0.74 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 58067 0 0 0 111877 157 0 0 25 0 1 0 539296495 259506176 53422 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63356 53422 603 41 0 63315 0
vsize: 253424
[startup+1130.23 s]
Raw data (loadavg): 1.00 0.97 0.74 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 58205 0 0 0 112877 157 0 0 25 0 1 0 539296495 260046848 53560 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63488 53560 603 41 0 63447 0
vsize: 253952
[startup+1140.23 s]
Raw data (loadavg): 1.00 0.97 0.74 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 58242 0 0 0 113878 157 0 0 25 0 1 0 539296495 260182016 53597 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63521 53597 603 41 0 63480 0
vsize: 254084
[startup+1150.24 s]
Raw data (loadavg): 1.00 0.97 0.74 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 58295 0 0 0 114879 158 0 0 25 0 1 0 539296495 260452352 53650 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63587 53650 603 41 0 63546 0
vsize: 254348
[startup+1160.24 s]
Raw data (loadavg): 1.00 0.97 0.75 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 58383 0 0 0 115879 158 0 0 25 0 1 0 539296495 260853760 53738 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63685 53738 603 41 0 63644 0
vsize: 254740
[startup+1170.24 s]
Raw data (loadavg): 1.00 0.97 0.75 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 58428 0 0 0 116879 158 0 0 25 0 1 0 539296495 260988928 53783 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63718 53783 603 41 0 63677 0
vsize: 254872
[startup+1180.24 s]
Raw data (loadavg): 1.00 0.97 0.75 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 58450 0 0 0 117879 158 0 0 25 0 1 0 539296495 261124096 53805 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63751 53805 603 41 0 63710 0
vsize: 255004
[startup+1190.24 s]
Raw data (loadavg): 1.00 0.97 0.75 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 58480 0 0 0 118880 158 0 0 25 0 1 0 539296495 261124096 53835 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63751 53835 603 41 0 63710 0
vsize: 255004
[startup+1200.24 s]
Raw data (loadavg): 1.00 0.97 0.75 2/54 6936
Raw data (stat): 6936 (minisat+) R 6935 10614 10613 0 -1 0 58507 0 0 0 119880 158 0 0 25 0 1 0 539296495 261255168 53862 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63783 53862 603 41 0 63742 0
vsize: 255132
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.46 s]
Raw data (loadavg): 1.00 0.97 0.75 1/54 6936
Raw data (stat): 6936 (minisat+) Z 6935 10614 10613 0 -1 12 58509 0 0 0 119880 168 0 0 23 0 1 0 539296495 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.46
CPU time (s): 1200.49
CPU user time (s): 1198.8
CPU system time (s): 1.68874
CPU usage (%): 100.003
Max. virtual memory (Kb): 255132
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####