<source>
  <clause name="o_even"> even(o). </clause>
  <clause name="suc_even_odd"> odd(s(X)) :- even(X). </clause>
  <clause name="suc_odd_even"> even(s(X)) :- odd(X). </clause>
  <clause name="nil_even_list"> list_even(nil). </clause>
  <clause name="cons_even_list"> list_even(cons(X,Y)) :- list_even(Y), even(X). </clause>
  <clause name="o_zero_mod_3"> zero_mod_3(o). </clause>
  <clause name="suc_zero_one_mod_3"> one_mod_3(s(X)) :- zero_mod_3(X). </clause>
  <clause name="suc_one_two_mod_3"> two_mod_3(s(X)) :- one_mod_3(X). </clause>
  <clause name="suc_two_zero_mod_3"> zero_mod_3(s(X)) :- two_mod_3(X). </clause>
  <clause name="nil_3n_plus_2_tree"> tree_3n_plus_2(nil). </clause>
  <clause name="two_mod_3_3n_plus_2_tree"> tree_3n_plus_2(X) :- two_mod_3(X). </clause>
  <clause name="cons_3n_plus_2_tree"> tree_3n_plus_2(cons(X,Y)) :- tree_3n_plus_2(Y), tree_3n_plus_2(X). </clause>
  <clause name="list_even_inter_tree3plus2"> q(X) :- tree_3n_plus_2(X), list_even(X). </clause>
  <clause name="q_is_not_empty"> #false(q_is_not_empty) :- q(X). </clause>
</source>
<definitions>
</definitions>
<approximation>
zero_mod_3(o).
odd(s(X1)) :- even(X1).
even(s(X1)) :- odd(X1).
list_even(cons(X1,X2)) :- list_even(X2), even(X1).
#false(q_is_not_empty) :- q(X1).
tree_3n_plus_2(cons(X1,X2)) :- tree_3n_plus_2(X2), tree_3n_plus_2(X1).
tree_3n_plus_2(nil).
q(X1) :- tree_3n_plus_2(X1), list_even(X1).
tree_3n_plus_2(X1) :- two_mod_3(X1).
one_mod_3(s(X1)) :- zero_mod_3(X1).
zero_mod_3(s(X1)) :- two_mod_3(X1).
even(o).
list_even(nil).
two_mod_3(s(X1)) :- one_mod_3(X1).
</approximation>
<justifications>
odd(s(X)) :- even(X). [rename-resolve:
  odd(s(X1)) :- even(X1). {X1=X}
  ]
even(s(X)) :- odd(X). [rename-resolve:
  even(s(X1)) :- odd(X1). {X1=X}
  ]
list_even(cons(X,Y)) :- list_even(Y), even(X). [rename-resolve:
  list_even(cons(X1,X2)) :- list_even(X2), even(X1). {X2=Y,X1=X}
  ]
one_mod_3(s(X)) :- zero_mod_3(X). [rename-resolve:
  one_mod_3(s(X1)) :- zero_mod_3(X1). {X1=X}
  ]
two_mod_3(s(X)) :- one_mod_3(X). [rename-resolve:
  two_mod_3(s(X1)) :- one_mod_3(X1). {X1=X}
  ]
zero_mod_3(s(X)) :- two_mod_3(X). [rename-resolve:
  zero_mod_3(s(X1)) :- two_mod_3(X1). {X1=X}
  ]
tree_3n_plus_2(X) :- two_mod_3(X). [rename-resolve:
  tree_3n_plus_2(X1) :- two_mod_3(X1). {X1=X}
  ]
tree_3n_plus_2(cons(X,Y)) :- tree_3n_plus_2(Y), tree_3n_plus_2(X). [rename-resolve:
  tree_3n_plus_2(cons(X1,X2)) :- tree_3n_plus_2(X2), tree_3n_plus_2(X1). {X2=Y,X1=X}
  ]
q(X) :- tree_3n_plus_2(X), list_even(X). [rename-resolve:
  q(X1) :- tree_3n_plus_2(X1), list_even(X1). {X1=X}
  ]
#false(q_is_not_empty) :- q(X). [rename-resolve:
  #false(q_is_not_empty) :- q(X1). {X1=X}
  ]
</justifications>
#ne(q) :- q(X1). [split-def]
#false(q_is_not_empty) :- #ne(q). [split-use:
  #false(q_is_not_empty) :- q(X1).
  ]
tree_3n_plus_2(s(X1)) :- one_mod_3(X1). [eps-resolve:
  tree_3n_plus_2(X1) :- two_mod_3(X1). {X1=s(X1)}
  two_mod_3(s(X1)) :- one_mod_3(X1).
  ]
q(nil) :- tree_3n_plus_2(nil). [eps-resolve:
  q(X1) :- tree_3n_plus_2(X1), list_even(X1). {X1=nil}
  list_even(nil).
  ]
q(cons(X1,X2)) :- tree_3n_plus_2(cons(X1,X2)), list_even(X2), even(X1). [eps-resolve:
  q(X1) :- tree_3n_plus_2(X1), list_even(X1). {X1=cons(X1,X2)}
  list_even(cons(X1,X2)) :- list_even(X2), even(X1).
  ]
q(cons(X1,X2)) :- tree_3n_plus_2(X2), list_even(X2), tree_3n_plus_2(X1), even(X1). [auto-resolve:
  q(cons(X1,X2)) :- tree_3n_plus_2(cons(X1,X2)), list_even(X2), even(X1).
  tree_3n_plus_2(cons(X1,X2)) :- tree_3n_plus_2(X2), tree_3n_plus_2(X1).
  ]
q(nil). [auto-resolve:
  q(nil) :- tree_3n_plus_2(nil).
  tree_3n_plus_2(nil).
  ]
#ne(q) :- tree_3n_plus_2(X2), list_even(X2), tree_3n_plus_2(X1), even(X1). [eps-resolve:
  #ne(q) :- q(X1). {X1=cons(X1,X2)}
  q(cons(X1,X2)) :- tree_3n_plus_2(X2), list_even(X2), tree_3n_plus_2(X1), even(X1).
  ]
#ne(tree_3n_plus_2 & list_even) :- tree_3n_plus_2(X1), list_even(X1). [split-def]
#ne(tree_3n_plus_2 & even) :- tree_3n_plus_2(X1), even(X1). [split-def]
#ne(q) :- #ne(tree_3n_plus_2 & list_even), #ne(tree_3n_plus_2 & even). [split-use:
  #ne(q) :- tree_3n_plus_2(X2), list_even(X2), tree_3n_plus_2(X1), even(X1).
  ]
#ne(q). [eps-resolve:
  #ne(q) :- q(X1). {X1=nil}
  q(nil).
  ]
#ne(tree_3n_plus_2 & list_even) :- tree_3n_plus_2(nil). [eps-resolve:
  #ne(tree_3n_plus_2 & list_even) :- tree_3n_plus_2(X1), list_even(X1). {X1=nil}
  list_even(nil).
  ]
#ne(tree_3n_plus_2 & list_even) :- tree_3n_plus_2(cons(X1,X2)), list_even(X2), even(X1). [eps-resolve:
  #ne(tree_3n_plus_2 & list_even) :- tree_3n_plus_2(X1), list_even(X1). {X1=cons(X1,X2)}
  list_even(cons(X1,X2)) :- list_even(X2), even(X1).
  ]
#ne(tree_3n_plus_2 & list_even) :- tree_3n_plus_2(X2), list_even(X2), tree_3n_plus_2(X1), even(X1). [auto-resolve:
  #ne(tree_3n_plus_2 & list_even) :- tree_3n_plus_2(cons(X1,X2)), list_even(X2), even(X1).
  tree_3n_plus_2(cons(X1,X2)) :- tree_3n_plus_2(X2), tree_3n_plus_2(X1).
  ]
#ne(tree_3n_plus_2 & list_even) :- #ne(tree_3n_plus_2 & list_even), #ne(tree_3n_plus_2 & even). [split-use:
  #ne(tree_3n_plus_2 & list_even) :- tree_3n_plus_2(X2), list_even(X2), tree_3n_plus_2(X1), even(X1).
  ]
#ne(tree_3n_plus_2 & list_even). [auto-resolve:
  #ne(tree_3n_plus_2 & list_even) :- tree_3n_plus_2(nil).
  tree_3n_plus_2(nil).
  ]
#ne(tree_3n_plus_2 & even) :- tree_3n_plus_2(s(X1)), odd(X1). [eps-resolve:
  #ne(tree_3n_plus_2 & even) :- tree_3n_plus_2(X1), even(X1). {X1=s(X1)}
  even(s(X1)) :- odd(X1).
  ]
#ne(tree_3n_plus_2 & even) :- odd(X1), one_mod_3(X1). [auto-resolve:
  #ne(tree_3n_plus_2 & even) :- tree_3n_plus_2(s(X1)), odd(X1).
  tree_3n_plus_2(s(X1)) :- one_mod_3(X1).
  ]
#ne(odd & one_mod_3) :- odd(X1), one_mod_3(X1). [split-def]
#ne(tree_3n_plus_2 & even) :- #ne(odd & one_mod_3). [split-use:
  #ne(tree_3n_plus_2 & even) :- odd(X1), one_mod_3(X1).
  ]
#false(q_is_not_empty). [q-resolve:
  #false(q_is_not_empty) :- #ne(q).
  #ne(q).
  ]
