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 13862

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-20 22:05:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20254 boxname=wulflinc17 idbench=1558 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  e8862b41c9b4f49ec8d11d1df0495e74  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-sp97ic.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-sp97ic.opb /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-sp97ic.opb
IDLAUNCH: 20254
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        712304 kB
Buffers:         33220 kB
Cached:         256344 kB
SwapCached:         48 kB
Active:          76788 kB
Inactive:       215756 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        712052 kB
SwapTotal:     2097892 kB
SwapFree:      2097840 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           7032 kB
Slab:            24004 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 22:25:56 (client local time) WITH STATUS 0 IN 1200.35 SECONDS
stats: 20254 7 1200.35 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1033 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .sssss.sssssssssssssssss..s.sss.s.sssss.ss.sssssssssssssssssssssssssssssss..ss.ss.sssssssss.s.ssss...sssss.s...s.ss.s.s.s.s....ss.ssss.s.ss..sssssssssssssssss...s..ssssss
c ---[1158]---> BDD-cost:   39
c ---[1157]---> BDD-cost:   39
c ---[1156]---> BDD-cost:   39
c ---[1155]---> BDD-cost:   39
c ---[1154]---> BDD-cost:   39
c ---[1153]---> BDD-cost:   47
c ---[1152]---> BDD-cost:   47
c ---[1151]---> BDD-cost:   47
c ---[1150]---> BDD-cost:   47
c ---[1149]---> BDD-cost:   35
c ---[1147]---> BDD-cost:    7
c ---[1146]---> BDD-cost:   23
c ---[1145]---> BDD-cost:   23
c ---[1144]---> BDD-cost:   13
c ---[1143]---> BDD-cost:   25
c ---[1142]---> BDD-cost:   19
c ---[1141]---> BDD-cost:   23
c ---[1140]---> BDD-cost:   23
c ---[1139]---> BDD-cost:   23
c ---[1138]---> BDD-cost:   23
c ---[1136]---> BDD-cost:   23
c ---[1135]---> BDD-cost:   23
c ---[1134]---> BDD-cost:   25
c ---[1133]---> BDD-cost:   25
c ---[1132]---> BDD-cost:    5
c ---[1131]---> BDD-cost:   25
c ---[1130]---> BDD-cost:   19
c ---[1129]---> BDD-cost:   19
c ---[1128]---> BDD-cost:   19
c ---[1127]---> BDD-cost:   25
c ---[1125]---> BDD-cost:   19
c ---[1124]---> BDD-cost:   25
c ---[1123]---> BDD-cost:   19
c ---[1117]---> Adder-cost: 23092   maxlim: 39   bits: 7/6
c ---[1114]---> Adder-cost: 13882   maxlim: 29   bits: 6/5
c ---[1098]---> BDD-cost:  161
c ---[1093]---> BDD-cost: 2360
c ---[1082]---> BDD-cost: 1572
c ---[1071]---> BDD-cost:  200
c ---[1067]---> BDD-cost:  189
c ---[1060]---> BDD-cost:  294
c ---[1051]---> BDD-cost: 4351
c ---[1050]---> Adder-cost: 838   maxlim: 12   bits: 5/4
c ---[1033]---> BDD-cost:  212
c ---[1011]---> BDD-cost:   25
c ---[1010]---> BDD-cost:    7
c ---[1009]---> BDD-cost:    3
c ---[1008]---> BDD-cost:   13
c ---[1007]---> BDD-cost:    3
c ---[1006]---> BDD-cost:   25
c ---[1005]---> BDD-cost:   19
c ---[1004]---> BDD-cost:10182
c ---[1003]---> BDD-cost:   25
c ---[1002]---> BDD-cost:   23
c ---[1001]---> BDD-cost:   19
c ---[ 999]---> BDD-cost:   19
c ---[ 998]---> BDD-cost:   19
c ---[ 997]---> BDD-cost:    9
c ---[ 996]---> BDD-cost:   47
c ---[ 995]---> BDD-cost:    3
c ---[ 994]---> BDD-cost:   25
c ---[ 992]---> BDD-cost:   47
c ---[ 991]---> BDD-cost:   47
c ---[ 990]---> BDD-cost:   47
c ---[ 989]---> BDD-cost:   47
c ---[ 988]---> BDD-cost:    9
c ---[ 987]---> BDD-cost:   13
c ---[ 985]---> BDD-cost:   25
c ---[ 984]---> BDD-cost:   19
c ---[ 983]---> BDD-cost:   19
c ---[ 981]---> BDD-cost:   19
c ---[ 980]---> BDD-cost:   47
c ---[ 978]---> BDD-cost:   25
c ---[ 977]---> BDD-cost:   19
c ---[ 976]---> BDD-cost:   19
c ---[ 975]---> BDD-cost:    9
c ---[ 974]---> BDD-cost:   19
c ---[ 973]---> BDD-cost:   19
c ---[ 972]---> BDD-cost:   19
c ---[ 970]---> BDD-cost:   47
c ---[ 969]---> BDD-cost:   19
c ---[ 968]---> BDD-cost:   47
c ---[ 967]---> BDD-cost:   47
c ---[ 966]---> BDD-cost:   47
c ---[ 965]---> BDD-cost:   35
c ---[ 964]---> BDD-cost:   19
c ---[ 963]---> BDD-cost:   19
c ---[ 962]---> BDD-cost:   25
c ---[ 961]---> BDD-cost:   19
c ---[ 960]---> BDD-cost:    0
c ---[ 959]---> BDD-cost:   19
c ---[ 958]---> BDD-cost:   19
c ---[ 957]---> BDD-cost:   19
c ---[ 956]---> BDD-cost:   19
c ---[ 955]---> BDD-cost:   19
c ---[ 953]---> BDD-cost:   11
c ---[ 952]---> BDD-cost:    9
c ---[ 951]---> BDD-cost:   11
c ---[ 950]---> BDD-cost:    3
c ---[ 949]---> BDD-cost: 5686
c ---[ 948]---> BDD-cost:    5
c ---[ 947]---> BDD-cost:   11
c ---[ 946]---> BDD-cost:   25
c ---[ 945]---> BDD-cost:   47
c ---[ 944]---> BDD-cost:   47
c ---[ 943]---> BDD-cost:   47
c ---[ 942]---> BDD-cost:   11
c ---[ 941]---> BDD-cost:   25
c ---[ 940]---> BDD-cost:   25
c ---[ 939]---> BDD-cost:   25
c ---[ 938]---> BDD-cost: 7868
c ---[ 937]---> BDD-cost:   11
c ---[ 936]---> BDD-cost:   11
c ---[ 935]---> BDD-cost:   47
c ---[ 934]---> BDD-cost:    5
c ---[ 933]---> BDD-cost:   11
c ---[ 932]---> BDD-cost:   47
c ---[ 931]---> BDD-cost:   47
c ---[ 930]---> BDD-cost:   47
c ---[ 929]---> BDD-cost:   47
c ---[ 928]---> BDD-cost:   11
c ---[ 926]---> BDD-cost:   11
c ---[ 925]---> BDD-cost:   25
c ---[ 924]---> BDD-cost:    5
c ---[ 923]---> BDD-cost:   11
c ---[ 922]---> BDD-cost:   25
c ---[ 921]---> BDD-cost:   25
c ---[ 920]---> BDD-cost:   25
c ---[ 919]---> BDD-cost:    0
c ---[ 918]---> BDD-cost:    5
c ---[ 917]---> BDD-cost:   11
c ---[ 915]---> BDD-cost:   25
c ---[ 914]---> BDD-cost:   25
c ---[ 913]---> BDD-cost:   25
c ---[ 912]---> BDD-cost:   25
c ---[ 911]---> BDD-cost:   11
c ---[ 910]---> BDD-cost:   11
c ---[ 909]---> BDD-cost:   25
c ---[ 908]---> BDD-cost:   25
c ---[ 907]---> BDD-cost:   47
c ---[ 906]---> BDD-cost:   25
c ---[ 905]---> BDD-cost: 3423
c ---[ 903]---> BDD-cost:   47
c ---[ 902]---> BDD-cost:   25
c ---[ 901]---> BDD-cost:   47
c ---[ 900]---> BDD-cost:    7
c ---[ 899]---> BDD-cost:   25
c ---[ 898]---> BDD-cost:   25
c ---[ 897]---> BDD-cost:   25
c ---[ 896]---> BDD-cost:   25
c ---[ 895]---> BDD-cost:   25
c ---[ 894]---> BDD-cost:   25
c ---[ 892]---> BDD-cost:   25
c ---[ 891]---> BDD-cost:   25
c ---[ 890]---> BDD-cost:    5
c ---[ 889]---> BDD-cost:   25
c ---[ 888]---> BDD-cost:   11
c ---[ 887]---> BDD-cost:   47
c ---[ 886]---> BDD-cost:   47
c ---[ 885]---> BDD-cost:   19
c ---[ 884]---> BDD-cost:   25
c ---[ 883]---> BDD-cost:    9
c ---[ 882]---> BDD-cost: 6499
c ---[ 881]---> BDD-cost:   47
c ---[ 880]---> BDD-cost:   47
c ---[ 879]---> BDD-cost:   25
c ---[ 878]---> BDD-cost:   19
c ---[ 877]---> BDD-cost:   25
c ---[ 876]---> BDD-cost:   19
c ---[ 875]---> BDD-cost:   25
c ---[ 874]---> BDD-cost:    7
c ---[ 873]---> BDD-cost:   19
c ---[ 872]---> BDD-cost:   25
c ---[ 870]---> BDD-cost:   19
c ---[ 869]---> BDD-cost:   19
c ---[ 868]---> BDD-cost:   47
c ---[ 867]---> BDD-cost:   47
c ---[ 866]---> BDD-cost:   47
c ---[ 865]---> BDD-cost:   25
c ---[ 864]---> BDD-cost:   25
c ---[ 863]---> BDD-cost:   19
c ---[ 862]---> BDD-cost:   25
c ---[ 861]---> BDD-cost:    7
c ---[ 859]---> BDD-cost:   11
c ---[ 858]---> BDD-cost:   47
c ---[ 857]---> BDD-cost:   47
c ---[ 856]---> BDD-cost:   25
c ---[ 855]---> BDD-cost:   19
c ---[ 854]---> BDD-cost:    9
c ---[ 853]---> BDD-cost:    5
c ---[ 852]---> BDD-cost:   11
c ---[ 851]---> BDD-cost:   47
c ---[ 850]---> BDD-cost:   47
c ---[ 849]---> BDD-cost: 3650
c ---[ 848]---> BDD-cost:    9
c ---[ 847]---> BDD-cost:   25
c ---[ 846]---> BDD-cost:   25
c ---[ 845]---> BDD-cost:   19
c ---[ 844]---> BDD-cost:   25
c ---[ 843]---> BDD-cost:   19
c ---[ 842]---> BDD-cost:    3
c ---[ 841]---> BDD-cost:   11
c ---[ 840]---> BDD-cost:   25
c ---[ 839]---> BDD-cost:   19
c ---[ 838]---> BDD-cost: 6888
c ---[ 837]---> BDD-cost:   19
c ---[ 836]---> BDD-cost:   47
c ---[ 835]---> BDD-cost:   25
c ---[ 834]---> BDD-cost:   47
c ---[ 833]---> BDD-cost:   47
c ---[ 832]---> BDD-cost:   25
c ---[ 831]---> BDD-cost:   25
c ---[ 830]---> BDD-cost:   19
c ---[ 829]---> BDD-cost:    3
c ---[ 828]---> BDD-cost:    5
c ---[ 827]---> Adder-cost: 7844   maxlim: 5   bits: 4/3
c ---[ 826]---> BDD-cost:   43
c ---[ 825]---> BDD-cost:   35
c ---[ 824]---> BDD-cost:   43
c ---[ 823]---> BDD-cost:   43
c ---[ 822]---> BDD-cost:   11
c ---[ 821]---> BDD-cost:   35
c ---[ 820]---> BDD-cost:   35
c ---[ 819]---> BDD-cost:   11
c ---[ 818]---> BDD-cost:   47
c ---[ 817]---> BDD-cost:   23
c ---[ 816]---> Adder-cost: 16310   maxlim: 39   bits: 7/6
c ---[ 815]---> BDD-cost:    5
c ---[ 814]---> BDD-cost:   19
c ---[ 813]---> BDD-cost:   25
c ---[ 812]---> BDD-cost:   23
c ---[ 811]---> BDD-cost:   25
c ---[ 810]---> BDD-cost:   11
c ---[ 809]---> BDD-cost:    5
c ---[ 808]---> BDD-cost:   35
c ---[ 807]---> BDD-cost:   35
c ---[ 806]---> BDD-cost:   13
c ---[ 805]---> BDD-cost: 3504
c ---[ 804]---> BDD-cost:   25
c ---[ 803]---> BDD-cost:    5
c ---[ 802]---> BDD-cost:   35
c ---[ 801]---> BDD-cost:   35
c ---[ 800]---> BDD-cost:   35
c ---[ 799]---> BDD-cost:   11
c ---[ 798]---> BDD-cost:   35
c ---[ 797]---> BDD-cost:   43
c ---[ 796]---> BDD-cost:   43
c ---[ 795]---> BDD-cost:   43
c ---[ 794]---> BDD-cost: 4241
c ---[ 793]---> BDD-cost: 1556
c ---[ 792]---> BDD-cost:   43
c ---[ 791]---> BDD-cost:   43
c ---[ 790]---> BDD-cost:   43
c ---[ 789]---> BDD-cost:   35
c ---[ 788]---> BDD-cost:   35
c ---[ 787]---> BDD-cost:   35
c ---[ 786]---> BDD-cost:   35
c ---[ 785]---> BDD-cost:   35
c ---[ 784]---> BDD-cost:    5
c ---[ 783]---> BDD-cost:   35
c ---[ 782]---> BDD-cost: 6026
c ---[ 781]---> BDD-cost:   47
c ---[ 780]---> BDD-cost:   47
c ---[ 779]---> BDD-cost:   25
c ---[ 778]---> BDD-cost:   19
c ---[ 777]---> BDD-cost:   11
c ---[ 776]---> BDD-cost:   47
c ---[ 775]---> BDD-cost:   47
c ---[ 774]---> BDD-cost:   11
c ---[ 773]---> BDD-cost:   25
c ---[ 772]---> BDD-cost:   25
c ---[ 771]---> Adder-cost: 6634   maxlim: 29   bits: 6/5
c ---[ 770]---> BDD-cost:   19
c ---[ 769]---> BDD-cost:    3
c ---[ 768]---> BDD-cost:   25
c ---[ 767]---> BDD-cost:   19
c ---[ 766]---> BDD-cost:   25
c ---[ 765]---> BDD-cost:   47
c ---[ 764]---> BDD-cost:   25
c ---[ 763]---> BDD-cost:   47
c ---[ 762]---> BDD-cost:   47
c ---[ 761]---> BDD-cost:   25
c ---[ 760]---> BDD-cost: 1112
c ---[ 759]---> BDD-cost:   25
c ---[ 758]---> BDD-cost:   25
c ---[ 757]---> BDD-cost:   19
c ---[ 756]---> BDD-cost:    3
c ---[ 755]---> BDD-cost:    5
c ---[ 754]---> BDD-cost:   19
c ---[ 753]---> BDD-cost:   25
c ---[ 752]---> BDD-cost:   25
c ---[ 751]---> BDD-cost:   47
c ---[ 750]---> BDD-cost:   43
c ---[ 749]---> BDD-cost: 1117
c ---[ 748]---> BDD-cost:   39
c ---[ 747]---> BDD-cost:   19
c ---[ 746]---> BDD-cost:   25
c ---[ 745]---> BDD-cost:   43
c ---[ 744]---> BDD-cost:   43
c ---[ 743]---> BDD-cost:   13
c ---[ 742]---> BDD-cost:   13
c ---[ 741]---> BDD-cost:    5
c ---[ 740]---> BDD-cost:   25
c ---[ 739]---> BDD-cost:   47
c ---[ 737]---> BDD-cost:   13
c ---[ 736]---> BDD-cost:   13
c ---[ 735]---> BDD-cost:    5
c ---[ 734]---> BDD-cost:   39
c ---[ 733]---> BDD-cost:   23
c ---[ 732]---> BDD-cost:   47
c ---[ 731]---> BDD-cost:    5
c ---[ 730]---> BDD-cost:   13
c ---[ 729]---> BDD-cost:   25
c ---[ 728]---> BDD-cost:   47
c ---[ 726]---> BDD-cost:   47
c ---[ 725]---> BDD-cost:   47
c ---[ 724]---> BDD-cost:   47
c ---[ 723]---> BDD-cost:   47
c ---[ 722]---> BDD-cost:    7
c ---[ 721]---> BDD-cost:   13
c ---[ 720]---> BDD-cost:   47
c ---[ 719]---> BDD-cost:   47
c ---[ 718]---> BDD-cost:   39
c ---[ 717]---> BDD-cost:   47
c ---[ 715]---> BDD-cost:   47
c ---[ 714]---> BDD-cost:   43
c ---[ 713]---> BDD-cost:   43
c ---[ 712]---> BDD-cost:   47
c ---[ 711]---> BDD-cost:   47
c ---[ 710]---> BDD-cost:   43
c ---[ 709]---> BDD-cost:   43
c ---[ 708]---> BDD-cost:   47
c ---[ 707]---> BDD-cost:   47
c ---[ 706]---> BDD-cost:   13
c ---[ 704]---> BDD-cost:   13
c ---[ 703]---> BDD-cost:    7
c ---[ 702]---> BDD-cost:   43
c ---[ 701]---> BDD-cost:   43
c ---[ 700]---> BDD-cost:   47
c ---[ 699]---> BDD-cost:   47
c ---[ 698]---> BDD-cost:   13
c ---[ 697]---> BDD-cost:   13
c ---[ 696]---> BDD-cost:    7
c ---[ 695]---> BDD-cost:   47
c ---[ 693]---> BDD-cost:   47
c ---[ 692]---> BDD-cost:   47
c ---[ 691]---> BDD-cost:   13
c ---[ 690]---> BDD-cost:   13
c ---[ 687]---> BDD-cost:   43
c ---[ 686]---> BDD-cost:   43
c ---[ 685]---> BDD-cost:   13
c ---[ 684]---> BDD-cost:   13
c ---[ 683]---> BDD-cost: 5449
c ---[ 681]---> BDD-cost:   47
c ---[ 680]---> BDD-cost:    7
c ---[ 679]---> BDD-cost:   13
c ---[ 678]---> BDD-cost:    7
c ---[ 677]---> BDD-cost:   13
c ---[ 676]---> BDD-cost:    7
c ---[ 675]---> BDD-cost:   13
c ---[ 674]---> BDD-cost:   47
c ---[ 673]---> BDD-cost:   47
c ---[ 672]---> BDD-cost:   47
c ---[ 670]---> BDD-cost:   19
c ---[ 669]---> BDD-cost:   19
c ---[ 668]---> BDD-cost:   25
c ---[ 667]---> BDD-cost:    9
c ---[ 666]---> BDD-cost:    3
c ---[ 665]---> BDD-cost:   47
c ---[ 664]---> BDD-cost:   47
c ---[ 663]---> BDD-cost:    9
c ---[ 662]---> BDD-cost:   25
c ---[ 661]---> BDD-cost:   19
c ---[ 659]---> BDD-cost:   25
c ---[ 658]---> BDD-cost:   19
c ---[ 657]---> BDD-cost:   25
c ---[ 655]---> BDD-cost:   19
c ---[ 654]---> BDD-cost:   25
c ---[ 653]---> BDD-cost:   19
c ---[ 652]---> BDD-cost:   19
c ---[ 651]---> BDD-cost:   47
c ---[ 650]---> BDD-cost:   47
c ---[ 648]---> BDD-cost:   47
c ---[ 647]---> BDD-cost:   25
c ---[ 646]---> BDD-cost:   25
c ---[ 645]---> BDD-cost:   19
c ---[ 644]---> BDD-cost:   25
c ---[ 643]---> BDD-cost:   23
c ---[ 642]---> BDD-cost:   25
c ---[ 641]---> BDD-cost:   25
c ---[ 640]---> BDD-cost:   25
c ---[ 639]---> BDD-cost:   25
c ---[ 637]---> BDD-cost:   25
c ---[ 636]---> BDD-cost:   47
c ---[ 635]---> BDD-cost:   47
c ---[ 634]---> BDD-cost:   25
c ---[ 633]---> BDD-cost:   25
c ---[ 632]---> BDD-cost:   35
c ---[ 631]---> BDD-cost:   23
c ---[ 630]---> BDD-cost:   25
c ---[ 629]---> BDD-cost:   23
c ---[ 628]---> BDD-cost:   25
c ---[ 627]---> BDD-cost: 7382
c ---[ 626]---> BDD-cost:   25
c ---[ 625]---> BDD-cost:   25
c ---[ 624]---> BDD-cost:   23
c ---[ 623]---> BDD-cost:   25
c ---[ 622]---> BDD-cost:   23
c ---[ 621]---> BDD-cost:   47
c ---[ 620]---> BDD-cost:   23
c ---[ 619]---> BDD-cost:   47
c ---[ 618]---> BDD-cost:   23
c ---[ 617]---> BDD-cost:   23
c ---[ 616]---> BDD-cost:  960
c ---[ 615]---> BDD-cost:   25
c ---[ 614]---> BDD-cost:   25
c ---[ 613]---> BDD-cost:   25
c ---[ 612]---> BDD-cost:   19
c ---[ 611]---> BDD-cost:   25
c ---[ 610]---> BDD-cost:   47
c ---[ 609]---> BDD-cost:   39
c ---[ 608]---> BDD-cost:   25
c ---[ 607]---> BDD-cost:   19
c ---[ 606]---> BDD-cost:   43
c ---[ 604]---> BDD-cost:   47
c ---[ 603]---> BDD-cost:   43
c ---[ 602]---> BDD-cost:   47
c ---[ 601]---> BDD-cost:   19
c ---[ 600]---> BDD-cost:   25
c ---[ 599]---> BDD-cost:   35
c ---[ 598]---> BDD-cost:   25
c ---[ 597]---> BDD-cost:   19
c ---[ 596]---> BDD-cost:   13
c ---[ 595]---> BDD-cost:   13
c ---[ 593]---> BDD-cost:   43
c ---[ 592]---> BDD-cost:   25
c ---[ 591]---> BDD-cost:   19
c ---[ 590]---> BDD-cost:   13
c ---[ 589]---> BDD-cost:   13
c ---[ 587]---> BDD-cost:   19
c ---[ 586]---> BDD-cost:   25
c ---[ 585]---> BDD-cost:   13
c ---[ 584]---> BDD-cost:    5
c ---[ 582]---> BDD-cost:   13
c ---[ 581]---> BDD-cost:    5
c ---[ 580]---> BDD-cost:   13
c ---[ 579]---> BDD-cost:   39
c ---[ 578]---> BDD-cost:   39
c ---[ 577]---> BDD-cost:   35
c ---[ 576]---> BDD-cost:   13
c ---[ 575]---> BDD-cost:   23
c ---[ 574]---> BDD-cost:   23
c ---[ 569]---> BDD-cost:   25
c ---[ 568]---> BDD-cost:   19
c ---[ 567]---> BDD-cost:   19
c ---[ 566]---> BDD-cost:   19
c ---[ 565]---> BDD-cost:   47
c ---[ 564]---> BDD-cost:   47
c ---[ 563]---> BDD-cost:   11
c ---[ 562]---> BDD-cost:   47
c ---[ 561]---> BDD-cost:   47
c ---[ 560]---> BDD-cost: 9003
c ---[ 559]---> BDD-cost:   47
c ---[ 558]---> BDD-cost:   47
c ---[ 557]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:    9
c ---[ 555]---> BDD-cost:   19
c ---[ 554]---> BDD-cost:   19
c ---[ 553]---> BDD-cost:   25
c ---[ 552]---> BDD-cost:   13
c ---[ 551]---> BDD-cost:    9
c ---[ 550]---> BDD-cost:   19
c ---[ 549]---> BDD-cost: 8735
c ---[ 548]---> BDD-cost:   19
c ---[ 546]---> BDD-cost:   19
c ---[ 545]---> BDD-cost:   25
c ---[ 544]---> BDD-cost:   19
c ---[ 543]---> BDD-cost:   47
c ---[ 542]---> BDD-cost:   19
c ---[ 541]---> BDD-cost:   47
c ---[ 540]---> BDD-cost:   47
c ---[ 539]---> BDD-cost:   47
c ---[ 538]---> BDD-cost: 7408
c ---[ 537]---> BDD-cost:   11
c ---[ 536]---> BDD-cost:   19
c ---[ 535]---> BDD-cost:   25
c ---[ 534]---> BDD-cost:   25
c ---[ 533]---> BDD-cost:   25
c ---[ 532]---> BDD-cost:   19
c ---[ 531]---> BDD-cost:   25
c ---[ 530]---> BDD-cost:   19
c ---[ 529]---> BDD-cost:   25
c ---[ 528]---> BDD-cost:   19
c ---[ 526]---> BDD-cost:   25
c ---[ 525]---> BDD-cost:    9
c ---[ 524]---> BDD-cost:    9
c ---[ 523]---> BDD-cost:   47
c ---[ 522]---> BDD-cost:   47
c ---[ 521]---> BDD-cost:   47
c ---[ 520]---> BDD-cost:   47
c ---[ 519]---> BDD-cost:   23
c ---[ 518]---> BDD-cost:   19
c ---[ 517]---> BDD-cost:   47
c ---[ 515]---> BDD-cost:   39
c ---[ 514]---> BDD-cost:   47
c ---[ 513]---> BDD-cost:   47
c ---[ 512]---> BDD-cost:   47
c ---[ 511]---> BDD-cost:   47
c ---[ 510]---> BDD-cost:   39
c ---[ 509]---> BDD-cost:   47
c ---[ 508]---> BDD-cost:   47
c ---[ 507]---> BDD-cost:   39
c ---[ 506]---> BDD-cost:   39
c ---[ 505]---> BDD-cost:25076
c ---[ 504]---> BDD-cost:   47
c ---[ 503]---> BDD-cost:   39
c ---[ 502]---> BDD-cost:   47
c ---[ 501]---> BDD-cost:   47
c ---[ 500]---> BDD-cost:   47
c ---[ 499]---> BDD-cost:   47
c ---[ 498]---> BDD-cost:   47
c ---[ 497]---> BDD-cost:   47
c ---[ 496]---> BDD-cost:   11
c ---[ 495]---> BDD-cost:   25
c ---[ 493]---> BDD-cost:    3
c ---[ 492]---> BDD-cost:   25
c ---[ 491]---> BDD-cost:   19
c ---[ 490]---> BDD-cost:   13
c ---[ 489]---> BDD-cost:    3
c ---[ 488]---> BDD-cost:   19
c ---[ 487]---> BDD-cost:   25
c ---[ 486]---> BDD-cost:   11
c ---[ 485]---> BDD-cost:   25
c ---[ 484]---> BDD-cost:   47
c ---[ 482]---> BDD-cost:   25
c ---[ 481]---> BDD-cost:   47
c ---[ 480]---> BDD-cost:   25
c ---[ 479]---> BDD-cost:   47
c ---[ 478]---> BDD-cost:   47
c ---[ 477]---> BDD-cost:    7
c ---[ 476]---> BDD-cost:   25
c ---[ 475]---> BDD-cost:   25
c ---[ 474]---> BDD-cost:   25
c ---[ 473]---> BDD-cost:   25
c ---[ 471]---> BDD-cost:   25
c ---[ 470]---> BDD-cost:   19
c ---[ 469]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:    3
c ---[ 467]---> BDD-cost:   25
c ---[ 466]---> BDD-cost:   47
c ---[ 465]---> BDD-cost:   47
c ---[ 464]---> BDD-cost:   19
c ---[ 463]---> BDD-cost:   23
c ---[ 462]---> BDD-cost:   43
c ---[ 459]---> BDD-cost:   47
c ---[ 458]---> BDD-cost:   47
c ---[ 457]---> BDD-cost:   43
c ---[ 456]---> BDD-cost:   47
c ---[ 455]---> BDD-cost:   47
c ---[ 454]---> BDD-cost:   43
c ---[ 453]---> BDD-cost:   47
c ---[ 452]---> BDD-cost:   47
c ---[ 451]---> BDD-cost:   47
c ---[ 450]---> BDD-cost:   43
c ---[ 449]---> Adder-cost: 2679   maxlim: 22   bits: 6/5
c ---[ 448]---> BDD-cost:   43
c ---[ 447]---> BDD-cost:   47
c ---[ 446]---> BDD-cost:   47
c ---[ 445]---> BDD-cost:   43
c ---[ 444]---> BDD-cost:   47
c ---[ 443]---> BDD-cost:   47
c ---[ 442]---> BDD-cost:   47
c ---[ 441]---> BDD-cost:   47
c ---[ 440]---> BDD-cost:   47
c ---[ 439]---> BDD-cost:   23
c ---[ 438]---> BDD-cost: 3640
c ---[ 437]---> BDD-cost:   19
c ---[ 436]---> BDD-cost:   47
c ---[ 435]---> BDD-cost:   47
c ---[ 434]---> BDD-cost:   43
c ---[ 433]---> BDD-cost:   47
c ---[ 432]---> BDD-cost:   47
c ---[ 431]---> BDD-cost:   43
c ---[ 430]---> BDD-cost:   47
c ---[ 429]---> BDD-cost:   47
c ---[ 428]---> BDD-cost:   43
c ---[ 426]---> BDD-cost:   47
c ---[ 425]---> BDD-cost:   47
c ---[ 424]---> BDD-cost:   47
c ---[ 423]---> BDD-cost:   47
c ---[ 422]---> BDD-cost:   47
c ---[ 421]---> BDD-cost:   43
c ---[ 420]---> BDD-cost:   47
c ---[ 419]---> BDD-cost:   43
c ---[ 418]---> BDD-cost:   43
c ---[ 417]---> BDD-cost:   43
c ---[ 415]---> BDD-cost:   43
c ---[ 414]---> BDD-cost:   23
c ---[ 413]---> BDD-cost:   19
c ---[ 412]---> BDD-cost:   43
c ---[ 411]---> BDD-cost:   47
c ---[ 410]---> BDD-cost:   47
c ---[ 409]---> BDD-cost:   43
c ---[ 408]---> BDD-cost:   47
c ---[ 407]---> BDD-cost:   43
c ---[ 406]---> BDD-cost:   47
c ---[ 404]---> BDD-cost:   43
c ---[ 403]---> BDD-cost:   47
c ---[ 402]---> BDD-cost:   47
c ---[ 401]---> BDD-cost:   47
c ---[ 400]---> BDD-cost:   47
c ---[ 399]---> BDD-cost:   47
c ---[ 398]---> BDD-cost:   25
c ---[ 397]---> BDD-cost:    9
c ---[ 396]---> BDD-cost:   19
c ---[ 395]---> BDD-cost:   25
c ---[ 393]---> BDD-cost:   19
c ---[ 392]---> BDD-cost:   25
c ---[ 391]---> BDD-cost:   13
c ---[ 390]---> BDD-cost:    9
c ---[ 389]---> BDD-cost:   19
c ---[ 388]---> BDD-cost:   25
c ---[ 387]---> BDD-cost:   19
c ---[ 386]---> BDD-cost:   19
c ---[ 385]---> BDD-cost:   25
c ---[ 384]---> BDD-cost:   19
c ---[ 382]---> BDD-cost:   47
c ---[ 381]---> BDD-cost:   19
c ---[ 380]---> BDD-cost:   47
c ---[ 379]---> BDD-cost:   47
c ---[ 378]---> BDD-cost:   47
c ---[ 377]---> BDD-cost:   11
c ---[ 376]---> BDD-cost:   19
c ---[ 375]---> BDD-cost:   25
c ---[ 374]---> BDD-cost:   25
c ---[ 373]---> BDD-cost:   25
c ---[ 371]---> BDD-cost:   19
c ---[ 370]---> BDD-cost:   25
c ---[ 369]---> BDD-cost:   19
c ---[ 368]---> BDD-cost:   25
c ---[ 367]---> BDD-cost:   19
c ---[ 366]---> BDD-cost:   25
c ---[ 365]---> BDD-cost:    9
c ---[ 364]---> BDD-cost:    9
c ---[ 363]---> BDD-cost:   25
c ---[ 362]---> BDD-cost:   35
c ---[ 360]---> BDD-cost:   35
c ---[ 359]---> BDD-cost:   25
c ---[ 358]---> BDD-cost:   35
c ---[ 357]---> BDD-cost:   35
c ---[ 356]---> BDD-cost:   35
c ---[ 355]---> BDD-cost:   25
c ---[ 354]---> BDD-cost:   35
c ---[ 353]---> BDD-cost:   43
c ---[ 352]---> BDD-cost:   43
c ---[ 351]---> BDD-cost:   43
c ---[ 350]---> BDD-cost:11166
c ---[ 348]---> BDD-cost:   43
c ---[ 347]---> BDD-cost:   43
c ---[ 346]---> BDD-cost:   43
c ---[ 345]---> BDD-cost:   25
c ---[ 344]---> BDD-cost:   13
c ---[ 343]---> BDD-cost:   35
c ---[ 342]---> BDD-cost:   35
c ---[ 341]---> BDD-cost:   35
c ---[ 340]---> BDD-cost:   35
c ---[ 339]---> BDD-cost:   35
c ---[ 337]---> BDD-cost:   25
c ---[ 336]---> BDD-cost:   35
c ---[ 335]---> BDD-cost:   25
c ---[ 334]---> BDD-cost:   25
c ---[ 333]---> BDD-cost:   19
c ---[ 332]---> BDD-cost:   25
c ---[ 331]---> BDD-cost:   19
c ---[ 330]---> BDD-cost:   25
c ---[ 329]---> BDD-cost:   47
c ---[ 328]---> BDD-cost:   25
c ---[ 326]---> BDD-cost:   47
c ---[ 325]---> BDD-cost:   47
c ---[ 324]---> BDD-cost:   25
c ---[ 323]---> BDD-cost:   25
c ---[ 322]---> BDD-cost:   25
c ---[ 321]---> BDD-cost:   19
c ---[ 319]---> BDD-cost:   13
c ---[ 318]---> BDD-cost:   13
c ---[ 317]---> BDD-cost:   43
c ---[ 316]---> BDD-cost: 4990
c ---[ 314]---> BDD-cost:   13
c ---[ 313]---> BDD-cost:   13
c ---[ 312]---> BDD-cost:    7
c ---[ 311]---> BDD-cost:   13
c ---[ 310]---> BDD-cost:   13
c ---[ 309]---> BDD-cost:   13
c ---[ 308]---> BDD-cost:   13
c ---[ 307]---> BDD-cost:   39
c ---[ 306]---> BDD-cost:   39
c ---[ 305]---> BDD-cost:10657
c ---[ 304]---> BDD-cost:   35
c ---[ 303]---> BDD-cost:   23
c ---[ 302]---> BDD-cost:   23
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 299]---> BDD-cost:    9
c ---[ 298]---> BDD-cost:   25
c ---[ 297]---> BDD-cost:   19
c ---[ 296]---> BDD-cost:   19
c ---[ 295]---> BDD-cost:   19
c ---[ 294]---> BDD-cost:12172
c ---[ 293]---> BDD-cost:   47
c ---[ 292]---> BDD-cost:   25
c ---[ 291]---> BDD-cost:   19
c ---[ 290]---> BDD-cost:   13
c ---[ 289]---> BDD-cost:   13
c ---[ 287]---> BDD-cost:   19
c ---[ 286]---> BDD-cost:   25
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost: 8229
c ---[ 282]---> BDD-cost:    5
c ---[ 281]---> BDD-cost:    5
c ---[ 280]---> BDD-cost:   39
c ---[ 279]---> BDD-cost:   47
c ---[ 278]---> BDD-cost:   35
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 275]---> BDD-cost:   23
c ---[ 274]---> BDD-cost:   13
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost: 4792
c ---[ 271]---> BDD-cost:   13
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:   13
c ---[ 268]---> BDD-cost:   25
c ---[ 267]---> BDD-cost:   19
c ---[ 266]---> BDD-cost:   19
c ---[ 265]---> BDD-cost:   13
c ---[ 264]---> BDD-cost:   43
c ---[ 263]---> BDD-cost:   47
c ---[ 262]---> BDD-cost:   43
c ---[ 261]---> BDD-cost: 8472
c ---[ 260]---> BDD-cost:   43
c ---[ 259]---> BDD-cost:   35
c ---[ 258]---> BDD-cost:   43
c ---[ 257]---> BDD-cost:   47
c ---[ 256]---> BDD-cost:   43
c ---[ 255]---> BDD-cost:   13
c ---[ 254]---> BDD-cost:   19
c ---[ 253]---> BDD-cost:   25
c ---[ 252]---> BDD-cost:    9
c ---[ 251]---> BDD-cost:   25
c ---[ 250]---> BDD-cost: 2697
c ---[ 249]---> BDD-cost:   19
c ---[ 248]---> BDD-cost:   47
c ---[ 247]---> BDD-cost:   25
c ---[ 246]---> BDD-cost:   47
c ---[ 245]---> BDD-cost:   25
c ---[ 244]---> BDD-cost:   47
c ---[ 243]---> BDD-cost:   47
c ---[ 242]---> BDD-cost:    7
c ---[ 241]---> BDD-cost:   25
c ---[ 240]---> BDD-cost:   25
c ---[ 238]---> BDD-cost: 2179
c ---[ 237]---> BDD-cost:   25
c ---[ 236]---> BDD-cost:   25
c ---[ 235]---> BDD-cost:   19
c ---[ 234]---> BDD-cost:   25
c ---[ 233]---> BDD-cost:   25
c ---[ 232]---> BDD-cost:   19
c ---[ 229]---> BDD-cost:   25
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost: 1419
c ---[ 226]---> BDD-cost:   13
c ---[ 225]---> BDD-cost:   19
c ---[ 224]---> BDD-cost:    9
c ---[ 223]---> BDD-cost:   13
c ---[ 222]---> BDD-cost:   13
c ---[ 221]---> BDD-cost:   13
c ---[ 220]---> BDD-cost:   13
c ---[ 219]---> BDD-cost:   39
c ---[ 218]---> BDD-cost:   39
c ---[ 217]---> BDD-cost:   35
c ---[ 216]---> BDD-cost:15660
c ---[ 215]---> BDD-cost:   23
c ---[ 214]---> BDD-cost:   23
c ---[ 213]---> BDD-cost:   13
c ---[ 212]---> BDD-cost:   13
c ---[ 211]---> BDD-cost:   13
c ---[ 210]---> BDD-cost:   25
c ---[ 209]---> BDD-cost:   19
c ---[ 208]---> BDD-cost:   19
c ---[ 207]---> BDD-cost:   19
c ---[ 206]---> BDD-cost:   19
c ---[ 205]---> BDD-cost: 1442
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   13
c ---[ 202]---> BDD-cost:    5
c ---[ 201]---> BDD-cost:    7
c ---[ 200]---> BDD-cost:    5
c ---[ 199]---> BDD-cost:    7
c ---[ 198]---> BDD-cost:   47
c ---[ 197]---> BDD-cost:   39
c ---[ 196]---> BDD-cost:   13
c ---[ 195]---> BDD-cost:   13
c ---[ 193]---> BDD-cost:   25
c ---[ 192]---> BDD-cost:   23
c ---[ 191]---> BDD-cost:   13
c ---[ 190]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:   13
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:   13
c ---[ 186]---> BDD-cost:    5
c ---[ 185]---> BDD-cost:   19
c ---[ 184]---> BDD-cost:   19
c ---[ 182]---> BDD-cost:   19
c ---[ 181]---> BDD-cost:   47
c ---[ 180]---> BDD-cost:   47
c ---[ 179]---> BDD-cost:   47
c ---[ 178]---> BDD-cost:   25
c ---[ 177]---> BDD-cost:   25
c ---[ 176]---> BDD-cost:   19
c ---[ 175]---> BDD-cost:   25
c ---[ 174]---> BDD-cost:    9
c ---[ 173]---> BDD-cost:   13
c ---[ 171]---> BDD-cost:   13
c ---[ 170]---> BDD-cost:   39
c ---[ 169]---> BDD-cost:   39
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   23
c ---[ 166]---> BDD-cost:   13
c ---[ 165]---> BDD-cost:   25
c ---[ 164]---> BDD-cost:   19
c ---[ 163]---> BDD-cost:   39
c ---[ 162]---> BDD-cost:   39
c ---[ 160]---> BDD-cost:   43
c ---[ 159]---> BDD-cost:   43
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   13
c ---[ 156]---> BDD-cost:   47
c ---[ 155]---> BDD-cost:   23
c ---[ 154]---> BDD-cost:    5
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:    5
c ---[ 151]---> BDD-cost:   13
c ---[ 149]---> BDD-cost:    5
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   47
c ---[ 146]---> BDD-cost:   25
c ---[ 145]---> BDD-cost:   19
c ---[ 144]---> BDD-cost:   47
c ---[ 143]---> BDD-cost:   39
c ---[ 142]---> BDD-cost:   39
c ---[ 141]---> BDD-cost:   47
c ---[ 140]---> BDD-cost:   23
c ---[ 138]---> BDD-cost:    5
c ---[ 137]---> BDD-cost:   13
c ---[ 136]---> BDD-cost:   47
c ---[ 135]---> BDD-cost:   25
c ---[ 134]---> BDD-cost:   43
c ---[ 133]---> BDD-cost:   43
c ---[ 132]---> BDD-cost:   39
c ---[ 131]---> BDD-cost:   39
c ---[ 130]---> BDD-cost:   47
c ---[ 129]---> BDD-cost:   39
c ---[ 128]---> BDD-cost:  526
c ---[ 127]---> BDD-cost: 6314
c ---[ 126]---> Adder-cost: 1713   maxlim: 4   bits: 4/3
c ---[ 125]---> BDD-cost: 5010
c ---[ 124]---> BDD-cost: 5984
c ---[ 123]---> BDD-cost: 6429
c ---[ 122]---> Adder-cost: 3066   maxlim: 6   bits: 4/3
c ---[ 121]---> Adder-cost: 8437   maxlim: 19   bits: 6/5
c ---[ 120]---> Adder-cost: 5125   maxlim: 18   bits: 6/5
c ---[ 119]---> Adder-cost: 1599   maxlim: 14   bits: 5/4
c ---[ 118]---> BDD-cost: 2172
c ---[ 117]---> BDD-cost:24906
c ---[ 116]---> Adder-cost: 885   maxlim: 12   bits: 5/4
c ---[ 115]---> BDD-cost: 2276
c ---[ 114]---> Adder-cost: 4102   maxlim: 9   bits: 5/4
c ---[ 113]---> BDD-cost: 2122
c ---[ 112]---> BDD-cost: 1446
c ---[ 111]---> BDD-cost:   44
c ---[ 110]---> BDD-cost: 6226
c ---[ 109]---> BDD-cost:  502
c ---[ 108]---> BDD-cost:  698
c ---[ 107]---> BDD-cost:  636
c ---[ 106]---> BDD-cost:  610
c ---[ 105]---> BDD-cost:   98
c ---[ 104]---> BDD-cost:  156
c ---[ 103]---> BDD-cost:  906
c ---[ 102]---> BDD-cost: 1270
c ---[ 101]---> BDD-cost: 1320
c ---[ 100]---> BDD-cost: 1876
c ---[  99]---> BDD-cost: 1098
c ---[  98]---> BDD-cost:  282
c ---[  97]---> BDD-cost:  230
c ---[  96]---> BDD-cost: 2814
c ---[  95]---> BDD-cost:  536
c ---[  94]---> BDD-cost: 2014
c ---[  93]---> BDD-cost: 1536
c ---[  92]---> BDD-cost: 4626
c ---[  91]---> BDD-cost: 3914
c ---[  90]---> BDD-cost: 3507
c ---[  89]---> BDD-cost:  217
c ---[  88]---> BDD-cost:12956
c ---[  87]---> BDD-cost: 1560
c ---[  86]---> BDD-cost: 2409
c ---[  85]---> BDD-cost: 2574
c ---[  84]---> BDD-cost: 1288
c ---[  83]---> BDD-cost:  279
c ---[  82]---> BDD-cost:  492
c ---[  81]---> BDD-cost:  775
c ---[  80]---> BDD-cost:  990
c ---[  79]---> BDD-cost: 1408
c ---[  78]---> BDD-cost:10070
c ---[  77]---> BDD-cost:  168
c ---[  76]---> BDD-cost: 4857
c ---[  75]---> BDD-cost: 3908
c ---[  74]---> BDD-cost: 3531
c ---[  73]---> BDD-cost: 1209
c ---[  72]---> BDD-cost:  468
c ---[  71]---> BDD-cost: 4718
c ---[  70]---> BDD-cost:  770
c ---[  69]---> BDD-cost: 3641
c ---[  68]---> BDD-cost:  748
c ---[  67]---> BDD-cost: 2696
c ---[  66]---> BDD-cost: 1134
c ---[  65]---> BDD-cost:  540
c ---[  64]---> BDD-cost:  100
c ---[  63]---> BDD-cost:  628
c ---[  62]---> BDD-cost:  494
c ---[  61]---> BDD-cost:  270
c ---[  60]---> BDD-cost:  326
c ---[  59]---> BDD-cost:  606
c ---[  58]---> BDD-cost:10995
c ---[  57]---> BDD-cost: 1283
c ---[  56]---> BDD-cost: 6499
c ---[  55]---> BDD-cost:  569
c ---[  54]---> BDD-cost:  657
c ---[  53]---> BDD-cost:  958
c ---[  52]---> BDD-cost:   88
c ---[  51]---> BDD-cost: 1082
c ---[  50]---> BDD-cost:  462
c ---[  49]---> BDD-cost: 1905
c ---[  48]---> BDD-cost:  297
c ---[  47]---> BDD-cost: 1018
c ---[  46]---> BDD-cost: 7706
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:  266
c ---[  43]---> BDD-cost:  148
c ---[  42]---> BDD-cost:  104
c ---[  41]---> BDD-cost: 1267
c ---[  40]---> Adder-cost: 7122   maxlim: 24   bits: 6/5
c ---[  39]---> BDD-cost:    1
c ---[  38]---> BDD-cost: 1432
c ---[  37]---> BDD-cost:  532
c ---[  36]---> BDD-cost:  182
c ---[  35]---> BDD-cost:    1
c ---[  34]---> BDD-cost:  106
c ---[  33]---> BDD-cost:  166
c ---[  32]---> BDD-cost: 1536
c ---[  31]---> BDD-cost:  498
c ---[  30]---> BDD-cost: 1740
c ---[  29]---> BDD-cost:  492
c ---[  28]---> BDD-cost:  844
c ---[  27]---> BDD-cost:  212
c ---[  26]---> BDD-cost: 2544
c ---[  25]---> BDD-cost:    2
c ---[  24]---> BDD-cost: 2508
c ---[  23]---> BDD-cost:  330
c ---[  22]---> BDD-cost:  278
c ---[  21]---> BDD-cost: 2578
c ---[  20]---> BDD-cost: 2470
c ---[  19]---> BDD-cost: 3216
c ---[  18]---> BDD-cost:   51
c ---[  17]---> BDD-cost: 3862
c ---[  16]---> BDD-cost:  384
c ---[  15]---> BDD-cost:  423
c ---[  14]---> BDD-cost:  884
c ---[  13]---> BDD-cost:  778
c ---[  12]---> BDD-cost: 1398
c ---[  11]---> BDD-cost: 1234
c ---[  10]---> BDD-cost: 1820
c ---[   9]---> BDD-cost: 1756
c ---[   8]---> BDD-cost: 2370
c ---[   7]---> BDD-cost: 2110
c ---[   6]---> BDD-cost: 2142
c ---[   5]---> BDD-cost: 2646
c ---[   4]---> BDD-cost: 3906
c ---[   3]---> BDD-cost: 5663
c ---[   2]---> Adder-cost: 3775   maxlim: 7   bits: 4/3
c ---[   1]---> Adder-cost: 2539   maxlim: 7   bits: 4/3
c ---[   0]---> BDD-cost: 3822
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2847944  8701829 |  949314       0        0     nan |  0.000 % |
c |       100 | 2847939  8701814 | 1044245      99      319     3.2 |  0.187 % |
c |       250 | 2847877  8701628 | 1148669     228      714     3.1 |  0.189 % |
c |       475 | 2847736  8701205 | 1263536     409     1653     4.0 |  0.194 % |
c |       817 | 2847185  8699552 | 1389890     561     2249     4.0 |  0.212 % |
c |      1323 | 2846435  8697318 | 1528879     813     3318     4.1 |  0.238 % |
c |      2082 | 2845873  8695626 | 1681767    1370     5774     4.2 |  0.258 % |
c |      3222 | 2844973  8692886 | 1849944    2189     9735     4.4 |  0.288 % |
c |      4932 | 2843916  8689681 | 2034938    3491    16658     4.8 |  0.325 % |
c |      7494 | 2842312  8684747 | 2238432    5485    27996     5.1 |  0.378 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.97 0.91 2/55 17061
Raw data (stat): 17061 (runsolver) R 17060 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539913182 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.94 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 16540 0 0 0 960 38 0 0 25 0 1 0 539913182 62656512 13300 4294967295 134512640 134672761 3221224544 3221222112 134523714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15297 13300 603 41 0 15256 0
vsize: 61188
[startup+19.9998 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 57751 0 0 0 1861 137 0 0 25 0 1 0 539913182 234221568 53106 4294967295 134512640 134672761 3221224544 3221221672 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57183 53106 603 41 0 57142 0
vsize: 228732
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63530 0 0 0 2846 153 0 0 25 0 1 0 539913182 285380608 58885 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69673 58885 603 41 0 69632 0
vsize: 278692
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63581 0 0 0 3845 153 0 0 25 0 1 0 539913182 285380608 58936 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69673 58936 603 41 0 69632 0
vsize: 278692
[startup+50.0016 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63606 0 0 0 4845 153 0 0 25 0 1 0 539913182 285515776 58961 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69706 58961 603 41 0 69665 0
vsize: 278824
[startup+60.0012 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63607 0 0 0 5845 154 0 0 25 0 1 0 539913182 285515776 58962 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69706 58962 603 41 0 69665 0
vsize: 278824
[startup+70.0008 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63648 0 0 0 6834 155 0 0 25 0 1 0 539913182 285515776 59003 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69706 59003 603 41 0 69665 0
vsize: 278824
[startup+80.0078 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63682 0 0 0 7835 155 0 0 25 0 1 0 539913182 285515776 59037 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69706 59037 603 41 0 69665 0
vsize: 278824
[startup+90.0074 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63699 0 0 0 8834 156 0 0 25 0 1 0 539913182 285650944 59054 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69739 59054 603 41 0 69698 0
vsize: 278956
[startup+100.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63733 0 0 0 9834 156 0 0 25 0 1 0 539913182 285650944 59088 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69739 59088 603 41 0 69698 0
vsize: 278956
[startup+110.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63738 0 0 0 10835 156 0 0 25 0 1 0 539913182 285650944 59093 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69739 59093 603 41 0 69698 0
vsize: 278956
[startup+120.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63739 0 0 0 11835 156 0 0 25 0 1 0 539913182 285650944 59094 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69739 59094 603 41 0 69698 0
vsize: 278956
[startup+130.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63740 0 0 0 12835 157 0 0 25 0 1 0 539913182 285650944 59095 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69739 59095 603 41 0 69698 0
vsize: 278956
[startup+140.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63741 0 0 0 13835 157 0 0 25 0 1 0 539913182 285650944 59096 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69739 59096 603 41 0 69698 0
vsize: 278956
[startup+150.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63769 0 0 0 14835 157 0 0 25 0 1 0 539913182 285650944 59124 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69739 59124 603 41 0 69698 0
vsize: 278956
[startup+160.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63777 0 0 0 15835 158 0 0 25 0 1 0 539913182 285650944 59132 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69739 59132 603 41 0 69698 0
vsize: 278956
[startup+170.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63777 0 0 0 16835 158 0 0 25 0 1 0 539913182 285650944 59132 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69739 59132 603 41 0 69698 0
vsize: 278956
[startup+180.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63795 0 0 0 17835 158 0 0 25 0 1 0 539913182 285786112 59150 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69772 59150 603 41 0 69731 0
vsize: 279088
[startup+190.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63824 0 0 0 18834 158 0 0 25 0 1 0 539913182 285786112 59179 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69772 59179 603 41 0 69731 0
vsize: 279088
[startup+200.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17061
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63830 0 0 0 19834 158 0 0 25 0 1 0 539913182 285786112 59185 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69772 59185 603 41 0 69731 0
vsize: 279088
[startup+210.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63840 0 0 0 20837 159 0 0 25 0 1 0 539913182 285921280 59195 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69805 59195 603 41 0 69764 0
vsize: 279220
[startup+220.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63846 0 0 0 21838 159 0 0 25 0 1 0 539913182 285921280 59201 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69805 59201 603 41 0 69764 0
vsize: 279220
[startup+230.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63849 0 0 0 22839 159 0 0 25 0 1 0 539913182 285921280 59204 4294967295 134512640 134672761 3221224544 3221223744 134557806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69805 59204 603 41 0 69764 0
vsize: 279220
[startup+240.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63858 0 0 0 23839 159 0 0 25 0 1 0 539913182 285921280 59213 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69805 59213 603 41 0 69764 0
vsize: 279220
[startup+250.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63861 0 0 0 24839 159 0 0 25 0 1 0 539913182 285921280 59216 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69805 59216 603 41 0 69764 0
vsize: 279220
[startup+260.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63866 0 0 0 25839 159 0 0 25 0 1 0 539913182 285921280 59221 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69805 59221 603 41 0 69764 0
vsize: 279220
[startup+270.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63869 0 0 0 26839 159 0 0 25 0 1 0 539913182 285921280 59224 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69805 59224 603 41 0 69764 0
vsize: 279220
[startup+280.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63876 0 0 0 27839 159 0 0 25 0 1 0 539913182 285921280 59231 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69805 59231 603 41 0 69764 0
vsize: 279220
[startup+290.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63878 0 0 0 28839 160 0 0 25 0 1 0 539913182 286056448 59233 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69838 59233 603 41 0 69797 0
vsize: 279352
[startup+300.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63888 0 0 0 29839 160 0 0 25 0 1 0 539913182 286056448 59243 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69838 59243 603 41 0 69797 0
vsize: 279352
[startup+310.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63892 0 0 0 30839 160 0 0 25 0 1 0 539913182 286056448 59247 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69838 59247 603 41 0 69797 0
vsize: 279352
[startup+320.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63897 0 0 0 31839 160 0 0 25 0 1 0 539913182 286056448 59252 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69838 59252 603 41 0 69797 0
vsize: 279352
[startup+330.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63906 0 0 0 32839 160 0 0 25 0 1 0 539913182 286056448 59261 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69838 59261 603 41 0 69797 0
vsize: 279352
[startup+340.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63910 0 0 0 33839 160 0 0 25 0 1 0 539913182 286056448 59265 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69838 59265 603 41 0 69797 0
vsize: 279352
[startup+350.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63911 0 0 0 34839 160 0 0 25 0 1 0 539913182 286056448 59266 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69838 59266 603 41 0 69797 0
vsize: 279352
[startup+360.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63911 0 0 0 35839 160 0 0 25 0 1 0 539913182 286056448 59266 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69838 59266 603 41 0 69797 0
vsize: 279352
[startup+370.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63914 0 0 0 36839 160 0 0 25 0 1 0 539913182 286056448 59269 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69838 59269 603 41 0 69797 0
vsize: 279352
[startup+380.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63927 0 0 0 37840 160 0 0 25 0 1 0 539913182 286191616 59282 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59282 603 41 0 69830 0
vsize: 279484
[startup+390.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63930 0 0 0 38839 160 0 0 25 0 1 0 539913182 286191616 59285 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59285 603 41 0 69830 0
vsize: 279484
[startup+400.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63933 0 0 0 39840 160 0 0 25 0 1 0 539913182 286191616 59288 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59288 603 41 0 69830 0
vsize: 279484
[startup+410.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63935 0 0 0 40840 161 0 0 25 0 1 0 539913182 286191616 59290 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59290 603 41 0 69830 0
vsize: 279484
[startup+420.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63936 0 0 0 41840 161 0 0 25 0 1 0 539913182 286191616 59291 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59291 603 41 0 69830 0
vsize: 279484
[startup+430.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63938 0 0 0 42840 161 0 0 25 0 1 0 539913182 286191616 59293 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59293 603 41 0 69830 0
vsize: 279484
[startup+440.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63938 0 0 0 43840 161 0 0 25 0 1 0 539913182 286191616 59293 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59293 603 41 0 69830 0
vsize: 279484
[startup+450.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63939 0 0 0 44840 161 0 0 25 0 1 0 539913182 286191616 59294 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59294 603 41 0 69830 0
vsize: 279484
[startup+460.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63939 0 0 0 45840 161 0 0 25 0 1 0 539913182 286191616 59294 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59294 603 41 0 69830 0
vsize: 279484
[startup+470.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63943 0 0 0 46840 161 0 0 25 0 1 0 539913182 286191616 59298 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59298 603 41 0 69830 0
vsize: 279484
[startup+480.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63944 0 0 0 47841 161 0 0 25 0 1 0 539913182 286191616 59299 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59299 603 41 0 69830 0
vsize: 279484
[startup+490.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63945 0 0 0 48841 161 0 0 25 0 1 0 539913182 286191616 59300 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59300 603 41 0 69830 0
vsize: 279484
[startup+500.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17063
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63947 0 0 0 49841 161 0 0 25 0 1 0 539913182 286191616 59302 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59302 603 41 0 69830 0
vsize: 279484
[startup+510.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63947 0 0 0 50841 161 0 0 25 0 1 0 539913182 286191616 59302 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59302 603 41 0 69830 0
vsize: 279484
[startup+520.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63948 0 0 0 51841 161 0 0 25 0 1 0 539913182 286191616 59303 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59303 603 41 0 69830 0
vsize: 279484
[startup+530.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63952 0 0 0 52841 161 0 0 25 0 1 0 539913182 286191616 59307 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69871 59307 603 41 0 69830 0
vsize: 279484
[startup+540.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63963 0 0 0 53841 161 0 0 25 0 1 0 539913182 286326784 59318 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59318 603 41 0 69863 0
vsize: 279616
[startup+550.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63967 0 0 0 54841 161 0 0 25 0 1 0 539913182 286326784 59322 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59322 603 41 0 69863 0
vsize: 279616
[startup+560.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63973 0 0 0 55852 161 0 0 25 0 1 0 539913182 286326784 59328 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59328 603 41 0 69863 0
vsize: 279616
[startup+570.273 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63975 0 0 0 56862 161 0 0 25 0 1 0 539913182 286326784 59330 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59330 603 41 0 69863 0
vsize: 279616
[startup+580.274 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63975 0 0 0 57862 161 0 0 25 0 1 0 539913182 286326784 59330 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59330 603 41 0 69863 0
vsize: 279616
[startup+590.273 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63975 0 0 0 58862 161 0 0 25 0 1 0 539913182 286326784 59330 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59330 603 41 0 69863 0
vsize: 279616
[startup+600.273 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63975 0 0 0 59862 161 0 0 25 0 1 0 539913182 286326784 59330 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59330 603 41 0 69863 0
vsize: 279616
[startup+610.272 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63979 0 0 0 60863 162 0 0 25 0 1 0 539913182 286326784 59334 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59334 603 41 0 69863 0
vsize: 279616
[startup+620.272 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63981 0 0 0 61863 162 0 0 25 0 1 0 539913182 286326784 59336 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59336 603 41 0 69863 0
vsize: 279616
[startup+630.272 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63986 0 0 0 62863 162 0 0 25 0 1 0 539913182 286326784 59341 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59341 603 41 0 69863 0
vsize: 279616
[startup+640.272 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 63994 0 0 0 63863 162 0 0 25 0 1 0 539913182 286326784 59349 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69904 59349 603 41 0 69863 0
vsize: 279616
[startup+650.272 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64000 0 0 0 64863 162 0 0 25 0 1 0 539913182 286461952 59355 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59355 603 41 0 69896 0
vsize: 279748
[startup+660.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64003 0 0 0 65863 162 0 0 25 0 1 0 539913182 286461952 59358 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59358 603 41 0 69896 0
vsize: 279748
[startup+670.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64003 0 0 0 66863 162 0 0 25 0 1 0 539913182 286461952 59358 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59358 603 41 0 69896 0
vsize: 279748
[startup+680.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64003 0 0 0 67863 162 0 0 25 0 1 0 539913182 286461952 59358 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59358 603 41 0 69896 0
vsize: 279748
[startup+690.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64008 0 0 0 68863 162 0 0 25 0 1 0 539913182 286461952 59363 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59363 603 41 0 69896 0
vsize: 279748
[startup+700.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64017 0 0 0 69863 162 0 0 25 0 1 0 539913182 286461952 59372 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59372 603 41 0 69896 0
vsize: 279748
[startup+710.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64019 0 0 0 70863 162 0 0 25 0 1 0 539913182 286461952 59374 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59374 603 41 0 69896 0
vsize: 279748
[startup+720.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64019 0 0 0 71863 162 0 0 25 0 1 0 539913182 286461952 59374 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69937 59374 603 41 0 69896 0
vsize: 279748
[startup+730.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64020 0 0 0 72863 162 0 0 25 0 1 0 539913182 286461952 59375 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59375 603 41 0 69896 0
vsize: 279748
[startup+740.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64022 0 0 0 73864 162 0 0 25 0 1 0 539913182 286461952 59377 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59377 603 41 0 69896 0
vsize: 279748
[startup+750.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64023 0 0 0 74864 163 0 0 25 0 1 0 539913182 286461952 59378 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59378 603 41 0 69896 0
vsize: 279748
[startup+760.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64025 0 0 0 75864 163 0 0 25 0 1 0 539913182 286461952 59380 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59380 603 41 0 69896 0
vsize: 279748
[startup+770.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64025 0 0 0 76864 163 0 0 25 0 1 0 539913182 286461952 59380 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59380 603 41 0 69896 0
vsize: 279748
[startup+780.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64026 0 0 0 77864 163 0 0 25 0 1 0 539913182 286461952 59381 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59381 603 41 0 69896 0
vsize: 279748
[startup+790.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17065
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64026 0 0 0 78864 163 0 0 25 0 1 0 539913182 286461952 59381 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59381 603 41 0 69896 0
vsize: 279748
[startup+800.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64027 0 0 0 79864 163 0 0 25 0 1 0 539913182 286461952 59382 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59382 603 41 0 69896 0
vsize: 279748
[startup+810.272 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64033 0 0 0 80865 163 0 0 25 0 1 0 539913182 286461952 59388 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59388 603 41 0 69896 0
vsize: 279748
[startup+820.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64033 0 0 0 81865 163 0 0 25 0 1 0 539913182 286461952 59388 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59388 603 41 0 69896 0
vsize: 279748
[startup+830.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64034 0 0 0 82865 163 0 0 25 0 1 0 539913182 286461952 59389 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59389 603 41 0 69896 0
vsize: 279748
[startup+840.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64034 0 0 0 83865 163 0 0 25 0 1 0 539913182 286461952 59389 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59389 603 41 0 69896 0
vsize: 279748
[startup+850.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64035 0 0 0 84865 163 0 0 25 0 1 0 539913182 286461952 59390 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69937 59390 603 41 0 69896 0
vsize: 279748
[startup+860.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64039 0 0 0 85865 163 0 0 25 0 1 0 539913182 286597120 59394 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69970 59394 603 41 0 69929 0
vsize: 279880
[startup+870.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64048 0 0 0 86865 163 0 0 25 0 1 0 539913182 286597120 59403 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69970 59403 603 41 0 69929 0
vsize: 279880
[startup+880.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64049 0 0 0 87865 163 0 0 25 0 1 0 539913182 286597120 59404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69970 59404 603 41 0 69929 0
vsize: 279880
[startup+890.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64052 0 0 0 88865 163 0 0 25 0 1 0 539913182 286597120 59407 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69970 59407 603 41 0 69929 0
vsize: 279880
[startup+900.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64053 0 0 0 89865 163 0 0 25 0 1 0 539913182 286597120 59408 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69970 59408 603 41 0 69929 0
vsize: 279880
[startup+910.269 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64054 0 0 0 90865 164 0 0 25 0 1 0 539913182 286597120 59409 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69970 59409 603 41 0 69929 0
vsize: 279880
[startup+920.269 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64055 0 0 0 91866 164 0 0 25 0 1 0 539913182 286597120 59410 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69970 59410 603 41 0 69929 0
vsize: 279880
[startup+930.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64056 0 0 0 92866 164 0 0 25 0 1 0 539913182 286597120 59411 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69970 59411 603 41 0 69929 0
vsize: 279880
[startup+940.269 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64060 0 0 0 93866 164 0 0 25 0 1 0 539913182 286597120 59415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69970 59415 603 41 0 69929 0
vsize: 279880
[startup+950.269 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64061 0 0 0 94866 164 0 0 25 0 1 0 539913182 286597120 59416 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69970 59416 603 41 0 69929 0
vsize: 279880
[startup+960.269 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64063 0 0 0 95866 164 0 0 25 0 1 0 539913182 286597120 59418 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69970 59418 603 41 0 69929 0
vsize: 279880
[startup+970.269 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64065 0 0 0 96866 164 0 0 25 0 1 0 539913182 286597120 59420 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69970 59420 603 41 0 69929 0
vsize: 279880
[startup+980.269 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64066 0 0 0 97856 164 0 0 25 0 1 0 539913182 286597120 59421 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59421 603 41 0 69929 0
vsize: 279880
[startup+990.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64071 0 0 0 98855 164 0 0 25 0 1 0 539913182 286597120 59426 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69970 59426 603 41 0 69929 0
vsize: 279880
[startup+1000.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64079 0 0 0 99855 164 0 0 25 0 1 0 539913182 286732288 59434 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70003 59434 603 41 0 69962 0
vsize: 280012
[startup+1010.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64082 0 0 0 100855 165 0 0 25 0 1 0 539913182 286732288 59437 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70003 59437 603 41 0 69962 0
vsize: 280012
[startup+1020.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64094 0 0 0 101855 165 0 0 25 0 1 0 539913182 286732288 59449 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70003 59449 603 41 0 69962 0
vsize: 280012
[startup+1030.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64103 0 0 0 102855 165 0 0 25 0 1 0 539913182 286732288 59458 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70003 59458 603 41 0 69962 0
vsize: 280012
[startup+1040.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64106 0 0 0 103855 165 0 0 25 0 1 0 539913182 286732288 59461 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70003 59461 603 41 0 69962 0
vsize: 280012
[startup+1050.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64106 0 0 0 104855 165 0 0 25 0 1 0 539913182 286732288 59461 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70003 59461 603 41 0 69962 0
vsize: 280012
[startup+1060.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64107 0 0 0 105855 165 0 0 25 0 1 0 539913182 286732288 59462 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70003 59462 603 41 0 69962 0
vsize: 280012
[startup+1070.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64113 0 0 0 106855 165 0 0 25 0 1 0 539913182 286732288 59468 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70003 59468 603 41 0 69962 0
vsize: 280012
[startup+1080.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64125 0 0 0 107855 165 0 0 25 0 1 0 539913182 286732288 59480 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70003 59480 603 41 0 69962 0
vsize: 280012
[startup+1090.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17067
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64125 0 0 0 108855 165 0 0 25 0 1 0 539913182 286732288 59480 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70003 59480 603 41 0 69962 0
vsize: 280012
[startup+1100.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17069
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64125 0 0 0 109855 165 0 0 25 0 1 0 539913182 286732288 59480 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70003 59480 603 41 0 69962 0
vsize: 280012
[startup+1110.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17069
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64127 0 0 0 110855 166 0 0 25 0 1 0 539913182 286867456 59482 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70036 59482 603 41 0 69995 0
vsize: 280144
[startup+1120.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17069
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64127 0 0 0 111855 166 0 0 25 0 1 0 539913182 286867456 59482 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70036 59482 603 41 0 69995 0
vsize: 280144
[startup+1130.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17069
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64129 0 0 0 112855 166 0 0 25 0 1 0 539913182 286867456 59484 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70036 59484 603 41 0 69995 0
vsize: 280144
[startup+1140.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17069
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64130 0 0 0 113856 166 0 0 25 0 1 0 539913182 286867456 59485 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70036 59485 603 41 0 69995 0
vsize: 280144
[startup+1150.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17069
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64130 0 0 0 114856 166 0 0 25 0 1 0 539913182 286867456 59485 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70036 59485 603 41 0 69995 0
vsize: 280144
[startup+1160.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17069
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64131 0 0 0 115856 166 0 0 25 0 1 0 539913182 286867456 59486 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70036 59486 603 41 0 69995 0
vsize: 280144
[startup+1170.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17069
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64131 0 0 0 116856 166 0 0 25 0 1 0 539913182 286867456 59486 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70036 59486 603 41 0 69995 0
vsize: 280144
[startup+1180.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17069
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64131 0 0 0 117856 166 0 0 25 0 1 0 539913182 286867456 59486 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70036 59486 603 41 0 69995 0
vsize: 280144
[startup+1190.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17069
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64132 0 0 0 118856 166 0 0 25 0 1 0 539913182 286867456 59487 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70036 59487 603 41 0 69995 0
vsize: 280144
[startup+1200.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 17069
Raw data (stat): 17061 (minisat+) R 17060 20838 20837 0 -1 0 64132 0 0 0 119856 166 0 0 25 0 1 0 539913182 286867456 59487 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70036 59487 603 41 0 69995 0
vsize: 280144
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.39 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 17069
Raw data (stat): 17061 (minisat+) Z 17060 20838 20837 0 -1 12 64134 0 0 0 119856 178 0 0 25 0 1 0 539913182 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.39
CPU time (s): 1200.35
CPU user time (s): 1198.57
CPU system time (s): 1.78273
CPU usage (%): 99.9971
Max. virtual memory (Kb): 280144
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####