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