Loading cryptarithm.pri ...
Preprocessing ...
Constructing satisfying assignment for the existential constants ...

Formula is valid, satisfying assignment for the existential constants is:
(D + -9 = 0 & N = 0 & R + -5 = 0 & U + -3 = 0 & O + -8 = 0 & Y + -7 = 0 & H + -1 = 0 & S + -6 = 0 & A + -2 = 0 & W + -4 = 0)

Loading functions0.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading functions1.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading functions2.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading functions0b.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading functions1b.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading functions0c.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading functions1c.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading functions2c.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading inequalities0.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading inequalities2.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading inequalities3.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading inequalities4.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading inequalities5.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading inequalities6.pri ...
Preprocessing ...
Constructing satisfying assignment for the existential constants ...

Formula is valid, satisfying assignment for the existential constants is:
(x = 0)

Loading inequalities7.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading inequalities8.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading optimisation0.pri ...
Preprocessing ...
Constructing satisfying assignment for the existential constants ...

Formula is valid, satisfying assignment for the existential constants is:
true

Loading optimisation1.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading optimisation4.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading optimisation5.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
(y + -12 = 0 & x + -3 = 0)

Concrete witness:
(y + -12 = 0 & x + -3 = 0)

Loading optimisation6.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
(y + -12 = 0 & x + -3 = 0)

Concrete witness:
(y + -12 = 0 & x + -3 = 0)

Loading predicates0.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading predicates1.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading predicates2.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading predicates3.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading predicates4.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading predicates5.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading predicates6.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading predicates7.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading sameModule.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading sameModule2.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading sameModule3.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading simpleEq0.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading simpleEq1.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading simpleEq2.pri ...
Preprocessing ...
Constructing satisfying assignment for the existential constants ...

Formula is valid, satisfying assignment for the existential constants is:
(X + -2 = 0)

Loading simpleEq4.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading simpleEq5.pri ...
Preprocessing ...
Constructing satisfying assignment for the existential constants ...

Formula is valid, satisfying assignment for the existential constants is:
(x3 = 0 & x5 + -1 = 0)

Loading simpleEq6.pri ...
Preprocessing ...
Constructing satisfying assignment for the existential constants ...

Formula is valid, satisfying assignment for the existential constants is:
(x2 = 0 & x3 = 0 & x4 = 0 & x5 = 0 & x6 = 0)

Loading simpleEq9.pri ...
Preprocessing ...
Constructing satisfying assignment for the existential constants ...

Formula is valid, satisfying assignment for the existential constants is:
(c = 0)

Loading simplify19.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading simplifyInequalities0.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading simplifyInequalities1.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading simplifyInequalities2.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading simplifyInequalities3.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading simplifyInequalities4.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading impliedEq.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading impliedEq2.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading SET043p1.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading SET063p3.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading reducePredLitsBug.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
(!q & !p)

Loading clam-001.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading clam-002.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading clam-003.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading clam-005.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading constraintFreedomBug.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
(c + 1 = 0 & b + -1 = 0 & a + -1 >= 0)

Concrete witness:
(c + 1 = 0 & b + -1 = 0 & a + -1 = 0)

Loading unitResolutionBug.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading functionBug.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading liaStar0.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
(! (! (-1*x1 + 60 >= 0 & x1 + -40 >= 0 & x0 + -80 >= 0 & ! ALL (4*_0 + -1*x1 != 0) & ! ALL (4*_0 + -1*x0 != 0)) & ! (-1*x1 + 45 >= 0 & x1 + -33 >= 0 & x0 + -60 >= 0 & ! ALL (3*_0 + -1*x1 != 0) & ! ALL (3*_0 + -1*x0 != 0))))

Concrete witness:
(x1 + -60 = 0 & x0 + -80 = 0)

Loading liaStar1.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
(-1*x1 + 30 >= 0 & x1 + -20 >= 0 & x0 + -40 >= 0)

Concrete witness:
(x1 + -30 = 0 & x0 + -40 = 0)

Loading liaStar2.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
(! (! (-1*x1 + 60 >= 0 & x1 + -40 >= 0 & x0 + -80 >= 0) & ! (-1*x1 + 45 >= 0 & x1 + -31 >= 0 & x0 + -60 >= 0)))

Concrete witness:
(x1 + -60 = 0 & x0 + -80 = 0)

Loading relationalFun.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading relationalFun3.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
(b + -15 = 0 & a + -16 = 0)

Concrete witness:
(b + -15 = 0 & a + -16 = 0)

Loading uniExConstants0.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
(! (Pete + -1*Jim != 0 & Pete + -1*X != 0))

Loading uniExConstants2.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
(! (Pete + -1*Jim != 0 & Pete + -1*X != 0 & Jim + -1*X != 0))

Loading interpolant0.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading interpolant1.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading vocabularyBug.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading compoundFormulaeBug.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading endsWithComment.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading triggerBug.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading non-body-trigger.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading ite.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading ite2.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading ite3.pri ...
Preprocessing ...
Proving ...

Formula is valid, resulting constraint:
true

Loading div-elimination.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
true

Loading bad-divisibility.pri ...
Preprocessing ...
Proving ...

No proof found

Loading linearRanking.pri ...
Preprocessing ...
Constructing satisfying assignment for the existential constants ...

No satisfying assignment for the existential constants exists, formula is invalid

Loading linearRanking2-quantified.pri ...
Preprocessing ...
Constructing satisfying assignment for the existential constants ...

Formula is valid, satisfying assignment for the existential constants is:

