PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-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	6.02808
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 14672

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        833420 kB
Buffers:         32188 kB
Cached:         139492 kB
SwapCached:        564 kB
Active:          20676 kB
Inactive:       153036 kB
HighTotal:      131008 kB
HighFree:        51520 kB
LowTotal:       903652 kB
LowFree:        781900 kB
SwapTotal:     2097892 kB
SwapFree:      2096484 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           5232 kB
Slab:            21648 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 00:59:24 (client local time) WITH STATUS 10 IN 1200.14 SECONDS
stats: 19601 7 1200.14 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.62 0.87 0.88 2/54 10125
Raw data (stat): 10125 (runsolver) R 10124 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540823278 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.0002 s]
Raw data (loadavg): 0.68 0.87 0.88 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 1311 0 0 0 995 3 0 0 25 0 1 0 540823278 7090176 1288 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1731 1288 603 41 0 1690 0
vsize: 6924
[startup+20.0015 s]
Raw data (loadavg): 0.73 0.87 0.88 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 1488 0 0 0 1994 4 0 0 25 0 1 0 540823278 7798784 1465 4294967295 134512640 134672761 3221224544 3221223712 134560852 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.0023 s]
Raw data (loadavg): 0.77 0.88 0.88 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 1627 0 0 0 2994 5 0 0 25 0 1 0 540823278 8335360 1604 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2035 1604 603 41 0 1994 0
vsize: 8140
[startup+40.0017 s]
Raw data (loadavg): 0.80 0.88 0.88 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 1880 0 0 0 3993 6 0 0 25 0 1 0 540823278 9416704 1857 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.0029 s]
Raw data (loadavg): 0.83 0.89 0.88 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 1898 0 0 0 4993 6 0 0 25 0 1 0 540823278 9416704 1875 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.0027 s]
Raw data (loadavg): 0.86 0.89 0.88 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2079 0 0 0 5992 7 0 0 25 0 1 0 540823278 10227712 2056 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2497 2056 603 41 0 2456 0
vsize: 9988
[startup+70.0032 s]
Raw data (loadavg): 0.88 0.89 0.88 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2141 0 0 0 6992 7 0 0 25 0 1 0 540823278 10493952 2118 4294967295 134512640 134672761 3221224544 3221223712 134561005 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.0044 s]
Raw data (loadavg): 0.90 0.89 0.88 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2143 0 0 0 7991 7 0 0 25 0 1 0 540823278 10493952 2120 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.0042 s]
Raw data (loadavg): 0.91 0.90 0.89 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2150 0 0 0 8991 8 0 0 25 0 1 0 540823278 10493952 2127 4294967295 134512640 134672761 3221224544 3221223696 134565092 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.005 s]
Raw data (loadavg): 0.93 0.90 0.89 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2155 0 0 0 9991 8 0 0 25 0 1 0 540823278 10493952 2132 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2562 2132 603 41 0 2521 0
vsize: 10248
[startup+110.006 s]
Raw data (loadavg): 0.94 0.90 0.89 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2202 0 0 0 10990 9 0 0 25 0 1 0 540823278 10891264 2179 4294967295 134512640 134672761 3221224544 3221223760 134558086 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.006 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2203 0 0 0 11990 9 0 0 25 0 1 0 540823278 10891264 2180 4294967295 134512640 134672761 3221224544 3221223712 134560852 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.007 s]
Raw data (loadavg): 1.04 0.93 0.89 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2203 0 0 0 12990 9 0 0 25 0 1 0 540823278 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+140.007 s]
Raw data (loadavg): 1.03 0.93 0.90 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2203 0 0 0 13990 10 0 0 25 0 1 0 540823278 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.008 s]
Raw data (loadavg): 1.03 0.93 0.90 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2203 0 0 0 14989 10 0 0 25 0 1 0 540823278 10891264 2180 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.008 s]
Raw data (loadavg): 1.02 0.93 0.90 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2203 0 0 0 15989 10 0 0 25 0 1 0 540823278 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+170.009 s]
Raw data (loadavg): 1.02 0.93 0.90 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2341 0 0 0 16988 12 0 0 25 0 1 0 540823278 11427840 2318 4294967295 134512640 134672761 3221224544 3221223712 134561205 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.009 s]
Raw data (loadavg): 1.02 0.94 0.90 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2344 0 0 0 17988 12 0 0 25 0 1 0 540823278 11427840 2321 4294967295 134512640 134672761 3221224544 3221223728 134558899 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.01 s]
Raw data (loadavg): 1.01 0.94 0.90 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2383 0 0 0 18988 12 0 0 25 0 1 0 540823278 11563008 2360 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.01 s]
Raw data (loadavg): 1.01 0.94 0.90 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2383 0 0 0 19988 13 0 0 25 0 1 0 540823278 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+210.01 s]
Raw data (loadavg): 1.01 0.94 0.90 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2383 0 0 0 20987 13 0 0 25 0 1 0 540823278 11563008 2360 4294967295 134512640 134672761 3221224544 3221223712 134561021 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.014 s]
Raw data (loadavg): 1.01 0.94 0.90 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2540 0 0 0 21985 14 0 0 25 0 1 0 540823278 12234752 2517 4294967295 134512640 134672761 3221224544 3221223728 134558687 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.018 s]
Raw data (loadavg): 1.00 0.94 0.90 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2540 0 0 0 22985 15 0 0 25 0 1 0 540823278 12234752 2517 4294967295 134512640 134672761 3221224544 3221223712 134561207 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.019 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2540 0 0 0 23984 15 0 0 25 0 1 0 540823278 12234752 2517 4294967295 134512640 134672761 3221224544 3221223712 134560895 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.019 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2540 0 0 0 24984 16 0 0 25 0 1 0 540823278 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.02 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2540 0 0 0 25984 16 0 0 25 0 1 0 540823278 12234752 2517 4294967295 134512640 134672761 3221224544 3221223648 134560405 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.021 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2540 0 0 0 26984 16 0 0 25 0 1 0 540823278 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+280.022 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2540 0 0 0 27984 16 0 0 25 0 1 0 540823278 12234752 2517 4294967295 134512640 134672761 3221224544 3221223724 134559056 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.021 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2540 0 0 0 28983 17 0 0 25 0 1 0 540823278 12234752 2517 4294967295 134512640 134672761 3221224544 3221223712 134561151 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.023 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2546 0 0 0 29984 17 0 0 25 0 1 0 540823278 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.022 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2566 0 0 0 30983 17 0 0 25 0 1 0 540823278 12369920 2543 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.023 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2579 0 0 0 31983 18 0 0 25 0 1 0 540823278 12369920 2556 4294967295 134512640 134672761 3221224544 3221223712 134560988 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.024 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2581 0 0 0 32983 18 0 0 25 0 1 0 540823278 12369920 2558 4294967295 134512640 134672761 3221224544 3221223728 134558914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3020 2558 603 41 0 2979 0
vsize: 12080
[startup+340.024 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2591 0 0 0 33983 18 0 0 25 0 1 0 540823278 12509184 2568 4294967295 134512640 134672761 3221224544 3221223648 134554662 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.025 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2591 0 0 0 34982 18 0 0 25 0 1 0 540823278 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.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2591 0 0 0 35982 18 0 0 25 0 1 0 540823278 12509184 2568 4294967295 134512640 134672761 3221224544 3221223712 134560892 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.026 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2641 0 0 0 36982 19 0 0 25 0 1 0 540823278 12644352 2618 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3087 2618 603 41 0 3046 0
vsize: 12348
[startup+380.027 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2799 0 0 0 37981 20 0 0 25 0 1 0 540823278 13328384 2776 4294967295 134512640 134672761 3221224544 3221223712 134561001 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.027 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2801 0 0 0 38981 20 0 0 25 0 1 0 540823278 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.028 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2808 0 0 0 39981 21 0 0 25 0 1 0 540823278 13328384 2785 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3254 2785 603 41 0 3213 0
vsize: 13016
[startup+410.028 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2923 0 0 0 40980 22 0 0 25 0 1 0 540823278 13860864 2900 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3384 2900 603 41 0 3343 0
vsize: 13536
[startup+420.029 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2989 0 0 0 41979 22 0 0 25 0 1 0 540823278 14131200 2966 4294967295 134512640 134672761 3221224544 3221223648 134560194 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.029 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2989 0 0 0 42979 22 0 0 25 0 1 0 540823278 14131200 2966 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.029 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2989 0 0 0 43979 23 0 0 25 0 1 0 540823278 14131200 2966 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2966 603 41 0 3409 0
vsize: 13800
[startup+450.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 2992 0 0 0 44979 23 0 0 25 0 1 0 540823278 14131200 2969 4294967295 134512640 134672761 3221224544 3221223712 134561005 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.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3000 0 0 0 45979 23 0 0 25 0 1 0 540823278 14131200 2977 4294967295 134512640 134672761 3221224544 3221223712 134561205 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.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3000 0 0 0 46978 24 0 0 25 0 1 0 540823278 14131200 2977 4294967295 134512640 134672761 3221224544 3221223712 134560926 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.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3000 0 0 0 47978 24 0 0 25 0 1 0 540823278 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+490.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3000 0 0 0 48977 25 0 0 25 0 1 0 540823278 14131200 2977 4294967295 134512640 134672761 3221224544 3221223712 134564451 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.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3001 0 0 0 49977 25 0 0 25 0 1 0 540823278 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134560980 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.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3001 0 0 0 50977 25 0 0 25 0 1 0 540823278 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+520.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3001 0 0 0 51977 26 0 0 25 0 1 0 540823278 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+530.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3001 0 0 0 52977 26 0 0 25 0 1 0 540823278 14131200 2978 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+540.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3001 0 0 0 53977 26 0 0 25 0 1 0 540823278 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+550.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3001 0 0 0 54977 26 0 0 25 0 1 0 540823278 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+560.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3001 0 0 0 55976 27 0 0 25 0 1 0 540823278 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+570.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3001 0 0 0 56976 27 0 0 25 0 1 0 540823278 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+580.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3001 0 0 0 57976 28 0 0 25 0 1 0 540823278 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+590.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3001 0 0 0 58975 28 0 0 25 0 1 0 540823278 14131200 2978 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3450 2978 603 41 0 3409 0
vsize: 13800
[startup+600.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3001 0 0 0 59975 28 0 0 25 0 1 0 540823278 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+610.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3001 0 0 0 60975 28 0 0 25 0 1 0 540823278 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+620.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3102 0 0 0 61975 29 0 0 25 0 1 0 540823278 14524416 3079 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3546 3079 603 41 0 3505 0
vsize: 14184
[startup+630.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3343 0 0 0 62974 30 0 0 25 0 1 0 540823278 15630336 3320 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3816 3320 603 41 0 3775 0
vsize: 15264
[startup+640.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3357 0 0 0 63974 30 0 0 25 0 1 0 540823278 15630336 3334 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3816 3334 603 41 0 3775 0
vsize: 15264
[startup+650.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3357 0 0 0 64973 31 0 0 25 0 1 0 540823278 15630336 3334 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3816 3334 603 41 0 3775 0
vsize: 15264
[startup+660.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3361 0 0 0 65973 31 0 0 25 0 1 0 540823278 15630336 3338 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3816 3338 603 41 0 3775 0
vsize: 15264
[startup+670.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3553 0 0 0 66972 32 0 0 25 0 1 0 540823278 16437248 3530 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4013 3530 603 41 0 3972 0
vsize: 16052
[startup+680.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3604 0 0 0 67972 32 0 0 25 0 1 0 540823278 16572416 3581 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+690.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3604 0 0 0 68972 32 0 0 25 0 1 0 540823278 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+700.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3604 0 0 0 69972 33 0 0 25 0 1 0 540823278 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+710.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3604 0 0 0 70972 33 0 0 25 0 1 0 540823278 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+720.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3604 0 0 0 71972 33 0 0 25 0 1 0 540823278 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+730.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3604 0 0 0 72972 33 0 0 25 0 1 0 540823278 16572416 3581 4294967295 134512640 134672761 3221224544 3221223648 134555078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+740.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3604 0 0 0 73972 34 0 0 25 0 1 0 540823278 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+750.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3604 0 0 0 74971 34 0 0 25 0 1 0 540823278 16572416 3581 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4046 3581 603 41 0 4005 0
vsize: 16184
[startup+760.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3616 0 0 0 75971 34 0 0 25 0 1 0 540823278 16732160 3593 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4085 3593 603 41 0 4044 0
vsize: 16340
[startup+770.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3819 0 0 0 76970 35 0 0 25 0 1 0 540823278 17539072 3796 4294967295 134512640 134672761 3221224544 3221223760 134558170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4282 3796 603 41 0 4241 0
vsize: 17128
[startup+780.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3898 0 0 0 77970 35 0 0 25 0 1 0 540823278 17809408 3875 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3875 603 41 0 4307 0
vsize: 17392
[startup+790.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3898 0 0 0 78970 35 0 0 25 0 1 0 540823278 17809408 3875 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3875 603 41 0 4307 0
vsize: 17392
[startup+800.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3898 0 0 0 79970 36 0 0 25 0 1 0 540823278 17809408 3875 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3875 603 41 0 4307 0
vsize: 17392
[startup+810.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3898 0 0 0 80970 36 0 0 25 0 1 0 540823278 17809408 3875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3875 603 41 0 4307 0
vsize: 17392
[startup+820.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3899 0 0 0 81970 36 0 0 25 0 1 0 540823278 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+830.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3899 0 0 0 82970 37 0 0 25 0 1 0 540823278 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+840.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3899 0 0 0 83970 37 0 0 25 0 1 0 540823278 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+850.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3899 0 0 0 84969 37 0 0 25 0 1 0 540823278 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+860.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3899 0 0 0 85969 38 0 0 25 0 1 0 540823278 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+870.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3899 0 0 0 86969 38 0 0 25 0 1 0 540823278 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+880.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3899 0 0 0 87969 38 0 0 25 0 1 0 540823278 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+890.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3899 0 0 0 88969 38 0 0 25 0 1 0 540823278 17809408 3876 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3876 603 41 0 4307 0
vsize: 17392
[startup+900.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3900 0 0 0 89968 39 0 0 25 0 1 0 540823278 17809408 3877 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3877 603 41 0 4307 0
vsize: 17392
[startup+910.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3901 0 0 0 90968 39 0 0 25 0 1 0 540823278 17809408 3878 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+920.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3901 0 0 0 91968 39 0 0 25 0 1 0 540823278 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+930.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3901 0 0 0 92967 40 0 0 25 0 1 0 540823278 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+940.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3901 0 0 0 93967 40 0 0 25 0 1 0 540823278 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+950.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3901 0 0 0 94967 40 0 0 25 0 1 0 540823278 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+960.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3901 0 0 0 95967 40 0 0 25 0 1 0 540823278 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+970.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3901 0 0 0 96967 41 0 0 25 0 1 0 540823278 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+980.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3901 0 0 0 97967 41 0 0 25 0 1 0 540823278 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+990.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3901 0 0 0 98967 42 0 0 25 0 1 0 540823278 17809408 3878 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3878 603 41 0 4307 0
vsize: 17392
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3903 0 0 0 99967 42 0 0 25 0 1 0 540823278 17809408 3880 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4348 3880 603 41 0 4307 0
vsize: 17392
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3914 0 0 0 100966 42 0 0 25 0 1 0 540823278 17973248 3891 4294967295 134512640 134672761 3221224544 3221223720 134558805 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3891 603 41 0 4347 0
vsize: 17552
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3915 0 0 0 101966 42 0 0 25 0 1 0 540823278 17973248 3892 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4388 3892 603 41 0 4347 0
vsize: 17552
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 102967 42 0 0 25 0 1 0 540823278 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+1040.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 103967 42 0 0 25 0 1 0 540823278 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+1050.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 104967 42 0 0 25 0 1 0 540823278 17973248 3893 4294967295 134512640 134672761 3221224544 3221223680 134565119 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.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 105967 42 0 0 25 0 1 0 540823278 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+1070.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 106967 42 0 0 25 0 1 0 540823278 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134561164 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.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 107967 42 0 0 25 0 1 0 540823278 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+1090.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 108968 42 0 0 25 0 1 0 540823278 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+1100.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 109968 42 0 0 25 0 1 0 540823278 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+1110.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 110968 43 0 0 25 0 1 0 540823278 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 111968 43 0 0 25 0 1 0 540823278 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134560876 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.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 112968 43 0 0 25 0 1 0 540823278 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+1140.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 113968 43 0 0 25 0 1 0 540823278 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+1150.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 114968 43 0 0 25 0 1 0 540823278 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+1160.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 115968 43 0 0 25 0 1 0 540823278 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134560956 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.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 116968 43 0 0 25 0 1 0 540823278 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+1180.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 117969 43 0 0 25 0 1 0 540823278 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+1190.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 118969 43 0 0 25 0 1 0 540823278 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.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 10125
Raw data (stat): 10125 (minisat+) R 10124 18865 18864 0 -1 0 3916 0 0 0 119969 43 0 0 25 0 1 0 540823278 17973248 3893 4294967295 134512640 134672761 3221224544 3221223712 134560940 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.08 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 10125
Raw data (stat): 10125 (minisat+) Z 10124 18865 18864 0 -1 12 3919 0 0 0 119969 44 0 0 25 0 1 0 540823278 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.08
CPU time (s): 1200.14
CPU user time (s): 1199.7
CPU system time (s): 0.444932
CPU usage (%): 100.005
Max. virtual memory (Kb): 17552
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####