WATCH: 0.00 CPU 0.01 WC
% Using real theory (possibly mixed with rationals)

SPASS V 2.2.14  in combination with yices.
SPASS beiseite: Proof found by SPASS.
Problem: /tmp/SPASST_23029_cl5-011 
SPASS derived 119 clauses, backtracked 0 clauses and kept 97 clauses.
SPASS backtracked 0 times (0 times due to theory inconsistency).
SPASS allocated 6388 KBytes.
SPASS spent	0:00:00.03 on the problem.
		0:00:00.00 for the input.
		0:00:00.00 for the FLOTTER CNF translation.
		0:00:00.02 for inferences.
		0:00:00.00 for the backtracking.
		0:00:00.01 for the reduction.
		0:00:00.00 for interacting with the SMT procedure.
		

Here is a proof with depth 1, length 5 :
2[0:Inp] ||  -> equal(minus(U,V),W)* equal(U,plus(W,V))*.
11[0:ThA] ||  -> equal(plus(U,0),U)**.
34[0:ArS:2.0] ||  -> equal(U,plus(V,W))* equal(plus(U,uminus(W)),V)*.
81[0:SpR:34.0,11.0] ||  -> equal(plus(U,uminus(0)),V)* equal(U,V).
155(e)[0:BLD:81.0] ||  -> .
Formulae used in the proof : fof_real_combined_problem_2


WATCH: 0.25 CPU 0.45 WC

FINAL WATCH: 0.25 CPU 0.45 WC