% Saved by Prover9-Mace4 Version 0.5, December 2007.

set(ignore_option_dependencies). % GUI handles dependencies

if(Prover9). % Options for Prover9
  assign(max_megs, 520).
  assign(max_weight, 375).
  assign(demod_step_limit, 1660).
  assign(demod_size_limit, 1620).
  assign(max_seconds, 60).
end_if.

if(Mace4).   % Options for Mace4
  assign(max_seconds, 60).
end_if.

if(Prover9). % Additional input for Prover9
assign(max_seconds, -1).

assign(max_seconds, -1).

assign(max_seconds, -1).

assign(max_seconds, -1).
end_if.

formulas(assumptions).

% Protocol MSI, counting abstraction

F(i(x),x2,x3) ->  F(plus(plus(x,x2),x3),i(0),0).
F(x,x2,i(x3)) -> F(plus(plus(x,x2),x3),i(0),0).
F(i(x),x2,x3) -> F(x,0,i(plus(x2,x3))).

F(i(x),0,0).

plus(0,y) = y. 
plus(i(x),y) = i(plus(x,y)).

end_of_list.

formulas(goals).

%exists x exists y exists z F(x,i(y),i(z)).

exists x exists y exists z F(x,i(y),i(z)).

% First correctness condition
%exists x exists x1 exists y exists y2 (F(i(x),0,0) -> 
%F(x1,i(y),i(y2))).

%Second correctness condition 
%all y all y2 -F(x1,i(i(y)),y2).

%F(i(0),0,i(i(0)),0,0,0) -> F(0,i(i(0)),0,i(0),i(0),0).

end_of_list.