assign(report_stderr, 2).
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).

% Peterson protocol. Specification taken from the paper Beyond Regular Model Checking 

(x * y) * z = x * (y * z). 

x * e = x. 
e * x = x. 

Z(e). 
Z(x) -> Z(x * 0). 

U(e). 
U(x) -> U(x * 1). 

R(((0 * 0) * 1) * 1). 
R(x) -> R(0 *(x * 1)).  

Z(x) & R(((x * 0) * 1) * y) -> R(((x * 1) * 0) * y). 
U(y) & R((((x * 1) * 0) * 1)* y) -> R((((x * 1) * 1) * 0)* y).  

%R((((x * 0) * 0) * 1)* y) -> R((((x * 0) * 1) * 0)* y).

R(x * 0) -> R(0 * x).

end_of_list.

formulas(goals).



exists x R((x * 0) * 0).



end_of_list.