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/MIPLIB/miplib2003/normalized-mps-v2-13-7-tr12-30.opb
MD5SUM	2d8f46b77d84c45a7178d4a463744176
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	7560
Biggest coefficient in the objective function	2097152
Number of bits for the biggest coefficient in the objective function	22
Sum of the numbers in the objective function	876993750
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	2097152
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	876993750
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.128979
Number of variables	14760
Total number of constraints	1110
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	360
Number of constraints which are nor clauses,nor cardinality constraints	750
Minimum length of a constraint	1
Maximum length of a constraint	252
Trace number 18387

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        790112 kB
Buffers:         15024 kB
Cached:         201620 kB
SwapCached:          4 kB
Active:         133532 kB
Inactive:        85960 kB
HighTotal:      131008 kB
HighFree:        14924 kB
LowTotal:       903652 kB
LowFree:        775188 kB
SwapTotal:     2097892 kB
SwapFree:      2097820 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6804 kB
Slab:            19332 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 15:04:50 (client local time) WITH STATUS 0 IN 1200.14 SECONDS
stats: 18106 7 1200.14 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1110 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1108]---> Adder-cost: 36   maxlim: 250751   bits: 19/18
c ---[1106]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[1104]---> Adder-cost: 80   maxlim: 1296894   bits: 22/21
c ---[1102]---> Adder-cost: 80   maxlim: 1299838   bits: 22/21
c ---[1100]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[1098]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[1096]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[1094]---> Adder-cost: 80   maxlim: 1296382   bits: 22/21
c ---[1092]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[1090]---> Adder-cost: 80   maxlim: 1300350   bits: 22/21
c ---[1088]---> Adder-cost: 80   maxlim: 1298814   bits: 22/21
c ---[1086]---> Adder-cost: 80   maxlim: 1300478   bits: 22/21
c ---[1084]---> Adder-cost: 80   maxlim: 1298174   bits: 22/21
c ---[1082]---> Adder-cost: 80   maxlim: 1300862   bits: 22/21
c ---[1080]---> Adder-cost: 80   maxlim: 1298942   bits: 22/21
c ---[1078]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[1076]---> Adder-cost: 80   maxlim: 1297022   bits: 22/21
c ---[1074]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[1072]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[1070]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[1068]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[1066]---> Adder-cost: 80   maxlim: 1301118   bits: 22/21
c ---[1064]---> Adder-cost: 80   maxlim: 1298942   bits: 22/21
c ---[1062]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[1060]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[1058]---> Adder-cost: 36   maxlim: 262143   bits: 19/18
c ---[1056]---> Adder-cost: 72   maxlim: 511742   bits: 20/19
c ---[1054]---> Adder-cost: 76   maxlim: 772990   bits: 21/20
c ---[1052]---> Adder-cost: 80   maxlim: 1300990   bits: 22/21
c ---[1050]---> Adder-cost: 80   maxlim: 1296894   bits: 22/21
c ---[1048]---> Adder-cost: 80   maxlim: 1296510   bits: 22/21
c ---[1046]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[1044]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[1042]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[1040]---> Adder-cost: 80   maxlim: 1296766   bits: 22/21
c ---[1038]---> Adder-cost: 80   maxlim: 1296510   bits: 22/21
c ---[1036]---> Adder-cost: 80   maxlim: 1297022   bits: 22/21
c ---[1034]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[1032]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[1030]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[1028]---> Adder-cost: 80   maxlim: 1295998   bits: 22/21
c ---[1026]---> Adder-cost: 80   maxlim: 1300222   bits: 22/21
c ---[1024]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[1022]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[1020]---> Adder-cost: 80   maxlim: 1300862   bits: 22/21
c ---[1018]---> Adder-cost: 80   maxlim: 1300094   bits: 22/21
c ---[1016]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[1014]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[1012]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[1010]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[1008]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[1006]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[1004]---> Adder-cost: 80   maxlim: 1296510   bits: 22/21
c ---[1002]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[1000]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 998]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 996]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[ 994]---> Adder-cost: 80   maxlim: 1294718   bits: 22/21
c ---[ 992]---> Adder-cost: 36   maxlim: 248831   bits: 19/18
c ---[ 990]---> Adder-cost: 72   maxlim: 509694   bits: 20/19
c ---[ 988]---> Adder-cost: 76   maxlim: 775550   bits: 21/20
c ---[ 986]---> Adder-cost: 80   maxlim: 1310718   bits: 22/21
c ---[ 984]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[ 982]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[ 980]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[ 978]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[ 976]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[ 974]---> Adder-cost: 80   maxlim: 1296766   bits: 22/21
c ---[ 972]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 970]---> Adder-cost: 80   maxlim: 1300990   bits: 22/21
c ---[ 968]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[ 966]---> Adder-cost: 80   maxlim: 1295614   bits: 22/21
c ---[ 964]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[ 962]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 960]---> Adder-cost: 80   maxlim: 1296510   bits: 22/21
c ---[ 958]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 956]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 954]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 952]---> Adder-cost: 80   maxlim: 1300990   bits: 22/21
c ---[ 950]---> Adder-cost: 80   maxlim: 1295358   bits: 22/21
c ---[ 948]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 946]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[ 944]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 942]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 940]---> Adder-cost: 80   maxlim: 1294718   bits: 22/21
c ---[ 938]---> Adder-cost: 80   maxlim: 1298942   bits: 22/21
c ---[ 936]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 934]---> Adder-cost: 80   maxlim: 1295614   bits: 22/21
c ---[ 932]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[ 930]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 928]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 926]---> Adder-cost: 36   maxlim: 248319   bits: 19/18
c ---[ 924]---> Adder-cost: 72   maxlim: 510974   bits: 20/19
c ---[ 922]---> Adder-cost: 76   maxlim: 770942   bits: 21/20
c ---[ 920]---> Adder-cost: 80   maxlim: 1310718   bits: 22/21
c ---[ 918]---> Adder-cost: 80   maxlim: 1296894   bits: 22/21
c ---[ 916]---> Adder-cost: 80   maxlim: 1297022   bits: 22/21
c ---[ 914]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[ 912]---> Adder-cost: 80   maxlim: 1298814   bits: 22/21
c ---[ 910]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 908]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 906]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 904]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 902]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 900]---> Adder-cost: 80   maxlim: 1297150   bits: 22/21
c ---[ 898]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 896]---> Adder-cost: 80   maxlim: 1295614   bits: 22/21
c ---[ 894]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[ 892]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 890]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 888]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[ 886]---> Adder-cost: 72   maxlim: 524286   bits: 20/19
c ---[ 884]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[ 882]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[ 880]---> Adder-cost: 80   maxlim: 1295614   bits: 22/21
c ---[ 878]---> Adder-cost: 80   maxlim: 1298686   bits: 22/21
c ---[ 876]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 874]---> Adder-cost: 80   maxlim: 1298558   bits: 22/21
c ---[ 872]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[ 870]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[ 868]---> Adder-cost: 80   maxlim: 1295102   bits: 22/21
c ---[ 866]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 864]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 862]---> Adder-cost: 80   maxlim: 1295998   bits: 22/21
c ---[ 860]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 858]---> Adder-cost: 36   maxlim: 247807   bits: 19/18
c ---[ 856]---> Adder-cost: 72   maxlim: 511998   bits: 20/19
c ---[ 854]---> Adder-cost: 76   maxlim: 772478   bits: 21/20
c ---[ 852]---> Adder-cost: 80   maxlim: 1310718   bits: 22/21
c ---[ 850]---> Adder-cost: 80   maxlim: 1300990   bits: 22/21
c ---[ 848]---> Adder-cost: 80   maxlim: 1301118   bits: 22/21
c ---[ 846]---> Adder-cost: 80   maxlim: 1297150   bits: 22/21
c ---[ 844]---> Adder-cost: 80   maxlim: 1300222   bits: 22/21
c ---[ 842]---> Adder-cost: 80   maxlim: 1298174   bits: 22/21
c ---[ 840]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 838]---> Adder-cost: 80   maxlim: 1296766   bits: 22/21
c ---[ 836]---> Adder-cost: 80   maxlim: 1298174   bits: 22/21
c ---[ 834]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[ 832]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 830]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 828]---> Adder-cost: 80   maxlim: 1296894   bits: 22/21
c ---[ 826]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 824]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 822]---> Adder-cost: 80   maxlim: 1294718   bits: 22/21
c ---[ 820]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[ 818]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[ 816]---> Adder-cost: 80   maxlim: 1300350   bits: 22/21
c ---[ 814]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[ 812]---> Adder-cost: 80   maxlim: 1295998   bits: 22/21
c ---[ 810]---> Adder-cost: 80   maxlim: 1296510   bits: 22/21
c ---[ 808]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[ 806]---> Adder-cost: 80   maxlim: 1297022   bits: 22/21
c ---[ 804]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 802]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[ 800]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 798]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 796]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[ 794]---> Adder-cost: 80   maxlim: 1298686   bits: 22/21
c ---[ 792]---> Adder-cost: 36   maxlim: 249215   bits: 19/18
c ---[ 790]---> Adder-cost: 72   maxlim: 524286   bits: 20/19
c ---[ 788]---> Adder-cost: 76   maxlim: 771838   bits: 21/20
c ---[ 786]---> Adder-cost: 80   maxlim: 1298942   bits: 22/21
c ---[ 784]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 782]---> Adder-cost: 80   maxlim: 1298814   bits: 22/21
c ---[ 780]---> Adder-cost: 80   maxlim: 1300478   bits: 22/21
c ---[ 778]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[ 776]---> Adder-cost: 80   maxlim: 1296382   bits: 22/21
c ---[ 774]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 772]---> Adder-cost: 80   maxlim: 1298814   bits: 22/21
c ---[ 770]---> Adder-cost: 80   maxlim: 1295998   bits: 22/21
c ---[ 768]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[ 766]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[ 764]---> Adder-cost: 80   maxlim: 1297918   bits: 22/21
c ---[ 762]---> Adder-cost: 80   maxlim: 1300222   bits: 22/21
c ---[ 760]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 758]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[ 756]---> Adder-cost: 80   maxlim: 1300094   bits: 22/21
c ---[ 754]---> Adder-cost: 80   maxlim: 1296766   bits: 22/21
c ---[ 752]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[ 750]---> Adder-cost: 80   maxlim: 1296254   bits: 22/21
c ---[ 748]---> Adder-cost: 80   maxlim: 1295102   bits: 22/21
c ---[ 746]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[ 744]---> Adder-cost: 80   maxlim: 1296382   bits: 22/21
c ---[ 742]---> Adder-cost: 80   maxlim: 1295614   bits: 22/21
c ---[ 740]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 738]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[ 736]---> Adder-cost: 80   maxlim: 1301118   bits: 22/21
c ---[ 734]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[ 732]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 730]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[ 728]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[ 726]---> Adder-cost: 36   maxlim: 262143   bits: 19/18
c ---[ 724]---> Adder-cost: 72   maxlim: 510974   bits: 20/19
c ---[ 722]---> Adder-cost: 76   maxlim: 786430   bits: 21/20
c ---[ 720]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 718]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 716]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 714]---> Adder-cost: 80   maxlim: 1300990   bits: 22/21
c ---[ 712]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 710]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 708]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[ 706]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 704]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[ 702]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 700]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 698]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 696]---> Adder-cost: 80   maxlim: 1295102   bits: 22/21
c ---[ 694]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[ 692]---> Adder-cost: 80   maxlim: 1298558   bits: 22/21
c ---[ 690]---> Adder-cost: 80   maxlim: 1300862   bits: 22/21
c ---[ 688]---> Adder-cost: 80   maxlim: 1296382   bits: 22/21
c ---[ 686]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 684]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[ 682]---> Adder-cost: 80   maxlim: 1300094   bits: 22/21
c ---[ 680]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[ 678]---> Adder-cost: 80   maxlim: 1294718   bits: 22/21
c ---[ 676]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 674]---> Adder-cost: 80   maxlim: 1298558   bits: 22/21
c ---[ 672]---> Adder-cost: 80   maxlim: 1296382   bits: 22/21
c ---[ 670]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[ 668]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 666]---> Adder-cost: 80   maxlim: 1300222   bits: 22/21
c ---[ 664]---> Adder-cost: 76   maxlim: 774654   bits: 21/20
c ---[ 662]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 660]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 658]---> Adder-cost: 36   maxlim: 249215   bits: 19/18
c ---[ 656]---> Adder-cost: 72   maxlim: 511486   bits: 20/19
c ---[ 654]---> Adder-cost: 76   maxlim: 775934   bits: 21/20
c ---[ 652]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[ 650]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 648]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 646]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 644]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 642]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 640]---> Adder-cost: 36   maxlim: 250367   bits: 19/18
c ---[ 638]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[ 636]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 634]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[ 632]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[ 630]---> Adder-cost: 80   maxlim: 1298174   bits: 22/21
c ---[ 628]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 626]---> Adder-cost: 80   maxlim: 1300222   bits: 22/21
c ---[ 624]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 622]---> Adder-cost: 80   maxlim: 1295998   bits: 22/21
c ---[ 620]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 618]---> Adder-cost: 72   maxlim: 510206   bits: 20/19
c ---[ 616]---> Adder-cost: 80   maxlim: 1298558   bits: 22/21
c ---[ 614]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[ 612]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 610]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 608]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 606]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[ 604]---> Adder-cost: 80   maxlim: 1300478   bits: 22/21
c ---[ 602]---> Adder-cost: 80   maxlim: 1299838   bits: 22/21
c ---[ 600]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[ 598]---> Adder-cost: 80   maxlim: 1300094   bits: 22/21
c ---[ 596]---> Adder-cost: 76   maxlim: 771582   bits: 21/20
c ---[ 594]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 592]---> Adder-cost: 36   maxlim: 262143   bits: 19/18
c ---[ 590]---> Adder-cost: 72   maxlim: 509566   bits: 20/19
c ---[ 588]---> Adder-cost: 76   maxlim: 776446   bits: 21/20
c ---[ 586]---> Adder-cost: 80   maxlim: 1310718   bits: 22/21
c ---[ 584]---> Adder-cost: 80   maxlim: 1296894   bits: 22/21
c ---[ 582]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 580]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[ 578]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[ 576]---> Adder-cost: 80   maxlim: 1297022   bits: 22/21
c ---[ 574]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[ 572]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[ 570]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[ 568]---> Adder-cost: 80   maxlim: 1294718   bits: 22/21
c ---[ 566]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 564]---> Adder-cost: 80   maxlim: 1295358   bits: 22/21
c ---[ 562]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 560]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[ 558]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 556]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 554]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[ 552]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 550]---> Adder-cost: 80   maxlim: 1298558   bits: 22/21
c ---[ 548]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 546]---> Adder-cost: 80   maxlim: 1295358   bits: 22/21
c ---[ 544]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[ 542]---> Adder-cost: 80   maxlim: 1297918   bits: 22/21
c ---[ 540]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 538]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[ 536]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[ 534]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 532]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[ 530]---> Adder-cost: 80   maxlim: 1299838   bits: 22/21
c ---[ 528]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 527]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 526]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 525]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 524]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 523]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 522]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 521]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 520]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 519]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 517]---> Adder-cost: 80   maxlim: 1297150   bits: 22/21
c ---[ 516]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 515]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 514]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 513]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 512]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 511]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 510]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 509]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 508]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 507]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 505]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[ 504]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 503]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 502]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 501]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 500]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 499]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 498]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 497]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 496]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 495]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 493]---> Adder-cost: 80   maxlim: 1298942   bits: 22/21
c ---[ 492]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 491]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 490]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 489]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 488]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 487]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 486]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 485]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 484]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 483]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 481]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[ 479]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 478]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 477]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 476]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 475]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 474]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 473]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 472]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 471]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 470]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 469]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 467]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[ 466]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 465]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 464]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 463]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 462]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 461]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 460]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 459]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 458]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 457]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 455]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 454]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 453]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 452]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 451]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 450]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 449]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 448]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 447]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 446]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 445]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 443]---> Adder-cost: 80   maxlim: 1300478   bits: 22/21
c ---[ 442]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 441]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 440]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 439]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 438]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 437]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 436]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 435]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 434]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 433]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 431]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 430]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 429]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 428]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 427]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 426]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 425]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 424]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 423]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 422]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 421]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 419]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[ 418]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 417]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 416]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 415]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 414]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 413]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 412]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 411]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 410]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 409]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 407]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[ 406]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 405]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 404]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 403]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 402]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 401]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 400]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 399]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 398]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 397]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 395]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 394]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 393]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 392]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 391]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 390]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 389]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 388]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 387]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 386]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 385]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 383]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 382]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 381]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 380]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 379]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 378]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 377]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 376]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 375]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 374]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 373]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 371]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 370]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 369]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 368]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 367]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 366]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 365]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 364]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 363]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 362]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 361]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 359]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[ 357]---> Adder-cost: 80   maxlim: 1298814   bits: 22/21
c ---[ 356]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 355]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 354]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 353]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 352]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 351]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 350]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 349]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 348]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 347]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 345]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[ 344]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 343]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 342]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 341]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 340]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 339]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 338]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 337]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 336]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 335]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 333]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[ 332]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 331]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 330]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 329]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 328]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 327]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 326]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 325]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 324]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 323]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 321]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[ 320]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 319]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 318]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 317]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 316]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 315]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 314]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 313]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 312]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 311]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 309]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 308]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 307]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 306]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 305]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 304]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 303]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 302]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 301]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 300]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 299]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 297]---> Adder-cost: 80   maxlim: 1298174   bits: 22/21
c ---[ 296]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 295]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 294]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 293]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 292]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 291]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 290]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 289]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 288]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 287]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 285]---> Adder-cost: 80   maxlim: 1300990   bits: 22/21
c ---[ 284]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 283]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 282]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 281]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 280]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 279]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 278]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 277]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 276]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 275]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 273]---> Adder-cost: 80   maxlim: 1299838   bits: 22/21
c ---[ 272]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 271]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 270]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 269]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 268]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 267]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 266]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 265]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 264]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 263]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 261]---> Adder-cost: 80   maxlim: 1296510   bits: 22/21
c ---[ 260]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 259]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 258]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 257]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 256]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 255]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 254]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 253]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 252]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 251]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 249]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 248]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 247]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 246]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 245]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 244]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 243]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 242]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 241]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 240]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 239]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 237]---> Adder-cost: 80   maxlim: 1296766   bits: 22/21
c ---[ 235]---> Adder-cost: 80   maxlim: 1295102   bits: 22/21
c ---[ 234]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 233]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 232]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 231]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 230]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 229]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 228]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 227]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 226]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 225]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 223]---> Adder-cost: 36   maxlim: 262143   bits: 19/18
c ---[ 222]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 221]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 220]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 219]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 218]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 217]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 216]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 215]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 214]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 213]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 211]---> Adder-cost: 72   maxlim: 509822   bits: 20/19
c ---[ 210]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 209]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 208]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 207]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 206]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 205]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 204]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 203]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 202]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 201]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 199]---> Adder-cost: 76   maxlim: 771198   bits: 21/20
c ---[ 198]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 197]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 196]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 195]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 194]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 193]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 192]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 191]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 190]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 189]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 187]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 186]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 185]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 184]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 183]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 182]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 181]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 180]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 179]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 178]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 177]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 175]---> Adder-cost: 80   maxlim: 1298942   bits: 22/21
c ---[ 174]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 173]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 172]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 171]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 170]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 169]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 168]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 167]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 166]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 165]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 163]---> Adder-cost: 80   maxlim: 1300478   bits: 22/21
c ---[ 162]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 161]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 160]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 159]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 158]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 157]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 156]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 155]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 154]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 153]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 151]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[ 150]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 149]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 148]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 147]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 146]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 145]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 144]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 143]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 142]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 141]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 139]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[ 138]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 137]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 136]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 135]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 134]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 133]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 132]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 131]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 130]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 129]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 127]---> Adder-cost: 80   maxlim: 1300862   bits: 22/21
c ---[ 126]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 125]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 124]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 123]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 122]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 121]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 120]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 119]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 118]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 117]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 115]---> Adder-cost: 80   maxlim: 1296766   bits: 22/21
c ---[ 113]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[ 112]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 111]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 110]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 109]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 108]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 107]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 106]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 105]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 104]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 103]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 101]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 100]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  99]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  98]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  97]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  96]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  95]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  94]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  93]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  92]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  91]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  89]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[  88]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  87]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  86]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  85]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  84]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  83]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  82]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  81]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  80]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  79]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  77]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[  76]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  75]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  74]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  73]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  72]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  71]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  70]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  69]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  68]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  67]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  65]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[  64]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  63]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  62]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  61]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  60]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  59]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  58]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  57]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  56]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  55]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  53]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[  52]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[  50]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[  48]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[  46]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[  44]---> Adder-cost: 80   maxlim: 1300094   bits: 22/21
c ---[  42]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[  40]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[  38]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[  36]---> Adder-cost: 80   maxlim: 1300862   bits: 22/21
c ---[  34]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[  32]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[  30]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[  28]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[  26]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[  24]---> Adder-cost: 80   maxlim: 1296382   bits: 22/21
c ---[  22]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[  20]---> Adder-cost: 80   maxlim: 1300478   bits: 22/21
c ---[  18]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[  16]---> Adder-cost: 36   maxlim: 250495   bits: 19/18
c ---[  14]---> Adder-cost: 72   maxlim: 513278   bits: 20/19
c ---[  12]---> Adder-cost: 76   maxlim: 786430   bits: 21/20
c ---[  10]---> Adder-cost: 80   maxlim: 1295102   bits: 22/21
c ---[   8]---> Adder-cost: 80   maxlim: 1298174   bits: 22/21
c ---[   6]---> Adder-cost: 80   maxlim: 1296254   bits: 22/21
c ---[   4]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[   2]---> Adder-cost: 80   maxlim: 1295614   bits: 22/21
c ---[   0]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  293478  1078218 |   97826       0        0     nan |  0.000 % |
c |       100 |  293369  1077829 |  107608      94      283     3.0 | 29.778 % |
c |       250 |  293369  1077829 |  118369     244      694     2.8 | 29.778 % |
c |       475 |  293317  1077644 |  130206     466     1456     3.1 | 29.780 % |
c |       812 |  293221  1077311 |  143227     792     2541     3.2 | 29.789 % |
c |      1318 |  293200  1077242 |  157549    1293     4262     3.3 | 29.793 % |
c |      2077 |  293143  1077054 |  173304    2040     7958     3.9 | 29.803 % |
c |      3216 |  293085  1076862 |  190635    3165    15202     4.8 | 29.814 % |
c |      4925 |  292880  1076198 |  209698    4825    24345     5.0 | 29.854 % |
c |      7487 |  292330  1074398 |  230668    7262    38820     5.3 | 29.951 % |
c |     11331 |  291726  1072397 |  253735   10959    67666     6.2 | 30.059 % |
c |     17097 |  291219  1070746 |  279108   16594   108452     6.5 | 30.153 % |
c |     25746 |  290267  1067619 |  307019   25036   179099     7.2 | 30.329 % |
c |     38720 |  288971  1063357 |  337721   37653   303843     8.1 | 30.567 % |
c |     58181 |  288449  1061636 |  371494   56975   807994    14.2 | 30.666 % |
c |     87373 |  288397  1061462 |  408643   86155  1816486    21.1 | 30.676 % |
c |    131162 |  288346  1061293 |  449507  129927  3190341    24.6 | 30.685 % |
c |    196849 |  288276  1061063 |  494458  195596  5253582    26.9 | 30.698 % |
c |    295376 |  288150  1060651 |  543904  294084  8086721    27.5 | 30.725 % |
#### 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.81 0.91 0.91 1/54 21508
Raw data (stat): 21508 (runsolver) D 21507 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 545896411 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.84 0.92 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 9417 0 0 0 962 23 0 0 25 0 1 0 545896411 42708992 8669 4294967295 134512640 134672761 3221224544 3221223712 134564726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10427 8669 603 41 0 10386 0
vsize: 41708
[startup+20.0022 s]
Raw data (loadavg): 0.87 0.92 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 9512 0 0 0 1961 24 0 0 25 0 1 0 545896411 43114496 8764 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10526 8764 603 41 0 10485 0
vsize: 42104
[startup+30.003 s]
Raw data (loadavg): 0.89 0.92 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 9607 0 0 0 2961 25 0 0 25 0 1 0 545896411 43409408 8859 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10598 8859 603 41 0 10557 0
vsize: 42392
[startup+40.0038 s]
Raw data (loadavg): 0.90 0.92 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 9748 0 0 0 3960 25 0 0 25 0 1 0 545896411 44101632 9000 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10767 9000 603 41 0 10726 0
vsize: 43068
[startup+50.0044 s]
Raw data (loadavg): 0.92 0.92 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 9829 0 0 0 4960 25 0 0 25 0 1 0 545896411 44367872 9081 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10832 9081 603 41 0 10791 0
vsize: 43328
[startup+60.0051 s]
Raw data (loadavg): 0.93 0.93 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 9907 0 0 0 5960 26 0 0 25 0 1 0 545896411 44638208 9159 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10898 9159 603 41 0 10857 0
vsize: 43592
[startup+70.0059 s]
Raw data (loadavg): 0.94 0.93 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 10010 0 0 0 6959 26 0 0 25 0 1 0 545896411 45043712 9262 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10997 9262 603 41 0 10956 0
vsize: 43988
[startup+80.006 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 10108 0 0 0 7959 27 0 0 25 0 1 0 545896411 45576192 9360 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11127 9360 603 41 0 11086 0
vsize: 44508
[startup+90.0065 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 10218 0 0 0 8959 27 0 0 25 0 1 0 545896411 45977600 9470 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11225 9470 603 41 0 11184 0
vsize: 44900
[startup+100.006 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 10698 0 0 0 9958 28 0 0 25 0 1 0 545896411 47980544 9950 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11714 9950 603 41 0 11673 0
vsize: 46856
[startup+110.007 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 11237 0 0 0 10957 29 0 0 25 0 1 0 545896411 50380800 10489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12300 10489 603 41 0 12259 0
vsize: 49200
[startup+120.008 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 11640 0 0 0 11956 31 0 0 25 0 1 0 545896411 51994624 10892 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12694 10892 603 41 0 12653 0
vsize: 50776
[startup+130.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 12049 0 0 0 12955 32 0 0 25 0 1 0 545896411 53743616 11301 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13121 11301 603 41 0 13080 0
vsize: 52484
[startup+140.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 12357 0 0 0 13954 33 0 0 25 0 1 0 545896411 55009280 11609 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13430 11609 603 41 0 13389 0
vsize: 53720
[startup+150.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 12535 0 0 0 14953 33 0 0 25 0 1 0 545896411 55717888 11787 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13603 11787 603 41 0 13562 0
vsize: 54412
[startup+160.01 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 12833 0 0 0 15953 34 0 0 25 0 1 0 545896411 56938496 12085 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13901 12085 603 41 0 13860 0
vsize: 55604
[startup+170.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 13053 0 0 0 16952 35 0 0 25 0 1 0 545896411 57769984 12305 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14104 12305 603 41 0 14063 0
vsize: 56416
[startup+180.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 13291 0 0 0 17952 36 0 0 25 0 1 0 545896411 58851328 12543 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14368 12543 603 41 0 14327 0
vsize: 57472
[startup+190.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 13501 0 0 0 18951 36 0 0 25 0 1 0 545896411 59707392 12753 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14577 12753 603 41 0 14536 0
vsize: 58308
[startup+200.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 13668 0 0 0 19951 36 0 0 25 0 1 0 545896411 60387328 12920 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 12920 603 41 0 14702 0
vsize: 58972
[startup+210.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 13837 0 0 0 20951 37 0 0 25 0 1 0 545896411 61059072 13089 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14907 13089 603 41 0 14866 0
vsize: 59628
[startup+220.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 13995 0 0 0 21951 37 0 0 25 0 1 0 545896411 61640704 13247 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15049 13247 603 41 0 15008 0
vsize: 60196
[startup+230.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 14139 0 0 0 22950 37 0 0 25 0 1 0 545896411 62844928 13391 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15343 13391 603 41 0 15302 0
vsize: 61372
[startup+240.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 14263 0 0 0 23951 38 0 0 25 0 1 0 545896411 63406080 13515 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15480 13515 603 41 0 15439 0
vsize: 61920
[startup+250.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 14398 0 0 0 24950 38 0 0 25 0 1 0 545896411 63946752 13650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15612 13650 603 41 0 15571 0
vsize: 62448
[startup+260.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 14502 0 0 0 25950 38 0 0 25 0 1 0 545896411 64344064 13754 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15709 13754 603 41 0 15668 0
vsize: 62836
[startup+270.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 14618 0 0 0 26950 39 0 0 25 0 1 0 545896411 64782336 13870 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15816 13870 603 41 0 15775 0
vsize: 63264
[startup+280.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 14761 0 0 0 27950 39 0 0 25 0 1 0 545896411 65351680 14013 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15955 14013 603 41 0 15914 0
vsize: 63820
[startup+290.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 14910 0 0 0 28949 40 0 0 25 0 1 0 545896411 65982464 14162 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16109 14162 603 41 0 16068 0
vsize: 64436
[startup+300.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 15063 0 0 0 29949 40 0 0 25 0 1 0 545896411 66654208 14315 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16273 14315 603 41 0 16232 0
vsize: 65092
[startup+310.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 15204 0 0 0 30949 41 0 0 25 0 1 0 545896411 67186688 14456 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16403 14456 603 41 0 16362 0
vsize: 65612
[startup+320.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 15357 0 0 0 31949 41 0 0 25 0 1 0 545896411 67854336 14609 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16566 14609 603 41 0 16525 0
vsize: 66264
[startup+330.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 15474 0 0 0 32949 41 0 0 25 0 1 0 545896411 68407296 14726 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16701 14726 603 41 0 16660 0
vsize: 66804
[startup+340.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 15581 0 0 0 33949 42 0 0 25 0 1 0 545896411 68800512 14833 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16797 14833 603 41 0 16756 0
vsize: 67188
[startup+350.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 15691 0 0 0 34949 42 0 0 25 0 1 0 545896411 69222400 14943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16900 14943 603 41 0 16859 0
vsize: 67600
[startup+360.038 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 15808 0 0 0 35950 43 0 0 25 0 1 0 545896411 69718016 15060 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17021 15060 603 41 0 16980 0
vsize: 68084
[startup+370.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 15910 0 0 0 36950 44 0 0 25 0 1 0 545896411 70123520 15162 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17120 15162 603 41 0 17079 0
vsize: 68480
[startup+380.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 16021 0 0 0 37950 44 0 0 25 0 1 0 545896411 70656000 15273 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17250 15273 603 41 0 17209 0
vsize: 69000
[startup+390.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 16161 0 0 0 38950 44 0 0 25 0 1 0 545896411 71237632 15413 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17392 15413 603 41 0 17351 0
vsize: 69568
[startup+400.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 16240 0 0 0 39950 44 0 0 25 0 1 0 545896411 71585792 15492 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17477 15492 603 41 0 17436 0
vsize: 69908
[startup+410.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 16304 0 0 0 40950 45 0 0 25 0 1 0 545896411 71847936 15556 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 15556 603 41 0 17500 0
vsize: 70164
[startup+420.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 16398 0 0 0 41950 45 0 0 25 0 1 0 545896411 72355840 15650 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17665 15650 603 41 0 17624 0
vsize: 70660
[startup+430.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 16467 0 0 0 42950 45 0 0 25 0 1 0 545896411 72622080 15719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17730 15719 603 41 0 17689 0
vsize: 70920
[startup+440.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 16553 0 0 0 43950 46 0 0 25 0 1 0 545896411 72888320 15805 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17795 15805 603 41 0 17754 0
vsize: 71180
[startup+450.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 16735 0 0 0 44949 46 0 0 25 0 1 0 545896411 73560064 15987 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17959 15987 603 41 0 17918 0
vsize: 71836
[startup+460.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 16830 0 0 0 45950 47 0 0 25 0 1 0 545896411 74100736 16082 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18091 16082 603 41 0 18050 0
vsize: 72364
[startup+470.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 16973 0 0 0 46949 47 0 0 25 0 1 0 545896411 74719232 16225 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18242 16225 603 41 0 18201 0
vsize: 72968
[startup+480.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 17061 0 0 0 47949 47 0 0 25 0 1 0 545896411 74985472 16313 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18307 16313 603 41 0 18266 0
vsize: 73228
[startup+490.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 17219 0 0 0 48948 48 0 0 25 0 1 0 545896411 75788288 16471 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18503 16471 603 41 0 18462 0
vsize: 74012
[startup+500.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 17293 0 0 0 49949 48 0 0 25 0 1 0 545896411 76115968 16545 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18583 16545 603 41 0 18542 0
vsize: 74332
[startup+510.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 17400 0 0 0 50949 48 0 0 25 0 1 0 545896411 76660736 16652 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18716 16652 603 41 0 18675 0
vsize: 74864
[startup+520.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 17525 0 0 0 51948 49 0 0 25 0 1 0 545896411 77185024 16777 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18844 16777 603 41 0 18803 0
vsize: 75376
[startup+530.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 17595 0 0 0 52948 49 0 0 25 0 1 0 545896411 77451264 16847 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18909 16847 603 41 0 18868 0
vsize: 75636
[startup+540.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 17698 0 0 0 53948 49 0 0 25 0 1 0 545896411 77852672 16950 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19007 16950 603 41 0 18966 0
vsize: 76028
[startup+550.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 17817 0 0 0 54948 50 0 0 25 0 1 0 545896411 78258176 17069 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19106 17069 603 41 0 19065 0
vsize: 76424
[startup+560.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 17973 0 0 0 55948 50 0 0 25 0 1 0 545896411 78929920 17225 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19270 17225 603 41 0 19229 0
vsize: 77080
[startup+570.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18039 0 0 0 56948 50 0 0 25 0 1 0 545896411 79200256 17291 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19336 17291 603 41 0 19295 0
vsize: 77344
[startup+580.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18128 0 0 0 57948 50 0 0 25 0 1 0 545896411 79597568 17380 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19433 17380 603 41 0 19392 0
vsize: 77732
[startup+590.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18193 0 0 0 58948 50 0 0 25 0 1 0 545896411 79732736 17445 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19466 17445 603 41 0 19425 0
vsize: 77864
[startup+600.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18273 0 0 0 59948 51 0 0 25 0 1 0 545896411 80154624 17525 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19569 17525 603 41 0 19528 0
vsize: 78276
[startup+610.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18338 0 0 0 60947 51 0 0 25 0 1 0 545896411 80424960 17590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19635 17590 603 41 0 19594 0
vsize: 78540
[startup+620.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18394 0 0 0 61947 51 0 0 25 0 1 0 545896411 80560128 17646 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19668 17646 603 41 0 19627 0
vsize: 78672
[startup+630.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18470 0 0 0 62947 52 0 0 25 0 1 0 545896411 80830464 17722 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19734 17722 603 41 0 19693 0
vsize: 78936
[startup+640.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18549 0 0 0 63947 52 0 0 25 0 1 0 545896411 81231872 17801 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19832 17801 603 41 0 19791 0
vsize: 79328
[startup+650.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18630 0 0 0 64947 52 0 0 25 0 1 0 545896411 81637376 17882 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19931 17882 603 41 0 19890 0
vsize: 79724
[startup+660.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18739 0 0 0 65947 52 0 0 25 0 1 0 545896411 82055168 17991 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20033 17991 603 41 0 19992 0
vsize: 80132
[startup+670.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18800 0 0 0 66947 52 0 0 25 0 1 0 545896411 82317312 18052 4294967295 134512640 134672761 3221224544 3221223728 134558890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20097 18052 603 41 0 20056 0
vsize: 80388
[startup+680.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18859 0 0 0 67947 53 0 0 25 0 1 0 545896411 82583552 18111 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20162 18111 603 41 0 20121 0
vsize: 80648
[startup+690.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 18931 0 0 0 68947 53 0 0 25 0 1 0 545896411 82849792 18183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20227 18183 603 41 0 20186 0
vsize: 80908
[startup+700.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19018 0 0 0 69947 53 0 0 25 0 1 0 545896411 83247104 18270 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20324 18270 603 41 0 20283 0
vsize: 81296
[startup+710.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19117 0 0 0 70947 53 0 0 25 0 1 0 545896411 83644416 18369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20421 18369 603 41 0 20380 0
vsize: 81684
[startup+720.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19194 0 0 0 71947 54 0 0 25 0 1 0 545896411 83906560 18446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20485 18446 603 41 0 20444 0
vsize: 81940
[startup+730.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19280 0 0 0 72947 54 0 0 25 0 1 0 545896411 84172800 18532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20550 18532 603 41 0 20509 0
vsize: 82200
[startup+740.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19358 0 0 0 73947 54 0 0 25 0 1 0 545896411 84647936 18610 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20666 18610 603 41 0 20625 0
vsize: 82664
[startup+750.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19406 0 0 0 74947 54 0 0 25 0 1 0 545896411 84877312 18658 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20722 18658 603 41 0 20681 0
vsize: 82888
[startup+760.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19470 0 0 0 75947 54 0 0 25 0 1 0 545896411 86188032 18722 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21042 18722 603 41 0 21001 0
vsize: 84168
[startup+770.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19521 0 0 0 76947 55 0 0 25 0 1 0 545896411 86462464 18773 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21109 18773 603 41 0 21068 0
vsize: 84436
[startup+780.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19561 0 0 0 77947 55 0 0 25 0 1 0 545896411 86597632 18813 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21142 18813 603 41 0 21101 0
vsize: 84568
[startup+790.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19634 0 0 0 78947 55 0 0 25 0 1 0 545896411 86892544 18886 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21214 18886 603 41 0 21173 0
vsize: 84856
[startup+800.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19698 0 0 0 79947 56 0 0 25 0 1 0 545896411 87027712 18950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21247 18950 603 41 0 21206 0
vsize: 84988
[startup+810.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19785 0 0 0 80947 56 0 0 25 0 1 0 545896411 87560192 19037 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21377 19037 603 41 0 21336 0
vsize: 85508
[startup+820.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19866 0 0 0 81947 56 0 0 25 0 1 0 545896411 88084480 19118 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21505 19118 603 41 0 21464 0
vsize: 86020
[startup+830.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 19928 0 0 0 82947 56 0 0 25 0 1 0 545896411 88215552 19180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21537 19180 603 41 0 21496 0
vsize: 86148
[startup+840.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20051 0 0 0 83947 56 0 0 25 0 1 0 545896411 88875008 19303 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21698 19303 603 41 0 21657 0
vsize: 86792
[startup+850.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20085 0 0 0 84947 57 0 0 25 0 1 0 545896411 89010176 19337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21731 19337 603 41 0 21690 0
vsize: 86924
[startup+860.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20141 0 0 0 85947 57 0 0 25 0 1 0 545896411 89403392 19393 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21827 19393 603 41 0 21786 0
vsize: 87308
[startup+870.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20193 0 0 0 86947 57 0 0 25 0 1 0 545896411 89538560 19445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21860 19445 603 41 0 21819 0
vsize: 87440
[startup+880.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20266 0 0 0 87947 57 0 0 25 0 1 0 545896411 89808896 19518 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21926 19518 603 41 0 21885 0
vsize: 87704
[startup+890.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20328 0 0 0 88947 57 0 0 25 0 1 0 545896411 90136576 19580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22006 19580 603 41 0 21965 0
vsize: 88024
[startup+900.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20385 0 0 0 89947 57 0 0 25 0 1 0 545896411 90406912 19637 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22072 19637 603 41 0 22031 0
vsize: 88288
[startup+910.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21508
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20457 0 0 0 90946 58 0 0 25 0 1 0 545896411 90677248 19709 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22138 19709 603 41 0 22097 0
vsize: 88552
[startup+920.081 s]
Raw data (loadavg): 1.07 0.99 0.92 3/58 21558
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20525 0 0 0 91943 62 0 0 25 0 1 0 545896411 90812416 19777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22171 19777 603 41 0 22130 0
vsize: 88684
[startup+930.081 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 21561
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20587 0 0 0 92942 62 0 0 25 0 1 0 545896411 91103232 19839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22242 19839 603 41 0 22201 0
vsize: 88968
[startup+940.081 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 21561
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20655 0 0 0 93942 63 0 0 25 0 1 0 545896411 91496448 19907 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22338 19907 603 41 0 22297 0
vsize: 89352
[startup+950.081 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 21561
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20746 0 0 0 94942 63 0 0 25 0 1 0 545896411 91901952 19998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22437 19998 603 41 0 22396 0
vsize: 89748
[startup+960.082 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 21561
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20831 0 0 0 95941 63 0 0 25 0 1 0 545896411 92332032 20083 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22542 20083 603 41 0 22501 0
vsize: 90168
[startup+970.082 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 21561
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 20889 0 0 0 96941 64 0 0 25 0 1 0 545896411 92467200 20141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22575 20141 603 41 0 22534 0
vsize: 90300
[startup+980.082 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 21561
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 21002 0 0 0 97940 64 0 0 25 0 1 0 545896411 93007872 20254 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22707 20254 603 41 0 22666 0
vsize: 90828
[startup+990.082 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 21147 0 0 0 98940 64 0 0 25 0 1 0 545896411 93544448 20399 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22838 20399 603 41 0 22797 0
vsize: 91352
[startup+1000.08 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 21305 0 0 0 99940 65 0 0 25 0 1 0 545896411 94081024 20557 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22969 20557 603 41 0 22928 0
vsize: 91876
[startup+1010.08 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 21343 0 0 0 100940 65 0 0 25 0 1 0 545896411 94216192 20595 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23002 20595 603 41 0 22961 0
vsize: 92008
[startup+1020.08 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 21385 0 0 0 101940 65 0 0 25 0 1 0 545896411 94367744 20637 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23039 20637 603 41 0 22998 0
vsize: 92156
[startup+1030.08 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 21472 0 0 0 102940 65 0 0 25 0 1 0 545896411 94892032 20724 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23167 20724 603 41 0 23126 0
vsize: 92668
[startup+1040.08 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 21657 0 0 0 103939 66 0 0 25 0 1 0 545896411 95694848 20909 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23363 20909 603 41 0 23322 0
vsize: 93452
[startup+1050.08 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 21770 0 0 0 104939 66 0 0 25 0 1 0 545896411 96141312 21022 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23472 21022 603 41 0 23431 0
vsize: 93888
[startup+1060.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 21807 0 0 0 105939 67 0 0 25 0 1 0 545896411 96276480 21059 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23505 21059 603 41 0 23464 0
vsize: 94020
[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 21844 0 0 0 106939 67 0 0 25 0 1 0 545896411 96436224 21096 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23544 21096 603 41 0 23503 0
vsize: 94176
[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 21892 0 0 0 107939 67 0 0 25 0 1 0 545896411 96571392 21144 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23577 21144 603 41 0 23536 0
vsize: 94308
[startup+1090.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 21933 0 0 0 108939 67 0 0 25 0 1 0 545896411 96706560 21185 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23610 21185 603 41 0 23569 0
vsize: 94440
[startup+1100.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 22014 0 0 0 109939 68 0 0 25 0 1 0 545896411 97103872 21266 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23707 21266 603 41 0 23666 0
vsize: 94828
[startup+1110.08 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 22029 0 0 0 110939 68 0 0 25 0 1 0 545896411 97239040 21281 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23740 21281 603 41 0 23699 0
vsize: 94960
[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 22112 0 0 0 111939 68 0 0 25 0 1 0 545896411 97583104 21364 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23824 21364 603 41 0 23783 0
vsize: 95296
[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 22171 0 0 0 112938 69 0 0 25 0 1 0 545896411 97849344 21423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23889 21423 603 41 0 23848 0
vsize: 95556
[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 22262 0 0 0 113938 69 0 0 25 0 1 0 545896411 98250752 21514 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23987 21514 603 41 0 23946 0
vsize: 95948
[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 22351 0 0 0 114938 70 0 0 25 0 1 0 545896411 98512896 21603 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24051 21603 603 41 0 24010 0
vsize: 96204
[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 22446 0 0 0 115938 70 0 0 25 0 1 0 545896411 98914304 21698 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24149 21698 603 41 0 24108 0
vsize: 96596
[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 22496 0 0 0 116938 70 0 0 25 0 1 0 545896411 99049472 21748 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24182 21748 603 41 0 24141 0
vsize: 96728
[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 22539 0 0 0 117938 70 0 0 25 0 1 0 545896411 99315712 21791 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24247 21791 603 41 0 24206 0
vsize: 96988
[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 22593 0 0 0 118938 71 0 0 25 0 1 0 545896411 99446784 21845 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24279 21845 603 41 0 24238 0
vsize: 97116
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 21563
Raw data (stat): 21508 (minisat+) R 21507 11931 11930 0 -1 0 22651 0 0 0 119938 71 0 0 25 0 1 0 545896411 99700736 21903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24341 21903 603 41 0 24300 0
vsize: 97364
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 21563
Raw data (stat): 21508 (minisat+) Z 21507 11931 11930 0 -1 12 22653 0 0 0 119938 75 0 0 25 0 1 0 545896411 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.13
CPU time (s): 1200.14
CPU user time (s): 1199.38
CPU system time (s): 0.752885
CPU usage (%): 100.001
Max. virtual memory (Kb): 97364
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####