--------------------------SPASS-START-----------------------------

Input Problem:

1[0:Inp] || -> equal(zero,one)**.

2[0:Inp] || -> equal(U,zero)*.

This is a unit equality problem.

This is a problem that has, if any, a finite domain model.

There is a finite domain clause.

There are no function symbols.

The conjecture is ground.

Axiom clauses: 1 Conjecture clauses: 1

Inferences: ISpR=1 ISpL=1

Reductions: RFRew=1 RBRew=1 RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RFSub=1 RBSub=1

Extras : Input Saturation, Always Selection, No Splitting, Full Reduction, Ratio: 5, FuncWeight: 1, VarWeight: 1

Precedence: zero > one

Ordering : KBO

Processed Problem:

Worked Off Clauses:

Usable Clauses:

3[0:Rew:1.0,2.0] || -> equal(U,one)*.

Given clause: 3[0:Rew:1.0,2.0] || -> equal(U,one)*.

Given clause: 5[0:SpR:3.0,3.0] || -> equal(U,V)*.

SPASS V 3.7

SPASS beiseite: Completion found.

Problem: Read from stdin.

SPASS derived 3 clauses, backtracked 0 clauses, performed 0 splits and kept 4 clauses.

SPASS allocated 45932 KBytes.

SPASS spent 0:00:00.23 on the problem.

0:00:00.07 for the input.

0:00:00.14 for the FLOTTER CNF translation.

0:00:00.00 for inferences.

0:00:00.00 for the backtracking.

0:00:00.00 for the reduction.

The saturated set of worked-off clauses is :

5[0:SpR:3.0,3.0] || -> equal(U,V)*.

--------------------------SPASS-STOP------------------------------