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

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

formulas(assumptions).

% tree transducer
T(n,n,q0).
T(t,n,q1).
T(n,t,q3).
T(x,z,q0) & T(y,v,q0) -> T(fT(x,y),fN(z,v),q1).
T(x,z,q1) & T(y,v,q0) -> T(fN(x,y),fT(z,v),q2).
T(x,z,q0) & T(y,v,q1) -> T(fN(x,y),fT(z,v),q2).
T(x,z,q0) & T(y,v,q0) -> T(fN(x,y),fN(z,v),q0).
T(x,z,q0) & T(y,v,q2) -> T(fN(x,y),fN(z,v),q2).
T(x,z,q2) & T(y,v,q0) -> T(fN(x,y),fN(z,v),q2).
T(x,z,q3) & T(y,v,q0) -> T(fT(x,y),fN(z,v),q2). 
T(x,z,q0) & T(y,v,q3) -> T(fT(x,y),fN(z,v),q2). 
T(x,z,q0) & T(y,v,q0) -> T(fN(x,y),fT(z,v),q3). 

% Initial states automaton 

Init(n,q0).
Init(t,q1).
Init(x,q0) & Init(y,q0) -> Init(fT(x,y),q1). 
Init(x,q0) & Init(y,q1) -> Init(fN(x,y),q1).
Init(x,q0) & Init(y,q0) -> Init(fN(x,y),q0).
Init(x,q1) & Init(y,q0) -> Init(fN(x,y),q1).

% Bad states automaton 

Bad(n,q0).
Bad(t,q1).
Bad(x,q0) & Bad(y,q0) -> Bad(fN(x,y),q0).
Bad(x,q0) & Bad(y,q0) -> Bad(fT(x,y),q1).
Bad(x,q0) & Bad(y,q1) -> Bad(fN(x,y),q1).
Bad(x,q1) & Bad(y,q0) -> Bad(fN(x,y),q0).

Bad(x,q0) & Bad(y,q1) -> Bad(fT(x,y),q2).
Bad(x,q1) & Bad(y,q0) -> Bad(fT(x,y),q2).
Bad(x,q1) & Bad(y,q1) -> Bad(fN(x,y),q2).
Bad(x,q1) & Bad(y,q2) -> Bad(fT(x,y),q2).

Bad(x,q2) & Bad(y,q1) -> Bad(fT(x,y),q2).
Bad(x,q2) & Bad(y,q2) -> Bad(fT(x,y),q2).
Bad(x,q1) & Bad(y,q1) -> Bad(fN(x,y),q2).
Bad(x,q0) & Bad(y,q2) -> Bad(fN(x,y),q2).
Bad(x,q2) & Bad(y,q0) -> Bad(fN(x,y),q2).
Bad(x,q1) & Bad(y,q2) -> Bad(fN(x,y),q2).
Bad(x,q2) & Bad(y,q1) -> Bad(fN(x,y),q2).
Bad(x,q2) & Bad(y,q2) -> Bad(fN(x,y),q2).

T(x,y,q2) -> R(x,y).
R(x,y) & R(y,z) -> R(x,z).

Init(x,q1) -> Init1(x). 
Bad(x,q2) -> Bad1(x).

end_of_list.

formulas(goals).

exists x exists y ((Init1(x) & R(x,y)) & Bad1(y)). 

%exists x exists y ((Init(x,q1) & R(x,y)) & Bad(y,q2)). 

%exists x exists y ((Init(x,q1) & T(x,y,q2)) & Bad(y,q2)).

%exists x T(fN(fN(n,fN(t,n)),n),x,q2).

end_of_list.