%%clingo -V0 0
a(X) :- b(X).
b(1). b(2).
b(1) b(2) a(1) a(2) SATISFIABLE
%%clingo -V0 0
a(X) :- b(X).
b(1). b(2). b(3).
%%clingo -V0 0
a(X) :- b(X), c(X).
b(1). b(2).
c(1).
c(1) b(1) b(2) a(1) SATISFIABLE
%%clingo -V0 0
a(X) :- b(X), c(X).
b(1). b(2).
c(1). c(2). c(3).
%%clingo -V0 0
a(X) :- b(X,Y), c(Y).
b(1,5). b(2,10).
c(10).
c(10) b(1,5) b(2,10) a(2) SATISFIABLE
%%clingo -V0 0
a(X) :- b(X,Y), c(Y).
b(1,5). b(2,10).
c(10). c(5).
%%clingo -V0 0
a(X) :- b(X), Y=X+1, not b(Y).
b(1). b(2).
b(1) b(2) a(2) SATISFIABLE
%%clingo -V0 0
a(X) :- b(X), Y=X+1, not b(Y).
b(1). b(3).
%%clingo -V0 0
a(X) :- b(X), not c(X).
b(1). b(2). c(1).
b(1) b(2) c(1) a(2) SATISFIABLE
%%clingo -V0 0
a(X) :- b(X), not c(X).
b(1). b(2). c(1).
b(3). c(2).
%%clingo -V0 0
a(X) :- b(X,Y), not c(Y).
b(1,5). b(2,10). c(10).
b(1,5) b(2,10) c(10) a(1) SATISFIABLE
%%clingo -V0 0
a(X) :- b(X,Y), not c(Y).
b(1,5). b(2,10).
%%clingo -V0 0
a(X) :- b(X,Y), c(Y).
b(1,2). b(2,3).
c(2).
c(2) b(1,2) b(2,3) a(1) SATISFIABLE
%%clingo -V0 0
a(X) :- b(X,Y), c(Y).
b(1,2). b(2,3).
c(2). c(3).
%%clingo -V0 0
a(X) :- b(X), Y = X+1, not b(Y).
b(1). b(2). b(3).
b(1) b(2) b(3) a(3) SATISFIABLE
%%clingo -V0 0
a(X) :- b(X), Y = X+1, not b(Y).
b(1). b(5).