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

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

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 ...
Constructing countermodel ...

No countermodel exists, formula is valid

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 countermodel ...

No countermodel exists, formula is valid

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 & x = 3

Concrete witness:
y = 12 & x = 3

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

Formula is valid, resulting constraint:
y = 12 & x = 3

Concrete witness:
y = 12 & x = 3

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 ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading sameModule2.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading sameModule3.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

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

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

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 & b = 1 & a >= 1

Concrete witness:
c = -1 & b = 1 & a = 1

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:
(60 >= x1 & x1 >= 40 & x0 >= 80 & \exists int v0; 4 * v0 = x1 & \exists int v0; 4 * v0 = x0) | (45 >= x1 & x1 >= 33 & x0 >= 60 & \exists int v0; 3 * v0 = x1 & \exists int v0; 3 * v0 = x0)

Concrete witness:
x1 = 60 & x0 = 80

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

Formula is valid, resulting constraint:
30 >= x1 & x1 >= 20 & x0 >= 40

Concrete witness:
x1 = 30 & x0 = 40

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

Formula is valid, resulting constraint:
(60 >= x1 & x1 >= 40 & x0 >= 80) | (45 >= x1 & x1 >= 31 & x0 >= 60)

Concrete witness:
x1 = 60 & x0 = 80

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

Formula is valid, resulting constraint:
true

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

Formula is valid, resulting constraint:
b = 15 & a = 16

Concrete witness:
b = 15 & a = 16

Loading relationalFun4.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
g(5) = 1 & g(5) = 0

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

Formula is valid, resulting constraint:
Pete = Jim | Pete = X

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

Formula is valid, resulting constraint:
Pete = Jim | Pete = X | Jim = X

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 ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
c = 0

Loading binderTypes.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading nestedITE.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading linearRanking.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
true

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

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

