WATCH: 0.00 CPU 0.01 WC
[1] 24439

--------------------------SPASS-START-----------------------------
Input Problem:
1[0:Inp] || $real(U) $real(V) $real(W) -> equal($difference(U,V),W)* equal(U,$sum(W,V))*.
2[0:Inp] || $real(U) $real(V) $real(W) -> equal(V,$difference(U,W))* equal(U,$sum(W,V))*.
3[0:Inp] || $real(U) $real(V) equal(V,$difference(U,W))* equal($difference(U,V),W)* equal(U,$sum(W,V))* $real(W) -> .
 This is a monadic Non-Horn problem with equality.
 Axiom clauses: 0 Conjecture clauses: 3
 Inferences: IEqR=1 IEqF=1 ISpR=1 ISpL=1 IORe=2 IOFc=2 
 Reductions: RFRew=1 RBRew=1 RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RFSub=1 RBSub=1 RAED=1 RCon=1 
 Extras    : No Input Saturation, Precedence Selection, Full Splitting, Full Reduction,  Ratio: 2147483646, FuncWeight: 1, VarWeight: 1, PrefCon: 1
 Precedence: $real > $product > $difference > $sum > $to_rat > $to_int > nequal > $$arithuneq > $int > $rat > $less > $lesseq > $greater > $greatereq > $evaleq > $is_int > $is_rat
 Ordering  : KBO
Processed Problem:

Worked Off Clauses:

Usable Clauses:
1[0:Inp] || $real(U) $real(V) $real(W) -> equal(W,$sum(U,V))* equal($difference(W,V),U)*.
2[0:Inp] || $real(U) $real(V) $real(W) -> equal(W,$sum(U,V))* equal(V,$difference(W,U))*.
3[0:Inp] || $real(U) $real(V) $real(W) equal(W,$sum(U,V))* equal(V,$difference(W,U))* equal($difference(W,V),U)* -> .
Using default external source real
Using default external source sum_equal_1
Using default external source equal_sum_1
Using default external source difference_equal_1
Using default external source equal_difference_1
Using default external source product_equal_1
Using default external source equal_product_1
Using default external source to_int_equal_1
Using default external source equal_to_int_1
Using default external source to_rat_equal_1
	Sending question: fof(real_Q1,question,? [V1] : ( $real(V1) ),unknown,[xdb(limit,number(3))]).
	Sending question: fof(nequal_1_Q2,question,? [V1] : ( $$arithuneq($difference(V1,V1),V1) & $real(V1) & $$arithuneq($sum(V1,V1),V1) ),unknown,[xdb(limit,number(3))]).
WATCH: 0.22 CPU 3.02 WC

	Receiving answer: fof(computed,answer,$$arithuneq($difference(271.000,271.000),271.000),answer_to(nequal_1_Q2,[])).
	Receiving answer: fof(computed,answer,$$arithuneq($difference(-269.000,-269.000),-269.000),answer_to(nequal_1_Q2,[])).
	Receiving answer: fof(computed,answer,$$arithuneq($difference(273.000,273.000),273.000),answer_to(nequal_1_Q2,[])).
	Sending question: fof(nequal_1_Q3,question,? [V1,V2] : ( $$arithuneq($difference(V1,V2),V2) & $real(V2) & $real(V1) & $$arithuneq(V1,$sum(V2,V2)) ),unknown,[xdb(limit,number(3))]).
External connection statistics for 'real':
Number of requests queued: 2
Number of questions asked: 1
Number of axioms delivered: 0

External connection statistics for 'nequal_1':
Number of requests queued: 34
Number of questions asked: 2
Number of axioms delivered: 3

External connection statistics for 'sum_equal_1':
Number of requests queued: 2
Number of questions asked: 0
Number of axioms delivered: 0

External connection statistics for 'equal_sum_1':
Number of requests queued: 2
Number of questions asked: 0
Number of axioms delivered: 0

External connection statistics for 'difference_equal_1':
Number of requests queued: 11
Number of questions asked: 0
Number of axioms delivered: 0

External connection statistics totals:
Number of requests queued: 51
Number of questions asked: 3
Number of axioms delivered: 3

SPASS V 3.5a 
SPASS beiseite: Proof found.
Problem: /CW/home-0/sutcliff/Systems/SPASS-XDB---0.8/HTTPExternals.ax 
SPASS derived 579 clauses, backtracked 0 clauses, performed 0 splits and kept 435 clauses.
SPASS allocated 112188 KBytes.
SPASS spent	0:00:05.16 on the problem.
		0:00:00.02 for the input.
		0:00:00.02 for the FLOTTER CNF translation.
		0:00:00.01 for inferences.
		0:00:00.00 for the backtracking.
		0:00:00.06 for the reduction.


Here is a proof with depth 4, length 7 :
1[0:Inp] || $real(U)+ $real(V)+ $real(W)+ -> equal(W,$sum(U,V))* equal($difference(W,V),U)*.
4[0:Fac:1.0,1.1] || $real(U)+ $real(V) -> equal(V,$sum(U,U))* equal($difference(V,U),U)**.
7[0:Fac:4.0,4.1] || $real(U)+ -> equal($sum(U,U),U) equal($difference(U,U),U)**.
124[0:Inp] ||  -> $$arithuneq($difference(271.000,271.000),271.000)*.
154[0:APN:124.0] || equal($difference(271.000,271.000),271.000)**+ -> .
439[0:Res:7.2,154.0] || $real(271.000)+ -> equal($sum(271.000,271.000),271.000)**.
640[0:ARw:439.0] ||  -> .
Formulae used in the proof :

--------------------------SPASS-STOP------------------------------
SELF  time: 0.146657
CHILD time: 0.006666
[1]  + Done                          ( sleep 2; /bin/rm -f $TEMP )

WATCH: 0.32 CPU 5.47 WC

FINAL WATCH: 0.32 CPU 5.47 WC