/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 >> tH t1 tF tG MODEL SEQUENCE: t0 t3 >> t5 tJ tH >> tF tG 1. distance 4 encoding time: 0.01 solving time: 0.04 LOG SEQUENCE: t1 tB tI tH >> >> tD MODEL SEQUENCE: t1 tB >> >> tC tE tD 2. distance 4 encoding time: 0.01 solving time: 0.09 LOG SEQUENCE: tF t1 tB tE tC tA >> tD 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.05 LOG SEQUENCE: t1 >> t4 tC >> tD tE MODEL SEQUENCE: t1 tB >> tC tE tD >> 5. distance 2 encoding time: 0.01 solving time: 0.02 LOG SEQUENCE: t1 >> tC tH 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 3 encoding time: 0.02 solving time: 0.08 LOG SEQUENCE: t0 t0 t2 tA tH tF tG tF tF 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.06 LOG SEQUENCE: >> tE tB tC tE tD t5 MODEL SEQUENCE: t1 >> tB tC tE tD >> 12. distance 3 encoding time: 0.01 solving time: 0.04 LOG SEQUENCE: tH t2 >> 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 >> tH 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 t2 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 tG MODEL SEQUENCE: t0 t3 t5 tJ tH tF >> tG 16. distance 2 encoding time: 0.01 solving time: 0.02 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 tF tB >> tE tD MODEL SEQUENCE: t1 >> tB tC tE tD 18. distance 1 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t5 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.06 LOG SEQUENCE: >> tI t0 >> tC tE tD MODEL SEQUENCE: t1 >> >> tB tC tE tD 21. distance 2 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 >> tC tG 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 t3 tB tC tE tD MODEL SEQUENCE: t1 >> tB tC tE tD 24. distance 5 encoding time: 0.01 solving time: 0.34 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.01 solving time: 0.06 LOG SEQUENCE: t0 t3 t4 tI tH t5 t0 tF >> MODEL SEQUENCE: t0 t3 t4 tI tH >> >> tF tG 27. distance 2 encoding time: 0.01 solving time: 0.04 LOG SEQUENCE: t0 t3 t4 >> tH tF tF tG MODEL SEQUENCE: t0 t3 t4 tI tH tF >> tG 28. distance 3 encoding time: 0.01 solving time: 0.03 LOG SEQUENCE: t1 tB tB tC tC >> 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 tJ tD MODEL SEQUENCE: t1 tB tC tE >> tD 30. distance 3 encoding time: 0.02 solving time: 0.11 LOG SEQUENCE: t0 t2 tA t2 t3 tH tF tG tG MODEL SEQUENCE: t0 t2 tA >> >> tH tF tG >> 31. distance 1 encoding time: 0.01 solving time: 0.01 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: 1.47 LOG SEQUENCE: >> tI t3 tF t5 t5 tG tJ >> tF tG MODEL SEQUENCE: t0 >> t3 >> >> t5 >> tJ tH tF tG 34. distance 6 encoding time: 0.01 solving time: 0.21 LOG SEQUENCE: t2 tB >> tB tI tG tC >> tD MODEL SEQUENCE: >> >> t1 tB >> >> tC tE tD 35. distance 5 encoding time: 0.01 solving time: 0.08 LOG SEQUENCE: t1 tB >> >> tD tE tH tE MODEL SEQUENCE: t1 tB tC tE tD >> >> >> 36. distance 2 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: >> tB tC t3 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 tF tF tF >> MODEL SEQUENCE: t0 t3 t4 tI tH tF >> >> tG 38. distance 2 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t0 t2 tA tH t3 >> 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 t5 >> tC tE tD MODEL SEQUENCE: t1 >> tB tC tE tD 41. distance 3 encoding time: 0.01 solving time: 0.07 LOG SEQUENCE: t0 t0 t2 t5 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: tF tE >> 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 tB tE >> MODEL SEQUENCE: t1 tB tC >> tE tD 46. distance 4 encoding time: 0.01 solving time: 0.04 LOG SEQUENCE: >> tB t1 tC >> tD t0 MODEL SEQUENCE: t1 tB >> tC tE tD >> 47. distance 3 encoding time: 0.02 solving time: 0.19 LOG SEQUENCE: t0 t0 t3 t5 t4 tI tH 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.09 LOG SEQUENCE: t1 t1 tB tB >> >> tD 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.04 LOG SEQUENCE: t0 t2 tA tH tH tI >> tG MODEL SEQUENCE: t0 t2 tA >> tH >> tF tG 53. distance 5 encoding time: 0.01 solving time: 0.13 LOG SEQUENCE: >> tB tB tE >> tE t2 tD MODEL SEQUENCE: t1 tB >> >> tC tE >> tD 54. distance 4 encoding time: 0.01 solving time: 0.06 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.10 LOG SEQUENCE: >> tB >> t1 tG tE tD MODEL SEQUENCE: t1 tB tC >> >> tE tD 58. distance 3 encoding time: 0.01 solving time: 0.05 LOG SEQUENCE: t1 tB t2 >> tE tD tG MODEL SEQUENCE: t1 tB >> tC tE tD >> 59. distance 2 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 >> tF tC tE tD MODEL SEQUENCE: t1 tB >> tC tE tD 60. 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 61. distance 3 encoding time: 0.02 solving time: 0.07 LOG SEQUENCE: t0 t3 tF t5 tJ tH tG tF >> MODEL SEQUENCE: t0 t3 >> t5 tJ tH >> tF tG 62. distance 3 encoding time: 0.02 solving time: 0.10 LOG SEQUENCE: t0 t3 >> tJ t5 tH tF tF tG MODEL SEQUENCE: t0 t3 t5 tJ >> tH tF >> tG 63. distance 4 encoding time: 0.01 solving time: 0.02 LOG SEQUENCE: t1 tB t0 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 6 encoding time: 0.01 solving time: 0.29 LOG SEQUENCE: t1 t0 >> >> tE tC >> tH MODEL SEQUENCE: t1 >> tB tC tE >> tD >> 66. distance 2 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: tH 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 t3 tH tF tG MODEL SEQUENCE: t0 t3 t4 tI >> tH tF tG 68. distance 4 encoding time: 0.02 solving time: 0.19 LOG SEQUENCE: tI t2 t2 t0 t2 >> tH tF tG 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.02 LOG SEQUENCE: t1 >> tC tB tE tD MODEL SEQUENCE: t1 tB tC >> tE tD 71. distance 4 encoding time: 0.02 solving time: 0.07 LOG SEQUENCE: t0 t3 t4 >> tH tH tA >> tG MODEL SEQUENCE: t0 t3 t4 tI tH >> >> tF tG 72. distance 1 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t0 t2 tA t2 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.04 LOG SEQUENCE: t3 t1 >> tC >> tD t3 MODEL SEQUENCE: >> t1 tB tC tE tD >> 75. distance 4 encoding time: 0.01 solving time: 0.10 LOG SEQUENCE: t0 t5 t3 >> tJ t3 >> tF tG MODEL SEQUENCE: t0 >> t3 t5 tJ >> tH tF tG 76. distance 4 encoding time: 0.01 solving time: 0.11 LOG SEQUENCE: t1 t1 >> tC tE tE tD tC MODEL SEQUENCE: >> t1 tB tC >> tE tD >> 77. distance 4 encoding time: 0.01 solving time: 0.09 LOG SEQUENCE: t0 t2 t2 tA >> >> tG tG MODEL SEQUENCE: t0 t2 >> tA tH tF tG >> 78. distance 2 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: >> t2 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 3 encoding time: 0.01 solving time: 0.03 LOG SEQUENCE: t1 tB tF tE tC >> tD MODEL SEQUENCE: t1 tB >> >> tC tE tD 82. distance 7 encoding time: 0.01 solving time: 0.50 LOG SEQUENCE: t1 tF tI t2 >> >> >> 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.11 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.01 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.03 LOG SEQUENCE: t1 >> tF tC t0 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.02 LOG SEQUENCE: t0 t2 tA tH tF tG tF MODEL SEQUENCE: t0 t2 tA tH tF tG >> 89. distance 2 encoding time: 0.01 solving time: 0.03 LOG SEQUENCE: t0 t3 tD t4 >> tH tF tG MODEL SEQUENCE: t0 t3 >> t4 tI tH tF tG 90. distance 3 encoding time: 0.01 solving time: 0.04 LOG SEQUENCE: t0 t1 tB t2 tC >> tD MODEL SEQUENCE: >> t1 tB >> tC tE tD 91. distance 2 encoding time: 0.01 solving time: 0.01 LOG SEQUENCE: t1 >> tC t0 tE tD MODEL SEQUENCE: t1 tB tC >> tE tD 92. distance 4 encoding time: 0.01 solving time: 0.04 LOG SEQUENCE: >> tB t1 tC >> tD t2 MODEL SEQUENCE: t1 tB >> tC tE tD >> 93. distance 5 encoding time: 0.02 solving time: 0.23 LOG SEQUENCE: t0 t3 >> tJ t2 tH tH >> tG tF MODEL SEQUENCE: t0 t3 t5 tJ >> tH >> tF tG >> 94. distance 3 encoding time: 0.02 solving time: 0.08 LOG SEQUENCE: t0 t3 tF >> tJ tC 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.05 LOG SEQUENCE: >> t3 t3 t4 tI tH tF tG MODEL SEQUENCE: t0 t3 >> t4 tI tH tF tG 97. distance 3 encoding time: 0.02 solving time: 0.12 LOG SEQUENCE: >> t3 t0 t5 tJ tH tF tG tG MODEL SEQUENCE: t0 t3 >> t5 tJ tH tF tG >> 98. distance 2 encoding time: 0.01 solving time: 0.02 LOG SEQUENCE: t1 tB t3 t2 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 t0 tC >> tD MODEL SEQUENCE: t1 tB >> tC tE tD encoding time: total 1.20 avg 0.01 median 0.01 solving time: total 6.78 avg 0.07 median 0.09 timeouts: 0 distance 1: 13 distance 0: 15 distance 6: 3 distance 5: 5 distance 7: 1 distance 4: 17 distance 3: 21 distance 2: 25