% 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 % Additional input for Mace4 assign(max_seconds, -1). end_if. formulas(assumptions). % rewriting rules R(fi(x,fr(y,z)),fr(x,fr(y,z))). R(fi(fr(x,y),z),fr(fr(x,y),z)). R(ft(x,fr(y,z)),fb(x,ft(y,z))). R(ft(fr(x,y),z),fb(ft(x,y),z)). R(fb(x,ft(y,z)),ft(x,fi(y,z))). R(fb(ft(x,y),z),ft(fi(x,y),z)). R(fi(e,e),fr(e,e)). % reflexivity R(x,x). %congruence (R(x,y) & R(z,v)) -> R(fn(x,z),fn(y,v)). (R(x,y) & R(z,v)) -> R(ft(x,z),ft(y,v)). (R(x,y) & R(z,v)) -> R(fr(x,z),fr(y,v)). (R(x,y) & R(z,v)) -> R(fi(x,z),fi(y,v)). % transitivity (R(x,y) & R(y,z)) -> R(x,z). I(fi(e,e)). I(x) & I(y) -> I(fi(x,y)). B1(ft(e,e)). (B1(x) & B1(y)) -> B1(fn(x,y)). (B1(x) & B1(y)) -> B1(ft(x,y)). (B1(x) & B1(y)) -> B1(fi(x,y)). (B1(x) & B1(y)) -> B1(fr(x,y)). (B1(x) & B1(y)) -> B(fn(x,y)). (B1(x) & B1(y)) -> B(ft(x,y)). (B1(x) & B1(y)) -> B(fi(x,y)). (B1(x) & B1(y)) -> B(fr(x,y)). % Not exactly necessary %B(x) -> B(fn(x,y)). %B(y) -> B(fn(x,y)). %B(x) -> B(ft(x,y)). %B(y) -> B(ft(x,y)). %B(x) -> B(fi(x,y)). %B(y) -> B(fi(x,y)). end_of_list. formulas(goals). exists x exists y((I(x) & B(y)) & R(x,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.