% 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(domain_size, 5).
  assign(start_size, 5).
  assign(end_size, 5).
  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 ABP

% F(SenderState,ReceiverState,MessageChannel, AckChannel,StateOfCorrectnessAutomata)

(x * y) * z = x * (y * z).
% associativity of append operation

F(1,1,e,e,1).

F(1,x,y,z,w) -> F(2,x,y,z,s(w)).
F(2,x,y,z,w) -> F(2,x,0 * y,z,w).
F(2,x,y,z * 1,w) -> F(2,x,y,z,w).
F(2,x,y,z * 0,w) -> F(3,x,y,z,w).
F(3,x,y,z,w) -> F(4,x,y,z,s(w)). 
F(4,x,y,z,w) -> F(4,x,1 * y,z,w).
F(4,x,y,z * 0,w) -> F(4,x,y,z,w). 
F(4,x,y,z * 1,w) -> F(1,x,y,z,w).

F(x,1,y,z,w) -> F(x,1,y,1 * z,w).
F(x,1,y * 1,z,w) -> F(x,1,y,z,w). 
F(x,1,y * 0,z,w) -> F(x,2,y,z,w).
F(x,2,y,z,w) -> F(x,3,y,z,r(w)).
F(x,3,y,z,w) -> F(x,3,y,0 * z,w).
F(x,3,y * 0,z,w) -> F(x,3,y,z,w).
F(x,3,y,z,w) -> F(x,4,1 * y,z,w).
F(x,4,y,z,w) -> F(x,1,y,z,r(w)). 

F(x,y,(z1 * z2) * z3,v,w) -> F(x,y,z1 * z3,v,w). 
F(x,y,z,(v1 * v2) * v3,w) -> F(x,y,z,v1 * v3,w).  

s(1) = 2.
s(2) = 3.
r(1) = 3. 
r(2) = 1. 

%-(1 = 2) & -(1 = 3) & -(1 = 4) & -(2 = 3) & -(2 = 4) & -(3 = 4).

end_of_list.

formulas(goals).

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

exists x exists y exists z  exists w F(x,y,z,w,3). 

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