From 398e35e3782ab19d51bab93d1d679b0663b0054e Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Mon, 20 Nov 2023 14:21:26 -0800 Subject: [PATCH] Update allSat7.gold --- SBVTestSuite/GoldFiles/allSat7.gold | 2724 +++++++++++++-------------- 1 file changed, 1362 insertions(+), 1362 deletions(-) diff --git a/SBVTestSuite/GoldFiles/allSat7.gold b/SBVTestSuite/GoldFiles/allSat7.gold index b1a36fef0..cebff7648 100644 --- a/SBVTestSuite/GoldFiles/allSat7.gold +++ b/SBVTestSuite/GoldFiles/allSat7.gold @@ -4093,9 +4093,9 @@ Fast allSat, Looking for solution 318 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s62) Fast allSat, Looking for solution 319 [SEND] (check-sat) [RECV] sat @@ -4104,9 +4104,9 @@ Fast allSat, Looking for solution 319 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s61) Fast allSat, Looking for solution 320 [SEND] (check-sat) [RECV] sat @@ -4126,9 +4126,9 @@ Fast allSat, Looking for solution 321 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s58) Fast allSat, Looking for solution 322 [SEND] (check-sat) [RECV] sat @@ -4137,9 +4137,9 @@ Fast allSat, Looking for solution 322 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s89) Fast allSat, Looking for solution 323 [SEND] (check-sat) [RECV] sat @@ -17925,9 +17925,9 @@ Fast allSat, Looking for solution 1416 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s63) Fast allSat, Looking for solution 1417 [SEND] (check-sat) [RECV] sat @@ -17936,9 +17936,9 @@ Fast allSat, Looking for solution 1417 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s62) Fast allSat, Looking for solution 1418 [SEND] (check-sat) [RECV] sat @@ -17947,9 +17947,9 @@ Fast allSat, Looking for solution 1418 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s61) Fast allSat, Looking for solution 1419 [SEND] (check-sat) [RECV] sat @@ -17958,9 +17958,9 @@ Fast allSat, Looking for solution 1419 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s65) Fast allSat, Looking for solution 1420 [SEND] (check-sat) [RECV] sat @@ -17969,9 +17969,9 @@ Fast allSat, Looking for solution 1420 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s60) Fast allSat, Looking for solution 1421 [SEND] (check-sat) [RECV] sat @@ -17980,9 +17980,9 @@ Fast allSat, Looking for solution 1421 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s66) Fast allSat, Looking for solution 1422 [SEND] (check-sat) [RECV] sat @@ -17991,9 +17991,9 @@ Fast allSat, Looking for solution 1422 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s58) Fast allSat, Looking for solution 1423 [SEND] (check-sat) [RECV] sat @@ -18002,9 +18002,9 @@ Fast allSat, Looking for solution 1423 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s67) Fast allSat, Looking for solution 1424 [SEND] (check-sat) [RECV] sat @@ -18013,9 +18013,9 @@ Fast allSat, Looking for solution 1424 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s72) Fast allSat, Looking for solution 1425 [SEND] (check-sat) [RECV] sat @@ -18024,9 +18024,9 @@ Fast allSat, Looking for solution 1425 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s69) Fast allSat, Looking for solution 1426 [SEND] (check-sat) [RECV] sat @@ -18035,9 +18035,9 @@ Fast allSat, Looking for solution 1426 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s70) Fast allSat, Looking for solution 1427 [SEND] (check-sat) [RECV] sat @@ -18046,9 +18046,9 @@ Fast allSat, Looking for solution 1427 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s71) Fast allSat, Looking for solution 1428 [SEND] (check-sat) [RECV] unsat @@ -18077,9 +18077,9 @@ Fast allSat, Looking for solution 1428 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s63) Fast allSat, Looking for solution 1429 [SEND] (check-sat) [RECV] sat @@ -18088,9 +18088,9 @@ Fast allSat, Looking for solution 1429 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s62) Fast allSat, Looking for solution 1430 [SEND] (check-sat) [RECV] sat @@ -18099,9 +18099,9 @@ Fast allSat, Looking for solution 1430 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s61) Fast allSat, Looking for solution 1431 [SEND] (check-sat) [RECV] sat @@ -18110,9 +18110,9 @@ Fast allSat, Looking for solution 1431 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s65) Fast allSat, Looking for solution 1432 [SEND] (check-sat) [RECV] sat @@ -18121,9 +18121,9 @@ Fast allSat, Looking for solution 1432 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s60) Fast allSat, Looking for solution 1433 [SEND] (check-sat) [RECV] sat @@ -18132,9 +18132,9 @@ Fast allSat, Looking for solution 1433 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s66) Fast allSat, Looking for solution 1434 [SEND] (check-sat) [RECV] sat @@ -18143,9 +18143,9 @@ Fast allSat, Looking for solution 1434 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s58) Fast allSat, Looking for solution 1435 [SEND] (check-sat) [RECV] sat @@ -18154,9 +18154,9 @@ Fast allSat, Looking for solution 1435 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s68) Fast allSat, Looking for solution 1436 [SEND] (check-sat) [RECV] sat @@ -18165,9 +18165,9 @@ Fast allSat, Looking for solution 1436 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s72) Fast allSat, Looking for solution 1437 [SEND] (check-sat) [RECV] sat @@ -21573,9 +21573,9 @@ Fast allSat, Looking for solution 1706 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s67) Fast allSat, Looking for solution 1707 [SEND] (check-sat) [RECV] sat @@ -21584,9 +21584,9 @@ Fast allSat, Looking for solution 1707 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s68) Fast allSat, Looking for solution 1708 [SEND] (check-sat) [RECV] sat @@ -21595,9 +21595,9 @@ Fast allSat, Looking for solution 1708 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s69) Fast allSat, Looking for solution 1709 [SEND] (check-sat) [RECV] sat @@ -21606,9 +21606,9 @@ Fast allSat, Looking for solution 1709 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s70) Fast allSat, Looking for solution 1710 [SEND] (check-sat) [RECV] sat @@ -21617,9 +21617,9 @@ Fast allSat, Looking for solution 1710 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s71) Fast allSat, Looking for solution 1711 [SEND] (check-sat) [RECV] sat @@ -21628,9 +21628,9 @@ Fast allSat, Looking for solution 1711 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s65) Fast allSat, Looking for solution 1712 [SEND] (check-sat) [RECV] sat @@ -21639,9 +21639,9 @@ Fast allSat, Looking for solution 1712 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s64) Fast allSat, Looking for solution 1713 [SEND] (check-sat) [RECV] sat @@ -21650,9 +21650,9 @@ Fast allSat, Looking for solution 1713 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s63) Fast allSat, Looking for solution 1714 [SEND] (check-sat) [RECV] sat @@ -21661,9 +21661,9 @@ Fast allSat, Looking for solution 1714 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s62) Fast allSat, Looking for solution 1715 [SEND] (check-sat) [RECV] sat @@ -21672,9 +21672,9 @@ Fast allSat, Looking for solution 1715 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s58) Fast allSat, Looking for solution 1716 [SEND] (check-sat) [RECV] sat @@ -21683,9 +21683,9 @@ Fast allSat, Looking for solution 1716 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s72) Fast allSat, Looking for solution 1717 [SEND] (check-sat) [RECV] sat @@ -21694,9 +21694,9 @@ Fast allSat, Looking for solution 1717 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) Fast allSat, Looking for solution 1718 [SEND] (check-sat) [RECV] unsat @@ -21725,9 +21725,9 @@ Fast allSat, Looking for solution 1718 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s89) Fast allSat, Looking for solution 1719 [SEND] (check-sat) [RECV] sat @@ -21736,9 +21736,9 @@ Fast allSat, Looking for solution 1719 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s72) Fast allSat, Looking for solution 1720 [SEND] (check-sat) [RECV] sat @@ -21747,9 +21747,9 @@ Fast allSat, Looking for solution 1720 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s58) Fast allSat, Looking for solution 1721 [SEND] (check-sat) [RECV] sat @@ -21758,9 +21758,9 @@ Fast allSat, Looking for solution 1721 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s60) Fast allSat, Looking for solution 1722 [SEND] (check-sat) [RECV] sat @@ -21769,9 +21769,9 @@ Fast allSat, Looking for solution 1722 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s63) Fast allSat, Looking for solution 1723 [SEND] (check-sat) [RECV] sat @@ -21780,9 +21780,9 @@ Fast allSat, Looking for solution 1723 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s64) Fast allSat, Looking for solution 1724 [SEND] (check-sat) [RECV] sat @@ -21791,9 +21791,9 @@ Fast allSat, Looking for solution 1724 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s65) Fast allSat, Looking for solution 1725 [SEND] (check-sat) [RECV] sat @@ -21802,9 +21802,9 @@ Fast allSat, Looking for solution 1725 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s67) Fast allSat, Looking for solution 1726 [SEND] (check-sat) [RECV] sat @@ -21813,9 +21813,9 @@ Fast allSat, Looking for solution 1726 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s68) Fast allSat, Looking for solution 1727 [SEND] (check-sat) [RECV] sat @@ -21824,9 +21824,9 @@ Fast allSat, Looking for solution 1727 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s69) Fast allSat, Looking for solution 1728 [SEND] (check-sat) [RECV] sat @@ -21835,9 +21835,9 @@ Fast allSat, Looking for solution 1728 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s70) Fast allSat, Looking for solution 1729 [SEND] (check-sat) [RECV] sat @@ -21846,9 +21846,9 @@ Fast allSat, Looking for solution 1729 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s71) Fast allSat, Looking for solution 1730 [SEND] (check-sat) [RECV] unsat @@ -21877,9 +21877,9 @@ Fast allSat, Looking for solution 1730 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s67) Fast allSat, Looking for solution 1731 [SEND] (check-sat) [RECV] sat @@ -21888,9 +21888,9 @@ Fast allSat, Looking for solution 1731 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s68) Fast allSat, Looking for solution 1732 [SEND] (check-sat) [RECV] sat @@ -21899,9 +21899,9 @@ Fast allSat, Looking for solution 1732 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s69) Fast allSat, Looking for solution 1733 [SEND] (check-sat) [RECV] sat @@ -21910,9 +21910,9 @@ Fast allSat, Looking for solution 1733 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s70) Fast allSat, Looking for solution 1734 [SEND] (check-sat) [RECV] sat @@ -21921,9 +21921,9 @@ Fast allSat, Looking for solution 1734 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s71) Fast allSat, Looking for solution 1735 [SEND] (check-sat) [RECV] sat @@ -21932,9 +21932,9 @@ Fast allSat, Looking for solution 1735 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s65) Fast allSat, Looking for solution 1736 [SEND] (check-sat) [RECV] sat @@ -21943,9 +21943,9 @@ Fast allSat, Looking for solution 1736 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s64) Fast allSat, Looking for solution 1737 [SEND] (check-sat) [RECV] sat @@ -21954,9 +21954,9 @@ Fast allSat, Looking for solution 1737 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s61) Fast allSat, Looking for solution 1738 [SEND] (check-sat) [RECV] sat @@ -21965,9 +21965,9 @@ Fast allSat, Looking for solution 1738 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s60) Fast allSat, Looking for solution 1739 [SEND] (check-sat) [RECV] sat @@ -21976,9 +21976,9 @@ Fast allSat, Looking for solution 1739 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s58) Fast allSat, Looking for solution 1740 [SEND] (check-sat) [RECV] sat @@ -21987,9 +21987,9 @@ Fast allSat, Looking for solution 1740 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s72) Fast allSat, Looking for solution 1741 [SEND] (check-sat) [RECV] sat @@ -21998,9 +21998,9 @@ Fast allSat, Looking for solution 1741 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) Fast allSat, Looking for solution 1742 [SEND] (check-sat) [RECV] unsat @@ -22029,9 +22029,9 @@ Fast allSat, Looking for solution 1742 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s89) Fast allSat, Looking for solution 1743 [SEND] (check-sat) [RECV] sat @@ -22040,9 +22040,9 @@ Fast allSat, Looking for solution 1743 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s72) Fast allSat, Looking for solution 1744 [SEND] (check-sat) [RECV] sat @@ -22051,9 +22051,9 @@ Fast allSat, Looking for solution 1744 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s58) Fast allSat, Looking for solution 1745 [SEND] (check-sat) [RECV] sat @@ -22062,9 +22062,9 @@ Fast allSat, Looking for solution 1745 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s60) Fast allSat, Looking for solution 1746 [SEND] (check-sat) [RECV] sat @@ -22073,9 +22073,9 @@ Fast allSat, Looking for solution 1746 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s61) Fast allSat, Looking for solution 1747 [SEND] (check-sat) [RECV] sat @@ -22084,9 +22084,9 @@ Fast allSat, Looking for solution 1747 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s62) Fast allSat, Looking for solution 1748 [SEND] (check-sat) [RECV] sat @@ -22095,9 +22095,9 @@ Fast allSat, Looking for solution 1748 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s65) Fast allSat, Looking for solution 1749 [SEND] (check-sat) [RECV] sat @@ -22106,9 +22106,9 @@ Fast allSat, Looking for solution 1749 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s67) Fast allSat, Looking for solution 1750 [SEND] (check-sat) [RECV] sat @@ -22117,9 +22117,9 @@ Fast allSat, Looking for solution 1750 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s68) Fast allSat, Looking for solution 1751 [SEND] (check-sat) [RECV] sat @@ -22128,9 +22128,9 @@ Fast allSat, Looking for solution 1751 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s69) Fast allSat, Looking for solution 1752 [SEND] (check-sat) [RECV] sat @@ -22139,9 +22139,9 @@ Fast allSat, Looking for solution 1752 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s70) Fast allSat, Looking for solution 1753 [SEND] (check-sat) [RECV] sat @@ -22150,9 +22150,9 @@ Fast allSat, Looking for solution 1753 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s71) Fast allSat, Looking for solution 1754 [SEND] (check-sat) [RECV] unsat @@ -22181,9 +22181,9 @@ Fast allSat, Looking for solution 1754 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s67) Fast allSat, Looking for solution 1755 [SEND] (check-sat) [RECV] sat @@ -22192,9 +22192,9 @@ Fast allSat, Looking for solution 1755 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s68) Fast allSat, Looking for solution 1756 [SEND] (check-sat) [RECV] sat @@ -22203,9 +22203,9 @@ Fast allSat, Looking for solution 1756 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s69) Fast allSat, Looking for solution 1757 [SEND] (check-sat) [RECV] sat @@ -22214,9 +22214,9 @@ Fast allSat, Looking for solution 1757 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s70) Fast allSat, Looking for solution 1758 [SEND] (check-sat) [RECV] sat @@ -22225,9 +22225,9 @@ Fast allSat, Looking for solution 1758 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s71) Fast allSat, Looking for solution 1759 [SEND] (check-sat) [RECV] sat @@ -22236,9 +22236,9 @@ Fast allSat, Looking for solution 1759 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 1760 [SEND] (check-sat) [RECV] sat @@ -22247,9 +22247,9 @@ Fast allSat, Looking for solution 1760 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s62) Fast allSat, Looking for solution 1761 [SEND] (check-sat) [RECV] sat @@ -22258,9 +22258,9 @@ Fast allSat, Looking for solution 1761 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s61) Fast allSat, Looking for solution 1762 [SEND] (check-sat) [RECV] sat @@ -22269,9 +22269,9 @@ Fast allSat, Looking for solution 1762 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s60) Fast allSat, Looking for solution 1763 [SEND] (check-sat) [RECV] sat @@ -22280,9 +22280,9 @@ Fast allSat, Looking for solution 1763 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s58) Fast allSat, Looking for solution 1764 [SEND] (check-sat) [RECV] sat @@ -22291,9 +22291,9 @@ Fast allSat, Looking for solution 1764 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s72) Fast allSat, Looking for solution 1765 [SEND] (check-sat) [RECV] sat @@ -22302,9 +22302,9 @@ Fast allSat, Looking for solution 1765 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) Fast allSat, Looking for solution 1766 [SEND] (check-sat) [RECV] unsat @@ -22333,9 +22333,9 @@ Fast allSat, Looking for solution 1766 [SEND] (get-value (s1)) [RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s89) Fast allSat, Looking for solution 1767 [SEND] (check-sat) [RECV] sat @@ -22344,9 +22344,9 @@ Fast allSat, Looking for solution 1767 [SEND] (get-value (s1)) [RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s72) Fast allSat, Looking for solution 1768 [SEND] (check-sat) [RECV] sat @@ -22355,9 +22355,9 @@ Fast allSat, Looking for solution 1768 [SEND] (get-value (s1)) [RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s58) Fast allSat, Looking for solution 1769 [SEND] (check-sat) [RECV] sat @@ -22366,9 +22366,9 @@ Fast allSat, Looking for solution 1769 [SEND] (get-value (s1)) [RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s60) Fast allSat, Looking for solution 1770 [SEND] (check-sat) [RECV] sat @@ -22377,9 +22377,9 @@ Fast allSat, Looking for solution 1770 [SEND] (get-value (s1)) [RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s61) Fast allSat, Looking for solution 1771 [SEND] (check-sat) [RECV] sat @@ -22388,9 +22388,9 @@ Fast allSat, Looking for solution 1771 [SEND] (get-value (s1)) [RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s62) Fast allSat, Looking for solution 1772 [SEND] (check-sat) [RECV] sat @@ -22399,9 +22399,9 @@ Fast allSat, Looking for solution 1772 [SEND] (get-value (s1)) [RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 1773 [SEND] (check-sat) [RECV] sat @@ -22410,9 +22410,9 @@ Fast allSat, Looking for solution 1773 [SEND] (get-value (s1)) [RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s64) Fast allSat, Looking for solution 1774 [SEND] (check-sat) [RECV] sat @@ -22421,9 +22421,9 @@ Fast allSat, Looking for solution 1774 [SEND] (get-value (s1)) [RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s67) Fast allSat, Looking for solution 1775 [SEND] (check-sat) [RECV] sat @@ -22432,9 +22432,9 @@ Fast allSat, Looking for solution 1775 [SEND] (get-value (s1)) [RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s68) Fast allSat, Looking for solution 1776 [SEND] (check-sat) [RECV] sat @@ -22443,9 +22443,9 @@ Fast allSat, Looking for solution 1776 [SEND] (get-value (s1)) [RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s69) Fast allSat, Looking for solution 1777 [SEND] (check-sat) [RECV] sat @@ -22454,9 +22454,9 @@ Fast allSat, Looking for solution 1777 [SEND] (get-value (s1)) [RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s70) Fast allSat, Looking for solution 1778 [SEND] (check-sat) [RECV] unsat @@ -22485,9 +22485,9 @@ Fast allSat, Looking for solution 1778 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s67) Fast allSat, Looking for solution 1779 [SEND] (check-sat) [RECV] sat @@ -22496,9 +22496,9 @@ Fast allSat, Looking for solution 1779 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s68) Fast allSat, Looking for solution 1780 [SEND] (check-sat) [RECV] sat @@ -22507,9 +22507,9 @@ Fast allSat, Looking for solution 1780 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s69) Fast allSat, Looking for solution 1781 [SEND] (check-sat) [RECV] sat @@ -22518,9 +22518,9 @@ Fast allSat, Looking for solution 1781 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s71) Fast allSat, Looking for solution 1782 [SEND] (check-sat) [RECV] sat @@ -22529,9 +22529,9 @@ Fast allSat, Looking for solution 1782 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s64) Fast allSat, Looking for solution 1783 [SEND] (check-sat) [RECV] sat @@ -22540,9 +22540,9 @@ Fast allSat, Looking for solution 1783 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 1784 [SEND] (check-sat) [RECV] sat @@ -22551,9 +22551,9 @@ Fast allSat, Looking for solution 1784 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s62) Fast allSat, Looking for solution 1785 [SEND] (check-sat) [RECV] sat @@ -22562,9 +22562,9 @@ Fast allSat, Looking for solution 1785 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s61) Fast allSat, Looking for solution 1786 [SEND] (check-sat) [RECV] sat @@ -22573,9 +22573,9 @@ Fast allSat, Looking for solution 1786 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s60) Fast allSat, Looking for solution 1787 [SEND] (check-sat) [RECV] sat @@ -22584,9 +22584,9 @@ Fast allSat, Looking for solution 1787 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s58) Fast allSat, Looking for solution 1788 [SEND] (check-sat) [RECV] sat @@ -22595,9 +22595,9 @@ Fast allSat, Looking for solution 1788 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s72) Fast allSat, Looking for solution 1789 [SEND] (check-sat) [RECV] sat @@ -22606,9 +22606,9 @@ Fast allSat, Looking for solution 1789 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) Fast allSat, Looking for solution 1790 [SEND] (check-sat) [RECV] unsat @@ -22637,9 +22637,9 @@ Fast allSat, Looking for solution 1790 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s89) Fast allSat, Looking for solution 1791 [SEND] (check-sat) [RECV] sat @@ -22648,9 +22648,9 @@ Fast allSat, Looking for solution 1791 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s72) Fast allSat, Looking for solution 1792 [SEND] (check-sat) [RECV] sat @@ -22659,9 +22659,9 @@ Fast allSat, Looking for solution 1792 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s58) Fast allSat, Looking for solution 1793 [SEND] (check-sat) [RECV] sat @@ -22670,9 +22670,9 @@ Fast allSat, Looking for solution 1793 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s60) Fast allSat, Looking for solution 1794 [SEND] (check-sat) [RECV] sat @@ -22681,9 +22681,9 @@ Fast allSat, Looking for solution 1794 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s61) Fast allSat, Looking for solution 1795 [SEND] (check-sat) [RECV] sat @@ -22692,9 +22692,9 @@ Fast allSat, Looking for solution 1795 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s62) Fast allSat, Looking for solution 1796 [SEND] (check-sat) [RECV] sat @@ -22703,9 +22703,9 @@ Fast allSat, Looking for solution 1796 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 1797 [SEND] (check-sat) [RECV] sat @@ -22714,9 +22714,9 @@ Fast allSat, Looking for solution 1797 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s64) Fast allSat, Looking for solution 1798 [SEND] (check-sat) [RECV] sat @@ -22725,9 +22725,9 @@ Fast allSat, Looking for solution 1798 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s67) Fast allSat, Looking for solution 1799 [SEND] (check-sat) [RECV] sat @@ -22736,9 +22736,9 @@ Fast allSat, Looking for solution 1799 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s68) Fast allSat, Looking for solution 1800 [SEND] (check-sat) [RECV] sat @@ -22747,9 +22747,9 @@ Fast allSat, Looking for solution 1800 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s70) Fast allSat, Looking for solution 1801 [SEND] (check-sat) [RECV] sat @@ -22758,9 +22758,9 @@ Fast allSat, Looking for solution 1801 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s71) Fast allSat, Looking for solution 1802 [SEND] (check-sat) [RECV] unsat @@ -22789,9 +22789,9 @@ Fast allSat, Looking for solution 1802 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s69) Fast allSat, Looking for solution 1803 [SEND] (check-sat) [RECV] sat @@ -22800,9 +22800,9 @@ Fast allSat, Looking for solution 1803 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s70) Fast allSat, Looking for solution 1804 [SEND] (check-sat) [RECV] sat @@ -22811,9 +22811,9 @@ Fast allSat, Looking for solution 1804 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s71) Fast allSat, Looking for solution 1805 [SEND] (check-sat) [RECV] sat @@ -22822,9 +22822,9 @@ Fast allSat, Looking for solution 1805 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s67) Fast allSat, Looking for solution 1806 [SEND] (check-sat) [RECV] sat @@ -22833,9 +22833,9 @@ Fast allSat, Looking for solution 1806 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s64) Fast allSat, Looking for solution 1807 [SEND] (check-sat) [RECV] sat @@ -22844,9 +22844,9 @@ Fast allSat, Looking for solution 1807 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 1808 [SEND] (check-sat) [RECV] sat @@ -22855,9 +22855,9 @@ Fast allSat, Looking for solution 1808 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s62) Fast allSat, Looking for solution 1809 [SEND] (check-sat) [RECV] sat @@ -22866,9 +22866,9 @@ Fast allSat, Looking for solution 1809 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s61) Fast allSat, Looking for solution 1810 [SEND] (check-sat) [RECV] sat @@ -22877,9 +22877,9 @@ Fast allSat, Looking for solution 1810 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s60) Fast allSat, Looking for solution 1811 [SEND] (check-sat) [RECV] sat @@ -22888,9 +22888,9 @@ Fast allSat, Looking for solution 1811 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s58) Fast allSat, Looking for solution 1812 [SEND] (check-sat) [RECV] sat @@ -22899,9 +22899,9 @@ Fast allSat, Looking for solution 1812 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s72) Fast allSat, Looking for solution 1813 [SEND] (check-sat) [RECV] sat @@ -22910,9 +22910,9 @@ Fast allSat, Looking for solution 1813 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) Fast allSat, Looking for solution 1814 [SEND] (check-sat) [RECV] unsat @@ -22942,9 +22942,9 @@ Fast allSat, Looking for solution 1814 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s89) Fast allSat, Looking for solution 1815 [SEND] (check-sat) [RECV] sat @@ -22953,9 +22953,9 @@ Fast allSat, Looking for solution 1815 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s72) Fast allSat, Looking for solution 1816 [SEND] (check-sat) [RECV] sat @@ -22964,9 +22964,9 @@ Fast allSat, Looking for solution 1816 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s58) Fast allSat, Looking for solution 1817 [SEND] (check-sat) [RECV] sat @@ -22975,9 +22975,9 @@ Fast allSat, Looking for solution 1817 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s60) Fast allSat, Looking for solution 1818 [SEND] (check-sat) [RECV] sat @@ -22986,9 +22986,9 @@ Fast allSat, Looking for solution 1818 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s61) Fast allSat, Looking for solution 1819 [SEND] (check-sat) [RECV] sat @@ -22997,9 +22997,9 @@ Fast allSat, Looking for solution 1819 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s62) Fast allSat, Looking for solution 1820 [SEND] (check-sat) [RECV] sat @@ -23008,9 +23008,9 @@ Fast allSat, Looking for solution 1820 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 1821 [SEND] (check-sat) [RECV] sat @@ -23019,9 +23019,9 @@ Fast allSat, Looking for solution 1821 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s64) Fast allSat, Looking for solution 1822 [SEND] (check-sat) [RECV] sat @@ -23030,9 +23030,9 @@ Fast allSat, Looking for solution 1822 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s68) Fast allSat, Looking for solution 1823 [SEND] (check-sat) [RECV] sat @@ -23041,9 +23041,9 @@ Fast allSat, Looking for solution 1823 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s69) Fast allSat, Looking for solution 1824 [SEND] (check-sat) [RECV] sat @@ -23052,9 +23052,9 @@ Fast allSat, Looking for solution 1824 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s70) Fast allSat, Looking for solution 1825 [SEND] (check-sat) [RECV] sat @@ -23063,9 +23063,9 @@ Fast allSat, Looking for solution 1825 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s71) Fast allSat, Looking for solution 1826 [SEND] (check-sat) [RECV] unsat @@ -23095,7 +23095,7 @@ Fast allSat, Looking for solution 1826 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 2)) [GOOD] (push 1) [GOOD] (assert s54) Fast allSat, Looking for solution 1827 @@ -23106,7 +23106,7 @@ Fast allSat, Looking for solution 1827 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 1)) [GOOD] (push 1) [GOOD] (assert s55) Fast allSat, Looking for solution 1828 @@ -23115,23 +23115,12 @@ Fast allSat, Looking for solution 1828 [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 1)) -[SEND] (get-value (s2)) -[RECV] ((s2 15)) -[GOOD] (push 1) -[GOOD] (assert s56) -Fast allSat, Looking for solution 1829 -[SEND] (check-sat) -[RECV] sat -[SEND] (get-value (s0)) -[RECV] ((s0 5)) -[SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s51) -Fast allSat, Looking for solution 1830 +Fast allSat, Looking for solution 1829 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -23139,10 +23128,10 @@ Fast allSat, Looking for solution 1830 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s50) -Fast allSat, Looking for solution 1831 +Fast allSat, Looking for solution 1830 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -23150,10 +23139,10 @@ Fast allSat, Looking for solution 1831 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s49) -Fast allSat, Looking for solution 1832 +Fast allSat, Looking for solution 1831 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -23161,10 +23150,10 @@ Fast allSat, Looking for solution 1832 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s48) -Fast allSat, Looking for solution 1833 +Fast allSat, Looking for solution 1832 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -23172,10 +23161,10 @@ Fast allSat, Looking for solution 1833 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s47) -Fast allSat, Looking for solution 1834 +Fast allSat, Looking for solution 1833 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -23183,10 +23172,10 @@ Fast allSat, Looking for solution 1834 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s46) -Fast allSat, Looking for solution 1835 +Fast allSat, Looking for solution 1834 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -23194,10 +23183,10 @@ Fast allSat, Looking for solution 1835 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s45) -Fast allSat, Looking for solution 1836 +Fast allSat, Looking for solution 1835 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -23205,10 +23194,10 @@ Fast allSat, Looking for solution 1836 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s43) -Fast allSat, Looking for solution 1837 +Fast allSat, Looking for solution 1836 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -23216,10 +23205,10 @@ Fast allSat, Looking for solution 1837 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s57) -Fast allSat, Looking for solution 1838 +Fast allSat, Looking for solution 1837 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -23227,148 +23216,159 @@ Fast allSat, Looking for solution 1838 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s87) +Fast allSat, Looking for solution 1838 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 5)) +[SEND] (get-value (s1)) +[RECV] ((s1 1)) +[SEND] (get-value (s2)) +[RECV] ((s2 4)) +[GOOD] (push 1) +[GOOD] (assert s56) Fast allSat, Looking for solution 1839 [SEND] (check-sat) [RECV] unsat [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s72) -[GOOD] (assert s88) +[GOOD] (assert s68) +[GOOD] (assert s73) Fast allSat, Looking for solution 1839 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 15)) +[RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s69) Fast allSat, Looking for solution 1840 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 15)) +[RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s70) Fast allSat, Looking for solution 1841 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 15)) +[RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s66) Fast allSat, Looking for solution 1842 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 15)) +[RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s65) Fast allSat, Looking for solution 1843 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 15)) +[RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s64) Fast allSat, Looking for solution 1844 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 15)) +[RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s63) Fast allSat, Looking for solution 1845 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 15)) +[RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s62) Fast allSat, Looking for solution 1846 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 15)) +[RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s61) Fast allSat, Looking for solution 1847 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 15)) +[RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s60) Fast allSat, Looking for solution 1848 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 15)) +[RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s58) Fast allSat, Looking for solution 1849 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 15)) +[RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s72) Fast allSat, Looking for solution 1850 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 15)) +[RECV] ((s1 1)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) Fast allSat, Looking for solution 1851 [SEND] (check-sat) [RECV] unsat @@ -23387,140 +23387,140 @@ Fast allSat, Looking for solution 1851 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s89) -[GOOD] (assert s59) +[GOOD] (assert s68) +[GOOD] (assert s88) Fast allSat, Looking for solution 1851 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 14)) +[RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s66) Fast allSat, Looking for solution 1852 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 14)) +[RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s65) Fast allSat, Looking for solution 1853 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 14)) +[RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s64) Fast allSat, Looking for solution 1854 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 14)) +[RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s63) Fast allSat, Looking for solution 1855 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 14)) +[RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s62) Fast allSat, Looking for solution 1856 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 14)) +[RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s61) Fast allSat, Looking for solution 1857 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 14)) +[RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s60) Fast allSat, Looking for solution 1858 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 14)) +[RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s58) Fast allSat, Looking for solution 1859 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 14)) +[RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s72) Fast allSat, Looking for solution 1860 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 14)) +[RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s69) Fast allSat, Looking for solution 1861 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 14)) +[RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s70) Fast allSat, Looking for solution 1862 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 14)) +[RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s71) Fast allSat, Looking for solution 1863 [SEND] (check-sat) [RECV] unsat @@ -23539,140 +23539,140 @@ Fast allSat, Looking for solution 1863 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s89) -[GOOD] (assert s85) +[GOOD] (assert s68) +[GOOD] (assert s59) Fast allSat, Looking for solution 1863 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 13)) +[RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s71) Fast allSat, Looking for solution 1864 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 13)) +[RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s70) Fast allSat, Looking for solution 1865 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 13)) +[RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s69) Fast allSat, Looking for solution 1866 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 13)) +[RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s89) Fast allSat, Looking for solution 1867 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 13)) +[RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s58) Fast allSat, Looking for solution 1868 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 13)) +[RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s60) Fast allSat, Looking for solution 1869 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 13)) +[RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s61) Fast allSat, Looking for solution 1870 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 13)) +[RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s62) Fast allSat, Looking for solution 1871 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 13)) +[RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s63) Fast allSat, Looking for solution 1872 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 13)) +[RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s64) Fast allSat, Looking for solution 1873 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 13)) +[RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s65) Fast allSat, Looking for solution 1874 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 13)) +[RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s66) Fast allSat, Looking for solution 1875 [SEND] (check-sat) [RECV] unsat @@ -23691,114 +23691,114 @@ Fast allSat, Looking for solution 1875 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s89) -[GOOD] (assert s84) +[GOOD] (assert s68) +[GOOD] (assert s85) Fast allSat, Looking for solution 1875 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 12)) +[RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s60) Fast allSat, Looking for solution 1876 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 12)) +[RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s61) Fast allSat, Looking for solution 1877 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 12)) +[RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s62) Fast allSat, Looking for solution 1878 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 12)) +[RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 1879 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 12)) +[RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s64) Fast allSat, Looking for solution 1880 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 12)) +[RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s65) Fast allSat, Looking for solution 1881 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 12)) +[RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s66) Fast allSat, Looking for solution 1882 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 12)) +[RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s72) Fast allSat, Looking for solution 1883 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 12)) +[RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s89) Fast allSat, Looking for solution 1884 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 12)) +[RECV] ((s1 13)) [SEND] (get-value (s2)) [RECV] ((s2 3)) [GOOD] (push 1) @@ -23809,7 +23809,7 @@ Fast allSat, Looking for solution 1885 [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 12)) +[RECV] ((s1 13)) [SEND] (get-value (s2)) [RECV] ((s2 2)) [GOOD] (push 1) @@ -23820,7 +23820,7 @@ Fast allSat, Looking for solution 1886 [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 12)) +[RECV] ((s1 13)) [SEND] (get-value (s2)) [RECV] ((s2 1)) [GOOD] (push 1) @@ -23843,140 +23843,140 @@ Fast allSat, Looking for solution 1887 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s89) -[GOOD] (assert s83) +[GOOD] (assert s68) +[GOOD] (assert s84) Fast allSat, Looking for solution 1887 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 11)) +[RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s71) Fast allSat, Looking for solution 1888 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 11)) +[RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s70) Fast allSat, Looking for solution 1889 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 11)) +[RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s69) Fast allSat, Looking for solution 1890 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 11)) +[RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s58) Fast allSat, Looking for solution 1891 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 11)) +[RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s72) Fast allSat, Looking for solution 1892 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 11)) +[RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s89) Fast allSat, Looking for solution 1893 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 11)) +[RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s61) Fast allSat, Looking for solution 1894 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 11)) +[RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s62) Fast allSat, Looking for solution 1895 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 11)) +[RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 1896 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 11)) +[RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s64) Fast allSat, Looking for solution 1897 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 11)) +[RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s65) Fast allSat, Looking for solution 1898 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 11)) +[RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s66) Fast allSat, Looking for solution 1899 [SEND] (check-sat) [RECV] unsat @@ -23995,114 +23995,114 @@ Fast allSat, Looking for solution 1899 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s89) -[GOOD] (assert s82) +[GOOD] (assert s68) +[GOOD] (assert s83) Fast allSat, Looking for solution 1899 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 10)) +[RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s62) Fast allSat, Looking for solution 1900 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 10)) +[RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s63) Fast allSat, Looking for solution 1901 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 10)) +[RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s64) Fast allSat, Looking for solution 1902 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 10)) +[RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s65) Fast allSat, Looking for solution 1903 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 10)) +[RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s66) Fast allSat, Looking for solution 1904 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 10)) +[RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s60) Fast allSat, Looking for solution 1905 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 10)) +[RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s58) Fast allSat, Looking for solution 1906 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 10)) +[RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s72) Fast allSat, Looking for solution 1907 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 10)) +[RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s89) Fast allSat, Looking for solution 1908 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 10)) +[RECV] ((s1 11)) [SEND] (get-value (s2)) [RECV] ((s2 3)) [GOOD] (push 1) @@ -24113,7 +24113,7 @@ Fast allSat, Looking for solution 1909 [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 10)) +[RECV] ((s1 11)) [SEND] (get-value (s2)) [RECV] ((s2 2)) [GOOD] (push 1) @@ -24124,7 +24124,7 @@ Fast allSat, Looking for solution 1910 [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 10)) +[RECV] ((s1 11)) [SEND] (get-value (s2)) [RECV] ((s2 1)) [GOOD] (push 1) @@ -24147,140 +24147,140 @@ Fast allSat, Looking for solution 1911 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s89) -[GOOD] (assert s81) +[GOOD] (assert s68) +[GOOD] (assert s82) Fast allSat, Looking for solution 1911 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 9)) +[RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s71) Fast allSat, Looking for solution 1912 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 9)) +[RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s70) Fast allSat, Looking for solution 1913 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 9)) +[RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s69) Fast allSat, Looking for solution 1914 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 9)) +[RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s61) Fast allSat, Looking for solution 1915 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 9)) +[RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s60) Fast allSat, Looking for solution 1916 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 9)) +[RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s58) Fast allSat, Looking for solution 1917 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 9)) +[RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s72) Fast allSat, Looking for solution 1918 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 9)) +[RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s89) Fast allSat, Looking for solution 1919 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 9)) +[RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s63) Fast allSat, Looking for solution 1920 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 9)) +[RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s64) Fast allSat, Looking for solution 1921 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 9)) +[RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s65) Fast allSat, Looking for solution 1922 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 9)) +[RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s66) Fast allSat, Looking for solution 1923 [SEND] (check-sat) [RECV] unsat @@ -24299,114 +24299,114 @@ Fast allSat, Looking for solution 1923 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s89) -[GOOD] (assert s80) +[GOOD] (assert s68) +[GOOD] (assert s81) Fast allSat, Looking for solution 1923 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 8)) +[RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s64) Fast allSat, Looking for solution 1924 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 8)) +[RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s65) Fast allSat, Looking for solution 1925 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 8)) +[RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s66) Fast allSat, Looking for solution 1926 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 8)) +[RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s62) Fast allSat, Looking for solution 1927 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 8)) +[RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s61) Fast allSat, Looking for solution 1928 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 8)) +[RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s60) Fast allSat, Looking for solution 1929 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 8)) +[RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s58) Fast allSat, Looking for solution 1930 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 8)) +[RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s72) Fast allSat, Looking for solution 1931 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 8)) +[RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s89) Fast allSat, Looking for solution 1932 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 8)) +[RECV] ((s1 9)) [SEND] (get-value (s2)) [RECV] ((s2 3)) [GOOD] (push 1) @@ -24417,7 +24417,7 @@ Fast allSat, Looking for solution 1933 [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 8)) +[RECV] ((s1 9)) [SEND] (get-value (s2)) [RECV] ((s2 2)) [GOOD] (push 1) @@ -24428,7 +24428,7 @@ Fast allSat, Looking for solution 1934 [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 8)) +[RECV] ((s1 9)) [SEND] (get-value (s2)) [RECV] ((s2 1)) [GOOD] (push 1) @@ -24451,140 +24451,140 @@ Fast allSat, Looking for solution 1935 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s89) -[GOOD] (assert s79) +[GOOD] (assert s68) +[GOOD] (assert s80) Fast allSat, Looking for solution 1935 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 7)) +[RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s71) Fast allSat, Looking for solution 1936 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 7)) +[RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s70) Fast allSat, Looking for solution 1937 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 7)) +[RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s69) Fast allSat, Looking for solution 1938 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 7)) +[RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s63) Fast allSat, Looking for solution 1939 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 7)) +[RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s62) Fast allSat, Looking for solution 1940 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 7)) +[RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s61) Fast allSat, Looking for solution 1941 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 7)) +[RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s60) Fast allSat, Looking for solution 1942 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 7)) +[RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s58) Fast allSat, Looking for solution 1943 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 7)) +[RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s72) Fast allSat, Looking for solution 1944 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 7)) +[RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s89) Fast allSat, Looking for solution 1945 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 7)) +[RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s65) Fast allSat, Looking for solution 1946 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 7)) +[RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s66) Fast allSat, Looking for solution 1947 [SEND] (check-sat) [RECV] unsat @@ -24603,114 +24603,114 @@ Fast allSat, Looking for solution 1947 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s89) -[GOOD] (assert s78) +[GOOD] (assert s68) +[GOOD] (assert s79) Fast allSat, Looking for solution 1947 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 6)) +[RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s66) Fast allSat, Looking for solution 1948 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 6)) +[RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s64) Fast allSat, Looking for solution 1949 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 6)) +[RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s63) Fast allSat, Looking for solution 1950 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 6)) +[RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s62) Fast allSat, Looking for solution 1951 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 6)) +[RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s61) Fast allSat, Looking for solution 1952 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 6)) +[RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s60) Fast allSat, Looking for solution 1953 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 6)) +[RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s58) Fast allSat, Looking for solution 1954 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 6)) +[RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s72) Fast allSat, Looking for solution 1955 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 6)) +[RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s89) Fast allSat, Looking for solution 1956 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 6)) +[RECV] ((s1 7)) [SEND] (get-value (s2)) [RECV] ((s2 3)) [GOOD] (push 1) @@ -24721,7 +24721,7 @@ Fast allSat, Looking for solution 1957 [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 6)) +[RECV] ((s1 7)) [SEND] (get-value (s2)) [RECV] ((s2 2)) [GOOD] (push 1) @@ -24732,7 +24732,7 @@ Fast allSat, Looking for solution 1958 [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 6)) +[RECV] ((s1 7)) [SEND] (get-value (s2)) [RECV] ((s2 1)) [GOOD] (push 1) @@ -24755,140 +24755,140 @@ Fast allSat, Looking for solution 1959 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s89) -[GOOD] (assert s73) +[GOOD] (assert s68) +[GOOD] (assert s78) Fast allSat, Looking for solution 1959 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 1)) +[RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s71) Fast allSat, Looking for solution 1960 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 1)) -[SEND] (get-value (s2)) -[RECV] ((s2 3)) -[GOOD] (push 1) -[GOOD] (assert s69) -Fast allSat, Looking for solution 1961 -[SEND] (check-sat) -[RECV] sat -[SEND] (get-value (s0)) -[RECV] ((s0 5)) -[SEND] (get-value (s1)) -[RECV] ((s1 1)) +[RECV] ((s1 6)) [SEND] (get-value (s2)) [RECV] ((s2 2)) [GOOD] (push 1) [GOOD] (assert s70) -Fast allSat, Looking for solution 1962 +Fast allSat, Looking for solution 1961 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 1)) +[RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s66) -Fast allSat, Looking for solution 1963 +[GOOD] (assert s69) +Fast allSat, Looking for solution 1962 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 1)) +[RECV] ((s1 6)) [SEND] (get-value (s2)) [RECV] ((s2 7)) [GOOD] (push 1) [GOOD] (assert s65) -Fast allSat, Looking for solution 1964 +Fast allSat, Looking for solution 1963 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 1)) +[RECV] ((s1 6)) [SEND] (get-value (s2)) [RECV] ((s2 8)) [GOOD] (push 1) [GOOD] (assert s64) -Fast allSat, Looking for solution 1965 +Fast allSat, Looking for solution 1964 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 1)) +[RECV] ((s1 6)) [SEND] (get-value (s2)) [RECV] ((s2 9)) [GOOD] (push 1) [GOOD] (assert s63) -Fast allSat, Looking for solution 1966 +Fast allSat, Looking for solution 1965 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 1)) +[RECV] ((s1 6)) [SEND] (get-value (s2)) [RECV] ((s2 10)) [GOOD] (push 1) [GOOD] (assert s62) -Fast allSat, Looking for solution 1967 +Fast allSat, Looking for solution 1966 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 1)) +[RECV] ((s1 6)) [SEND] (get-value (s2)) [RECV] ((s2 11)) [GOOD] (push 1) [GOOD] (assert s61) -Fast allSat, Looking for solution 1968 +Fast allSat, Looking for solution 1967 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 1)) +[RECV] ((s1 6)) [SEND] (get-value (s2)) [RECV] ((s2 12)) [GOOD] (push 1) [GOOD] (assert s60) -Fast allSat, Looking for solution 1969 +Fast allSat, Looking for solution 1968 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 1)) +[RECV] ((s1 6)) [SEND] (get-value (s2)) [RECV] ((s2 13)) [GOOD] (push 1) [GOOD] (assert s58) -Fast allSat, Looking for solution 1970 +Fast allSat, Looking for solution 1969 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) [RECV] ((s0 5)) [SEND] (get-value (s1)) -[RECV] ((s1 1)) +[RECV] ((s1 6)) [SEND] (get-value (s2)) [RECV] ((s2 14)) [GOOD] (push 1) [GOOD] (assert s72) +Fast allSat, Looking for solution 1970 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 5)) +[SEND] (get-value (s1)) +[RECV] ((s1 6)) +[SEND] (get-value (s2)) +[RECV] ((s2 15)) +[GOOD] (push 1) +[GOOD] (assert s89) Fast allSat, Looking for solution 1971 [SEND] (check-sat) [RECV] unsat @@ -24907,7 +24907,7 @@ Fast allSat, Looking for solution 1971 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s71) [GOOD] (assert s74) Fast allSat, Looking for solution 1971 [SEND] (check-sat) @@ -24917,10 +24917,21 @@ Fast allSat, Looking for solution 1971 [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) +[RECV] ((s2 15)) +[GOOD] (push 1) +[GOOD] (assert s89) +Fast allSat, Looking for solution 1972 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 5)) +[SEND] (get-value (s1)) +[RECV] ((s1 2)) +[SEND] (get-value (s2)) [RECV] ((s2 14)) [GOOD] (push 1) [GOOD] (assert s72) -Fast allSat, Looking for solution 1972 +Fast allSat, Looking for solution 1973 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -24931,7 +24942,7 @@ Fast allSat, Looking for solution 1972 [RECV] ((s2 13)) [GOOD] (push 1) [GOOD] (assert s58) -Fast allSat, Looking for solution 1973 +Fast allSat, Looking for solution 1974 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -24942,7 +24953,7 @@ Fast allSat, Looking for solution 1973 [RECV] ((s2 12)) [GOOD] (push 1) [GOOD] (assert s60) -Fast allSat, Looking for solution 1974 +Fast allSat, Looking for solution 1975 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -24953,7 +24964,7 @@ Fast allSat, Looking for solution 1974 [RECV] ((s2 11)) [GOOD] (push 1) [GOOD] (assert s61) -Fast allSat, Looking for solution 1975 +Fast allSat, Looking for solution 1976 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -24964,7 +24975,7 @@ Fast allSat, Looking for solution 1975 [RECV] ((s2 10)) [GOOD] (push 1) [GOOD] (assert s62) -Fast allSat, Looking for solution 1976 +Fast allSat, Looking for solution 1977 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -24975,7 +24986,7 @@ Fast allSat, Looking for solution 1976 [RECV] ((s2 9)) [GOOD] (push 1) [GOOD] (assert s63) -Fast allSat, Looking for solution 1977 +Fast allSat, Looking for solution 1978 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -24986,7 +24997,7 @@ Fast allSat, Looking for solution 1977 [RECV] ((s2 8)) [GOOD] (push 1) [GOOD] (assert s64) -Fast allSat, Looking for solution 1978 +Fast allSat, Looking for solution 1979 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -24997,7 +25008,7 @@ Fast allSat, Looking for solution 1978 [RECV] ((s2 7)) [GOOD] (push 1) [GOOD] (assert s65) -Fast allSat, Looking for solution 1979 +Fast allSat, Looking for solution 1980 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -25008,7 +25019,7 @@ Fast allSat, Looking for solution 1979 [RECV] ((s2 6)) [GOOD] (push 1) [GOOD] (assert s66) -Fast allSat, Looking for solution 1980 +Fast allSat, Looking for solution 1981 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -25019,7 +25030,7 @@ Fast allSat, Looking for solution 1980 [RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s68) -Fast allSat, Looking for solution 1981 +Fast allSat, Looking for solution 1982 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -25030,17 +25041,6 @@ Fast allSat, Looking for solution 1981 [RECV] ((s2 3)) [GOOD] (push 1) [GOOD] (assert s69) -Fast allSat, Looking for solution 1982 -[SEND] (check-sat) -[RECV] sat -[SEND] (get-value (s0)) -[RECV] ((s0 5)) -[SEND] (get-value (s1)) -[RECV] ((s1 2)) -[SEND] (get-value (s2)) -[RECV] ((s2 1)) -[GOOD] (push 1) -[GOOD] (assert s71) Fast allSat, Looking for solution 1983 [SEND] (check-sat) [RECV] unsat @@ -25059,7 +25059,7 @@ Fast allSat, Looking for solution 1983 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s70) [GOOD] (assert s75) Fast allSat, Looking for solution 1983 [SEND] (check-sat) @@ -25069,9 +25069,9 @@ Fast allSat, Looking for solution 1983 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s68) Fast allSat, Looking for solution 1984 [SEND] (check-sat) [RECV] sat @@ -25091,21 +25091,10 @@ Fast allSat, Looking for solution 1985 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) -[GOOD] (push 1) -[GOOD] (assert s68) -Fast allSat, Looking for solution 1986 -[SEND] (check-sat) -[RECV] sat -[SEND] (get-value (s0)) -[RECV] ((s0 5)) -[SEND] (get-value (s1)) -[RECV] ((s1 3)) -[SEND] (get-value (s2)) [RECV] ((s2 6)) [GOOD] (push 1) [GOOD] (assert s66) -Fast allSat, Looking for solution 1987 +Fast allSat, Looking for solution 1986 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -25116,7 +25105,7 @@ Fast allSat, Looking for solution 1987 [RECV] ((s2 7)) [GOOD] (push 1) [GOOD] (assert s65) -Fast allSat, Looking for solution 1988 +Fast allSat, Looking for solution 1987 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -25127,7 +25116,7 @@ Fast allSat, Looking for solution 1988 [RECV] ((s2 8)) [GOOD] (push 1) [GOOD] (assert s64) -Fast allSat, Looking for solution 1989 +Fast allSat, Looking for solution 1988 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -25138,7 +25127,7 @@ Fast allSat, Looking for solution 1989 [RECV] ((s2 9)) [GOOD] (push 1) [GOOD] (assert s63) -Fast allSat, Looking for solution 1990 +Fast allSat, Looking for solution 1989 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -25149,7 +25138,7 @@ Fast allSat, Looking for solution 1990 [RECV] ((s2 10)) [GOOD] (push 1) [GOOD] (assert s62) -Fast allSat, Looking for solution 1991 +Fast allSat, Looking for solution 1990 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -25160,7 +25149,7 @@ Fast allSat, Looking for solution 1991 [RECV] ((s2 11)) [GOOD] (push 1) [GOOD] (assert s61) -Fast allSat, Looking for solution 1992 +Fast allSat, Looking for solution 1991 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -25171,7 +25160,7 @@ Fast allSat, Looking for solution 1992 [RECV] ((s2 12)) [GOOD] (push 1) [GOOD] (assert s60) -Fast allSat, Looking for solution 1993 +Fast allSat, Looking for solution 1992 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -25182,7 +25171,7 @@ Fast allSat, Looking for solution 1993 [RECV] ((s2 13)) [GOOD] (push 1) [GOOD] (assert s58) -Fast allSat, Looking for solution 1994 +Fast allSat, Looking for solution 1993 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -25193,6 +25182,17 @@ Fast allSat, Looking for solution 1994 [RECV] ((s2 14)) [GOOD] (push 1) [GOOD] (assert s72) +Fast allSat, Looking for solution 1994 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 5)) +[SEND] (get-value (s1)) +[RECV] ((s1 3)) +[SEND] (get-value (s2)) +[RECV] ((s2 15)) +[GOOD] (push 1) +[GOOD] (assert s89) Fast allSat, Looking for solution 1995 [SEND] (check-sat) [RECV] unsat @@ -25222,9 +25222,9 @@ Fast allSat, Looking for solution 1995 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s89) Fast allSat, Looking for solution 1996 [SEND] (check-sat) [RECV] sat @@ -25233,9 +25233,9 @@ Fast allSat, Looking for solution 1996 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s72) Fast allSat, Looking for solution 1997 [SEND] (check-sat) [RECV] sat @@ -25244,9 +25244,9 @@ Fast allSat, Looking for solution 1997 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s58) Fast allSat, Looking for solution 1998 [SEND] (check-sat) [RECV] sat @@ -25255,9 +25255,9 @@ Fast allSat, Looking for solution 1998 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s60) Fast allSat, Looking for solution 1999 [SEND] (check-sat) [RECV] sat @@ -25266,9 +25266,9 @@ Fast allSat, Looking for solution 1999 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s61) Fast allSat, Looking for solution 2000 [SEND] (check-sat) [RECV] sat @@ -25277,9 +25277,9 @@ Fast allSat, Looking for solution 2000 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s62) Fast allSat, Looking for solution 2001 [SEND] (check-sat) [RECV] sat @@ -25288,9 +25288,9 @@ Fast allSat, Looking for solution 2001 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s63) Fast allSat, Looking for solution 2002 [SEND] (check-sat) [RECV] sat @@ -25299,9 +25299,9 @@ Fast allSat, Looking for solution 2002 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s64) Fast allSat, Looking for solution 2003 [SEND] (check-sat) [RECV] sat @@ -25310,9 +25310,9 @@ Fast allSat, Looking for solution 2003 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s65) Fast allSat, Looking for solution 2004 [SEND] (check-sat) [RECV] sat @@ -25677,9 +25677,9 @@ Fast allSat, Looking for solution 2032 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s67) Fast allSat, Looking for solution 2033 [SEND] (check-sat) [RECV] sat @@ -25688,9 +25688,9 @@ Fast allSat, Looking for solution 2033 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s66) Fast allSat, Looking for solution 2034 [SEND] (check-sat) [RECV] sat @@ -25699,9 +25699,9 @@ Fast allSat, Looking for solution 2034 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s65) Fast allSat, Looking for solution 2035 [SEND] (check-sat) [RECV] sat @@ -25710,9 +25710,9 @@ Fast allSat, Looking for solution 2035 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s64) Fast allSat, Looking for solution 2036 [SEND] (check-sat) [RECV] sat @@ -25721,9 +25721,9 @@ Fast allSat, Looking for solution 2036 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 2037 [SEND] (check-sat) [RECV] sat @@ -25732,9 +25732,9 @@ Fast allSat, Looking for solution 2037 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s62) Fast allSat, Looking for solution 2038 [SEND] (check-sat) [RECV] sat @@ -25743,9 +25743,9 @@ Fast allSat, Looking for solution 2038 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s61) Fast allSat, Looking for solution 2039 [SEND] (check-sat) [RECV] sat @@ -25754,9 +25754,9 @@ Fast allSat, Looking for solution 2039 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s60) Fast allSat, Looking for solution 2040 [SEND] (check-sat) [RECV] sat @@ -25765,9 +25765,9 @@ Fast allSat, Looking for solution 2040 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s58) Fast allSat, Looking for solution 2041 [SEND] (check-sat) [RECV] sat @@ -25776,9 +25776,9 @@ Fast allSat, Looking for solution 2041 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s72) Fast allSat, Looking for solution 2042 [SEND] (check-sat) [RECV] sat @@ -26003,9 +26003,9 @@ Fast allSat, Looking for solution 2058 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s60) Fast allSat, Looking for solution 2059 [SEND] (check-sat) [RECV] sat @@ -26014,9 +26014,9 @@ Fast allSat, Looking for solution 2059 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s61) Fast allSat, Looking for solution 2060 [SEND] (check-sat) [RECV] sat @@ -26025,9 +26025,9 @@ Fast allSat, Looking for solution 2060 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s62) Fast allSat, Looking for solution 2061 [SEND] (check-sat) [RECV] sat @@ -26036,9 +26036,9 @@ Fast allSat, Looking for solution 2061 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s63) Fast allSat, Looking for solution 2062 [SEND] (check-sat) [RECV] sat @@ -26047,9 +26047,9 @@ Fast allSat, Looking for solution 2062 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s64) Fast allSat, Looking for solution 2063 [SEND] (check-sat) [RECV] sat @@ -26058,9 +26058,9 @@ Fast allSat, Looking for solution 2063 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s65) Fast allSat, Looking for solution 2064 [SEND] (check-sat) [RECV] sat @@ -26069,9 +26069,9 @@ Fast allSat, Looking for solution 2064 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s66) Fast allSat, Looking for solution 2065 [SEND] (check-sat) [RECV] sat @@ -26080,9 +26080,9 @@ Fast allSat, Looking for solution 2065 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s67) Fast allSat, Looking for solution 2066 [SEND] (check-sat) [RECV] sat @@ -26155,9 +26155,9 @@ Fast allSat, Looking for solution 2070 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s58) Fast allSat, Looking for solution 2071 [SEND] (check-sat) [RECV] sat @@ -26166,9 +26166,9 @@ Fast allSat, Looking for solution 2071 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s72) Fast allSat, Looking for solution 2072 [SEND] (check-sat) [RECV] sat @@ -26177,9 +26177,9 @@ Fast allSat, Looking for solution 2072 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s89) Fast allSat, Looking for solution 2073 [SEND] (check-sat) [RECV] sat @@ -26188,9 +26188,9 @@ Fast allSat, Looking for solution 2073 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s61) Fast allSat, Looking for solution 2074 [SEND] (check-sat) [RECV] sat @@ -26199,9 +26199,9 @@ Fast allSat, Looking for solution 2074 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s62) Fast allSat, Looking for solution 2075 [SEND] (check-sat) [RECV] sat @@ -26210,9 +26210,9 @@ Fast allSat, Looking for solution 2075 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 2076 [SEND] (check-sat) [RECV] sat @@ -26221,9 +26221,9 @@ Fast allSat, Looking for solution 2076 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s64) Fast allSat, Looking for solution 2077 [SEND] (check-sat) [RECV] sat @@ -26232,9 +26232,9 @@ Fast allSat, Looking for solution 2077 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s65) Fast allSat, Looking for solution 2078 [SEND] (check-sat) [RECV] sat @@ -26243,9 +26243,9 @@ Fast allSat, Looking for solution 2078 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s66) Fast allSat, Looking for solution 2079 [SEND] (check-sat) [RECV] sat @@ -26254,9 +26254,9 @@ Fast allSat, Looking for solution 2079 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s67) Fast allSat, Looking for solution 2080 [SEND] (check-sat) [RECV] unsat @@ -26285,9 +26285,9 @@ Fast allSat, Looking for solution 2080 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s62) Fast allSat, Looking for solution 2081 [SEND] (check-sat) [RECV] sat @@ -26296,9 +26296,9 @@ Fast allSat, Looking for solution 2081 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s63) Fast allSat, Looking for solution 2082 [SEND] (check-sat) [RECV] sat @@ -26307,9 +26307,9 @@ Fast allSat, Looking for solution 2082 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s64) Fast allSat, Looking for solution 2083 [SEND] (check-sat) [RECV] sat @@ -26318,9 +26318,9 @@ Fast allSat, Looking for solution 2083 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s65) Fast allSat, Looking for solution 2084 [SEND] (check-sat) [RECV] sat @@ -26329,9 +26329,9 @@ Fast allSat, Looking for solution 2084 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s66) Fast allSat, Looking for solution 2085 [SEND] (check-sat) [RECV] sat @@ -26340,9 +26340,9 @@ Fast allSat, Looking for solution 2085 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s67) Fast allSat, Looking for solution 2086 [SEND] (check-sat) [RECV] sat @@ -26351,9 +26351,9 @@ Fast allSat, Looking for solution 2086 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s60) Fast allSat, Looking for solution 2087 [SEND] (check-sat) [RECV] sat @@ -26362,9 +26362,9 @@ Fast allSat, Looking for solution 2087 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s58) Fast allSat, Looking for solution 2088 [SEND] (check-sat) [RECV] sat @@ -26373,9 +26373,9 @@ Fast allSat, Looking for solution 2088 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s72) Fast allSat, Looking for solution 2089 [SEND] (check-sat) [RECV] sat @@ -26384,9 +26384,9 @@ Fast allSat, Looking for solution 2089 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s89) Fast allSat, Looking for solution 2090 [SEND] (check-sat) [RECV] sat @@ -26459,9 +26459,9 @@ Fast allSat, Looking for solution 2094 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s61) Fast allSat, Looking for solution 2095 [SEND] (check-sat) [RECV] sat @@ -26470,9 +26470,9 @@ Fast allSat, Looking for solution 2095 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s60) Fast allSat, Looking for solution 2096 [SEND] (check-sat) [RECV] sat @@ -26481,9 +26481,9 @@ Fast allSat, Looking for solution 2096 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s58) Fast allSat, Looking for solution 2097 [SEND] (check-sat) [RECV] sat @@ -26492,9 +26492,9 @@ Fast allSat, Looking for solution 2097 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s72) Fast allSat, Looking for solution 2098 [SEND] (check-sat) [RECV] sat @@ -26503,9 +26503,9 @@ Fast allSat, Looking for solution 2098 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s89) Fast allSat, Looking for solution 2099 [SEND] (check-sat) [RECV] sat @@ -26514,9 +26514,9 @@ Fast allSat, Looking for solution 2099 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s63) Fast allSat, Looking for solution 2100 [SEND] (check-sat) [RECV] sat @@ -26525,9 +26525,9 @@ Fast allSat, Looking for solution 2100 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s64) Fast allSat, Looking for solution 2101 [SEND] (check-sat) [RECV] sat @@ -26536,9 +26536,9 @@ Fast allSat, Looking for solution 2101 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s65) Fast allSat, Looking for solution 2102 [SEND] (check-sat) [RECV] sat @@ -26547,9 +26547,9 @@ Fast allSat, Looking for solution 2102 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s66) Fast allSat, Looking for solution 2103 [SEND] (check-sat) [RECV] sat @@ -26558,9 +26558,9 @@ Fast allSat, Looking for solution 2103 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s67) Fast allSat, Looking for solution 2104 [SEND] (check-sat) [RECV] unsat @@ -26589,9 +26589,9 @@ Fast allSat, Looking for solution 2104 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s64) Fast allSat, Looking for solution 2105 [SEND] (check-sat) [RECV] sat @@ -26600,9 +26600,9 @@ Fast allSat, Looking for solution 2105 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s65) Fast allSat, Looking for solution 2106 [SEND] (check-sat) [RECV] sat @@ -26611,9 +26611,9 @@ Fast allSat, Looking for solution 2106 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s66) Fast allSat, Looking for solution 2107 [SEND] (check-sat) [RECV] sat @@ -26622,9 +26622,9 @@ Fast allSat, Looking for solution 2107 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s67) Fast allSat, Looking for solution 2108 [SEND] (check-sat) [RECV] sat @@ -26633,9 +26633,9 @@ Fast allSat, Looking for solution 2108 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s62) Fast allSat, Looking for solution 2109 [SEND] (check-sat) [RECV] sat @@ -26644,9 +26644,9 @@ Fast allSat, Looking for solution 2109 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s61) Fast allSat, Looking for solution 2110 [SEND] (check-sat) [RECV] sat @@ -26655,9 +26655,9 @@ Fast allSat, Looking for solution 2110 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s60) Fast allSat, Looking for solution 2111 [SEND] (check-sat) [RECV] sat @@ -26666,9 +26666,9 @@ Fast allSat, Looking for solution 2111 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s58) Fast allSat, Looking for solution 2112 [SEND] (check-sat) [RECV] sat @@ -26677,9 +26677,9 @@ Fast allSat, Looking for solution 2112 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s72) Fast allSat, Looking for solution 2113 [SEND] (check-sat) [RECV] sat @@ -26688,9 +26688,9 @@ Fast allSat, Looking for solution 2113 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s89) Fast allSat, Looking for solution 2114 [SEND] (check-sat) [RECV] sat @@ -26763,9 +26763,9 @@ Fast allSat, Looking for solution 2118 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s63) Fast allSat, Looking for solution 2119 [SEND] (check-sat) [RECV] sat @@ -26774,9 +26774,9 @@ Fast allSat, Looking for solution 2119 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s62) Fast allSat, Looking for solution 2120 [SEND] (check-sat) [RECV] sat @@ -26785,9 +26785,9 @@ Fast allSat, Looking for solution 2120 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s61) Fast allSat, Looking for solution 2121 [SEND] (check-sat) [RECV] sat @@ -26796,9 +26796,9 @@ Fast allSat, Looking for solution 2121 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s60) Fast allSat, Looking for solution 2122 [SEND] (check-sat) [RECV] sat @@ -26807,9 +26807,9 @@ Fast allSat, Looking for solution 2122 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s58) Fast allSat, Looking for solution 2123 [SEND] (check-sat) [RECV] sat @@ -26818,9 +26818,9 @@ Fast allSat, Looking for solution 2123 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s72) Fast allSat, Looking for solution 2124 [SEND] (check-sat) [RECV] sat @@ -26829,9 +26829,9 @@ Fast allSat, Looking for solution 2124 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s89) Fast allSat, Looking for solution 2125 [SEND] (check-sat) [RECV] sat @@ -26840,9 +26840,9 @@ Fast allSat, Looking for solution 2125 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s65) Fast allSat, Looking for solution 2126 [SEND] (check-sat) [RECV] sat @@ -26851,9 +26851,9 @@ Fast allSat, Looking for solution 2126 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s66) Fast allSat, Looking for solution 2127 [SEND] (check-sat) [RECV] sat @@ -26862,9 +26862,9 @@ Fast allSat, Looking for solution 2127 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s67) Fast allSat, Looking for solution 2128 [SEND] (check-sat) [RECV] unsat @@ -26893,9 +26893,9 @@ Fast allSat, Looking for solution 2128 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s66) Fast allSat, Looking for solution 2129 [SEND] (check-sat) [RECV] sat @@ -26904,9 +26904,9 @@ Fast allSat, Looking for solution 2129 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s67) Fast allSat, Looking for solution 2130 [SEND] (check-sat) [RECV] sat @@ -26915,9 +26915,9 @@ Fast allSat, Looking for solution 2130 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s64) Fast allSat, Looking for solution 2131 [SEND] (check-sat) [RECV] sat @@ -26926,9 +26926,9 @@ Fast allSat, Looking for solution 2131 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s63) Fast allSat, Looking for solution 2132 [SEND] (check-sat) [RECV] sat @@ -26937,9 +26937,9 @@ Fast allSat, Looking for solution 2132 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s62) Fast allSat, Looking for solution 2133 [SEND] (check-sat) [RECV] sat @@ -26948,9 +26948,9 @@ Fast allSat, Looking for solution 2133 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s61) Fast allSat, Looking for solution 2134 [SEND] (check-sat) [RECV] sat @@ -26959,9 +26959,9 @@ Fast allSat, Looking for solution 2134 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s60) Fast allSat, Looking for solution 2135 [SEND] (check-sat) [RECV] sat @@ -26970,9 +26970,9 @@ Fast allSat, Looking for solution 2135 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s58) Fast allSat, Looking for solution 2136 [SEND] (check-sat) [RECV] sat @@ -26981,9 +26981,9 @@ Fast allSat, Looking for solution 2136 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s72) Fast allSat, Looking for solution 2137 [SEND] (check-sat) [RECV] sat @@ -26992,9 +26992,9 @@ Fast allSat, Looking for solution 2137 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s89) Fast allSat, Looking for solution 2138 [SEND] (check-sat) [RECV] sat @@ -27067,21 +27067,10 @@ Fast allSat, Looking for solution 2142 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) -[GOOD] (push 1) -[GOOD] (assert s67) -Fast allSat, Looking for solution 2143 -[SEND] (check-sat) -[RECV] sat -[SEND] (get-value (s0)) -[RECV] ((s0 4)) -[SEND] (get-value (s1)) -[RECV] ((s1 6)) -[SEND] (get-value (s2)) [RECV] ((s2 7)) [GOOD] (push 1) [GOOD] (assert s65) -Fast allSat, Looking for solution 2144 +Fast allSat, Looking for solution 2143 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27092,7 +27081,7 @@ Fast allSat, Looking for solution 2144 [RECV] ((s2 8)) [GOOD] (push 1) [GOOD] (assert s64) -Fast allSat, Looking for solution 2145 +Fast allSat, Looking for solution 2144 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27103,7 +27092,7 @@ Fast allSat, Looking for solution 2145 [RECV] ((s2 9)) [GOOD] (push 1) [GOOD] (assert s63) -Fast allSat, Looking for solution 2146 +Fast allSat, Looking for solution 2145 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27114,7 +27103,7 @@ Fast allSat, Looking for solution 2146 [RECV] ((s2 10)) [GOOD] (push 1) [GOOD] (assert s62) -Fast allSat, Looking for solution 2147 +Fast allSat, Looking for solution 2146 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27125,7 +27114,7 @@ Fast allSat, Looking for solution 2147 [RECV] ((s2 11)) [GOOD] (push 1) [GOOD] (assert s61) -Fast allSat, Looking for solution 2148 +Fast allSat, Looking for solution 2147 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27136,7 +27125,7 @@ Fast allSat, Looking for solution 2148 [RECV] ((s2 12)) [GOOD] (push 1) [GOOD] (assert s60) -Fast allSat, Looking for solution 2149 +Fast allSat, Looking for solution 2148 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27147,7 +27136,7 @@ Fast allSat, Looking for solution 2149 [RECV] ((s2 13)) [GOOD] (push 1) [GOOD] (assert s58) -Fast allSat, Looking for solution 2150 +Fast allSat, Looking for solution 2149 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27158,7 +27147,7 @@ Fast allSat, Looking for solution 2150 [RECV] ((s2 14)) [GOOD] (push 1) [GOOD] (assert s72) -Fast allSat, Looking for solution 2151 +Fast allSat, Looking for solution 2150 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27169,6 +27158,17 @@ Fast allSat, Looking for solution 2151 [RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s89) +Fast allSat, Looking for solution 2151 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 4)) +[SEND] (get-value (s1)) +[RECV] ((s1 6)) +[SEND] (get-value (s2)) +[RECV] ((s2 5)) +[GOOD] (push 1) +[GOOD] (assert s67) Fast allSat, Looking for solution 2152 [SEND] (check-sat) [RECV] unsat @@ -27197,9 +27197,9 @@ Fast allSat, Looking for solution 2152 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s66) Fast allSat, Looking for solution 2153 [SEND] (check-sat) [RECV] sat @@ -27208,9 +27208,9 @@ Fast allSat, Looking for solution 2153 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s65) Fast allSat, Looking for solution 2154 [SEND] (check-sat) [RECV] sat @@ -27219,9 +27219,9 @@ Fast allSat, Looking for solution 2154 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s64) Fast allSat, Looking for solution 2155 [SEND] (check-sat) [RECV] sat @@ -27230,9 +27230,9 @@ Fast allSat, Looking for solution 2155 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s63) Fast allSat, Looking for solution 2156 [SEND] (check-sat) [RECV] sat @@ -27241,9 +27241,9 @@ Fast allSat, Looking for solution 2156 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s62) Fast allSat, Looking for solution 2157 [SEND] (check-sat) [RECV] sat @@ -27252,9 +27252,9 @@ Fast allSat, Looking for solution 2157 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s61) Fast allSat, Looking for solution 2158 [SEND] (check-sat) [RECV] sat @@ -27263,9 +27263,9 @@ Fast allSat, Looking for solution 2158 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s60) Fast allSat, Looking for solution 2159 [SEND] (check-sat) [RECV] sat @@ -27274,9 +27274,9 @@ Fast allSat, Looking for solution 2159 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s58) Fast allSat, Looking for solution 2160 [SEND] (check-sat) [RECV] sat @@ -27285,9 +27285,9 @@ Fast allSat, Looking for solution 2160 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s72) Fast allSat, Looking for solution 2161 [SEND] (check-sat) [RECV] sat @@ -27296,9 +27296,9 @@ Fast allSat, Looking for solution 2161 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s89) Fast allSat, Looking for solution 2162 [SEND] (check-sat) [RECV] sat @@ -27339,20 +27339,9 @@ Fast allSat, Looking for solution 2164 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) -[GOOD] (assert s74) -Fast allSat, Looking for solution 2164 -[SEND] (check-sat) -[RECV] sat -[SEND] (get-value (s0)) -[RECV] ((s0 4)) -[SEND] (get-value (s1)) -[RECV] ((s1 2)) -[SEND] (get-value (s2)) -[RECV] ((s2 3)) -[GOOD] (push 1) -[GOOD] (assert s69) -Fast allSat, Looking for solution 2165 +[GOOD] (assert s71) +[GOOD] (assert s74) +Fast allSat, Looking for solution 2164 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27363,7 +27352,7 @@ Fast allSat, Looking for solution 2165 [RECV] ((s2 5)) [GOOD] (push 1) [GOOD] (assert s67) -Fast allSat, Looking for solution 2166 +Fast allSat, Looking for solution 2165 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27374,7 +27363,7 @@ Fast allSat, Looking for solution 2166 [RECV] ((s2 6)) [GOOD] (push 1) [GOOD] (assert s66) -Fast allSat, Looking for solution 2167 +Fast allSat, Looking for solution 2166 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27385,7 +27374,7 @@ Fast allSat, Looking for solution 2167 [RECV] ((s2 7)) [GOOD] (push 1) [GOOD] (assert s65) -Fast allSat, Looking for solution 2168 +Fast allSat, Looking for solution 2167 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27396,7 +27385,7 @@ Fast allSat, Looking for solution 2168 [RECV] ((s2 8)) [GOOD] (push 1) [GOOD] (assert s64) -Fast allSat, Looking for solution 2169 +Fast allSat, Looking for solution 2168 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27407,7 +27396,7 @@ Fast allSat, Looking for solution 2169 [RECV] ((s2 9)) [GOOD] (push 1) [GOOD] (assert s63) -Fast allSat, Looking for solution 2170 +Fast allSat, Looking for solution 2169 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27418,7 +27407,7 @@ Fast allSat, Looking for solution 2170 [RECV] ((s2 10)) [GOOD] (push 1) [GOOD] (assert s62) -Fast allSat, Looking for solution 2171 +Fast allSat, Looking for solution 2170 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27429,7 +27418,7 @@ Fast allSat, Looking for solution 2171 [RECV] ((s2 11)) [GOOD] (push 1) [GOOD] (assert s61) -Fast allSat, Looking for solution 2172 +Fast allSat, Looking for solution 2171 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27440,7 +27429,7 @@ Fast allSat, Looking for solution 2172 [RECV] ((s2 12)) [GOOD] (push 1) [GOOD] (assert s60) -Fast allSat, Looking for solution 2173 +Fast allSat, Looking for solution 2172 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27451,7 +27440,7 @@ Fast allSat, Looking for solution 2173 [RECV] ((s2 13)) [GOOD] (push 1) [GOOD] (assert s58) -Fast allSat, Looking for solution 2174 +Fast allSat, Looking for solution 2173 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27462,7 +27451,7 @@ Fast allSat, Looking for solution 2174 [RECV] ((s2 14)) [GOOD] (push 1) [GOOD] (assert s72) -Fast allSat, Looking for solution 2175 +Fast allSat, Looking for solution 2174 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -27473,6 +27462,17 @@ Fast allSat, Looking for solution 2175 [RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s89) +Fast allSat, Looking for solution 2175 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 4)) +[SEND] (get-value (s1)) +[RECV] ((s1 2)) +[SEND] (get-value (s2)) +[RECV] ((s2 3)) +[GOOD] (push 1) +[GOOD] (assert s69) Fast allSat, Looking for solution 2176 [SEND] (check-sat) [RECV] unsat @@ -27502,9 +27502,9 @@ Fast allSat, Looking for solution 2176 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s70) Fast allSat, Looking for solution 2177 [SEND] (check-sat) [RECV] sat @@ -27513,9 +27513,9 @@ Fast allSat, Looking for solution 2177 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s71) Fast allSat, Looking for solution 2178 [SEND] (check-sat) [RECV] sat @@ -27524,9 +27524,9 @@ Fast allSat, Looking for solution 2178 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s66) Fast allSat, Looking for solution 2179 [SEND] (check-sat) [RECV] sat @@ -27535,9 +27535,9 @@ Fast allSat, Looking for solution 2179 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s65) Fast allSat, Looking for solution 2180 [SEND] (check-sat) [RECV] sat @@ -27546,9 +27546,9 @@ Fast allSat, Looking for solution 2180 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s64) Fast allSat, Looking for solution 2181 [SEND] (check-sat) [RECV] sat @@ -27557,9 +27557,9 @@ Fast allSat, Looking for solution 2181 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 2182 [SEND] (check-sat) [RECV] sat @@ -27568,9 +27568,9 @@ Fast allSat, Looking for solution 2182 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s62) Fast allSat, Looking for solution 2183 [SEND] (check-sat) [RECV] sat @@ -27579,9 +27579,9 @@ Fast allSat, Looking for solution 2183 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s61) Fast allSat, Looking for solution 2184 [SEND] (check-sat) [RECV] sat @@ -27590,9 +27590,9 @@ Fast allSat, Looking for solution 2184 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s60) Fast allSat, Looking for solution 2185 [SEND] (check-sat) [RECV] sat @@ -27601,9 +27601,9 @@ Fast allSat, Looking for solution 2185 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s58) Fast allSat, Looking for solution 2186 [SEND] (check-sat) [RECV] sat @@ -27612,9 +27612,9 @@ Fast allSat, Looking for solution 2186 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s72) Fast allSat, Looking for solution 2187 [SEND] (check-sat) [RECV] sat @@ -27623,9 +27623,9 @@ Fast allSat, Looking for solution 2187 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) Fast allSat, Looking for solution 2188 [SEND] (check-sat) [RECV] unsat @@ -27655,7 +27655,7 @@ Fast allSat, Looking for solution 2188 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s54) Fast allSat, Looking for solution 2189 @@ -27666,7 +27666,7 @@ Fast allSat, Looking for solution 2189 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s53) Fast allSat, Looking for solution 2190 @@ -27677,7 +27677,7 @@ Fast allSat, Looking for solution 2190 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s52) Fast allSat, Looking for solution 2191 @@ -27688,7 +27688,7 @@ Fast allSat, Looking for solution 2191 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s51) Fast allSat, Looking for solution 2192 @@ -27699,7 +27699,7 @@ Fast allSat, Looking for solution 2192 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s50) Fast allSat, Looking for solution 2193 @@ -27710,7 +27710,7 @@ Fast allSat, Looking for solution 2193 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s49) Fast allSat, Looking for solution 2194 @@ -27721,7 +27721,7 @@ Fast allSat, Looking for solution 2194 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s48) Fast allSat, Looking for solution 2195 @@ -27732,7 +27732,7 @@ Fast allSat, Looking for solution 2195 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s47) Fast allSat, Looking for solution 2196 @@ -27743,7 +27743,7 @@ Fast allSat, Looking for solution 2196 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s46) Fast allSat, Looking for solution 2197 @@ -27754,7 +27754,7 @@ Fast allSat, Looking for solution 2197 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s45) Fast allSat, Looking for solution 2198 @@ -27765,7 +27765,7 @@ Fast allSat, Looking for solution 2198 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s43) Fast allSat, Looking for solution 2199 @@ -27776,7 +27776,7 @@ Fast allSat, Looking for solution 2199 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 15)) [GOOD] (push 1) [GOOD] (assert s57) Fast allSat, Looking for solution 2200 @@ -27787,7 +27787,7 @@ Fast allSat, Looking for solution 2200 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 1)) +[RECV] ((s2 14)) [GOOD] (push 1) [GOOD] (assert s87) Fast allSat, Looking for solution 2201 @@ -27795,7 +27795,7 @@ Fast allSat, Looking for solution 2201 [RECV] unsat [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s72) [GOOD] (assert s88) Fast allSat, Looking for solution 2201 [SEND] (check-sat) @@ -27805,9 +27805,9 @@ Fast allSat, Looking for solution 2201 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s58) Fast allSat, Looking for solution 2202 [SEND] (check-sat) [RECV] sat @@ -27816,9 +27816,9 @@ Fast allSat, Looking for solution 2202 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s60) Fast allSat, Looking for solution 2203 [SEND] (check-sat) [RECV] sat @@ -27827,9 +27827,9 @@ Fast allSat, Looking for solution 2203 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s61) Fast allSat, Looking for solution 2204 [SEND] (check-sat) [RECV] sat @@ -27838,9 +27838,9 @@ Fast allSat, Looking for solution 2204 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s62) Fast allSat, Looking for solution 2205 [SEND] (check-sat) [RECV] sat @@ -27849,9 +27849,9 @@ Fast allSat, Looking for solution 2205 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s63) Fast allSat, Looking for solution 2206 [SEND] (check-sat) [RECV] sat @@ -27871,9 +27871,9 @@ Fast allSat, Looking for solution 2207 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s65) Fast allSat, Looking for solution 2208 [SEND] (check-sat) [RECV] sat @@ -27882,9 +27882,9 @@ Fast allSat, Looking for solution 2208 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s66) Fast allSat, Looking for solution 2209 [SEND] (check-sat) [RECV] sat @@ -27893,9 +27893,9 @@ Fast allSat, Looking for solution 2209 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s67) Fast allSat, Looking for solution 2210 [SEND] (check-sat) [RECV] sat @@ -27904,9 +27904,9 @@ Fast allSat, Looking for solution 2210 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s68) Fast allSat, Looking for solution 2211 [SEND] (check-sat) [RECV] sat @@ -27915,9 +27915,9 @@ Fast allSat, Looking for solution 2211 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s69) Fast allSat, Looking for solution 2212 [SEND] (check-sat) [RECV] sat @@ -27926,9 +27926,9 @@ Fast allSat, Looking for solution 2212 [SEND] (get-value (s1)) [RECV] ((s1 15)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s71) Fast allSat, Looking for solution 2213 [SEND] (check-sat) [RECV] unsat @@ -27947,7 +27947,7 @@ Fast allSat, Looking for solution 2213 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) [GOOD] (assert s59) Fast allSat, Looking for solution 2213 [SEND] (check-sat) @@ -27957,9 +27957,9 @@ Fast allSat, Looking for solution 2213 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s71) Fast allSat, Looking for solution 2214 [SEND] (check-sat) [RECV] sat @@ -27968,9 +27968,9 @@ Fast allSat, Looking for solution 2214 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s69) Fast allSat, Looking for solution 2215 [SEND] (check-sat) [RECV] sat @@ -27979,9 +27979,9 @@ Fast allSat, Looking for solution 2215 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s68) Fast allSat, Looking for solution 2216 [SEND] (check-sat) [RECV] sat @@ -27990,9 +27990,9 @@ Fast allSat, Looking for solution 2216 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s67) Fast allSat, Looking for solution 2217 [SEND] (check-sat) [RECV] sat @@ -28001,9 +28001,9 @@ Fast allSat, Looking for solution 2217 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s66) Fast allSat, Looking for solution 2218 [SEND] (check-sat) [RECV] sat @@ -28012,9 +28012,9 @@ Fast allSat, Looking for solution 2218 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s65) Fast allSat, Looking for solution 2219 [SEND] (check-sat) [RECV] sat @@ -28023,9 +28023,9 @@ Fast allSat, Looking for solution 2219 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s64) Fast allSat, Looking for solution 2220 [SEND] (check-sat) [RECV] sat @@ -28034,9 +28034,9 @@ Fast allSat, Looking for solution 2220 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s63) Fast allSat, Looking for solution 2221 [SEND] (check-sat) [RECV] sat @@ -28045,9 +28045,9 @@ Fast allSat, Looking for solution 2221 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s62) Fast allSat, Looking for solution 2222 [SEND] (check-sat) [RECV] sat @@ -28056,9 +28056,9 @@ Fast allSat, Looking for solution 2222 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s61) Fast allSat, Looking for solution 2223 [SEND] (check-sat) [RECV] sat @@ -28067,9 +28067,9 @@ Fast allSat, Looking for solution 2223 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s60) Fast allSat, Looking for solution 2224 [SEND] (check-sat) [RECV] sat @@ -28078,9 +28078,9 @@ Fast allSat, Looking for solution 2224 [SEND] (get-value (s1)) [RECV] ((s1 14)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s58) Fast allSat, Looking for solution 2225 [SEND] (check-sat) [RECV] unsat @@ -28099,7 +28099,7 @@ Fast allSat, Looking for solution 2225 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) [GOOD] (assert s85) Fast allSat, Looking for solution 2225 [SEND] (check-sat) @@ -28109,9 +28109,9 @@ Fast allSat, Looking for solution 2225 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s60) Fast allSat, Looking for solution 2226 [SEND] (check-sat) [RECV] sat @@ -28120,9 +28120,9 @@ Fast allSat, Looking for solution 2226 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s61) Fast allSat, Looking for solution 2227 [SEND] (check-sat) [RECV] sat @@ -28131,9 +28131,9 @@ Fast allSat, Looking for solution 2227 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s62) Fast allSat, Looking for solution 2228 [SEND] (check-sat) [RECV] sat @@ -28142,9 +28142,9 @@ Fast allSat, Looking for solution 2228 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s63) Fast allSat, Looking for solution 2229 [SEND] (check-sat) [RECV] sat @@ -28153,9 +28153,9 @@ Fast allSat, Looking for solution 2229 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s64) Fast allSat, Looking for solution 2230 [SEND] (check-sat) [RECV] sat @@ -28164,9 +28164,9 @@ Fast allSat, Looking for solution 2230 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s65) Fast allSat, Looking for solution 2231 [SEND] (check-sat) [RECV] sat @@ -28175,9 +28175,9 @@ Fast allSat, Looking for solution 2231 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s66) Fast allSat, Looking for solution 2232 [SEND] (check-sat) [RECV] sat @@ -28186,9 +28186,9 @@ Fast allSat, Looking for solution 2232 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s67) Fast allSat, Looking for solution 2233 [SEND] (check-sat) [RECV] sat @@ -28197,9 +28197,9 @@ Fast allSat, Looking for solution 2233 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s68) Fast allSat, Looking for solution 2234 [SEND] (check-sat) [RECV] sat @@ -28208,9 +28208,9 @@ Fast allSat, Looking for solution 2234 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s69) Fast allSat, Looking for solution 2235 [SEND] (check-sat) [RECV] sat @@ -28219,9 +28219,9 @@ Fast allSat, Looking for solution 2235 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s72) Fast allSat, Looking for solution 2236 [SEND] (check-sat) [RECV] sat @@ -28230,9 +28230,9 @@ Fast allSat, Looking for solution 2236 [SEND] (get-value (s1)) [RECV] ((s1 13)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s71) Fast allSat, Looking for solution 2237 [SEND] (check-sat) [RECV] unsat @@ -28251,7 +28251,7 @@ Fast allSat, Looking for solution 2237 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) [GOOD] (assert s84) Fast allSat, Looking for solution 2237 [SEND] (check-sat) @@ -28261,9 +28261,9 @@ Fast allSat, Looking for solution 2237 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s71) Fast allSat, Looking for solution 2238 [SEND] (check-sat) [RECV] sat @@ -28272,9 +28272,9 @@ Fast allSat, Looking for solution 2238 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s69) Fast allSat, Looking for solution 2239 [SEND] (check-sat) [RECV] sat @@ -28283,9 +28283,9 @@ Fast allSat, Looking for solution 2239 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s68) Fast allSat, Looking for solution 2240 [SEND] (check-sat) [RECV] sat @@ -28294,9 +28294,9 @@ Fast allSat, Looking for solution 2240 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s67) Fast allSat, Looking for solution 2241 [SEND] (check-sat) [RECV] sat @@ -28305,9 +28305,9 @@ Fast allSat, Looking for solution 2241 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s66) Fast allSat, Looking for solution 2242 [SEND] (check-sat) [RECV] sat @@ -28316,9 +28316,9 @@ Fast allSat, Looking for solution 2242 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s65) Fast allSat, Looking for solution 2243 [SEND] (check-sat) [RECV] sat @@ -28327,9 +28327,9 @@ Fast allSat, Looking for solution 2243 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s64) Fast allSat, Looking for solution 2244 [SEND] (check-sat) [RECV] sat @@ -28338,9 +28338,9 @@ Fast allSat, Looking for solution 2244 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s63) Fast allSat, Looking for solution 2245 [SEND] (check-sat) [RECV] sat @@ -28349,9 +28349,9 @@ Fast allSat, Looking for solution 2245 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s62) Fast allSat, Looking for solution 2246 [SEND] (check-sat) [RECV] sat @@ -28360,9 +28360,9 @@ Fast allSat, Looking for solution 2246 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s61) Fast allSat, Looking for solution 2247 [SEND] (check-sat) [RECV] sat @@ -28371,9 +28371,9 @@ Fast allSat, Looking for solution 2247 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s58) Fast allSat, Looking for solution 2248 [SEND] (check-sat) [RECV] sat @@ -28382,9 +28382,9 @@ Fast allSat, Looking for solution 2248 [SEND] (get-value (s1)) [RECV] ((s1 12)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s72) Fast allSat, Looking for solution 2249 [SEND] (check-sat) [RECV] unsat @@ -28403,7 +28403,7 @@ Fast allSat, Looking for solution 2249 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) [GOOD] (assert s83) Fast allSat, Looking for solution 2249 [SEND] (check-sat) @@ -28413,21 +28413,10 @@ Fast allSat, Looking for solution 2249 [SEND] (get-value (s1)) [RECV] ((s1 11)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) -[GOOD] (push 1) -[GOOD] (assert s89) -Fast allSat, Looking for solution 2250 -[SEND] (check-sat) -[RECV] sat -[SEND] (get-value (s0)) -[RECV] ((s0 2)) -[SEND] (get-value (s1)) -[RECV] ((s1 11)) -[SEND] (get-value (s2)) [RECV] ((s2 14)) [GOOD] (push 1) [GOOD] (assert s72) -Fast allSat, Looking for solution 2251 +Fast allSat, Looking for solution 2250 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28438,7 +28427,7 @@ Fast allSat, Looking for solution 2251 [RECV] ((s2 13)) [GOOD] (push 1) [GOOD] (assert s58) -Fast allSat, Looking for solution 2252 +Fast allSat, Looking for solution 2251 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28449,7 +28438,7 @@ Fast allSat, Looking for solution 2252 [RECV] ((s2 12)) [GOOD] (push 1) [GOOD] (assert s60) -Fast allSat, Looking for solution 2253 +Fast allSat, Looking for solution 2252 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28460,7 +28449,7 @@ Fast allSat, Looking for solution 2253 [RECV] ((s2 10)) [GOOD] (push 1) [GOOD] (assert s62) -Fast allSat, Looking for solution 2254 +Fast allSat, Looking for solution 2253 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28471,7 +28460,7 @@ Fast allSat, Looking for solution 2254 [RECV] ((s2 9)) [GOOD] (push 1) [GOOD] (assert s63) -Fast allSat, Looking for solution 2255 +Fast allSat, Looking for solution 2254 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28482,7 +28471,7 @@ Fast allSat, Looking for solution 2255 [RECV] ((s2 8)) [GOOD] (push 1) [GOOD] (assert s64) -Fast allSat, Looking for solution 2256 +Fast allSat, Looking for solution 2255 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28493,7 +28482,7 @@ Fast allSat, Looking for solution 2256 [RECV] ((s2 7)) [GOOD] (push 1) [GOOD] (assert s65) -Fast allSat, Looking for solution 2257 +Fast allSat, Looking for solution 2256 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28504,7 +28493,7 @@ Fast allSat, Looking for solution 2257 [RECV] ((s2 6)) [GOOD] (push 1) [GOOD] (assert s66) -Fast allSat, Looking for solution 2258 +Fast allSat, Looking for solution 2257 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28515,7 +28504,7 @@ Fast allSat, Looking for solution 2258 [RECV] ((s2 5)) [GOOD] (push 1) [GOOD] (assert s67) -Fast allSat, Looking for solution 2259 +Fast allSat, Looking for solution 2258 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28526,7 +28515,7 @@ Fast allSat, Looking for solution 2259 [RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s68) -Fast allSat, Looking for solution 2260 +Fast allSat, Looking for solution 2259 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28537,6 +28526,17 @@ Fast allSat, Looking for solution 2260 [RECV] ((s2 3)) [GOOD] (push 1) [GOOD] (assert s69) +Fast allSat, Looking for solution 2260 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 2)) +[SEND] (get-value (s1)) +[RECV] ((s1 11)) +[SEND] (get-value (s2)) +[RECV] ((s2 1)) +[GOOD] (push 1) +[GOOD] (assert s71) Fast allSat, Looking for solution 2261 [SEND] (check-sat) [RECV] unsat @@ -28555,7 +28555,7 @@ Fast allSat, Looking for solution 2261 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) [GOOD] (assert s82) Fast allSat, Looking for solution 2261 [SEND] (check-sat) @@ -28565,9 +28565,9 @@ Fast allSat, Looking for solution 2261 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s71) Fast allSat, Looking for solution 2262 [SEND] (check-sat) [RECV] sat @@ -28576,9 +28576,9 @@ Fast allSat, Looking for solution 2262 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s69) Fast allSat, Looking for solution 2263 [SEND] (check-sat) [RECV] sat @@ -28587,9 +28587,9 @@ Fast allSat, Looking for solution 2263 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s68) Fast allSat, Looking for solution 2264 [SEND] (check-sat) [RECV] sat @@ -28598,9 +28598,9 @@ Fast allSat, Looking for solution 2264 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s67) Fast allSat, Looking for solution 2265 [SEND] (check-sat) [RECV] sat @@ -28609,9 +28609,9 @@ Fast allSat, Looking for solution 2265 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s66) Fast allSat, Looking for solution 2266 [SEND] (check-sat) [RECV] sat @@ -28620,9 +28620,9 @@ Fast allSat, Looking for solution 2266 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s65) Fast allSat, Looking for solution 2267 [SEND] (check-sat) [RECV] sat @@ -28631,9 +28631,9 @@ Fast allSat, Looking for solution 2267 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s64) Fast allSat, Looking for solution 2268 [SEND] (check-sat) [RECV] sat @@ -28642,9 +28642,9 @@ Fast allSat, Looking for solution 2268 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s63) Fast allSat, Looking for solution 2269 [SEND] (check-sat) [RECV] sat @@ -28653,9 +28653,9 @@ Fast allSat, Looking for solution 2269 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s61) Fast allSat, Looking for solution 2270 [SEND] (check-sat) [RECV] sat @@ -28664,9 +28664,9 @@ Fast allSat, Looking for solution 2270 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s60) Fast allSat, Looking for solution 2271 [SEND] (check-sat) [RECV] sat @@ -28675,9 +28675,9 @@ Fast allSat, Looking for solution 2271 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s58) Fast allSat, Looking for solution 2272 [SEND] (check-sat) [RECV] sat @@ -28686,9 +28686,9 @@ Fast allSat, Looking for solution 2272 [SEND] (get-value (s1)) [RECV] ((s1 10)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s72) Fast allSat, Looking for solution 2273 [SEND] (check-sat) [RECV] unsat @@ -28707,7 +28707,7 @@ Fast allSat, Looking for solution 2273 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) [GOOD] (assert s81) Fast allSat, Looking for solution 2273 [SEND] (check-sat) @@ -28717,21 +28717,10 @@ Fast allSat, Looking for solution 2273 [SEND] (get-value (s1)) [RECV] ((s1 9)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) -[GOOD] (push 1) -[GOOD] (assert s89) -Fast allSat, Looking for solution 2274 -[SEND] (check-sat) -[RECV] sat -[SEND] (get-value (s0)) -[RECV] ((s0 2)) -[SEND] (get-value (s1)) -[RECV] ((s1 9)) -[SEND] (get-value (s2)) [RECV] ((s2 14)) [GOOD] (push 1) [GOOD] (assert s72) -Fast allSat, Looking for solution 2275 +Fast allSat, Looking for solution 2274 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28742,7 +28731,7 @@ Fast allSat, Looking for solution 2275 [RECV] ((s2 13)) [GOOD] (push 1) [GOOD] (assert s58) -Fast allSat, Looking for solution 2276 +Fast allSat, Looking for solution 2275 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28753,7 +28742,7 @@ Fast allSat, Looking for solution 2276 [RECV] ((s2 12)) [GOOD] (push 1) [GOOD] (assert s60) -Fast allSat, Looking for solution 2277 +Fast allSat, Looking for solution 2276 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28764,7 +28753,7 @@ Fast allSat, Looking for solution 2277 [RECV] ((s2 11)) [GOOD] (push 1) [GOOD] (assert s61) -Fast allSat, Looking for solution 2278 +Fast allSat, Looking for solution 2277 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28775,7 +28764,7 @@ Fast allSat, Looking for solution 2278 [RECV] ((s2 10)) [GOOD] (push 1) [GOOD] (assert s62) -Fast allSat, Looking for solution 2279 +Fast allSat, Looking for solution 2278 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28786,7 +28775,7 @@ Fast allSat, Looking for solution 2279 [RECV] ((s2 8)) [GOOD] (push 1) [GOOD] (assert s64) -Fast allSat, Looking for solution 2280 +Fast allSat, Looking for solution 2279 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28797,7 +28786,7 @@ Fast allSat, Looking for solution 2280 [RECV] ((s2 7)) [GOOD] (push 1) [GOOD] (assert s65) -Fast allSat, Looking for solution 2281 +Fast allSat, Looking for solution 2280 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28808,7 +28797,7 @@ Fast allSat, Looking for solution 2281 [RECV] ((s2 6)) [GOOD] (push 1) [GOOD] (assert s66) -Fast allSat, Looking for solution 2282 +Fast allSat, Looking for solution 2281 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28819,7 +28808,7 @@ Fast allSat, Looking for solution 2282 [RECV] ((s2 5)) [GOOD] (push 1) [GOOD] (assert s67) -Fast allSat, Looking for solution 2283 +Fast allSat, Looking for solution 2282 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28830,7 +28819,7 @@ Fast allSat, Looking for solution 2283 [RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s68) -Fast allSat, Looking for solution 2284 +Fast allSat, Looking for solution 2283 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -28841,6 +28830,17 @@ Fast allSat, Looking for solution 2284 [RECV] ((s2 3)) [GOOD] (push 1) [GOOD] (assert s69) +Fast allSat, Looking for solution 2284 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 2)) +[SEND] (get-value (s1)) +[RECV] ((s1 9)) +[SEND] (get-value (s2)) +[RECV] ((s2 1)) +[GOOD] (push 1) +[GOOD] (assert s71) Fast allSat, Looking for solution 2285 [SEND] (check-sat) [RECV] unsat @@ -28859,7 +28859,7 @@ Fast allSat, Looking for solution 2285 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) [GOOD] (assert s80) Fast allSat, Looking for solution 2285 [SEND] (check-sat) @@ -28869,9 +28869,9 @@ Fast allSat, Looking for solution 2285 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s71) Fast allSat, Looking for solution 2286 [SEND] (check-sat) [RECV] sat @@ -28880,9 +28880,9 @@ Fast allSat, Looking for solution 2286 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s69) Fast allSat, Looking for solution 2287 [SEND] (check-sat) [RECV] sat @@ -28891,9 +28891,9 @@ Fast allSat, Looking for solution 2287 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s68) Fast allSat, Looking for solution 2288 [SEND] (check-sat) [RECV] sat @@ -28902,9 +28902,9 @@ Fast allSat, Looking for solution 2288 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s67) Fast allSat, Looking for solution 2289 [SEND] (check-sat) [RECV] sat @@ -28913,9 +28913,9 @@ Fast allSat, Looking for solution 2289 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s66) Fast allSat, Looking for solution 2290 [SEND] (check-sat) [RECV] sat @@ -28924,9 +28924,9 @@ Fast allSat, Looking for solution 2290 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s65) Fast allSat, Looking for solution 2291 [SEND] (check-sat) [RECV] sat @@ -28935,9 +28935,9 @@ Fast allSat, Looking for solution 2291 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 2292 [SEND] (check-sat) [RECV] sat @@ -28946,9 +28946,9 @@ Fast allSat, Looking for solution 2292 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s62) Fast allSat, Looking for solution 2293 [SEND] (check-sat) [RECV] sat @@ -28957,9 +28957,9 @@ Fast allSat, Looking for solution 2293 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s61) Fast allSat, Looking for solution 2294 [SEND] (check-sat) [RECV] sat @@ -28968,9 +28968,9 @@ Fast allSat, Looking for solution 2294 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s60) Fast allSat, Looking for solution 2295 [SEND] (check-sat) [RECV] sat @@ -28979,9 +28979,9 @@ Fast allSat, Looking for solution 2295 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s58) Fast allSat, Looking for solution 2296 [SEND] (check-sat) [RECV] sat @@ -28990,9 +28990,9 @@ Fast allSat, Looking for solution 2296 [SEND] (get-value (s1)) [RECV] ((s1 8)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s72) Fast allSat, Looking for solution 2297 [SEND] (check-sat) [RECV] unsat @@ -29011,7 +29011,7 @@ Fast allSat, Looking for solution 2297 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) [GOOD] (assert s79) Fast allSat, Looking for solution 2297 [SEND] (check-sat) @@ -29021,21 +29021,10 @@ Fast allSat, Looking for solution 2297 [SEND] (get-value (s1)) [RECV] ((s1 7)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) -[GOOD] (push 1) -[GOOD] (assert s89) -Fast allSat, Looking for solution 2298 -[SEND] (check-sat) -[RECV] sat -[SEND] (get-value (s0)) -[RECV] ((s0 2)) -[SEND] (get-value (s1)) -[RECV] ((s1 7)) -[SEND] (get-value (s2)) [RECV] ((s2 14)) [GOOD] (push 1) [GOOD] (assert s72) -Fast allSat, Looking for solution 2299 +Fast allSat, Looking for solution 2298 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29046,7 +29035,7 @@ Fast allSat, Looking for solution 2299 [RECV] ((s2 13)) [GOOD] (push 1) [GOOD] (assert s58) -Fast allSat, Looking for solution 2300 +Fast allSat, Looking for solution 2299 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29057,7 +29046,7 @@ Fast allSat, Looking for solution 2300 [RECV] ((s2 12)) [GOOD] (push 1) [GOOD] (assert s60) -Fast allSat, Looking for solution 2301 +Fast allSat, Looking for solution 2300 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29068,7 +29057,7 @@ Fast allSat, Looking for solution 2301 [RECV] ((s2 11)) [GOOD] (push 1) [GOOD] (assert s61) -Fast allSat, Looking for solution 2302 +Fast allSat, Looking for solution 2301 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29079,7 +29068,7 @@ Fast allSat, Looking for solution 2302 [RECV] ((s2 10)) [GOOD] (push 1) [GOOD] (assert s62) -Fast allSat, Looking for solution 2303 +Fast allSat, Looking for solution 2302 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29090,7 +29079,7 @@ Fast allSat, Looking for solution 2303 [RECV] ((s2 9)) [GOOD] (push 1) [GOOD] (assert s63) -Fast allSat, Looking for solution 2304 +Fast allSat, Looking for solution 2303 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29101,7 +29090,7 @@ Fast allSat, Looking for solution 2304 [RECV] ((s2 8)) [GOOD] (push 1) [GOOD] (assert s64) -Fast allSat, Looking for solution 2305 +Fast allSat, Looking for solution 2304 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29112,7 +29101,7 @@ Fast allSat, Looking for solution 2305 [RECV] ((s2 6)) [GOOD] (push 1) [GOOD] (assert s66) -Fast allSat, Looking for solution 2306 +Fast allSat, Looking for solution 2305 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29123,7 +29112,7 @@ Fast allSat, Looking for solution 2306 [RECV] ((s2 5)) [GOOD] (push 1) [GOOD] (assert s67) -Fast allSat, Looking for solution 2307 +Fast allSat, Looking for solution 2306 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29134,7 +29123,7 @@ Fast allSat, Looking for solution 2307 [RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s68) -Fast allSat, Looking for solution 2308 +Fast allSat, Looking for solution 2307 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29145,6 +29134,17 @@ Fast allSat, Looking for solution 2308 [RECV] ((s2 3)) [GOOD] (push 1) [GOOD] (assert s69) +Fast allSat, Looking for solution 2308 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 2)) +[SEND] (get-value (s1)) +[RECV] ((s1 7)) +[SEND] (get-value (s2)) +[RECV] ((s2 1)) +[GOOD] (push 1) +[GOOD] (assert s71) Fast allSat, Looking for solution 2309 [SEND] (check-sat) [RECV] unsat @@ -29163,7 +29163,7 @@ Fast allSat, Looking for solution 2309 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) [GOOD] (assert s78) Fast allSat, Looking for solution 2309 [SEND] (check-sat) @@ -29173,9 +29173,9 @@ Fast allSat, Looking for solution 2309 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 1)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s71) Fast allSat, Looking for solution 2310 [SEND] (check-sat) [RECV] sat @@ -29184,9 +29184,9 @@ Fast allSat, Looking for solution 2310 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 3)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s69) Fast allSat, Looking for solution 2311 [SEND] (check-sat) [RECV] sat @@ -29195,9 +29195,9 @@ Fast allSat, Looking for solution 2311 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 3)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s69) +[GOOD] (assert s68) Fast allSat, Looking for solution 2312 [SEND] (check-sat) [RECV] sat @@ -29206,9 +29206,9 @@ Fast allSat, Looking for solution 2312 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s67) Fast allSat, Looking for solution 2313 [SEND] (check-sat) [RECV] sat @@ -29217,9 +29217,9 @@ Fast allSat, Looking for solution 2313 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s65) Fast allSat, Looking for solution 2314 [SEND] (check-sat) [RECV] sat @@ -29228,9 +29228,9 @@ Fast allSat, Looking for solution 2314 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s64) Fast allSat, Looking for solution 2315 [SEND] (check-sat) [RECV] sat @@ -29239,9 +29239,9 @@ Fast allSat, Looking for solution 2315 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s63) Fast allSat, Looking for solution 2316 [SEND] (check-sat) [RECV] sat @@ -29250,9 +29250,9 @@ Fast allSat, Looking for solution 2316 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s62) Fast allSat, Looking for solution 2317 [SEND] (check-sat) [RECV] sat @@ -29261,9 +29261,9 @@ Fast allSat, Looking for solution 2317 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s61) Fast allSat, Looking for solution 2318 [SEND] (check-sat) [RECV] sat @@ -29272,9 +29272,9 @@ Fast allSat, Looking for solution 2318 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s60) Fast allSat, Looking for solution 2319 [SEND] (check-sat) [RECV] sat @@ -29283,9 +29283,9 @@ Fast allSat, Looking for solution 2319 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s58) Fast allSat, Looking for solution 2320 [SEND] (check-sat) [RECV] sat @@ -29294,9 +29294,9 @@ Fast allSat, Looking for solution 2320 [SEND] (get-value (s1)) [RECV] ((s1 6)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s89) +[GOOD] (assert s72) Fast allSat, Looking for solution 2321 [SEND] (check-sat) [RECV] unsat @@ -29315,7 +29315,7 @@ Fast allSat, Looking for solution 2321 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) [GOOD] (assert s77) Fast allSat, Looking for solution 2321 [SEND] (check-sat) @@ -29325,21 +29325,10 @@ Fast allSat, Looking for solution 2321 [SEND] (get-value (s1)) [RECV] ((s1 5)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) -[GOOD] (push 1) -[GOOD] (assert s89) -Fast allSat, Looking for solution 2322 -[SEND] (check-sat) -[RECV] sat -[SEND] (get-value (s0)) -[RECV] ((s0 2)) -[SEND] (get-value (s1)) -[RECV] ((s1 5)) -[SEND] (get-value (s2)) [RECV] ((s2 14)) [GOOD] (push 1) [GOOD] (assert s72) -Fast allSat, Looking for solution 2323 +Fast allSat, Looking for solution 2322 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29350,7 +29339,7 @@ Fast allSat, Looking for solution 2323 [RECV] ((s2 13)) [GOOD] (push 1) [GOOD] (assert s58) -Fast allSat, Looking for solution 2324 +Fast allSat, Looking for solution 2323 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29361,7 +29350,7 @@ Fast allSat, Looking for solution 2324 [RECV] ((s2 12)) [GOOD] (push 1) [GOOD] (assert s60) -Fast allSat, Looking for solution 2325 +Fast allSat, Looking for solution 2324 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29372,7 +29361,7 @@ Fast allSat, Looking for solution 2325 [RECV] ((s2 11)) [GOOD] (push 1) [GOOD] (assert s61) -Fast allSat, Looking for solution 2326 +Fast allSat, Looking for solution 2325 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29383,7 +29372,7 @@ Fast allSat, Looking for solution 2326 [RECV] ((s2 10)) [GOOD] (push 1) [GOOD] (assert s62) -Fast allSat, Looking for solution 2327 +Fast allSat, Looking for solution 2326 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29394,7 +29383,7 @@ Fast allSat, Looking for solution 2327 [RECV] ((s2 9)) [GOOD] (push 1) [GOOD] (assert s63) -Fast allSat, Looking for solution 2328 +Fast allSat, Looking for solution 2327 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29405,7 +29394,7 @@ Fast allSat, Looking for solution 2328 [RECV] ((s2 8)) [GOOD] (push 1) [GOOD] (assert s64) -Fast allSat, Looking for solution 2329 +Fast allSat, Looking for solution 2328 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29416,7 +29405,7 @@ Fast allSat, Looking for solution 2329 [RECV] ((s2 7)) [GOOD] (push 1) [GOOD] (assert s65) -Fast allSat, Looking for solution 2330 +Fast allSat, Looking for solution 2329 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29427,7 +29416,7 @@ Fast allSat, Looking for solution 2330 [RECV] ((s2 6)) [GOOD] (push 1) [GOOD] (assert s66) -Fast allSat, Looking for solution 2331 +Fast allSat, Looking for solution 2330 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29438,7 +29427,7 @@ Fast allSat, Looking for solution 2331 [RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s68) -Fast allSat, Looking for solution 2332 +Fast allSat, Looking for solution 2331 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29449,6 +29438,17 @@ Fast allSat, Looking for solution 2332 [RECV] ((s2 3)) [GOOD] (push 1) [GOOD] (assert s69) +Fast allSat, Looking for solution 2332 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 2)) +[SEND] (get-value (s1)) +[RECV] ((s1 5)) +[SEND] (get-value (s2)) +[RECV] ((s2 1)) +[GOOD] (push 1) +[GOOD] (assert s71) Fast allSat, Looking for solution 2333 [SEND] (check-sat) [RECV] unsat @@ -29467,7 +29467,7 @@ Fast allSat, Looking for solution 2333 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) [GOOD] (assert s76) Fast allSat, Looking for solution 2333 [SEND] (check-sat) @@ -29477,10 +29477,21 @@ Fast allSat, Looking for solution 2333 [SEND] (get-value (s1)) [RECV] ((s1 4)) [SEND] (get-value (s2)) +[RECV] ((s2 1)) +[GOOD] (push 1) +[GOOD] (assert s71) +Fast allSat, Looking for solution 2334 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 2)) +[SEND] (get-value (s1)) +[RECV] ((s1 4)) +[SEND] (get-value (s2)) [RECV] ((s2 3)) [GOOD] (push 1) [GOOD] (assert s69) -Fast allSat, Looking for solution 2334 +Fast allSat, Looking for solution 2335 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29491,7 +29502,7 @@ Fast allSat, Looking for solution 2334 [RECV] ((s2 5)) [GOOD] (push 1) [GOOD] (assert s67) -Fast allSat, Looking for solution 2335 +Fast allSat, Looking for solution 2336 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29502,7 +29513,7 @@ Fast allSat, Looking for solution 2335 [RECV] ((s2 6)) [GOOD] (push 1) [GOOD] (assert s66) -Fast allSat, Looking for solution 2336 +Fast allSat, Looking for solution 2337 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29513,7 +29524,7 @@ Fast allSat, Looking for solution 2336 [RECV] ((s2 7)) [GOOD] (push 1) [GOOD] (assert s65) -Fast allSat, Looking for solution 2337 +Fast allSat, Looking for solution 2338 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29524,7 +29535,7 @@ Fast allSat, Looking for solution 2337 [RECV] ((s2 8)) [GOOD] (push 1) [GOOD] (assert s64) -Fast allSat, Looking for solution 2338 +Fast allSat, Looking for solution 2339 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29535,7 +29546,7 @@ Fast allSat, Looking for solution 2338 [RECV] ((s2 9)) [GOOD] (push 1) [GOOD] (assert s63) -Fast allSat, Looking for solution 2339 +Fast allSat, Looking for solution 2340 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29546,7 +29557,7 @@ Fast allSat, Looking for solution 2339 [RECV] ((s2 10)) [GOOD] (push 1) [GOOD] (assert s62) -Fast allSat, Looking for solution 2340 +Fast allSat, Looking for solution 2341 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29557,7 +29568,7 @@ Fast allSat, Looking for solution 2340 [RECV] ((s2 11)) [GOOD] (push 1) [GOOD] (assert s61) -Fast allSat, Looking for solution 2341 +Fast allSat, Looking for solution 2342 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29568,7 +29579,7 @@ Fast allSat, Looking for solution 2341 [RECV] ((s2 12)) [GOOD] (push 1) [GOOD] (assert s60) -Fast allSat, Looking for solution 2342 +Fast allSat, Looking for solution 2343 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29579,7 +29590,7 @@ Fast allSat, Looking for solution 2342 [RECV] ((s2 13)) [GOOD] (push 1) [GOOD] (assert s58) -Fast allSat, Looking for solution 2343 +Fast allSat, Looking for solution 2344 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29590,17 +29601,6 @@ Fast allSat, Looking for solution 2343 [RECV] ((s2 14)) [GOOD] (push 1) [GOOD] (assert s72) -Fast allSat, Looking for solution 2344 -[SEND] (check-sat) -[RECV] sat -[SEND] (get-value (s0)) -[RECV] ((s0 2)) -[SEND] (get-value (s1)) -[RECV] ((s1 4)) -[SEND] (get-value (s2)) -[RECV] ((s2 15)) -[GOOD] (push 1) -[GOOD] (assert s89) Fast allSat, Looking for solution 2345 [SEND] (check-sat) [RECV] unsat @@ -29619,7 +29619,7 @@ Fast allSat, Looking for solution 2345 [GOOD] (pop 1) [GOOD] (pop 1) [GOOD] (push 1) -[GOOD] (assert s71) +[GOOD] (assert s89) [GOOD] (assert s75) Fast allSat, Looking for solution 2345 [SEND] (check-sat) @@ -29629,21 +29629,10 @@ Fast allSat, Looking for solution 2345 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 15)) -[GOOD] (push 1) -[GOOD] (assert s89) -Fast allSat, Looking for solution 2346 -[SEND] (check-sat) -[RECV] sat -[SEND] (get-value (s0)) -[RECV] ((s0 2)) -[SEND] (get-value (s1)) -[RECV] ((s1 3)) -[SEND] (get-value (s2)) [RECV] ((s2 14)) [GOOD] (push 1) [GOOD] (assert s72) -Fast allSat, Looking for solution 2347 +Fast allSat, Looking for solution 2346 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29654,7 +29643,7 @@ Fast allSat, Looking for solution 2347 [RECV] ((s2 13)) [GOOD] (push 1) [GOOD] (assert s58) -Fast allSat, Looking for solution 2348 +Fast allSat, Looking for solution 2347 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29665,7 +29654,7 @@ Fast allSat, Looking for solution 2348 [RECV] ((s2 12)) [GOOD] (push 1) [GOOD] (assert s60) -Fast allSat, Looking for solution 2349 +Fast allSat, Looking for solution 2348 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29676,7 +29665,7 @@ Fast allSat, Looking for solution 2349 [RECV] ((s2 11)) [GOOD] (push 1) [GOOD] (assert s61) -Fast allSat, Looking for solution 2350 +Fast allSat, Looking for solution 2349 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29687,7 +29676,7 @@ Fast allSat, Looking for solution 2350 [RECV] ((s2 10)) [GOOD] (push 1) [GOOD] (assert s62) -Fast allSat, Looking for solution 2351 +Fast allSat, Looking for solution 2350 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29698,7 +29687,7 @@ Fast allSat, Looking for solution 2351 [RECV] ((s2 9)) [GOOD] (push 1) [GOOD] (assert s63) -Fast allSat, Looking for solution 2352 +Fast allSat, Looking for solution 2351 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29709,7 +29698,7 @@ Fast allSat, Looking for solution 2352 [RECV] ((s2 8)) [GOOD] (push 1) [GOOD] (assert s64) -Fast allSat, Looking for solution 2353 +Fast allSat, Looking for solution 2352 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29720,7 +29709,7 @@ Fast allSat, Looking for solution 2353 [RECV] ((s2 7)) [GOOD] (push 1) [GOOD] (assert s65) -Fast allSat, Looking for solution 2354 +Fast allSat, Looking for solution 2353 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29731,7 +29720,7 @@ Fast allSat, Looking for solution 2354 [RECV] ((s2 6)) [GOOD] (push 1) [GOOD] (assert s66) -Fast allSat, Looking for solution 2355 +Fast allSat, Looking for solution 2354 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29742,7 +29731,7 @@ Fast allSat, Looking for solution 2355 [RECV] ((s2 5)) [GOOD] (push 1) [GOOD] (assert s67) -Fast allSat, Looking for solution 2356 +Fast allSat, Looking for solution 2355 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) @@ -29753,6 +29742,17 @@ Fast allSat, Looking for solution 2356 [RECV] ((s2 4)) [GOOD] (push 1) [GOOD] (assert s68) +Fast allSat, Looking for solution 2356 +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s0)) +[RECV] ((s0 2)) +[SEND] (get-value (s1)) +[RECV] ((s1 3)) +[SEND] (get-value (s2)) +[RECV] ((s2 1)) +[GOOD] (push 1) +[GOOD] (assert s71) Fast allSat, Looking for solution 2357 [SEND] (check-sat) [RECV] unsat @@ -34189,9 +34189,9 @@ Fast allSat, Looking for solution 2707 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 14)) +[RECV] ((s2 2)) [GOOD] (push 1) -[GOOD] (assert s72) +[GOOD] (assert s70) Fast allSat, Looking for solution 2708 [SEND] (check-sat) [RECV] sat @@ -34200,9 +34200,9 @@ Fast allSat, Looking for solution 2708 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 13)) +[RECV] ((s2 4)) [GOOD] (push 1) -[GOOD] (assert s58) +[GOOD] (assert s68) Fast allSat, Looking for solution 2709 [SEND] (check-sat) [RECV] sat @@ -34211,9 +34211,9 @@ Fast allSat, Looking for solution 2709 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 12)) +[RECV] ((s2 5)) [GOOD] (push 1) -[GOOD] (assert s60) +[GOOD] (assert s67) Fast allSat, Looking for solution 2710 [SEND] (check-sat) [RECV] sat @@ -34222,9 +34222,9 @@ Fast allSat, Looking for solution 2710 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 11)) +[RECV] ((s2 6)) [GOOD] (push 1) -[GOOD] (assert s61) +[GOOD] (assert s66) Fast allSat, Looking for solution 2711 [SEND] (check-sat) [RECV] sat @@ -34233,9 +34233,9 @@ Fast allSat, Looking for solution 2711 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 10)) +[RECV] ((s2 7)) [GOOD] (push 1) -[GOOD] (assert s62) +[GOOD] (assert s65) Fast allSat, Looking for solution 2712 [SEND] (check-sat) [RECV] sat @@ -34244,9 +34244,9 @@ Fast allSat, Looking for solution 2712 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 9)) +[RECV] ((s2 8)) [GOOD] (push 1) -[GOOD] (assert s63) +[GOOD] (assert s64) Fast allSat, Looking for solution 2713 [SEND] (check-sat) [RECV] sat @@ -34255,9 +34255,9 @@ Fast allSat, Looking for solution 2713 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 8)) +[RECV] ((s2 9)) [GOOD] (push 1) -[GOOD] (assert s64) +[GOOD] (assert s63) Fast allSat, Looking for solution 2714 [SEND] (check-sat) [RECV] sat @@ -34266,9 +34266,9 @@ Fast allSat, Looking for solution 2714 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 7)) +[RECV] ((s2 10)) [GOOD] (push 1) -[GOOD] (assert s65) +[GOOD] (assert s62) Fast allSat, Looking for solution 2715 [SEND] (check-sat) [RECV] sat @@ -34277,9 +34277,9 @@ Fast allSat, Looking for solution 2715 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 6)) +[RECV] ((s2 11)) [GOOD] (push 1) -[GOOD] (assert s66) +[GOOD] (assert s61) Fast allSat, Looking for solution 2716 [SEND] (check-sat) [RECV] sat @@ -34288,9 +34288,9 @@ Fast allSat, Looking for solution 2716 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 5)) +[RECV] ((s2 12)) [GOOD] (push 1) -[GOOD] (assert s67) +[GOOD] (assert s60) Fast allSat, Looking for solution 2717 [SEND] (check-sat) [RECV] sat @@ -34299,9 +34299,9 @@ Fast allSat, Looking for solution 2717 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 4)) +[RECV] ((s2 13)) [GOOD] (push 1) -[GOOD] (assert s68) +[GOOD] (assert s58) Fast allSat, Looking for solution 2718 [SEND] (check-sat) [RECV] sat @@ -34310,9 +34310,9 @@ Fast allSat, Looking for solution 2718 [SEND] (get-value (s1)) [RECV] ((s1 3)) [SEND] (get-value (s2)) -[RECV] ((s2 2)) +[RECV] ((s2 14)) [GOOD] (push 1) -[GOOD] (assert s70) +[GOOD] (assert s72) Fast allSat, Looking for solution 2719 [SEND] (check-sat) [RECV] unsat