PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-10teams.opb
MD5SUM	1ff3cc3253012886aa21be4feac6111e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	924
Optimality of the best value was proved	NO
Number of terms in the objective function	1800
Biggest coefficient in the objective function	86
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	41700
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	86
Number of bits of the biggest number in a constraint	7
Biggest sum of numbers in a constraint	41700
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.71
Number of variables	1800
Total number of constraints	2015
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2015
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	72
Trace number 21944

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-22 01:32:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12387 boxname=wulflinc3 idbench=953 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1ff3cc3253012886aa21be4feac6111e  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-10teams.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-10teams.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-10teams.opb
IDLAUNCH: 12387
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 2
cpu MHz		: 451.190
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:        491752 kB
Buffers:         34360 kB
Cached:         486248 kB
SwapCached:          0 kB
Active:          42520 kB
Inactive:       480880 kB
HighTotal:      131008 kB
HighFree:        26908 kB
LowTotal:       903652 kB
LowFree:        464844 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            13768 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 01:52:09 (client local time) WITH STATUS 10 IN 1200.34 SECONDS
stats: 12387 7 1200.34 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 330 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 329]---> BDD-cost:  125
c ---[ 328]---> BDD-cost:  185
c ---[ 326]---> BDD-cost:   77
c ---[ 324]---> BDD-cost:   77
c ---[ 322]---> BDD-cost:   77
c ---[ 320]---> BDD-cost:   77
c ---[ 318]---> BDD-cost:   77
c ---[ 316]---> BDD-cost:   77
c ---[ 314]---> BDD-cost:   77
c ---[ 312]---> BDD-cost:   77
c ---[ 310]---> BDD-cost:   77
c ---[ 308]---> BDD-cost:   77
c ---[ 307]---> BDD-cost:  185
c ---[ 305]---> BDD-cost:   77
c ---[ 303]---> BDD-cost:   77
c ---[ 301]---> BDD-cost:   77
c ---[ 299]---> BDD-cost:   77
c ---[ 297]---> BDD-cost:   77
c ---[ 295]---> BDD-cost:   77
c ---[ 293]---> BDD-cost:   77
c ---[ 291]---> BDD-cost:   77
c ---[ 289]---> BDD-cost:   77
c ---[ 288]---> BDD-cost:  125
c ---[ 286]---> BDD-cost:   77
c ---[ 284]---> BDD-cost:   77
c ---[ 282]---> BDD-cost:   77
c ---[ 280]---> BDD-cost:   77
c ---[ 278]---> BDD-cost:   77
c ---[ 276]---> BDD-cost:   77
c ---[ 274]---> BDD-cost:   77
c ---[ 272]---> BDD-cost:   77
c ---[ 270]---> BDD-cost:   77
c ---[ 269]---> BDD-cost:  185
c ---[ 267]---> BDD-cost:   77
c ---[ 265]---> BDD-cost:   77
c ---[ 263]---> BDD-cost:   77
c ---[ 261]---> BDD-cost:   77
c ---[ 259]---> BDD-cost:   77
c ---[ 257]---> BDD-cost:   77
c ---[ 255]---> BDD-cost:   77
c ---[ 253]---> BDD-cost:   77
c ---[ 251]---> BDD-cost:   77
c ---[ 250]---> BDD-cost:  185
c ---[ 248]---> BDD-cost:   70
c ---[ 246]---> BDD-cost:   77
c ---[ 244]---> BDD-cost:   77
c ---[ 242]---> BDD-cost:   77
c ---[ 240]---> BDD-cost:   77
c ---[ 238]---> BDD-cost:   77
c ---[ 236]---> BDD-cost:   77
c ---[ 234]---> BDD-cost:   77
c ---[ 233]---> BDD-cost:  185
c ---[ 231]---> BDD-cost:   77
c ---[ 229]---> BDD-cost:   77
c ---[ 227]---> BDD-cost:   77
c ---[ 225]---> BDD-cost:   77
c ---[ 223]---> BDD-cost:   77
c ---[ 221]---> BDD-cost:   77
c ---[ 219]---> BDD-cost:   77
c ---[ 217]---> BDD-cost:   77
c ---[ 216]---> BDD-cost:  185
c ---[ 214]---> BDD-cost:   70
c ---[ 212]---> BDD-cost:   77
c ---[ 210]---> BDD-cost:   77
c ---[ 208]---> BDD-cost:   77
c ---[ 206]---> BDD-cost:   77
c ---[ 204]---> BDD-cost:   77
c ---[ 202]---> BDD-cost:   77
c ---[ 200]---> BDD-cost:   77
c ---[ 198]---> BDD-cost:   70
c ---[ 197]---> BDD-cost:  185
c ---[ 195]---> BDD-cost:   77
c ---[ 193]---> BDD-cost:   77
c ---[ 191]---> BDD-cost:   77
c ---[ 189]---> BDD-cost:   77
c ---[ 187]---> BDD-cost:   77
c ---[ 185]---> BDD-cost:   77
c ---[ 183]---> BDD-cost:   77
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   77
c ---[ 178]---> BDD-cost:  125
c ---[ 176]---> BDD-cost:   77
c ---[ 174]---> BDD-cost:   77
c ---[ 172]---> BDD-cost:   77
c ---[ 170]---> BDD-cost:   77
c ---[ 168]---> BDD-cost:   77
c ---[ 166]---> BDD-cost:   77
c ---[ 164]---> BDD-cost:   77
c ---[ 162]---> BDD-cost:   77
c ---[ 160]---> BDD-cost:   77
c ---[ 159]---> BDD-cost:  185
c ---[ 157]---> BDD-cost:   77
c ---[ 155]---> BDD-cost:   77
c ---[ 153]---> BDD-cost:   77
c ---[ 151]---> BDD-cost:   77
c ---[ 149]---> BDD-cost:   77
c ---[ 147]---> BDD-cost:   77
c ---[ 145]---> BDD-cost:   77
c ---[ 143]---> BDD-cost:   77
c ---[ 141]---> BDD-cost:   77
c ---[ 140]---> BDD-cost:  185
c ---[ 139]---> BDD-cost:  185
c ---[ 137]---> BDD-cost:   77
c ---[ 135]---> BDD-cost:   77
c ---[ 133]---> BDD-cost:   77
c ---[ 131]---> BDD-cost:   77
c ---[ 129]---> BDD-cost:   77
c ---[ 127]---> BDD-cost:   77
c ---[ 125]---> BDD-cost:   77
c ---[ 123]---> BDD-cost:   77
c ---[ 121]---> BDD-cost:   77
c ---[ 120]---> BDD-cost:  178
c ---[ 118]---> BDD-cost:   77
c ---[ 116]---> BDD-cost:   77
c ---[ 114]---> BDD-cost:   77
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:   77
c ---[ 108]---> BDD-cost:   77
c ---[ 106]---> BDD-cost:   77
c ---[ 104]---> BDD-cost:   77
c ---[ 102]---> BDD-cost:   77
c ---[ 101]---> BDD-cost:  185
c ---[  99]---> BDD-cost:   77
c ---[  97]---> BDD-cost:   77
c ---[  95]---> BDD-cost:   77
c ---[  93]---> BDD-cost:   77
c ---[  91]---> BDD-cost:   77
c ---[  89]---> BDD-cost:   77
c ---[  87]---> BDD-cost:   77
c ---[  85]---> BDD-cost:   77
c ---[  83]---> BDD-cost:   77
c ---[  82]---> BDD-cost:  125
c ---[  80]---> BDD-cost:   77
c ---[  79]---> BDD-cost:  185
c ---[  78]---> BDD-cost:  185
c ---[  77]---> BDD-cost:  178
c ---[  76]---> BDD-cost:  185
c ---[  75]---> BDD-cost:  185
c ---[  74]---> BDD-cost:  125
c ---[  73]---> BDD-cost:  185
c ---[  72]---> BDD-cost:  185
c ---[  71]---> BDD-cost:  178
c ---[  70]---> BDD-cost:  185
c ---[  69]---> BDD-cost:  185
c ---[  68]---> BDD-cost:  125
c ---[  67]---> BDD-cost:  185
c ---[  66]---> BDD-cost:  178
c ---[  65]---> BDD-cost:  185
c ---[  64]---> BDD-cost:  185
c ---[  63]---> BDD-cost:  185
c ---[  62]---> BDD-cost:  185
c ---[  61]---> BDD-cost:  125
c ---[  60]---> BDD-cost:  118
c ---[  59]---> BDD-cost:  185
c ---[  58]---> BDD-cost:  185
c ---[  57]---> BDD-cost:  185
c ---[  56]---> BDD-cost:  185
c ---[  55]---> BDD-cost:  178
c ---[  54]---> BDD-cost:  185
c ---[  53]---> BDD-cost:  185
c ---[  52]---> BDD-cost:  185
c ---[  51]---> BDD-cost:  185
c ---[  50]---> BDD-cost:  125
c ---[  49]---> BDD-cost:   76
c ---[  48]---> BDD-cost:   76
c ---[  47]---> BDD-cost:   76
c ---[  46]---> BDD-cost:   76
c ---[  45]---> BDD-cost:   76
c ---[  44]---> BDD-cost:   76
c ---[  43]---> BDD-cost:   76
c ---[  42]---> BDD-cost:   76
c ---[  41]---> BDD-cost:  177
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:  123
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:  183
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   75
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:  183
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   53221   141547 |   15966       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/22273          
c   -- var.elim.:  2000/22273          
c   -- var.elim.:  3000/22273          
c   -- var.elim.:  4000/22273          
c   -- var.elim.:  5000/22273          
c   -- var.elim.:  6000/22273          
c   -- var.elim.:  7000/22273          
c   -- var.elim.:  8000/22273          
c   -- var.elim.:  9000/22273          
c   -- var.elim.:  10000/22273          
c   -- var.elim.:  11000/22273          
c   -- var.elim.:  12000/22273          
c   -- var.elim.:  13000/22273          
c   -- var.elim.:  14000/22273          
c   -- var.elim.:  15000/22273          
c   -- var.elim.:  16000/22273          
c   -- var.elim.:  17000/22273          
c   -- var.elim.:  18000/22273          
c   -- var.elim.:  19000/22273          
c   -- var.elim.:  20000/22273          
c   -- var.elim.:  21000/22273          
c   -- var.elim.:  22000/22273          
c   -- var.elim.:  22273/22273          
c   -- var.elim.:  1000/1593          
c   -- var.elim.:  1593/1593          
c   -- subsuming                       
c   -- var.elim.:  1000/1133          
c   -- var.elim.:  1133/1133          
c   -- var.elim.:  1000/1203          
c   -- var.elim.:  1203/1203          
c   -- subsuming                       
c   -- var.elim.:  734/734          
c   -- var.elim.:  187/187          
c   -- subsuming                       
c   -- var.elim.:  185/185          
c |         0 |   52136   138492 |      --       0       --      -- |     --   | -1085/-2425
c |         0 |   52136   138492 |   20854       0        0     nan |  0.000 % |
c |       101 |   52136   138492 |   22939     101     3830    37.9 |  1.881 % |
c |       251 |   52136   138492 |   25233     251    19416    77.4 |  1.881 % |
c |       477 |   52136   138492 |   27757     477    38333    80.4 |  1.881 % |
c |       814 |   52136   138492 |   30532     814    98840   121.4 |  1.881 % |
c |      1320 |   52136   138492 |   33586    1320   172120   130.4 |  1.881 % |
c |      2080 |   52136   138492 |   36944    2080   301396   144.9 |  1.881 % |
c |      3219 |   52136   138492 |   40639    3219   660173   205.1 |  1.881 % |
c |      4927 |   52136   138492 |   44703    4927  1111412   225.6 |  1.881 % |
c |      7489 |   52136   138492 |   49173    7489  1955470   261.1 |  1.881 % |
c |     11337 |   52136   138492 |   54090   11337  3889115   343.0 |  1.881 % |
c ==============================================================================
c (current CPU-time: 47.5128 s)
c ==============================================================================
c [1mFound solution: 1020[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 7750   maxlim: 38980   bits: 16/16
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15476 |  106290   331879 |   31886   15476  4915909   317.6 |  1.881 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9299          
c   -- var.elim.:  2000/9299          
c   -- var.elim.:  3000/9299          
c   -- var.elim.:  4000/9299          
c   -- var.elim.:  5000/9299          
c   -- var.elim.:  6000/9299          
c   -- var.elim.:  7000/9299          
c   -- var.elim.:  8000/9299          
c   -- var.elim.:  9000/9299          
c   -- var.elim.:  9299/9299          
c   -- var.elim.:  21/21          
c |     15476 |  105937   330469 |      --   15476       --      -- |     --   | -321/-1265
c |     15476 |  105937   330469 |   42374   15476  4915909   317.6 |  1.881 % |
c |     15581 |  105937   330469 |   46612   15581  4938018   316.9 |  1.577 % |
c |     15733 |  105937   330469 |   51273   15733  4946441   314.4 |  1.577 % |
c |     15958 |  105937   330469 |   56400   15958  4983234   312.3 |  1.577 % |
c |     16300 |  105937   330469 |   62040   16300  5070057   311.0 |  1.577 % |
c |     16807 |  105937   330469 |   68245   16807  5170781   307.7 |  1.577 % |
c |     17568 |  105937   330469 |   75069   17568  5385993   306.6 |  1.577 % |
c |     18710 |  105937   330469 |   82576   18710  5588133   298.7 |  1.577 % |
c |     20421 |  105937   330469 |   90834   20421  6278716   307.5 |  1.577 % |
c |     22984 |  105937   330469 |   99917   22984  7293789   317.3 |  1.577 % |
c ==============================================================================
c (current CPU-time: 92.9759 s)
c ==============================================================================
c [1mFound solution: 1014[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 38986   bits: 16/16
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     23459 |  105954   330547 |   31786   23459  7415419   316.1 |  1.577 % |
c   -- subsuming                       
c   -- var.elim.:  22/22          
c   -- var.elim.:  12/12          
c |     23459 |  105950   330545 |      --   23459       --      -- |     --   | -4/1
c |     23459 |  105950   330545 |   42380   23459  7415419   316.1 |  1.577 % |
c |     23561 |  105950   330545 |   46618   23561  7438013   315.7 |  1.587 % |
c |     23712 |  105950   330545 |   51279   23712  7445497   314.0 |  1.587 % |
c |     23939 |  105950   330545 |   56407   23939  7482810   312.6 |  1.587 % |
c |     24276 |  105950   330545 |   62048   24276  7546752   310.9 |  1.587 % |
c ==============================================================================
c (current CPU-time: 99.1539 s)
c ==============================================================================
c [1mFound solution: 976[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39024   bits: 16/16
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     24355 |  105961   330596 |   31788   24355  7550134   310.0 |  1.587 % |
c   -- subsuming                       
c   -- var.elim.:  19/19          
c   -- var.elim.:  11/11          
c |     24355 |  105955   330565 |      --   24355       --      -- |     --   | -1/20
c |     24355 |  105955   330565 |   42382   24355  7550134   310.0 |  1.587 % |
c |     24455 |  105955   330565 |   46620   24455  7561272   309.2 |  1.597 % |
c |     24605 |  105955   330565 |   51282   24605  7576281   307.9 |  1.597 % |
c |     24830 |  105955   330565 |   56410   24830  7638056   307.6 |  1.597 % |
c |     25168 |  105955   330565 |   62051   25168  7707377   306.2 |  1.597 % |
c |     25676 |  105955   330565 |   68256   25676  7823570   304.7 |  1.597 % |
c |     26436 |  105955   330565 |   75082   26436  8015793   303.2 |  1.597 % |
c |     27575 |  105955   330565 |   82590   27575  8528839   309.3 |  1.597 % |
c |     29287 |  105955   330565 |   90849   29287  9153015   312.5 |  1.597 % |
c |     31849 |  105955   330565 |   99934   31849 10026971   314.8 |  1.597 % |
c |     35693 |  105955   330565 |  109927   35693 11985582   335.8 |  1.597 % |
c |     41461 |  105955   330565 |  120920   41461 14563012   351.2 |  1.597 % |
c |     50110 |  105955   330565 |  133012   50110 19364496   386.4 |  1.597 % |
c ==============================================================================
c (current CPU-time: 320.841 s)
c ==============================================================================
c [1mFound solution: 960[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39040   bits: 16/16
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     55366 |  105968   330618 |   31790   55366 21509920   388.5 |  1.597 % |
c   -- subsuming                       
c   -- var.elim.:  23/23          
c   -- var.elim.:  15/15          
c |     55366 |  105947   330531 |      --   55366       --      -- |     --   | -5/61
c |     55366 |  105947   330531 |   42378   55366 21509920   388.5 |  1.597 % |
c |     55470 |  105947   330531 |   46616   15472  6082070   393.1 |  1.604 % |
c |     55620 |  105947   330531 |   51278   15622  6100838   390.5 |  1.604 % |
c |     55847 |  105947   330531 |   56406   15849  6150444   388.1 |  1.604 % |
c |     56185 |  105947   330531 |   62046   16187  6196148   382.8 |  1.604 % |
c |     56694 |  105947   330531 |   68251   16696  6271052   375.6 |  1.604 % |
c |     57453 |  105947   330531 |   75076   17455  6442749   369.1 |  1.604 % |
c |     58593 |  105947   330531 |   82584   18595  6862391   369.0 |  1.604 % |
c |     60301 |  105947   330531 |   90842   20303  7686541   378.6 |  1.604 % |
c |     62863 |  105947   330531 |   99926   22865  8584346   375.4 |  1.604 % |
c |     66707 |  105947   330531 |  109919   26709  9714836   363.7 |  1.604 % |
c |     72476 |  105947   330531 |  120911   32478 13698569   421.8 |  1.604 % |
c |     81127 |  105947   330531 |  133002   41129 17297556   420.6 |  1.604 % |
c |     94102 |  105947   330531 |  146303   54104 27246116   503.6 |  1.604 % |
c |    113565 |  105947   330531 |  160933   73567 38685267   525.9 |  1.604 % |
c |    142757 |  105947   330531 |  177026  102759 58413395   568.5 |  1.604 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x226_bit0 -x227_bit0 -x228_bit0 -x229_bit0 -x230_bit0 -x231_bit0 -x232_bit0 -x233_bit0 x234_bit0 -x235_bit0 -x236_bit0 -x237_bit0 -x238_bit0 -x239_bit0 -x240_bit0 -x241_bit0 -x242_bit0 -x243_bit0 -x244_bit0 -x245_bit0 -x246_bit0 -x247_bit0 -x248_bit0 -x249_bit0 -x250_bit0 -x251_bit0 -x252_bit0 -x253_bit0 -x254_bit0 -x255_bit0 -x256_bit0 -x257_bit0 -x258_bit0 -x259_bit0 -x260_bit0 -x261_bit0 -x262_bit0 -x263_bit0 -x264_bit0 -x265_bit0 -x266_bit0 -x267_bit0 -x268_bit0 -x269_bit0 -x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 -x275_bit0 -x276_bit0 -x277_bit0 -x278_bit0 -x279_bit0 -x280_bit0 -x281_bit0 -x282_bit0 -x283_bit0 -x284_bit0 -x285_bit0 -x286_bit0 -x287_bit0 -x288_bit0 -x289_bit0 -x290_bit0 -x291_bit0 -x292_bit0 -x293_bit0 -x294_bit0 -x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 -x299_bit0 -x300_bit0 -x301_bit0 -x302_bit0 -x303_bit0 -x304_bit0 -x305_bit0 -x306_bit0 -x307_bit0 -x308_bit0 -x309_bit0 -x310_bit0 -x311_bit0 -x312_bit0 x313_bit0 -x314_bit0 -x315_bit0 -x316_bit0 -x317_bit0 -x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 -x333_bit0 -x334_bit0 -x335_bit0 -x336_bit0 -x337_bit0 -x338_bit0 -x339_bit0 -x340_bit0 -x341_bit0 -x342_bit0 -x343_bit0 -x344_bit0 -x345_bit0 -x346_bit0 x347_bit0 -x348_bit0 -x349_bit0 -x350_bit0 -x351_bit0 -x352_bit0 -x353_bit0 -x354_bit0 -x355_bit0 -x356_bit0 -x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 -x366_bit0 -x367_bit0 -x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 -x373_bit0 -x374_bit0 -x375_bit0 -x376_bit0 -x377_bit0 -x378_bit0 -x379_bit0 -x380_bit0 -x381_bit0 -x382_bit0 x383_bit0 -x384_bit0 -x385_bit0 -x386_bit0 -x387_bit0 -x388_bit0 -x389_bit0 -x390_bit0 -x391_bit0 -x392_bit0 -x393_bit0 -x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 -x399_bit0 -x400_bit0 -x401_bit0 -x402_bit0 -x403_bit0 -x404_bit0 -x405_bit0 -x406_bit0 -x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0 -x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 x416_bit0 -x417_bit0 -x418_bit0 -x419_bit0 -x420_bit0 -x421_bit0 -x422_bit0 -x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x427_bit0 -x428_bit0 -x429_bit0 -x430_bit0 -x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 -x436_bit0 -x437_bit0 -x438_bit0 -x439_bit0 -x440_bit0 -x441_bit0 -x442_bit0 -x443_bit0 -x444_bit0 -x445_bit0 -x446_bit0 -x447_bit0 -x448_bit0 -x449_bit0 -x450_bit0 -x451_bit0 -x452_bit0 -x453_bit0 -x454_bit0 -x455_bit0 -x456_bit0 -x457_bit0 -x458_bit0 -x459_bit0 -x460_bit0 -x461_bit0 -x462_bit0 -x463_bit0 -x464_bit0 -x465_bit0 -x466_bit0 -x467_bit0 -x468_bit0 -x469_bit0 -x470_bit0 -x471_bit0 x472_bit0 -x473_bit0 -x474_bit0 -x475_bit0 -x476_bit0 -x477_bit0 -x478_bit0 -x479_bit0 -x480_bit0 -x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 -x485_bit0 -x486_bit0 -x487_bit0 -x488_bit0 -x489_bit0 -x490_bit0 -x491_bit0 -x492_bit0 -x493_bit0 -x494_bit0 -x495_bit0 -x496_bit0 -x497_bit0 -x498_bit0 -x499_bit0 -x500_bit0 -x501_bit0 -x502_bit0 -x503_bit0 -x504_bit0 -x505_bit0 -x506_bit0 -x507_bit0 -x508_bit0 -x509_bit0 -x510_bit0 -x511_bit0 -x512_bit0 -x513_bit0 -x514_bit0 x515_bit0 -x516_bit0 -x517_bit0 -x518_bit0 -x519_bit0 -x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 -x524_bit0 -x525_bit0 -x526_bit0 -x527_bit0 -x528_bit0 -x529_bit0 -x530_bit0 -x531_bit0 -x532_bit0 -x533_bit0 -x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 -x540_bit0 -x541_bit0 -x542_bit0 -x543_bit0 -x544_bit0 -x545_bit0 -x546_bit0 -x547_bit0 -x548_bit0 -x549_bit0 -x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 -x556_bit0 -x557_bit0 -x558_bit0 -x559_bit0 -x560_bit0 -x561_bit0 -x562_bit0 -x563_bit0 -x564_bit0 -x565_bit0 -x566_bit0 -x567_bit0 -x568_bit0 -x569_bit0 x570_bit0 -x571_bit0 -x572_bit0 -x573_bit0 -x574_bit0 -x575_bit0 -x576_bit0 -x577_bit0 -x578_bit0 -x579_bit0 -x580_bit0 -x581_bit0 -x582_bit0 -x583_bit0 -x584_bit0 -x585_bit0 -x586_bit0 -x587_bit0 -x588_bit0 -x589_bit0 -x590_bit0 -x591_bit0 -x592_bit0 -x593_bit0 -x594_bit0 -x595_bit0 -x596_bit0 -x597_bit0 -x598_bit0 x599_bit0 -x600_bit0 -x601_bit0 -x602_bit0 -x603_bit0 -x604_bit0 -x605_bit0 -x606_bit0 -x607_bit0 -x608_bit0 -x609_bit0 -x610_bit0 -x611_bit0 -x612_bit0 -x613_bit0 -x614_bit0 -x615_bit0 -x616_bit0 -x617_bit0 -x618_bit0 -x619_bit0 -x620_bit0 -x621_bit0 -x622_bit0 -x623_bit0 -x624_bit0 -x625_bit0 -x626_bit0 -x627_bit0 -x628_bit0 -x629_bit0 -x630_bit0 -x631_bit0 -x632_bit0 -x633_bit0 -x634_bit0 -x635_bit0 -x636_bit0 -x637_bit0 -x638_bit0 -x639_bit0 -x640_bit0 -x641_bit0 -x642_bit0 -x643_bit0 -x644_bit0 -x645_bit0 -x646_bit0 -x647_bit0 -x648_bit0 -x649_bit0 -x650_bit0 -x651_bit0 -x652_bit0 -x653_bit0 -x654_bit0 -x655_bit0 -x656_bit0 -x657_bit0 -x658_bit0 -x659_bit0 -x660_bit0 -x661_bit0 -x662_bit0 -x663_bit0 -x664_bit0 -x665_bit0 -x666_bit0 -x667_bit0 -x668_bit0 x669_bit0 -x670_bit0 -x671_bit0 -x672_bit0 -x673_bit0 -x674_bit0 -x675_bit0 -x676_bit0 -x677_bit0 -x678_bit0 -x679_bit0 -x680_bit0 -x681_bit0 -x682_bit0 -x683_bit0 -x684_bit0 -x685_bit0 -x686_bit0 -x687_bit0 -x688_bit0 -x689_bit0 -x690_bit0 -x691_bit0 -x692_bit0 -x693_bit0 -x694_bit0 -x695_bit0 -x696_bit0 -x697_bit0 -x698_bit0 x699_bit0 -x700_bit0 -x701_bit0 -x702_bit0 -x703_bit0 -x704_bit0 -x705_bit0 -x706_bit0 -x707_bit0 -x708_bit0 -x709_bit0 -x710_bit0 -x711_bit0 -x712_bit0 -x713_bit0 -x714_bit0 -x715_bit0 -x716_bit0 -x717_bit0 -x718_bit0 -x719_bit0 -x720_bit0 -x721_bit0 -x722_bit0 -x723_bit0 -x724_bit0 -x725_bit0 -x726_bit0 -x727_bit0 -x728_bit0 -x729_bit0 -x730_bit0 -x731_bit0 -x732_bit0 -x733_bit0 -x734_bit0 -x735_bit0 -x736_bit0 -x737_bit0 -x738_bit0 -x739_bit0 -x740_bit0 -x741_bit0 -x742_bit0 -x743_bit0 -x744_bit0 -x745_bit0 -x746_bit0 -x747_bit0 -x748_bit0 -x749_bit0 -x750_bit0 -x751_bit0 -x752_bit0 -x753_bit0 -x754_bit0 -x755_bit0 -x756_bit0 -x757_bit0 x758_bit0 -x759_bit0 -x760_bit0 -x761_bit0 -x762_bit0 -x763_bit0 -x764_bit0 -x765_bit0 -x766_bit0 -x767_bit0 -x768_bit0 x769_bit0 -x770_bit0 -x771_bit0 -x772_bit0 -x773_bit0 -x774_bit0 -x775_bit0 -x776_bit0 -x777_bit0 -x778_bit0 -x779_bit0 -x780_bit0 -x781_bit0 -x782_bit0 -x783_bit0 -x784_bit0 -x785_bit0 -x786_bit0 -x787_bit0 -x788_bit0 -x789_bit0 -x790_bit0 -x791_bit0 -x792_bit0 -x793_bit0 -x794_bit0 -x795_bit0 -x796_bit0 -x797_bit0 -x798_bit0 -x799_bit0 -x800_bit0 -x801_bit0 -x802_bit0 -x803_bit0 -x804_bit0 -x805_bit0 -x806_bit0 -x807_bit0 -x808_bit0 -x809_bit0 -x810_bit0 -x811_bit0 -x812_bit0 -x813_bit0 -x814_bit0 -x815_bit0 -x816_bit0 -x817_bit0 -x818_bit0 -x819_bit0 -x820_bit0 -x821_bit0 -x822_bit0 -x823_bit0 -x824_bit0 -x825_bit0 -x826_bit0 -x827_bit0 -x828_bit0 -x829_bit0 -x830_bit0 -x831_bit0 -x832_bit0 -x833_bit0 -x834_bit0 -x835_bit0 -x836_bit0 -x837_bit0 -x838_bit0 -x839_bit0 -x840_bit0 -x841_bit0 -x842_bit0 x843_bit0 -x844_bit0 -x845_bit0 -x846_bit0 -x847_bit0 -x848_bit0 -x849_bit0 -x850_bit0 -x851_bit0 -x852_bit0 -x853_bit0 -x854_bit0 -x855_bit0 -x856_bit0 -x857_bit0 -x858_bit0 -x859_bit0 -x860_bit0 -x861_bit0 -x862_bit0 -x863_bit0 -x864_bit0 -x865_bit0 -x866_bit0 -x867_bit0 -x868_bit0 -x869_bit0 -x870_bit0 -x871_bit0 -x872_bit0 -x873_bit0 -x874_bit0 -x875_bit0 x876_bit0 -x877_bit0 -x878_bit0 -x879_bit0 -x880_bit0 -x881_bit0 -x882_bit0 -x883_bit0 -x884_bit0 -x885_bit0 -x886_bit0 -x887_bit0 -x888_bit0 -x889_bit0 -x890_bit0 -x891_bit0 -x892_bit0 -x893_bit0 -x894_bit0 -x895_bit0 -x896_bit0 -x897_bit0 -x898_bit0 -x899_bit0 -x900_bit0 -x901_bit0 -x902_bit0 -x903_bit0 -x904_bit0 -x905_bit0 -x906_bit0 -x907_bit0 -x908_bit0 -x909_bit0 -x910_bit0 -x911_bit0 -x912_bit0 -x913_bit0 -x914_bit0 -x915_bit0 -x916_bit0 -x917_bit0 -x918_bit0 -x919_bit0 -x920_bit0 -x921_bit0 -x922_bit0 -x923_bit0 -x924_bit0 -x925_bit0 -x926_bit0 -x927_bit0 -x928_bit0 -x929_bit0 -x930_bit0 -x931_bit0 -x932_bit0 -x933_bit0 -x934_bit0 -x935_bit0 -x936_bit0 -x937_bit0 -x938_bit0 -x939_bit0 x940_bit0 -x941_bit0 -x942_bit0 -x943_bit0 -x944_bit0 -x945_bit0 -x946_bit0 -x947_bit0 -x948_bit0 -x949_bit0 -x950_bit0 -x951_bit0 -x952_bit0 -x953_bit0 -x954_bit0 -x955_bit0 -x956_bit0 -x957_bit0 -x958_bit0 -x959_bit0 -x960_bit0 -x961_bit0 -x962_bit0 -x963_bit0 -x964_bit0 -x965_bit0 -x966_bit0 -x967_bit0 -x968_bit0 -x969_bit0 -x970_bit0 -x971_bit0 -x972_bit0 -x973_bit0 x974_bit0 -x975_bit0 -x976_bit0 -x977_bit0 -x978_bit0 -x979_bit0 -x980_bit0 -x981_bit0 -x982_bit0 -x983_bit0 -x984_bit0 -x985_bit0 -x986_bit0 -x987_bit0 -x988_bit0 -x989_bit0 -x990_bit0 -x991_bit0 -x992_bit0 -x993_bit0 -x994_bit0 -x995_bit0 -x996_bit0 -x997_bit0 -x998_bit0 -x999_bit0 -x1000_bit0 -x1001_bit0 -x1002_bit0 -x1003_bit0 -x1004_bit0 -x1005_bit0 -x1006_bit0 x1007_bit0 -x1008_bit0 -x1009_bit0 -x1010_bit0 -x1011_bit0 -x1012_bit0 -x1013_bit0 -x1014_bit0 -x1015_bit0 -x1016_bit0 -x1017_bit0 -x1018_bit0 -x1019_bit0 -x1020_bit0 -x1021_bit0 -x1022_bit0 -x1023_bit0 -x1024_bit0 -x1025_bit0 -x1026_bit0 -x1027_bit0 -x1028_bit0 -x1029_bit0 -x1030_bit0 -x1031_bit0 -x1032_bit0 -x1033_bit0 -x1034_bit0 -x1035_bit0 -x1036_bit0 -x1037_bit0 -x1038_bit0 -x1039_bit0 -x1040_bit0 -x1041_bit0 -x1042_bit0 -x1043_bit0 -x1044_bit0 -x1045_bit0 -x1046_bit0 -x1047_bit0 x1048_bit0 -x1049_bit0 -x1050_bit0 -x1051_bit0 -x1052_bit0 -x1053_bit0 -x1054_bit0 -x1055_bit0 -x1056_bit0 -x1057_bit0 -x1058_bit0 -x1059_bit0 -x1060_bit0 -x1061_bit0 -x1062_bit0 -x1063_bit0 -x1064_bit0 -x1065_bit0 -x1066_bit0 -x1067_bit0 -x1068_bit0 -x1069_bit0 -x1070_bit0 -x1071_bit0 -x1072_bit0 -x1073_bit0 -x1074_bit0 -x1075_bit0 -x1076_bit0 -x1077_bit0 -x1078_bit0 -x1079_bit0 -x1080_bit0 -x1081_bit0 -x1082_bit0 -x1083_bit0 -x1084_bit0 -x1085_bit0 -x1086_bit0 -x1087_bit0 -x1088_bit0 -x1089_bit0 -x1090_bit0 -x1091_bit0 -x1092_bit0 -x1093_bit0 -x1094_bit0 -x1095_bit0 -x1096_bit0 -x1097_bit0 -x1098_bit0 -x1099_bit0 -x1100_bit0 -x1101_bit0 -x1102_bit0 -x1103_bit0 -x1104_bit0 -x1105_bit0 x1106_bit0 -x1107_bit0 -x1108_bit0 -x1109_bit0 -x1110_bit0 -x1111_bit0 -x1112_bit0 -x1113_bit0 -x1114_bit0 -x1115_bit0 -x1116_bit0 -x1117_bit0 -x1118_bit0 -x1119_bit0 -x1120_bit0 -x1121_bit0 -x1122_bit0 -x1123_bit0 -x1124_bit0 -x1125_bit0 -x1126_bit0 -x1127_bit0 -x1128_bit0 -x1129_bit0 -x1130_bit0 -x1131_bit0 -x1132_bit0 -x1133_bit0 -x1134_bit0 -x1135_bit0 -x1136_bit0 -x1137_bit0 -x1138_bit0 -x1139_bit0 -x1140_bit0 -x1141_bit0 -x1142_bit0 -x1143_bit0 -x1144_bit0 -x1145_bit0 -x1146_bit0 -x1147_bit0 -x1148_bit0 -x1149_bit0 -x1150_bit0 -x1151_bit0 -x1152_bit0 -x1153_bit0 -x1154_bit0 -x1155_bit0 -x1156_bit0 -x1157_bit0 -x1158_bit0 -x1159_bit0 -x1160_bit0 -x1161_bit0 -x1162_bit0 -x1163_bit0 -x1164_bit0 -x1165_bit0 x1166_bit0 -x1167_bit0 -x1168_bit0 -x1169_bit0 -x1170_bit0 -x1171_bit0 -x1172_bit0 -x1173_bit0 -x1174_bit0 -x1175_bit0 -x1176_bit0 -x1177_bit0 -x1178_bit0 -x1179_bit0 -x1180_bit0 -x1181_bit0 -x1182_bit0 -x1183_bit0 -x1184_bit0 -x1185_bit0 -x1186_bit0 -x1187_bit0 -x1188_bit0 -x1189_bit0 -x1190_bit0 -x1191_bit0 -x1192_bit0 -x1193_bit0 -x1194_bit0 -x1195_bit0 -x1196_bit0 x1197_bit0 -x1198_bit0 -x1199_bit0 -x1200_bit0 -x1201_bit0 -x1202_bit0 -x1203_bit0 -x1204_bit0 -x1205_bit0 -x1206_bit0 -x1207_bit0 -x1208_bit0 -x1209_bit0 -x1210_bit0 -x1211_bit0 -x1212_bit0 -x1213_bit0 -x1214_bit0 -x1215_bit0 -x1216_bit0 x1217_bit0 -x1218_bit0 -x1219_bit0 -x1220_bit0 -x1221_bit0 -x1222_bit0 -x1223_bit0 -x1224_bit0 -x1225_bit0 -x1226_bit0 -x1227_bit0 -x1228_bit0 -x1229_bit0 -x1230_bit0 -x1231_bit0 -x1232_bit0 -x1233_bit0 -x1234_bit0 -x1235_bit0 -x1236_bit0 -x1237_bit0 -x1238_bit0 -x1239_bit0 -x1240_bit0 -x1241_bit0 -x1242_bit0 -x1243_bit0 -x1244_bit0 -x1245_bit0 -x1246_bit0 -x1247_bit0 -x1248_bit0 -x1249_bit0 -x1250_bit0 -x1251_bit0 -x1252_bit0 -x1253_bit0 -x1254_bit0 -x1255_bit0 -x1256_bit0 -x1257_bit0 -x1258_bit0 -x1259_bit0 -x1260_bit0 -x1261_bit0 -x1262_bit0 -x1263_bit0 -x1264_bit0 -x1265_bit0 -x1266_bit0 -x1267_bit0 -x1268_bit0 -x1269_bit0 -x1270_bit0 -x1271_bit0 -x1272_bit0 -x1273_bit0 -x1274_bit0 -x1275_bit0 -x1276_bit0 -x1277_bit0 -x1278_bit0 -x1279_bit0 -x1280_bit0 -x1281_bit0 -x1282_bit0 -x1283_bit0 -x1284_bit0 -x1285_bit0 -x1286_bit0 -x1287_bit0 -x1288_bit0 -x1289_bit0 -x1290_bit0 -x1291_bit0 -x1292_bit0 -x1293_bit0 -x1294_bit0 x1295_bit0 -x1296_bit0 -x1297_bit0 -x1298_bit0 -x1299_bit0 -x1300_bit0 -x1301_bit0 -x1302_bit0 -x1303_bit0 -x1304_bit0 -x1305_bit0 -x1306_bit0 -x1307_bit0 -x1308_bit0 -x1309_bit0 x1310_bit0 -x1311_bit0 -x1312_bit0 -x1313_bit0 -x1314_bit0 -x1315_bit0 -x1316_bit0 -x1317_bit0 -x1318_bit0 -x1319_bit0 -x1320_bit0 -x1321_bit0 -x1322_bit0 -x1323_bit0 -x1324_bit0 -x1325_bit0 -x1326_bit0 -x1327_bit0 -x1328_bit0 -x1329_bit0 -x1330_bit0 -x1331_bit0 -x1332_bit0 -x1333_bit0 -x1334_bit0 -x1335_bit0 -x1336_bit0 -x1337_bit0 -x1338_bit0 -x1339_bit0 -x1340_bit0 -x1341_bit0 -x1342_bit0 -x1343_bit0 -x1344_bit0 -x1345_bit0 -x1346_bit0 -x1347_bit0 -x1348_bit0 -x1349_bit0 -x1350_bit0 -x1351_bit0 -x1352_bit0 -x1353_bit0 -x1354_bit0 -x1355_bit0 -x1356_bit0 -x1357_bit0 -x1358_bit0 -x1359_bit0 -x1360_bit0 -x1361_bit0 -x1362_bit0 -x1363_bit0 -x1364_bit0 -x1365_bit0 -x1366_bit0 -x1367_bit0 -x1368_bit0 -x1369_bit0 -x1370_bit0 -x1371_bit0 -x1372_bit0 -x1373_bit0 -x1374_bit0 -x1375_bit0 -x1376_bit0 -x1377_bit0 -x1378_bit0 -x1379_bit0 -x1380_bit0 -x1381_bit0 -x1382_bit0 -x1383_bit0 x1384_bit0 -x1385_bit0 -x1386_bit0 -x1387_bit0 -x1388_bit0 -x1389_bit0 -x1390_bit0 -x1391_bit0 -x1392_bit0 -x1393_bit0 -x1394_bit0 -x1395_bit0 -x1396_bit0 -x1397_bit0 -x1398_bit0 -x1399_bit0 -x1400_bit0 -x1401_bit0 -x1402_bit0 -x1403_bit0 -x1404_bit0 -x1405_bit0 -x1406_bit0 -x1407_bit0 -x1408_bit0 -x1409_bit0 -x1410_bit0 -x1411_bit0 -x1412_bit0 -x1413_bit0 -x1414_bit0 -x1415_bit0 -x1416_bit0 -x1417_bit0 -x1418_bit0 -x1419_bit0 x1420_bit0 -x1421_bit0 -x1422_bit0 -x1423_bit0 -x1424_bit0 -x1425_bit0 -x1426_bit0 -x1427_bit0 -x1428_bit0 -x1429_bit0 -x1430_bit0 -x1431_bit0 -x1432_bit0 -x1433_bit0 -x1434_bit0 -x1435_bit0 -x1436_bit0 -x1437_bit0 -x1438_bit0 -x1439_bit0 -x1440_bit0 -x1441_bit0 -x1442_bit0 -x1443_bit0 -x1444_bit0 -x1445_bit0 -x1446_bit0 -x1447_bit0 -x1448_bit0 -x1449_bit0 -x1450_bit0 -x1451_bit0 -x1452_bit0 -x1453_bit0 -x1454_bit0 -x1455_bit0 -x1456_bit0 -x1457_bit0 x1458_bit0 -x1459_bit0 -x1460_bit0 -x1461_bit0 -x1462_bit0 -x1463_bit0 -x1464_bit0 -x1465_bit0 -x1466_bit0 -x1467_bit0 -x1468_bit0 -x1469_bit0 -x1470_bit0 -x1471_bit0 -x1472_bit0 -x1473_bit0 -x1474_bit0 -x1475_bit0 -x1476_bit0 -x1477_bit0 -x1478_bit0 -x1479_bit0 -x1480_bit0 -x1481_bit0 -x1482_bit0 -x1483_bit0 -x1484_bit0 -x1485_bit0 -x1486_bit0 -x1487_bit0 -x1488_bit0 -x1489_bit0 -x1490_bit0 -x1491_bit0 -x1492_bit0 -x1493_bit0 -x1494_bit0 -x1495_bit0 -x1496_bit0 -x1497_bit0 -x1498_bit0 -x1499_bit0 -x1500_bit0 -x1501_bit0 -x1502_bit0 -x1503_bit0 -x1504_bit0 -x1505_bit0 -x1506_bit0 -x1507_bit0 -x1508_bit0 -x1509_bit0 -x1510_bit0 -x1511_bit0 -x1512_bit0 -x1513_bit0 -x1514_bit0 -x1515_bit0 -x1516_bit0 -x1517_bit0 -x1518_bit0 -x1519_bit0 -x1520_bit0 -x1521_bit0 x1522_bit0 -x1523_bit0 -x1524_bit0 -x1525_bit0 -x1526_bit0 -x1527_bit0 -x1528_bit0 -x1529_bit0 -x1530_bit0 -x1531_bit0 -x1532_bit0 -x1533_bit0 -x1534_bit0 -x1535_bit0 -x1536_bit0 -x1537_bit0 x1538_bit0 -x1539_bit0 -x1540_bit0 -x1541_bit0 -x1542_bit0 -x1543_bit0 -x1544_bit0 -x1545_bit0 -x1546_bit0 -x1547_bit0 -x1548_bit0 -x1549_bit0 -x1550_bit0 -x1551_bit0 -x1552_bit0 -x1553_bit0 -x1554_bit0 -x1555_bit0 -x1556_bit0 -x1557_bit0 -x1558_bit0 -x1559_bit0 -x1560_bit0 -x1561_bit0 -x1562_bit0 -x1563_bit0 -x1564_bit0 -x1565_bit0 -x1566_bit0 -x1567_bit0 -x1568_bit0 -x1569_bit0 -x1570_bit0 -x1571_bit0 -x1572_bit0 -x1573_bit0 -x1574_bit0 -x1575_bit0 -x1576_bit0 -x1577_bit0 -x1578_bit0 -x1579_bit0 -x1580_bit0 -x1581_bit0 -x1582_bit0 -x1583_bit0 -x1584_bit0 -x1585_bit0 -x1586_bit0 -x1587_bit0 -x1588_bit0 -x1589_bit0 -x1590_bit0 -x1591_bit0 -x1592_bit0 -x1593_bit0 x1594_bit0 -x1595_bit0 -x1596_bit0 -x1597_bit0 -x1598_bit0 -x1599_bit0 -x1600_bit0 -x1601_bit0 -x1602_bit0 -x1603_bit0 -x1604_bit0 -x1605_bit0 -x1606_bit0 -x1607_bit0 -x1608_bit0 -x1609_bit0 -x1610_bit0 -x1611_bit0 -x1612_bit0 -x1613_bit0 -x1614_bit0 -x1615_bit0 -x1616_bit0 -x1617_bit0 -x1618_bit0 -x1619_bit0 -x1620_bit0 -x1621_bit0 -x1622_bit0 -x1623_bit0 -x1624_bit0 -x1625_bit0 -x1626_bit0 x1627_bit0 -x1628_bit0 -x1629_bit0 -x1630_bit0 -x1631_bit0 -x1632_bit0 -x1633_bit0 -x1634_bit0 -x1635_bit0 -x1636_bit0 -x1637_bit0 -x1638_bit0 -x1639_bit0 -x1640_bit0 -x1641_bit0 -x1642_bit0 -x1643_bit0 -x1644_bit0 -x1645_bit0 -x1646_bit0 -x1647_bit0 -x1648_bit0 -x1649_bit0 -x1650_bit0 -x1651_bit0 -x1652_bit0 -x1653_bit0 -x1654_bit0 -x1655_bit0 -x1656_bit0 -x1657_bit0 -x1658_bit0 -x1659_bit0 -x1660_bit0 -x1661_bit0 -x1662_bit0 -x1663_bit0 -x1664_bit0 -x1665_bit0 -x1666_bit0 -x1667_bit0 -x1668_bit0 -x1669_bit0 -x1670_bit0 -x1671_bit0 -x1672_bit0 -x1673_bit0 -x1674_bit0 -x1675_bit0 -x1676_bit0 -x1677_bit0 -x1678_bit0 -x1679_bit0 -x1680_bit0 -x1681_bit0 -x1682_bit0 -x1683_bit0 -x1684_bit0 -x1685_bit0 -x1686_bit0 -x1687_bit0 -x1688_bit0 -x1689_bit0 -x1690_bit0 -x1691_bit0 -x1692_bit0 -x1693_bit0 -x1694_bit0 -x1695_bit0 -x1696_bit0 -x1697_bit0 -x1698_bit0 -x1699_bit0 -x1700_bit0 -x1701_bit0 -x1702_bit0 -x1703_bit0 -x1704_bit0 -x1705_bit0 -x1706_bit0 x1707_bit0 -x1708_bit0 -x1709_bit0 -x1710_bit0 -x1711_bit0 -x1712_bit0 x1713_bit0 -x1714_bit0 -x1715_bit0 -x1716_bit0 -x1717_bit0 -x1718_bit0 -x1719_bit0 -x1720_bit0 -x1721_bit0 -x1722_bit0 -x1723_bit0 -x1724_bit0 -x1725_bit0 -x1726_bit0 -x1727_bit0 -x1728_bit0 -x1729_bit0 -x1730_bit0 -x1731_bit0 -x1732_bit0 -x1733_bit0 -x1734_bit0 -x1735_bit0 -x1736_bit0 -x1737_bit0 -x1738_bit0 -x1739_bit0 -x1740_bit0 -x1741_bit0 -x1742_bit0 -x1743_bit0 -x1744_bit0 -x1745_bit0 -x1746_bit0 -x1747_bit0 -x1748_bit0 -x1749_bit0 -x1750_bit0 -x1751_bit0 -x1752_bit0 -x1753_bit0 -x1754_bit0 -x1755_bit0 -x1756_bit0 -x1757_bit0 -x1758_bit0 -x1759_bit0 -x1760_bit0 -x1761_bit0 -x1762_bit0 -x1763_bit0 -x1764_bit0 -x1765_bit0 -x1766_bit0 -x1767_bit0 -x1768_bit0 -x1769_bit0 -x1770_bit0 -x1771_bit0 -x1772_bit0 -x1773_bit0 -x1774_bit0 -x1775_bit0 -x1776_bit0 -x1777_bit0 -x1778_bit0 -x1779_bit0 -x1780_bit0 -x1781_bit0 -x1782_bit0 -x1783_bit0 -x1784_bit0 -x1785_bit0 -x1786_bit0 -x1787_bit0 -x1788_bit0 -x1789_bit0 -x1790_bit0 x1791_bit0 -x1792_bit0 -x1793_bit0 -x1794_bit0 -x1795_bit0 -x1796_bit0 -x1797_bit0 -x1798_bit0 -x1799_bit0 -x1800_bit0 -x1801_bit0 -x1802_bit0 -x1803_bit0 -x1804_bit0 -x1805_bit0 -x1806_bit0 -x1807_bit0 -x1808_bit0 -x1809_bit0 -x1810_bit0 -x1811_bit0 x1812_bit0 -x1813_bit0 -x1814_bit0 -x1815_bit0 -x1816_bit0 -x1817_bit0 -x1818_bit0 -x1819_bit0 -x1820_bit0 -x1821_bit0 -x1822_bit0 -x1823_bit0 -x1824_bit0 -x1825_bit0 -x1826_bit0 -x1827_bit0 -x1828_bit0 -x1829_bit0 -x1830_bit0 -x1831_bit0 -x1832_bit0 -x1833_bit0 -x1834_bit0 -x1835_bit0 -x1836_bit0 -x1837_bit0 -x1838_bit0 -x1839_bit0 -x1840_bit0 -x1841_bit0 -x1842_bit0 -x1843_bit0 -x1844_bit0 -x1845_bit0 -x1846_bit0 -x1847_bit0 -x1848_bit0 -x1849_bit0 -x1850_bit0 -x1851_bit0 -x1852_bit0 -x1853_bit0 -x1854_bit0 -x1855_bit0 -x1856_bit0 -x1857_bit0 -x1858_bit0 -x1859_bit0 -x1860_bit0 -x1861_bit0 -x1862_bit0 -x1863_bit0 -x1864_bit0 -x1865_bit0 -x1866_bit0 -x1867_bit0 -x1868_bit0 -x1869_bit0 -x1870_bit0 -x1871_bit0 -x1872_bit0 -x1873_bit0 -x1874_bit0 -x1875_bit0 x1876_bit0 -x1877_bit0 -x1878_bit0 -x1879_bit0 -x1880_bit0 -x1881_bit0 -x1882_bit0 -x1883_bit0 -x1884_bit0 -x1885_bit0 -x1886_bit0 -x1887_bit0 -x1888_bit0 -x1889_bit0 -x1890_bit0 -x1891_bit0 -x1892_bit0 -x1893_bit0 -x1894_bit0 -x1895_bit0 -x1896_bit0 -x1897_bit0 -x1898_bit0 -x1899_bit0 -x1900_bit0 -x1901_bit0 -x1902_bit0 -x#### 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.92 0.95 0.90 2/54 24427
Raw data (stat): 24427 (runsolver) R 24426 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491557820 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99998 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 4568 0 0 0 984 14 0 0 25 0 1 0 491557820 20029440 4189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4189 603 41 0 4849 0
vsize: 19560
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 5664 0 0 0 1981 16 0 0 25 0 1 0 491557820 24506368 5285 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5983 5285 603 41 0 5942 0
vsize: 23932
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 6831 0 0 0 2978 19 0 0 25 0 1 0 491557820 29388800 6452 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7175 6452 603 41 0 7134 0
vsize: 28700
[startup+40.0013 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 8127 0 0 0 3975 22 0 0 25 0 1 0 491557820 34656256 7748 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8461 7748 603 41 0 8420 0
vsize: 33844
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 15825 0 0 0 4955 42 0 0 25 0 1 0 491557820 61100032 13894 4294967295 134512640 134672761 3221224544 3221223184 134622580 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14917 13894 603 41 0 14876 0
vsize: 59668
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 16454 0 0 0 5953 44 0 0 25 0 1 0 491557820 63201280 14408 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15430 14408 603 41 0 15389 0
vsize: 61720
[startup+70.0029 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 16890 0 0 0 6953 45 0 0 25 0 1 0 491557820 65048576 14844 4294967295 134512640 134672761 3221224544 3221223584 134614348 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15881 14844 603 41 0 15840 0
vsize: 63524
[startup+80.0027 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 17647 0 0 0 7951 47 0 0 25 0 1 0 491557820 68087808 15601 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16623 15601 603 41 0 16582 0
vsize: 66492
[startup+90.0038 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 18432 0 0 0 8949 49 0 0 25 0 1 0 491557820 71245824 16386 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17394 16386 603 41 0 17353 0
vsize: 69576
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 20560 0 0 0 9944 54 0 0 25 0 1 0 491557820 74620928 17208 4294967295 134512640 134672761 3221224544 3221222816 134522981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18218 17208 603 41 0 18177 0
vsize: 72872
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 20666 0 0 0 10944 54 0 0 25 0 1 0 491557820 74620928 17210 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18218 17210 603 41 0 18177 0
vsize: 72872
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 21271 0 0 0 11942 56 0 0 25 0 1 0 491557820 76967936 17815 4294967295 134512640 134672761 3221224544 3221223584 134612827 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18791 17815 603 41 0 18750 0
vsize: 75164
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 21901 0 0 0 12941 57 0 0 25 0 1 0 491557820 79593472 18445 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19432 18445 603 41 0 19391 0
vsize: 77728
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 22466 0 0 0 13939 59 0 0 25 0 1 0 491557820 81833984 19010 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19979 19010 603 41 0 19938 0
vsize: 79916
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 23078 0 0 0 14938 61 0 0 25 0 1 0 491557820 84463616 19622 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20621 19622 603 41 0 20580 0
vsize: 82484
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 23697 0 0 0 15937 62 0 0 25 0 1 0 491557820 87085056 20241 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21261 20241 603 41 0 21220 0
vsize: 85044
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 24576 0 0 0 16935 64 0 0 25 0 1 0 491557820 90603520 21120 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22120 21120 603 41 0 22079 0
vsize: 88480
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 25161 0 0 0 17934 65 0 0 25 0 1 0 491557820 93097984 21705 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22729 21705 603 41 0 22688 0
vsize: 90916
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 25829 0 0 0 18932 67 0 0 25 0 1 0 491557820 95735808 22373 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23373 22373 603 41 0 23332 0
vsize: 93492
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 26609 0 0 0 19930 69 0 0 25 0 1 0 491557820 99004416 23153 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24171 23153 603 41 0 24130 0
vsize: 96684
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 27208 0 0 0 20929 71 0 0 25 0 1 0 491557820 101380096 23752 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24751 23752 603 41 0 24710 0
vsize: 99004
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 27811 0 0 0 21928 72 0 0 25 0 1 0 491557820 103882752 24355 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25362 24355 603 41 0 25321 0
vsize: 101448
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 28453 0 0 0 22926 74 0 0 25 0 1 0 491557820 106512384 24997 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26004 24997 603 41 0 25963 0
vsize: 104016
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 29217 0 0 0 23924 76 0 0 25 0 1 0 491557820 109670400 25761 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26775 25761 603 41 0 26734 0
vsize: 107100
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 29814 0 0 0 24923 78 0 0 25 0 1 0 491557820 112037888 26358 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27353 26358 603 41 0 27312 0
vsize: 109412
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 30407 0 0 0 25922 78 0 0 25 0 1 0 491557820 114536448 26951 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27963 26951 603 41 0 27922 0
vsize: 111852
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 30969 0 0 0 26921 80 0 0 25 0 1 0 491557820 116776960 27513 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28510 27513 603 41 0 28469 0
vsize: 114040
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 31805 0 0 0 27920 81 0 0 25 0 1 0 491557820 120156160 28349 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29335 28349 603 41 0 29294 0
vsize: 117340
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 32587 0 0 0 28918 83 0 0 25 0 1 0 491557820 123424768 29131 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30133 29131 603 41 0 30092 0
vsize: 120532
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 33129 0 0 0 29917 85 0 0 25 0 1 0 491557820 125665280 29673 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30680 29673 603 41 0 30639 0
vsize: 122720
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 33710 0 0 0 30915 87 0 0 25 0 1 0 491557820 128028672 30254 4294967295 134512640 134672761 3221224544 3221223728 134615945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31257 30254 603 41 0 31216 0
vsize: 125028
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 34313 0 0 0 31913 89 0 0 25 0 1 0 491557820 130400256 30857 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31836 30857 603 41 0 31795 0
vsize: 127344
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 32908 93 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 33908 93 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 34907 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 35907 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 36906 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 37906 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 38906 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 39906 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 40906 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 41906 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 42907 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 43907 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 44907 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 45907 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 46907 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 47908 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 48908 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 49908 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 50908 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 51908 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 52909 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35626 0 0 0 53909 94 0 0 25 0 1 0 491557820 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 35964 0 0 0 54908 95 0 0 25 0 1 0 491557820 132812800 31415 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32425 31415 603 41 0 32384 0
vsize: 129700
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 36629 0 0 0 55908 96 0 0 25 0 1 0 491557820 135569408 32080 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33098 32080 603 41 0 33057 0
vsize: 132392
[startup+570.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 37403 0 0 0 56907 98 0 0 25 0 1 0 491557820 138719232 32854 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33867 32854 603 41 0 33826 0
vsize: 135468
[startup+580.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 38156 0 0 0 57906 100 0 0 25 0 1 0 491557820 141803520 33607 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34620 33607 603 41 0 34579 0
vsize: 138480
[startup+590.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 39183 0 0 0 58904 102 0 0 25 0 1 0 491557820 146051072 34634 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35657 34634 603 41 0 35616 0
vsize: 142628
[startup+600.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 40222 0 0 0 59902 104 0 0 25 0 1 0 491557820 150278144 35673 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36689 35673 603 41 0 36648 0
vsize: 146756
[startup+610.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 41022 0 0 0 60901 106 0 0 25 0 1 0 491557820 153501696 36473 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37476 36473 603 41 0 37435 0
vsize: 149904
[startup+620.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 41573 0 0 0 61899 108 0 0 25 0 1 0 491557820 155860992 37024 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38052 37024 603 41 0 38011 0
vsize: 152208
[startup+630.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 42277 0 0 0 62898 110 0 0 25 0 1 0 491557820 158748672 37728 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38757 37728 603 41 0 38716 0
vsize: 155028
[startup+640.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 42964 0 0 0 63898 110 0 0 25 0 1 0 491557820 161505280 38415 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39430 38415 603 41 0 39389 0
vsize: 157720
[startup+650.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 43832 0 0 0 64896 112 0 0 25 0 1 0 491557820 165003264 39283 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40284 39283 603 41 0 40243 0
vsize: 161136
[startup+660.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 44822 0 0 0 65894 115 0 0 25 0 1 0 491557820 169127936 40273 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41291 40273 603 41 0 41250 0
vsize: 165164
[startup+670.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 45745 0 0 0 66891 118 0 0 25 0 1 0 491557820 172838912 41196 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42197 41196 603 41 0 42156 0
vsize: 168788
[startup+680.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 46128 0 0 0 67890 119 0 0 25 0 1 0 491557820 174428160 41579 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42585 41579 603 41 0 42544 0
vsize: 170340
[startup+690.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 46657 0 0 0 68889 120 0 0 25 0 1 0 491557820 176668672 42108 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43132 42108 603 41 0 43091 0
vsize: 172528
[startup+700.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 47144 0 0 0 69888 122 0 0 25 0 1 0 491557820 178647040 42595 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43615 42595 603 41 0 43574 0
vsize: 174460
[startup+710.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 47672 0 0 0 70887 123 0 0 25 0 1 0 491557820 180744192 43123 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44127 43123 603 41 0 44086 0
vsize: 176508
[startup+720.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 48115 0 0 0 71886 124 0 0 25 0 1 0 491557820 182849536 43566 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44641 43566 603 41 0 44600 0
vsize: 178564
[startup+730.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 48736 0 0 0 72884 126 0 0 25 0 1 0 491557820 185335808 44187 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45248 44187 603 41 0 45207 0
vsize: 180992
[startup+740.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 49462 0 0 0 73883 128 0 0 25 0 1 0 491557820 188346368 44913 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45983 44913 603 41 0 45942 0
vsize: 183932
[startup+750.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 50129 0 0 0 74881 130 0 0 25 0 1 0 491557820 191074304 45580 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46649 45580 603 41 0 46608 0
vsize: 186596
[startup+760.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 50741 0 0 0 75880 131 0 0 25 0 1 0 491557820 193564672 46192 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47257 46192 603 41 0 47216 0
vsize: 189028
[startup+770.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 51334 0 0 0 76879 133 0 0 25 0 1 0 491557820 196034560 46785 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47860 46785 603 41 0 47819 0
vsize: 191440
[startup+780.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 51886 0 0 0 77878 134 0 0 25 0 1 0 491557820 198283264 47337 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48409 47337 603 41 0 48368 0
vsize: 193636
[startup+790.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 52619 0 0 0 78876 136 0 0 25 0 1 0 491557820 201224192 48070 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49127 48070 603 41 0 49086 0
vsize: 196508
[startup+800.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 53234 0 0 0 79874 138 0 0 25 0 1 0 491557820 203714560 48685 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49735 48685 603 41 0 49694 0
vsize: 198940
[startup+810.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 53902 0 0 0 80873 139 0 0 25 0 1 0 491557820 206471168 49353 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50408 49353 603 41 0 50367 0
vsize: 201632
[startup+820.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 54585 0 0 0 81871 141 0 0 25 0 1 0 491557820 209244160 50036 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51085 50036 603 41 0 51044 0
vsize: 204340
[startup+830.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 55056 0 0 0 82871 142 0 0 25 0 1 0 491557820 211214336 50507 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51566 50507 603 41 0 51525 0
vsize: 206264
[startup+840.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 55552 0 0 0 83870 143 0 0 25 0 1 0 491557820 213196800 51003 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52050 51003 603 41 0 52009 0
vsize: 208200
[startup+850.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 56233 0 0 0 84868 145 0 0 25 0 1 0 491557820 216059904 51684 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52749 51684 603 41 0 52708 0
vsize: 210996
[startup+860.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 56957 0 0 0 85866 147 0 0 25 0 1 0 491557820 218939392 52408 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53452 52408 603 41 0 53411 0
vsize: 213808
[startup+870.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 57641 0 0 0 86865 148 0 0 25 0 1 0 491557820 221822976 53092 4294967295 134512640 134672761 3221224544 3221223696 134614555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54156 53092 603 41 0 54115 0
vsize: 216624
[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 58223 0 0 0 87864 150 0 0 25 0 1 0 491557820 224202752 53674 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54737 53674 603 41 0 54696 0
vsize: 218948
[startup+890.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 58655 0 0 0 88863 151 0 0 25 0 1 0 491557820 225910784 54106 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55154 54106 603 41 0 55113 0
vsize: 220616
[startup+900.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 59144 0 0 0 89861 153 0 0 25 0 1 0 491557820 227876864 54595 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55634 54595 603 41 0 55593 0
vsize: 222536
[startup+910.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 59681 0 0 0 90860 154 0 0 25 0 1 0 491557820 230113280 55132 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56180 55132 603 41 0 56139 0
vsize: 224720
[startup+920.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 60256 0 0 0 91859 155 0 0 25 0 1 0 491557820 232468480 55707 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56755 55707 603 41 0 56714 0
vsize: 227020
[startup+930.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 60824 0 0 0 92858 157 0 0 25 0 1 0 491557820 234835968 56275 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57333 56275 603 41 0 57292 0
vsize: 229332
[startup+940.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 61370 0 0 0 93856 159 0 0 25 0 1 0 491557820 237060096 56821 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57876 56821 603 41 0 57835 0
vsize: 231504
[startup+950.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 62077 0 0 0 94854 161 0 0 25 0 1 0 491557820 239980544 57528 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58589 57528 603 41 0 58548 0
vsize: 234356
[startup+960.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 62687 0 0 0 95853 162 0 0 25 0 1 0 491557820 242483200 58138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59200 58138 603 41 0 59159 0
vsize: 236800
[startup+970.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 63546 0 0 0 96851 164 0 0 25 0 1 0 491557820 245915648 58997 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60038 58997 603 41 0 59997 0
vsize: 240152
[startup+980.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 64230 0 0 0 97850 165 0 0 25 0 1 0 491557820 248676352 59681 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60712 59681 603 41 0 60671 0
vsize: 242848
[startup+990.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 64881 0 0 0 98849 167 0 0 25 0 1 0 491557820 251412480 60332 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61380 60332 603 41 0 61339 0
vsize: 245520
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 65626 0 0 0 99847 169 0 0 25 0 1 0 491557820 254410752 61077 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62112 61077 603 41 0 62071 0
vsize: 248448
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 66322 0 0 0 100846 170 0 0 25 0 1 0 491557820 257241088 61773 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62803 61773 603 41 0 62762 0
vsize: 251212
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 66983 0 0 0 101845 171 0 0 25 0 1 0 491557820 259981312 62434 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63472 62434 603 41 0 63431 0
vsize: 253888
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 67900 0 0 0 102843 174 0 0 25 0 1 0 491557820 263708672 63351 4294967295 134512640 134672761 3221224544 3221223680 134614513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64382 63351 603 41 0 64341 0
vsize: 257528
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 68402 0 0 0 103842 174 0 0 25 0 1 0 491557820 265781248 63853 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64888 63853 603 41 0 64847 0
vsize: 259552
[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 68885 0 0 0 104841 176 0 0 25 0 1 0 491557820 267771904 64336 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65374 64336 603 41 0 65333 0
vsize: 261496
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 69363 0 0 0 105841 176 0 0 25 0 1 0 491557820 269733888 64814 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65853 64814 603 41 0 65812 0
vsize: 263412
[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 69801 0 0 0 106840 177 0 0 25 0 1 0 491557820 271568896 65252 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66301 65252 603 41 0 66260 0
vsize: 265204
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 70273 0 0 0 107839 178 0 0 25 0 1 0 491557820 273420288 65724 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66753 65724 603 41 0 66712 0
vsize: 267012
[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 70702 0 0 0 108838 180 0 0 25 0 1 0 491557820 275263488 66153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67203 66153 603 41 0 67162 0
vsize: 268812
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 71341 0 0 0 109836 182 0 0 25 0 1 0 491557820 277868544 66792 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67839 66792 603 41 0 67798 0
vsize: 271356
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 71973 0 0 0 110835 183 0 0 25 0 1 0 491557820 280461312 67424 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68472 67424 603 41 0 68431 0
vsize: 273888
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 72688 0 0 0 111833 185 0 0 25 0 1 0 491557820 283361280 68139 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69180 68139 603 41 0 69139 0
vsize: 276720
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 73089 0 0 0 112833 186 0 0 25 0 1 0 491557820 284950528 68540 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69568 68540 603 41 0 69527 0
vsize: 278272
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 73730 0 0 0 113831 187 0 0 25 0 1 0 491557820 287571968 69181 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70208 69181 603 41 0 70167 0
vsize: 280832
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 74583 0 0 0 114830 189 0 0 25 0 1 0 491557820 291090432 70034 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71067 70034 603 41 0 71026 0
vsize: 284268
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 75175 0 0 0 115829 190 0 0 25 0 1 0 491557820 293564416 70626 4294967295 134512640 134672761 3221224544 3221223584 134612616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71671 70627 603 41 0 71630 0
vsize: 286684
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 75806 0 0 0 116828 192 0 0 25 0 1 0 491557820 296054784 71257 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72279 71257 603 41 0 72238 0
vsize: 289116
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 76304 0 0 0 117826 193 0 0 25 0 1 0 491557820 298131456 71755 4294967295 134512640 134672761 3221224544 3221223724 134615849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72786 71755 603 41 0 72745 0
vsize: 291144
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 76738 0 0 0 118825 194 0 0 25 0 1 0 491557820 299843584 72189 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73204 72189 603 41 0 73163 0
vsize: 292816
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24427
Raw data (stat): 24427 (minisat+) R 24426 10720 10719 0 -1 0 77171 0 0 0 119824 195 0 0 25 0 1 0 491557820 301678592 72622 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73652 72622 603 41 0 73611 0
vsize: 294608
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.22 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 24427
Raw data (stat): 24427 (minisat+) Z 24426 10720 10719 0 -1 12 77172 0 0 0 119825 209 0 0 25 0 1 0 491557820 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: 10
Real time (s): 1200.22
CPU time (s): 1200.34
CPU user time (s): 1198.25
CPU system time (s): 2.09268
CPU usage (%): 100.011
Max. virtual memory (Kb): 294608
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####