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 13282

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-20 20:23:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15249 boxname=wulflinc11 idbench=1173 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  e8862b41c9b4f49ec8d11d1df0495e74  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-sp97ic.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-sp97ic.opb /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-sp97ic.opb
IDLAUNCH: 15249
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        574628 kB
Buffers:         42368 kB
Cached:         389192 kB
SwapCached:       4932 kB
Active:         214092 kB
Inactive:       225308 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        574376 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            15032 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 20:43:44 (client local time) WITH STATUS 0 IN 1200.49 SECONDS
stats: 15249 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 | 2847944  8701829 |  949314       0        0     nan |  0.000 % |
c |       100 | 2847939  8701814 | 1044245      99      319     3.2 |  0.187 % |
c |       250 | 2847877  8701628 | 1148669     228      714     3.1 |  0.189 % |
c |       475 | 2847736  8701205 | 1263536     409     1653     4.0 |  0.194 % |
c |       817 | 2847185  8699552 | 1389890     561     2249     4.0 |  0.212 % |
c |      1323 | 2846435  8697318 | 1528879     813     3318     4.1 |  0.238 % |
c |      2082 | 2845873  8695626 | 1681767    1370     5774     4.2 |  0.258 % |
c |      3222 | 2844973  8692886 | 1849944    2189     9735     4.4 |  0.288 % |
c |      4932 | 2843916  8689681 | 2034938    3491    16658     4.8 |  0.325 % |
c |      7494 | 2842312  8684747 | 2238432    5485    27996     5.1 |  0.378 % |
#### 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.08 0.02 0.01 2/54 21496
Raw data (stat): 21496 (runsolver) R 21495 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481067850 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.22 0.05 0.02 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 16540 0 0 0 959 39 0 0 25 0 1 0 481067850 62656512 13300 4294967295 134512640 134672761 3221224544 3221222112 134523706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15297 13300 603 41 0 15256 0
vsize: 61188
[startup+20.0089 s]
Raw data (loadavg): 0.34 0.08 0.02 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 58953 0 0 0 1858 141 0 0 25 0 1 0 481067850 238006272 54308 4294967295 134512640 134672761 3221224544 3221216736 1075350064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58107 54308 603 41 0 58066 0
vsize: 232428
[startup+30.0091 s]
Raw data (loadavg): 0.44 0.11 0.03 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63530 0 0 0 2845 154 0 0 25 0 1 0 481067850 285380608 58885 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69673 58885 603 41 0 69632 0
vsize: 278692
[startup+40.0095 s]
Raw data (loadavg): 0.53 0.14 0.04 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63581 0 0 0 3844 155 0 0 25 0 1 0 481067850 285380608 58936 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69673 58936 603 41 0 69632 0
vsize: 278692
[startup+50.0221 s]
Raw data (loadavg): 0.60 0.17 0.05 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63606 0 0 0 4846 155 0 0 25 0 1 0 481067850 285515776 58961 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69706 58961 603 41 0 69665 0
vsize: 278824
[startup+60.0225 s]
Raw data (loadavg): 0.66 0.19 0.06 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63607 0 0 0 5846 155 0 0 25 0 1 0 481067850 285515776 58962 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69706 58962 603 41 0 69665 0
vsize: 278824
[startup+70.0233 s]
Raw data (loadavg): 0.71 0.22 0.07 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63648 0 0 0 6845 156 0 0 25 0 1 0 481067850 285515776 59003 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69706 59003 603 41 0 69665 0
vsize: 278824
[startup+80.0257 s]
Raw data (loadavg): 0.76 0.24 0.08 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63682 0 0 0 7845 156 0 0 25 0 1 0 481067850 285515776 59037 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69706 59037 603 41 0 69665 0
vsize: 278824
[startup+90.0297 s]
Raw data (loadavg): 0.79 0.27 0.09 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63699 0 0 0 8845 156 0 0 25 0 1 0 481067850 285650944 59054 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69739 59054 603 41 0 69698 0
vsize: 278956
[startup+100.031 s]
Raw data (loadavg): 0.82 0.29 0.10 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63733 0 0 0 9845 156 0 0 25 0 1 0 481067850 285650944 59088 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69739 59088 603 41 0 69698 0
vsize: 278956
[startup+110.052 s]
Raw data (loadavg): 0.85 0.31 0.11 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63738 0 0 0 10847 157 0 0 25 0 1 0 481067850 285650944 59093 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69739 59093 603 41 0 69698 0
vsize: 278956
[startup+120.058 s]
Raw data (loadavg): 0.87 0.34 0.12 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63739 0 0 0 11847 157 0 0 25 0 1 0 481067850 285650944 59094 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69739 59094 603 41 0 69698 0
vsize: 278956
[startup+130.058 s]
Raw data (loadavg): 0.89 0.36 0.13 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63740 0 0 0 12847 157 0 0 25 0 1 0 481067850 285650944 59095 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69739 59095 603 41 0 69698 0
vsize: 278956
[startup+140.059 s]
Raw data (loadavg): 0.91 0.38 0.14 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63746 0 0 0 13847 157 0 0 25 0 1 0 481067850 285650944 59101 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69739 59101 603 41 0 69698 0
vsize: 278956
[startup+150.067 s]
Raw data (loadavg): 0.92 0.40 0.15 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63769 0 0 0 14847 158 0 0 25 0 1 0 481067850 285650944 59124 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69739 59124 603 41 0 69698 0
vsize: 278956
[startup+160.067 s]
Raw data (loadavg): 0.93 0.42 0.15 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63777 0 0 0 15847 158 0 0 25 0 1 0 481067850 285650944 59132 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69739 59132 603 41 0 69698 0
vsize: 278956
[startup+170.074 s]
Raw data (loadavg): 0.94 0.44 0.16 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63777 0 0 0 16847 158 0 0 25 0 1 0 481067850 285650944 59132 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69739 59132 603 41 0 69698 0
vsize: 278956
[startup+180.083 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63795 0 0 0 17848 158 0 0 25 0 1 0 481067850 285786112 59150 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69772 59150 603 41 0 69731 0
vsize: 279088
[startup+190.092 s]
Raw data (loadavg): 0.96 0.47 0.18 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63826 0 0 0 18849 158 0 0 25 0 1 0 481067850 285786112 59181 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69772 59181 603 41 0 69731 0
vsize: 279088
[startup+200.096 s]
Raw data (loadavg): 0.96 0.49 0.19 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63830 0 0 0 19850 158 0 0 25 0 1 0 481067850 285786112 59185 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69772 59185 603 41 0 69731 0
vsize: 279088
[startup+210.098 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63840 0 0 0 20850 159 0 0 25 0 1 0 481067850 285921280 59195 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69805 59195 603 41 0 69764 0
vsize: 279220
[startup+220.098 s]
Raw data (loadavg): 1.05 0.54 0.21 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63846 0 0 0 21850 159 0 0 25 0 1 0 481067850 285921280 59201 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69805 59201 603 41 0 69764 0
vsize: 279220
[startup+230.098 s]
Raw data (loadavg): 1.04 0.56 0.22 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63852 0 0 0 22850 159 0 0 25 0 1 0 481067850 285921280 59207 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69805 59207 603 41 0 69764 0
vsize: 279220
[startup+240.099 s]
Raw data (loadavg): 1.03 0.57 0.23 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63858 0 0 0 23851 159 0 0 25 0 1 0 481067850 285921280 59213 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69805 59213 603 41 0 69764 0
vsize: 279220
[startup+250.099 s]
Raw data (loadavg): 1.03 0.59 0.24 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63861 0 0 0 24851 159 0 0 25 0 1 0 481067850 285921280 59216 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69805 59216 603 41 0 69764 0
vsize: 279220
[startup+260.099 s]
Raw data (loadavg): 1.02 0.60 0.25 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63866 0 0 0 25851 159 0 0 25 0 1 0 481067850 285921280 59221 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69805 59221 603 41 0 69764 0
vsize: 279220
[startup+270.098 s]
Raw data (loadavg): 1.02 0.61 0.25 3/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63869 0 0 0 26851 159 0 0 25 0 1 0 481067850 285921280 59224 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69805 59224 603 41 0 69764 0
vsize: 279220
[startup+280.098 s]
Raw data (loadavg): 1.02 0.63 0.26 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63876 0 0 0 27851 159 0 0 25 0 1 0 481067850 285921280 59231 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69805 59231 603 41 0 69764 0
vsize: 279220
[startup+290.098 s]
Raw data (loadavg): 1.01 0.64 0.27 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63879 0 0 0 28851 159 0 0 25 0 1 0 481067850 286056448 59234 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69838 59234 603 41 0 69797 0
vsize: 279352
[startup+300.098 s]
Raw data (loadavg): 1.01 0.65 0.28 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63888 0 0 0 29851 159 0 0 25 0 1 0 481067850 286056448 59243 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69838 59243 603 41 0 69797 0
vsize: 279352
[startup+310.098 s]
Raw data (loadavg): 1.01 0.66 0.28 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63893 0 0 0 30852 159 0 0 25 0 1 0 481067850 286056448 59248 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69838 59248 603 41 0 69797 0
vsize: 279352
[startup+320.098 s]
Raw data (loadavg): 1.01 0.67 0.29 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63897 0 0 0 31852 159 0 0 25 0 1 0 481067850 286056448 59252 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69838 59252 603 41 0 69797 0
vsize: 279352
[startup+330.098 s]
Raw data (loadavg): 1.01 0.68 0.30 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63906 0 0 0 32852 159 0 0 25 0 1 0 481067850 286056448 59261 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69838 59261 603 41 0 69797 0
vsize: 279352
[startup+340.098 s]
Raw data (loadavg): 1.00 0.69 0.30 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63910 0 0 0 33852 159 0 0 25 0 1 0 481067850 286056448 59265 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69838 59265 603 41 0 69797 0
vsize: 279352
[startup+350.099 s]
Raw data (loadavg): 1.00 0.70 0.31 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63911 0 0 0 34852 159 0 0 25 0 1 0 481067850 286056448 59266 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69838 59266 603 41 0 69797 0
vsize: 279352
[startup+360.098 s]
Raw data (loadavg): 1.00 0.71 0.32 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63911 0 0 0 35852 159 0 0 25 0 1 0 481067850 286056448 59266 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69838 59266 603 41 0 69797 0
vsize: 279352
[startup+370.099 s]
Raw data (loadavg): 1.00 0.72 0.32 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63914 0 0 0 36852 159 0 0 25 0 1 0 481067850 286056448 59269 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69838 59269 603 41 0 69797 0
vsize: 279352
[startup+380.099 s]
Raw data (loadavg): 1.00 0.73 0.33 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63927 0 0 0 37853 159 0 0 25 0 1 0 481067850 286191616 59282 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59282 603 41 0 69830 0
vsize: 279484
[startup+390.099 s]
Raw data (loadavg): 1.00 0.74 0.34 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63930 0 0 0 38853 159 0 0 25 0 1 0 481067850 286191616 59285 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59285 603 41 0 69830 0
vsize: 279484
[startup+400.099 s]
Raw data (loadavg): 1.00 0.74 0.34 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63933 0 0 0 39853 159 0 0 25 0 1 0 481067850 286191616 59288 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59288 603 41 0 69830 0
vsize: 279484
[startup+410.098 s]
Raw data (loadavg): 1.00 0.75 0.35 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63935 0 0 0 40853 159 0 0 25 0 1 0 481067850 286191616 59290 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59290 603 41 0 69830 0
vsize: 279484
[startup+420.099 s]
Raw data (loadavg): 1.00 0.76 0.36 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63936 0 0 0 41853 159 0 0 25 0 1 0 481067850 286191616 59291 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59291 603 41 0 69830 0
vsize: 279484
[startup+430.099 s]
Raw data (loadavg): 1.00 0.77 0.37 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63938 0 0 0 42853 159 0 0 25 0 1 0 481067850 286191616 59293 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59293 603 41 0 69830 0
vsize: 279484
[startup+440.1 s]
Raw data (loadavg): 1.00 0.77 0.37 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63938 0 0 0 43854 159 0 0 25 0 1 0 481067850 286191616 59293 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59293 603 41 0 69830 0
vsize: 279484
[startup+450.1 s]
Raw data (loadavg): 1.00 0.78 0.38 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63939 0 0 0 44854 159 0 0 25 0 1 0 481067850 286191616 59294 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59294 603 41 0 69830 0
vsize: 279484
[startup+460.1 s]
Raw data (loadavg): 1.00 0.79 0.38 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63939 0 0 0 45854 159 0 0 25 0 1 0 481067850 286191616 59294 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59294 603 41 0 69830 0
vsize: 279484
[startup+470.1 s]
Raw data (loadavg): 1.00 0.80 0.39 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63943 0 0 0 46854 159 0 0 25 0 1 0 481067850 286191616 59298 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59298 603 41 0 69830 0
vsize: 279484
[startup+480.1 s]
Raw data (loadavg): 1.00 0.80 0.39 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63944 0 0 0 47854 159 0 0 25 0 1 0 481067850 286191616 59299 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59299 603 41 0 69830 0
vsize: 279484
[startup+490.101 s]
Raw data (loadavg): 1.00 0.81 0.40 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63945 0 0 0 48855 159 0 0 25 0 1 0 481067850 286191616 59300 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59300 603 41 0 69830 0
vsize: 279484
[startup+500.1 s]
Raw data (loadavg): 1.00 0.81 0.41 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63946 0 0 0 49855 159 0 0 25 0 1 0 481067850 286191616 59301 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59301 603 41 0 69830 0
vsize: 279484
[startup+510.1 s]
Raw data (loadavg): 1.00 0.82 0.41 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63947 0 0 0 50855 159 0 0 25 0 1 0 481067850 286191616 59302 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59302 603 41 0 69830 0
vsize: 279484
[startup+520.101 s]
Raw data (loadavg): 1.00 0.82 0.42 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63948 0 0 0 51855 159 0 0 25 0 1 0 481067850 286191616 59303 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59303 603 41 0 69830 0
vsize: 279484
[startup+530.101 s]
Raw data (loadavg): 1.00 0.83 0.42 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63952 0 0 0 52855 159 0 0 25 0 1 0 481067850 286191616 59307 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69871 59307 603 41 0 69830 0
vsize: 279484
[startup+540.101 s]
Raw data (loadavg): 1.00 0.83 0.43 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63958 0 0 0 53855 159 0 0 25 0 1 0 481067850 286326784 59313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69904 59313 603 41 0 69863 0
vsize: 279616
[startup+550.101 s]
Raw data (loadavg): 1.00 0.84 0.44 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63967 0 0 0 54856 159 0 0 25 0 1 0 481067850 286326784 59322 4294967295 134512640 134672761 3221224544 3221223760 134561982 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59322 603 41 0 69863 0
vsize: 279616
[startup+560.101 s]
Raw data (loadavg): 1.00 0.84 0.44 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63971 0 0 0 55855 159 0 0 25 0 1 0 481067850 286326784 59326 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59326 603 41 0 69863 0
vsize: 279616
[startup+570.101 s]
Raw data (loadavg): 1.00 0.85 0.45 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63975 0 0 0 56854 160 0 0 25 0 1 0 481067850 286326784 59330 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59330 603 41 0 69863 0
vsize: 279616
[startup+580.101 s]
Raw data (loadavg): 1.00 0.85 0.45 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63975 0 0 0 57854 160 0 0 25 0 1 0 481067850 286326784 59330 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69904 59330 603 41 0 69863 0
vsize: 279616
[startup+590.105 s]
Raw data (loadavg): 1.00 0.86 0.46 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63975 0 0 0 58854 160 0 0 25 0 1 0 481067850 286326784 59330 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69904 59330 603 41 0 69863 0
vsize: 279616
[startup+600.104 s]
Raw data (loadavg): 1.00 0.86 0.46 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63975 0 0 0 59854 160 0 0 25 0 1 0 481067850 286326784 59330 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69904 59330 603 41 0 69863 0
vsize: 279616
[startup+610.11 s]
Raw data (loadavg): 1.00 0.87 0.47 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63978 0 0 0 60855 160 0 0 25 0 1 0 481067850 286326784 59333 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69904 59333 603 41 0 69863 0
vsize: 279616
[startup+620.11 s]
Raw data (loadavg): 1.00 0.87 0.47 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63981 0 0 0 61855 160 0 0 25 0 1 0 481067850 286326784 59336 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69904 59336 603 41 0 69863 0
vsize: 279616
[startup+630.112 s]
Raw data (loadavg): 1.00 0.87 0.48 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63986 0 0 0 62856 160 0 0 25 0 1 0 481067850 286326784 59341 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69904 59341 603 41 0 69863 0
vsize: 279616
[startup+640.111 s]
Raw data (loadavg): 1.00 0.88 0.48 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 63992 0 0 0 63856 160 0 0 25 0 1 0 481067850 286326784 59347 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69904 59347 603 41 0 69863 0
vsize: 279616
[startup+650.111 s]
Raw data (loadavg): 1.00 0.88 0.49 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64000 0 0 0 64856 160 0 0 25 0 1 0 481067850 286461952 59355 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59355 603 41 0 69896 0
vsize: 279748
[startup+660.124 s]
Raw data (loadavg): 1.00 0.88 0.49 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64002 0 0 0 65857 160 0 0 25 0 1 0 481067850 286461952 59357 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59357 603 41 0 69896 0
vsize: 279748
[startup+670.124 s]
Raw data (loadavg): 1.00 0.89 0.50 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64003 0 0 0 66857 160 0 0 25 0 1 0 481067850 286461952 59358 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59358 603 41 0 69896 0
vsize: 279748
[startup+680.124 s]
Raw data (loadavg): 1.00 0.89 0.50 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64003 0 0 0 67858 160 0 0 25 0 1 0 481067850 286461952 59358 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59358 603 41 0 69896 0
vsize: 279748
[startup+690.124 s]
Raw data (loadavg): 1.00 0.89 0.51 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64004 0 0 0 68858 160 0 0 25 0 1 0 481067850 286461952 59359 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59359 603 41 0 69896 0
vsize: 279748
[startup+700.125 s]
Raw data (loadavg): 1.00 0.90 0.51 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64009 0 0 0 69858 160 0 0 25 0 1 0 481067850 286461952 59364 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59364 603 41 0 69896 0
vsize: 279748
[startup+710.125 s]
Raw data (loadavg): 1.00 0.90 0.52 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64019 0 0 0 70858 160 0 0 25 0 1 0 481067850 286461952 59374 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59374 603 41 0 69896 0
vsize: 279748
[startup+720.125 s]
Raw data (loadavg): 1.00 0.90 0.52 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64019 0 0 0 71858 160 0 0 25 0 1 0 481067850 286461952 59374 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59374 603 41 0 69896 0
vsize: 279748
[startup+730.13 s]
Raw data (loadavg): 1.00 0.91 0.53 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64020 0 0 0 72858 160 0 0 25 0 1 0 481067850 286461952 59375 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59375 603 41 0 69896 0
vsize: 279748
[startup+740.13 s]
Raw data (loadavg): 1.00 0.91 0.53 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64021 0 0 0 73858 160 0 0 25 0 1 0 481067850 286461952 59376 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59376 603 41 0 69896 0
vsize: 279748
[startup+750.13 s]
Raw data (loadavg): 1.00 0.91 0.54 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64023 0 0 0 74859 160 0 0 25 0 1 0 481067850 286461952 59378 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59378 603 41 0 69896 0
vsize: 279748
[startup+760.13 s]
Raw data (loadavg): 1.00 0.91 0.54 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64024 0 0 0 75859 160 0 0 25 0 1 0 481067850 286461952 59379 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59379 603 41 0 69896 0
vsize: 279748
[startup+770.131 s]
Raw data (loadavg): 1.00 0.92 0.55 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64025 0 0 0 76859 160 0 0 25 0 1 0 481067850 286461952 59380 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59380 603 41 0 69896 0
vsize: 279748
[startup+780.13 s]
Raw data (loadavg): 1.00 0.92 0.55 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64026 0 0 0 77859 160 0 0 25 0 1 0 481067850 286461952 59381 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59381 603 41 0 69896 0
vsize: 279748
[startup+790.139 s]
Raw data (loadavg): 1.00 0.92 0.55 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64026 0 0 0 78860 160 0 0 25 0 1 0 481067850 286461952 59381 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59381 603 41 0 69896 0
vsize: 279748
[startup+800.144 s]
Raw data (loadavg): 1.00 0.92 0.56 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64027 0 0 0 79861 160 0 0 25 0 1 0 481067850 286461952 59382 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59382 603 41 0 69896 0
vsize: 279748
[startup+810.144 s]
Raw data (loadavg): 1.00 0.92 0.56 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64028 0 0 0 80861 160 0 0 25 0 1 0 481067850 286461952 59383 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59383 603 41 0 69896 0
vsize: 279748
[startup+820.144 s]
Raw data (loadavg): 1.00 0.93 0.57 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64033 0 0 0 81861 160 0 0 25 0 1 0 481067850 286461952 59388 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59388 603 41 0 69896 0
vsize: 279748
[startup+830.143 s]
Raw data (loadavg): 1.00 0.93 0.57 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64033 0 0 0 82861 160 0 0 25 0 1 0 481067850 286461952 59388 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59388 603 41 0 69896 0
vsize: 279748
[startup+840.152 s]
Raw data (loadavg): 1.08 0.95 0.58 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64034 0 0 0 83862 160 0 0 25 0 1 0 481067850 286461952 59389 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59389 603 41 0 69896 0
vsize: 279748
[startup+850.152 s]
Raw data (loadavg): 1.07 0.95 0.58 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64035 0 0 0 84862 160 0 0 25 0 1 0 481067850 286461952 59390 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59390 603 41 0 69896 0
vsize: 279748
[startup+860.152 s]
Raw data (loadavg): 1.06 0.95 0.59 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64036 0 0 0 85863 160 0 0 25 0 1 0 481067850 286461952 59391 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59391 603 41 0 69896 0
vsize: 279748
[startup+870.16 s]
Raw data (loadavg): 1.05 0.95 0.59 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64048 0 0 0 86864 160 0 0 25 0 1 0 481067850 286597120 59403 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59403 603 41 0 69929 0
vsize: 279880
[startup+880.16 s]
Raw data (loadavg): 1.04 0.95 0.59 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64049 0 0 0 87864 160 0 0 25 0 1 0 481067850 286597120 59404 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59404 603 41 0 69929 0
vsize: 279880
[startup+890.161 s]
Raw data (loadavg): 1.03 0.95 0.60 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64052 0 0 0 88864 160 0 0 25 0 1 0 481067850 286597120 59407 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59407 603 41 0 69929 0
vsize: 279880
[startup+900.161 s]
Raw data (loadavg): 1.03 0.95 0.60 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64052 0 0 0 89864 160 0 0 25 0 1 0 481067850 286597120 59407 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59407 603 41 0 69929 0
vsize: 279880
[startup+910.168 s]
Raw data (loadavg): 1.10 0.97 0.61 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64053 0 0 0 90865 160 0 0 25 0 1 0 481067850 286597120 59408 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59408 603 41 0 69929 0
vsize: 279880
[startup+920.168 s]
Raw data (loadavg): 1.09 0.97 0.62 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64054 0 0 0 91865 160 0 0 25 0 1 0 481067850 286597120 59409 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59409 603 41 0 69929 0
vsize: 279880
[startup+930.168 s]
Raw data (loadavg): 1.07 0.97 0.62 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64055 0 0 0 92865 160 0 0 25 0 1 0 481067850 286597120 59410 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59410 603 41 0 69929 0
vsize: 279880
[startup+940.169 s]
Raw data (loadavg): 1.06 0.97 0.62 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64057 0 0 0 93866 160 0 0 25 0 1 0 481067850 286597120 59412 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59412 603 41 0 69929 0
vsize: 279880
[startup+950.169 s]
Raw data (loadavg): 1.05 0.97 0.63 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64061 0 0 0 94866 160 0 0 25 0 1 0 481067850 286597120 59416 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59416 603 41 0 69929 0
vsize: 279880
[startup+960.168 s]
Raw data (loadavg): 1.04 0.97 0.63 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64061 0 0 0 95866 160 0 0 25 0 1 0 481067850 286597120 59416 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59416 603 41 0 69929 0
vsize: 279880
[startup+970.168 s]
Raw data (loadavg): 1.04 0.97 0.64 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64063 0 0 0 96866 160 0 0 25 0 1 0 481067850 286597120 59418 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59418 603 41 0 69929 0
vsize: 279880
[startup+980.169 s]
Raw data (loadavg): 1.03 0.97 0.64 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64065 0 0 0 97866 160 0 0 25 0 1 0 481067850 286597120 59420 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59420 603 41 0 69929 0
vsize: 279880
[startup+990.17 s]
Raw data (loadavg): 1.02 0.97 0.64 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64067 0 0 0 98866 160 0 0 25 0 1 0 481067850 286597120 59422 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59422 603 41 0 69929 0
vsize: 279880
[startup+1000.17 s]
Raw data (loadavg): 1.02 0.97 0.64 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64078 0 0 0 99866 160 0 0 25 0 1 0 481067850 286732288 59433 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70003 59433 603 41 0 69962 0
vsize: 280012
[startup+1010.17 s]
Raw data (loadavg): 1.02 0.97 0.65 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64081 0 0 0 100866 160 0 0 25 0 1 0 481067850 286732288 59436 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70003 59436 603 41 0 69962 0
vsize: 280012
[startup+1020.17 s]
Raw data (loadavg): 1.01 0.97 0.65 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64086 0 0 0 101866 160 0 0 25 0 1 0 481067850 286732288 59441 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70003 59441 603 41 0 69962 0
vsize: 280012
[startup+1030.17 s]
Raw data (loadavg): 1.01 0.97 0.65 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64102 0 0 0 102866 160 0 0 25 0 1 0 481067850 286732288 59457 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70003 59457 603 41 0 69962 0
vsize: 280012
[startup+1040.17 s]
Raw data (loadavg): 1.01 0.97 0.66 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64106 0 0 0 103867 160 0 0 25 0 1 0 481067850 286732288 59461 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70003 59461 603 41 0 69962 0
vsize: 280012
[startup+1050.18 s]
Raw data (loadavg): 1.01 0.97 0.66 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64106 0 0 0 104868 160 0 0 25 0 1 0 481067850 286732288 59461 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70003 59461 603 41 0 69962 0
vsize: 280012
[startup+1060.18 s]
Raw data (loadavg): 1.01 0.97 0.66 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64106 0 0 0 105868 160 0 0 25 0 1 0 481067850 286732288 59461 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70003 59461 603 41 0 69962 0
vsize: 280012
[startup+1070.18 s]
Raw data (loadavg): 1.00 0.97 0.66 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64108 0 0 0 106868 160 0 0 25 0 1 0 481067850 286732288 59463 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70003 59463 603 41 0 69962 0
vsize: 280012
[startup+1080.19 s]
Raw data (loadavg): 1.00 0.97 0.67 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64114 0 0 0 107869 161 0 0 25 0 1 0 481067850 286732288 59469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70003 59469 603 41 0 69962 0
vsize: 280012
[startup+1090.19 s]
Raw data (loadavg): 1.00 0.97 0.67 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64125 0 0 0 108869 161 0 0 25 0 1 0 481067850 286732288 59480 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70003 59480 603 41 0 69962 0
vsize: 280012
[startup+1100.19 s]
Raw data (loadavg): 1.00 0.97 0.67 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64125 0 0 0 109869 161 0 0 25 0 1 0 481067850 286732288 59480 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70003 59480 603 41 0 69962 0
vsize: 280012
[startup+1110.19 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64126 0 0 0 110869 161 0 0 25 0 1 0 481067850 286732288 59481 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70003 59481 603 41 0 69962 0
vsize: 280012
[startup+1120.19 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64127 0 0 0 111870 161 0 0 25 0 1 0 481067850 286867456 59482 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70036 59482 603 41 0 69995 0
vsize: 280144
[startup+1130.19 s]
Raw data (loadavg): 1.00 0.97 0.68 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64127 0 0 0 112870 161 0 0 25 0 1 0 481067850 286867456 59482 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70036 59482 603 41 0 69995 0
vsize: 280144
[startup+1140.23 s]
Raw data (loadavg): 1.00 0.97 0.69 3/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64129 0 0 0 113874 161 0 0 25 0 1 0 481067850 286867456 59484 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70036 59484 603 41 0 69995 0
vsize: 280144
[startup+1150.24 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64130 0 0 0 114875 161 0 0 25 0 1 0 481067850 286867456 59485 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70036 59485 603 41 0 69995 0
vsize: 280144
[startup+1160.24 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64130 0 0 0 115875 161 0 0 25 0 1 0 481067850 286867456 59485 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70036 59485 603 41 0 69995 0
vsize: 280144
[startup+1170.24 s]
Raw data (loadavg): 1.00 0.97 0.69 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64131 0 0 0 116875 161 0 0 25 0 1 0 481067850 286867456 59486 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70036 59486 603 41 0 69995 0
vsize: 280144
[startup+1180.24 s]
Raw data (loadavg): 1.00 0.97 0.70 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64131 0 0 0 117875 161 0 0 25 0 1 0 481067850 286867456 59486 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70036 59486 603 41 0 69995 0
vsize: 280144
[startup+1190.24 s]
Raw data (loadavg): 1.00 0.97 0.70 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64131 0 0 0 118875 161 0 0 25 0 1 0 481067850 286867456 59486 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70036 59486 603 41 0 69995 0
vsize: 280144
[startup+1200.24 s]
Raw data (loadavg): 1.00 0.97 0.70 2/54 21496
Raw data (stat): 21496 (minisat+) R 21495 32461 32460 0 -1 0 64132 0 0 0 119876 161 0 0 25 0 1 0 481067850 286867456 59487 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70036 59487 603 41 0 69995 0
vsize: 280144
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.78 s]
Raw data (loadavg): 1.00 0.97 0.70 1/54 21496
Raw data (stat): 21496 (minisat+) Z 21495 32461 32460 0 -1 12 64134 0 0 0 119876 172 0 0 22 0 1 0 481067850 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.78
CPU time (s): 1200.49
CPU user time (s): 1198.76
CPU system time (s): 1.72874
CPU usage (%): 99.9756
Max. virtual memory (Kb): 280144
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####