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

0. distance 1
encoding time: 0.02
solving time: 0.25
LOG SEQUENCE:
               >>         t3           t5           tJ           tH           tF           tG           

MODEL SEQUENCE:
             t0           t3           t5           tJ           tH           tF           tG           

1. distance 1
encoding time: 0.01
solving time: 0.03
LOG SEQUENCE:
             t1           tB             >>         tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

2. distance 1
encoding time: 0.01
solving time: 0.06
LOG SEQUENCE:
             t1           tB             >>         tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

3. distance 1
encoding time: 0.01
solving time: 0.02
LOG SEQUENCE:
             t1           tB           tC           tE             >>         

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

4. distance 2
encoding time: 0.07
solving time: 0.08
LOG SEQUENCE:
             t1             >>         tC           tE             >>         

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

5. distance 0
encoding time: 0.01
solving time: 0.01
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.07
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.04
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.01
LOG SEQUENCE:
             t1           tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

10. distance 0
encoding time: 0.01
solving time: 0.01
LOG SEQUENCE:
             t1           tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

11. distance 1
encoding time: 0.01
solving time: 0.05
LOG SEQUENCE:
               >>         tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

12. distance 1
encoding time: 0.02
solving time: 0.09
LOG SEQUENCE:
               >>         tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

13. distance 1
encoding time: 0.01
solving time: 0.05
LOG SEQUENCE:
             t0             >>         tA           tH           tF           tG           

MODEL SEQUENCE:
             t0           t2           tA           tH           tF           tG           

14. distance 0
encoding time: 0.02
solving time: 0.04
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.03
LOG SEQUENCE:
             t0           t3           t5           tJ           tH           tF           tG           

MODEL SEQUENCE:
             t0           t3           t5           tJ           tH           tF           tG           

16. distance 1
encoding time: 0.01
solving time: 0.02
LOG SEQUENCE:
             t0           t2           tA           tH           tF             >>         

MODEL SEQUENCE:
             t0           t2           tA           tH           tF           tG           

17. distance 1
encoding time: 0.01
solving time: 0.03
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.07
LOG SEQUENCE:
             t0           t3           t5           tJ           tH           tF           tG           

MODEL SEQUENCE:
             t0           t3           t5           tJ           tH           tF           tG           

20. distance 2
encoding time: 0.01
solving time: 0.09
LOG SEQUENCE:
               >>           >>         tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

21. distance 1
encoding time: 0.01
solving time: 0.04
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.02
solving time: 0.01
LOG SEQUENCE:
             t1           tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

24. distance 2
encoding time: 0.01
solving time: 0.24
LOG SEQUENCE:
             t0           t3             >>         tI           tH           tF             >>         

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 1
encoding time: 0.02
solving time: 0.14
LOG SEQUENCE:
             t0           t3           t4           tI           tH             >>         tG           

MODEL SEQUENCE:
             t0           t3           t4           tI           tH           tF           tG           

27. distance 1
encoding time: 0.01
solving time: 0.06
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.08
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 0
encoding time: 0.02
solving time: 0.03
LOG SEQUENCE:
             t0           t2           tA           tH           tF           tG           

MODEL SEQUENCE:
             t0           t2           tA           tH           tF           tG           

31. 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           

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: 2.00
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:
             t1           tB           tC             >>         tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

35. distance 2
encoding time: 0.01
solving time: 0.22
LOG SEQUENCE:
             t1           tB             >>         tE             >>         

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

36. distance 0
encoding time: 0.01
solving time: 0.01
LOG SEQUENCE:
             t1           tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

37. distance 1
encoding time: 0.02
solving time: 0.14
LOG SEQUENCE:
             t0           t3           t4           tI           tH           tF             >>         

MODEL SEQUENCE:
             t0           t3           t4           tI           tH           tF           tG           

38. distance 1
encoding time: 0.02
solving time: 0.03
LOG SEQUENCE:
             t0           t2           tA           tH             >>         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 0
encoding time: 0.01
solving time: 0.02
LOG SEQUENCE:
             t1           tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

41. distance 1
encoding time: 0.01
solving time: 0.21
LOG SEQUENCE:
             t0           t2           tA             >>         tF           tG           

MODEL SEQUENCE:
             t0           t2           tA           tH           tF           tG           

42. distance 0
encoding time: 0.02
solving time: 0.03
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 2
encoding time: 0.01
solving time: 0.18
LOG SEQUENCE:
             tJ             >>         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.08
LOG SEQUENCE:
             t1             >>         tC           tE             >>         

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

47. distance 0
encoding time: 0.03
solving time: 0.71
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.07
LOG SEQUENCE:
               >>         tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

50. distance 2
encoding time: 0.01
solving time: 0.26
LOG SEQUENCE:
             t1             >>         tC             >>         tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

51. distance 0
encoding time: 0.02
solving time: 0.03
LOG SEQUENCE:
             t0           t2           tA           tH           tF           tG           

MODEL SEQUENCE:
             t0           t2           tA           tH           tF           tG           

52. distance 1
encoding time: 0.01
solving time: 0.09
LOG SEQUENCE:
             t0           t2           tA           tH             >>         tG           

MODEL SEQUENCE:
             t0           t2           tA           tH           tF           tG           

53. distance 1
encoding time: 0.02
solving time: 0.04
LOG SEQUENCE:
               >>         tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

54. distance 2
encoding time: 0.02
solving time: 0.30
LOG SEQUENCE:
             t0           t3           t5           tJ           tH             >>           >>         

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.01
LOG SEQUENCE:
             t1           tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

57. distance 2
encoding time: 0.01
solving time: 0.09
LOG SEQUENCE:
               >>         tB             >>         tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

58. distance 1
encoding time: 0.02
solving time: 0.05
LOG SEQUENCE:
             t1           tB             >>         tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

59. distance 1
encoding time: 0.01
solving time: 0.03
LOG SEQUENCE:
             t1             >>         tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

60. distance 0
encoding time: 0.02
solving time: 0.09
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.03
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.29
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.02
LOG SEQUENCE:
             t1           tB           tC           tE             >>         

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

64. 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           

65. distance 4
encoding time: 0.01
solving time: 0.30
LOG SEQUENCE:
             t1           t0             >>         tC             >>           >>         

MODEL SEQUENCE:
             t1             >>         tB           tC           tE           tD           

66. distance 1
encoding time: 0.01
solving time: 0.04
LOG SEQUENCE:
             t1             >>         tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

67. distance 1
encoding time: 0.01
solving time: 0.05
LOG SEQUENCE:
             t0           t3             >>         tI           tH           tF           tG           

MODEL SEQUENCE:
             t0           t3           t4           tI           tH           tF           tG           

68. distance 2
encoding time: 0.02
solving time: 1.08
LOG SEQUENCE:
               >>         t2           tA           tH             >>         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           tB             >>         tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

71. distance 1
encoding time: 0.02
solving time: 0.12
LOG SEQUENCE:
             t0           t3           t4           tI             >>         tF           tG           

MODEL SEQUENCE:
             t0           t3           t4           tI           tH           tF           tG           

72. distance 0
encoding time: 0.01
solving time: 0.02
LOG SEQUENCE:
             t0           t2           tA           tH           tF           tG           

MODEL SEQUENCE:
             t0           t2           tA           tH           tF           tG           

73. distance 0
encoding time: 0.02
solving time: 0.01
LOG SEQUENCE:
             t1           tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

74. distance 2
encoding time: 0.01
solving time: 0.07
LOG SEQUENCE:
             t1             >>         tC           tE             >>         

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

75. distance 1
encoding time: 0.02
solving time: 0.65
LOG SEQUENCE:
             t0             >>         t5           tJ           tH           tF           tG           

MODEL SEQUENCE:
             t0           t3           t5           tJ           tH           tF           tG           

76. distance 1
encoding time: 0.02
solving time: 0.14
LOG SEQUENCE:
             t1             >>         tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

77. distance 3
encoding time: 0.01
solving time: 0.25
LOG SEQUENCE:
             t0           t2           tA             >>           >>         tG           tE           

MODEL SEQUENCE:
             t0           t2           tA           tH           tF           tG             >>         

78. distance 1
encoding time: 0.01
solving time: 0.02
LOG SEQUENCE:
               >>         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 0
encoding time: 0.01
solving time: 0.01
LOG SEQUENCE:
             t1           tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

82. distance 1
encoding time: 0.02
solving time: 0.11
LOG SEQUENCE:
             t1           tB             >>         tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

83. distance 0
encoding time: 0.01
solving time: 0.03
LOG SEQUENCE:
             t0           t2           tA           tH           tF           tG           

MODEL SEQUENCE:
             t0           t2           tA           tH           tF           tG           

84. distance 2
encoding time: 0.02
solving time: 0.48
LOG SEQUENCE:
             t0             >>         t4           tI           tH             >>         tG           

MODEL SEQUENCE:
             t0           t3           t4           tI           tH           tF           tG           

85. 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           

86. distance 1
encoding time: 0.01
solving time: 0.02
LOG SEQUENCE:
             t1             >>         tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

87. distance 1
encoding time: 0.01
solving time: 0.02
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.05
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.02
LOG SEQUENCE:
             t1           tB           tC             >>         tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

91. distance 0
encoding time: 0.01
solving time: 0.01
LOG SEQUENCE:
             t1           tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

92. distance 2
encoding time: 0.01
solving time: 0.03
LOG SEQUENCE:
               >>         tB           tC           tE             >>         

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

93. distance 0
encoding time: 0.02
solving time: 0.05
LOG SEQUENCE:
             t0           t2           tA           tH           tF           tG           

MODEL SEQUENCE:
             t0           t2           tA           tH           tF           tG           

94. distance 1
encoding time: 0.02
solving time: 0.28
LOG SEQUENCE:
             t0           t2             >>         tH           tF           tG           

MODEL SEQUENCE:
             t0           t2           tA           tH           tF           tG           

95. distance 1
encoding time: 0.01
solving time: 0.04
LOG SEQUENCE:
             t1           tB           tC             >>         tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

96. distance 0
encoding time: 0.02
solving time: 0.06
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.17
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.16
LOG SEQUENCE:
               >>         tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

99. distance 0
encoding time: 0.01
solving time: 0.02
LOG SEQUENCE:
             t1           tB           tC           tE           tD           

MODEL SEQUENCE:
             t1           tB           tC           tE           tD           

encoding time: total 1.58  avg 0.02 median 0.01
solving time:  total 11.33  avg 0.11 median 0.26
timeouts: 0
distance 2: 14
distance 0: 45
distance 1: 39
distance 4: 1
distance 3: 1