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 20265

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        592072 kB
Buffers:         28084 kB
Cached:         390824 kB
SwapCached:        516 kB
Active:          38960 kB
Inactive:       381896 kB
HighTotal:      131008 kB
HighFree:        13188 kB
LowTotal:       903652 kB
LowFree:        578884 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            16136 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 20:51:40 (client local time) WITH STATUS 0 IN 1200.45 SECONDS
stats: 15247 7 1200.45 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.97 0.98 0.91 2/54 12144
Raw data (stat): 12144 (runsolver) R 12143 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547979916 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.97 0.98 0.91 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 16991 0 0 0 954 44 0 0 25 0 1 0 547979916 64348160 13741 4294967295 134512640 134672761 3221224544 3221222112 134523717 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.0013 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 67021 0 0 0 1831 168 0 0 25 0 1 0 547979916 284004352 62375 4294967295 134512640 134672761 3221224544 3220925040 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69337 62376 603 41 0 69296 0
vsize: 277348
[startup+30.0022 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 87304 0 0 0 2779 220 0 0 25 0 1 0 547979916 402821120 82657 4294967295 134512640 134672761 3221224544 3221223088 134621062 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.0027 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 87304 0 0 0 3779 220 0 0 25 0 1 0 547979916 402821120 82657 4294967295 134512640 134672761 3221224544 3221223108 1075346974 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.0024 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 87304 0 0 0 4779 220 0 0 25 0 1 0 547979916 402821120 82657 4294967295 134512640 134672761 3221224544 3221223088 134621090 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.0022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 88767 0 0 0 5776 223 0 0 25 0 1 0 547979916 412618752 84120 4294967295 134512640 134672761 3221224544 3221223136 134621211 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.0019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 93221 0 0 0 6761 238 0 0 25 0 1 0 547979916 418582528 86011 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 102193 86011 603 41 0 102152 0
vsize: 408772
[startup+80.0026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 95440 0 0 0 7750 250 0 0 25 0 1 0 547979916 427876352 88230 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 104462 88230 603 41 0 104421 0
vsize: 417848
[startup+90.0026 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 96985 0 0 0 8741 258 0 0 25 0 1 0 547979916 434569216 89775 4294967295 134512640 134672761 3221224544 3221222668 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 106096 89775 603 41 0 106055 0
vsize: 424384
[startup+100.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 98635 0 0 0 9732 267 0 0 25 0 1 0 547979916 441573376 91425 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 107806 91425 603 41 0 107765 0
vsize: 431224
[startup+110.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 100019 0 0 0 10727 272 0 0 25 0 1 0 547979916 447545344 92809 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109264 92809 603 41 0 109223 0
vsize: 437056
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 101213 0 0 0 11721 278 0 0 25 0 1 0 547979916 453054464 94003 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110609 94003 603 41 0 110568 0
vsize: 442436
[startup+130.003 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 102415 0 0 0 12717 282 0 0 25 0 1 0 547979916 458276864 95205 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111884 95205 603 41 0 111843 0
vsize: 447536
[startup+140.003 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 103470 0 0 0 13712 287 0 0 25 0 1 0 547979916 462782464 96260 4294967295 134512640 134672761 3221224544 3221222208 134566712 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112984 96261 603 41 0 112943 0
vsize: 451936
[startup+150.011 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 104335 0 0 0 14709 291 0 0 25 0 1 0 547979916 466558976 97125 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113906 97125 603 41 0 113865 0
vsize: 455624
[startup+160.011 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 105195 0 0 0 15705 294 0 0 25 0 1 0 547979916 470142976 97985 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114781 97985 603 41 0 114740 0
vsize: 459124
[startup+170.011 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 106624 0 0 0 16695 304 0 0 25 0 1 0 547979916 476200960 99414 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116260 99414 603 41 0 116219 0
vsize: 465040
[startup+180.012 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 108165 0 0 0 17688 311 0 0 25 0 1 0 547979916 483147776 100955 4294967295 134512640 134672761 3221224544 3221222896 134604052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 117956 100955 603 41 0 117915 0
vsize: 471824
[startup+190.013 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 109633 0 0 0 18681 318 0 0 25 0 1 0 547979916 489136128 102423 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119418 102423 603 41 0 119377 0
vsize: 477672
[startup+200.012 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 110302 0 0 0 19676 323 0 0 25 0 1 0 547979916 491991040 103092 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120115 103092 603 41 0 120074 0
vsize: 480460
[startup+210.012 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 111481 0 0 0 20669 330 0 0 25 0 1 0 547979916 497229824 104271 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121394 104271 603 41 0 121353 0
vsize: 485576
[startup+220.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 113536 0 0 0 21658 340 0 0 25 0 1 0 547979916 505790464 106326 4294967295 134512640 134672761 3221224544 3221222960 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123484 106326 603 41 0 123443 0
vsize: 493936
[startup+230.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 115199 0 0 0 22650 348 0 0 25 0 1 0 547979916 513392640 107989 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125340 107989 603 41 0 125299 0
vsize: 501360
[startup+240.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 116576 0 0 0 23644 354 0 0 25 0 1 0 547979916 519122944 109366 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 126739 109366 603 41 0 126698 0
vsize: 506956
[startup+250.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 117879 0 0 0 24638 360 0 0 25 0 1 0 547979916 524419072 110669 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 128032 110669 603 41 0 127991 0
vsize: 512128
[startup+260.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 119032 0 0 0 25633 364 0 0 25 0 1 0 547979916 529174528 111822 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 129193 111822 603 41 0 129152 0
vsize: 516772
[startup+270.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 119949 0 0 0 26629 368 0 0 25 0 1 0 547979916 532959232 112739 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 130117 112739 603 41 0 130076 0
vsize: 520468
[startup+280.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 120829 0 0 0 27625 372 0 0 25 0 1 0 547979916 536743936 113619 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 131041 113619 603 41 0 131000 0
vsize: 524164
[startup+290.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 121813 0 0 0 28621 376 0 0 25 0 1 0 547979916 541396992 114603 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 132177 114603 603 41 0 132136 0
vsize: 528708
[startup+300.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 122742 0 0 0 29617 381 0 0 25 0 1 0 547979916 545669120 115532 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133220 115532 603 41 0 133179 0
vsize: 532880
[startup+310.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 123786 0 0 0 30613 385 0 0 25 0 1 0 547979916 551239680 116576 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134580 116576 603 41 0 134539 0
vsize: 538320
[startup+320.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 124634 0 0 0 31608 389 0 0 25 0 1 0 547979916 555495424 117424 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135619 117424 603 41 0 135578 0
vsize: 542476
[startup+330.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 125349 0 0 0 32605 392 0 0 25 0 1 0 547979916 558911488 118139 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 136453 118139 603 41 0 136412 0
vsize: 545812
[startup+340.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 125942 0 0 0 33602 395 0 0 25 0 1 0 547979916 561303552 118732 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 137037 118732 603 41 0 136996 0
vsize: 548148
[startup+350.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 126640 0 0 0 34600 398 0 0 25 0 1 0 547979916 564273152 119430 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 137762 119430 603 41 0 137721 0
vsize: 551048
[startup+360.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 127326 0 0 0 35597 400 0 0 25 0 1 0 547979916 567697408 120116 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 138598 120116 603 41 0 138557 0
vsize: 554392
[startup+370.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 128016 0 0 0 36594 403 0 0 25 0 1 0 547979916 570888192 120806 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 139377 120806 603 41 0 139336 0
vsize: 557508
[startup+380.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 128608 0 0 0 37592 406 0 0 25 0 1 0 547979916 573497344 121398 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 140014 121398 603 41 0 139973 0
vsize: 560056
[startup+390.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 129371 0 0 0 38590 408 0 0 25 0 1 0 547979916 577126400 122161 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 140900 122161 603 41 0 140859 0
vsize: 563600
[startup+400.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 130043 0 0 0 39587 411 0 0 25 0 1 0 547979916 580280320 122833 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 141670 122833 603 41 0 141629 0
vsize: 566680
[startup+410.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 130685 0 0 0 40584 414 0 0 25 0 1 0 547979916 583053312 123475 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 142347 123475 603 41 0 142306 0
vsize: 569388
[startup+420.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 131349 0 0 0 41580 418 0 0 25 0 1 0 547979916 585961472 124139 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 143057 124139 603 41 0 143016 0
vsize: 572228
[startup+430.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 132144 0 0 0 42577 421 0 0 25 0 1 0 547979916 589754368 124934 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 143983 124934 603 41 0 143942 0
vsize: 575932
[startup+440.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 132832 0 0 0 43574 424 0 0 25 0 1 0 547979916 592908288 125622 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 144753 125622 603 41 0 144712 0
vsize: 579012
[startup+450.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 133561 0 0 0 44571 427 0 0 25 0 1 0 547979916 596267008 126351 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 145573 126351 603 41 0 145532 0
vsize: 582292
[startup+460.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 134245 0 0 0 45569 429 0 0 25 0 1 0 547979916 599642112 127035 4294967295 134512640 134672761 3221224544 3221222720 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 146397 127035 603 41 0 146356 0
vsize: 585588
[startup+470.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 134844 0 0 0 46567 431 0 0 25 0 1 0 547979916 602075136 127634 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146991 127634 603 41 0 146950 0
vsize: 587964
[startup+480.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 135335 0 0 0 47563 435 0 0 25 0 1 0 547979916 604430336 128125 4294967295 134512640 134672761 3221224544 3221222752 1075730206 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 147566 128125 603 41 0 147525 0
vsize: 590264
[startup+490.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 135622 0 0 0 48558 439 0 0 25 0 1 0 547979916 605556736 128412 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 147841 128412 603 41 0 147800 0
vsize: 591364
[startup+500.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 135813 0 0 0 49554 443 0 0 25 0 1 0 547979916 606294016 128603 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 148021 128603 603 41 0 147980 0
vsize: 592084
[startup+510.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 136375 0 0 0 50552 445 0 0 25 0 1 0 547979916 608940032 129165 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 148667 129165 603 41 0 148626 0
vsize: 594668
[startup+520.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 136808 0 0 0 51547 449 0 0 25 0 1 0 547979916 610754560 129598 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 149110 129598 603 41 0 149069 0
vsize: 596440
[startup+530.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 137457 0 0 0 52544 452 0 0 25 0 1 0 547979916 614019072 130247 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 149907 130247 603 41 0 149866 0
vsize: 599628
[startup+540.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 137722 0 0 0 53541 455 0 0 25 0 1 0 547979916 614952960 130512 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 150135 130512 603 41 0 150094 0
vsize: 600540
[startup+550.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 137835 0 0 0 54538 458 0 0 25 0 1 0 547979916 614952960 130625 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 150135 130625 603 41 0 150094 0
vsize: 600540
[startup+560.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 138091 0 0 0 55537 459 0 0 25 0 1 0 547979916 615755776 130881 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 150331 130881 603 41 0 150290 0
vsize: 601324
[startup+570.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 138327 0 0 0 56535 462 0 0 25 0 1 0 547979916 616898560 131117 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 150610 131117 603 41 0 150569 0
vsize: 602440
[startup+580.018 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 138739 0 0 0 57532 464 0 0 25 0 1 0 547979916 619286528 131529 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 151193 131529 603 41 0 151152 0
vsize: 604772
[startup+590.03 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 138932 0 0 0 58531 466 0 0 25 0 1 0 547979916 619941888 131722 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 151353 131722 603 41 0 151312 0
vsize: 605412
[startup+600.03 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 139101 0 0 0 59530 468 0 0 25 0 1 0 547979916 620597248 131891 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 151513 131891 603 41 0 151472 0
vsize: 606052
[startup+610.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 139627 0 0 0 60527 471 0 0 25 0 1 0 547979916 623656960 132417 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 152260 132417 603 41 0 152219 0
vsize: 609040
[startup+620.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 140028 0 0 0 61525 472 0 0 25 0 1 0 547979916 626110464 132818 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 152859 132818 603 41 0 152818 0
vsize: 611436
[startup+630.031 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 140557 0 0 0 62523 474 0 0 25 0 1 0 547979916 629116928 133347 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 153593 133347 603 41 0 153552 0
vsize: 614372
[startup+640.031 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 140950 0 0 0 63521 476 0 0 25 0 1 0 547979916 631336960 133740 4294967295 134512640 134672761 3221224544 3221222992 134643977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 154135 133740 603 41 0 154094 0
vsize: 616540
[startup+650.031 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 141501 0 0 0 64520 478 0 0 25 0 1 0 547979916 634662912 134291 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 154947 134291 603 41 0 154906 0
vsize: 619788
[startup+660.032 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 141952 0 0 0 65518 480 0 0 25 0 1 0 547979916 636805120 134742 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 155470 134742 603 41 0 155429 0
vsize: 621880
[startup+670.031 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 142385 0 0 0 66516 481 0 0 25 0 1 0 547979916 638984192 135175 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 156002 135175 603 41 0 155961 0
vsize: 624008
[startup+680.032 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 142787 0 0 0 67515 483 0 0 25 0 1 0 547979916 640688128 135577 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 156418 135577 603 41 0 156377 0
vsize: 625672
[startup+690.033 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 143237 0 0 0 68514 485 0 0 25 0 1 0 547979916 643129344 136027 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 157014 136027 603 41 0 156973 0
vsize: 628056
[startup+700.034 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 143708 0 0 0 69511 487 0 0 25 0 1 0 547979916 645447680 136498 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 157580 136498 603 41 0 157539 0
vsize: 630320
[startup+710.034 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 144182 0 0 0 70510 489 0 0 25 0 1 0 547979916 647475200 136972 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 158075 136972 603 41 0 158034 0
vsize: 632300
[startup+720.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 144650 0 0 0 71508 491 0 0 25 0 1 0 547979916 649789440 137440 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 158640 137440 603 41 0 158599 0
vsize: 634560
[startup+730.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 145091 0 0 0 72506 493 0 0 25 0 1 0 547979916 652107776 137881 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 159206 137881 603 41 0 159165 0
vsize: 636824
[startup+740.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 145470 0 0 0 73505 495 0 0 25 0 1 0 547979916 653692928 138260 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 159593 138260 603 41 0 159552 0
vsize: 638372
[startup+750.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 145862 0 0 0 74503 497 0 0 25 0 1 0 547979916 654950400 138652 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 159900 138652 603 41 0 159859 0
vsize: 639600
[startup+760.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 146276 0 0 0 75501 498 0 0 25 0 1 0 547979916 656707584 139066 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 160329 139066 603 41 0 160288 0
vsize: 641316
[startup+770.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 146735 0 0 0 76499 500 0 0 25 0 1 0 547979916 658853888 139525 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 160853 139525 603 41 0 160812 0
vsize: 643412
[startup+780.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 147182 0 0 0 77497 503 0 0 25 0 1 0 547979916 660910080 139972 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 161355 139972 603 41 0 161314 0
vsize: 645420
[startup+790.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 147583 0 0 0 78494 505 0 0 25 0 1 0 547979916 662630400 140373 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 161775 140373 603 41 0 161734 0
vsize: 647100
[startup+800.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 148050 0 0 0 79493 507 0 0 25 0 1 0 547979916 664449024 140840 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 162219 140840 603 41 0 162178 0
vsize: 648876
[startup+810.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 148490 0 0 0 80491 509 0 0 25 0 1 0 547979916 666279936 141280 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 162666 141280 603 41 0 162625 0
vsize: 650664
[startup+820.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 148942 0 0 0 81490 511 0 0 25 0 1 0 547979916 668176384 141732 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 163129 141732 603 41 0 163088 0
vsize: 652516
[startup+830.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 149460 0 0 0 82487 512 0 0 25 0 1 0 547979916 670961664 142250 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 163809 142250 603 41 0 163768 0
vsize: 655236
[startup+840.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 149847 0 0 0 83485 514 0 0 25 0 1 0 547979916 672849920 142637 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 164270 142637 603 41 0 164229 0
vsize: 657080
[startup+850.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 150236 0 0 0 84483 516 0 0 25 0 1 0 547979916 674406400 143026 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 164650 143026 603 41 0 164609 0
vsize: 658600
[startup+860.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 150714 0 0 0 85481 518 0 0 25 0 1 0 547979916 676765696 143504 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 165226 143504 603 41 0 165185 0
vsize: 660904
[startup+870.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 151197 0 0 0 86479 520 0 0 25 0 1 0 547979916 679063552 143987 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 165787 143987 603 41 0 165746 0
vsize: 663148
[startup+880.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 151556 0 0 0 87477 522 0 0 25 0 1 0 547979916 680669184 144346 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 166179 144346 603 41 0 166138 0
vsize: 664716
[startup+890.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 151758 0 0 0 88474 524 0 0 25 0 1 0 547979916 681467904 144548 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 166374 144548 603 41 0 166333 0
vsize: 665496
[startup+900.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 152175 0 0 0 89472 527 0 0 25 0 1 0 547979916 683958272 144965 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166982 144965 603 41 0 166941 0
vsize: 667928
[startup+910.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 152601 0 0 0 90469 530 0 0 25 0 1 0 547979916 686346240 145391 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 167565 145391 603 41 0 167524 0
vsize: 670260
[startup+920.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 152813 0 0 0 91466 533 0 0 25 0 1 0 547979916 687394816 145603 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 167821 145603 603 41 0 167780 0
vsize: 671284
[startup+930.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 153198 0 0 0 92465 535 0 0 25 0 1 0 547979916 689651712 145988 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 168372 145988 603 41 0 168331 0
vsize: 673488
[startup+940.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 153329 0 0 0 93462 538 0 0 25 0 1 0 547979916 690110464 146119 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 168484 146119 603 41 0 168443 0
vsize: 673936
[startup+950.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 153978 0 0 0 94458 541 0 0 25 0 1 0 547979916 693563392 146768 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 169327 146768 603 41 0 169286 0
vsize: 677308
[startup+960.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 154656 0 0 0 95456 544 0 0 25 0 1 0 547979916 696774656 147446 4294967295 134512640 134672761 3221224544 3221222728 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170111 147449 603 41 0 170070 0
vsize: 680444
[startup+970.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 155290 0 0 0 96453 547 0 0 25 0 1 0 547979916 700702720 148080 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171070 148080 603 41 0 171029 0
vsize: 684280
[startup+980.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 155558 0 0 0 97451 549 0 0 25 0 1 0 547979916 701849600 148348 4294967295 134512640 134672761 3221224544 3221222992 134643524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171350 148348 603 41 0 171309 0
vsize: 685400
[startup+990.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 155847 0 0 0 98449 551 0 0 25 0 1 0 547979916 702992384 148637 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171629 148637 603 41 0 171588 0
vsize: 686516
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 156095 0 0 0 99447 553 0 0 25 0 1 0 547979916 703975424 148885 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171869 148885 603 41 0 171828 0
vsize: 687476
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 156463 0 0 0 100445 555 0 0 25 0 1 0 547979916 706101248 149253 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 172388 149253 603 41 0 172347 0
vsize: 689552
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 156841 0 0 0 101443 557 0 0 25 0 1 0 547979916 707727360 149631 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 172785 149631 603 41 0 172744 0
vsize: 691140
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 157426 0 0 0 102440 560 0 0 25 0 1 0 547979916 710692864 150216 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 173509 150216 603 41 0 173468 0
vsize: 694036
[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 158004 0 0 0 103437 563 0 0 25 0 1 0 547979916 713388032 150794 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 174167 150794 603 41 0 174126 0
vsize: 696668
[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 158590 0 0 0 104434 566 0 0 25 0 1 0 547979916 716042240 151380 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 174815 151380 603 41 0 174774 0
vsize: 699260
[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 159191 0 0 0 105431 569 0 0 25 0 1 0 547979916 718807040 151981 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 175490 151981 603 41 0 175449 0
vsize: 701960
[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 159679 0 0 0 106430 571 0 0 25 0 1 0 547979916 721006592 152469 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 176027 152469 603 41 0 175986 0
vsize: 704108
[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 160213 0 0 0 107427 574 0 0 25 0 1 0 547979916 723193856 153003 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 176561 153003 603 41 0 176520 0
vsize: 706244
[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 160817 0 0 0 108424 577 0 0 25 0 1 0 547979916 726020096 153607 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 177251 153607 603 41 0 177210 0
vsize: 709004
[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 161368 0 0 0 109420 581 0 0 25 0 1 0 547979916 728113152 154158 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 177762 154158 603 41 0 177721 0
vsize: 711048
[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 161800 0 0 0 110419 583 0 0 25 0 1 0 547979916 730103808 154590 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 178248 154590 603 41 0 178207 0
vsize: 712992
[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 162260 0 0 0 111416 586 0 0 25 0 1 0 547979916 732065792 155050 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 178727 155050 603 41 0 178686 0
vsize: 714908
[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 162681 0 0 0 112414 588 0 0 25 0 1 0 547979916 734097408 155471 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 179223 155471 603 41 0 179182 0
vsize: 716892
[startup+1140.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 163119 0 0 0 113413 589 0 0 25 0 1 0 547979916 736169984 155909 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 179729 155909 603 41 0 179688 0
vsize: 718916
[startup+1150.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 163554 0 0 0 114411 591 0 0 25 0 1 0 547979916 737873920 156344 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 180145 156344 603 41 0 180104 0
vsize: 720580
[startup+1160.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 164042 0 0 0 115410 593 0 0 25 0 1 0 547979916 740233216 156832 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 180721 156832 603 41 0 180680 0
vsize: 722884
[startup+1170.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 164667 0 0 0 116407 595 0 0 25 0 1 0 547979916 743653376 157457 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 181556 157457 603 41 0 181515 0
vsize: 726224
[startup+1180.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 165218 0 0 0 117405 598 0 0 25 0 1 0 547979916 746352640 158008 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 182215 158008 603 41 0 182174 0
vsize: 728860
[startup+1190.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 165750 0 0 0 118403 600 0 0 25 0 1 0 547979916 749031424 158540 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 182869 158540 603 41 0 182828 0
vsize: 731476
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 12144
Raw data (stat): 12144 (minisat+) R 12143 27565 27564 0 -1 0 166301 0 0 0 119401 602 0 0 25 0 1 0 547979916 752009216 159091 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 183596 159091 603 41 0 183555 0
vsize: 734384
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.47 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 12144
Raw data (stat): 12144 (minisat+) Z 12143 27565 27564 0 -1 12 166301 0 0 0 119401 643 0 0 25 0 1 0 547979916 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.47
CPU time (s): 1200.45
CPU user time (s): 1194.02
CPU system time (s): 6.43102
CPU usage (%): 99.9983
Max. virtual memory (Kb): 734384
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####