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