The following images show two-sided clausal tableaux proofs underlying interpolation for a simple synthesis problem, obtained by different provers or prover configurations.

**Input: Two Programs and a Vocabulary**

P = [(p(X) <-- q(X))], Q = [(r(X) <-- p(X)), (r(X) <-- q(X))], V = [p, r].

R = [(r(A)<--p(A))]

all(x, ((~q0(x);p0(x)), (~q1(x);p1(x)), (~p0(x);r0(x)), (~p1(x);r1(x)), (~q0(x);r0(x)), (~q1(x);r1(x)))), all(x, ((~p0(x);p1(x)),(~q0(x);q1(x)),(~r0(x);r1(x))))

->

(ex(x, (p0(x),~p1(x); q_prime_0(x),~q_prime_1(x); r0(x),~r1(x))); ex(x, (q_prime_0(x),~p0(x);q_prime_1(x),~p1(x))); all(x, ((~p0(x);r0(x)), (~p1(x);r1(x)), (~q_prime_0(x);r0(x)), (~q_prime_1(x);r1(x)))))

Contact: info@christophwernhard.com