PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-tr12-30.opb
MD5SUM	9136d330eaa53552ba154b6915193b35
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.131979
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 14243

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-20 23:19:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20290 boxname=wulflinc23 idbench=1561 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9136d330eaa53552ba154b6915193b35  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-tr12-30.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-tr12-30.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-tr12-30.opb
IDLAUNCH: 20290
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        830452 kB
Buffers:          7860 kB
Cached:         165360 kB
SwapCached:        520 kB
Active:          51936 kB
Inactive:       123392 kB
HighTotal:      131008 kB
HighFree:        19432 kB
LowTotal:       903652 kB
LowFree:        811020 kB
SwapTotal:     2097136 kB
SwapFree:      2095824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5220 kB
Slab:            23284 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:39:44 (client local time) WITH STATUS 0 IN 1200.31 SECONDS
stats: 20290 7 1200.31 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1110 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1109]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1108]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1107]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1106]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1105]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1104]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1103]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1102]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1101]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1100]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1099]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1098]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1097]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1096]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1095]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1094]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1093]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1092]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1091]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1090]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1089]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1088]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1087]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1086]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1085]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1084]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1083]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1082]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1081]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1080]---> Adder-cost: 454   maxlim: 2997491   bits: 22/22
c ---[1078]---> Adder-cost: 36   maxlim: 250751   bits: 19/18
c ---[1076]---> Adder-cost: 72   maxlim: 524286   bits: 20/19
c ---[1074]---> Adder-cost: 76   maxlim: 774654   bits: 21/20
c ---[1072]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[1070]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[1068]---> Adder-cost: 80   maxlim: 1296766   bits: 22/21
c ---[1066]---> Adder-cost: 80   maxlim: 1296766   bits: 22/21
c ---[1064]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[1062]---> Adder-cost: 80   maxlim: 1300478   bits: 22/21
c ---[1060]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[1058]---> Adder-cost: 80   maxlim: 1298174   bits: 22/21
c ---[1056]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[1054]---> Adder-cost: 80   maxlim: 1296766   bits: 22/21
c ---[1052]---> Adder-cost: 80   maxlim: 1300094   bits: 22/21
c ---[1050]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[1048]---> Adder-cost: 80   maxlim: 1296766   bits: 22/21
c ---[1046]---> Adder-cost: 80   maxlim: 1300990   bits: 22/21
c ---[1044]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[1042]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[1040]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[1038]---> Adder-cost: 80   maxlim: 1295998   bits: 22/21
c ---[1036]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[1034]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[1032]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[1030]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[1028]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[1026]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[1024]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[1022]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[1020]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[1018]---> Adder-cost: 36   maxlim: 250367   bits: 19/18
c ---[1016]---> Adder-cost: 72   maxlim: 510206   bits: 20/19
c ---[1014]---> Adder-cost: 76   maxlim: 771582   bits: 21/20
c ---[1012]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[1010]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[1008]---> Adder-cost: 80   maxlim: 1299838   bits: 22/21
c ---[1006]---> Adder-cost: 80   maxlim: 1297150   bits: 22/21
c ---[1004]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[1002]---> Adder-cost: 80   maxlim: 1298942   bits: 22/21
c ---[1000]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 998]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[ 996]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 994]---> Adder-cost: 80   maxlim: 1300478   bits: 22/21
c ---[ 992]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 990]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[ 988]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[ 986]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 984]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 982]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 980]---> Adder-cost: 80   maxlim: 1298814   bits: 22/21
c ---[ 978]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[ 976]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[ 974]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[ 972]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 970]---> Adder-cost: 80   maxlim: 1298174   bits: 22/21
c ---[ 968]---> Adder-cost: 80   maxlim: 1300990   bits: 22/21
c ---[ 966]---> Adder-cost: 80   maxlim: 1299838   bits: 22/21
c ---[ 964]---> Adder-cost: 80   maxlim: 1296510   bits: 22/21
c ---[ 962]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 960]---> Adder-cost: 80   maxlim: 1295102   bits: 22/21
c ---[ 958]---> Adder-cost: 36   maxlim: 262143   bits: 19/18
c ---[ 956]---> Adder-cost: 72   maxlim: 509822   bits: 20/19
c ---[ 954]---> Adder-cost: 76   maxlim: 771198   bits: 21/20
c ---[ 952]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 950]---> Adder-cost: 80   maxlim: 1298942   bits: 22/21
c ---[ 948]---> Adder-cost: 80   maxlim: 1300478   bits: 22/21
c ---[ 946]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[ 944]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[ 942]---> Adder-cost: 80   maxlim: 1300862   bits: 22/21
c ---[ 940]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[ 938]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 936]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[ 934]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[ 932]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[ 930]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[ 928]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[ 926]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 924]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 922]---> Adder-cost: 80   maxlim: 1300094   bits: 22/21
c ---[ 920]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[ 918]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[ 916]---> Adder-cost: 80   maxlim: 1300862   bits: 22/21
c ---[ 914]---> Adder-cost: 80   maxlim: 1299454   bits: 22/21
c ---[ 912]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 910]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 908]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 906]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[ 904]---> Adder-cost: 80   maxlim: 1296382   bits: 22/21
c ---[ 902]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 900]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[ 898]---> Adder-cost: 36   maxlim: 250495   bits: 19/18
c ---[ 896]---> Adder-cost: 72   maxlim: 513278   bits: 20/19
c ---[ 894]---> Adder-cost: 76   maxlim: 786430   bits: 21/20
c ---[ 892]---> Adder-cost: 80   maxlim: 1295102   bits: 22/21
c ---[ 890]---> Adder-cost: 80   maxlim: 1298174   bits: 22/21
c ---[ 888]---> Adder-cost: 80   maxlim: 1296254   bits: 22/21
c ---[ 886]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[ 884]---> Adder-cost: 80   maxlim: 1295614   bits: 22/21
c ---[ 882]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[ 880]---> Adder-cost: 80   maxlim: 1296894   bits: 22/21
c ---[ 878]---> Adder-cost: 80   maxlim: 1299838   bits: 22/21
c ---[ 876]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 874]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 872]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 870]---> Adder-cost: 80   maxlim: 1296382   bits: 22/21
c ---[ 868]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[ 866]---> Adder-cost: 80   maxlim: 1300350   bits: 22/21
c ---[ 864]---> Adder-cost: 80   maxlim: 1298814   bits: 22/21
c ---[ 862]---> Adder-cost: 80   maxlim: 1300478   bits: 22/21
c ---[ 860]---> Adder-cost: 80   maxlim: 1300862   bits: 22/21
c ---[ 858]---> Adder-cost: 80   maxlim: 1298942   bits: 22/21
c ---[ 856]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[ 854]---> Adder-cost: 80   maxlim: 1297022   bits: 22/21
c ---[ 852]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 850]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[ 848]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 846]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[ 844]---> Adder-cost: 80   maxlim: 1301118   bits: 22/21
c ---[ 842]---> Adder-cost: 80   maxlim: 1298942   bits: 22/21
c ---[ 840]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 838]---> Adder-cost: 36   maxlim: 262143   bits: 19/18
c ---[ 836]---> Adder-cost: 72   maxlim: 511742   bits: 20/19
c ---[ 834]---> Adder-cost: 76   maxlim: 772990   bits: 21/20
c ---[ 832]---> Adder-cost: 80   maxlim: 1300990   bits: 22/21
c ---[ 830]---> Adder-cost: 80   maxlim: 1296894   bits: 22/21
c ---[ 828]---> Adder-cost: 80   maxlim: 1296510   bits: 22/21
c ---[ 826]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[ 824]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[ 822]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 820]---> Adder-cost: 80   maxlim: 1296510   bits: 22/21
c ---[ 818]---> Adder-cost: 80   maxlim: 1297022   bits: 22/21
c ---[ 816]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[ 814]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 812]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[ 810]---> Adder-cost: 80   maxlim: 1295998   bits: 22/21
c ---[ 808]---> Adder-cost: 80   maxlim: 1300222   bits: 22/21
c ---[ 806]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[ 804]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[ 802]---> Adder-cost: 80   maxlim: 1300862   bits: 22/21
c ---[ 800]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 798]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[ 796]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[ 794]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[ 792]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 790]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[ 788]---> Adder-cost: 80   maxlim: 1296510   bits: 22/21
c ---[ 786]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 784]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 782]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 780]---> Adder-cost: 80   maxlim: 1294718   bits: 22/21
c ---[ 778]---> Adder-cost: 36   maxlim: 248831   bits: 19/18
c ---[ 776]---> Adder-cost: 72   maxlim: 509694   bits: 20/19
c ---[ 774]---> Adder-cost: 76   maxlim: 775550   bits: 21/20
c ---[ 772]---> Adder-cost: 80   maxlim: 1310718   bits: 22/21
c ---[ 770]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[ 768]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[ 766]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[ 764]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[ 762]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[ 760]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 758]---> Adder-cost: 80   maxlim: 1300990   bits: 22/21
c ---[ 756]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[ 754]---> Adder-cost: 80   maxlim: 1295614   bits: 22/21
c ---[ 752]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[ 750]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 748]---> Adder-cost: 80   maxlim: 1296510   bits: 22/21
c ---[ 746]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 744]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 742]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 740]---> Adder-cost: 80   maxlim: 1295358   bits: 22/21
c ---[ 738]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 736]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[ 734]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 732]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 730]---> Adder-cost: 80   maxlim: 1294718   bits: 22/21
c ---[ 728]---> Adder-cost: 80   maxlim: 1298942   bits: 22/21
c ---[ 726]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 724]---> Adder-cost: 80   maxlim: 1295614   bits: 22/21
c ---[ 722]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[ 720]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 718]---> Adder-cost: 36   maxlim: 248319   bits: 19/18
c ---[ 716]---> Adder-cost: 72   maxlim: 510974   bits: 20/19
c ---[ 714]---> Adder-cost: 76   maxlim: 770942   bits: 21/20
c ---[ 712]---> Adder-cost: 80   maxlim: 1310718   bits: 22/21
c ---[ 710]---> Adder-cost: 80   maxlim: 1296894   bits: 22/21
c ---[ 708]---> Adder-cost: 80   maxlim: 1297022   bits: 22/21
c ---[ 706]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[ 704]---> Adder-cost: 80   maxlim: 1298814   bits: 22/21
c ---[ 702]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 700]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 698]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 696]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 694]---> Adder-cost: 80   maxlim: 1297150   bits: 22/21
c ---[ 692]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 690]---> Adder-cost: 80   maxlim: 1295614   bits: 22/21
c ---[ 688]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[ 686]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 684]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 682]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[ 680]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[ 678]---> Adder-cost: 80   maxlim: 1295614   bits: 22/21
c ---[ 676]---> Adder-cost: 80   maxlim: 1298686   bits: 22/21
c ---[ 674]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 672]---> Adder-cost: 80   maxlim: 1298558   bits: 22/21
c ---[ 670]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[ 668]---> Adder-cost: 80   maxlim: 1297790   bits: 22/21
c ---[ 666]---> Adder-cost: 80   maxlim: 1295102   bits: 22/21
c ---[ 664]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 662]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 660]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 658]---> Adder-cost: 36   maxlim: 247807   bits: 19/18
c ---[ 656]---> Adder-cost: 72   maxlim: 511998   bits: 20/19
c ---[ 654]---> Adder-cost: 76   maxlim: 772478   bits: 21/20
c ---[ 652]---> Adder-cost: 80   maxlim: 1310718   bits: 22/21
c ---[ 650]---> Adder-cost: 80   maxlim: 1300990   bits: 22/21
c ---[ 648]---> Adder-cost: 80   maxlim: 1301118   bits: 22/21
c ---[ 646]---> Adder-cost: 80   maxlim: 1297150   bits: 22/21
c ---[ 644]---> Adder-cost: 80   maxlim: 1300222   bits: 22/21
c ---[ 642]---> Adder-cost: 80   maxlim: 1298174   bits: 22/21
c ---[ 640]---> Adder-cost: 80   maxlim: 1296766   bits: 22/21
c ---[ 638]---> Adder-cost: 80   maxlim: 1298174   bits: 22/21
c ---[ 636]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[ 634]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 632]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 630]---> Adder-cost: 80   maxlim: 1296894   bits: 22/21
c ---[ 628]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 626]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 624]---> Adder-cost: 80   maxlim: 1294718   bits: 22/21
c ---[ 622]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[ 620]---> Adder-cost: 80   maxlim: 1300350   bits: 22/21
c ---[ 618]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[ 616]---> Adder-cost: 80   maxlim: 1295998   bits: 22/21
c ---[ 614]---> Adder-cost: 80   maxlim: 1296510   bits: 22/21
c ---[ 612]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[ 610]---> Adder-cost: 80   maxlim: 1297022   bits: 22/21
c ---[ 608]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 606]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[ 604]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 602]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 600]---> Adder-cost: 80   maxlim: 1298686   bits: 22/21
c ---[ 598]---> Adder-cost: 36   maxlim: 249215   bits: 19/18
c ---[ 596]---> Adder-cost: 72   maxlim: 524286   bits: 20/19
c ---[ 594]---> Adder-cost: 76   maxlim: 771838   bits: 21/20
c ---[ 592]---> Adder-cost: 80   maxlim: 1298942   bits: 22/21
c ---[ 590]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 588]---> Adder-cost: 80   maxlim: 1298814   bits: 22/21
c ---[ 586]---> Adder-cost: 80   maxlim: 1300478   bits: 22/21
c ---[ 584]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[ 582]---> Adder-cost: 80   maxlim: 1296382   bits: 22/21
c ---[ 580]---> Adder-cost: 80   maxlim: 1298814   bits: 22/21
c ---[ 578]---> Adder-cost: 80   maxlim: 1295998   bits: 22/21
c ---[ 576]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[ 574]---> Adder-cost: 80   maxlim: 1299326   bits: 22/21
c ---[ 572]---> Adder-cost: 80   maxlim: 1297918   bits: 22/21
c ---[ 570]---> Adder-cost: 80   maxlim: 1300222   bits: 22/21
c ---[ 568]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 566]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[ 564]---> Adder-cost: 80   maxlim: 1300094   bits: 22/21
c ---[ 562]---> Adder-cost: 80   maxlim: 1296766   bits: 22/21
c ---[ 560]---> Adder-cost: 80   maxlim: 1296254   bits: 22/21
c ---[ 558]---> Adder-cost: 80   maxlim: 1295102   bits: 22/21
c ---[ 556]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[ 554]---> Adder-cost: 80   maxlim: 1296382   bits: 22/21
c ---[ 552]---> Adder-cost: 80   maxlim: 1295614   bits: 22/21
c ---[ 550]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 548]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[ 546]---> Adder-cost: 80   maxlim: 1301118   bits: 22/21
c ---[ 544]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[ 542]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 540]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[ 538]---> Adder-cost: 36   maxlim: 262143   bits: 19/18
c ---[ 536]---> Adder-cost: 72   maxlim: 510974   bits: 20/19
c ---[ 534]---> Adder-cost: 76   maxlim: 786430   bits: 21/20
c ---[ 532]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 530]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 528]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 526]---> Adder-cost: 80   maxlim: 1300990   bits: 22/21
c ---[ 524]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 522]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 520]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 518]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[ 516]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 514]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 512]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 510]---> Adder-cost: 80   maxlim: 1295102   bits: 22/21
c ---[ 508]---> Adder-cost: 80   maxlim: 1294974   bits: 22/21
c ---[ 506]---> Adder-cost: 80   maxlim: 1298558   bits: 22/21
c ---[ 504]---> Adder-cost: 80   maxlim: 1300862   bits: 22/21
c ---[ 502]---> Adder-cost: 80   maxlim: 1296382   bits: 22/21
c ---[ 500]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[ 498]---> Adder-cost: 80   maxlim: 1300094   bits: 22/21
c ---[ 496]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[ 494]---> Adder-cost: 80   maxlim: 1294718   bits: 22/21
c ---[ 492]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 490]---> Adder-cost: 80   maxlim: 1298558   bits: 22/21
c ---[ 488]---> Adder-cost: 80   maxlim: 1296382   bits: 22/21
c ---[ 486]---> Adder-cost: 80   maxlim: 1296638   bits: 22/21
c ---[ 484]---> Adder-cost: 80   maxlim: 1294846   bits: 22/21
c ---[ 482]---> Adder-cost: 80   maxlim: 1300222   bits: 22/21
c ---[ 480]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 478]---> Adder-cost: 36   maxlim: 249215   bits: 19/18
c ---[ 476]---> Adder-cost: 72   maxlim: 511486   bits: 20/19
c ---[ 474]---> Adder-cost: 76   maxlim: 775934   bits: 21/20
c ---[ 472]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[ 470]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 468]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 466]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 464]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 462]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 460]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[ 458]---> Adder-cost: 80   maxlim: 1299198   bits: 22/21
c ---[ 456]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[ 454]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[ 452]---> Adder-cost: 80   maxlim: 1298174   bits: 22/21
c ---[ 450]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 448]---> Adder-cost: 80   maxlim: 1300222   bits: 22/21
c ---[ 446]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 444]---> Adder-cost: 80   maxlim: 1295998   bits: 22/21
c ---[ 442]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 440]---> Adder-cost: 80   maxlim: 1298558   bits: 22/21
c ---[ 438]---> Adder-cost: 80   maxlim: 1297662   bits: 22/21
c ---[ 436]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 434]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 432]---> Adder-cost: 80   maxlim: 1299070   bits: 22/21
c ---[ 430]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[ 428]---> Adder-cost: 80   maxlim: 1300478   bits: 22/21
c ---[ 426]---> Adder-cost: 80   maxlim: 1299838   bits: 22/21
c ---[ 424]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[ 422]---> Adder-cost: 80   maxlim: 1300094   bits: 22/21
c ---[ 420]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 418]---> Adder-cost: 36   maxlim: 262143   bits: 19/18
c ---[ 416]---> Adder-cost: 72   maxlim: 509566   bits: 20/19
c ---[ 414]---> Adder-cost: 76   maxlim: 776446   bits: 21/20
c ---[ 412]---> Adder-cost: 80   maxlim: 1310718   bits: 22/21
c ---[ 410]---> Adder-cost: 80   maxlim: 1296894   bits: 22/21
c ---[ 408]---> Adder-cost: 80   maxlim: 1300734   bits: 22/21
c ---[ 406]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[ 404]---> Adder-cost: 80   maxlim: 1295870   bits: 22/21
c ---[ 402]---> Adder-cost: 80   maxlim: 1297022   bits: 22/21
c ---[ 400]---> Adder-cost: 80   maxlim: 1297406   bits: 22/21
c ---[ 398]---> Adder-cost: 80   maxlim: 1297534   bits: 22/21
c ---[ 396]---> Adder-cost: 80   maxlim: 1294718   bits: 22/21
c ---[ 394]---> Adder-cost: 80   maxlim: 1299582   bits: 22/21
c ---[ 392]---> Adder-cost: 80   maxlim: 1295358   bits: 22/21
c ---[ 390]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 388]---> Adder-cost: 80   maxlim: 1299710   bits: 22/21
c ---[ 386]---> Adder-cost: 80   maxlim: 1295742   bits: 22/21
c ---[ 384]---> Adder-cost: 80   maxlim: 1298430   bits: 22/21
c ---[ 382]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[ 380]---> Adder-cost: 80   maxlim: 1298558   bits: 22/21
c ---[ 378]---> Adder-cost: 80   maxlim: 1295486   bits: 22/21
c ---[ 376]---> Adder-cost: 80   maxlim: 1295358   bits: 22/21
c ---[ 374]---> Adder-cost: 80   maxlim: 1298046   bits: 22/21
c ---[ 372]---> Adder-cost: 80   maxlim: 1297918   bits: 22/21
c ---[ 370]---> Adder-cost: 80   maxlim: 1299966   bits: 22/21
c ---[ 368]---> Adder-cost: 80   maxlim: 1295230   bits: 22/21
c ---[ 366]---> Adder-cost: 80   maxlim: 1296126   bits: 22/21
c ---[ 364]---> Adder-cost: 80   maxlim: 1300606   bits: 22/21
c ---[ 362]---> Adder-cost: 80   maxlim: 1297278   bits: 22/21
c ---[ 360]---> Adder-cost: 80   maxlim: 1298302   bits: 22/21
c ---[ 359]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 358]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 357]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
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 ---[ 346]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 345]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
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 ---[ 334]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 333]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
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: 18   maxlim: 262142   bits: 19/18
c ---[ 328]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 327]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 326]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 325]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 324]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 323]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 322]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 321]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 320]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 319]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 318]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 317]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 316]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 315]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 314]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 313]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 312]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 311]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 310]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 309]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 308]---> Adder-cost: 18   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: 14   maxlim: 262142   bits: 19/18
c ---[ 298]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 297]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 296]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 295]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 294]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 293]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 292]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 291]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 290]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 289]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 288]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 287]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 286]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 285]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 284]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 283]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 282]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 281]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 280]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 279]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 278]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 277]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 276]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 275]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 274]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 273]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 272]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 271]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 270]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[ 269]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 268]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 267]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 266]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 265]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 264]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 263]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 262]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 261]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 260]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 259]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 258]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 257]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 256]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 255]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 254]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 253]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 252]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 251]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 250]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 249]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 248]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 247]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 246]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 245]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 244]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 243]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 242]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 241]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 240]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 239]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 238]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 237]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 236]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 235]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 234]---> Adder-cost: 20   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 ---[ 224]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 223]---> Adder-cost: 20   maxlim: 262142   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 ---[ 212]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 211]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
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 ---[ 200]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 199]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 198]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 197]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 196]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 195]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 194]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 193]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 192]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 191]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 190]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 189]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 188]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 187]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 186]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 185]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 184]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 183]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 182]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 181]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 180]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 179]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 178]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 177]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 176]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 175]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 174]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 173]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 172]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 171]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 170]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 169]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 168]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 167]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 166]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 165]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 164]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 163]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 162]---> Adder-cost: 18   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 ---[ 152]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 151]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
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 ---[ 140]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 139]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
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 ---[ 128]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 127]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 126]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 125]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 124]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 123]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 122]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 121]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 120]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 119]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 118]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 117]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 116]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 115]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 114]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 113]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 112]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 111]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 110]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 109]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 108]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 107]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 106]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 105]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 104]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 103]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 102]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 101]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 100]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[  99]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[  98]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[  97]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[  96]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[  95]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[  94]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[  93]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[  92]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[  91]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[  90]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[  89]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  88]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  87]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  86]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  85]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  84]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  83]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  82]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  81]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  80]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  79]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  78]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  77]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  76]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  75]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  74]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  73]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  72]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  71]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  70]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  69]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  68]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  67]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  66]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  65]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  64]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  63]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  62]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  61]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  60]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  59]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  58]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  57]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  56]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  55]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  54]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  53]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  52]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  51]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  50]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  49]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  48]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  47]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  46]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  45]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  44]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  43]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  42]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  41]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  40]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  39]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  38]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  37]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  36]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  35]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  34]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  33]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  32]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  31]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  30]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[  29]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  28]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  27]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  26]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  25]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  24]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  23]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  22]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  21]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  20]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  19]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  18]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  17]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  16]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  15]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  14]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  13]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  12]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  11]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[  10]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[   9]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[   8]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[   7]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[   6]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[   5]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[   4]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[   3]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[   2]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[   1]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
c ---[   0]---> Adder-cost: 14   maxlim: 262142   bits: 19/18
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 |  293433  1078056 |  107608      99      305     3.1 | 29.774 % |
c |       251 |  293433  1078056 |  118369     250      774     3.1 | 29.774 % |
c |       476 |  293382  1077872 |  130206     472     2590     5.5 | 29.775 % |
c |       813 |  293355  1077785 |  143227     803     4468     5.6 | 29.780 % |
c |      1319 |  293343  1077749 |  157549    1307     7541     5.8 | 29.783 % |
c |      2079 |  293275  1077529 |  173304    2050    11650     5.7 | 29.796 % |
c |      3218 |  293102  1076955 |  190635    3157    17851     5.7 | 29.822 % |
c |      4926 |  292848  1076097 |  209698    4830    27985     5.8 | 29.854 % |
c |      7488 |  292447  1074800 |  230668    7275    42374     5.8 | 29.930 % |
c |     11332 |  292042  1073495 |  253735   11001    62983     5.7 | 30.008 % |
c |     17098 |  291380  1071349 |  279108   16580    95288     5.7 | 30.134 % |
c |     25747 |  290005  1066846 |  307019   24858   148114     6.0 | 30.378 % |
c |     38721 |  288314  1061331 |  337721   37336   243613     6.5 | 30.697 % |
c |     58182 |  286019  1053802 |  371494   56089   411863     7.3 | 31.129 % |
c |     87374 |  284154  1047688 |  408643   84733   709729     8.4 | 31.488 % |
c |    131163 |  282387  1041909 |  449507  127979  1222142     9.5 | 31.825 % |
c |    196849 |  279777  1033328 |  494458  192841  2014356    10.4 | 32.322 % |
c |    295375 |  277387  1025508 |  543904  290632  3312337    11.4 | 32.773 % |
c |    443165 |  275137  1018126 |  598294  437729  5373548    12.3 | 33.205 % |
#### 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.78 0.93 0.91 2/54 24273
Raw data (stat): 24273 (runsolver) R 24272 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540347402 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.81 0.93 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 9567 0 0 0 974 25 0 0 25 0 1 0 540347402 43909120 8838 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10720 8838 603 41 0 10679 0
vsize: 42880
[startup+20.0012 s]
Raw data (loadavg): 0.84 0.93 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 9673 0 0 0 1973 26 0 0 25 0 1 0 540347402 44314624 8944 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10819 8944 603 41 0 10778 0
vsize: 43276
[startup+30.0019 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 9766 0 0 0 2973 26 0 0 25 0 1 0 540347402 44748800 9037 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10925 9037 603 41 0 10884 0
vsize: 43700
[startup+40.0021 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 9858 0 0 0 3973 26 0 0 25 0 1 0 540347402 45019136 9129 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10991 9129 603 41 0 10950 0
vsize: 43964
[startup+50.0022 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 9943 0 0 0 4973 27 0 0 25 0 1 0 540347402 45424640 9214 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11090 9214 603 41 0 11049 0
vsize: 44360
[startup+60.0025 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10018 0 0 0 5973 27 0 0 25 0 1 0 540347402 45694976 9289 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11156 9289 603 41 0 11115 0
vsize: 44624
[startup+70.0031 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10087 0 0 0 6973 27 0 0 25 0 1 0 540347402 46092288 9358 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11253 9358 603 41 0 11212 0
vsize: 45012
[startup+80.0028 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10161 0 0 0 7973 27 0 0 25 0 1 0 540347402 46358528 9432 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11318 9432 603 41 0 11277 0
vsize: 45272
[startup+90.0034 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10223 0 0 0 8973 27 0 0 25 0 1 0 540347402 46628864 9494 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11384 9494 603 41 0 11343 0
vsize: 45536
[startup+100.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10288 0 0 0 9973 28 0 0 25 0 1 0 540347402 46899200 9559 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11450 9559 603 41 0 11409 0
vsize: 45800
[startup+110.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10384 0 0 0 10973 28 0 0 25 0 1 0 540347402 47304704 9655 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11549 9655 603 41 0 11508 0
vsize: 46196
[startup+120.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10450 0 0 0 11972 28 0 0 25 0 1 0 540347402 47439872 9721 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11582 9721 603 41 0 11541 0
vsize: 46328
[startup+130.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10521 0 0 0 12972 29 0 0 25 0 1 0 540347402 47841280 9792 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11680 9792 603 41 0 11639 0
vsize: 46720
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10611 0 0 0 13972 29 0 0 25 0 1 0 540347402 48107520 9882 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11745 9882 603 41 0 11704 0
vsize: 46980
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10684 0 0 0 14972 29 0 0 25 0 1 0 540347402 48377856 9955 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11811 9955 603 41 0 11770 0
vsize: 47244
[startup+160.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10770 0 0 0 15972 29 0 0 25 0 1 0 540347402 49045504 10041 4294967295 134512640 134672761 3221224544 3221223560 1075352749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11974 10041 603 41 0 11933 0
vsize: 47896
[startup+170.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10861 0 0 0 16972 29 0 0 25 0 1 0 540347402 49315840 10132 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12040 10132 603 41 0 11999 0
vsize: 48160
[startup+180.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 10974 0 0 0 17971 30 0 0 25 0 1 0 540347402 49856512 10245 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12172 10245 603 41 0 12131 0
vsize: 48688
[startup+190.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 11088 0 0 0 18972 30 0 0 25 0 1 0 540347402 50257920 10359 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12270 10359 603 41 0 12229 0
vsize: 49080
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 11175 0 0 0 19971 30 0 0 25 0 1 0 540347402 50528256 10446 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12336 10446 603 41 0 12295 0
vsize: 49344
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 11261 0 0 0 20971 31 0 0 25 0 1 0 540347402 50933760 10532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12435 10532 603 41 0 12394 0
vsize: 49740
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 11395 0 0 0 21971 31 0 0 25 0 1 0 540347402 51470336 10666 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12566 10666 603 41 0 12525 0
vsize: 50264
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 11531 0 0 0 22971 32 0 0 25 0 1 0 540347402 52011008 10802 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12698 10802 603 41 0 12657 0
vsize: 50792
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 11657 0 0 0 23970 32 0 0 25 0 1 0 540347402 52416512 10928 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12797 10928 603 41 0 12756 0
vsize: 51188
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 11765 0 0 0 24970 32 0 0 25 0 1 0 540347402 52957184 11036 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12929 11036 603 41 0 12888 0
vsize: 51716
[startup+260.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 11847 0 0 0 25970 33 0 0 25 0 1 0 540347402 53227520 11118 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12995 11118 603 41 0 12954 0
vsize: 51980
[startup+270.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 11946 0 0 0 26970 33 0 0 25 0 1 0 540347402 53633024 11217 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13094 11217 603 41 0 13053 0
vsize: 52376
[startup+280.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 12068 0 0 0 27969 34 0 0 25 0 1 0 540347402 54038528 11339 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13193 11339 603 41 0 13152 0
vsize: 52772
[startup+290.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 12171 0 0 0 28969 35 0 0 25 0 1 0 540347402 54964224 11442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13419 11442 603 41 0 13378 0
vsize: 53676
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 12276 0 0 0 29969 35 0 0 25 0 1 0 540347402 55369728 11547 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13518 11547 603 41 0 13477 0
vsize: 54072
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 12363 0 0 0 30969 35 0 0 25 0 1 0 540347402 55767040 11634 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13615 11634 603 41 0 13574 0
vsize: 54460
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 12492 0 0 0 31969 35 0 0 25 0 1 0 540347402 56307712 11763 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13747 11763 603 41 0 13706 0
vsize: 54988
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 12601 0 0 0 32968 36 0 0 25 0 1 0 540347402 56713216 11872 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13846 11872 603 41 0 13805 0
vsize: 55384
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 12689 0 0 0 33968 36 0 0 25 0 1 0 540347402 56983552 11960 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13912 11960 603 41 0 13871 0
vsize: 55648
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 12773 0 0 0 34968 36 0 0 25 0 1 0 540347402 57389056 12044 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14011 12044 603 41 0 13970 0
vsize: 56044
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 12847 0 0 0 35968 37 0 0 25 0 1 0 540347402 57659392 12118 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14077 12118 603 41 0 14036 0
vsize: 56308
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 12935 0 0 0 36968 37 0 0 25 0 1 0 540347402 58064896 12206 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14176 12206 603 41 0 14135 0
vsize: 56704
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 13025 0 0 0 37968 37 0 0 25 0 1 0 540347402 58335232 12296 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14242 12296 603 41 0 14201 0
vsize: 56968
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 13143 0 0 0 38968 37 0 0 25 0 1 0 540347402 58875904 12414 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14374 12414 603 41 0 14333 0
vsize: 57496
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 13248 0 0 0 39968 38 0 0 25 0 1 0 540347402 59281408 12519 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14473 12519 603 41 0 14432 0
vsize: 57892
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 13350 0 0 0 40968 38 0 0 25 0 1 0 540347402 59686912 12621 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14572 12621 603 41 0 14531 0
vsize: 58288
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 13440 0 0 0 41968 38 0 0 25 0 1 0 540347402 59957248 12711 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14638 12711 603 41 0 14597 0
vsize: 58552
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 13516 0 0 0 42968 39 0 0 25 0 1 0 540347402 60227584 12787 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14704 12787 603 41 0 14663 0
vsize: 58816
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 13615 0 0 0 43967 39 0 0 25 0 1 0 540347402 60633088 12886 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14803 12886 603 41 0 14762 0
vsize: 59212
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 13686 0 0 0 44966 40 0 0 25 0 1 0 540347402 60903424 12957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14869 12957 603 41 0 14828 0
vsize: 59476
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 13740 0 0 0 45966 40 0 0 25 0 1 0 540347402 61173760 13011 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14935 13011 603 41 0 14894 0
vsize: 59740
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 13804 0 0 0 46966 40 0 0 25 0 1 0 540347402 61444096 13075 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15001 13075 603 41 0 14960 0
vsize: 60004
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 13905 0 0 0 47965 40 0 0 25 0 1 0 540347402 61849600 13176 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15100 13176 603 41 0 15059 0
vsize: 60400
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 13983 0 0 0 48965 41 0 0 25 0 1 0 540347402 62119936 13254 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15166 13254 603 41 0 15125 0
vsize: 60664
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 14076 0 0 0 49965 41 0 0 25 0 1 0 540347402 62390272 13347 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15232 13347 603 41 0 15191 0
vsize: 60928
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 14167 0 0 0 50965 42 0 0 25 0 1 0 540347402 62795776 13438 4294967295 134512640 134672761 3221224544 3221223668 134566040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15331 13438 603 41 0 15290 0
vsize: 61324
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 14271 0 0 0 51965 42 0 0 25 0 1 0 540347402 63197184 13542 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15429 13542 603 41 0 15388 0
vsize: 61716
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 14369 0 0 0 52964 42 0 0 25 0 1 0 540347402 63598592 13640 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15527 13640 603 41 0 15486 0
vsize: 62108
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 14464 0 0 0 53964 43 0 0 25 0 1 0 540347402 64000000 13735 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15625 13735 603 41 0 15584 0
vsize: 62500
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 14528 0 0 0 54964 43 0 0 25 0 1 0 540347402 64270336 13799 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15691 13799 603 41 0 15650 0
vsize: 62764
[startup+560.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 14592 0 0 0 55974 44 0 0 25 0 1 0 540347402 64405504 13863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15724 13863 603 41 0 15683 0
vsize: 62896
[startup+570.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 14720 0 0 0 56974 44 0 0 25 0 1 0 540347402 64942080 13991 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15855 13991 603 41 0 15814 0
vsize: 63420
[startup+580.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 14822 0 0 0 57974 44 0 0 25 0 1 0 540347402 65347584 14093 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15954 14093 603 41 0 15913 0
vsize: 63816
[startup+590.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 14944 0 0 0 58974 45 0 0 25 0 1 0 540347402 65884160 14215 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16085 14215 603 41 0 16044 0
vsize: 64340
[startup+600.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 15023 0 0 0 59974 45 0 0 25 0 1 0 540347402 66150400 14294 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16150 14294 603 41 0 16109 0
vsize: 64600
[startup+610.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 15129 0 0 0 60974 45 0 0 25 0 1 0 540347402 66555904 14400 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16249 14400 603 41 0 16208 0
vsize: 64996
[startup+620.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 15225 0 0 0 61973 46 0 0 25 0 1 0 540347402 66957312 14496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16347 14496 603 41 0 16306 0
vsize: 65388
[startup+630.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 15321 0 0 0 62973 46 0 0 25 0 1 0 540347402 68407296 14592 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16701 14592 603 41 0 16660 0
vsize: 66804
[startup+640.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 15396 0 0 0 63973 46 0 0 25 0 1 0 540347402 68677632 14667 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16767 14667 603 41 0 16726 0
vsize: 67068
[startup+650.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 15479 0 0 0 64973 46 0 0 25 0 1 0 540347402 68947968 14750 4294967295 134512640 134672761 3221224544 3221223712 134564734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16833 14750 603 41 0 16792 0
vsize: 67332
[startup+660.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 15592 0 0 0 65973 47 0 0 25 0 1 0 540347402 69484544 14863 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16964 14863 603 41 0 16923 0
vsize: 67856
[startup+670.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 15687 0 0 0 66973 47 0 0 25 0 1 0 540347402 69885952 14958 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17062 14958 603 41 0 17021 0
vsize: 68248
[startup+680.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 15786 0 0 0 67973 47 0 0 25 0 1 0 540347402 70156288 15057 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17128 15057 603 41 0 17087 0
vsize: 68512
[startup+690.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 15871 0 0 0 68973 48 0 0 25 0 1 0 540347402 70557696 15142 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17226 15142 603 41 0 17185 0
vsize: 68904
[startup+700.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 15937 0 0 0 69972 48 0 0 25 0 1 0 540347402 70823936 15208 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17291 15208 603 41 0 17250 0
vsize: 69164
[startup+710.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16004 0 0 0 70971 49 0 0 25 0 1 0 540347402 71094272 15275 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17357 15275 603 41 0 17316 0
vsize: 69428
[startup+720.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16074 0 0 0 71970 49 0 0 25 0 1 0 540347402 71364608 15345 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17423 15345 603 41 0 17382 0
vsize: 69692
[startup+730.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16166 0 0 0 72969 50 0 0 25 0 1 0 540347402 71634944 15437 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17489 15437 603 41 0 17448 0
vsize: 69956
[startup+740.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16256 0 0 0 73968 51 0 0 25 0 1 0 540347402 72036352 15527 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17587 15527 603 41 0 17546 0
vsize: 70348
[startup+750.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16321 0 0 0 74968 51 0 0 25 0 1 0 540347402 72306688 15592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17653 15592 603 41 0 17612 0
vsize: 70612
[startup+760.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16392 0 0 0 75967 51 0 0 25 0 1 0 540347402 72577024 15663 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17719 15663 603 41 0 17678 0
vsize: 70876
[startup+770.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16451 0 0 0 76967 52 0 0 25 0 1 0 540347402 72843264 15722 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17784 15722 603 41 0 17743 0
vsize: 71136
[startup+780.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16504 0 0 0 77967 52 0 0 25 0 1 0 540347402 72978432 15775 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17817 15775 603 41 0 17776 0
vsize: 71268
[startup+790.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16566 0 0 0 78967 52 0 0 25 0 1 0 540347402 73248768 15837 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17883 15837 603 41 0 17842 0
vsize: 71532
[startup+800.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16639 0 0 0 79967 53 0 0 25 0 1 0 540347402 73515008 15910 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17948 15910 603 41 0 17907 0
vsize: 71792
[startup+810.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16715 0 0 0 80966 53 0 0 25 0 1 0 540347402 73785344 15986 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18014 15986 603 41 0 17973 0
vsize: 72056
[startup+820.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16778 0 0 0 81966 54 0 0 25 0 1 0 540347402 74047488 16049 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18078 16049 603 41 0 18037 0
vsize: 72312
[startup+830.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16881 0 0 0 82966 54 0 0 25 0 1 0 540347402 74448896 16152 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18176 16152 603 41 0 18135 0
vsize: 72704
[startup+840.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 16951 0 0 0 83966 54 0 0 25 0 1 0 540347402 74719232 16222 4294967295 134512640 134672761 3221224544 3221223744 134557892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18242 16222 603 41 0 18201 0
vsize: 72968
[startup+850.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 17037 0 0 0 84966 55 0 0 25 0 1 0 540347402 75124736 16308 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18341 16308 603 41 0 18300 0
vsize: 73364
[startup+860.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 17132 0 0 0 85966 55 0 0 25 0 1 0 540347402 75530240 16403 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18440 16403 603 41 0 18399 0
vsize: 73760
[startup+870.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 17238 0 0 0 86966 55 0 0 25 0 1 0 540347402 75931648 16509 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18538 16509 603 41 0 18497 0
vsize: 74152
[startup+880.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 17327 0 0 0 87966 56 0 0 25 0 1 0 540347402 76201984 16598 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18604 16598 603 41 0 18563 0
vsize: 74416
[startup+890.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 17441 0 0 0 88965 56 0 0 25 0 1 0 540347402 76742656 16712 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18736 16712 603 41 0 18695 0
vsize: 74944
[startup+900.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 17525 0 0 0 89965 56 0 0 25 0 1 0 540347402 77004800 16796 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18800 16796 603 41 0 18759 0
vsize: 75200
[startup+910.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 17603 0 0 0 90965 56 0 0 25 0 1 0 540347402 77275136 16874 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18866 16874 603 41 0 18825 0
vsize: 75464
[startup+920.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 17689 0 0 0 91965 57 0 0 25 0 1 0 540347402 77680640 16960 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18965 16960 603 41 0 18924 0
vsize: 75860
[startup+930.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 17766 0 0 0 92965 57 0 0 25 0 1 0 540347402 77950976 17037 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19031 17037 603 41 0 18990 0
vsize: 76124
[startup+940.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 17855 0 0 0 93965 57 0 0 25 0 1 0 540347402 78352384 17126 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19129 17126 603 41 0 19088 0
vsize: 76516
[startup+950.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 17931 0 0 0 94965 58 0 0 25 0 1 0 540347402 78622720 17202 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19195 17202 603 41 0 19154 0
vsize: 76780
[startup+960.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18030 0 0 0 95965 58 0 0 25 0 1 0 540347402 79028224 17301 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19294 17301 603 41 0 19253 0
vsize: 77176
[startup+970.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18102 0 0 0 96965 58 0 0 25 0 1 0 540347402 79298560 17373 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19360 17373 603 41 0 19319 0
vsize: 77440
[startup+980.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18168 0 0 0 97965 58 0 0 25 0 1 0 540347402 79568896 17439 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19426 17439 603 41 0 19385 0
vsize: 77704
[startup+990.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18251 0 0 0 98965 58 0 0 25 0 1 0 540347402 79839232 17522 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19492 17522 603 41 0 19451 0
vsize: 77968
[startup+1000.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18337 0 0 0 99965 58 0 0 25 0 1 0 540347402 80240640 17608 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19590 17608 603 41 0 19549 0
vsize: 78360
[startup+1010.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18404 0 0 0 100965 59 0 0 25 0 1 0 540347402 80506880 17675 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19655 17675 603 41 0 19614 0
vsize: 78620
[startup+1020.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18474 0 0 0 101965 59 0 0 25 0 1 0 540347402 80773120 17745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19720 17745 603 41 0 19679 0
vsize: 78880
[startup+1030.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18548 0 0 0 102965 59 0 0 25 0 1 0 540347402 81043456 17819 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19786 17819 603 41 0 19745 0
vsize: 79144
[startup+1040.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18630 0 0 0 103965 59 0 0 25 0 1 0 540347402 81448960 17901 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19885 17901 603 41 0 19844 0
vsize: 79540
[startup+1050.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18687 0 0 0 104965 60 0 0 25 0 1 0 540347402 81584128 17958 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19918 17958 603 41 0 19877 0
vsize: 79672
[startup+1060.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18785 0 0 0 105965 60 0 0 25 0 1 0 540347402 81993728 18056 4294967295 134512640 134672761 3221224544 3221223728 134559548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20018 18056 603 41 0 19977 0
vsize: 80072
[startup+1070.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18870 0 0 0 106965 60 0 0 25 0 1 0 540347402 82264064 18141 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20084 18141 603 41 0 20043 0
vsize: 80336
[startup+1080.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 18945 0 0 0 107965 60 0 0 25 0 1 0 540347402 82669568 18216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20183 18216 603 41 0 20142 0
vsize: 80732
[startup+1090.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 19029 0 0 0 108964 61 0 0 25 0 1 0 540347402 82931712 18300 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20247 18300 603 41 0 20206 0
vsize: 80988
[startup+1100.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 19122 0 0 0 109964 61 0 0 25 0 1 0 540347402 83333120 18393 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20345 18393 603 41 0 20304 0
vsize: 81380
[startup+1110.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 19207 0 0 0 110964 62 0 0 25 0 1 0 540347402 83603456 18478 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20411 18478 603 41 0 20370 0
vsize: 81644
[startup+1120.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 19295 0 0 0 111964 62 0 0 25 0 1 0 540347402 84008960 18566 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20510 18566 603 41 0 20469 0
vsize: 82040
[startup+1130.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 19422 0 0 0 112963 63 0 0 25 0 1 0 540347402 84545536 18693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20641 18693 603 41 0 20600 0
vsize: 82564
[startup+1140.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 19525 0 0 0 113963 64 0 0 25 0 1 0 540347402 84951040 18796 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20740 18796 603 41 0 20699 0
vsize: 82960
[startup+1150.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 19648 0 0 0 114963 64 0 0 25 0 1 0 540347402 85352448 18919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20838 18919 603 41 0 20797 0
vsize: 83352
[startup+1160.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 19720 0 0 0 115962 64 0 0 25 0 1 0 540347402 85622784 18991 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20904 18991 603 41 0 20863 0
vsize: 83616
[startup+1170.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 19863 0 0 0 116961 65 0 0 25 0 1 0 540347402 86163456 19134 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21036 19134 603 41 0 20995 0
vsize: 84144
[startup+1180.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 19964 0 0 0 117960 66 0 0 25 0 1 0 540347402 86573056 19235 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21136 19235 603 41 0 21095 0
vsize: 84544
[startup+1190.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 20065 0 0 0 118960 66 0 0 25 0 1 0 540347402 86978560 19336 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21235 19336 603 41 0 21194 0
vsize: 84940
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 24273
Raw data (stat): 24273 (minisat+) R 24272 3260 3259 0 -1 0 20172 0 0 0 119960 67 0 0 25 0 1 0 540347402 87384064 19443 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21334 19443 603 41 0 21293 0
vsize: 85336
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 24273
Raw data (stat): 24273 (minisat+) Z 24272 3260 3259 0 -1 12 20174 0 0 0 119960 70 0 0 25 0 1 0 540347402 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.18
CPU time (s): 1200.31
CPU user time (s): 1199.6
CPU system time (s): 0.708892
CPU usage (%): 100.011
Max. virtual memory (Kb): 85336
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####