% 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, -1).
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 FutureBus, counting abstraction

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

%-(i(x) = x).

F(i(x1),x2,x3,x4,x5,0,x7,x8,x9) -> F(x1,0,0,0,i(x5),0,plus(x4,x7),x8,plus(x2,plus(x3,x9))).

F(x1,x2,x3,x4,x5,x6,i(x7),x8,x9) -> 
F(x1,plus(i(0),plus(x2,x5)),x3,x4,0,x6,x7,x8,x9).

F(x1,x2,x3,x4,x5,x6,x7,x8,i(x9)) -> 
F(x1,i(plus(x2,plus(x5,x9))),x3,x4,0,x6,x7,x8,0). 

F(x1,x2,x3,x4,i(i(x5)),x6,0,x8,0) -> 
F(x1,i(i(plus(x5,x2))),x3,x4,0,x6,0,x8,0). 

F(x1,x2,x3,x4,i(0),x6,0,x8,0) -> 
F(x1,x2,i(x3),x4,0,x6,0,x8,0).

F(i(x1),x2,x3,x4,x5,0,x7,x8,x9) -> 
F(plus(x1,plus(x3,plus(x2,plus(x9,plus(x5,x7))))),0,0,0,0,i(0),0,plus(x4,x8),0). 

 F(x1,x2,x3,x4,x5,x6,x7,i(x8),x9) -> 
F(i(x1),x2,x3,plus(x6,x4),x5,0,x7,x8,x9). 

F(x1,x2,x3,x4,x5,x6,x7,0,x9) -> 
F(x1,x2,x3,plus(x6,x4),x5,0,x7,0,x9). 

F(x1,x2,i(x3),x4,x5,x6,x7,x8,x9) ->
F(x1,x2,x3,i(x4),x5,x6,x7,x8,x9).

F(x1,i(x2),x3,x4,x5,x6,x7,x8,x9) ->
F(plus(x2,x1),0,x3,i(x4),x5,x6,x7,x8,x9). 

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

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)).

exists x1 exists x2 exists x3 exists x4 exists x5 exists x6 
exists x7 exists x8 exists x9 F(x1,x2,i(i(x3)),x4,x5,x6,x7,x8,x9) |  

exists x1 exists x2 exists x3 exists x4 exists x5 exists x6 
exists x7 exists x8 exists x9 F(x1,x2,i(x3),i(x4),x5,x6,x7,x8,x9) |

exists x1 exists x2 exists x3 exists x4 exists x5 exists x6 
exists x7 exists x8 exists x9 F(x1,x2,x3,i(i(x4)),x5,x6,x7,x8,x9) |

exists x1 exists x2 exists x3 exists x4 exists x5 exists x6 
exists x7 exists x8 exists x9 F(x1,i(x2),i(x3),x4,x5,x6,x7,x8,x9) |

exists x1 exists x2 exists x3 exists x4 exists x5 exists x6 
exists x7 exists x8 exists x9 F(x1,i(x2),x3,i(x4),x5,x6,x7,x8,x9).  

% 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.