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