PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        235424 kB
Buffers:         18576 kB
Cached:         756828 kB
SwapCached:          0 kB
Active:         134600 kB
Inactive:       643700 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        235172 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            15236 kB
Committed_AS:    63792 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 23:41:58 (client local time) WITH STATUS 0 IN 1210.36 SECONDS
stats: 20252 7 1210.36 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 | 1641312  5475838 |  492393       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/545303          
c   -- var.elim.:  2000/545303          
c   -- var.elim.:  3000/545303          
c   -- var.elim.:  4000/545303          
c   -- var.elim.:  5000/545303          
c   -- var.elim.:  6000/545303          
c   -- var.elim.:  7000/545303          
c   -- var.elim.:  8000/545303          
c   -- var.elim.:  9000/545303          
c   -- var.elim.:  10000/545303          
c   -- var.elim.:  11000/545303          
c   -- var.elim.:  12000/545303          
c   -- var.elim.:  13000/545303          
c   -- var.elim.:  14000/545303          
c   -- var.elim.:  15000/545303          
c   -- var.elim.:  16000/545303          
c   -- var.elim.:  17000/545303          
c   -- var.elim.:  18000/545303          
c   -- v#### 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.89 0.95 0.92 2/55 31166
Raw data (stat): 31166 (runsolver) R 31165 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 417623964 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.91 0.95 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 16991 0 0 0 955 44 0 0 25 0 1 0 417623964 64348160 13741 4294967295 134512640 134672761 3221224544 3221222112 134523752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15710 13741 603 41 0 15669 0
vsize: 62840
[startup+20.001 s]
Raw data (loadavg): 0.92 0.96 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 66940 0 0 0 1829 168 0 0 25 0 1 0 417623964 283734016 62294 4294967295 134512640 134672761 3221224544 3220825376 134604055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69271 62294 603 41 0 69230 0
vsize: 277084
[startup+30.0016 s]
Raw data (loadavg): 0.93 0.96 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 87304 0 0 0 2768 221 0 0 25 0 1 0 417623964 402821120 82657 4294967295 134512640 134672761 3221224544 3221223088 134621107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 98345 82657 603 41 0 98304 0
vsize: 393380
[startup+40.0013 s]
Raw data (loadavg): 0.94 0.96 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 87304 0 0 0 3768 221 0 0 25 0 1 0 417623964 402821120 82657 4294967295 134512640 134672761 3221224544 3221223088 134621179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 98345 82657 603 41 0 98304 0
vsize: 393380
[startup+50.001 s]
Raw data (loadavg): 0.95 0.96 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 87304 0 0 0 4768 221 0 0 25 0 1 0 417623964 402821120 82657 4294967295 134512640 134672761 3221224544 3221223184 134622620 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 98345 82657 603 41 0 98304 0
vsize: 393380
[startup+60.001 s]
Raw data (loadavg): 0.96 0.96 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 88767 0 0 0 5764 225 0 0 25 0 1 0 417623964 412618752 84120 4294967295 134512640 134672761 3221224544 3221223136 134621359 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100737 84120 603 41 0 100696 0
vsize: 402948
[startup+70.0013 s]
Raw data (loadavg): 0.96 0.96 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 93149 0 0 0 6746 241 0 0 25 0 1 0 417623964 418177024 85939 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 102094 85939 603 41 0 102053 0
vsize: 408376
[startup+80.001 s]
Raw data (loadavg): 0.97 0.96 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 95412 0 0 0 7734 253 0 0 25 0 1 0 417623964 427741184 88202 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 104429 88202 603 41 0 104388 0
vsize: 417716
[startup+90.0007 s]
Raw data (loadavg): 0.97 0.96 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 96940 0 0 0 8724 261 0 0 25 0 1 0 417623964 434434048 89730 4294967295 134512640 134672761 3221224544 3221222992 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 106063 89730 603 41 0 106022 0
vsize: 424252
[startup+100 s]
Raw data (loadavg): 0.98 0.96 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 98589 0 0 0 9714 271 0 0 25 0 1 0 417623964 441298944 91379 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 107739 91379 603 41 0 107698 0
vsize: 430956
[startup+110.001 s]
Raw data (loadavg): 0.98 0.96 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 99989 0 0 0 10706 278 0 0 25 0 1 0 417623964 447410176 92779 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109231 92779 603 41 0 109190 0
vsize: 436924
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 101177 0 0 0 11699 285 0 0 25 0 1 0 417623964 452919296 93967 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110576 93967 603 41 0 110535 0
vsize: 442304
[startup+130.001 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 102388 0 0 0 12693 289 0 0 25 0 1 0 417623964 458141696 95178 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111851 95178 603 41 0 111810 0
vsize: 447404
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 103445 0 0 0 13689 293 0 0 25 0 1 0 417623964 462782464 96235 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 112984 96235 603 41 0 112943 0
vsize: 451936
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 104293 0 0 0 14685 297 0 0 25 0 1 0 417623964 466411520 97083 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113870 97083 603 41 0 113829 0
vsize: 455480
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 105170 0 0 0 15681 301 0 0 25 0 1 0 417623964 470003712 97960 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114747 97960 603 41 0 114706 0
vsize: 458988
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 106506 0 0 0 16673 310 0 0 25 0 1 0 417623964 475643904 99296 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116124 99296 603 41 0 116083 0
vsize: 464496
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 108068 0 0 0 17663 317 0 0 25 0 1 0 417623964 482729984 100858 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117854 100858 603 41 0 117813 0
vsize: 471416
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 109549 0 0 0 18656 324 0 0 25 0 1 0 417623964 488861696 102339 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119351 102339 603 41 0 119310 0
vsize: 477404
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 110219 0 0 0 19649 330 0 0 25 0 1 0 417623964 491581440 103009 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120015 103009 603 41 0 119974 0
vsize: 480060
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 111379 0 0 0 20641 336 0 0 25 0 1 0 417623964 496656384 104169 4294967295 134512640 134672761 3221224544 3221222824 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121254 104169 603 41 0 121213 0
vsize: 485016
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 113377 0 0 0 21631 345 0 0 25 0 1 0 417623964 505110528 106167 4294967295 134512640 134672761 3221224544 3221221984 134566712 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123318 106167 603 41 0 123277 0
vsize: 493272
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 115070 0 0 0 22622 353 0 0 25 0 1 0 417623964 512675840 107860 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125165 107860 603 41 0 125124 0
vsize: 500660
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 116464 0 0 0 23615 359 0 0 25 0 1 0 417623964 518713344 109254 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 126639 109254 603 41 0 126598 0
vsize: 506556
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 117790 0 0 0 24609 365 0 0 25 0 1 0 417623964 524132352 110580 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 127962 110580 603 41 0 127921 0
vsize: 511848
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 118949 0 0 0 25603 369 0 0 25 0 1 0 417623964 528756736 111739 4294967295 134512640 134672761 3221224544 3221222960 134644235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 129091 111739 603 41 0 129050 0
vsize: 516364
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 119892 0 0 0 26600 373 0 0 25 0 1 0 417623964 532811776 112682 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 130081 112682 603 41 0 130040 0
vsize: 520324
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 120739 0 0 0 27595 378 0 0 25 0 1 0 417623964 536469504 113529 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 130974 113529 603 41 0 130933 0
vsize: 523896
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 121705 0 0 0 28592 382 0 0 25 0 1 0 417623964 540835840 114495 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 132040 114495 603 41 0 131999 0
vsize: 528160
[startup+300.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 122633 0 0 0 29588 386 0 0 25 0 1 0 417623964 545099776 115423 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 133081 115423 603 41 0 133040 0
vsize: 532324
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 123644 0 0 0 30585 389 0 0 25 0 1 0 417623964 550494208 116434 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134398 116434 603 41 0 134357 0
vsize: 537592
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 124544 0 0 0 31582 391 0 0 25 0 1 0 417623964 555077632 117334 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135517 117334 603 41 0 135476 0
vsize: 542068
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 125273 0 0 0 32578 396 0 0 25 0 1 0 417623964 558616576 118063 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136381 118063 603 41 0 136340 0
vsize: 545524
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 125841 0 0 0 33574 400 0 0 25 0 1 0 417623964 560869376 118631 4294967295 134512640 134672761 3221224544 3221222720 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136931 118631 603 41 0 136890 0
vsize: 547724
[startup+350 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 126520 0 0 0 34571 403 0 0 25 0 1 0 417623964 563855360 119310 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 137660 119310 603 41 0 137619 0
vsize: 550640
[startup+360.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 127220 0 0 0 35568 406 0 0 25 0 1 0 417623964 567091200 120010 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138450 120010 603 41 0 138409 0
vsize: 553800
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 127912 0 0 0 36566 409 0 0 25 0 1 0 417623964 570474496 120702 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139276 120702 603 41 0 139235 0
vsize: 557104
[startup+380 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 128480 0 0 0 37564 411 0 0 25 0 1 0 417623964 573071360 121270 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139910 121270 603 41 0 139869 0
vsize: 559640
[startup+390 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 129202 0 0 0 38561 414 0 0 25 0 1 0 417623964 576278528 121992 4294967295 134512640 134672761 3221224544 3221222832 134603506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 140693 121992 603 41 0 140652 0
vsize: 562772
[startup+400 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 129906 0 0 0 39558 417 0 0 25 0 1 0 417623964 579559424 122696 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141494 122696 603 41 0 141453 0
vsize: 565976
[startup+409.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 130558 0 0 0 40555 420 0 0 25 0 1 0 417623964 582475776 123348 4294967295 134512640 134672761 3221224544 3221222992 134606977 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142206 123348 603 41 0 142165 0
vsize: 568824
[startup+419.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 131221 0 0 0 41553 422 0 0 25 0 1 0 417623964 585367552 124011 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142912 124011 603 41 0 142871 0
vsize: 571648
[startup+429.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 131960 0 0 0 42550 425 0 0 25 0 1 0 417623964 588845056 124750 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143761 124750 603 41 0 143720 0
vsize: 575044
[startup+439.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 132675 0 0 0 43548 428 0 0 25 0 1 0 417623964 592187392 125465 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144577 125465 603 41 0 144536 0
vsize: 578308
[startup+449.998 s]
Raw data (loadavg): 1.07 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 133388 0 0 0 44546 430 0 0 25 0 1 0 417623964 595566592 126178 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145402 126178 603 41 0 145361 0
vsize: 581608
[startup+459.998 s]
Raw data (loadavg): 1.06 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 134063 0 0 0 45543 433 0 0 25 0 1 0 417623964 598618112 126853 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146147 126853 603 41 0 146106 0
vsize: 584588
[startup+469.998 s]
Raw data (loadavg): 1.05 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 134689 0 0 0 46541 435 0 0 25 0 1 0 417623964 601526272 127479 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146857 127479 603 41 0 146816 0
vsize: 587428
[startup+479.998 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 135239 0 0 0 47538 438 0 0 25 0 1 0 417623964 603971584 128029 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 147454 128029 603 41 0 147413 0
vsize: 589816
[startup+489.998 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 135586 0 0 0 48534 443 0 0 25 0 1 0 417623964 605409280 128376 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 147805 128376 603 41 0 147764 0
vsize: 591220
[startup+499.998 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 135735 0 0 0 49531 446 0 0 25 0 1 0 417623964 605851648 128525 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 147913 128525 603 41 0 147872 0
vsize: 591652
[startup+509.997 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 136196 0 0 0 50527 449 0 0 25 0 1 0 417623964 608055296 128986 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 148451 128986 603 41 0 148410 0
vsize: 593804
[startup+519.997 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 136623 0 0 0 51524 453 0 0 25 0 1 0 417623964 609837056 129413 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 148886 129413 603 41 0 148845 0
vsize: 595544
[startup+529.997 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 137265 0 0 0 52521 456 0 0 25 0 1 0 417623964 612990976 130055 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 149656 130055 603 41 0 149615 0
vsize: 598624
[startup+539.997 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 137688 0 0 0 53518 458 0 0 25 0 1 0 417623964 614952960 130478 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150135 130478 603 41 0 150094 0
vsize: 600540
[startup+549.996 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 137781 0 0 0 54517 460 0 0 25 0 1 0 417623964 614952960 130571 4294967295 134512640 134672761 3221224544 3221223024 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150135 130571 603 41 0 150094 0
vsize: 600540
[startup+559.997 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 137968 0 0 0 55516 461 0 0 25 0 1 0 417623964 615264256 130758 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150211 130758 603 41 0 150170 0
vsize: 600844
[startup+569.996 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 138275 0 0 0 56513 464 0 0 25 0 1 0 417623964 616570880 131065 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150530 131065 603 41 0 150489 0
vsize: 602120
[startup+579.996 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 138610 0 0 0 57511 466 0 0 25 0 1 0 417623964 618598400 131400 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151025 131400 603 41 0 150984 0
vsize: 604100
[startup+589.997 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 138858 0 0 0 58510 467 0 0 25 0 1 0 417623964 619778048 131648 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151313 131648 603 41 0 151272 0
vsize: 605252
[startup+599.997 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 139067 0 0 0 59508 469 0 0 25 0 1 0 417623964 620597248 131857 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151513 131857 603 41 0 151472 0
vsize: 606052
[startup+609.997 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 139401 0 0 0 60507 471 0 0 25 0 1 0 417623964 622084096 132191 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151876 132191 603 41 0 151835 0
vsize: 607504
[startup+619.997 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 139850 0 0 0 61505 473 0 0 25 0 1 0 417623964 624934912 132640 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 152572 132640 603 41 0 152531 0
vsize: 610288
[startup+629.996 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 140327 0 0 0 62503 475 0 0 25 0 1 0 417623964 627658752 133117 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 153237 133117 603 41 0 153196 0
vsize: 612948
[startup+639.996 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 140799 0 0 0 63501 477 0 0 25 0 1 0 417623964 630603776 133589 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 153956 133589 603 41 0 153915 0
vsize: 615824
[startup+649.996 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 141268 0 0 0 64499 480 0 0 25 0 1 0 417623964 633245696 134058 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 154601 134058 603 41 0 154560 0
vsize: 618404
[startup+659.998 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 141745 0 0 0 65497 482 0 0 25 0 1 0 417623964 635899904 134535 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 155249 134535 603 41 0 155208 0
vsize: 620996
[startup+669.998 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 142198 0 0 0 66495 484 0 0 25 0 1 0 417623964 638078976 134988 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 155781 134988 603 41 0 155740 0
vsize: 623124
[startup+679.998 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 142568 0 0 0 67493 486 0 0 25 0 1 0 417623964 639729664 135358 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156184 135358 603 41 0 156143 0
vsize: 624736
[startup+689.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 143033 0 0 0 68491 489 0 0 25 0 1 0 417623964 641974272 135823 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156732 135823 603 41 0 156691 0
vsize: 626928
[startup+699.998 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 143474 0 0 0 69489 491 0 0 25 0 1 0 417623964 644222976 136264 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 157281 136264 603 41 0 157240 0
vsize: 629124
[startup+709.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 143929 0 0 0 70487 493 0 0 25 0 1 0 417623964 646393856 136719 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 157811 136719 603 41 0 157770 0
vsize: 631244
[startup+719.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 144401 0 0 0 71487 494 0 0 25 0 1 0 417623964 648671232 137191 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 158367 137191 603 41 0 158326 0
vsize: 633468
[startup+729.998 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 144877 0 0 0 72485 495 0 0 25 0 1 0 417623964 651071488 137667 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 158953 137667 603 41 0 158912 0
vsize: 635812
[startup+739.998 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 145263 0 0 0 73483 497 0 0 25 0 1 0 417623964 652845056 138053 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 159386 138053 603 41 0 159345 0
vsize: 637544
[startup+749.998 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 145649 0 0 0 74481 499 0 0 25 0 1 0 417623964 654254080 138439 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 159730 138439 603 41 0 159689 0
vsize: 638920
[startup+759.998 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 146050 0 0 0 75480 501 0 0 25 0 1 0 417623964 655831040 138840 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 160115 138840 603 41 0 160074 0
vsize: 640460
[startup+769.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 146482 0 0 0 76478 503 0 0 25 0 1 0 417623964 657707008 139272 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 160573 139272 603 41 0 160532 0
vsize: 642292
[startup+779.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 146937 0 0 0 77476 505 0 0 25 0 1 0 417623964 659755008 139727 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 161073 139727 603 41 0 161032 0
vsize: 644292
[startup+789.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 147330 0 0 0 78474 507 0 0 25 0 1 0 417623964 661471232 140120 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 161492 140120 603 41 0 161451 0
vsize: 645968
[startup+799.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 147782 0 0 0 79473 509 0 0 25 0 1 0 417623964 663322624 140572 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 161944 140572 603 41 0 161903 0
vsize: 647776
[startup+810 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 148237 0 0 0 80471 511 0 0 25 0 1 0 417623964 665165824 141027 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 162394 141027 603 41 0 162353 0
vsize: 649576
[startup+819.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 148665 0 0 0 81469 513 0 0 25 0 1 0 417623964 666984448 141455 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 162838 141455 603 41 0 162797 0
vsize: 651352
[startup+829.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 149135 0 0 0 82467 515 0 0 25 0 1 0 417623964 669118464 141925 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 163359 141925 603 41 0 163318 0
vsize: 653436
[startup+839.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 149606 0 0 0 83465 517 0 0 25 0 1 0 417623964 671608832 142396 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 163967 142396 603 41 0 163926 0
vsize: 655868
[startup+849.998 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 149994 0 0 0 84464 518 0 0 25 0 1 0 417623964 673431552 142784 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 164412 142784 603 41 0 164371 0
vsize: 657648
[startup+859.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 150423 0 0 0 85461 520 0 0 25 0 1 0 417623964 675180544 143213 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 164839 143213 603 41 0 164798 0
vsize: 659356
[startup+869.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 150869 0 0 0 86458 523 0 0 25 0 1 0 417623964 677355520 143659 4294967295 134512640 134672761 3221224544 3221221984 134566712 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 165370 143659 603 41 0 165329 0
vsize: 661480
[startup+879.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 151372 0 0 0 87456 525 0 0 25 0 1 0 417623964 679997440 144162 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 166015 144162 603 41 0 165974 0
vsize: 664060
[startup+889.999 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 151683 0 0 0 88453 528 0 0 25 0 1 0 417623964 681320448 144473 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 166338 144473 603 41 0 166297 0
vsize: 665352
[startup+900.114 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 151865 0 0 0 89462 531 0 0 25 0 1 0 417623964 681992192 144655 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 166502 144655 603 41 0 166461 0
vsize: 666008
[startup+910.115 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 152351 0 0 0 90460 533 0 0 25 0 1 0 417623964 684871680 145141 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 167205 145141 603 41 0 167164 0
vsize: 668820
[startup+920.114 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 152765 0 0 0 91456 536 0 0 25 0 1 0 417623964 687394816 145555 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 167821 145555 603 41 0 167780 0
vsize: 671284
[startup+930.114 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 152981 0 0 0 92455 538 0 0 25 0 1 0 417623964 688472064 145771 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168084 145771 603 41 0 168043 0
vsize: 672336
[startup+940.114 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 153216 0 0 0 93452 541 0 0 25 0 1 0 417623964 689651712 146006 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168372 146006 603 41 0 168331 0
vsize: 673488
[startup+950.113 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 153576 0 0 0 94450 543 0 0 25 0 1 0 417623964 691646464 146366 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 168859 146366 603 41 0 168818 0
vsize: 675436
[startup+960.114 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 154222 0 0 0 95447 547 0 0 25 0 1 0 417623964 694595584 147012 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169579 147012 603 41 0 169538 0
vsize: 678316
[startup+970.114 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 154843 0 0 0 96444 549 0 0 25 0 1 0 417623964 697888768 147633 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170383 147633 603 41 0 170342 0
vsize: 681532
[startup+980.113 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 155371 0 0 0 97440 553 0 0 25 0 1 0 417623964 701030400 148161 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171150 148161 603 41 0 171109 0
vsize: 684600
[startup+990.113 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 155648 0 0 0 98437 555 0 0 25 0 1 0 417623964 702177280 148438 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171430 148438 603 41 0 171389 0
vsize: 685720
[startup+1000.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 155921 0 0 0 99436 557 0 0 25 0 1 0 417623964 703320064 148711 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171709 148711 603 41 0 171668 0
vsize: 686836
[startup+1010.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 156170 0 0 0 100434 559 0 0 25 0 1 0 417623964 704303104 148960 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171949 148960 603 41 0 171908 0
vsize: 687796
[startup+1020.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 156497 0 0 0 101431 562 0 0 25 0 1 0 417623964 706101248 149287 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 172388 149287 603 41 0 172347 0
vsize: 689552
[startup+1030.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 157067 0 0 0 102428 565 0 0 25 0 1 0 417623964 708784128 149857 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 173043 149857 603 41 0 173002 0
vsize: 692172
[startup+1040.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 157599 0 0 0 103425 567 0 0 25 0 1 0 417623964 711442432 150389 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 173692 150389 603 41 0 173651 0
vsize: 694768
[startup+1050.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 158253 0 0 0 104423 569 0 0 25 0 1 0 417623964 714756096 151043 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 174501 151043 603 41 0 174460 0
vsize: 698004
[startup+1060.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 158832 0 0 0 105419 573 0 0 25 0 1 0 417623964 717160448 151622 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 175088 151622 603 41 0 175047 0
vsize: 700352
[startup+1070.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 159393 0 0 0 106416 576 0 0 25 0 1 0 417623964 719900672 152183 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 175757 152183 603 41 0 175716 0
vsize: 703028
[startup+1080.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 159816 0 0 0 107414 579 0 0 25 0 1 0 417623964 721420288 152606 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 176128 152606 603 41 0 176087 0
vsize: 704512
[startup+1090.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 160393 0 0 0 108410 582 0 0 25 0 1 0 417623964 723886080 153183 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 176730 153183 603 41 0 176689 0
vsize: 706920
[startup+1100.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 161013 0 0 0 109408 584 0 0 25 0 1 0 417623964 726708224 153803 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 177419 153803 603 41 0 177378 0
vsize: 709676
[startup+1110.12 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 161482 0 0 0 110406 586 0 0 25 0 1 0 417623964 728555520 154272 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 177870 154272 603 41 0 177829 0
vsize: 711480
[startup+1120.12 s]
Raw data (loadavg): 1.07 1.00 0.93 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 161900 0 0 0 111404 588 0 0 25 0 1 0 417623964 730656768 154690 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 178383 154690 603 41 0 178342 0
vsize: 713532
[startup+1130.12 s]
Raw data (loadavg): 1.06 1.00 0.93 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 162398 0 0 0 112401 591 0 0 25 0 1 0 417623964 732758016 155188 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 178896 155188 603 41 0 178855 0
vsize: 715584
[startup+1140.12 s]
Raw data (loadavg): 1.05 1.00 0.93 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 162796 0 0 0 113399 593 0 0 25 0 1 0 417623964 734666752 155586 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 179362 155586 603 41 0 179321 0
vsize: 717448
[startup+1150.12 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 163213 0 0 0 114398 595 0 0 25 0 1 0 417623964 736591872 156003 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 179832 156003 603 41 0 179791 0
vsize: 719328
[startup+1160.12 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 163670 0 0 0 115395 598 0 0 25 0 1 0 417623964 738463744 156460 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 180289 156460 603 41 0 180248 0
vsize: 721156
[startup+1170.12 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 164174 0 0 0 116392 601 0 0 25 0 1 0 417623964 740823040 156964 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 180865 156964 603 41 0 180824 0
vsize: 723460
[startup+1180.12 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 164789 0 0 0 117390 603 0 0 25 0 1 0 417623964 744349696 157579 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 181726 157579 603 41 0 181685 0
vsize: 726904
[startup+1190.12 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 165341 0 0 0 118388 605 0 0 25 0 1 0 417623964 746975232 158131 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 182367 158131 603 41 0 182326 0
vsize: 729468
[startup+1200.12 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 165829 0 0 0 119386 608 0 0 25 0 1 0 417623964 749391872 158619 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 182957 158619 603 41 0 182916 0
vsize: 731828
[startup+1210.12 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 31166
Raw data (stat): 31166 (minisat+) R 31165 30927 30926 0 -1 0 166373 0 0 0 120384 610 0 0 25 0 1 0 417623964 752291840 159163 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 183665 159163 603 41 0 183624 0
vsize: 734660
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.54 s]
Raw data (loadavg): 1.01 1.00 0.93 1/55 31166
Raw data (stat): 31166 (minisat+) Z 31165 30927 30926 0 -1 12 166373 0 0 0 120384 651 0 0 25 0 1 0 417623964 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): 1210.53
CPU time (s): 1210.36
CPU user time (s): 1203.84
CPU system time (s): 6.51801
CPU usage (%): 99.9856
Max. virtual memory (Kb): 734660
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####