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.

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

formulas(assumptions).

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

T(x,e,x). 
% transitions of Init automaton
T(a1,bt,a2).
T(a2,bn,a2).
%transitions of Bad automaton
T(a3,bn,a3).
T(a3,bt,a4).
T(a4,bn,a4).
T(a4,bt,a5).
T(a5,bn,a5).
T(a5,bt,a5).

%sequence of transitions
(T(x,y,z) & T(z,v,w)) -> T(x,y * v,w). 

%definition of Init 
T(a1,x,a2) -> Init(x). 

%definition of Bad
T(a3,x,a3) -> Bad(x). 
T(a3,x,a5) -> Bad(x). 

%transitions of transducer

TD(a6,bn,bn,a6).
TD(a6,bt,bn,a7).
TD(a7,bn,bt,a8).
TD(a8,bn,bn,a8).
TD(a6,bt,bt,a9).
TD(a9,bn,bn,a9).
TD(a9,bt,bt,a9). 

%sequence of transitions
(TD(x,y,z,v) & TD(v,s,t,w)) -> TD(x,y * s,z * t,w).  

%definition of transition
Trans(x,y) <-> (TD(a6,x,y,a9) | TD(a6,x,y,a8)).

% definition of reachable states 
Init(x) -> R(x). 
(R(x) & Trans(x,y)) -> R(y).

end_of_list.

formulas(goals).

exists x (R(x) & Bad(x)).

end_of_list.