Loading columnRed.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 4), simplifying (4), interpolating ...

No countermodel exists, formula is valid

Interpolants:
EX (2*_0 + x = 0)

Loading cryptarithm.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 303), simplifying (344), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(D + -1*O != 0 & N + -1*O != 0 & U + -1*O != 0)

Loading eqProof2.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 15), simplifying (15), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(c + b + -26 = 0)

Loading eqProof3.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 6), simplifying (6), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(c + b + -26 = 0)

Loading eqProof4.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 5), simplifying (5), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(y + -2*d != 0)

Loading eqProof5.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 5), simplifying (5), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(y + -2*d != 0)

Loading eqProof6.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 6), simplifying (6), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(c + b + -1*a != 0)

Loading eqProof.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 15), simplifying (15), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(a + -26 = 0)

Loading surprising.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 8), simplifying (8), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (! EX (5*_0 + y + 1 = 0) & ! EX (5*_0 + y = 0)))

Loading inEqProof0.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 7), simplifying (7), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(x + -5 >= 0)

Loading inEqProof1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 2), simplifying (2), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(y + -1*x = 0)

Loading inEqProof2.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 12), simplifying (13), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (y + -1*x + 3 != 0 & y + -1*x + 2 != 0 & y + -1*x + 1 != 0 & y + -1*x != 0))

Loading inEqProof3.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 2), simplifying (2), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(x1 + -1 >= 0)

Loading inEqProof.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 5), simplifying (5), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(3*b + -1*a >= 0)

Loading int_incompleteness2.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 8), simplifying (8), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (-1*x1 + -1*x2 + 4 >= 0 & ! (x1 + x2 + -4 = 0 & ! ALL (6*_0 + -1*x1 + 2 != 0)) & ! (x1 + x2 + -4 = 0 & ! ALL (6*_0 + -1*x2 + 1 != 0)) & ! (-1*x1 + -1*x2 + 4 >= 0 & x1 + x2 + -3 >= 0 & ! ALL (6*_0 + -1*x1 + 1 != 0)) & ! (-1*x1 + -1*x2 + 4 >= 0 & x1 + x2 + -3 >= 0 & ! ALL (6*_0 + -1*x2 != 0)) & ! (-1*x1 + -1*x2 + 3 >= 0 & x1 + x2 + -2 >= 0 & ! ALL (6*_0 + -1*x2 + 1 != 0)) & ! (-1*x1 + -1*x2 + 2 >= 0 & x1 + x2 + -1 >= 0 & ! ALL (6*_0 + -1*x2 != 0))))

Loading int_incompleteness3.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 3), simplifying (3), interpolating ...

No countermodel exists, formula is valid

Interpolants:
EX (6*_0 + x1 + -8 = 0)

Loading pidgeon.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 100), simplifying (161), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (x3 + -1*x1 != 0 & x2 + -1*x1 != 0))

Loading pidgeonSimplified.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 24), simplifying (39), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (x3 + -1*x1 != 0 & x2 + -1*x1 != 0))

Loading pidgeonSuperSimplified.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 3), simplifying (3), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(x2 + -1*x1 = 0)

Loading prog.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 8), simplifying (8), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (-1*a + 2 >= 0 & ! (a >= 0 & ! ALL (2*_0 + -1*a != 0))))
(3*b + -1*a >= 0)
(c + -1*a + -1 >= 0)

Loading prop0.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 15), simplifying (15), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (p & !q))

Loading prop1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 17), simplifying (19), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! ALL (2*_0 + -1*a != 0) & ! (-2*c + 6*b + -1*a + 1 >= 0 & p))

Loading prop2.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 4), simplifying (4), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(p(14, 2*x))

Loading prop3.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 4), simplifying (4), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(x + -13 = 0)

Loading prop4.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 7), simplifying (7), interpolating ...

No countermodel exists, formula is valid

Interpolants:
ALL (! (2*_0 + -1*y = 0 & !p(_0)))

Loading prop5.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 17), simplifying (18), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (!p(2) & !p(1)))
(! (!p(3) & !p(2) & !p(1) & !p(0)))

Loading queen2-1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 12), simplifying (13), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (x1 + -1*x0 + -1 != 0 & x1 + -1*x0 + 1 != 0 & x1 + -1*x0 != 0 & x2 + -1*x0 + 1 >= 0))

Loading queen3-1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 12), simplifying (13), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (x1 + -1*x0 + -1 != 0 & x1 + -1*x0 + 1 != 0 & x1 + -1*x0 != 0 & x2 + -1*x0 + 1 >= 0))

Loading super_queen2-1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 12), simplifying (13), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (x1 + -1*x0 + -1 != 0 & x1 + -1*x0 + 1 != 0 & x2 + -1*x0 + 1 >= 0))

Loading super_queen3-1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 16), simplifying (17), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (x2 + -1*x1 + -2 != 0 & x2 + -1*x1 + 2 != 0 & x2 + -1*x1 + -1 != 0 & x2 + -1*x1 + 1 != 0))

Loading cav-ex4b.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 106), simplifying (99), interpolating ...

No countermodel exists, formula is valid

Interpolants:
ALL ALL ALL ALL ALL ALL (! (-1*_0 + n >= 0 & _0 + -1*_1 >= 0 & _1 >= 0 & -1*_2 + _4 + -1 >= 0 & h'(_3, _2) & h'(_5, _4) & f(_0, _3) & f(_1, _5)))
EX EX EX EX EX EX (-1*_0 + n >= 0 & _0 + -1*_1 >= 0 & _0 >= 0 & _1 >= 0 & -1*_2 + _4 + -1 >= 0 & h'(_3, _2) & h'(_5, _4) & f(_0, _3) & f(_1, _5))

Loading quan.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 7), simplifying (7), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(c >= 0)

Loading ring_2exp10_3vars_2ite_unsat.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 2825), simplifying (2930), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (-1*v2 + 1023 >= 0 & ! (v_princess_0 + -2*v2 + 1024 = 0 & ! (v2 + -512 != 0 & ! (-1*v2 + 1023 >= 0 & v2 + -513 >= 0))) & ! (v_princess_0 + -2*v2 = 0 & -1*v2 + 511 >= 0)))

Loading arrays0.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 11), simplifying (11), interpolating ...

No countermodel exists, formula is valid

Interpolants:
true
true
true
true
true
ALL (! (prob_index'2 + -1 = 0 & store(_0, 1, 0, prres0'1)))
ALL (! (prob_index'2 + -1 = 0 & store(_0, 1, 0, prres0'1)))
(prob_index'2 + -1 != 0)
(prob_index'2 + -1 != 0)

Loading constOrderBug.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 130), simplifying (138), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (sym2 != 0 & ! (sym2 + -1*sym1 = 0 & ! (sym1 + -1 != 0 & ! (sym1 + -2 = 0 & ! ALL (2*_0 + -1*sym1 + -2 != 0))))))

Loading strange_concurrency.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
EX (id1 = 0 & id0 + -2 = 0 & write1' + -33 = 0 & write0' + -16 = 0 & write1 + -33 = 0 & write0 + -32 = 0 & read1' + -33 = 0 & read0' + -16 = 0 & read1 + -33 = 0 & read0 + -32 = 0 & A2 = 0 & A1 + -1 = 0 & A0 + -2 = 0 & j1' + -33 = 0 & j0' + -16 = 0 & j2 + -2 = 0 & j1 + -1 = 0 & j0 = 0 & i2' = 0 & i1' = 0 & i0' = 0 & i2 + -32 = 0 & i1 + -32 = 0 & i0 + -32 = 0 & select(A3, 33, 1) & select(2, 33, 0) & select(2, 32, _0) & select(2, 16, 0) & select(1, 33, 0) & select(1, 16, 0) & select(0, 33, 1) & select(0, 16, 0) & store(A3, 33, 2, A4) & store(2, 32, _0 + 1, 1) & store(1, 33, 1, 0) & store(0, 16, 1, A3) & T(32, 32, 1, 2, 1, 0, 33, 33) & T(32, 32, 0, 1, 2, 1, 32, 32) & T(0, 0, 33, j2', A3, A4, 33, 33) & T(0, 0, 16, 33, 0, A3, 16, 16) & !select(1, 32, 0) & !select(0, 33, 0) & !store(A3, 33, 2, A3) & !store(A3, 33, 2, 2) & !store(A3, 33, 2, 1) & !store(A3, 33, 2, 0) & !store(2, 32, _0 + 1, 2) & !store(1, 33, 1, 2) & !store(1, 33, 1, 1) & !store(0, 33, 1, A3) & !store(0, 16, 1, 2) & !store(0, 16, 1, 1) & !store(0, 16, 1, 0))

Loading wrongInterpolant3.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 141), simplifying (137), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! ALL (4*_0 + j2 + i1 + -2 != 0) & ! ALL (4*_0 + j1 + i1 + -1 != 0) & ! ALL (4*_0 + i1 != 0))

Loading omegaBug.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
(sym9 = 0 & sym8 = 0 & sym7 = 0 & sym6 = 0 & sym5 + -1 = 0 & sym4 + -2 = 0 & sym3 + -1 = 0 & sym2 + -1 = 0 & sym1 + -1 = 0 & sym0 + -268435456 = 0 & select(0, 1, 12) & store(1, 1, 12, 0) & store(0, 2, 3, 0) & inUnsigned(32, 2) & inUnsigned(32, 1) & inUnsigned(32, 0) & inSigned(32, 268435456) & inArray(1) & inArray(0) & !select(1, 1, 12))

Loading splitEq.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 371), simplifying (276), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(-1*x + 10000000 >= 0 & x + 1000000 >= 0)

Loading incorrectPredInterpolant.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 9), simplifying (13), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (-1*e + d + 1 >= 0 & ! (e + -1*d + -1 = 0 & p(-1*d)) & ! (e = 0 & ! (d >= 0 & ! (d = 0 & p(0))))))

Loading certificateBug.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 1), simplifying (1), interpolating ...

No countermodel exists, formula is valid

Interpolants:
true

Loading missingOmegaSupport.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 1135), simplifying (1010), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(x5 + -1*x2 + x8 + -1*x6 + x3 + 1 >= 0 & x5 + x2 + -2*x9 + -1*x8 + 2*x0 + 4*x6 + x3 + -5 >= 0 & ! (-1*x7 + -5*x5 + -4*x2 + x9 + x8 + -4*x0 + -7*x6 + -1*x3 + 8 >= 0 & ! (x7 + 5*x5 + 4*x2 + -1*x9 + -1*x8 + 4*x0 + 7*x6 + x3 + -7 >= 0 & ! ALL (5*_0 + -8*x7 + 10*x5 + 5*x2 + 5*x8 + -3*x0 + -6*x6 + 6 != 0))))

Loading bignum_lia1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 58), simplifying (44), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (-1*x4 + 19670160000*x1 + -1 >= 0 & -1*x4 + 16039976000*x1 + -1 >= 0 & -1*x4 + 9835080000*x1 + -1 >= 0 & -1*x4 + 8019988000*x1 + -1 >= 0 & -1*x4 >= 0))

Loading linear-combination-bug.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 13), simplifying (13), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (! EX (8*_0 + -1*x1 + 8 = 0) & ! EX (8*_0 + -1*x1 + 7 = 0) & ! EX (8*_0 + -1*x1 + 6 = 0) & ! EX (8*_0 + -1*x1 + 5 = 0) & ! EX (8*_0 + -1*x1 + 4 = 0)))

Loading div-right-bug.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 14), simplifying (14), interpolating ...

No countermodel exists, formula is valid

Interpolants:
EX (10*_0 + c + -2 = 0)

Loading prp-2-17.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 4505), simplifying (3675), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (! (v_princess_0 + -402 = 0 & i844 + -1 != 0) & ! (v_princess_0 + -30 = 0 & i844 + -1 != 0) & ! (v_princess_0 + -18 = 0 & i844 + -1 != 0) & ! (v_princess_0 + -22 != 0 & i844 + -1 != 0)))

Loading prp-3-18.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 6772), simplifying (4055), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(v_princess_0 + -400 = 0 & i844 + -1 != 0)

Loading surprising25.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 8), interpolating ...

No countermodel exists, formula is valid

Interpolants:
EX (-1*_0 + 23 >= 0 & _0 >= 0 & ! ALL (25*_0 + _1 + -1*y + -10 != 0) & ! ALL (! (-1*_0 + -1*_1 + 10 >= 0 & -1*_0 + 19 >= 0 & _0 >= 0 & ! ALL (25*_0 + _1 + y != 0))))

Loading bignum_lia1.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 58), interpolating ...

No countermodel exists, formula is valid

Interpolants:
(! (-1*x4 + 19670160000*x1 + 7998 >= 0 & -1*x4 + 16039976000*x1 + 7998 >= 0 & -1*x4 + 9835080000*x1 + 3998 >= 0 & -1*x4 + 8019988000*x1 + 3998 >= 0 & -1*x4 + 7998 >= 0 & ! EX (-1*_0 + x4 + -19670160000*x1 >= 0 & -1*_0 + 7998 >= 0 & _0 >= 0 & ! ALL (8000*_0 + _1 + -1*x4 != 0)) & ! EX (-1*_0 + x4 + -16039976000*x1 >= 0 & -1*_0 + 7998 >= 0 & _0 >= 0 & ! ALL (8000*_0 + _1 + -1*x4 != 0)) & ! EX (-1*_0 + x4 + -9835080000*x1 >= 0 & -1*_0 + 3998 >= 0 & _0 >= 0 & ! ALL (4000*_0 + _1 + -1*x4 != 0)) & ! EX (-1*_0 + x4 + -8019988000*x1 >= 0 & -1*_0 + 3998 >= 0 & _0 >= 0 & ! ALL (4000*_0 + _1 + -1*x4 != 0)) & ! EX (-1*_0 + x4 + -10487999 >= 0 & -1*_0 + 10471999 >= 0 & _0 >= 0 & ! ALL (10480000*_0 + _1 + -1*x4 + 7999 != 0)) & ! EX (-1*_0 + x4 + -4000 >= 0 & -1*_0 + 3998 >= 0 & _0 >= 0 & ! ALL (4000*_0 + _1 + -1*x4 != 0)) & ! EX (-1*_0 + 7998 >= 0 & _0 >= 0 & ! ALL (8000*_0 + _1 + -1*x4 != 0) & ! (_0 + -1*x4 + 20951999 >= 0 & ! EX (-1*_0 + -1*_1 + x4 + -10480000 >= 0 & -1*_0 + 10471999 >= 0 & _0 >= 0 & ! ALL (10480000*_0 + _1 + _2 + -1*x4 != 0))))))

Loading ring_2exp10_3vars_0ite_unsat.pri ...
Preprocessing ...
Constructing countermodel ...
Found proof (size 1019), simplifying (1323)


No countermodel exists, formula is valid

Constraint: true
