/home/swinkler/confchecksmt/src/libyices.so.2.6.2 0. distance 0 encoding time: 0.02 solving time: 0.02 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 1. distance 0 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 2. distance 2 encoding time: 0.01 solving time: 0.26 LOG SEQUENCE: t0 t3 t5 >> tH tF >> MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 3. distance 1 encoding time: 0.02 solving time: 0.27 LOG SEQUENCE: t0 >> tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 4. distance 0 encoding time: 0.02 solving time: 0.03 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 5. distance 1 encoding time: 0.02 solving time: 0.03 LOG SEQUENCE: t0 t2 tA tH tF tG tB MODEL SEQUENCE: t0 t2 tA tH tF tG >> 6. distance 1 encoding time: 0.03 solving time: 0.79 LOG SEQUENCE: >> t3 t5 tJ tH tF tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 7. distance 0 encoding time: 0.02 solving time: 0.01 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 8. distance 1 encoding time: 0.01 solving time: 0.08 LOG SEQUENCE: t0 t2 tA >> tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 9. distance 0 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 10. distance 1 encoding time: 0.02 solving time: 0.02 LOG SEQUENCE: t0 t3 t5 tJ tH tF tG t4 MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG >> 11. distance 0 encoding time: 0.02 solving time: 0.06 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 12. distance 0 encoding time: 0.04 solving time: 0.04 LOG SEQUENCE: t0 t3 t5 tJ tH tF tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 13. distance 2 encoding time: 0.01 solving time: 0.09 LOG SEQUENCE: t1 tB tC >> >> MODEL SEQUENCE: t1 tB tC tE tD 14. distance 0 encoding time: 0.02 solving time: 0.02 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 15. distance 2 encoding time: 0.01 solving time: 0.53 LOG SEQUENCE: >> >> tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 16. distance 1 encoding time: 0.01 solving time: 0.04 LOG SEQUENCE: t1 >> tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 17. distance 0 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 18. distance 0 encoding time: 0.02 solving time: 0.03 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 19. distance 0 encoding time: 0.02 solving time: 0.04 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 20. distance 1 encoding time: 0.01 solving time: 0.04 LOG SEQUENCE: >> tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 21. distance 0 encoding time: 0.02 solving time: 0.04 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 22. distance 1 encoding time: 0.01 solving time: 0.05 LOG SEQUENCE: t1 tB >> tE tD MODEL SEQUENCE: t1 tB tC tE tD 23. distance 2 encoding time: 0.02 solving time: 0.59 LOG SEQUENCE: >> t3 >> tI tH tF tG MODEL SEQUENCE: t0 t3 t4 tI tH tF tG 24. distance 1 encoding time: 0.02 solving time: 0.14 LOG SEQUENCE: t0 t2 tA >> tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 25. distance 1 encoding time: 0.01 solving time: 0.09 LOG SEQUENCE: t0 t3 t5 >> tH tF tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 26. distance 0 encoding time: 0.02 solving time: 0.08 LOG SEQUENCE: t0 t3 t5 tJ tH tF tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 27. distance 2 encoding time: 0.02 solving time: 2.57 LOG SEQUENCE: >> >> t5 tJ tH tF tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 28. distance 0 encoding time: 0.03 solving time: 0.02 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 29. distance 1 encoding time: 0.02 solving time: 0.04 LOG SEQUENCE: t1 tB tC >> tD MODEL SEQUENCE: t1 tB tC tE tD 30. distance 2 encoding time: 0.02 solving time: 0.24 LOG SEQUENCE: t0 t2 tA tH >> >> MODEL SEQUENCE: t0 t2 tA tH tF tG 31. distance 0 encoding time: 0.02 solving time: 0.02 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 32. distance 1 encoding time: 0.03 solving time: 0.25 LOG SEQUENCE: t0 >> tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 33. distance 1 encoding time: 0.02 solving time: 0.07 LOG SEQUENCE: t0 t3 >> tI tH tF tG MODEL SEQUENCE: t0 t3 t4 tI tH tF tG 34. distance 1 encoding time: 0.01 solving time: 0.02 LOG SEQUENCE: t1 tB >> tE tD MODEL SEQUENCE: t1 tB tC tE tD 35. distance 0 encoding time: 0.02 solving time: 0.04 LOG SEQUENCE: t0 t3 t4 tI tH tF tG MODEL SEQUENCE: t0 t3 t4 tI tH tF tG 36. distance 0 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 37. distance 3 encoding time: 0.03 solving time: 6.60 LOG SEQUENCE: t0 t3 t4 tI tH >> >> tC MODEL SEQUENCE: t0 t3 t4 tI tH tF tG >> 38. distance 0 encoding time: 0.01 solving time: 0.00 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 39. distance 1 encoding time: 0.02 solving time: 0.03 LOG SEQUENCE: t1 tB tC tE >> MODEL SEQUENCE: t1 tB tC tE tD 40. distance 1 encoding time: 0.01 solving time: 0.05 LOG SEQUENCE: t0 t2 >> tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 41. distance 1 encoding time: 0.02 solving time: 0.17 LOG SEQUENCE: t0 >> tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 42. distance 0 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 43. distance 0 encoding time: 0.02 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 44. distance 1 encoding time: 0.02 solving time: 0.11 LOG SEQUENCE: t0 t3 t4 tI tH >> tG MODEL SEQUENCE: t0 t3 t4 tI tH tF tG 45. distance 0 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 46. distance 1 encoding time: 0.01 solving time: 0.02 LOG SEQUENCE: t1 tB tC tE >> MODEL SEQUENCE: t1 tB tC tE tD 47. distance 1 encoding time: 0.01 solving time: 0.08 LOG SEQUENCE: >> tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 48. distance 0 encoding time: 0.03 solving time: 0.04 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 49. distance 2 encoding time: 0.01 solving time: 0.02 LOG SEQUENCE: t1 tB tC >> tD tB MODEL SEQUENCE: t1 tB tC tE tD >> 50. distance 0 encoding time: 0.02 solving time: 0.13 LOG SEQUENCE: t0 t3 t4 tI tH tF tG MODEL SEQUENCE: t0 t3 t4 tI tH tF tG 51. distance 0 encoding time: 0.02 solving time: 0.07 LOG SEQUENCE: t0 t3 t5 tJ tH tF tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 52. distance 1 encoding time: 0.01 solving time: 0.03 LOG SEQUENCE: t1 tB >> tE tD MODEL SEQUENCE: t1 tB tC tE tD 53. distance 2 encoding time: 0.01 solving time: 0.12 LOG SEQUENCE: t1 tB tC tE >> tF MODEL SEQUENCE: t1 tB tC tE tD >> 54. distance 0 encoding time: 0.02 solving time: 0.05 LOG SEQUENCE: t0 t3 t4 tI tH tF tG MODEL SEQUENCE: t0 t3 t4 tI tH tF tG 55. distance 0 encoding time: 0.02 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 56. distance 2 encoding time: 0.02 solving time: 0.22 LOG SEQUENCE: t0 >> t5 tJ tH tF >> MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 57. distance 0 encoding time: 0.02 solving time: 0.05 LOG SEQUENCE: t0 t3 t5 tJ tH tF tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 58. distance 0 encoding time: 0.02 solving time: 0.04 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 59. distance 1 encoding time: 0.01 solving time: 0.03 LOG SEQUENCE: t0 t3 t5 tJ tH >> tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 60. distance 0 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 61. distance 1 encoding time: 0.04 solving time: 0.47 LOG SEQUENCE: t0 t3 t5 tJ tH >> tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 62. distance 1 encoding time: 0.01 solving time: 0.23 LOG SEQUENCE: t0 t3 >> tJ tH tF tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 63. distance 0 encoding time: 0.03 solving time: 0.05 LOG SEQUENCE: t0 t3 t4 tI tH tF tG MODEL SEQUENCE: t0 t3 t4 tI tH tF tG 64. distance 0 encoding time: 0.02 solving time: 0.09 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 65. distance 0 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 66. distance 0 encoding time: 0.01 solving time: 0.00 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 67. distance 1 encoding time: 0.01 solving time: 0.02 LOG SEQUENCE: t1 tB >> tE tD MODEL SEQUENCE: t1 tB tC tE tD 68. distance 1 encoding time: 0.03 solving time: 0.28 LOG SEQUENCE: t0 t3 t5 tJ tH tF >> MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 69. distance 2 encoding time: 0.01 solving time: 0.13 LOG SEQUENCE: >> tB tC tE >> MODEL SEQUENCE: t1 tB tC tE tD 70. distance 0 encoding time: 0.03 solving time: 0.09 LOG SEQUENCE: t0 t3 t4 tI tH tF tG MODEL SEQUENCE: t0 t3 t4 tI tH tF tG 71. distance 1 encoding time: 0.02 solving time: 0.30 LOG SEQUENCE: >> t3 t4 tI tH tF tG MODEL SEQUENCE: t0 t3 t4 tI tH tF tG 72. distance 1 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 tB >> tE tD MODEL SEQUENCE: t1 tB tC tE tD 73. distance 0 encoding time: 0.01 solving time: 0.00 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 74. distance 1 encoding time: 0.01 solving time: 0.03 LOG SEQUENCE: t1 tB tC tE >> MODEL SEQUENCE: t1 tB tC tE tD 75. distance 0 encoding time: 0.02 solving time: 0.04 LOG SEQUENCE: t0 t3 t5 tJ tH tF tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 76. distance 0 encoding time: 0.03 solving time: 0.02 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 77. distance 0 encoding time: 0.01 solving time: 0.02 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 78. distance 1 encoding time: 0.01 solving time: 0.03 LOG SEQUENCE: t1 tB >> tE tD MODEL SEQUENCE: t1 tB tC tE tD 79. distance 0 encoding time: 0.01 solving time: 0.02 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 80. distance 0 encoding time: 0.02 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 81. distance 1 encoding time: 0.02 solving time: 0.30 LOG SEQUENCE: t0 t3 t4 tI tH >> tG MODEL SEQUENCE: t0 t3 t4 tI tH tF tG 82. distance 1 encoding time: 0.02 solving time: 0.09 LOG SEQUENCE: t0 t3 t4 tI tH tF >> MODEL SEQUENCE: t0 t3 t4 tI tH tF tG 83. distance 2 encoding time: 0.02 solving time: 0.16 LOG SEQUENCE: t0 t2 >> tH tF >> MODEL SEQUENCE: t0 t2 tA tH tF tG 84. distance 0 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 85. distance 0 encoding time: 0.02 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 86. distance 0 encoding time: 0.03 solving time: 0.12 LOG SEQUENCE: t0 t3 t5 tJ tH tF tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF tG 87. distance 2 encoding time: 0.01 solving time: 0.29 LOG SEQUENCE: >> tB >> tE tD MODEL SEQUENCE: t1 tB tC tE tD 88. distance 0 encoding time: 0.02 solving time: 0.03 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 89. distance 1 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE >> MODEL SEQUENCE: t1 tB tC tE tD 90. distance 1 encoding time: 0.03 solving time: 0.08 LOG SEQUENCE: t0 t2 >> tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 91. distance 2 encoding time: 0.01 solving time: 0.10 LOG SEQUENCE: >> tB tC >> tD MODEL SEQUENCE: t1 tB tC tE tD 92. distance 2 encoding time: 0.02 solving time: 0.32 LOG SEQUENCE: t0 t3 t4 tI >> tF tG tE MODEL SEQUENCE: t0 t3 t4 tI tH tF tG >> 93. distance 1 encoding time: 0.02 solving time: 0.08 LOG SEQUENCE: t0 t2 tA >> tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 94. distance 2 encoding time: 0.02 solving time: 0.20 LOG SEQUENCE: t0 >> tA tH >> tG MODEL SEQUENCE: t0 t2 tA tH tF tG 95. distance 0 encoding time: 0.02 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 96. distance 0 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 97. distance 0 encoding time: 0.02 solving time: 0.02 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG 98. distance 0 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 tB tC tE tD MODEL SEQUENCE: t1 tB tC tE tD 99. distance 0 encoding time: 0.02 solving time: 0.04 LOG SEQUENCE: t0 t2 tA tH tF tG MODEL SEQUENCE: t0 t2 tA tH tF tG encoding time: total 1.80 avg 0.02 median 0.02 solving time: total 18.32 avg 0.18 median 0.13 timeouts: 0 distance 3: 1 distance 1: 35 distance 2: 15 distance 0: 49