~ubuntu-branches/ubuntu/precise/spass/precise : revision 5

1

@setfilename SPASS.info

2

@settitle automated theorem prover for full first-order logic with equality

3

4

@page

5

@node SPASS, checkstat, Top, Top

6

@comment node-name, next, previous, up

7

@chapter SPASS

8

@cindex SPASS

9

@cindex SPASS options

10

11

@section NAME

12

@noindent

13

SPASS - an automated theorem prover for full first-order logic with equality

14

15

@section SYNOPSIS

16

@noindent

17

@c man begin SYNOPSIS

18

SPASS [@option{options}] [@var{inputfile}]

19

@c man end

20

21

@section DESCRIPTION

22

@noindent

23

@c man begin DESCRIPTION

24

SPASS is an automated theorem prover for full sorted first-order logic with equality

25

that extends superposition by sorts and a splitting rule for case analysis.

26

SPASS can also be used as a modal logic and description logic theorem prover.

27

@c man end

28

29

@section OPTIONS

30

@noindent

31

@c man begin OPTIONS

32

Command line options in SPASS are implemented via modifications to the GNU command

33

line option package for C. Just giving the option sets its value to 1 and means enabling

34

the option. In order to disable

35

an option the value has to be set to 0 by declaring -@i{Option}=0.

36

The following options are currently supported by SPASS:

37

38

@table @kbd

39

@item -Auto

40

@*Enables/disables the auto mode where SPASS configures itself automatically.

41

The inference/reduction rules, the sort technology, the ordering and precedence

42

as well as the splitting and selection strategy are set.

43

In auto mode SPASS is complete. Mixing the auto mode with user defined options

44

may destroy completeness.

45

Default is 1.

46

@item -Stdin

47

Enables/disables input in SPASS via stdin. The file argument is ignored. Default is 0.

48

@item -Interactive

49

Enables/disables the interactive mode. First, SPASS is given a set of axioms and then

50

the prover accepts subsequent proof tasks. Default is 0.

51

@item -Flotter

52

Enables/disables the CNF translation mode of SPASS. If the option is set, SPASS only

53

performs a clause normal form translation. If no output file argument is given

54

SPASS prints the CNF to stdout. Default is 0.

55

@item -SOS

56

Enables/disables the set of support strategy. Default is 0.

57

@item -Splits=@i{n}

58

Sets the number of possible splitting applications to @i{n}. If @i{n}=-1 then

59

the number of splits is not limited. Default is 0.

60

@item -Memory=@i{n}

61

Sets the amount of memory available to SPASS for the proof search to @i{n} bytes.

62

The memory needed to startup SPASS cannot be restricted.

63

Default is -1 meaning that memory allocations is only restricted by available memory.

64

@item -TimeLimit=@i{n}

65

Sets a time limit for the proof search to @i{n} seconds. Default is -1 meaning that

66

SPASS may run forever. The time limit is polled when SPASS selects a new clause for

67

inferences. If a single inference step causes an explosion to the number of generated

68

clauses it may therefore happen that a given time limit is significantly exceeded.

69

@item -DocSST

70

Enables/disables documentation output for static soft typing.

71

The used sort theory as well as the (failed) proof attempt for

72

the sort constraint is printed.

73

Default is 0.

74

@item -DocProof

75

Enables/disables proof documentation. If SPASS finds a proof it is eventually

76

printed. If SPASS finds a saturation, the saturated set of clauses is eventually printed.

77

Enabling proof documentation may significantly decrease SPASS's performance, because

78

the prover must store clauses that can be thrown away otherwise. Default is 0.

79

@item -DocSplit

80

Sets the documentation of split backtracking steps. If set to 1, the

81

current backtracking level is printed. If set to 2, it also prints in case

82

of a split backtrack the backtracked clauese.

83

Default is 0.

84

@item -Loops

85

Sets the maximal number of mainloop iterations for SPASS.

86

Default is -1.

87

@item -PSub

88

Enables/disables printing of subsumed clauses.

89

Default is 0.

90

@item -PRew

91

Enables/disables printing of simple rewrite applications.

92

Default is 0.

93

@item -PCon

94

Enables/disables printing of condensation applications.

95

Default is 0.

96

@item -PTaut

97

Enables/disables printing of tautology deletion applications.

98

Default is 0.

99

@item -PObv

100

Enables/disables printing of obvious reduction applications.

101

Default is 0.

102

@item -PSSi

103

Enables/disables printing of sort simplification applications.

104

Default is 0.

105

@item -PSST

106

Enables/disables printing of static soft typing applications.

107

All deleted clauses are printed.

108

Default is 0.

109

@item -PMRR

110

Enables/disables printing of matching replacement resolution applications.

111

Default is 0.

112

@item -PUnC

113

Enables/disables printing of unit conflict applications.

114

Default is 0.

115

@item -PAED

116

Enables/disables printing of clauses where redundant

117

equations have been removed (assignment equation deletion).

118

@item -PDer

119

Enables/disables printing of clauses derived by inferences.

120

Default is 0.

121

@item -PGiven

122

Enables/disables printing of the given clause, selected

123

to perform inferences.

124

Default is 0.

125

@item -PLabels

126

Enables/disables printing of labels. If the -DocProof is

127

set and no labels for formulae are provided by the input,

128

SPASS generates generic labels that are then printed by enabling this option.

129

Default is 0.

130

@item -PKept

131

Enables/disables printing of kept clauses. These are clauses

132

generated by inferences (backtracking) that are not redundant.

133

Clauses derived during input reduction/saturation are not printed.

134

Default is 0.

135

@item -PProblem

136

Enables/disables printing of the input clause set.

137

Default is 1.

138

@item -PEmptyClause

139

Enables/disables printing of derived empty clauses.

140

Default is 0.

141

@item -PStatistic

142

Enables/disables printing of a final statistics on derived/backtracked/kept clauses, performed splits,

143

used time and used space.

144

Default is 1.

145

@item -FPModel

146

Enables/disables the output of an eventually found model to a file. If set

147

to 1, all clauses in the final set are printed. If set to 2, only

148

potentially productive clauses are printed, that are clauses with no selected

149

negative literal and a maximal positive one. If <problemfile> is the name

150

of the input problem and the eventually generated set is saturated, the

151

saturation is printed to the file <problemfile>.model, for otherwise

152

to <problemfile>.clauses. The latter case may, e.g., be caused by a time limit.

153

Default is 0.

154

@item -FPDFGProof

155

Enables/disables the output of an eventually found proof to a file. Using this

156

option requires to set the option -DocProof. If <problemfile> is the name

157

of the input problem the proof is printed to <problemfile>.prf.

158

Default is 0.

159

@item -PFlags

160

Enables/disables the output of all flag values. The flag settings are

161

printed at the end of a SPASS run in form of a DFG-Syntax input section.

162

Default is 0.

163

@item -POptSkolem

164

Enables/disables the output of optimized Skolemization applications.

165

Default is 0.

166

@item -PStrSkolem

167

Enables/disables the output of strong Skolemization applications.

168

Default is 0.

169

@item -PBDC

170

Enables/disables the output of clauses deleted because of

171

bound restrictions.

172

Default is 0.

173

@item -PBInc

174

Enables/disables the output of bound restriction changes.

175

Default is 0.

176

@item -PApplyDefs

177

Enables/disables printing of expansions of atom definitions.

178

Default is 0.

179

@item -Select

180

Sets the selection strategy for SPASS. If set to 0 no selection

181

of negative literals is done. If set to any other value, at most

182

one negative literal in a clause is selected. If set to 1 negative

183

literals in clauses with more than one maximal literal are selected.

184

Either a negative literal with a predicate from the selection list (see below) is chosen

185

or if no such negative literal is available, a negative literal with maximal weight is chosen.

186

If set to 2 negative literals are always selected. Again,

187

either a negative literal with a predicate from the selection list (see below) is chosen

188

or if no such negative literal is available, a negative literal with maximal weight is chosen.

189

The latter case results

190

in an ordered hyperresolution like behavior of ordered resolution.

191

If set to 3 any negative literal with a predicate specified by the selection list (see below)

192

is selected.

193

Default is 1.

194

@item -RInput

195

Enables/disables the reduction of the initial clause set.

196

Default is 1.

197

@item -Sorts

198

Determines the monadic literals that built the sort constraint

199

for the initial clause set.

200

If set to 0, no sort constraint is built. If set to 1, all negative

201

monadic literals with a variable as argument form the sort constraint.

202

If set to 2, all negative monadic literals form the sort constraint.

203

Setting -Sorts to 2 may harm completeness, since sort constraints are

204

subject to the basic strategy and to static soft typing.

205

Default is 1.

206

@item -SatInput

207

Enables/disables input saturation. The saturation is incomplete

208

but is guaranteed to terminate.

209

Default is 0.

210

@item -WDRatio

211

Sets the ratio between given clauses selected by

212

weight or the depth in the search space. The weight is the

213

sum of all symbol weights determined by the -FuncWeight and

214

-VarWeight options. The depth of all initial clauses is 0 and

215

clauses generated by inferences get the maximal depth of a parent

216

clause plus 1.

217

Default is 5, meaning

218

that 4 clauses are selected by weight and the fifth clause is

219

selected by depth.

220

@item -PrefCon

221

Sets the ratio to compute the weight for conjecture clauses

222

and therefore allows to prefer those. Default is 0 meaning that

223

the weight computation for conjecture clauses is not changed.

224

@item -FullRed

225

Enables/disables full reduction. If set to 0, only the set of worked

226

off clauses is completely inter-reduced. If set to 1, all currently

227

hold clauses (worked off and usable) are completely inter-reduced.

228

Default is 1.

229

@item -FuncWeight

230

Sets the weight of function/predicate symbols. The weight of

231

clauses is the sum of all symbol weights. This weight is considered

232

for the selection of the given clause. Default is 1.

233

@item -VarWeight

234

Sets the weight of variable symbols (see -FuncWeight).

235

Default is 1.

236

@item -PrefVar

237

Enables/disables the preference for clauses with many variables.

238

While clauses are selected by weight, if this option is set and

239

two clauses have the same weight, the clause with more variable

240

occurrences is preferred.

241

Default is 0.

242

@item -BoundMode

243

Selects the mode for bound restrictions. Mode 0 means no

244

restriction, if set to 1 all newly generated clauses are restricted by weight

245

(see -BoundStart) and if set to 2 clauses are restricted

246

by depth. Default is 0.

247

@item -BoundStart

248

The start restriction of the selected bound mode. For example,

249

if bound mode is 1 and bound start set to 5, all clauses with

250

a weight larger than 5 are deleted until the set is saturated.

251

This causes an increase of the used bound value that is

252

determined by the minimal increase saving a before deleted

253

clause. Default is -1 meaning no bound restriction.

254

@item -BoundLoops

255

The number of loops applying the actions restrictions/increasing bound.

256

If the number of loops is exceeded all bound restrictions are

257

cancelled. Default is 1.

258

@item -ApplyDefs

259

Sets the maximal number of applications of atom definitions to input formulae.

260

Default is 0, meaning no applications at all.

261

@item -Ordering

262

Sets the term ordering. If 0 then KBO is selected,

263

if 1 the RPOS is selected. Default is 0.

264

@item -CNFQuantExch

265

If set, non-constant Skolem terms in the clausal form of the

266

conjecture are replaced by constants.

267

Will automatically be set for the optimized functional translation of

268

modal or description logic formulae.

269

Default is 0.

270

@item -CNFOptSkolem

271

Enables/disables optimized Skolemization.

272

Default is 1.

273

@item -CNFStrSkolem

274

Enables/disables Strong Skolemization.

275

Default is 1.

276

@item -CNFProofSteps

277

Sets the maximal number of proof steps

278

in an optimized Skolemization proof attempt.

279

Default is 100.

280

@item -CNFSub

281

Enables/disables subsumption on the clauses generated by the CNF procedure.

282

Default is 1.

283

@item -CNFCon

284

Enables/disables condensing on the clauses generated by the CNF procedure.

285

Default is 1.

286

@item -CNFRedTime

287

Sets the overall amount of time in seconds to be spend on reduction during

288

CNF transformation. Affected reductions are optimized Skolemization, condensing,

289

and subsumption. Default is -1 meaning that the reduction time is not limited

290

at all.

291

@item -CNFRenaming

292

Enables/disables formula renaming.

293

If set to 1 optimized renaming is enabled that minimizes

294

the number of eventually generated clauses.

295

If set to 2 complex renaming is enabled that introduces a

296

new Skolem predicate for every complex formula, i.e., any

297

formula that is not a literal.

298

If set to 3 quantification renaming is enabled that introduces

299

a new Skolem predicate for every subformula starting with

300

a quantifier.

301

Default is 1.

302

@item -CNFRenMatch

303

If set, renaming variant subformulae are replaced by the same

304

Skolem literal.

305

Default is 1.

306

@item -CNFPRenaming

307

Enables/disables the printing of formula renaming applications.

308

Default is 0.

309

@item -CNFFEqR

310

Enables/disables certain equality reduction techniques

311

on the formula level. Default is 1.

312

@item -IEmS

313

Enables/disables the inference rule Empty Sort.

314

Default is 0.

315

@item -ISoR

316

Enables/disables the inference rule Sort Resolution.

317

Default is 0.

318

@item -IEqR

319

Enables/disables the inference rule Equality Resolution.

320

Default is 0.

321

@item -IERR

322

Enables/disables the inference rule Reflexivity Resolution.

323

Default is 0.

324

@item -IEqF

325

Enables/disables the inference rule Equality Factoring.

326

Default is 0.

327

@item -IMPm

328

Enables/disables the inference rule Merging Paramodulation.

329

Default is 0.

330

@item -ISpR

331

Enables/disables the inference rule Superposition Right.

332

Default is 0.

333

@item -IOPm

334

Enables/disables the inference rule Ordered Paramodulation.

335

Default is 0.

336

@item -ISPm

337

Enables/disables the inference rule Standard Paramodulation.

338

Default is 0.

339

@item -ISpL

340

Enables/disables the inference rule Superposition Left.

341

Default is 0.

342

@item -IORe

343

Enables/disables the inference rule Ordered Resolution.

344

If set to 1, Ordered Resolution is enabled but no resolution

345

inferences with equations are generated. If set to 2, equations

346

are considered for Ordered Resolution steps as well.

347

Default is 0.

348

@item -ISRe

349

Enables/disables the inference rule Standard Resolution.

350

If set to 1, Standard Resolution is enabled but no resolution

351

inferences with equations are generated. If set to 2, equations

352

are considered for Standard Resolution steps as well.

353

Default is 0.

354

@item -ISHy

355

Enables/disables the inference rule Standard Hyper-Resolution.

356

Default is 0.

357

@item -IOHy

358

Enables/disables the inference rule Ordered Hyper-Resolution.

359

Default is 0.

360

@item -IURR

361

Enables/disables the inference rule Unit Resulting Resolution.

362

Default is 0.

363

@item -IOFc

364

Enables/disables the inference rule Ordered Factoring.

365

If set to 1, Ordered Factoring is enabled but only factoring

366

inferences with positive literals are generated. If set to 2,

367

negative literals are considered for inferences as well.

368

Default is 0.

369

@item -ISFc

370

Enables/disables the inference rule Standard Factoring.

371

Default is 0.

372

@item -IUnR

373

Enables/disables the inference rule Unit Resolution.

374

Default is 0.

375

@item -IBUR

376

Enables/disables the inference rule Bounded Depth Unit Resolution.

377

Default is 0.

378

@item -IDEF

379

Enables/disables the inference rule Apply Definitions.

380

Currently not supported.

381

Default is 0.

382

@item -RFRew

383

Enables/disables the reduction rule Forward Rewriting.

384

If set to 1 unit rewriting and non-unit rewriting based on

385

a subsumption test is activated.

386

If set to 2 in addition to unit and non-unit rewriting

387

local contextual rewriting is activated.

388

If set to 3 in addition to unit and non-unit rewriting

389

subterm contextual rewriting is activiated. Subterm contextual

390

rewriting subsumes local contextual rewriting.

391

If set to 4 in addition of the rewriting rules of 3, subterm

392

contextual rewriting also tests for negative literal elimination.

393

Default is 0.

394

@item -RBRew

395

Enables/disables the reduction rule Backward Rewriting.

396

Same values and meaning as for flag -RFRew but used in backward direction.

397

Default is 0.

398

@item -RFMRR

399

Enables/disables the reduction rule Forward Matching Replacement Resolution.

400

Default is 0.

401

@item -RBMRR

402

Enables/disables the reduction rule Backward Matching Replacement Resolution.

403

Default is 0.

404

@item -RObv

405

Enables/disables the reduction rule Obvious Reduction.

406

Default is 0.

407

@item -RUnC

408

Enables/disables the reduction rule Unit Conflict.

409

Default is 0.

410

@item -RTer

411

Enables/disables the terminator by setting the maximal number

412

of non-unit clauses to be used during the search.

413

Default is 0.

414

@item -RTaut

415

Enables/disables the reduction rule Tautology Deletion. If

416

set to 1, only syntactic tautologies are detected and

417

deleted. If

418

set to 2, additionally semantic tautologies are removed.

419

Default is 0.

420

@item -RSST

421

Enables/disables the reduction rule Static Soft Typing.

422

Default is 0.

423

@item -RSSi

424

Enables/disables the reduction rule Sort Simplification.

425

Default is 0.

426

@item -RFSub

427

Enables/disables the reduction rule Forward Subsumption Deletion.

428

Default is 0.

429

@item -RBSub

430

Enables/disables the reduction rule Backward Subsumption Deletion.

431

Default is 0.

432

@item -RAED

433

Enables/disables the reduction rule Assignment Equation Deletion.

434

This rule removes particular occurrences of equations from clauses.

435

If set to 1, the reduction is guaranteed to be sound.

436

If set to 2, the reduction is only sound if any potential model

437

of the considered problem has a non-trivial domain.

438

Default is 0.

439

@item -RCon

440

Enables/disables the reduction rule Condensation.

441

Default is 0.

442

@item -TDfg2OtterOptions

443

Enables/disables the inclusion of an Otter options

444

header. This option only applies to dfg2otter. If

445

set to 1 it includes a setting that makes Otter nearly

446

complete. If set to 2 it activates auto modus and if

447

set to 3 it activates the auto2 modus.

448

Default is 0.

449

@item -EML

450

A special EML flag for modal logic or description logic formulae.

451

Never needs to be set explicitly. Is set during parsing.

452

@item -EMLAuto

453

Intended for EML Autonomous mode, as yet not functional.

454

Default is 0.

455

@item -EMLTranslation

456

Determines the translation method used

457

for modal logic or description logic formulae.

458

If set to 0, the standard relational translation method (which

459

is determined by the usual Kripke semantics) is used.

460

If set to 1, the functional translation method is used.

461

If set to 2, the optimised functional translation method is used.

462

If set to 3, the semi-functional translation method is used.

463

A variation of the optimised functional translation method is used, when

464

the following settings are specified: -EMLTranslation=2 -EMLFuncNary=1.

465

The translation will be in terms of n-ary predicates instead of unary

466

predicates and paths.

467

In the current implementation the standard relational translation method

468

is most general. Some

469

restrictions apply to the other methods. The functional translation

470

method and semi-functional translation methods are available only for

471

the basic multi-modal logic K(m) possibly with serial (total) modalities

472

(-EMLTheory=1), plus nominals (ABox statements), terminological axioms

473

and general inclusion and equivalence axioms. The optimised functional

474

translation methods are implemented only for K(m), possibly with serial

475

modalities.

476

Default is 0.

477

@item -EML2Rel

478

If set, propositional/Boolean-type formulae are converted to relational formulae

479

before they are translated to first-order logic.

480

Default is 0.

481

@item -EMLTheory

482

Determines which background theory is assumed.

483

If set to 0, the background theory is empty.

484

If set to 1, then seriality (the background theory for KD) is added for

485

all modalities.

486

If set to 2, then reflexivity (the background theory for KT) is added for

487

all modalities.

488

If set to 3, then symmetry (the background theory for KB) is added for

489

all modalities.

490

If set to 4, then transitivity (the background theory for K4) is added for

491

all modalities.

492

If set to 5, then Euclideanness (the background theory for K5) is added for

493

all modalities.

494

If set to 6, then transitivity and Euclideanness (the background theory

495

for S4) is added for all modalities.

496

If set to 7, then reflexivity, transitivity and Euclideanness (the

497

background theory for S5) is added for all modalities.

498

Default is 0.

499

@item -EMLFuncNdeQ

500

If set, diamond formulae are translated according to

501

tr(dia(phi),s) = nde(s) /\ exists x tr(phi,[s x])

502

(a nde / quantifier formula),

503

otherwise the translation is in accordance with

504

tr(dia(phi),s) = exists x nde(s) /\ tr(phi,[s x])

505

(a quantifier / nde formula).

506

The transltion for box formulae is defined dually.

507

Setting this flag is only meaningful when the flag for the functional or

508

semi functional translation method is set.

509

Default is 1.

510

@item -EMLFuncNary

511

If set, the functional translation into fluted logic is used.

512

This means n-ary predicate symbols are used instead of unary predicate

513

symbols and paths.

514

Setting this flag is only meaningful for testing local

515

satisfiability/validity in multi-modal K.

516

Default is 0.

517

@item -EMLFFSorts

518

If set, sorts for terms are used.

519

Default is 0.

520

@item -EMLElimComp

521

If set, try to eliminate relational composition in modal parameters.

522

Default is 0.

523

@item -EMLPTrans

524

If set, the EML to first-order logic translation is documented.

525

Default is 0.

526

@item -TPTP

527

If set, SPASS expects an input file in TPTP syntax.

528

Default is 0.

529

@item -rf

530

If set, SPASS deletes the input file before termination.

531

Default is 0.

532

@end table

533

@c man end

534

535

@section SETTINGS

536

@noindent

537

@c man begin NOTES

538

You can also specify options for SPASS in the input problem.

539

In the DFG syntax, you would use

540

@example

541

list_of_settings(SPASS).

542

@{*

543

set_flag(DocProof,1).

544

*@}

545

end_of_list.

546

@end example

547

to set the DocProof flag.

548

549

There are three types of options you can set in the input:

550

551

@table @code

552

@item set_flag(<flag>,<value>).

553

Sets a flag to a value. Valid flags and values are described

554

in the OPTIONS section.

555

@item set_precedence(<comma-separated list of function and/or predicate symbols>).

556

Sets the precedence for the listed symbols. The precedence is

557

decreasing from left to right, i.e. the leftmost symbol has

558

the highest precedence.

559

560

Every entry in the list has the form

561

@example

562

SYMBOL | (SYMBOL, WEIGHT [, @{l, r, m@}])

563

@end example

564

You can use the second form to assign weights to symbols (for KBO) or a

565

status (for RPOS). Status is either @t{l} for left-to-right, @t{m} for

566

multiset, or @t{r} for right-to-left. Weight is given as an integer.

567

568

@item set_DomPred(<comma-separated list of predicate symbols>).

569

Listed predicate (@emph{DomPred} for dominant predicate) symbols are

570

first ordered according to their precedence, not according to

571

their argument lists. Only in case of equal predicates, the

572

arguments are examined. For example, if we add the option

573

@example

574

set_DomPred(P).

575

@end example

576

then in the clause

577

@example

578

-> R(f(x,y),a), P(x,a).

579

@end example

580

the atom @i{P(x,a)} is strictly maximal.

581

Predicates listed by the @i{set_DomPred} option are

582

compared according to the precedence.

583

584

@item set_selection(<comma-separated list of predicate symbols>).

585

Sets the selection list that can be employed by the Select flag (see above).

586

587

@item set_ClauseFormulaRelation(<comma separated list auf tuples (<clause number>, sequence of axiom name strings)).

588

This list is in particular set by FLOTTER and enables SPASS for an eventually found proof to show

589

the relation between the clauses used in the proof and the input formulas.

590

If combined with option DocProof, then there needs to be an entry for every clause number.

591

Otherwise an error is reported.

592

@example

593

set_ClauseFormulaRelation((1,ax2),(2,ax1),(3,ax3,ax1)).

594

@end example

595

596

@end table

597

@c man end

598

599

@section EXAMPLES

600

@noindent

601

@c man begin EXAMPLES

602

To run SPASS on a single file without options:

603

@example

604

SPASS @i{filename}

605

@end example

606

@noindent

607

To disable all SPASS output except for the final result:

608

@example

609

SPASS -PGiven=0 -PProblem=0 @i{filename}

610

@end example

611

@c man end

612

613

@section AUTHORS

614

@noindent

615

@c man begin AUTHORS

616

Contact : spass@@mpi-inf.mpg.de

617

618

@c man end

619

620

@section SEE ALSO

621

@noindent

622

@c man begin SEEALSO

623

checkstat(1), filestat(1), pcs(1), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), dfg2dfg(1)

624

@c man end

625