/home/swinkler/confchecksmt/src/libyices.so.2.6.2

0. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

1. distance 5
encoding time: 0.02
solving time: 0.33
LOG SEQUENCE:
               >>         t5           t0           tG           tH           tH           t2           tC           tE           t2             >>         tJ           

MODEL SEQUENCE:
             t0           t5             >>         tG           tH             >>         t2           tC           tE             >>         tD           tJ           

2. distance 4
encoding time: 0.02
solving time: 0.13
LOG SEQUENCE:
             t0           t4           t6           tF             >>         t2           tC           tE           tD           tH             >>         

MODEL SEQUENCE:
             t0           t4           t6             >>         tA           t2           tC           tE           tD             >>         tJ           

3. distance 2
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           t4             >>         

MODEL SEQUENCE:
             t1             >>         tB           

4. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

5. distance 0
encoding time: 0.02
solving time: 0.01
LOG SEQUENCE:
             t0           t5           tG           tH           t2           tC           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t5           tG           tH           t2           tC           tE           tD           tJ           

6. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

7. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

8. distance 2
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           t3             >>         

MODEL SEQUENCE:
             t1             >>         tB           

9. distance 3
encoding time: 0.02
solving time: 0.07
LOG SEQUENCE:
             t0           t5           tG           tH           t3           tF           tE           tD             >>         tA           tA           

MODEL SEQUENCE:
             t0           t5           tG           tH           t3           tF           tE           tD           tJ             >>           >>         

10. distance 4
encoding time: 0.02
solving time: 0.38
LOG SEQUENCE:
             t0           t5           t3           tH             >>         tH           t3           tF           tE           tD           tJ           tJ           

MODEL SEQUENCE:
             t0           t5             >>           >>         tG           tH           t3           tF           tE           tD           tJ             >>         

11. distance 3
encoding time: 0.02
solving time: 0.11
LOG SEQUENCE:
             t0           t0           t4           t6           tA           t2           tC           tE             >>         tJ           tD           

MODEL SEQUENCE:
               >>         t0           t4           t6           tA           t2           tC           tE           tD           tJ             >>         

12. distance 1
encoding time: 0.02
solving time: 0.03
LOG SEQUENCE:
             t0           t5           tG           tH           t3           tF           tE           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t5           tG           tH           t3           tF           tE             >>         tD           tJ           

13. distance 7
encoding time: 0.02
solving time: 0.48
LOG SEQUENCE:
               >>         t4           t0           t7           tI           t3           tF           tE           tI           t0             >>           >>         t0           

MODEL SEQUENCE:
             t0           t4             >>         t7           tI           t3           tF           tE             >>           >>         tD           tJ             >>         

14. distance 7
encoding time: 0.02
solving time: 1.56
LOG SEQUENCE:
             t0           tI           tD             >>           >>         tH           tF             >>         tF           tE           tD           tD           tJ           

MODEL SEQUENCE:
             t0             >>           >>         t5           tG           tH             >>         t3           tF           tE           tD             >>         tJ           

15. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

16. distance 3
encoding time: 0.02
solving time: 0.13
LOG SEQUENCE:
             t0           t5           tJ           tG           tH             >>         tC           t2           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t5             >>         tG           tH           t2           tC             >>         tE           tD           tJ           

17. distance 2
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
               >>         t0           tB           

MODEL SEQUENCE:
             t1             >>         tB           

18. distance 2
encoding time: 0.02
solving time: 0.06
LOG SEQUENCE:
             t0           t5           tG           t3           tH             >>         tF           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t5           tG             >>         tH           t3           tF           tE           tD           tJ           

19. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

20. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

21. distance 6
encoding time: 0.02
solving time: 0.39
LOG SEQUENCE:
             t0           t5           tG             >>         t3           tD           tA             >>         tE             >>         tJ           tJ           

MODEL SEQUENCE:
             t0           t5           tG           tH           t3             >>           >>         tF           tE           tD           tJ             >>         

22. distance 2
encoding time: 0.02
solving time: 0.06
LOG SEQUENCE:
             t0             >>         tG           tC           tH           t3           tF           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t5           tG             >>         tH           t3           tF           tE           tD           tJ           

23. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

24. distance 1
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           tB           

MODEL SEQUENCE:
             t1             >>         tB           

25. distance 6
encoding time: 0.02
solving time: 0.79
LOG SEQUENCE:
             t0             >>         t7           t7           t2           tI           tI           t2           tC           tE             >>         tJ           tD           

MODEL SEQUENCE:
             t0           t4           t7             >>           >>         tI             >>         t2           tC           tE           tD           tJ             >>         

26. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

27. distance 1
encoding time: 0.02
solving time: 0.04
LOG SEQUENCE:
             t0           t4           t6           tA           tA           t2           tC           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t4           t6             >>         tA           t2           tC           tE           tD           tJ           

28. distance 3
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             tB           tB           t1             >>         

MODEL SEQUENCE:
               >>           >>         t1           tB           

29. distance 2
encoding time: 0.02
solving time: 0.05
LOG SEQUENCE:
               >>         t4           t7           t0           tI           t3           tF           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t4           t7             >>         tI           t3           tF           tE           tD           tJ           

30. distance 6
encoding time: 0.02
solving time: 0.64
LOG SEQUENCE:
             t0           t5           tG           tG             >>         t3           tH           tF             >>         tD           tD           tE           tJ           

MODEL SEQUENCE:
             t0           t5           tG             >>         tH           t3             >>         tF           tE           tD             >>           >>         tJ           

31. distance 7
encoding time: 0.02
solving time: 1.39
LOG SEQUENCE:
             t0           t4           t4           t7           t3             >>         t2           tC           tE           tJ           tJ           tD             >>         tD           

MODEL SEQUENCE:
             t0           t4             >>         t7             >>         tI           t2           tC           tE             >>           >>         tD           tJ             >>         

32. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

33. distance 1
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           t1           tB           

MODEL SEQUENCE:
               >>         t1           tB           

34. distance 2
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tJ             >>         

MODEL SEQUENCE:
             t1             >>         tB           

35. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

36. distance 2
encoding time: 0.02
solving time: 0.06
LOG SEQUENCE:
             t0           t5           tG           tH             >>         tF           t1           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t5           tG           tH           t3           tF             >>         tE           tD           tJ           

37. distance 4
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t4           tJ             >>           >>         

MODEL SEQUENCE:
               >>           >>         t1           tB           

38. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

39. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

40. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

41. distance 5
encoding time: 0.02
solving time: 0.30
LOG SEQUENCE:
             t0           t4           t6           t0           t3           t3             >>           >>         tC           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t4           t6             >>           >>           >>         tA           t2           tC           tE           tD           tJ           

42. distance 5
encoding time: 0.02
solving time: 0.33
LOG SEQUENCE:
             t0           t0           t5             >>         tH           tB           tG             >>         tC           tE           tD           tJ           

MODEL SEQUENCE:
               >>         t0           t5           tG           tH             >>           >>         t2           tC           tE           tD           tJ           

43. distance 2
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
               >>         t4           tB           

MODEL SEQUENCE:
             t1             >>         tB           

44. distance 5
encoding time: 0.02
solving time: 0.56
LOG SEQUENCE:
               >>           >>         tD           t6           tA           t4           t3           tF           tE           tD           tJ           tJ           

MODEL SEQUENCE:
             t0           t4             >>         t6           tA             >>         t3           tF           tE           tD           tJ             >>         

45. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

46. distance 1
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           t1           tB           

MODEL SEQUENCE:
               >>         t1           tB           

47. distance 3
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             tB           tB           t1             >>         

MODEL SEQUENCE:
               >>           >>         t1           tB           

48. distance 1
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           tB           

MODEL SEQUENCE:
             t1             >>         tB           

49. distance 1
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           t1           tB           

MODEL SEQUENCE:
               >>         t1           tB           

50. distance 3
encoding time: 0.02
solving time: 0.08
LOG SEQUENCE:
             t0           t4           t6           tA           t2           tC             >>         tD           tD           tE           tJ           

MODEL SEQUENCE:
             t0           t4           t6           tA           t2           tC           tE           tD             >>           >>         tJ           

51. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

52. distance 1
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           tB           

MODEL SEQUENCE:
             t1             >>         tB           

53. distance 2
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
               >>         tH           tB           

MODEL SEQUENCE:
             t1             >>         tB           

54. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

55. distance 4
encoding time: 0.02
solving time: 0.21
LOG SEQUENCE:
             t0           t4           t6           t6           tA           t2           tC           tE           tJ           tD           tD             >>         

MODEL SEQUENCE:
             t0           t4             >>         t6           tA           t2           tC           tE             >>         tD             >>         tJ           

56. distance 0
encoding time: 0.02
solving time: 0.01
LOG SEQUENCE:
             t0           t5           tG           tH           t2           tC           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t5           tG           tH           t2           tC           tE           tD           tJ           

57. distance 1
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           t1           tB           

MODEL SEQUENCE:
               >>         t1           tB           

58. distance 2
encoding time: 0.02
solving time: 0.04
LOG SEQUENCE:
             t0           t5           tG           tH           t3           tF           t7           tE             >>         tJ           

MODEL SEQUENCE:
             t0           t5           tG           tH           t3           tF             >>         tE           tD           tJ           

59. distance 2
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
               >>         tB           tI           

MODEL SEQUENCE:
             t1           tB             >>         

60. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

61. distance 3
encoding time: 0.02
solving time: 0.11
LOG SEQUENCE:
             t0           t4           t7           t7           tI           t2           t2             >>         tE           tD           tJ           

MODEL SEQUENCE:
             t0           t4             >>         t7           tI           t2             >>         tC           tE           tD           tJ           

62. distance 7
encoding time: 0.02
solving time: 0.93
LOG SEQUENCE:
             t0           t5             >>         tH           tG           tC           t2           tD             >>         tE           tJ             >>         tJ           

MODEL SEQUENCE:
             t0           t5           tG           tH             >>           >>         t2             >>         tC           tE             >>         tD           tJ           

63. distance 3
encoding time: 0.02
solving time: 0.15
LOG SEQUENCE:
             t0           t4           t7             >>         tA           t2           tC           tE           tD           tJ           tJ           

MODEL SEQUENCE:
             t0           t4             >>         t6           tA           t2           tC           tE           tD           tJ             >>         

64. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

65. distance 2
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
               >>         tG           tB           

MODEL SEQUENCE:
             t1             >>         tB           

66. distance 4
encoding time: 0.02
solving time: 0.18
LOG SEQUENCE:
             t6           t0           t4           t2             >>         tA             >>         tC           tE           tD           tJ           

MODEL SEQUENCE:
               >>         t0           t4             >>         t6           tA           t2           tC           tE           tD           tJ           

67. distance 4
encoding time: 0.02
solving time: 0.15
LOG SEQUENCE:
             t0             >>         tG           tH           t2           t5           tE           tC             >>         tD           tJ           

MODEL SEQUENCE:
             t0           t5           tG           tH           t2             >>           >>         tC           tE           tD           tJ           

68. distance 3
encoding time: 0.02
solving time: 0.12
LOG SEQUENCE:
             t0           t5           t5           t3           tG           tH             >>         tF           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t5             >>           >>         tG           tH           t3           tF           tE           tD           tJ           

69. distance 2
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             tB           t1             >>         

MODEL SEQUENCE:
               >>         t1           tB           

70. distance 5
encoding time: 0.02
solving time: 0.29
LOG SEQUENCE:
               >>         tE           t4           t6           tA           t2           tC           tC           tE           t4             >>         tJ           

MODEL SEQUENCE:
             t0             >>         t4           t6           tA           t2           tC             >>         tE             >>         tD           tJ           

71. distance 10
encoding time: 0.02
solving time: 2.08
LOG SEQUENCE:
             t4           t4             >>         tH           t5           t5           tG             >>         t3             >>         tE           tF           t0             >>         tJ           

MODEL SEQUENCE:
               >>           >>         t0             >>           >>         t5           tG           tH           t3           tF           tE             >>           >>         tD           tJ           

72. distance 7
encoding time: 0.02
solving time: 0.56
LOG SEQUENCE:
             t5           t0           t0           t5             >>         tH           t3           t5           tD             >>         tE             >>         tJ           

MODEL SEQUENCE:
               >>         t0             >>         t5           tG           tH           t3             >>           >>         tF           tE           tD           tJ           

73. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

74. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

75. distance 1
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           tB           

MODEL SEQUENCE:
             t1             >>         tB           

76. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

77. distance 3
encoding time: 0.00
solving time: 0.01
LOG SEQUENCE:
             tB           t1           t1             >>         

MODEL SEQUENCE:
               >>           >>         t1           tB           

78. distance 0
encoding time: 0.02
solving time: 0.01
LOG SEQUENCE:
             t0           t5           tG           tH           t3           tF           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t5           tG           tH           t3           tF           tE           tD           tJ           

79. distance 2
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tA             >>         

MODEL SEQUENCE:
             t1             >>         tB           

80. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

81. distance 2
encoding time: 0.02
solving time: 0.07
LOG SEQUENCE:
             t0             >>         t1           tG           tH           t3           tF           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t5             >>         tG           tH           t3           tF           tE           tD           tJ           

82. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

83. distance 6
encoding time: 0.02
solving time: 0.31
LOG SEQUENCE:
             t0           t4           tI           t7             >>         t3             >>         tE           tF           tD           tB             >>         

MODEL SEQUENCE:
             t0           t4             >>         t7           tI           t3           tF           tE             >>         tD             >>         tJ           

84. distance 1
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           tB           

MODEL SEQUENCE:
             t1             >>         tB           

85. distance 3
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             tE           tE             >>         tB           

MODEL SEQUENCE:
               >>           >>         t1           tB           

86. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

87. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

88. distance 2
encoding time: 0.02
solving time: 0.05
LOG SEQUENCE:
               >>         t5           t0           tG           tH           t2           tC           tE           tD           tJ           

MODEL SEQUENCE:
             t0           t5             >>         tG           tH           t2           tC           tE           tD           tJ           

89. distance 9
encoding time: 0.02
solving time: 2.15
LOG SEQUENCE:
             t0           t5           t5             >>         t7           tI           t1           t1           t6             >>           >>         tE           tD           tD           tJ           

MODEL SEQUENCE:
             t0             >>           >>         t4           t7           tI             >>           >>           >>         t3           tF           tE           tD             >>         tJ           

90. distance 2
encoding time: 0.01
solving time: 0.00
LOG SEQUENCE:
             t1           t4             >>         

MODEL SEQUENCE:
             t1             >>         tB           

91. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

92. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

93. distance 1
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           tB           

MODEL SEQUENCE:
             t1             >>         tB           

94. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

95. distance 5
encoding time: 0.02
solving time: 0.24
LOG SEQUENCE:
             t0           t5           tG             >>         t2           tH           tH           tC           tE           tB           tD             >>         

MODEL SEQUENCE:
             t0           t5           tG           tH           t2             >>           >>         tC           tE             >>         tD           tJ           

96. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

97. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

98. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

99. distance 0
encoding time: 0.00
solving time: 0.00
LOG SEQUENCE:
             t1           tB           

MODEL SEQUENCE:
             t1           tB           

encoding time: total 0.90  avg 0.01 median 0.02
solving time:  total 15.70  avg 0.16 median 0.08
timeouts: 0
distance 5: 6
distance 1: 12
distance 4: 6
distance 6: 4
distance 10: 1
distance 2: 18
distance 9: 1
distance 3: 11
distance 0: 36
distance 7: 5