% PxButton | prover9 | prover9 -f inconsistent502.in

set(auto).

clauses(sos).
e_t = e_plus4 | e_t = e_plus3 | e_t = e_plus9.
e_t = e_plus4 | e_t = e_plus3 | e_t = e_plus6.
e_t = e_minus9 | e_t = e_plus4 | e_t = e_plus3.
e_t = e_minus7 | e_t = e_plus9 | e_t = e_plus5.
e_t = e_plus2 | e_t = e_minus1 | e_t = e_plus4.
e_t = e_plus8 | e_t = e_minus4 | e_t = e_plus2.
e_t = e_plus4 | e_t = e_plus1 | e_t = e_plus3.
e_t = e_plus5 | e_t = e_plus2 | e_t = e_plus9.
e_t = e_plus6 | e_t = e_minus7 | e_t = e_minus8.
e_t = e_minus2 | e_t = e_minus3 | e_t = e_plus1.
e_t = e_minus6 | e_t = e_plus1 | e_t = e_minus9.
e_t = e_minus4 | e_t = e_plus1 | e_t = e_plus9.
e_t = e_plus6 | e_t = e_minus2 | e_t = e_plus9.
e_t = e_minus7 | e_t = e_minus3 | e_t = e_minus4.
e_t = e_minus3 | e_t = e_plus6 | e_t = e_minus4.
e_t = e_plus8 | e_t = e_minus7 | e_t = e_plus3.
e_t = e_plus7 | e_t = e_minus9 | e_t = e_minus2.
e_t = e_minus9 | e_t = e_minus4 | e_t = e_minus8.
e_t = e_plus9 | e_t = e_minus4 | e_t = e_plus5.
e_t = e_plus4 | e_t = e_minus8 | e_t = e_plus6.
e_t = e_plus2 | e_t = e_minus5 | e_t = e_minus7.
e_t = e_plus6 | e_t = e_minus4 | e_t = e_minus1.
e_t = e_plus4 | e_t = e_minus6 | e_t = e_minus2.
e_t = e_plus4 | e_t = e_plus6 | e_t = e_minus5.
e_t = e_plus1 | e_t = e_minus4 | e_t = e_minus6.
e_t = e_plus8 | e_t = e_minus4 | e_t = e_plus6.
e_t = e_minus4 | e_t = e_plus9 | e_t = e_minus8.
e_t = e_plus6 | e_t = e_minus2 | e_t = e_minus7.
e_t = e_minus3 | e_t = e_plus8 | e_t = e_plus7.
e_t = e_plus1 | e_t = e_plus9 | e_t = e_minus6.
e_t = e_minus9 | e_t = e_plus3 | e_t = e_minus2.
e_t = e_plus2 | e_t = e_plus1 | e_t = e_minus6.
e_t = e_minus8 | e_t = e_minus2 | e_t = e_plus3.
e_t = e_plus9 | e_t = e_minus8 | e_t = e_plus3.
e_t = e_plus1 | e_t = e_plus7 | e_t = e_plus4.
e_t = e_plus7 | e_t = e_minus4 | e_t = e_plus9.
e_t = e_minus7 | e_t = e_minus6 | e_t = e_plus9.
e_t = e_plus6 | e_t = e_plus3 | e_t = e_minus4.
e_t = e_minus5 | e_t = e_plus3 | e_t = e_minus9.
e_t = e_minus3 | e_t = e_plus8 | e_t = e_plus2.
e_t = e_minus5 | e_t = e_minus2 | e_t = e_minus9.
e_t = e_plus1 | e_t = e_plus2 | e_t = e_minus4.
e_t = e_minus5 | e_t = e_plus8 | e_t = e_plus7.
e_t = e_minus8 | e_t = e_minus5 | e_t = e_minus3.
e_t = e_minus3 | e_t = e_plus5 | e_t = e_minus8.
e_plus1 != e_minus1.
e_plus2 != e_minus2.
e_plus3 != e_minus3.
e_plus4 != e_minus4.
e_plus5 != e_minus5.
e_plus6 != e_minus6.
e_plus7 != e_minus7.
e_plus8 != e_minus8.
e_plus9 != e_minus9.
end_of_list.