WATCH: 0.00 CPU 0.01 WC
% Using integer theory

SPASS V 2.2.14  in combination with yices.
SPASS beiseite: Proof found by SPASS and SMT.
Problem: /tmp/SPASST_14164_cl5-025 
SPASS derived 384 clauses, backtracked 6 clauses and kept 193 clauses.
SPASS backtracked 2 times (1 times due to theory inconsistency).
SPASS allocated 6923 KBytes.
SPASS spent	0:00:00.05 on the problem.
		0:00:00.00 for the input.
		0:00:00.00 for the FLOTTER CNF translation.
		0:00:00.00 for inferences.
		0:00:00.00 for the backtracking.
		0:00:00.03 for the reduction.
		0:00:00.02 for interacting with the SMT procedure.
		

Here is a proof with depth 0, length 4 :
2[0:Inp] ||  -> lesseq(f(7),3)*.
3[0:Inp] || lesseq(f(4),3)* -> .
4[0:Inp] ||  -> lesseq(f(plus(U,1)),f(plus(U,2)))*.
770(e)[0:ThR:4,3,2] ||  -> .
Formulae used in the proof : fof_co1


WATCH: 0.29 CPU 0.40 WC

FINAL WATCH: 0.29 CPU 0.40 WC