PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-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	920
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.75
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 18875

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        311752 kB
Buffers:         34556 kB
Cached:         659728 kB
SwapCached:        540 kB
Active:         146776 kB
Inactive:       549464 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        311500 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20940 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:17:24 (client local time) WITH STATUS 10 IN 1200.31 SECONDS
stats: 17379 7 1200.31 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: 48.3267 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: 95.3625 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: 101.669 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: 330.679 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.63 0.88 0.88 2/54 29225
Raw data (stat): 29225 (runsolver) R 29224 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546680669 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.0006 s]
Raw data (loadavg): 0.69 0.88 0.88 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 4563 0 0 0 987 11 0 0 25 0 1 0 546680669 20029440 4184 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4184 603 41 0 4849 0
vsize: 19560
[startup+20.0009 s]
Raw data (loadavg): 0.73 0.89 0.88 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 5645 0 0 0 1983 15 0 0 25 0 1 0 546680669 24506368 5266 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5983 5266 603 41 0 5942 0
vsize: 23932
[startup+30.0014 s]
Raw data (loadavg): 0.77 0.89 0.88 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 6772 0 0 0 2979 20 0 0 25 0 1 0 546680669 29126656 6393 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7111 6393 603 41 0 7070 0
vsize: 28444
[startup+40.0014 s]
Raw data (loadavg): 0.81 0.89 0.88 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 8053 0 0 0 3975 23 0 0 25 0 1 0 546680669 34385920 7674 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8395 7674 603 41 0 8354 0
vsize: 33580
[startup+50.0024 s]
Raw data (loadavg): 0.84 0.89 0.89 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 14569 0 0 0 4958 41 0 0 25 0 1 0 546680669 56324096 12638 4294967295 134512640 134672761 3221224544 3221223728 134593694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13751 12638 603 41 0 13710 0
vsize: 55004
[startup+60.0022 s]
Raw data (loadavg): 0.86 0.90 0.89 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 16377 0 0 0 5954 45 0 0 25 0 1 0 546680669 62939136 14331 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15366 14331 603 41 0 15325 0
vsize: 61464
[startup+70.0021 s]
Raw data (loadavg): 0.88 0.90 0.89 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 16793 0 0 0 6953 46 0 0 25 0 1 0 546680669 64655360 14747 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15785 14747 603 41 0 15744 0
vsize: 63140
[startup+80.0035 s]
Raw data (loadavg): 0.90 0.90 0.89 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 17529 0 0 0 7951 48 0 0 25 0 1 0 546680669 67555328 15483 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16493 15483 603 41 0 16452 0
vsize: 65972
[startup+90.003 s]
Raw data (loadavg): 0.92 0.91 0.89 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 18211 0 0 0 8948 50 0 0 25 0 1 0 546680669 70455296 16165 4294967295 134512640 134672761 3221224544 3221223744 134610614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17201 16165 603 41 0 17160 0
vsize: 68804
[startup+100.004 s]
Raw data (loadavg): 0.93 0.91 0.89 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 19714 0 0 0 9944 55 0 0 25 0 1 0 546680669 72970240 16840 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17815 16840 603 41 0 17774 0
vsize: 71260
[startup+110.005 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 20665 0 0 0 10941 58 0 0 25 0 1 0 546680669 74620928 17209 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18218 17209 603 41 0 18177 0
vsize: 72872
[startup+120.005 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 21007 0 0 0 11940 59 0 0 25 0 1 0 546680669 75935744 17551 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18539 17551 603 41 0 18498 0
vsize: 74156
[startup+130.005 s]
Raw data (loadavg): 0.95 0.92 0.89 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 21633 0 0 0 12938 61 0 0 25 0 1 0 546680669 78544896 18177 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19176 18177 603 41 0 19135 0
vsize: 76704
[startup+140.006 s]
Raw data (loadavg): 0.96 0.92 0.89 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 22273 0 0 0 13936 63 0 0 25 0 1 0 546680669 81043456 18817 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19786 18817 603 41 0 19745 0
vsize: 79144
[startup+150.007 s]
Raw data (loadavg): 0.97 0.92 0.89 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 22845 0 0 0 14935 65 0 0 25 0 1 0 546680669 83415040 19389 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20365 19389 603 41 0 20324 0
vsize: 81460
[startup+160.007 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 29225
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 23400 0 0 0 15933 66 0 0 25 0 1 0 546680669 85905408 19944 4294967295 134512640 134672761 3221224544 3221223680 134614576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20973 19944 603 41 0 20932 0
vsize: 83892
[startup+170.006 s]
Raw data (loadavg): 1.20 0.97 0.91 2/54 29278
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 24231 0 0 0 16926 73 0 0 25 0 1 0 546680669 89174016 20775 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21771 20775 603 41 0 21730 0
vsize: 87084
[startup+180.006 s]
Raw data (loadavg): 1.17 0.97 0.91 2/54 29278
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 24941 0 0 0 17923 76 0 0 25 0 1 0 546680669 92168192 21485 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22502 21485 603 41 0 22461 0
vsize: 90008
[startup+190.006 s]
Raw data (loadavg): 1.14 0.97 0.91 2/54 29278
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 25420 0 0 0 18922 77 0 0 25 0 1 0 546680669 94142464 21964 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22984 21964 603 41 0 22943 0
vsize: 91936
[startup+200.007 s]
Raw data (loadavg): 1.12 0.97 0.91 2/54 29278
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 26093 0 0 0 19920 79 0 0 25 0 1 0 546680669 96796672 22637 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23632 22637 603 41 0 23591 0
vsize: 94528
[startup+210.008 s]
Raw data (loadavg): 1.10 0.97 0.91 2/54 29278
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 26887 0 0 0 20918 82 0 0 25 0 1 0 546680669 100048896 23431 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24426 23431 603 41 0 24385 0
vsize: 97704
[startup+220.008 s]
Raw data (loadavg): 1.08 0.97 0.91 2/54 29278
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 27408 0 0 0 21916 84 0 0 25 0 1 0 546680669 102174720 23952 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24945 23952 603 41 0 24904 0
vsize: 99780
[startup+230.008 s]
Raw data (loadavg): 1.07 0.97 0.91 2/54 29278
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 28024 0 0 0 22915 85 0 0 25 0 1 0 546680669 104804352 24568 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25587 24568 603 41 0 25546 0
vsize: 102348
[startup+240.008 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 28692 0 0 0 23912 88 0 0 25 0 1 0 546680669 107425792 25236 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26227 25236 603 41 0 26186 0
vsize: 104908
[startup+250.009 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 29451 0 0 0 24909 91 0 0 25 0 1 0 546680669 110583808 25995 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26998 25995 603 41 0 26957 0
vsize: 107992
[startup+260.009 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 29966 0 0 0 25908 92 0 0 25 0 1 0 546680669 112701440 26510 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27515 26510 603 41 0 27474 0
vsize: 110060
[startup+270.009 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 30538 0 0 0 26906 94 0 0 25 0 1 0 546680669 115060736 27082 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28091 27082 603 41 0 28050 0
vsize: 112364
[startup+280.01 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 31095 0 0 0 27905 96 0 0 25 0 1 0 546680669 117301248 27639 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28638 27639 603 41 0 28597 0
vsize: 114552
[startup+290.01 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 32023 0 0 0 28903 98 0 0 25 0 1 0 546680669 121057280 28567 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29555 28567 603 41 0 29514 0
vsize: 118220
[startup+300.01 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 32668 0 0 0 29901 100 0 0 25 0 1 0 546680669 123686912 29212 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30197 29212 603 41 0 30156 0
vsize: 120788
[startup+310.01 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 33172 0 0 0 30899 102 0 0 25 0 1 0 546680669 125796352 29716 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30712 29716 603 41 0 30671 0
vsize: 122848
[startup+320.01 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 33752 0 0 0 31898 104 0 0 25 0 1 0 546680669 128155648 30296 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31288 30296 603 41 0 31247 0
vsize: 125152
[startup+330.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 34318 0 0 0 32896 105 0 0 25 0 1 0 546680669 130531328 30862 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31868 30862 603 41 0 31827 0
vsize: 127472
[startup+340.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 33894 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+350.012 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 34893 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+360.013 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 35893 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+370.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 36893 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615940 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.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 37894 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+390.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 38894 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+400.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 39894 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+410.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 40894 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+420.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 41894 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+430.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 42894 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+440.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 43894 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+450.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 44895 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+460.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 45895 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+470.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29280
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 46895 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+480.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 47895 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+490.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 48895 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+500.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 49896 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223680 134614503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+510.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 50896 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+520.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 51896 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+530.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 52896 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+540.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 53896 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+550.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 54896 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+560.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 35626 0 0 0 55896 108 0 0 25 0 1 0 546680669 131387392 31077 4294967295 134512640 134672761 3221224544 3221223728 134615554 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32077 31077 603 41 0 32036 0
vsize: 128308
[startup+570.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 36123 0 0 0 56895 110 0 0 25 0 1 0 546680669 133464064 31574 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32584 31574 603 41 0 32543 0
vsize: 130336
[startup+580.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 36870 0 0 0 57894 111 0 0 25 0 1 0 546680669 136609792 32321 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33352 32321 603 41 0 33311 0
vsize: 133408
[startup+590.02 s]
Raw data (loadavg): 1.15 1.01 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 37551 0 0 0 58892 113 0 0 25 0 1 0 546680669 139378688 33002 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34028 33002 603 41 0 33987 0
vsize: 136112
[startup+600.02 s]
Raw data (loadavg): 1.13 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 38307 0 0 0 59890 115 0 0 25 0 1 0 546680669 142438400 33758 4294967295 134512640 134672761 3221224544 3221223728 134615755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34775 33758 603 41 0 34734 0
vsize: 139100
[startup+610.02 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 39245 0 0 0 60888 117 0 0 25 0 1 0 546680669 146300928 34696 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35718 34696 603 41 0 35677 0
vsize: 142872
[startup+620.02 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 40263 0 0 0 61885 120 0 0 25 0 1 0 546680669 150405120 35714 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36720 35714 603 41 0 36679 0
vsize: 146880
[startup+630.021 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 41020 0 0 0 62883 123 0 0 25 0 1 0 546680669 153501696 36471 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37476 36471 603 41 0 37435 0
vsize: 149904
[startup+640.02 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 41546 0 0 0 63882 124 0 0 25 0 1 0 546680669 155729920 36997 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38020 36997 603 41 0 37979 0
vsize: 152080
[startup+650.021 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 42222 0 0 0 64880 126 0 0 25 0 1 0 546680669 158486528 37673 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38693 37673 603 41 0 38652 0
vsize: 154772
[startup+660.022 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 42899 0 0 0 65878 128 0 0 25 0 1 0 546680669 161243136 38350 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39366 38350 603 41 0 39325 0
vsize: 157464
[startup+670.021 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 43669 0 0 0 66877 130 0 0 25 0 1 0 546680669 164356096 39120 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40126 39120 603 41 0 40085 0
vsize: 160504
[startup+680.021 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 44712 0 0 0 67874 133 0 0 25 0 1 0 546680669 168595456 40163 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41161 40163 603 41 0 41120 0
vsize: 164644
[startup+690.021 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 45597 0 0 0 68872 135 0 0 25 0 1 0 546680669 172318720 41048 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42070 41048 603 41 0 42029 0
vsize: 168280
[startup+700.022 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 46004 0 0 0 69871 136 0 0 25 0 1 0 546680669 173891584 41455 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42454 41455 603 41 0 42413 0
vsize: 169816
[startup+710.022 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 46500 0 0 0 70870 137 0 0 25 0 1 0 546680669 176009216 41951 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42971 41951 603 41 0 42930 0
vsize: 171884
[startup+720.022 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 46955 0 0 0 71869 138 0 0 25 0 1 0 546680669 177852416 42406 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43421 42406 603 41 0 43380 0
vsize: 173684
[startup+730.023 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 47460 0 0 0 72868 140 0 0 25 0 1 0 546680669 179830784 42911 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43904 42911 603 41 0 43863 0
vsize: 175616
[startup+740.023 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 47938 0 0 0 73867 141 0 0 25 0 1 0 546680669 182050816 43389 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44446 43389 603 41 0 44405 0
vsize: 177784
[startup+750.024 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 48480 0 0 0 74866 143 0 0 25 0 1 0 546680669 184291328 43931 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44993 43931 603 41 0 44952 0
vsize: 179972
[startup+760.023 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 48994 0 0 0 75864 144 0 0 25 0 1 0 546680669 186384384 44445 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45504 44445 603 41 0 45463 0
vsize: 182016
[startup+770.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 49826 0 0 0 76862 146 0 0 25 0 1 0 546680669 189882368 45277 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46358 45277 603 41 0 46317 0
vsize: 185432
[startup+780.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 50386 0 0 0 77860 148 0 0 25 0 1 0 546680669 192118784 45837 4294967295 134512640 134672761 3221224544 3221223728 134615951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46904 45837 603 41 0 46863 0
vsize: 187616
[startup+790.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 50931 0 0 0 78859 149 0 0 25 0 1 0 546680669 194347008 46382 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47448 46382 603 41 0 47407 0
vsize: 189792
[startup+800.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 51552 0 0 0 79857 152 0 0 25 0 1 0 546680669 196825088 47003 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48053 47003 603 41 0 48012 0
vsize: 192212
[startup+810.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 52030 0 0 0 80856 154 0 0 25 0 1 0 546680669 198799360 47481 4294967295 134512640 134672761 3221224544 3221223728 134616011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48535 47481 603 41 0 48494 0
vsize: 194140
[startup+820.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 52725 0 0 0 81854 155 0 0 25 0 1 0 546680669 201629696 48176 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49226 48176 603 41 0 49185 0
vsize: 196904
[startup+830.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 53340 0 0 0 82852 157 0 0 25 0 1 0 546680669 204230656 48791 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49861 48791 603 41 0 49820 0
vsize: 199444
[startup+840.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 53982 0 0 0 83851 159 0 0 25 0 1 0 546680669 206860288 49433 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50503 49433 603 41 0 50462 0
vsize: 202012
[startup+850.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 54621 0 0 0 84849 161 0 0 25 0 1 0 546680669 209379328 50072 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51118 50072 603 41 0 51077 0
vsize: 204472
[startup+860.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 55060 0 0 0 85848 162 0 0 25 0 1 0 546680669 211214336 50511 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51566 50511 603 41 0 51525 0
vsize: 206264
[startup+870.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 55534 0 0 0 86847 163 0 0 25 0 1 0 546680669 213196800 50985 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52050 50985 603 41 0 52009 0
vsize: 208200
[startup+880.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 56177 0 0 0 87846 165 0 0 25 0 1 0 546680669 215801856 51628 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52686 51628 603 41 0 52645 0
vsize: 210744
[startup+890.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 56867 0 0 0 88844 167 0 0 25 0 1 0 546680669 218677248 52318 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53388 52318 603 41 0 53347 0
vsize: 213552
[startup+900.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 57539 0 0 0 89843 168 0 0 25 0 1 0 546680669 221425664 52990 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54059 52990 603 41 0 54018 0
vsize: 216236
[startup+910.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 58097 0 0 0 90841 170 0 0 25 0 1 0 546680669 223666176 53548 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54606 53548 603 41 0 54565 0
vsize: 218424
[startup+920.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 58564 0 0 0 91841 171 0 0 25 0 1 0 546680669 225517568 54015 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55058 54015 603 41 0 55017 0
vsize: 220232
[startup+930.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 59008 0 0 0 92839 172 0 0 25 0 1 0 546680669 227356672 54459 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55507 54459 603 41 0 55466 0
vsize: 222028
[startup+940.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 59495 0 0 0 93838 173 0 0 25 0 1 0 546680669 229322752 54946 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55987 54946 603 41 0 55946 0
vsize: 223948
[startup+950.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 60012 0 0 0 94838 174 0 0 25 0 1 0 546680669 231428096 55463 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56501 55463 603 41 0 56460 0
vsize: 226004
[startup+960.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 60583 0 0 0 95836 176 0 0 25 0 1 0 546680669 233791488 56034 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57078 56034 603 41 0 57037 0
vsize: 228312
[startup+970.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 61087 0 0 0 96835 177 0 0 25 0 1 0 546680669 235876352 56538 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57587 56538 603 41 0 57546 0
vsize: 230348
[startup+980.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 61712 0 0 0 97834 179 0 0 25 0 1 0 546680669 238383104 57163 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58199 57163 603 41 0 58158 0
vsize: 232796
[startup+990.029 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 62343 0 0 0 98832 180 0 0 25 0 1 0 546680669 241037312 57794 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58847 57794 603 41 0 58806 0
vsize: 235388
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 62991 0 0 0 99832 181 0 0 25 0 1 0 546680669 243646464 58442 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59484 58442 603 41 0 59443 0
vsize: 237936
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 63862 0 0 0 100830 183 0 0 25 0 1 0 546680669 247226368 59313 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60358 59313 603 41 0 60317 0
vsize: 241432
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 64388 0 0 0 101829 184 0 0 25 0 1 0 546680669 249335808 59839 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60873 59839 603 41 0 60832 0
vsize: 243492
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 65053 0 0 0 102828 186 0 0 25 0 1 0 546680669 252076032 60504 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61542 60504 603 41 0 61501 0
vsize: 246168
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 65806 0 0 0 103827 186 0 0 25 0 1 0 546680669 255176704 61257 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62299 61257 603 41 0 62258 0
vsize: 249196
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 66401 0 0 0 104827 187 0 0 25 0 1 0 546680669 257634304 61852 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62899 61853 603 41 0 62858 0
vsize: 251596
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 67120 0 0 0 105826 188 0 0 25 0 1 0 546680669 260624384 62571 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63629 62571 603 41 0 63588 0
vsize: 254516
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 67958 0 0 0 106823 191 0 0 25 0 1 0 546680669 263962624 63409 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64444 63409 603 41 0 64403 0
vsize: 257776
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 68415 0 0 0 107822 192 0 0 25 0 1 0 546680669 265916416 63866 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64921 63866 603 41 0 64880 0
vsize: 259684
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 68894 0 0 0 108821 193 0 0 25 0 1 0 546680669 267771904 64345 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65374 64345 603 41 0 65333 0
vsize: 261496
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 69356 0 0 0 109820 195 0 0 25 0 1 0 546680669 269733888 64807 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65853 64807 603 41 0 65812 0
vsize: 263412
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 69764 0 0 0 110819 196 0 0 25 0 1 0 546680669 271310848 65215 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66238 65215 603 41 0 66197 0
vsize: 264952
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 70189 0 0 0 111818 197 0 0 25 0 1 0 546680669 273149952 65640 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66687 65640 603 41 0 66646 0
vsize: 266748
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 70648 0 0 0 112817 199 0 0 25 0 1 0 546680669 275001344 66099 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67139 66099 603 41 0 67098 0
vsize: 268556
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 71177 0 0 0 113814 201 0 0 25 0 1 0 546680669 277094400 66628 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67650 66628 603 41 0 67609 0
vsize: 270600
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 71820 0 0 0 114813 203 0 0 25 0 1 0 546680669 279810048 67271 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68313 67271 603 41 0 68272 0
vsize: 273252
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 72466 0 0 0 115811 205 0 0 25 0 1 0 546680669 282427392 67917 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68952 67917 603 41 0 68911 0
vsize: 275808
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 72939 0 0 0 116810 206 0 0 25 0 1 0 546680669 284295168 68390 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69408 68390 603 41 0 69367 0
vsize: 277632
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 73447 0 0 0 117808 208 0 0 25 0 1 0 546680669 286400512 68898 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69922 68898 603 41 0 69881 0
vsize: 279688
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 74198 0 0 0 118806 210 0 0 25 0 1 0 546680669 289550336 69649 4294967295 134512640 134672761 3221224544 3221223584 134614274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70691 69649 603 41 0 70650 0
vsize: 282764
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29282
Raw data (stat): 29225 (minisat+) R 29224 23176 23175 0 -1 0 74954 0 0 0 119805 211 0 0 25 0 1 0 546680669 292646912 70405 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71447 70405 603 41 0 71406 0
vsize: 285788
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 29282
Raw data (stat): 29225 (minisat+) Z 29224 23176 23175 0 -1 12 74955 0 0 0 119805 225 0 0 25 0 1 0 546680669 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.18
CPU time (s): 1200.31
CPU user time (s): 1198.06
CPU system time (s): 2.25166
CPU usage (%): 100.011
Max. virtual memory (Kb): 285788
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####