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/milp/normalized-mps-v2-20-10-neos16.opb
MD5SUM	44281820d2b00a47b643433ffa4e2d73
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	117
Optimality of the best value was proved	NO
Number of terms in the objective function	8
Biggest coefficient in the objective function	128
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	255
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	138
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	535
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	5.96709
Number of variables	464
Total number of constraints	1395
Number of constraints which are clauses	336
Number of constraints which are cardinality constraints (but not clauses)	336
Number of constraints which are nor clauses,nor cardinality constraints	723
Minimum length of a constraint	1
Maximum length of a constraint	128
Trace number 13638

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        780332 kB
Buffers:         33456 kB
Cached:         197812 kB
SwapCached:          0 kB
Active:          48444 kB
Inactive:       185676 kB
HighTotal:      131008 kB
HighFree:        14448 kB
LowTotal:       903652 kB
LowFree:        765884 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              20 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14520 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 21:30:17 (client local time) WITH STATUS 10 IN 1200.59 SECONDS
stats: 14596 7 1200.59 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1069 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................
c ---[1028]---> Adder-cost: 14   maxlim: 116   bits: 8/7
c ---[1026]---> Adder-cost: 42   maxlim: 38   bits: 6/6
c ---[1024]---> Adder-cost: 42   maxlim: 29   bits: 6/5
c ---[1022]---> Adder-cost: 42   maxlim: 27   bits: 6/5
c ---[1020]---> Adder-cost: 42   maxlim: 33   bits: 6/6
c ---[1018]---> Adder-cost: 42   maxlim: 28   bits: 6/5
c ---[1016]---> Adder-cost: 42   maxlim: 25   bits: 6/5
c ---[1014]---> Adder-cost: 42   maxlim: 26   bits: 6/5
c ---[1012]---> Adder-cost: 42   maxlim: 38   bits: 6/6
c ---[1010]---> Adder-cost: 42   maxlim: 40   bits: 6/6
c ---[1009]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[1008]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[1007]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[1006]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[1005]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[1004]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[1003]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[1002]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[1001]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[1000]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 999]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 998]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 997]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 996]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 995]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 994]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 993]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 992]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 991]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 990]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 989]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 988]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 987]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 986]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 985]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 984]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 983]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 982]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 981]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 980]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 979]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 978]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 977]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 976]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 975]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 974]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 973]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 972]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 971]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 970]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 969]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 968]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 967]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 966]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 965]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 964]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 963]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 962]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 961]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 960]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 959]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 958]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 957]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 956]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 955]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 954]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 953]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 952]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 951]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 950]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 949]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 948]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 947]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 946]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 945]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 944]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 943]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 942]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 941]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 940]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 939]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 938]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 937]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 936]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 935]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 934]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 933]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 932]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 931]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 930]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 929]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 928]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 927]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 926]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 925]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 924]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 923]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 922]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 921]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 920]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 919]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 918]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 917]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 916]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 915]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 914]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 913]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 912]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 911]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 910]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 909]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 908]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 907]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 906]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 905]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 904]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 903]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 902]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 901]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 900]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 899]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 898]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 897]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 896]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 895]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 894]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 893]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 892]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 891]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 890]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 889]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 888]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 887]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 886]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 885]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 884]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 883]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 882]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 881]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 880]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 879]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 878]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 877]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 876]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 875]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 874]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 873]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 872]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 871]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 870]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 869]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 868]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 867]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 866]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 865]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 864]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 863]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 862]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 861]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 860]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 859]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 858]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 857]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 856]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 855]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 854]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 853]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 852]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 851]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 850]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 849]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 848]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 847]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 846]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 845]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 844]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 843]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 842]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 841]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 840]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 839]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 838]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 837]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 836]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 835]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 834]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 833]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 832]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 831]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 830]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 829]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 828]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 827]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 826]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 825]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 824]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 823]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 822]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 821]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 820]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 819]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 818]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 817]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 816]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 815]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 814]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 813]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 812]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 811]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 810]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 809]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 808]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 807]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 806]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 805]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 804]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 803]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 802]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 801]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 800]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 799]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 798]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 797]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 796]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 795]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 794]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 793]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 792]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 791]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 790]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 789]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 788]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 787]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 786]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 785]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 784]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 783]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 782]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 781]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 780]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 779]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 778]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 777]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 776]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 775]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 774]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 773]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 772]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 771]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 770]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 769]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 768]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 767]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 766]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 765]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 764]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 763]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 762]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 761]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 760]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 759]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 758]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 757]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 756]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 755]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 754]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 753]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 752]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 751]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 750]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 749]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 748]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 747]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 746]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 745]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 744]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 743]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 742]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 741]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 740]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 739]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 738]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 737]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 736]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 735]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 734]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 733]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 732]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 731]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 730]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 729]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 728]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 727]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 726]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 725]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 724]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 723]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 722]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 721]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 720]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 719]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 718]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 717]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 716]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 715]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 714]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 713]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 712]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 711]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 710]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 709]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 708]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 707]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 706]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 705]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 704]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 703]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 702]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 701]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 700]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 699]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 698]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 697]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 696]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 695]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 694]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 693]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 692]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 691]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 690]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 689]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 688]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 687]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 686]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 685]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 684]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 683]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 682]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 681]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 680]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 679]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 678]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 677]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 676]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 675]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 674]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 505]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 504]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 503]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 502]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 501]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 500]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 499]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 498]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 497]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 496]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 495]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 494]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 493]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 492]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 491]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 490]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 489]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 488]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 487]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 486]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 485]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 484]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 483]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 482]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 481]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 480]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 479]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 478]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 477]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 476]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 475]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 474]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 473]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 472]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 471]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 470]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 469]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 468]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 467]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 466]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 465]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 464]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 463]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 462]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 461]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 460]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 459]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 458]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 457]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 456]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 455]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 454]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 453]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 452]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 451]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 450]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 449]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 448]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 447]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 446]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 445]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 444]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 443]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 442]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 441]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 440]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 439]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 438]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 437]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 436]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 435]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 434]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 433]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 432]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 431]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 430]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 429]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 428]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 427]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 426]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 425]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 424]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 423]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 422]---> Adder-cost: 11   maxlim: 6   bits: 4/3
c ---[ 421]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 420]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 419]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 418]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 417]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 416]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 415]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 414]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 413]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 412]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 411]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 410]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 409]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 408]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 407]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 406]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 405]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 404]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 403]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 402]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 401]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 400]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 399]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 398]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 397]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 396]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 395]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 394]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 393]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 392]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 391]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 390]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 389]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 388]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 387]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 386]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 385]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 384]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 383]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 382]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 381]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 380]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 379]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 378]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 377]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 376]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 375]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 374]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 373]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 372]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 371]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 370]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 369]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 368]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 367]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 366]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 365]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 364]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 363]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 362]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 361]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 360]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 359]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 358]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 357]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 356]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 355]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 354]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 353]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 352]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 351]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 350]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 349]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 348]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 347]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 346]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 345]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 344]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 343]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 342]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 341]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 340]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 339]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 338]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 337]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 336]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 335]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 334]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 333]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 332]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 331]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 330]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 329]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 328]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 327]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 326]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 325]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 324]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 323]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 322]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 321]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 320]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 319]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 318]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 317]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 316]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 315]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 314]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 313]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 312]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 311]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 310]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 309]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 308]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 307]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 306]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 305]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 304]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 303]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 302]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 301]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 300]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 299]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 298]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 297]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 296]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 295]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 294]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 293]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 292]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 291]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 290]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 289]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 288]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 287]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 286]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 285]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 284]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 283]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 282]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 281]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 280]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 279]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 278]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 277]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 276]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 275]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 274]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 273]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 272]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 271]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 270]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 269]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 268]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 267]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 266]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 265]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 264]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 263]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 262]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 261]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 260]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 259]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 258]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 257]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 256]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 255]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 254]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 253]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 252]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 251]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 250]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 249]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 248]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 247]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 246]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 245]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 244]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 243]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 242]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 241]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 240]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 239]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 238]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 237]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 236]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 235]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 234]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 233]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 232]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 231]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 230]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 229]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 228]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 227]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 226]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 225]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 224]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 223]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 222]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 221]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 220]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 219]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 218]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 217]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 216]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 215]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 214]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 213]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 212]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 211]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 210]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 209]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 208]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 207]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 206]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 205]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 204]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 203]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 202]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 201]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 200]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 199]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 198]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 197]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 196]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 195]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 194]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 193]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 192]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 191]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 190]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 189]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 188]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 187]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 186]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 185]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 184]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 183]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 182]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 181]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 180]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 179]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 178]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 177]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 176]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 175]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 174]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 173]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 172]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 171]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[ 170]---> Adder-cost: 7   maxlim: 7   bits: 4/3
c ---[   0]---> Adder-cost: 227   maxlim: 255   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25446    85117 |    8482       0        0     nan |  0.000 % |
c |       100 |   25446    85117 |    9330     100      472     4.7 | 20.894 % |
c |       250 |   25446    85117 |   10263     250     1512     6.0 | 20.895 % |
c |       475 |   25424    85047 |   11289     472     2884     6.1 | 20.937 % |
c |       812 |   25416    85021 |   12418     808     5295     6.6 | 20.951 % |
c |      1318 |   25408    84995 |   13660    1313     9354     7.1 | 20.966 % |
c |      2077 |   25392    84943 |   15026    2070    17139     8.3 | 20.994 % |
c |      3216 |   25386    84925 |   16529    3208    27877     8.7 | 21.008 % |
c |      4925 |   25370    84873 |   18181    4915    48847     9.9 | 21.037 % |
c |      7490 |   25370    84873 |   20000    7480    86486    11.6 | 21.037 % |
c |     11335 |   25370    84873 |   22000   11325   145894    12.9 | 21.037 % |
c |     17102 |   25370    84873 |   24200   17092   246204    14.4 | 21.037 % |
c ==============================================================================
c [1mFound solution: 127[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21145 |   25323    84715 |    8441   21135   322106    15.2 | 21.037 % |
c |     21245 |   25323    84715 |    9285    5384    72659    13.5 | 21.108 % |
c |     21396 |   25323    84715 |   10213    5535    74656    13.5 | 21.108 % |
c |     21621 |   25323    84715 |   11234    5760    77406    13.4 | 21.108 % |
c |     21958 |   25323    84715 |   12358    6097    80770    13.2 | 21.108 % |
c |     22464 |   25323    84715 |   13594    6603    95010    14.4 | 21.108 % |
c |     23224 |   25323    84715 |   14953    7363   111865    15.2 | 21.108 % |
c |     24363 |   25323    84715 |   16449    8502   137495    16.2 | 21.108 % |
c |     26072 |   25323    84715 |   18094   10211   168159    16.5 | 21.108 % |
c |     28635 |   25323    84715 |   19903   12774   255725    20.0 | 21.108 % |
c |     32480 |   25317    84697 |   21893   16618   337824    20.3 | 21.122 % |
c |     38251 |   25317    84697 |   24083   22389   523828    23.4 | 21.122 % |
c |     46900 |   25317    84697 |   26491   17866   485838    27.2 | 21.122 % |
c |     59874 |   25317    84697 |   29140   15786   437986    27.7 | 21.122 % |
c |     79336 |   25317    84697 |   32054   18939   396671    20.9 | 21.122 % |
c ==============================================================================
c [1mFound solution: 126[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     96376 |   25318    84703 |    8439   17295   324903    18.8 | 21.122 % |
c |     96478 |   25318    84703 |    9282    8750   135907    15.5 | 21.122 % |
c |     96628 |   25318    84703 |   10211    8900   137265    15.4 | 21.122 % |
c |     96854 |   25318    84703 |   11232    9126   139716    15.3 | 21.122 % |
c |     97192 |   25318    84703 |   12355    9464   144132    15.2 | 21.122 % |
c |     97698 |   25318    84703 |   13591    9970   152259    15.3 | 21.122 % |
c |     98457 |   25318    84703 |   14950   10729   168065    15.7 | 21.122 % |
c |     99596 |   25318    84703 |   16445   11868   184141    15.5 | 21.122 % |
c |    101304 |   25318    84703 |   18089   13576   214006    15.8 | 21.122 % |
c |    103867 |   25318    84703 |   19898   16139   279653    17.3 | 21.122 % |
c |    107711 |   25318    84703 |   21888   19983   367812    18.4 | 21.122 % |
c |    113478 |   25318    84703 |   24077   13691   314760    23.0 | 21.122 % |
c |    122129 |   25318    84703 |   26485   22342   563186    25.2 | 21.122 % |
c |    135103 |   25318    84703 |   29133   21077   579979    27.5 | 21.122 % |
c |    154564 |   25318    84703 |   32047   23210   668028    28.8 | 21.122 % |
c |    183756 |   25318    84703 |   35251   33191  1029702    31.0 | 21.122 % |
c ==============================================================================
c [1mFound solution: 125[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Adder-cost: 4   maxlim: 2   bits: 3/2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    185687 |   25337    84770 |    8445   35122  1079538    30.7 | 21.122 % |
c |    185787 |   25337    84770 |    9289    8250   178378    21.6 | 21.130 % |
c |    185937 |   25337    84770 |   10218    8400   180015    21.4 | 21.130 % |
c |    186162 |   25337    84770 |   11240    8625   183536    21.3 | 21.130 % |
c |    186499 |   25337    84770 |   12364    8962   191576    21.4 | 21.130 % |
c |    187005 |   25337    84770 |   13600    9468   204574    21.6 | 21.130 % |
c |    187766 |   25337    84770 |   14960   10229   221992    21.7 | 21.130 % |
c |    188905 |   25337    84770 |   16456   11368   241647    21.3 | 21.130 % |
c |    190613 |   25331    84752 |   18102   13075   269915    20.6 | 21.144 % |
c |    193175 |   25331    84752 |   19912   15637   358794    22.9 | 21.144 % |
c |    197021 |   25331    84752 |   21904   19483   458718    23.5 | 21.144 % |
c |    202787 |   25331    84752 |   24094   12991   301924    23.2 | 21.144 % |
c |    211436 |   25331    84752 |   26504   21640   589189    27.2 | 21.144 % |
c |    224410 |   25331    84752 |   29154   20468   439890    21.5 | 21.144 % |
c |    243874 |   25331    84752 |   32069   23645   803999    34.0 | 21.144 % |
c |    273066 |   25331    84752 |   35276   33230   872677    26.3 | 21.144 % |
c |    316855 |   25323    84726 |   38804   33489  1112200    33.2 | 21.158 % |
c ==============================================================================
c [1mFound solution: 123[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Adder-cost: 6   maxlim: 4   bits: 4/3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    345816 |   25347    84806 |    8449   36388  1056577    29.0 | 21.158 % |
c |    345917 |   25347    84806 |    9293    8321   160091    19.2 | 21.160 % |
c |    346067 |   25347    84806 |   10223    8471   161980    19.1 | 21.160 % |
c |    346292 |   25347    84806 |   11245    8696   164527    18.9 | 21.160 % |
c |    346630 |   25347    84806 |   12370    9034   169672    18.8 | 21.160 % |
c |    347137 |   25347    84806 |   13607    9541   178787    18.7 | 21.160 % |
c |    347897 |   25347    84806 |   14967   10301   194988    18.9 | 21.160 % |
c |    349037 |   25347    84806 |   16464   11441   223784    19.6 | 21.160 % |
c |    350745 |   25347    84806 |   18111   13149   269332    20.5 | 21.160 % |
c |    353307 |   25347    84806 |   19922   15711   331415    21.1 | 21.160 % |
c |    357151 |   25347    84806 |   21914   19555   416440    21.3 | 21.160 % |
c |    362917 |   25347    84806 |   24105   12965   330361    25.5 | 21.160 % |
c |    371566 |   25347    84806 |   26516   21614   694942    32.2 | 21.160 % |
c |    384540 |   25347    84806 |   29168   20386   575561    28.2 | 21.160 % |
c |    404002 |   25347    84806 |   32085   22266   868307    39.0 | 21.160 % |
c |    433194 |   25340    84783 |   35293   31764  1012005    31.9 | 21.174 % |
c |    476984 |   25340    84783 |   38822   29048  1281905    44.1 | 21.174 % |
c |    542668 |   25340    84783 |   42705   39962  1922844    48.1 | 21.174 % |
c |    641194 |   25333    84760 |   46975   24410   821833    33.7 | 21.188 % |
c ==============================================================================
c [1mFound solution: 119[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Adder-cost: 8   maxlim: 8   bits: 5/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    691844 |   25362    84853 |    8454   44157  1234434    28.0 | 21.188 % |
c |    691944 |   25362    84853 |    9299    8600   161980    18.8 | 21.183 % |
c |    692094 |   25362    84853 |   10229    8750   163781    18.7 | 21.183 % |
c |    692320 |   25362    84853 |   11252    8976   166336    18.5 | 21.183 % |
c |    692657 |   25362    84853 |   12377    9313   170359    18.3 | 21.183 % |
c |    693163 |   25362    84853 |   13615    9819   175784    17.9 | 21.183 % |
c |    693922 |   25362    84853 |   14976   10578   195404    18.5 | 21.183 % |
c |    695061 |   25362    84853 |   16474   11717   230603    19.7 | 21.183 % |
c |    696769 |   25362    84853 |   18121   13425   268158    20.0 | 21.183 % |
c |    699333 |   25362    84853 |   19934   15989   379211    23.7 | 21.183 % |
c |    703177 |   25362    84853 |   21927   19833   470185    23.7 | 21.183 % |
c |    708944 |   25362    84853 |   24120   25600   712846    27.8 | 21.183 % |
c |    717593 |   25362    84853 |   26532   20985   589201    28.1 | 21.183 % |
c |    730569 |   25362    84853 |   29185   19825   738719    37.3 | 21.183 % |
c |    750030 |   25362    84853 |   32104   20719   890847    43.0 | 21.183 % |
c |    779222 |   25362    84853 |   35314   28609  1212363    42.4 | 21.183 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v C0377_bit0 C0377_bit1 C0377_bit2 -C0377_bit3 C0377_bit4 C0377_bit5 C0377_bit6 -C0377_bit7 C0001_bit0 C0002_bit0 C0003_bit0 C0004_bit0 -C0005_bit0 C0006_bit0 C0007_bit0 C0008_bit0 C0009_bit0 -C0010_bit0 C0011_bit0 -C0012_bit0 C0013_bit0 -C0014_bit0 -C0015_bit0 C0016_bit0 -C0017_bit0 C0018_bit0 -C0019_bit0 -C0020_bit0 C0021_bit0 C0022_bit0 C0023_bit0 C0024_bit0 C0025_bit0 C0026_bit0 C0027_bit0 C0028_bit0 C0029_bit0 C0030_bit0 C0031_bit0 C0032_bit0 -C0033_bit0 -C0034_bit0 C0035_bit0 C0036_bit0 -C0037_bit0 C0038_bit0 C0039_bit0 C0040_bit0 C0041_bit0 -C0042_bit0 C0043_bit0 C0044_bit0 -C0045_bit0 C0046_bit0 C0047_bit0 -C0048_bit0 C0049_bit0 -C0050_bit0 C0051_bit0 -C0052_bit0 -C0053_bit0 -C0054_bit0 -C0055_bit0 -C0056_bit0 -C0057_bit0 C0058_bit0 C0059_bit0 -C0060_bit0 -C0061_bit0 -C0062_bit0 -C0063_bit0 -C0064_bit0 -C0065_bit0 -C0066_bit0 -C0067_bit0 -C0068_bit0 -C0069_bit0 -C0070_bit0 -C0071_bit0 -C0072_bit0 -C0073_bit0 -C0074_bit0 C0075_bit0 C0076_bit0 C0077_bit0 C0078_bit0 -C0079_bit0 C0080_bit0 -C0081_bit0 C0082_bit0 C0083_bit0 -C0084_bit0 -C0085_bit0 -C0086_bit0 -C0087_bit0 -C0088_bit0 C0089_bit0 -C0090_bit0 -C0091_bit0 -C0092_bit0 -C0093_bit0 C0094_bit0 -C0095_bit0 C0096_bit0 -C0097_bit0 C0098_bit0 C0099_bit0 -C0100_bit0 C0101_bit0 -C0102_bit0 C0103_bit0 C0104_bit0 -C0105_bit0 -C0106_bit0 -C0107_bit0 -C0108_bit0 -C0109_bit0 -C0110_bit0 -C0111_bit0 -C0112_bit0 -C0113_bit0 -C0114_bit0 -C0115_bit0 -C0116_bit0 C0117_bit0 C0118_bit0 -C0119_bit0 -C0120_bit0 C0121_bit0 -C0122_bit0 -C0123_bit0 -C0124_bit0 -C0125_bit0 C0126_bit0 -C0127_bit0 -C0128_bit0 C0129_bit0 -C0130_bit0 -C0131_bit0 C0132_bit0 -C0133_bit0 C0134_bit0 -C0135_bit0 C0136_bit0 C0137_bit0 C0138_bit0 C0139_bit0 C0140_bit0 C0141_bit0 -C0142_bit0 -C0143_bit0 C0144_bit0 C0145_bit0 C0146_bit0 C0147_bit0 C0148_bit0 C0149_bit0 C0150_bit0 C0151_bit0 C0152_bit0 C0153_bit0 C0154_bit0 C0155_bit0 C0156_bit0 C0157_bit0 C0158_bit0 -C0159_bit0 -C0160_bit0 -C0161_bit0 -C0162_bit0 C0163_bit0 -C0164_bit0 C0165_bit0 -C0166_bit0 -C0167_bit0 C0168_bit0 C0169_bit0 -C0170_bit0 C0171_bit0 C0172_bit0 C0173_bit0 C0174_bit0 -C0175_bit0 -C0176_bit0 -C0177_bit0 C0178_bit0 C0179_bit0 C0180_bit0 C0181_bit0 C0182_bit0 C0183_bit0 -C0184_bit0 C0185_bit0 C0186_bit0 C0187_bit0 C0188_bit0 C0189_bit0 -C0190_bit0 -C0191_bit0 -C0192_bit0 C0193_bit0 -C0194_bit0 -C0195_bit0 C0196_bit0 C0197_bit0 C0198_bit0 C0199_bit0 -C0200_bit0 -C0201_bit0 C0202_bit0 -C0203_bit0 -C0204_bit0 C0205_bit0 -C0206_bit0 -C0207_bit0 -C0208_bit0 -C0209_bit0 -C0210_bit0 -C0211_bit0 -C0212_bit0 -C0213_bit0 -C0214_bit0 -C0215_bit0 -C0216_bit0 -C0217_bit0 C0218_bit0 C0219_bit0 -C0220_bit0 -C0221_bit0 C0222_bit0 C0223_bit0 -C0224_bit0 -C0225_bit0 C0226_bit0 -C0227_bit0 -C0228_bit0 -C0229_bit0 -C0230_bit0 C0231_bit0 -C0232_bit0 C0233_bit0 C0234_bit0 -C0235_bit0 -C0236_bit0 -C0237_bit0 C0238_bit0 C0239_bit0 -C0240_bit0 -C0241_bit0 -C0242_bit0 C0243_bit0 -C0244_bit0 -C0245_bit0 -C0246_bit0 -C0247_bit0 -C0248_bit0 -C0249_bit0 C0250_bit0 C0251_bit0 C0252_bit0 -C0253_bit0 C0254_bit0 -C0255_bit0 -C0256_bit0 -C0257_bit0 -C0258_bit0 C0259_bit0 C0260_bit0 C0261_bit0 -C0262_bit0 -C0263_bit0 -C0264_bit0 -C0265_bit0 -C0266_bit0 -C0267_bit0 C0268_bit0 -C0269_bit0 -C0270_bit0 -C0271_bit0 -C0272_bit0 -C0273_bit0 C0274_bit0 C0275_bit0 C0276_bit0 -C0277_bit0 C0278_bit0 C0279_bit0 -C0280_bit0 -C0281_bit0 -C0282_bit0 -C0283_bit0 C0284_bit0 C0285_bit0 -C0286_bit0 C0287_bit0 C0288_bit0 -C0289_bit0 C0290_bit0 C0291_bit0 C0292_bit0 C0293_bit0 C0294_bit0 C0295_bit0 C0296_bit0 C0297_bit0 C0298_bit0 C0299_bit0 C0300_bit0 C0301_bit0 -C0302_bit0 -C0303_bit0 C0304_bit0 C0305_bit0 -C0306_bit0 -C0307_bit0 C0308_bit0 C0309_bit0 -C0310_bit0 C0311_bit0 C0312_bit0 C0313_bit0 C0314_bit0 -C0315_bit0 C0316_bit0 -C0317_bit0 -C0318_bit0 C0319_bit0 C0320_bit0 C0321_bit0 -C0322_bit0 -C0323_bit0 C0324_bit0 C0325_bit0 C0326_bit0 -C0327_bit0 C0328_bit0 C0329_bit0 C0330_bit0 C0331_bit0 C0332_bit0 C0333_bit0 -C0334_bit0 -C0335_bit0 -C0336_bit0 C0337_bit0 -C0337_bit1 -C0337_bit2 -C0338_bit0 C0338_bit1 -C0338_bit2 C0339_bit0 -C0339_bit1 C0339_bit#### 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.73 0.88 0.87 2/54 15590
Raw data (stat): 15590 (runsolver) R 15589 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 467784809 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.77 0.89 0.87 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 1312 0 0 0 995 3 0 0 25 0 1 0 467784809 7090176 1289 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1731 1289 603 41 0 1690 0
vsize: 6924
[startup+20.0011 s]
Raw data (loadavg): 0.80 0.89 0.88 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 1488 0 0 0 1994 4 0 0 25 0 1 0 467784809 7798784 1465 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1904 1465 603 41 0 1863 0
vsize: 7616
[startup+30.0014 s]
Raw data (loadavg): 0.83 0.89 0.88 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 1628 0 0 0 2993 5 0 0 25 0 1 0 467784809 8335360 1605 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2035 1605 603 41 0 1994 0
vsize: 8140
[startup+40.0017 s]
Raw data (loadavg): 0.86 0.89 0.88 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 1880 0 0 0 3992 6 0 0 25 0 1 0 467784809 9416704 1857 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2299 1857 603 41 0 2258 0
vsize: 9196
[startup+50.0034 s]
Raw data (loadavg): 0.88 0.90 0.88 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 1898 0 0 0 4992 7 0 0 25 0 1 0 467784809 9416704 1875 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2299 1875 603 41 0 2258 0
vsize: 9196
[startup+60.0042 s]
Raw data (loadavg): 0.90 0.90 0.88 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2086 0 0 0 5991 8 0 0 25 0 1 0 467784809 10227712 2063 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2497 2063 603 41 0 2456 0
vsize: 9988
[startup+70.005 s]
Raw data (loadavg): 0.91 0.90 0.88 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2141 0 0 0 6990 8 0 0 25 0 1 0 467784809 10493952 2118 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2562 2118 603 41 0 2521 0
vsize: 10248
[startup+80.0053 s]
Raw data (loadavg): 0.93 0.91 0.88 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2143 0 0 0 7990 9 0 0 25 0 1 0 467784809 10493952 2120 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2562 2120 603 41 0 2521 0
vsize: 10248
[startup+90.0056 s]
Raw data (loadavg): 0.94 0.91 0.88 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2150 0 0 0 8990 9 0 0 25 0 1 0 467784809 10493952 2127 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2562 2127 603 41 0 2521 0
vsize: 10248
[startup+100.014 s]
Raw data (loadavg): 0.95 0.91 0.88 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2158 0 0 0 9990 9 0 0 25 0 1 0 467784809 10493952 2135 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2562 2135 603 41 0 2521 0
vsize: 10248
[startup+110.022 s]
Raw data (loadavg): 0.95 0.91 0.88 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2202 0 0 0 10990 10 0 0 25 0 1 0 467784809 10891264 2179 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2179 603 41 0 2618 0
vsize: 10636
[startup+120.026 s]
Raw data (loadavg): 0.96 0.92 0.89 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2203 0 0 0 11989 10 0 0 25 0 1 0 467784809 10891264 2180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2180 603 41 0 2618 0
vsize: 10636
[startup+130.029 s]
Raw data (loadavg): 0.97 0.92 0.89 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2203 0 0 0 12989 10 0 0 25 0 1 0 467784809 10891264 2180 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2180 603 41 0 2618 0
vsize: 10636
[startup+140.028 s]
Raw data (loadavg): 0.97 0.92 0.89 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2203 0 0 0 13988 10 0 0 25 0 1 0 467784809 10891264 2180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2180 603 41 0 2618 0
vsize: 10636
[startup+150.029 s]
Raw data (loadavg): 0.97 0.92 0.89 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2203 0 0 0 14988 11 0 0 25 0 1 0 467784809 10891264 2180 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2180 603 41 0 2618 0
vsize: 10636
[startup+160.03 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2203 0 0 0 15987 11 0 0 25 0 1 0 467784809 10891264 2180 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2659 2180 603 41 0 2618 0
vsize: 10636
[startup+170.029 s]
Raw data (loadavg): 0.98 0.93 0.89 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2341 0 0 0 16986 12 0 0 25 0 1 0 467784809 11427840 2318 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2790 2318 603 41 0 2749 0
vsize: 11160
[startup+180.03 s]
Raw data (loadavg): 0.98 0.93 0.89 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2344 0 0 0 17986 12 0 0 25 0 1 0 467784809 11427840 2321 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2790 2321 603 41 0 2749 0
vsize: 11160
[startup+190.03 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2383 0 0 0 18985 13 0 0 25 0 1 0 467784809 11563008 2360 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2823 2360 603 41 0 2782 0
vsize: 11292
[startup+200.031 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2383 0 0 0 19985 13 0 0 25 0 1 0 467784809 11563008 2360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2823 2360 603 41 0 2782 0
vsize: 11292
[startup+210.031 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2383 0 0 0 20985 13 0 0 25 0 1 0 467784809 11563008 2360 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2823 2360 603 41 0 2782 0
vsize: 11292
[startup+220.032 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2540 0 0 0 21984 14 0 0 25 0 1 0 467784809 12234752 2517 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2987 2517 603 41 0 2946 0
vsize: 11948
[startup+230.032 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2540 0 0 0 22983 15 0 0 25 0 1 0 467784809 12234752 2517 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2987 2517 603 41 0 2946 0
vsize: 11948
[startup+240.032 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2540 0 0 0 23983 15 0 0 25 0 1 0 467784809 12234752 2517 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2987 2517 603 41 0 2946 0
vsize: 11948
[startup+250.034 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2540 0 0 0 24982 16 0 0 25 0 1 0 467784809 12234752 2517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2987 2517 603 41 0 2946 0
vsize: 11948
[startup+260.034 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2540 0 0 0 25982 16 0 0 25 0 1 0 467784809 12234752 2517 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2987 2517 603 41 0 2946 0
vsize: 11948
[startup+270.035 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2540 0 0 0 26982 16 0 0 25 0 1 0 467784809 12234752 2517 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2987 2517 603 41 0 2946 0
vsize: 11948
[startup+280.036 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2540 0 0 0 27981 16 0 0 25 0 1 0 467784809 12234752 2517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2987 2517 603 41 0 2946 0
vsize: 11948
[startup+290.036 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2540 0 0 0 28981 16 0 0 25 0 1 0 467784809 12234752 2517 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2987 2517 603 41 0 2946 0
vsize: 11948
[startup+300.037 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2546 0 0 0 29981 17 0 0 25 0 1 0 467784809 12234752 2523 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2987 2523 603 41 0 2946 0
vsize: 11948
[startup+310.038 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2566 0 0 0 30980 17 0 0 25 0 1 0 467784809 12369920 2543 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3020 2543 603 41 0 2979 0
vsize: 12080
[startup+320.038 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2579 0 0 0 31980 17 0 0 25 0 1 0 467784809 12369920 2556 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3020 2556 603 41 0 2979 0
vsize: 12080
[startup+330.038 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2584 0 0 0 32980 17 0 0 25 0 1 0 467784809 12369920 2561 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3020 2561 603 41 0 2979 0
vsize: 12080
[startup+340.044 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2591 0 0 0 33980 18 0 0 25 0 1 0 467784809 12509184 2568 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2568 603 41 0 3013 0
vsize: 12216
[startup+350.045 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2591 0 0 0 34980 18 0 0 25 0 1 0 467784809 12509184 2568 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2568 603 41 0 3013 0
vsize: 12216
[startup+360.065 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2591 0 0 0 35982 18 0 0 25 0 1 0 467784809 12509184 2568 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3054 2568 603 41 0 3013 0
vsize: 12216
[startup+370.065 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2663 0 0 0 36981 19 0 0 25 0 1 0 467784809 12791808 2640 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3123 2640 603 41 0 3082 0
vsize: 12492
[startup+380.069 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2799 0 0 0 37980 20 0 0 25 0 1 0 467784809 13328384 2776 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3254 2776 603 41 0 3213 0
vsize: 13016
[startup+390.073 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2801 0 0 0 38980 20 0 0 25 0 1 0 467784809 13328384 2778 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3254 2778 603 41 0 3213 0
vsize: 13016
[startup+400.078 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2810 0 0 0 39981 20 0 0 25 0 1 0 467784809 13328384 2787 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3254 2787 603 41 0 3213 0
vsize: 13016
[startup+410.078 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2950 0 0 0 40979 22 0 0 25 0 1 0 467784809 13860864 2927 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3384 2927 603 41 0 3343 0
vsize: 13536
[startup+420.079 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2989 0 0 0 41979 22 0 0 25 0 1 0 467784809 14131200 2966 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2966 603 41 0 3409 0
vsize: 13800
[startup+430.086 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2989 0 0 0 42979 22 0 0 25 0 1 0 467784809 14131200 2966 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2966 603 41 0 3409 0
vsize: 13800
[startup+440.086 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2990 0 0 0 43979 23 0 0 25 0 1 0 467784809 14131200 2967 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2967 603 41 0 3409 0
vsize: 13800
[startup+450.091 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 2992 0 0 0 44979 23 0 0 25 0 1 0 467784809 14131200 2969 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2969 603 41 0 3409 0
vsize: 13800
[startup+460.093 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3000 0 0 0 45979 23 0 0 25 0 1 0 467784809 14131200 2977 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2977 603 41 0 3409 0
vsize: 13800
[startup+470.093 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3000 0 0 0 46979 24 0 0 25 0 1 0 467784809 14131200 2977 4294967295 134512640 134672761 3221224544 3221223720 134559668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2977 603 41 0 3409 0
vsize: 13800
[startup+480.093 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3000 0 0 0 47979 24 0 0 25 0 1 0 467784809 14131200 2977 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2977 603 41 0 3409 0
vsize: 13800
[startup+490.093 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3000 0 0 0 48978 24 0 0 25 0 1 0 467784809 14131200 2977 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2977 603 41 0 3409 0
vsize: 13800
[startup+500.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3001 0 0 0 49978 24 0 0 25 0 1 0 467784809 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+510.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3001 0 0 0 50978 24 0 0 25 0 1 0 467784809 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+520.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3001 0 0 0 51978 24 0 0 25 0 1 0 467784809 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+530.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3001 0 0 0 52979 24 0 0 25 0 1 0 467784809 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+540.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3001 0 0 0 53979 24 0 0 25 0 1 0 467784809 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+550.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3001 0 0 0 54979 24 0 0 25 0 1 0 467784809 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+560.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3001 0 0 0 55980 24 0 0 25 0 1 0 467784809 14131200 2978 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+570.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3001 0 0 0 56980 24 0 0 25 0 1 0 467784809 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+580.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3001 0 0 0 57980 24 0 0 25 0 1 0 467784809 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+590.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3001 0 0 0 58980 24 0 0 25 0 1 0 467784809 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+600.225 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3001 0 0 0 59993 24 0 0 25 0 1 0 467784809 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+610.232 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3001 0 0 0 60994 24 0 0 25 0 1 0 467784809 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+620.239 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3111 0 0 0 61994 25 0 0 25 0 1 0 467784809 14655488 3088 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3578 3088 603 41 0 3537 0
vsize: 14312
[startup+630.249 s]
Raw data (loadavg): 1.15 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3349 0 0 0 62995 26 0 0 25 0 1 0 467784809 15630336 3326 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3816 3326 603 41 0 3775 0
vsize: 15264
[startup+640.369 s]
Raw data (loadavg): 1.13 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3357 0 0 0 64007 26 0 0 25 0 1 0 467784809 15630336 3334 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3816 3334 603 41 0 3775 0
vsize: 15264
[startup+650.371 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3357 0 0 0 65007 26 0 0 25 0 1 0 467784809 15630336 3334 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3816 3334 603 41 0 3775 0
vsize: 15264
[startup+660.377 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3361 0 0 0 66008 26 0 0 25 0 1 0 467784809 15630336 3338 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3816 3338 603 41 0 3775 0
vsize: 15264
[startup+670.387 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3552 0 0 0 67009 26 0 0 25 0 1 0 467784809 16437248 3529 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4013 3529 603 41 0 3972 0
vsize: 16052
[startup+680.387 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3604 0 0 0 68009 26 0 0 25 0 1 0 467784809 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+690.394 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3604 0 0 0 69009 26 0 0 25 0 1 0 467784809 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+700.512 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3604 0 0 0 70021 26 0 0 25 0 1 0 467784809 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+710.512 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3604 0 0 0 71022 26 0 0 25 0 1 0 467784809 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+720.511 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3604 0 0 0 72022 26 0 0 25 0 1 0 467784809 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+730.512 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3604 0 0 0 73022 26 0 0 25 0 1 0 467784809 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+740.513 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3604 0 0 0 74022 26 0 0 25 0 1 0 467784809 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+750.514 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3604 0 0 0 75022 26 0 0 25 0 1 0 467784809 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+760.514 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3611 0 0 0 76023 26 0 0 25 0 1 0 467784809 16732160 3588 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4085 3588 603 41 0 4044 0
vsize: 16340
[startup+770.515 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3795 0 0 0 77022 27 0 0 25 0 1 0 467784809 17408000 3772 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4250 3772 603 41 0 4209 0
vsize: 17000
[startup+780.515 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3898 0 0 0 78021 28 0 0 25 0 1 0 467784809 17809408 3875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3875 603 41 0 4307 0
vsize: 17392
[startup+790.515 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3898 0 0 0 79021 28 0 0 25 0 1 0 467784809 17809408 3875 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3875 603 41 0 4307 0
vsize: 17392
[startup+800.516 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3898 0 0 0 80022 28 0 0 25 0 1 0 467784809 17809408 3875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3875 603 41 0 4307 0
vsize: 17392
[startup+810.516 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3898 0 0 0 81022 28 0 0 25 0 1 0 467784809 17809408 3875 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3875 603 41 0 4307 0
vsize: 17392
[startup+820.524 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3898 0 0 0 82023 28 0 0 25 0 1 0 467784809 17809408 3875 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3875 603 41 0 4307 0
vsize: 17392
[startup+830.529 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3899 0 0 0 83023 28 0 0 25 0 1 0 467784809 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+840.528 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3899 0 0 0 84024 28 0 0 25 0 1 0 467784809 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+850.528 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3899 0 0 0 85024 28 0 0 25 0 1 0 467784809 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+860.532 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3899 0 0 0 86024 28 0 0 25 0 1 0 467784809 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+870.532 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3899 0 0 0 87024 28 0 0 25 0 1 0 467784809 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+880.533 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3899 0 0 0 88025 28 0 0 25 0 1 0 467784809 17809408 3876 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+890.533 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3899 0 0 0 89025 28 0 0 25 0 1 0 467784809 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+900.534 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3900 0 0 0 90025 28 0 0 25 0 1 0 467784809 17809408 3877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3877 603 41 0 4307 0
vsize: 17392
[startup+910.534 s]
Raw data (loadavg): 1.06 1.02 0.93 3/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3901 0 0 0 91025 28 0 0 25 0 1 0 467784809 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+920.534 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3901 0 0 0 92025 28 0 0 25 0 1 0 467784809 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+930.535 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3901 0 0 0 93026 28 0 0 25 0 1 0 467784809 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+940.535 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3901 0 0 0 94026 28 0 0 25 0 1 0 467784809 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+950.535 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3901 0 0 0 95026 28 0 0 25 0 1 0 467784809 17809408 3878 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+960.536 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3901 0 0 0 96026 28 0 0 25 0 1 0 467784809 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+970.536 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3901 0 0 0 97026 28 0 0 25 0 1 0 467784809 17809408 3878 4294967295 134512640 134672761 3221224544 3221223648 134555133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+980.536 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3901 0 0 0 98026 28 0 0 25 0 1 0 467784809 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+990.537 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3901 0 0 0 99026 28 0 0 25 0 1 0 467784809 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+1000.54 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3901 0 0 0 100027 28 0 0 25 0 1 0 467784809 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+1010.54 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3914 0 0 0 101027 28 0 0 25 0 1 0 467784809 17973248 3891 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3891 603 41 0 4347 0
vsize: 17552
[startup+1020.54 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3915 0 0 0 102027 28 0 0 25 0 1 0 467784809 17973248 3892 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3892 603 41 0 4347 0
vsize: 17552
[startup+1030.54 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 103027 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1040.54 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 104027 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1050.54 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 105027 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1060.54 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 106027 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1070.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 107028 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1080.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 108027 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223728 134559176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1090.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 109027 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1100.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 110027 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1110.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 111027 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1120.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 112027 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1130.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 113028 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1140.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 114028 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1150.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 115028 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1160.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 116028 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1170.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 117028 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1180.54 s]
Raw data (loadavg): 1.00 1.00 0.93 3/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 118029 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1190.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 119029 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
[startup+1200.54 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15590
Raw data (stat): 15590 (minisat+) R 15589 26667 26666 0 -1 0 3916 0 0 0 120029 28 0 0 25 0 1 0 467784809 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4388 3893 603 41 0 4347 0
vsize: 17552
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.56 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 15590
Raw data (stat): 15590 (minisat+) Z 15589 26667 26666 0 -1 12 3919 0 0 0 120029 29 0 0 25 0 1 0 467784809 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: 10
Real time (s): 1200.56
CPU time (s): 1200.59
CPU user time (s): 1200.3
CPU system time (s): 0.296954
CPU usage (%): 100.003
Max. virtual memory (Kb): 17552
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####